Theory CompoScheds

Up to index of Isabelle/HOLCF/IOA

theory CompoScheds
imports CompoExecs
uses [CompoScheds.ML]
begin

(*  Title:      HOLCF/IOA/meta_theory/CompoScheds.thy
    ID:         $Id: CompoScheds.thy,v 1.9 2005/09/02 15:24:00 wenzelm Exp $
    Author:     Olaf Müller
*)

header {* Compositionality on Schedule level *}

theory CompoScheds
imports CompoExecs
begin

consts

 mkex     ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq =>
              ('a,'s)execution => ('a,'t)execution =>('a,'s*'t)execution"
 mkex2    ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq ->
              ('a,'s)pairs -> ('a,'t)pairs ->
              ('s => 't => ('a,'s*'t)pairs)"
 par_scheds ::"['a schedule_module,'a schedule_module] => 'a schedule_module"


defs

mkex_def:
  "mkex A B sch exA exB ==
       ((fst exA,fst exB),
        (mkex2 A B$sch$(snd exA)$(snd exB)) (fst exA) (fst exB))"

mkex2_def:
  "mkex2 A B == (fix$(LAM h sch exA exB. (%s t. case sch of
       nil => nil
    | x##xs =>
      (case x of
        UU => UU
      | Def y =>
         (if y:act A then
             (if y:act B then
                (case HD$exA of
                   UU => UU
                 | Def a => (case HD$exB of
                              UU => UU
                            | Def b =>
                   (y,(snd a,snd b))>>
                     (h$xs$(TL$exA)$(TL$exB)) (snd a) (snd b)))
              else
                (case HD$exA of
                   UU => UU
                 | Def a =>
                   (y,(snd a,t))>>(h$xs$(TL$exA)$exB) (snd a) t)
              )
          else
             (if y:act B then
                (case HD$exB of
                   UU => UU
                 | Def b =>
                   (y,(s,snd b))>>(h$xs$exA$(TL$exB)) s (snd b))
             else
               UU
             )
         )
       ))))"

par_scheds_def:
  "par_scheds SchedsA SchedsB ==
       let schA = fst SchedsA; sigA = snd SchedsA;
           schB = fst SchedsB; sigB = snd SchedsB
       in
       (    {sch. Filter (%a. a:actions sigA)$sch : schA}
        Int {sch. Filter (%a. a:actions sigB)$sch : schB}
        Int {sch. Forall (%x. x:(actions sigA Un actions sigB)) sch},
        asig_comp sigA sigB)"

ML {* use_legacy_bindings (the_context ()) *}

end

mkex rewrite rules

