Theory CompoScheds

theory CompoScheds
imports CompoExecs
```(*  Title:      HOL/HOLCF/IOA/CompoScheds.thy
Author:     Olaf MÃ¼ller
*)

section ‹Compositionality on Schedule level›

theory CompoScheds
imports CompoExecs
begin

definition mkex2 :: "('a, 's) ioa ⇒ ('a, 't) ioa ⇒ 'a Seq →
('a, 's) pairs → ('a, 't) pairs → ('s ⇒ 't ⇒ ('a, 's × 't) pairs)"
where "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))))))"

definition mkex :: "('a, 's) ioa ⇒ ('a, 't) ioa ⇒ 'a Seq ⇒
('a, 's) execution ⇒ ('a, 't) execution ⇒ ('a, 's × 't) execution"
where "mkex A B sch exA exB =
((fst exA, fst exB), (mkex2 A B ⋅ sch ⋅ (snd exA) ⋅ (snd exB)) (fst exA) (fst exB))"

definition par_scheds :: "'a schedule_module ⇒ 'a schedule_module ⇒ 'a schedule_module"
where "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} ∩
{sch. Filter (%a. a:actions sigB)⋅sch : schB} ∩
{sch. Forall (%x. x:(actions sigA Un actions sigB)) sch},
asig_comp sigA sigB))"

subsection ‹‹mkex› rewrite rules›

lemma 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)))))"
apply (rule trans)
apply (rule fix_eq2)
apply (simp only: mkex2_def)
apply (rule beta_cfun)
apply simp
done

lemma mkex2_UU: "(mkex2 A B ⋅ UU ⋅ exA ⋅ exB) s t = UU"
apply (subst mkex2_unfold)
apply simp
done

lemma mkex2_nil: "(mkex2 A B ⋅ nil ⋅ exA ⋅ exB) s t = nil"
apply (subst mkex2_unfold)
apply simp
done

lemma 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"
apply (rule trans)
apply (subst mkex2_unfold)
done

lemma 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)"
apply (rule trans)
apply (subst mkex2_unfold)
done

lemma 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)"
apply (rule trans)
apply (subst mkex2_unfold)
done

declare mkex2_UU [simp] mkex2_nil [simp] mkex2_cons_1 [simp]
mkex2_cons_2 [simp] mkex2_cons_3 [simp]

subsection ‹‹mkex››

lemma mkex_UU: "mkex A B UU  (s,exA) (t,exB) = ((s,t),UU)"

lemma mkex_nil: "mkex A B nil (s,exA) (t,exB) = ((s,t),nil)"

lemma 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)))"
apply (unfold mkex_def)
apply (cut_tac exA = "a ↝ exA" in mkex2_cons_1)
apply auto
done

lemma 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)))"
apply (unfold mkex_def)
apply (cut_tac exB = "b↝exB" in mkex2_cons_2)
apply auto
done

lemma 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)))"
apply (unfold mkex_def)
apply (cut_tac exB = "b↝exB" and exA = "a↝exA" in mkex2_cons_3)
apply auto
done

declare mkex2_UU [simp del] mkex2_nil [simp del]
mkex2_cons_1 [simp del] mkex2_cons_2 [simp del] mkex2_cons_3 [simp del]

lemmas composch_simps = mkex_UU mkex_nil mkex_cons_1 mkex_cons_2 mkex_cons_3

declare composch_simps [simp]

subsection ‹Compositionality on schedule level›

subsubsection ‹Lemmas for ‹⟹››

lemma lemma_2_1a:
― ‹‹tfilter ex› and ‹filter_act› are commutative›
"filter_act ⋅ (Filter_ex2 (asig_of A) ⋅ xs) =
Filter (λa. a ∈ act A) ⋅ (filter_act ⋅ xs)"
apply (unfold filter_act_def Filter_ex2_def)
done

lemma lemma_2_1b:
― ‹State-projections do not affect ‹filter_act››
"filter_act ⋅ (ProjA2 ⋅ xs) = filter_act ⋅ xs ∧
filter_act ⋅ (ProjB2 ⋅ xs) = filter_act ⋅ xs"
by (pair_induct xs)

text ‹
Schedules of ‹A ∥ B› have only ‹A›- or ‹B›-actions.

Very similar to ‹lemma_1_1c›, but it is not checking if every action element
of an ‹ex› is in ‹A› or ‹B›, but after projecting it onto the action
schedule. Of course, this is the same proposition, but we cannot change this
one, when then rather ‹lemma_1_1c›.
›

lemma sch_actions_in_AorB:
"∀s. is_exec_frag (A ∥ B) (s, xs) ⟶ Forall (λx. x ∈ act (A ∥ B)) (filter_act ⋅ xs)"
apply (pair_induct xs simp: is_exec_frag_def Forall_def sforall_def)
text ‹main case›
apply auto
apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
done

subsubsection ‹Lemmas for ‹⟸››

text ‹
Filtering actions out of ‹mkex (sch, exA, exB)› yields the oracle ‹sch›
structural induction.
›

lemma 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"
apply (Seq_induct sch simp: Filter_def Forall_def sforall_def mkex_def)

text ‹main case: splitting into 4 cases according to ‹a ∈ A›, ‹a ∈ B››
apply auto

text ‹Case ‹y ∈ A›, ‹y ∈ B››
apply (Seq_case_simp exA)
text ‹Case ‹exA = UU›, Case ‹exA = nil››
text ‹
These ‹UU› and ‹nil› cases are the only places where the assumption
‹filter A sch ⊑ f_act exA› is used!
‹⟶› to generate a contradiction using ‹¬ a ↝ ss ⊑ UU nil›,
using theorems ‹Cons_not_less_UU› and ‹Cons_not_less_nil›.›
apply (Seq_case_simp exB)
text ‹Case ‹exA = a ↝ x›, ‹exB = b ↝ y››
text ‹
Here it is important that @{method Seq_case_simp} uses no ‹!full!_simp_tac›
for the cons case, as otherwise ‹mkex_cons_3› would not be rewritten
without use of ‹rotate_tac›: then tactic would not be generally
applicable.›
apply simp

text ‹Case ‹y ∈ A›, ‹y ∉ B››
apply (Seq_case_simp exA)
apply simp

text ‹Case ‹y ∉ A›, ‹y ∈ B››
apply (Seq_case_simp exB)
apply simp

text ‹Case ‹y ∉ A›, ‹y ∉ B››
done

text ‹Generalizing the proof above to a proof method:›
ML ‹
fun mkex_induct_tac ctxt sch exA exB =
EVERY' [
Seq_induct_tac ctxt sch
@{thms Filter_def Forall_def sforall_def mkex_def stutter_def},
asm_full_simp_tac ctxt,
SELECT_GOAL
(safe_tac (Context.raw_transfer (Proof_Context.theory_of ctxt) @{theory_context Fun})),
Seq_case_simp_tac ctxt exA,
Seq_case_simp_tac ctxt exB,
asm_full_simp_tac ctxt,
Seq_case_simp_tac ctxt exA,
asm_full_simp_tac ctxt,
Seq_case_simp_tac ctxt exB,
asm_full_simp_tac ctxt,
asm_full_simp_tac (ctxt addsimps @{thms asig_of_par actions_asig_comp})]
›

method_setup mkex_induct = ‹
Scan.lift (Args.embedded -- Args.embedded -- Args.embedded)
>> (fn ((sch, exA), exB) => fn ctxt =>
SIMPLE_METHOD' (mkex_induct_tac ctxt sch exA exB))
›

text ‹
Projection of ‹mkex (sch, exA, exB)› onto ‹A› stutters on ‹A›
structural induction.
›

lemma 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))))"
by (mkex_induct sch exA exB)

lemma 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))"
apply (cut_tac stutterA_mkex)
apply (simp add: stutter_def ProjA_def mkex_def)
apply (erule allE)+
apply (drule mp)
prefer 2 apply (assumption)
apply simp
done

text ‹
Projection of ‹mkex (sch, exA, exB)› onto ‹B› stutters on ‹B›
structural induction.
›

lemma 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))))"
by (mkex_induct sch exA exB)

lemma 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))"
apply (cut_tac stutterB_mkex)
apply (simp add: stutter_def ProjB_def mkex_def)
apply (erule allE)+
apply (drule mp)
prefer 2 apply (assumption)
apply simp
done

text ‹
Filter of ‹mkex (sch, exA, exB)› to ‹A› after projection onto ‹A› is ‹exA›,
using ‹zip ⋅ (proj1 ⋅ exA) ⋅ (proj2 ⋅ exA)› instead of ‹exA›,
because of admissibility problems structural induction.
›

lemma 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)"
by (mkex_induct sch exB exA)

text ‹
‹zip ⋅ (proj1 ⋅ y) ⋅ (proj2 ⋅ y) = y›  (using the lift operations)
›

lemma Zip_Map_fst_snd: "Zip ⋅ (Map fst ⋅ y) ⋅ (Map snd ⋅ y) = y"
by (Seq_induct y)

text ‹
‹filter A ⋅ sch = proj1 ⋅ ex ⟶ zip ⋅ (filter A ⋅ sch) ⋅ (proj2 ⋅ ex) = ex›
lemma for eliminating non admissible equations in assumptions
›

lemma 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)"
apply (rule Zip_Map_fst_snd [symmetric])
done

text ‹
Filter of ‹mkex (sch, exA, exB)› to ‹A› after projection onto ‹A› is ‹exA›
using the above trick.
›

lemma 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"
apply (pair exA)
apply (pair exB)
apply (rule conjI)
apply (simplesubst trick_against_eq_in_ass)
back
apply assumption
done

text ‹
Filter of ‹mkex (sch, exA, exB)› to ‹B› after projection onto ‹B› is ‹exB›
using ‹zip ⋅ (proj1 ⋅ exB) ⋅ (proj2 ⋅ exB)› instead of ‹exB›
because of admissibility problems structural induction.
›

lemma 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)"
(*notice necessary change of arguments exA and exB*)
by (mkex_induct sch exA exB)

text ‹
Filter of ‹mkex (sch, exA, exB)› to ‹A› after projection onto ‹B› is ‹exB›
using the above trick.
›

lemma 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"
apply (pair exA)
apply (pair exB)
apply (rule conjI)
apply (simplesubst trick_against_eq_in_ass)
back
apply assumption
done

lemma mkex_actions_in_AorB:
― ‹‹mkex› has only ‹A›- or ‹B›-actions›
"∀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)))"
by (mkex_induct sch exA 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"
apply auto
text ‹‹⟹››
apply (rule_tac x = "Filter_ex (asig_of A) (ProjA ex)" in bexI)
prefer 2
apply (simp (no_asm) add: Filter_ex_def ProjA_def lemma_2_1a lemma_2_1b)
apply (rule_tac x = "Filter_ex (asig_of B) (ProjB ex)" in bexI)
prefer 2
apply (simp add: Filter_ex_def ProjB_def lemma_2_1a lemma_2_1b)
apply (pair ex)
apply (erule conjE)
text ‹‹⟸››
text ‹‹mkex› is exactly the construction of ‹exA∥B› out of ‹exA›, ‹exB›,
and the oracle ‹sch›, we need here›
apply (rename_tac exA exB)
apply (rule_tac x = "mkex A B sch exA exB" in bexI)
text ‹‹mkex› actions are just the oracle›
apply (pair exA)
apply (pair exB)
text ‹‹mkex› is an execution -- use compositionality on ex-level›
apply (simp add: stutter_mkex_on_A stutter_mkex_on_B filter_mkex_is_exB filter_mkex_is_exA)
apply (pair exA)
apply (pair exB)
done

theorem compositionality_sch_modules:
"Scheds (A ∥ B) = par_scheds (Scheds A) (Scheds B)"
apply (unfold Scheds_def par_scheds_def)