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

section ‹Compositionality on Trace level›

theory CompoTraces
imports CompoScheds ShortExecutions
begin

definition mksch ::
    "('a, 's) ioa → ('a, 't) ioa → 'a Seq → 'a Seq → 'a Seq → 'a Seq"
  where "mksch A B =
    (fix ⋅
      (LAM h tr schA schB.
        case tr of
          nil → nil
        | x ## xs →
            (case x of
              UU → UU
            | Def y →
                (if y ∈ act A then
                  (if y ∈ act B then
                    ((Takewhile (λa. a ∈ int A) ⋅ schA) @@
                     (Takewhile (λa. a ∈ int B) ⋅ schB) @@
                     (y ↝ (h ⋅ xs ⋅ (TL ⋅ (Dropwhile (λa. a ∈ int A) ⋅ schA))
                                   ⋅ (TL ⋅ (Dropwhile (λa. a ∈ int B) ⋅ schB)))))
                   else
                    ((Takewhile (λa. a ∈ int A) ⋅ schA) @@
                     (y ↝ (h ⋅ xs ⋅ (TL ⋅ (Dropwhile (λa. a ∈ int A) ⋅ schA)) ⋅ schB))))
                 else
                  (if y ∈ act B then
                    ((Takewhile (λa. a ∈ int B) ⋅ schB) @@
                     (y ↝ (h ⋅ xs ⋅ schA ⋅ (TL ⋅ (Dropwhile (λa. a ∈ int B) ⋅ schB)))))
                   else UU)))))"

definition par_traces :: "'a trace_module → 'a trace_module → 'a trace_module"
  where "par_traces TracesA TracesB =
    (let
      trA = fst TracesA; sigA = snd TracesA;
      trB = fst TracesB; sigB = snd TracesB
     in
       ({tr. Filter (λa. a ∈ actions sigA) ⋅ tr ∈ trA} ∩
        {tr. Filter (λa. a ∈ actions sigB) ⋅ tr ∈ trB} ∩
        {tr. Forall (λx. x ∈ externals sigA ∪ externals sigB) tr},
        asig_comp sigA sigB))"

axiomatization where
  finiteR_mksch: "Finite (mksch A B ⋅ tr ⋅ x ⋅ y) ==> Finite tr"

lemma finiteR_mksch': "¬ Finite tr ==> ¬ Finite (mksch A B ⋅ tr ⋅ x ⋅ y)"
  by (blast intro: finiteR_mksch)


declaration ‹fn _ => Simplifier.map_ss (Simplifier.set_mksym (K (K NONE)))›


subsection "mksch rewrite rules"

lemma mksch_unfold:
  "mksch A B =
    (LAM tr schA schB.
      case tr of
        nil → nil
      | x ## xs →
          (case x of
            UU → UU
          | Def y →
              (if y ∈ act A then
                (if y ∈ act B then
                  ((Takewhile (λa. a ∈ int A) ⋅ schA) @@
                   (Takewhile (λa. a ∈ int B) ⋅ schB) @@
                   (y ↝ (mksch A B ⋅ xs ⋅(TL ⋅ (Dropwhile (λa. a ∈ int A) ⋅ schA))
                                         ⋅(TL ⋅ (Dropwhile (λa. a ∈ int B) ⋅ schB)))))
                 else
                  ((Takewhile (λa. a ∈ int A) ⋅ schA) @@
                   (y ↝ (mksch A B ⋅ xs ⋅ (TL ⋅ (Dropwhile (λa. a ∈ int A) ⋅ schA)) ⋅ schB))))
               else
                (if y ∈ act B then
                  ((Takewhile (λa. a ∈ int B) ⋅ schB) @@
                   (y ↝ (mksch A B ⋅ xs ⋅ schA ⋅ (TL ⋅ (Dropwhile (λa. a ∈ int B) ⋅ schB)))))
                 else UU))))"
  apply (rule trans)
  apply (rule fix_eq4)
  apply (rule mksch_def)
  apply (rule beta_cfun)
  apply simp
  done

lemma mksch_UU: "mksch A B ⋅ UU ⋅ schA ⋅ schB = UU"
  apply (subst mksch_unfold)
  apply simp
  done

lemma mksch_nil: "mksch A B ⋅ nil ⋅ schA ⋅ schB = nil"
  apply (subst mksch_unfold)
  apply simp
  done

lemma mksch_cons1:
  "x ∈ act A ==> x ∉ act B ==>
    mksch A B ⋅ (x ↝ tr) ⋅ schA ⋅ schB =
      (Takewhile (λa. a ∈ int A) ⋅ schA) @@
      (x ↝ (mksch A B ⋅ tr ⋅ (TL ⋅ (Dropwhile (λa. a ∈ int A) ⋅ schA)) ⋅ schB))"
  apply (rule trans)
  apply (subst mksch_unfold)
  apply (simp add: Consq_def If_and_if)
  apply (simp add: Consq_def)
  done

lemma mksch_cons2:
  "x ∉ act A ==> x ∈ act B ==>
    mksch A B ⋅ (x ↝ tr) ⋅ schA ⋅ schB =
      (Takewhile (λa. a ∈ int B) ⋅ schB) @@
      (x ↝ (mksch A B ⋅ tr ⋅ schA ⋅ (TL ⋅ (Dropwhile (λa. a ∈ int B) ⋅ schB))))"
  apply (rule trans)
  apply (subst mksch_unfold)
  apply (simp add: Consq_def If_and_if)
  apply (simp add: Consq_def)
  done

