Theory CompositionBase

theory CompositionBase
imports "../Basics/BSPTaxonomy"
begin

definition 
properSeparationOfViews :: 
"'e ES_rec ⇒ 'e ES_rec ⇒ 'e V_rec ⇒ 'e V_rec ⇒ 'e V_rec ⇒ bool"
where
"properSeparationOfViews ES1 ES2 𝒱 𝒱1 𝒱2 ≡
   V⇘𝒱⇙ ∩ E⇘ES1⇙ = V⇘𝒱1⇙
   ∧ V⇘𝒱⇙ ∩ E⇘ES2⇙ = V⇘𝒱2⇙
   ∧ C⇘𝒱⇙ ∩ E⇘ES1⇙ ⊆ C⇘𝒱1⇙
   ∧ C⇘𝒱⇙ ∩ E⇘ES2⇙ ⊆ C⇘𝒱2⇙
   ∧ N⇘𝒱1⇙ ∩ N⇘𝒱2⇙ = {}"

definition
wellBehavedComposition :: 
"'e ES_rec ⇒ 'e ES_rec ⇒ 'e V_rec ⇒ 'e V_rec ⇒ 'e V_rec ⇒ bool"
where
"wellBehavedComposition ES1 ES2 𝒱 𝒱1 𝒱2 ≡
( N⇘𝒱1⇙ ∩ E⇘ES2⇙ = {} ∧ N⇘𝒱2⇙ ∩ E⇘ES1⇙ = {} )
  ∨ (∃ρ1. ( N⇘𝒱1⇙ ∩ E⇘ES2⇙ = {} ∧ total ES1 (C⇘𝒱1⇙ ∩ N⇘𝒱2⇙) 
            ∧ BSIA ρ1 𝒱1 Tr⇘ES1⇙ ))
  ∨ (∃ρ2. ( N⇘𝒱2⇙ ∩ E⇘ES1⇙ = {} ∧ total ES2 (C⇘𝒱2⇙ ∩ N⇘𝒱1⇙) 
            ∧ BSIA ρ2 𝒱2 Tr⇘ES2⇙ ))
  ∨ (∃ρ1 ρ2 Γ1 Γ2. ( 
      ∇⇘Γ1⇙ ⊆ E⇘ES1⇙ ∧ Δ⇘Γ1⇙ ⊆ E⇘ES1⇙ ∧ Υ⇘Γ1⇙ ⊆ E⇘ES1⇙
      ∧ ∇⇘Γ2⇙ ⊆ E⇘ES2⇙ ∧ Δ⇘Γ2⇙ ⊆ E⇘ES2⇙ ∧ Υ⇘Γ2⇙ ⊆ E⇘ES2⇙
      ∧ BSIA ρ1 𝒱1 Tr⇘ES1⇙ ∧ BSIA ρ2 𝒱2 Tr⇘ES2⇙
      ∧ total ES1 (C⇘𝒱1⇙ ∩ N⇘𝒱2⇙) ∧ total ES2 (C⇘𝒱2⇙ ∩ N⇘𝒱1⇙)
      ∧ FCIA ρ1 Γ1 𝒱1 Tr⇘ES1⇙ ∧ FCIA ρ2 Γ2 𝒱2 Tr⇘ES2⇙
      ∧ V⇘𝒱1⇙ ∩ V⇘𝒱2⇙ ⊆ ∇⇘Γ1⇙ ∪ ∇⇘Γ2⇙
      ∧ C⇘𝒱1⇙ ∩ N⇘𝒱2⇙ ⊆ Υ⇘Γ1⇙ ∧ C⇘𝒱2⇙ ∩ N⇘𝒱1⇙ ⊆ Υ⇘Γ2⇙
      ∧ N⇘𝒱1⇙ ∩ Δ⇘Γ1⇙ ∩ E⇘ES2⇙ = {} ∧ N⇘𝒱2⇙ ∩ Δ⇘Γ2⇙ ∩ E⇘ES1⇙ = {} ))"

locale Compositionality =
fixes ES1 :: "'e ES_rec"
and ES2 :: "'e ES_rec"
and 𝒱 :: "'e V_rec" (* view of the composed system *)
and 𝒱1 :: "'e V_rec" (* view for component ES1 *)
and 𝒱2 :: "'e V_rec" (* view for component ES2 *)

(* assumptions about the event systems *)
assumes validES1: "ES_valid ES1"
and validES2: "ES_valid ES2"
and composableES1ES2: "composable ES1 ES2"

(* basic assumptions about the views *)
and validVC: "isViewOn 𝒱 (E⇘(ES1 ∥ ES2)⇙)"
and validV1: "isViewOn 𝒱1 E⇘ES1⇙"
and validV2: "isViewOn 𝒱2 E⇘ES2⇙"


