(*  Title:      HOL/HOLCF/IOA/CompoScheds.thy
    Author:     Olaf Müller
*)

section \<open>Compositionality on Schedule level\<close>

theory CompoScheds
imports CompoExecs
begin

definition mkex2 :: "('a, 's) ioa \<Rightarrow> ('a, 't) ioa \<Rightarrow> 'a Seq \<rightarrow>
  ('a, 's) pairs \<rightarrow> ('a, 't) pairs \<rightarrow> ('s \<Rightarrow> 't \<Rightarrow> ('a, 's \<times> 't) pairs)"
  where "mkex2 A B =
    (fix \<cdot>
      (LAM h sch exA exB.
        (\<lambda>s t.
          case sch of
            nil \<Rightarrow> nil
        | x ## xs \<Rightarrow>
            (case x of
              UU \<Rightarrow> UU
            | Def y \<Rightarrow>
               (if y \<in> act A then
                 (if y \<in> act B then
                    (case HD \<cdot> exA of
                      UU \<Rightarrow> UU
                    | Def a \<Rightarrow>
                        (case HD \<cdot> exB of
                          UU \<Rightarrow> UU
                        | Def b \<Rightarrow>
                           (y, (snd a, snd b)) \<leadsto>
                            (h \<cdot> xs \<cdot> (TL \<cdot> exA) \<cdot> (TL \<cdot> exB)) (snd a) (snd b)))
                  else
                    (case HD \<cdot> exA of
                      UU \<Rightarrow> UU
                    | Def a \<Rightarrow> (y, (snd a, t)) \<leadsto> (h \<cdot> xs \<cdot> (TL \<cdot> exA) \<cdot> exB) (snd a) t))
                else
                  (if y \<in> act B then
                    (case HD \<cdot> exB of
                      UU \<Rightarrow> UU
                    | Def b \<Rightarrow> (y, (s, snd b)) \<leadsto> (h \<cdot> xs \<cdot> exA \<cdot> (TL \<cdot> exB)) s (snd b))
                   else UU))))))"

definition mkex :: "('a, 's) ioa \<Rightarrow> ('a, 't) ioa \<Rightarrow> 'a Seq \<Rightarrow>
    ('a, 's) execution \<Rightarrow> ('a, 't) execution \<Rightarrow> ('a, 's \<times> 't) execution"
  where "mkex A B sch exA exB =
    ((fst exA, fst exB), (mkex2 A B \<cdot> sch \<cdot> (snd exA) \<cdot> (snd exB)) (fst exA) (fst exB))"

definition par_scheds :: "'a schedule_module \<Rightarrow> 'a schedule_module \<Rightarrow> 'a schedule_module"
  where "par_scheds SchedsA SchedsB =
    (let
      schA = fst SchedsA; sigA = snd SchedsA;
      schB = fst SchedsB; sigB = snd SchedsB
     in
      ({sch. Filter (\<lambda>a. a\<in>actions sigA)\<cdot>sch \<in> schA} \<inter>
       {sch. Filter (\<lambda>a. a\<in>actions sigB)\<cdot>sch \<in> schB} \<inter>
       {sch. Forall (\<lambda>x. x\<in>(actions sigA Un actions sigB)) sch},
        asig_comp sigA sigB))"


subsection \<open>\<open>mkex\<close> rewrite rules\<close>

lemma mkex2_unfold:
  "mkex2 A B =
    (LAM sch exA exB.
      (\<lambda>s t.
        case sch of
          nil \<Rightarrow> nil
        | x ## xs \<Rightarrow>
            (case x of
              UU \<Rightarrow> UU
            | Def y \<Rightarrow>
                (if y \<in> act A then
                  (if y \<in> act B then
                    (case HD \<cdot> exA of
                      UU \<Rightarrow> UU
                    | Def a \<Rightarrow>
                        (case HD \<cdot> exB of
                          UU \<Rightarrow> UU
                        | Def b \<Rightarrow>
                            (y, (snd a, snd b)) \<leadsto>
                              (mkex2 A B \<cdot> xs \<cdot> (TL \<cdot> exA) \<cdot> (TL \<cdot> exB)) (snd a) (snd b)))
                   else
                     (case HD \<cdot> exA of
                       UU \<Rightarrow> UU
                     | Def a \<Rightarrow> (y, (snd a, t)) \<leadsto> (mkex2 A B \<cdot> xs \<cdot> (TL \<cdot> exA) \<cdot> exB) (snd a) t))
                 else
                   (if y \<in> act B then
                     (case HD \<cdot> exB of
                       UU \<Rightarrow> UU
                     | Def b \<Rightarrow> (y, (s, snd b)) \<leadsto> (mkex2 A B \<cdot> xs \<cdot> exA \<cdot> (TL \<cdot> 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 \<cdot> UU \<cdot> exA \<cdot> exB) s t = UU"
  apply (subst mkex2_unfold)
  apply simp
  done

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

lemma mkex2_cons_1:
  "x \<in> act A \<Longrightarrow> x \<notin> act B \<Longrightarrow> HD \<cdot> exA = Def a \<Longrightarrow>
    (mkex2 A B \<cdot> (x \<leadsto> sch) \<cdot> exA \<cdot> exB) s t =
      (x, snd a,t) \<leadsto> (mkex2 A B \<cdot> sch \<cdot> (TL \<cdot> exA) \<cdot> 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 \<notin> act A \<Longrightarrow> x \<in> act B \<Longrightarrow> HD \<cdot> exB = Def b \<Longrightarrow>
    (mkex2 A B \<cdot> (x \<leadsto> sch) \<cdot> exA \<cdot> exB) s t =
      (x, s, snd b) \<leadsto> (mkex2 A B \<cdot> sch \<cdot> exA \<cdot> (TL \<cdot> 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 \<in> act A \<Longrightarrow> x \<in> act B \<Longrightarrow> HD \<cdot> exA = Def a \<Longrightarrow> HD \<cdot> exB = Def b \<Longrightarrow>
    (mkex2 A B \<cdot> (x \<leadsto> sch) \<cdot> exA \<cdot> exB) s t =
      (x, snd a,snd b) \<leadsto> (mkex2 A B \<cdot> sch \<cdot> (TL \<cdot> exA) \<cdot> (TL \<cdot> 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 \<open>\<open>mkex\<close>\<close>

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 \<in> act A \<Longrightarrow> x \<notin> act B \<Longrightarrow>
    mkex A B (x \<leadsto> sch) (s, a \<leadsto> exA) (t, exB) =
      ((s, t), (x, snd a, t) \<leadsto> snd (mkex A B sch (snd a, exA) (t, exB)))"
  apply (unfold mkex_def)
  apply (cut_tac exA = "a \<leadsto> exA" in mkex2_cons_1)
  apply auto
  done

lemma mkex_cons_2:
  "x \<notin> act A \<Longrightarrow> x \<in> act B \<Longrightarrow>
    mkex A B (x \<leadsto> sch) (s, exA) (t, b \<leadsto> exB) =
      ((s, t), (x, s, snd b) \<leadsto> snd (mkex A B sch (s, exA) (snd b, exB)))"
  apply (unfold mkex_def)
  apply (cut_tac exB = "b\<leadsto>exB" in mkex2_cons_2)
  apply auto
  done

lemma mkex_cons_3:
  "x \<in> act A \<Longrightarrow> x \<in> act B \<Longrightarrow>
    mkex A B (x \<leadsto> sch) (s, a \<leadsto> exA) (t, b \<leadsto> exB) =
      ((s, t), (x, snd a, snd b) \<leadsto> snd (mkex A B sch (snd a, exA) (snd b, exB)))"
  apply (unfold mkex_def)
  apply (cut_tac exB = "b\<leadsto>exB" and exA = "a\<leadsto>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 \<open>Compositionality on schedule level\<close>

subsubsection \<open>Lemmas for \<open>\<Longrightarrow>\<close>\<close>

lemma lemma_2_1a:
  \<comment> \<open>\<open>tfilter ex\<close> and \<open>filter_act\<close> are commutative\<close>
  "filter_act \<cdot> (Filter_ex2 (asig_of A) \<cdot> xs) =
    Filter (\<lambda>a. a \<in> act A) \<cdot> (filter_act \<cdot> xs)"
  apply (unfold filter_act_def Filter_ex2_def)
  apply (simp add: MapFilter o_def)
  done

lemma lemma_2_1b:
  \<comment> \<open>State-projections do not affect \<open>filter_act\<close>\<close>
  "filter_act \<cdot> (ProjA2 \<cdot> xs) = filter_act \<cdot> xs \<and>
    filter_act \<cdot> (ProjB2 \<cdot> xs) = filter_act \<cdot> xs"
  by (pair_induct xs)


text \<open>
  Schedules of \<open>A \<parallel> B\<close> have only \<open>A\<close>- or \<open>B\<close>-actions.

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

lemma sch_actions_in_AorB:
  "\<forall>s. is_exec_frag (A \<parallel> B) (s, xs) \<longrightarrow> Forall (\<lambda>x. x \<in> act (A \<parallel> B)) (filter_act \<cdot> xs)"
  apply (pair_induct xs simp: is_exec_frag_def Forall_def sforall_def)
  text \<open>main case\<close>
  apply auto
  apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
  done


subsubsection \<open>Lemmas for \<open>\<Longleftarrow>\<close>\<close>

text \<open>
  Filtering actions out of \<open>mkex (sch, exA, exB)\<close> yields the oracle \<open>sch\<close>
  structural induction.
\<close>

lemma Mapfst_mkex_is_sch:
  "\<forall>exA exB s t.
    Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and>
    Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exA \<and>
    Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exB \<longrightarrow>
    filter_act \<cdot> (snd (mkex A B sch (s, exA) (t, exB))) = sch"
  apply (Seq_induct sch simp: Filter_def Forall_def sforall_def mkex_def)

  text \<open>main case: splitting into 4 cases according to \<open>a \<in> A\<close>, \<open>a \<in> B\<close>\<close>
  apply auto

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

  text \<open>Case \<open>y \<in> A\<close>, \<open>y \<notin> B\<close>\<close>
  apply (Seq_case_simp exA)
  apply simp

  text \<open>Case \<open>y \<notin> A\<close>, \<open>y \<in> B\<close>\<close>
  apply (Seq_case_simp exB)
  apply simp

  text \<open>Case \<open>y \<notin> A\<close>, \<open>y \<notin> B\<close>\<close>
  apply (simp add: asig_of_par actions_asig_comp)
  done


text \<open>Generalizing the proof above to a proof method:\<close>
ML \<open>
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})]
\<close>

method_setup mkex_induct = \<open>
  Scan.lift (Args.embedded -- Args.embedded -- Args.embedded)
    >> (fn ((sch, exA), exB) => fn ctxt =>
      SIMPLE_METHOD' (mkex_induct_tac ctxt sch exA exB))
\<close>


text \<open>
  Projection of \<open>mkex (sch, exA, exB)\<close> onto \<open>A\<close> stutters on \<open>A\<close>
  structural induction.
\<close>

lemma stutterA_mkex:
  "\<forall>exA exB s t.
    Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and>
    Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exA \<and>
    Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exB \<longrightarrow>
    stutter (asig_of A) (s, ProjA2 \<cdot> (snd (mkex A B sch (s, exA) (t, exB))))"
  by (mkex_induct sch exA exB)

lemma stutter_mkex_on_A:
  "Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<Longrightarrow>
    Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<sqsubseteq> filter_act \<cdot> (snd exA) \<Longrightarrow>
    Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> (snd exB) \<Longrightarrow>
    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 \<open>
  Projection of \<open>mkex (sch, exA, exB)\<close> onto \<open>B\<close> stutters on \<open>B\<close>
  structural induction.
\<close>

lemma stutterB_mkex:
  "\<forall>exA exB s t.
    Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and>
    Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exA \<and>
    Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exB \<longrightarrow>
    stutter (asig_of B) (t, ProjB2 \<cdot> (snd (mkex A B sch (s, exA) (t, exB))))"
  by (mkex_induct sch exA exB)


lemma stutter_mkex_on_B:
  "Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<Longrightarrow>
   Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<sqsubseteq> filter_act \<cdot> (snd exA) \<Longrightarrow>
   Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> (snd exB) \<Longrightarrow>
   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 \<open>
  Filter of \<open>mkex (sch, exA, exB)\<close> to \<open>A\<close> after projection onto \<open>A\<close> is \<open>exA\<close>,
  using \<open>zip \<cdot> (proj1 \<cdot> exA) \<cdot> (proj2 \<cdot> exA)\<close> instead of \<open>exA\<close>,
  because of admissibility problems structural induction.
\<close>

lemma filter_mkex_is_exA_tmp:
  "\<forall>exA exB s t.
    Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and>
    Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exA \<and>
    Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exB \<longrightarrow>
    Filter_ex2 (asig_of A) \<cdot> (ProjA2 \<cdot> (snd (mkex A B sch (s, exA) (t, exB)))) =
      Zip \<cdot> (Filter (\<lambda>a. a \<in> act A) \<cdot> sch) \<cdot> (Map snd \<cdot> exA)"
  by (mkex_induct sch exB exA)

text \<open>
  \<open>zip \<cdot> (proj1 \<cdot> y) \<cdot> (proj2 \<cdot> y) = y\<close>  (using the lift operations)
  lemma for admissibility problems
\<close>

lemma Zip_Map_fst_snd: "Zip \<cdot> (Map fst \<cdot> y) \<cdot> (Map snd \<cdot> y) = y"
  by (Seq_induct y)


text \<open>
  \<open>filter A \<cdot> sch = proj1 \<cdot> ex \<longrightarrow> zip \<cdot> (filter A \<cdot> sch) \<cdot> (proj2 \<cdot> ex) = ex\<close>
  lemma for eliminating non admissible equations in assumptions
\<close>

lemma trick_against_eq_in_ass:
  "Filter (\<lambda>a. a \<in> act AB) \<cdot> sch = filter_act \<cdot> ex \<Longrightarrow>
    ex = Zip \<cdot> (Filter (\<lambda>a. a \<in> act AB) \<cdot> sch) \<cdot> (Map snd \<cdot> ex)"
  apply (simp add: filter_act_def)
  apply (rule Zip_Map_fst_snd [symmetric])
  done

text \<open>
  Filter of \<open>mkex (sch, exA, exB)\<close> to \<open>A\<close> after projection onto \<open>A\<close> is \<open>exA\<close>
  using the above trick.
\<close>

lemma filter_mkex_is_exA:
  "Forall (\<lambda>a. a \<in> act (A \<parallel> B)) sch \<Longrightarrow>
    Filter (\<lambda>a. a \<in> act A) \<cdot> sch = filter_act \<cdot> (snd exA) \<Longrightarrow>
    Filter (\<lambda>a. a \<in> act B) \<cdot> sch = filter_act \<cdot> (snd exB) \<Longrightarrow>
  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 \<open>
  Filter of \<open>mkex (sch, exA, exB)\<close> to \<open>B\<close> after projection onto \<open>B\<close> is \<open>exB\<close>
  using \<open>zip \<cdot> (proj1 \<cdot> exB) \<cdot> (proj2 \<cdot> exB)\<close> instead of \<open>exB\<close>
  because of admissibility problems structural induction.
\<close>

lemma filter_mkex_is_exB_tmp:
  "\<forall>exA exB s t.
    Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and>
    Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exA \<and>
    Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exB \<longrightarrow>
    Filter_ex2 (asig_of B) \<cdot> (ProjB2 \<cdot> (snd (mkex A B sch (s, exA) (t, exB)))) =
      Zip \<cdot> (Filter (\<lambda>a. a \<in> act B) \<cdot> sch) \<cdot> (Map snd \<cdot> exB)"
  (*notice necessary change of arguments exA and exB*)
  by (mkex_induct sch exA exB)

text \<open>
  Filter of \<open>mkex (sch, exA, exB)\<close> to \<open>A\<close> after projection onto \<open>B\<close> is \<open>exB\<close>
  using the above trick.
\<close>

lemma filter_mkex_is_exB:
  "Forall (\<lambda>a. a \<in> act (A \<parallel> B)) sch \<Longrightarrow>
    Filter (\<lambda>a. a \<in> act A) \<cdot> sch = filter_act \<cdot> (snd exA) \<Longrightarrow>
    Filter (\<lambda>a. a \<in> act B) \<cdot> sch = filter_act \<cdot> (snd exB) \<Longrightarrow>
    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:
  \<comment> \<open>\<open>mkex\<close> has only \<open>A\<close>- or \<open>B\<close>-actions\<close>
  "\<forall>s t exA exB.
    Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch &
    Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exA \<and>
    Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exB \<longrightarrow>
    Forall (\<lambda>x. fst x \<in> act (A \<parallel> B)) (snd (mkex A B sch (s, exA) (t, exB)))"
  by (mkex_induct sch exA exB)


theorem compositionality_sch:
  "sch \<in> schedules (A \<parallel> B) \<longleftrightarrow>
    Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<in> schedules A \<and>
    Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<in> schedules B \<and>
    Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch"
  apply (simp add: schedules_def has_schedule_def)
  apply auto
  text \<open>\<open>\<Longrightarrow>\<close>\<close>
  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 \<open>\<open>\<Longleftarrow>\<close>\<close>
  text \<open>\<open>mkex\<close> is exactly the construction of \<open>exA\<parallel>B\<close> out of \<open>exA\<close>, \<open>exB\<close>,
    and the oracle \<open>sch\<close>, we need here\<close>
  apply (rename_tac exA exB)
  apply (rule_tac x = "mkex A B sch exA exB" in bexI)
  text \<open>\<open>mkex\<close> actions are just the oracle\<close>
  apply (pair exA)
  apply (pair exB)
  apply (simp add: Mapfst_mkex_is_sch)
  text \<open>\<open>mkex\<close> is an execution -- use compositionality on ex-level\<close>
  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 \<parallel> 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