Quelle  CompoScheds.thy

(*  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)
  apply (simp add: Consq_def If_and_if)
  apply (simp add: Consq_def)
  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)
  apply (simp add: Consq_def If_and_if)
  apply (simp add: Consq_def)
  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)
  apply (simp add: Consq_def If_and_if)
  apply (simp add: Consq_def)
  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)"
  by (simp add: mkex_def)

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

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)
  apply (simp add: MapFilter o_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›\›
  apply (simp add: asig_of_par actions_asig_comp)
  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) 🍋‹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 (Parse.embedded -- Parse.embedded -- Parse.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 for admissibility problems
 ›

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 (simp add: filter_act_def)
  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 (simp add: ProjA_def Filter_ex_def)
  apply (pair exA)
  apply (pair exB)
  apply (rule conjI)
  apply (simp (no_asm) add: mkex_def)
  apply (simplesubst trick_against_eq_in_ass)
  back
  apply assumption
  apply (simp add: filter_mkex_is_exA_tmp)
  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)› t
  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 (simp add: ProjB_def Filter_ex_def)
  apply (pair exA)
  apply (pair exB)
  apply (rule conjI)
  apply (simp add: mkex_def)
  apply (simplesubst trick_against_eq_in_ass)
  back
  apply assumption
  apply (simp add: filter_mkex_is_exB_tmp)
  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 (simp add: schedules_def has_schedule_def)
  apply auto
  text ‹‹==>›\   apply (rule_tac x = "Filter_ex (asig_of A) (ProjA ex)" in bexI)
  prefer 2
  apply (simp add: compositionality_ex)
  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: compositionality_ex)
  apply (simp add: Filter_ex_def ProjB_def lemma_2_1a lemma_2_1b)
  apply (simp add: executions_def)
  apply (pair ex)
  apply (erule conjE)
  apply (simp add: sch_actions_in_AorB)
  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)
  apply (simp add: Mapfst_mkex_is_sch)
  text ‹‹mkex› is an execution -- use compositionality on ex-level›
  apply (simp add: compositionality_ex)
  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)
  apply (simp add: mkex_actions_in_AorB)
  done

theorem compositionality_sch_modules:
  "Scheds (A ∥ B) = par_scheds (Scheds A) (Scheds B)"
  apply (unfold Scheds_def par_scheds_def)
  apply (simp add: asig_of_par)
  apply (rule set_eqI)
  apply (simp add: compositionality_sch actions_of_par)
  done

declare compoex_simps [simp del]
declare composch_simps [simp del]

end