Up to index of Isabelle/HOLCF/IOA
theory CompoScheds(* 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
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·exA)·exB) (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>>sch)·exA·exB) s t = (x, snd a, t)>>(mkex2 A B·sch·(TL·exA)·exB) (snd a) t
theorem mkex2_cons_2:
[| x ∉ act A; x ∈ act B; HD·exB = Def b |] ==> (mkex2 A B·(x>>sch)·exA·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>>sch)·exA·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)))
theorem lemma_2_1a:
filter_act·(Filter_ex2 (asig_of A)·xs) = 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)
theorem Mapfst_mkex_is_sch:
∀exA exB s t. Forall (%x. x ∈ act (A || B)) sch ∧ Filter (%a. a ∈ act A)·sch << filter_act·exA ∧ Filter (%a. a ∈ act B)·sch << 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 A)·sch << filter_act·exA ∧ Filter (%a. a ∈ act B)·sch << 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 A)·sch << filter_act·(snd exA); Filter (%a. a ∈ act B)·sch << 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 A)·sch << filter_act·exA ∧ Filter (%a. a ∈ act B)·sch << 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 A)·sch << filter_act·(snd exA); Filter (%a. a ∈ act B)·sch << 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 A)·sch << filter_act·exA ∧ Filter (%a. a ∈ act B)·sch << filter_act·exB --> Filter_ex2 (asig_of A)·(ProjA2·(snd (mkex A B sch (s, exA) (t, exB)))) = Zip·(Filter (%a. a ∈ act A)·sch)·(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 AB)·sch = filter_act·ex ==> ex = Zip·(Filter (%a. a ∈ act AB)·sch)·(Map snd·ex)
theorem filter_mkex_is_exA:
[| Forall (%a. a ∈ act (A || B)) sch; Filter (%a. a ∈ act A)·sch = filter_act·(snd exA); Filter (%a. a ∈ act B)·sch = 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 A)·sch << filter_act·exA ∧ Filter (%a. a ∈ act B)·sch << filter_act·exB --> Filter_ex2 (asig_of B)·(ProjB2·(snd (mkex A B sch (s, exA) (t, exB)))) = Zip·(Filter (%a. a ∈ act B)·sch)·(Map snd·exB)
theorem filter_mkex_is_exB:
[| Forall (%a. a ∈ act (A || B)) sch; Filter (%a. a ∈ act A)·sch = filter_act·(snd exA); Filter (%a. a ∈ act B)·sch = 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 A)·sch << filter_act·exA ∧ Filter (%a. a ∈ act B)·sch << 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 A)·sch ∈ schedules A ∧ Filter (%a. a ∈ act B)·sch ∈ schedules B ∧ Forall (%x. x ∈ act (A || B)) sch)
theorem compositionality_sch_modules:
Scheds (A || B) = par_scheds (Scheds A) (Scheds B)