lemma mksch_cons3:
  "x ∈ act A ==> x ∈ act B ==>
    mksch A B ⋅ (x ↝ tr) ⋅ schA ⋅ schB =
      (Takewhile (λa. a ∈ int A) ⋅ schA) @@
      ((Takewhile (λa. a ∈ int B) ⋅ schB) @@
      (x ↝ (mksch A B ⋅ tr ⋅ (TL ⋅ (Dropwhile (λa. a ∈ int A) ⋅ schA))
                            ⋅ (TL ⋅ (Dropwhile (λa. a ∈ int B) ⋅ schB)))))"
  apply (rule trans)
  apply (subst mksch_unfold)
  apply (simp add: Consq_def If_and_if)
  apply (simp add: Consq_def)
  done

lemmas compotr_simps = mksch_UU mksch_nil mksch_cons1 mksch_cons2 mksch_cons3

declare compotr_simps [simp]


subsection ‹COMPOSITIONALITY on TRACE Level›

subsubsection "Lemmata for ‹==>›"

text ‹
  Consequence out of ‹ext1_ext2_is_not_act1(2)›, which in turn are
  consequences out of the compatibility of IOA, in particular out of the
  condition that internals are really hidden.
\<close>

lemma compatibility_consequence1: " eB ∧ ¬ eA ⟶ ¬ A) ⟶ A ∧ (eA ∨ eB) ⟷ eA ∧ A"
 by fast


(* very similar to above, only the commutativity of | is used to make a slight change *)
lemma compatibility_consequence2: "(eB ∧ ¬ eA ⟶ ¬ A) ⟶ A ∧ (eB ∨ eA) ⟷ eA ∧ A"
  by fast


subsubsection ‹Lemmata for ‹<==››

(* Lemma for substitution of looping assumption in another specific assumption *)
lemma subst_lemma1: "f ⊑ g x ==> x = h x ==> f ⊑ g (h x)"
  by (erule subst)

(* Lemma for substitution of looping assumption in another specific assumption *)
lemma subst_lemma2: "(f x) = y ↝ g ==> x = h x ==> f (h x) = y ↝ g"
  by (erule subst)

lemma ForallAorB_mksch [rule_format]:
  "compatible A B ==>
    ∀schA schB. Forall (λx. x ∈ act (A ∥ B)) tr ⟶
      Forall (λx. x ∈ act (A ∥ B)) (mksch A B ⋅ tr ⋅ schA ⋅ schB)"
  apply (Seq_induct tr simp: Forall_def sforall_def mksch_def)
  apply auto
  apply (simp add: actions_of_par)
  apply (case_tac "a ∈ act A")
  apply (case_tac "a ∈ act B")
  text ‹‹a ∈ A›, ‹a ∈ B››
  apply simp
  apply (rule Forall_Conc_impl [THEN mp])
  apply (simp add: intA_is_not_actB int_is_act)
  apply (rule Forall_Conc_impl [THEN mp])
  apply (simp add: intA_is_not_actB int_is_act)
  text ‹‹a ∈ A›, ‹a ∉ B››
  apply simp
  apply (rule Forall_Conc_impl [THEN mp])
  apply (simp add: intA_is_not_actB int_is_act)
  apply (case_tac "a∈act B")
  text ‹‹a ∉ A›, ‹a ∈ B››
  apply simp
  apply (rule Forall_Conc_impl [THEN mp])
  apply (simp add: intA_is_not_actB int_is_act)
  text ‹‹a ∉ A›, ‹a ∉ B››
  apply auto
  done

lemma ForallBnAmksch [rule_format]:
  "compatible B A ==>
    ∀schA schB. Forall (λx. x ∈ act B ∧ x ∉ act A) tr ⟶
      Forall (λx. x ∈ act B ∧ x ∉ act A) (mksch A B ⋅ tr ⋅ schA ⋅ schB)"
  apply (Seq_induct tr simp: Forall_def sforall_def mksch_def)
  apply auto
  apply (rule Forall_Conc_impl [THEN mp])
  apply (simp add: intA_is_not_actB int_is_act)
  done

lemma ForallAnBmksch [rule_format]:
  "compatible A B ==>
    ∀schA schB. Forall (λx. x ∈ act A ∧ x ∉ act B) tr ⟶
      Forall (λx. x ∈ act A ∧ x ∉ act B) (mksch A B ⋅ tr ⋅ schA ⋅ schB)"
  apply (Seq_induct tr simp: Forall_def sforall_def mksch_def)
  apply auto
  apply (rule Forall_Conc_impl [THEN mp])
  apply (simp add: intA_is_not_actB int_is_act)
  done

(* safe_tac makes too many case distinctions with this lemma in the next proof *)
declare FiniteConc [simp del]