theorem mkex2_unfold:

  mkex2 A B =
  (LAM sch exA exB.
      (%s t. case sch of nil => nil
             | x ## xs =>
                 case x of UU => UU
                 | Def y =>
                     if y ∈ act A
                     then if y ∈ act B
                          then case HD·exA of UU => UU
                               | Def a =>
                                   case HD·exB of UU => UU
                                   | Def b =>
                                       (y, snd a, snd b)
                                       >>(mkex2 A B·xs·(TL·exA)·(TL·exB)) (snd a)
  (snd b)
                          else case HD·exA of UU => UU
                               | Def a =>
                                   (y, snd a, t)
                                   >>(mkex2 A B·xs·(TL·exAexB) (snd a) t
                     else if y ∈ act B
                          then case HD·exB of UU => UU
                               | Def b =>
                                   (y, s, snd b)
                                   >>(mkex2 A B·xs·exA·(TL·exB)) s (snd b)
                          else UU))

theorem mkex2_UU:

  (mkex2 A B·UU·exA·exB) s t = UU

theorem mkex2_nil:

  (mkex2 A B·nil·exA·exB) s t = nil

theorem mkex2_cons_1:

  [| x ∈ act A; x ∉ act B; HD·exA = Def a |]
  ==> (mkex2 A B·(x>>schexA·exB) s t =
      (x, snd a, t)>>(mkex2 A B·sch·(TL·exAexB) (snd a) t

theorem mkex2_cons_2:

  [| x ∉ act A; x ∈ act B; HD·exB = Def b |]
  ==> (mkex2 A B·(x>>schexA·exB) s t =
      (x, s, snd b)>>(mkex2 A B·sch·exA·(TL·exB)) s (snd b)

theorem mkex2_cons_3:

  [| x ∈ act A; x ∈ act B; HD·exA = Def a; HD·exB = Def b |]
  ==> (mkex2 A B·(x>>schexA·exB) s t =
      (x, snd a, snd b)>>(mkex2 A B·sch·(TL·exA)·(TL·exB)) (snd a) (snd b)

theorem mkex_UU:

  mkex A B UU (s, exA) (t, exB) = ((s, t), UU)

theorem mkex_nil:

  mkex A B nil (s, exA) (t, exB) = ((s, t), nil)

theorem mkex_cons_1:

  [| x ∈ act A; x ∉ act B |]
  ==> mkex A B (x>>sch) (s, a>>exA) (t, exB) =
      ((s, t), (x, snd a, t)>>snd (mkex A B sch (snd a, exA) (t, exB)))

theorem mkex_cons_2:

  [| x ∉ act A; x ∈ act B |]
  ==> mkex A B (x>>sch) (s, exA) (t, b>>exB) =
      ((s, t), (x, s, snd b)>>snd (mkex A B sch (s, exA) (snd b, exB)))

theorem mkex_cons_3:

  [| x ∈ act A; x ∈ act B |]
  ==> mkex A B (x>>sch) (s, a>>exA) (t, b>>exB) =
      ((s, t), (x, snd a, snd b)>>snd (mkex A B sch (snd a, exA) (snd b, exB)))

Lemmas for ==>

theorem lemma_2_1a:

  filter_act·(Filter_ex2 (asig_of Axs) = Filter (%a. a ∈ act A)·(filter_act·xs)

theorem lemma_2_1b:

  filter_act·(ProjA2·xs) = filter_act·xs ∧ filter_act·(ProjB2·xs) = filter_act·xs

theorem sch_actions_in_AorB:

s. is_exec_frag (A || B) (s, xs) -->
      Forall (%x. x ∈ act (A || B)) (filter_act·xs)

Lemmas for <==

theorem Mapfst_mkex_is_sch:

exA exB s t.
     Forall (%x. x ∈ act (A || B)) sch ∧
     Filter (%a. a ∈ act Asch << filter_act·exA ∧
     Filter (%a. a ∈ act Bsch << filter_act·exB -->
     filter_act·(snd (mkex A B sch (s, exA) (t, exB))) = sch

theorem stutterA_mkex:

exA exB s t.
     Forall (%x. x ∈ act (A || B)) sch ∧
     Filter (%a. a ∈ act Asch << filter_act·exA ∧
     Filter (%a. a ∈ act Bsch << filter_act·exB -->
     stutter (asig_of A) (s, ProjA2·(snd (mkex A B sch (s, exA) (t, exB))))

theorem stutter_mkex_on_A:

  [| Forall (%x. x ∈ act (A || B)) sch;
     Filter (%a. a ∈ act Asch << filter_act·(snd exA);
     Filter (%a. a ∈ act Bsch << filter_act·(snd exB) |]
  ==> stutter (asig_of A) (ProjA (mkex A B sch exA exB))

theorem stutterB_mkex:

exA exB s t.
     Forall (%x. x ∈ act (A || B)) sch ∧
     Filter (%a. a ∈ act Asch << filter_act·exA ∧
     Filter (%a. a ∈ act Bsch << filter_act·exB -->
     stutter (asig_of B) (t, ProjB2·(snd (mkex A B sch (s, exA) (t, exB))))

theorem stutter_mkex_on_B:

  [| Forall (%x. x ∈ act (A || B)) sch;
     Filter (%a. a ∈ act Asch << filter_act·(snd exA);
     Filter (%a. a ∈ act Bsch << filter_act·(snd exB) |]
  ==> stutter (asig_of B) (ProjB (mkex A B sch exA exB))

theorem filter_mkex_is_exA_tmp:

exA exB s t.
     Forall (%x. x ∈ act (A || B)) sch ∧
     Filter (%a. a ∈ act Asch << filter_act·exA ∧
     Filter (%a. a ∈ act Bsch << filter_act·exB -->
     Filter_ex2 (asig_of A)·(ProjA2·(snd (mkex A B sch (s, exA) (t, exB)))) =
     Zip·(Filter (%a. a ∈ act Asch)·(Map snd·exA)

theorem Zip_Map_fst_snd:

  Zip·(Map fst·y)·(Map snd·y) = y

theorem trick_against_eq_in_ass:

  Filter (%a. a ∈ act ABsch = filter_act·ex
  ==> ex = Zip·(Filter (%a. a ∈ act ABsch)·(Map snd·ex)

theorem filter_mkex_is_exA:

  [| Forall (%a. a ∈ act (A || B)) sch;
     Filter (%a. a ∈ act Asch = filter_act·(snd exA);
     Filter (%a. a ∈ act Bsch = filter_act·(snd exB) |]
  ==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA

theorem filter_mkex_is_exB_tmp:

exA exB s t.
     Forall (%x. x ∈ act (A || B)) sch ∧
     Filter (%a. a ∈ act Asch << filter_act·exA ∧
     Filter (%a. a ∈ act Bsch << filter_act·exB -->
     Filter_ex2 (asig_of B)·(ProjB2·(snd (mkex A B sch (s, exA) (t, exB)))) =
     Zip·(Filter (%a. a ∈ act Bsch)·(Map snd·exB)

theorem filter_mkex_is_exB:

  [| Forall (%a. a ∈ act (A || B)) sch;
     Filter (%a. a ∈ act Asch = filter_act·(snd exA);
     Filter (%a. a ∈ act Bsch = filter_act·(snd exB) |]
  ==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB

theorem mkex_actions_in_AorB:

s t exA exB.
     Forall (%x. x ∈ act (A || B)) sch ∧
     Filter (%a. a ∈ act Asch << filter_act·exA ∧
     Filter (%a. a ∈ act Bsch << filter_act·exB -->
     Forall (%x. fst x ∈ act (A || B)) (snd (mkex A B sch (s, exA) (t, exB)))

theorem compositionality_sch:

  (sch ∈ schedules (A || B)) =
  (Filter (%a. a ∈ act Asch ∈ schedules A ∧
   Filter (%a. a ∈ act Bsch ∈ schedules B ∧ Forall (%x. x ∈ act (A || B)) sch)

theorem compositionality_sch_modules:

  Scheds (A || B) = par_scheds (Scheds A) (Scheds B)