(* the following assumptions constitute proper separation of views 
  (Def. 6.3.2 in Heiko Mantel's dissertation) *)
and propSepViews: "properSeparationOfViews ES1 ES2 𝒱 𝒱1 𝒱2" 

(* the following assumptions constitute well behaved composition (Def. 6.3.6 in Mantel's dissertation) *)
and well_behaved_composition: "wellBehavedComposition ES1 ES2 𝒱 𝒱1 𝒱2"



(* sublocale relations for Compositionality *)
sublocale Compositionality ⊆ BSPTaxonomyDifferentCorrections "ES1 ∥ ES2" "𝒱"
  by (unfold_locales, rule composeES_yields_ES, rule validES1,
    rule validES2, rule validVC)


(* body of Compositionality *)
context Compositionality
begin


(* proper separation of views implies the following equality *)
lemma Vv_is_Vv1_union_Vv2: "V⇘𝒱⇙ = V⇘𝒱1⇙ ∪ V⇘𝒱2⇙"
proof -
  from propSepViews have "V⇘𝒱⇙ ∩ E⇘ES1⇙ ∪ V⇘𝒱⇙ ∩ E⇘ES2⇙ = V⇘𝒱1⇙ ∪ V⇘𝒱2⇙"
    unfolding properSeparationOfViews_def by auto
  hence "V⇘𝒱⇙ ∩ (E⇘ES1⇙ ∪ E⇘ES2⇙) = V⇘𝒱1⇙ ∪ V⇘𝒱2⇙"
    by auto
  hence "V⇘𝒱⇙ ∩ E⇘(ES1 ∥ ES2)⇙ = V⇘𝒱1⇙ ∪ V⇘𝒱2⇙"
    by (simp add: composeES_def)
  with validVC show ?thesis
    by (simp add: isViewOn_def, auto)
qed

lemma disjoint_Nv1_Vv2: "N⇘𝒱1⇙ ∩ V⇘𝒱2⇙ = {}"
proof -
  from validV1 have "N⇘𝒱1⇙ ⊆ E⇘ES1⇙"
    by (simp add: isViewOn_def, auto)
  with propSepViews have "N⇘𝒱1⇙ ∩ V⇘𝒱2⇙ = (N⇘𝒱1⇙ ∩ E⇘ES1⇙ ∩ V⇘𝒱⇙) ∩ E⇘ES2⇙"
    unfolding properSeparationOfViews_def by auto
  hence "N⇘𝒱1⇙ ∩ V⇘𝒱2⇙ = (N⇘𝒱1⇙ ∩ V⇘𝒱⇙ ∩ E⇘ES1⇙) ∩ E⇘ES2⇙"
    by auto
  moreover
  from validV1 have "N⇘𝒱1⇙ ∩ V⇘𝒱⇙ ∩ E⇘ES1⇙ = {}" 
    using propSepViews unfolding properSeparationOfViews_def
    by (metis VN_disjoint_def V_valid_def inf_assoc inf_commute isViewOn_def)
  ultimately show ?thesis
    by auto      
qed

lemma disjoint_Nv2_Vv1: "N⇘𝒱2⇙ ∩ V⇘𝒱1⇙ = {}"
proof -
  from validV2 have "N⇘𝒱2⇙ ⊆ E⇘ES2⇙"
    by (simp add:isViewOn_def, auto)
  with propSepViews have "N⇘𝒱2⇙ ∩ V⇘𝒱1⇙ = (N⇘𝒱2⇙ ∩ E⇘ES2⇙ ∩ V⇘𝒱⇙) ∩ E⇘ES1⇙"
    unfolding properSeparationOfViews_def by auto
  hence "N⇘𝒱2⇙ ∩ V⇘𝒱1⇙ = (N⇘𝒱2⇙ ∩ V⇘𝒱⇙ ∩ E⇘ES2⇙) ∩ E⇘ES1⇙"
    by auto
  moreover
  from validV2 have "N⇘𝒱2⇙ ∩ V⇘𝒱⇙ ∩ E⇘ES2⇙ = {}"
    using propSepViews unfolding properSeparationOfViews_def 
    by (metis VN_disjoint_def V_valid_def inf_assoc inf_commute isViewOn_def)
  ultimately show ?thesis
    by auto      
qed

(* An extended variant of the merge_property.
 Useful for the proof of the generalized zipping lemma. *)
lemma merge_property': " ⟦ set t1 ⊆ E⇘ES1⇙; set t2 ⊆ E⇘ES2⇙; 
  t1 ↿ E⇘ES2⇙ = t2 ↿ E⇘ES1⇙; t1 ↿ V⇘𝒱⇙ = []; t2 ↿ V⇘𝒱⇙ = []; 
  t1 ↿ C⇘𝒱⇙ = []; t2 ↿ C⇘𝒱⇙ = [] ⟧ 
⟹ ∃ t. (t ↿ E⇘ES1⇙ = t1 ∧ t ↿ E⇘ES2⇙ = t2 ∧ t ↿ V⇘𝒱⇙ = [] ∧ t ↿ C⇘𝒱⇙ = [] ∧ set t ⊆ (E⇘ES1⇙ ∪ E⇘ES2⇙))"
proof -
  assume t1_in_E1star: "set t1 ⊆ E⇘ES1⇙"
  and t2_in_E2star: "set t2 ⊆ E⇘ES2⇙"
  and t1_t2_synchronized: "t1 ↿ E⇘ES2⇙ = t2 ↿ E⇘ES1⇙"
  and t1Vv_empty: "t1 ↿ V⇘𝒱⇙ = []"
  and t2Vv_empty: "t2 ↿ V⇘𝒱⇙ = []"
  and t1Cv_empty: "t1 ↿ C⇘𝒱⇙ = []"
  and t2Cv_empty: "t2 ↿ C⇘𝒱⇙ = []"

  from merge_property[OF t1_in_E1star t2_in_E2star t1_t2_synchronized] obtain t
    where t_is_interleaving: "t ↿ E⇘ES1⇙ = t1 ∧ t ↿ E⇘ES2⇙ = t2"
    and t_contains_only_events_from_t1_t2: "set t ⊆ set t1 ∪ set t2"
    unfolding Let_def
    by auto
  moreover
  from t1Vv_empty t2Vv_empty t_contains_only_events_from_t1_t2
  have "t ↿ V⇘𝒱⇙ = []" 
    using propSepViews unfolding properSeparationOfViews_def
    by (metis Int_commute Vv_is_Vv1_union_Vv2 projection_on_union projection_sequence t_is_interleaving)
  moreover
  have "t ↿ C⇘𝒱⇙ = []"
    proof -
      from t1Cv_empty have "∀c ∈ C⇘𝒱⇙. c ∉ set t1"
        by (simp add: projection_def filter_empty_conv, fast)
      moreover
      from t2Cv_empty have "∀c ∈ C⇘𝒱⇙. c ∉ set t2"
        by (simp add: projection_def filter_empty_conv, fast)
      ultimately have
      "∀c ∈ C⇘𝒱⇙. c ∉ (set t1 ∪ set t2)"
        by auto
      with t_contains_only_events_from_t1_t2 have "∀c ∈ C⇘𝒱⇙. c ∉ set t"
        by auto
      thus ?thesis
        by (simp add: projection_def, metis filter_empty_conv)
    qed
  moreover
  from t1_in_E1star t2_in_E2star t_contains_only_events_from_t1_t2 
  have "set t ⊆ (E⇘ES1⇙ ∪ E⇘ES2⇙)"
    by auto
  ultimately show ?thesis
    by blast
qed

lemma Nv1_union_Nv2_subsetof_Nv: "N⇘𝒱1⇙ ∪ N⇘𝒱2⇙ ⊆ N⇘𝒱⇙"
proof -
  {
    fix e
    assume e_in_N1: "e ∈ N⇘𝒱1⇙"
    with validV1 have 
      e_in_E1: "e ∈ E⇘ES1⇙"
      and e_notin_V1: "e ∉ V⇘𝒱1⇙"
      and e_notin_C1: "e ∉ C⇘𝒱1⇙"
      by (simp only: isViewOn_def V_valid_def VC_disjoint_def NC_disjoint_def
        VN_disjoint_def, auto)+
    
    from e_in_E1 e_notin_V1 propSepViews have "e ∉ V⇘𝒱⇙"
     unfolding properSeparationOfViews_def by auto
    moreover
    from e_in_E1 e_notin_C1 propSepViews have "e ∉ C⇘𝒱⇙"
     unfolding properSeparationOfViews_def by auto
    moreover
    note e_in_E1 validVC
    ultimately have "e ∈ N⇘𝒱⇙"
      by (simp add: isViewOn_def V_valid_def VC_disjoint_def NC_disjoint_def VN_disjoint_def
         composeES_def, auto)
  }
  moreover {
    fix e
    assume e_in_N2: "e ∈ N⇘𝒱2⇙"
    with validV2 have 
      e_in_E2: "e ∈ E_ES ES2"
      and e_notin_V2: "e ∉ V⇘𝒱2⇙"
      and e_notin_C2: "e ∉ C⇘𝒱2⇙"
      by (simp only: isViewOn_def V_valid_def VC_disjoint_def NC_disjoint_def VN_disjoint_def
        , auto)+
    
    from e_in_E2 e_notin_V2 propSepViews have "e ∉ V⇘𝒱⇙"
     unfolding properSeparationOfViews_def by auto
    moreover
    from e_in_E2 e_notin_C2 propSepViews have "e ∉ C⇘𝒱⇙"
     unfolding properSeparationOfViews_def by auto
    moreover
    note e_in_E2 validVC
    ultimately have "e ∈ N⇘𝒱⇙"
      by (simp add: isViewOn_def V_valid_def VC_disjoint_def VN_disjoint_def NC_disjoint_def
         composeES_def, auto)
  }
  ultimately show ?thesis
    by auto
qed

end

end