lemma FiniteL_mksch [rule_format]:
  "Finite tr ==> is_asig (asig_of A) ==> is_asig (asig_of B) ==>
    ∀x y.
      Forall (λx. x ∈ act A) x ∧ Forall (λx. x ∈ act B) y ∧
      Filter (λa. a ∈ ext A) ⋅ x = Filter (λa. a ∈ act A) ⋅ tr ∧
      Filter (λa. a ∈ ext B) ⋅ y = Filter (λa. a ∈ act B) ⋅ tr ∧
      Forall (λx. x ∈ ext (A ∥ B)) tr ⟶ Finite (mksch A B ⋅ tr ⋅ x ⋅ y)"
  apply (erule Seq_Finite_ind)
  apply simp
  text ‹main case›
  apply simp
  apply auto

  text ‹‹a ∈ act A›; ‹a ∈ act B››
  apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
  apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
  back
  apply (erule conjE)+
  text ‹‹Finite (tw iA x)› and ‹Finite (tw iB y)››
  apply (simp add: not_ext_is_int_or_not_act FiniteConc)
  text ‹now for conclusion IH applicable, but assumptions have to be transformed›
  apply (drule_tac x = "x" and g = "Filter (λa. a ∈ act A) ⋅ s" in subst_lemma2)
  apply assumption
  apply (drule_tac x = "y" and g = "Filter (λa. a ∈ act B) ⋅ s" in subst_lemma2)
  apply assumption
  text ‹IH›
  apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)

  text ‹‹a ∈ act B›; ‹a ∉ act A››
  apply (frule sym [THEN eq_imp_below, THEN divide_Seq])

  apply (erule conjE)+
  text ‹‹Finite (tw iB y)››
  apply (simp add: not_ext_is_int_or_not_act FiniteConc)
  text ‹now for conclusion IH applicable, but assumptions have to be transformed›
  apply (drule_tac x = "y" and g = "Filter (λa. a ∈ act B) ⋅ s" in subst_lemma2)
  apply assumption
  text ‹IH›
  apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)

  text ‹‹a ∉ act B›; ‹a ∈ act A››
  apply (frule sym [THEN eq_imp_below, THEN divide_Seq])

  apply (erule conjE)+
  text ‹‹Finite (tw iA x)››
  apply (simp add: not_ext_is_int_or_not_act FiniteConc)
  text ‹now for conclusion IH applicable, but assumptions have to be transformed›
  apply (drule_tac x = "x" and g = "Filter (λa. a ∈ act A) ⋅ s" in subst_lemma2)
  apply assumption
  text ‹IH›
  apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)

  text ‹‹a ∉ act B›; ‹a ∉ act A››
  apply (fastforce intro!: ext_is_act simp: externals_of_par)
  done

declare FiniteConc [simp]

declare FilterConc [simp del]

lemma reduceA_mksch1 [rule_format]:
  "Finite bs ==> is_asig (asig_of A) ==> is_asig (asig_of B) ==> compatible A B ==>
    ∀y. Forall (λx. x ∈ act B) y ∧ Forall (λx. x ∈ act B ∧ x ∉ act A) bs ∧
      Filter (λa. a ∈ ext B) ⋅ y = Filter (λa. a ∈ act B) ⋅ (bs @@ z) ⟶
      (∃y1 y2.
        (mksch A B ⋅ (bs @@ z) ⋅ x ⋅ y) = (y1 @@ (mksch A B ⋅ z ⋅ x ⋅ y2)) ∧
        Forall (λx. x ∈ act B ∧ x ∉ act A) y1 ∧
        Finite y1 ∧ y = (y1 @@ y2) ∧
        Filter (λa. a ∈ ext B) ⋅ y1 = bs)"
  apply (frule_tac A1 = "A" in compat_commute [THEN iffD1])
  apply (erule Seq_Finite_ind)
  apply (rule allI)+
  apply (rule impI)
  apply (rule_tac x = "nil" in exI)
  apply (rule_tac x = "y" in exI)
  apply simp
  text ‹main case›
  apply (rule allI)+
  apply (rule impI)
  apply simp
  apply (erule conjE)+
  apply simp
  text ‹‹divide_Seq› on ‹s››
  apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
  apply (erule conjE)+
  text ‹transform assumption ‹f eB y = f B (s @ z)››
  apply (drule_tac x = "y" and g = "Filter (λa. a ∈ act B) ⋅ (s @@ z) " in subst_lemma2)
  apply assumption
  apply (simp add: not_ext_is_int_or_not_act FilterConc)
  text ‹apply IH›
  apply (erule_tac x = "TL ⋅ (Dropwhile (λa. a ∈ int B) ⋅ y)" in allE)
  apply (simp add: ForallTL ForallDropwhile FilterConc)
  apply (erule exE)+
  apply (erule conjE)+
  apply (simp add: FilterConc)
  text ‹for replacing IH in conclusion›
  apply (rotate_tac -2)
  text ‹instantiate ‹y1a› and ‹y2a››
  apply (rule_tac x = "Takewhile (λa. a ∈ int B) ⋅ y @@ a ↝ y1" in exI)
  apply (rule_tac x = "y2" in exI)
  text ‹elminate all obligations up to two depending on ‹Conc_assoc››
  apply (simp add: intA_is_not_actB int_is_act int_is_not_ext FilterConc)
  apply (simp add: Conc_assoc FilterConc)
  done

lemmas reduceA_mksch = conjI [THEN [6] conjI [THEN [5] reduceA_mksch1]]

lemma reduceB_mksch1 [rule_format]:
  "Finite a_s ==> is_asig (asig_of A) ==> is_asig (asig_of B) ==> compatible A B ==>
    ∀x. Forall (λx. x ∈ act A) x ∧ Forall (λx. x ∈ act A ∧ x ∉ act B) a_s ∧
      Filter (λa. a ∈ ext A) ⋅ x = Filter (λa. a ∈ act A) ⋅ (a_s @@ z) ⟶
      (∃x1 x2.
        (mksch A B ⋅ (a_s @@ z) ⋅ x ⋅ y) = (x1 @@ (mksch A B ⋅ z ⋅ x2 ⋅ y)) ∧
        Forall (λx. x ∈ act A ∧ x ∉ act B) x1 ∧
        Finite x1 ∧ x = (x1 @@ x2) ∧
        Filter (λa. a ∈ ext A) ⋅ x1 = a_s)"
  apply (frule_tac A1 = "A" in compat_commute [THEN iffD1])
  apply (erule Seq_Finite_ind)
  apply (rule allI)+
  apply (rule impI)
  apply (rule_tac x = "nil" in exI)
  apply (rule_tac x = "x" in exI)
  apply simp
  text ‹main case›
  apply (rule allI)+
  apply (rule impI)
  apply simp
  apply (erule conjE)+
  apply simp
  text ‹‹divide_Seq› on ‹s››
  apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
  apply (erule conjE)+
  text ‹transform assumption ‹f eA x = f A (s @ z)››
  apply (drule_tac x = "x" and g = "Filter (λa. a ∈ act A) ⋅ (s @@ z)" in subst_lemma2)
  apply assumption
  apply (simp add: not_ext_is_int_or_not_act FilterConc)
  text ‹apply IH›
  apply (erule_tac x = "TL ⋅ (Dropwhile (λa. a ∈ int A) ⋅ x)" in allE)
  apply (simp add: ForallTL ForallDropwhile FilterConc)
  apply (erule exE)+
  apply (erule conjE)+
  apply (simp add: FilterConc)
  text ‹for replacing IH in conclusion›
  apply (rotate_tac -2)
  text ‹instantiate ‹y1a› and ‹y2a››
  apply (rule_tac x = "Takewhile (λa. a ∈ int A) ⋅ x @@ a ↝ x1" in exI)
  apply (rule_tac x = "x2" in exI)
  text ‹eliminate all obligations up to two depending on ‹Conc_assoc››
  apply (simp add: intA_is_not_actB int_is_act int_is_not_ext FilterConc)
  apply (simp add: Conc_assoc FilterConc)
  done

lemmas reduceB_mksch = conjI [THEN [6] conjI [THEN [5] reduceB_mksch1]]

declare FilterConc [simp]


subsection ‹Filtering external actions out of ‹mksch (tr, schA, schB)› yields the oracle ‹tr››

lemma FilterA_mksch_is_tr:
  "compatible A B ==> compatible B A ==> is_asig (asig_of A) ==> is_asig (asig_of B) ==>
    ∀schA schB.
      Forall (λx. x ∈ act A) schA ∧
      Forall (λx. x ∈ act B) schB ∧
      Forall (λx. x ∈ ext (A ∥ B)) tr ∧
      Filter (λa. a ∈ act A) ⋅ tr ⊑ Filter (λa. a ∈ ext A) ⋅ schA ∧
      Filter (λa. a ∈ act B) ⋅ tr ⊑ Filter (λa. a ∈ ext B) ⋅ schB
      ⟶ Filter (λa. a ∈ ext (A ∥ B)) ⋅ (mksch A B ⋅ tr ⋅ schA ⋅ schB) = tr"
  apply (Seq_induct tr simp: Forall_def sforall_def mksch_def)
  text ‹main case›
  text ‹splitting into 4 cases according to ‹a ∈ A›, ‹a ∈ B››
  apply auto

  text ‹Case ‹a ∈ A›, ‹a ∈ B››
  apply (frule divide_Seq)
  apply (frule divide_Seq)
  back
  apply (erule conjE)+
  text ‹filtering internals of ‹A› in ‹schA› and of ‹B› in ‹schB› is ‹nil››
  apply (simp add: not_ext_is_int_or_not_act externals_of_par intA_is_not_extB int_is_not_ext)
  text ‹conclusion of IH ok, but assumptions of IH have to be transformed›
  apply (drule_tac x = "schA" in subst_lemma1)
  apply assumption
  apply (drule_tac x = "schB" in subst_lemma1)
  apply assumption
  text ‹IH›
  apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)

  text ‹Case ‹a ∈ A›, ‹a ∉ B››
  apply (frule divide_Seq)
  apply (erule conjE)+
  text ‹filtering internals of ‹A› is ‹nil››
  apply (simp add: not_ext_is_int_or_not_act externals_of_par intA_is_not_extB int_is_not_ext)
  apply (drule_tac x = "schA" in subst_lemma1)
  apply assumption
  apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)

  text ‹Case ‹a ∈ B›, ‹a ∉ A››
  apply (frule divide_Seq)
  apply (erule conjE)+
  text ‹filtering internals of ‹A› is ‹nil››
  apply (simp add: not_ext_is_int_or_not_act externals_of_par intA_is_not_extB int_is_not_ext)
  apply (drule_tac x = "schB" in subst_lemma1)
  back
  apply assumption
  apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)

  text ‹Case ‹a ∉ A›, ‹a ∉ B››
  apply (fastforce intro!: ext_is_act simp: externals_of_par)
  done


subsection" Filter of mksch(tr,schA,schB) to A is schA -- take lemma proof"

lemma FilterAmksch_is_schA:
  "compatible A B ==> compatible B A ==> is_asig (asig_of A) ==> is_asig (asig_of B) ==>
    Forall (λx. x ∈ ext (A ∥ B)) tr ∧
    Forall (λx. x ∈ act A) schA ∧
    Forall (λx. x ∈ act B) schB ∧
    Filter (λa. a ∈ ext A) ⋅ schA = Filter (λa. a ∈ act A) ⋅ tr ∧
    Filter (λa. a ∈ ext B) ⋅ schB = Filter (λa. a ∈ act B) ⋅ tr ∧
    LastActExtsch A schA ∧ LastActExtsch B schB
    ⟶ Filter (λa. a ∈ act A) ⋅ (mksch A B ⋅ tr ⋅ schA ⋅ schB) = schA"
  apply (intro strip)
  apply (rule seq.take_lemma)
  apply (rule mp)
  prefer 2 apply assumption
  back back back back
  apply (rule_tac x = "schA" in spec)
  apply (rule_tac x = "schB" in spec)
  apply (rule_tac x = "tr" in spec)
  apply (tactic "thin_tac' context 5 1")
  apply (rule nat_less_induct)
  apply (rule allI)+
  apply (rename_tac tr schB schA)
  apply (intro strip)
  apply (erule conjE)+

  apply (case_tac "Forall (λx. x ∈ act B ∧ x ∉ act A) tr")

  apply (rule seq_take_lemma [THEN iffD2, THEN spec])
  apply (tactic "thin_tac' context 5 1")


  apply (case_tac "Finite tr")

  text ‹both sides of this equation are ‹nil››
  apply (subgoal_tac "schA = nil")
  apply simp
  text ‹first side: ‹mksch = nil››
  apply (auto intro!: ForallQFilterPnil ForallBnAmksch FiniteL_mksch)[1]
  text ‹second side: ‹schA = nil››
  apply (erule_tac A = "A" in LastActExtimplnil)
  apply simp
  apply (erule_tac Q = "λx. x ∈ act B ∧ x ∉ act A" in ForallQFilterPnil)
  apply assumption
  apply fast

  text ‹case ‹¬ Finite s››

  text ‹both sides of this equation are ‹UU››
  apply (subgoal_tac "schA = UU")
  apply simp
  text ‹first side: ‹mksch = UU››
  apply (auto intro!: ForallQFilterPUU finiteR_mksch' ForallBnAmksch)[1]
  text ‹‹schA = UU››
  apply (erule_tac A = "A" in LastActExtimplUU)
  apply simp
  apply (erule_tac Q = "λx. x ∈ act B ∧ x ∉ act A" in ForallQFilterPUU)
  apply assumption
  apply fast

  text ‹case ‹¬ Forall (λx. x ∈ act B ∧ x ∉ act A) s››

  apply (drule divide_Seq3)

  apply (erule exE)+
  apply (erule conjE)+
  apply hypsubst

  text ‹bring in lemma ‹reduceA_mksch››
  apply (frule_tac x = "schA" and y = "schB" and A = "A" and B = "B" in reduceA_mksch)
  apply assumption+
  apply (erule exE)+
  apply (erule conjE)+

  text ‹use ‹reduceA_mksch› to rewrite conclusion›
  apply hypsubst
  apply simp

  text ‹eliminate the ‹B›-only prefix›

  apply (subgoal_tac "(Filter (λa. a ∈ act A) ⋅ y1) = nil")
  apply (erule_tac [2] ForallQFilterPnil)
  prefer 2 apply assumption
  prefer 2 apply fast

  text ‹Now real recursive step follows (in ‹y›)›

  apply simp
  apply (case_tac "x ∈ act A")
  apply (case_tac "x ∉ act B")
  apply (rotate_tac -2)
  apply simp

  apply (subgoal_tac "Filter (λa. a ∈ act A ∧ a ∈ ext B) ⋅ y1 = nil")
  apply (rotate_tac -1)
  apply simp
  text ‹eliminate introduced subgoal 2›
  apply (erule_tac [2] ForallQFilterPnil)
  prefer 2 apply assumption
  prefer 2 apply fast

  text ‹bring in ‹divide_Seq› for ‹s››
  apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
  apply (erule conjE)+

  text ‹subst ‹divide_Seq› in conclusion, but only at the rightest occurrence›
  apply (rule_tac t = "schA" in ssubst)
  back
  back
  back
  apply assumption

  text ‹reduce trace_takes from ‹n› to strictly smaller ‹k››
  apply (rule take_reduction)

  text ‹‹f A (tw iA) = tw ¬ eA››
  apply (simp add: int_is_act not_ext_is_int_or_not_act)
  apply (rule refl)
  apply (simp add: int_is_act not_ext_is_int_or_not_act)
  apply (rotate_tac -11)

  text ‹now conclusion fulfills induction hypothesis, but assumptions are not ready›

  text ‹assumption ‹Forall tr››
  text ‹assumption ‹schB››
  apply (simp add: ext_and_act)
  text ‹assumption ‹schA››
  apply (drule_tac x = "schA" and g = "Filter (λa. a ∈ act A) ⋅ rs" in subst_lemma2)
  apply assumption
  apply (simp add: int_is_not_ext)
  text ‹assumptions concerning ‹LastActExtsch›, cannot be rewritten, as ‹LastActExtsmalli› are looping›
  apply (drule_tac sch = "schA" and P = "λa. a ∈ int A" in LastActExtsmall1)
  apply (frule_tac ?sch1.0 = "y1" in LastActExtsmall2)
  apply assumption

  text ‹assumption ‹Forall schA››
  apply (drule_tac s = "schA" and P = "Forall (λx. x ∈ act A) " in subst)
  apply assumption
  apply (simp add: int_is_act)

  text ‹case ‹x ∈ actions (asig_of A) ∧ x ∈ actions (asig_of B)››

  apply (rotate_tac -2)
  apply simp

  apply (subgoal_tac "Filter (λa. a ∈ act A ∧ a ∈ ext B) ⋅ y1 = nil")
  apply (rotate_tac -1)
  apply simp
  text ‹eliminate introduced subgoal 2›
  apply (erule_tac [2] ForallQFilterPnil)
  prefer 2 apply assumption
  prefer 2 apply fast

  text ‹bring in ‹divide_Seq› for ‹s››
  apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
  apply (erule conjE)+

  text ‹subst ‹divide_Seq› in conclusion, but only at the rightmost occurrence›
  apply (rule_tac t = "schA" in ssubst)
  back
  back
  back
  apply assumption

  text ‹‹f A (tw iA) = tw ¬ eA››
  apply (simp add: int_is_act not_ext_is_int_or_not_act)

  text ‹rewrite assumption forall and ‹schB››
  apply (rotate_tac 13)
  apply (simp add: ext_and_act)

  text ‹‹divide_Seq› for ‹schB2››
  apply (frule_tac y = "y2" in sym [THEN eq_imp_below, THEN divide_Seq])
  apply (erule conjE)+
  text ‹assumption ‹schA››
  apply (drule_tac x = "schA" and g = "Filter (λa. a∈act A) ⋅rs" in subst_lemma2)
  apply assumption
  apply (simp add: int_is_not_ext)

  text ‹‹f A (tw iB schB2) = nil››
  apply (simp add: int_is_not_ext not_ext_is_int_or_not_act intA_is_not_actB)


  text ‹reduce trace_takes from ‹n› to strictly smaller ‹k››
  apply (rule take_reduction)
  apply (rule refl)
  apply (rule refl)

  text ‹now conclusion fulfills induction hypothesis, but assumptions are not all ready›

  text ‹assumption ‹schB››
  apply (drule_tac x = "y2" and g = "Filter (λa. a ∈ act B) ⋅ rs" in subst_lemma2)
  apply assumption
  apply (simp add: intA_is_not_actB int_is_not_ext)

  text ‹conclusions concerning ‹LastActExtsch›, cannot be rewritten, as ‹LastActExtsmalli› are looping›
  apply (drule_tac sch = "schA" and P = "λa. a ∈ int A" in LastActExtsmall1)
  apply (frule_tac ?sch1.0 = "y1" in LastActExtsmall2)
  apply assumption
  apply (drule_tac sch = "y2" and P = "λa. a ∈ int B" in LastActExtsmall1)

  text ‹assumption ‹Forall schA›, and ‹Forall schA› are performed by ‹ForallTL›, ‹ForallDropwhile››
  apply (simp add: ForallTL ForallDropwhile)

  text ‹case ‹x ∉ A ∧ x ∈ B››
  text ‹cannot occur, as just this case has been scheduled out before as the ‹B›-only prefix›
  apply (case_tac "x ∈ act B")
  apply fast

  text ‹case ‹x ∉ A ∧ x ∉ B››
  text ‹cannot occur because of assumption: ‹Forall (a ∈ ext A ∨ a ∈ ext B)››
  apply (rotate_tac -9)
  text ‹reduce forall assumption from ‹tr› to ‹x ↝ rs››
  apply (simp add: externals_of_par)
  apply (fast intro!: ext_is_act)
  done


subsection ‹Filter of ‹mksch (tr, schA, schB)› to ‹B› is ‹schB› -- take lemma proof›

lemma FilterBmksch_is_schB:
  "compatible A B ==> compatible B A ==> is_asig (asig_of A) ==> is_asig (asig_of B) ==>
    Forall (λx. x ∈ ext (A ∥ B)) tr ∧
    Forall (λx. x ∈ act A) schA ∧
    Forall (λx. x ∈ act B) schB ∧
    Filter (λa. a ∈ ext A) ⋅ schA = Filter (λa. a ∈ act A) ⋅ tr ∧
    Filter (λa. a ∈ ext B) ⋅ schB = Filter (λa. a ∈ act B) ⋅ tr ∧
    LastActExtsch A schA ∧ LastActExtsch B schB
    ⟶ Filter (λa. a ∈ act B) ⋅ (mksch A B ⋅ tr ⋅ schA ⋅ schB) = schB"
  apply (intro strip)
  apply (rule seq.take_lemma)
  apply (rule mp)
  prefer 2 apply assumption
  back back back back
  apply (rule_tac x = "schA" in spec)
  apply (rule_tac x = "schB" in spec)
  apply (rule_tac x = "tr" in spec)
  apply (tactic "thin_tac' context 5 1")
  apply (rule nat_less_induct)
  apply (rule allI)+
  apply (rename_tac tr schB schA)
  apply (intro strip)
  apply (erule conjE)+

  apply (case_tac "Forall (λx. x ∈ act A ∧ x ∉ act B) tr")

  apply (rule seq_take_lemma [THEN iffD2, THEN spec])
  apply (tactic "thin_tac' context 5 1")

  apply (case_tac "Finite tr")

  text ‹both sides of this equation are ‹nil››
  apply (subgoal_tac "schB = nil")
  apply simp
  text ‹first side: ‹mksch = nil››
  apply (auto intro!: ForallQFilterPnil ForallAnBmksch FiniteL_mksch)[1]
  text ‹second side: ‹schA = nil››
  apply (erule_tac A = "B" in LastActExtimplnil)
  apply (simp (no_asm_simp))
  apply (erule_tac Q = "λx. x ∈ act A ∧ x ∉ act B" in ForallQFilterPnil)
  apply assumption
  apply fast

  text ‹case ‹¬ Finite tr››

  text ‹both sides of this equation are ‹UU››
  apply (subgoal_tac "schB = UU")
  apply simp
  text ‹first side: ‹mksch = UU››
  apply (force intro!: ForallQFilterPUU finiteR_mksch' ForallAnBmksch)
  text ‹‹schA = UU››
  apply (erule_tac A = "B" in LastActExtimplUU)
  apply simp
  apply (erule_tac Q = "λx. x ∈ act A ∧ x ∉ act B" in ForallQFilterPUU)
  apply assumption
  apply fast

  text ‹case ‹¬ Forall (λx. x ∈ act B ∧ x ∉ act A) s››

  apply (drule divide_Seq3)

  apply (erule exE)+
  apply (erule conjE)+
  apply hypsubst

  text ‹bring in lemma ‹reduceB_mksch››
  apply (frule_tac y = "schB" and x = "schA" and A = "A" and B = "B" in reduceB_mksch)
  apply assumption+
  apply (erule exE)+
  apply (erule conjE)+

  text ‹use ‹reduceB_mksch› to rewrite conclusion›
  apply hypsubst
  apply simp

  text ‹eliminate the ‹A›-only prefix›

  apply (subgoal_tac "(Filter (λa. a ∈ act B) ⋅ x1) = nil")
  apply (erule_tac [2] ForallQFilterPnil)
  prefer 2 apply (assumption)
  prefer 2 apply (fast)

  text ‹Now real recursive step follows (in ‹x›)›

  apply simp
  apply (case_tac "x ∈ act B")
  apply (case_tac "x ∉ act A")
  apply (rotate_tac -2)
  apply simp

  apply (subgoal_tac "Filter (λa. a ∈ act B ∧ a ∈ ext A) ⋅ x1 = nil")
  apply (rotate_tac -1)
  apply simp
  text ‹eliminate introduced subgoal 2›
  apply (erule_tac [2] ForallQFilterPnil)
  prefer 2 apply assumption
  prefer 2 apply fast

  text ‹bring in ‹divide_Seq› for ‹s››
  apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
  apply (erule conjE)+

  text ‹subst ‹divide_Seq› in conclusion, but only at the rightmost occurrence›
  apply (rule_tac t = "schB" in ssubst)
  back
  back
  back
  apply assumption

  text ‹reduce ‹trace_takes› from ‹n› to strictly smaller ‹k››
  apply (rule take_reduction)

  text ‹‹f B (tw iB) = tw ¬ eB››
  apply (simp add: int_is_act not_ext_is_int_or_not_act)
  apply (rule refl)
  apply (simp add: int_is_act not_ext_is_int_or_not_act)
  apply (rotate_tac -11)

  text ‹now conclusion fulfills induction hypothesis, but assumptions are not ready›

  text ‹assumption ‹schA››
  apply (simp add: ext_and_act)
  text ‹assumption ‹schB››
  apply (drule_tac x = "schB" and g = "Filter (λa. a ∈ act B) ⋅ rs" in subst_lemma2)
  apply assumption
  apply (simp add: int_is_not_ext)
  text ‹assumptions concerning ‹LastActExtsch›, cannot be rewritten, as ‹LastActExtsmalli› are looping›
  apply (drule_tac sch = "schB" and P = "λa. a ∈ int B" in LastActExtsmall1)
  apply (frule_tac ?sch1.0 = "x1" in LastActExtsmall2)
  apply assumption

  text ‹assumption ‹Forall schB››
  apply (drule_tac s = "schB" and P = "Forall (λx. x ∈ act B)" in subst)
  apply assumption
  apply (simp add: int_is_act)

  text ‹case ‹x ∈ actions (asig_of A) ∧ x ∈ actions (asig_of B)››

  apply (rotate_tac -2)
  apply simp

  apply (subgoal_tac "Filter (λa. a ∈ act B ∧ a ∈ ext A) ⋅ x1 = nil")
  apply (rotate_tac -1)
  apply simp
  text ‹eliminate introduced subgoal 2›
  apply (erule_tac [2] ForallQFilterPnil)
  prefer 2 apply assumption
  prefer 2 apply fast

  text ‹bring in ‹divide_Seq› for ‹s››
  apply (frule sym [THEN eq_imp_below, THEN divide_Seq])
  apply (erule conjE)+

  text ‹subst ‹divide_Seq› in conclusion, but only at the rightmost occurrence›
  apply (rule_tac t = "schB" in ssubst)
  back
  back
  back
  apply assumption

  text ‹‹f B (tw iB) = tw ¬ eB››
  apply (simp add: int_is_act not_ext_is_int_or_not_act)

  text ‹rewrite assumption forall and ‹schB››
  apply (rotate_tac 13)
  apply (simp add: ext_and_act)

  text ‹‹divide_Seq› for ‹schB2››
  apply (frule_tac y = "x2" in sym [THEN eq_imp_below, THEN divide_Seq])
  apply (erule conjE)+
  text ‹assumption ‹schA››
  apply (drule_tac x = "schB" and g = "Filter (λa. a ∈ act B) ⋅ rs" in subst_lemma2)
  apply assumption
  apply (simp add: int_is_not_ext)

  text ‹‹f B (tw iA schA2) = nil››
  apply (simp add: int_is_not_ext not_ext_is_int_or_not_act intA_is_not_actB)


  text ‹reduce ‹trace_takes from ‹n› to strictly smaller ‹k›››
  apply (rule take_reduction)
  apply (rule refl)
  apply (rule refl)

  text ‹now conclusion fulfills induction hypothesis, but assumptions are not all ready›

  text ‹assumption ‹schA››
  apply (drule_tac x = "x2" and g = "Filter (λa. a ∈ act A) ⋅ rs" in subst_lemma2)
  apply assumption
  apply (simp add: intA_is_not_actB int_is_not_ext)

  text ‹conclusions concerning ‹LastActExtsch›, cannot be rewritten, as ‹LastActExtsmalli› are looping›
  apply (drule_tac sch = "schB" and P = "λa. a∈int B" in LastActExtsmall1)
  apply (frule_tac ?sch1.0 = "x1" in LastActExtsmall2)
  apply assumption
  apply (drule_tac sch = "x2" and P = "λa. a∈int A" in LastActExtsmall1)

  text ‹assumption ‹Forall schA›, and ‹Forall schA› are performed by ‹ForallTL›, ‹ForallDropwhile››
  apply (simp add: ForallTL ForallDropwhile)

  text ‹case ‹x ∉ B ∧ x ∈ A››
  text ‹cannot occur, as just this case has been scheduled out before as the ‹B›-only prefix›
  apply (case_tac "x ∈ act A")
  apply fast

  text ‹case ‹x ∉ B ∧ x ∉ A››
  text ‹cannot occur because of assumption: ‹Forall (a ∈ ext A ∨ a ∈ ext B)››
  apply (rotate_tac -9)
  text ‹reduce forall assumption from ‹tr› to ‹x ↝ rs››
  apply (simp add: externals_of_par)
  apply (fast intro!: ext_is_act)
  done


subsection "COMPOSITIONALITY on TRACE Level -- Main Theorem"

theorem compositionality_tr:
  "is_trans_of A ==> is_trans_of B ==> compatible A B ==> compatible B A ==>
    is_asig (asig_of A) ==> is_asig (asig_of B) ==>
    tr ∈ traces (A ∥ B) ⟷
      Filter (λa. a ∈ act A) ⋅ tr ∈ traces A ∧
      Filter (λa. a ∈ act B) ⋅ tr ∈ traces B ∧
      Forall (λx. x ∈ ext(A ∥ B)) tr"
  apply (simp add: traces_def has_trace_def)
  apply auto

  text ‹‹==>››
  text ‹There is a schedule of ‹A››
  apply (rule_tac x = "Filter (λa. a ∈ act A) ⋅ sch" in bexI)
  prefer 2
  apply (simp add: compositionality_sch)
  apply (simp add: compatibility_consequence1 externals_of_par ext1_ext2_is_not_act1)
  text ‹There is a schedule of ‹B››
  apply (rule_tac x = "Filter (λa. a ∈ act B) ⋅ sch" in bexI)
  prefer 2
  apply (simp add: compositionality_sch)
  apply (simp add: compatibility_consequence2 externals_of_par ext1_ext2_is_not_act2)
  text ‹Traces of ‹A ∥ B› have only external actions from ‹A› or ‹B››
  apply (rule ForallPFilterP)

  text ‹‹<==››

  text ‹replace ‹schA› and ‹schB› by ‹Cut schA› and ‹Cut schB››
  apply (drule exists_LastActExtsch)
  apply assumption
  apply (drule exists_LastActExtsch)
  apply assumption
  apply (erule exE)+
  apply (erule conjE)+
  text ‹Schedules of A(B) have only actions of A(B)›
  apply (drule scheds_in_sig)
  apply assumption
  apply (drule scheds_in_sig)
  apply assumption

  apply (rename_tac h1 h2 schA schB)
  text ‹‹mksch› is exactly the construction of ‹trA∥B› out of ‹schA›, ‹schB›, and the oracle ‹tr›,
 we need here›
  apply (rule_tac x = "mksch A B ⋅ tr ⋅ schA ⋅ schB" in bexI)

  text ‹External actions of mksch are just the oracle›
  apply (simp add: FilterA_mksch_is_tr)

  text ‹‹mksch› is a schedule -- use compositionality on sch-level›
  apply (simp add: compositionality_sch)
  apply (simp add: FilterAmksch_is_schA FilterBmksch_is_schB)
  apply (erule ForallAorB_mksch)
  apply (erule ForallPForallQ)
  apply (erule ext_is_act)
  done



subsection ‹COMPOSITIONALITY on TRACE Level -- for Modules›

lemma compositionality_tr_modules:
  "is_trans_of A ==> is_trans_of B ==> compatible A B ==> compatible B A ==>
    is_asig(asig_of A) ==> is_asig(asig_of B) ==>
    Traces (A∥B) = par_traces (Traces A) (Traces B)"
  apply (unfold Traces_def par_traces_def)
  apply (simp add: asig_of_par)
  apply (rule set_eqI)
  apply (simp add: compositionality_tr externals_of_par)
  done


declaration ‹fn _ => Simplifier.map_ss (Simplifier.set_mksym Simplifier.default_mk_sym)›

end