Theory CompositionSupport

theory CompositionSupport
imports CompositionBase
begin

locale CompositionSupport =
fixes ESi :: "'e ES_rec"
and 𝒱 :: "'e V_rec"
and 𝒱i :: "'e V_rec"

(* assumption about the component event system *)
assumes validESi: "ES_valid ESi"

(* assumption about the views (part of proper separation) *)
and validVi: "isViewOn 𝒱i E⇘ESi⇙"
and Vv_inter_Ei_is_Vvi: "V⇘𝒱⇙ ∩ E⇘ESi⇙ = V⇘𝒱i⇙"
and Cv_inter_Ei_subsetof_Cvi: "C⇘𝒱⇙ ∩ E⇘ESi⇙ ⊆ C⇘𝒱i⇙"

(* sublocale relations for CompositionSupport *)

(* body of CompositionSupport *)
context CompositionSupport
begin

(* This lemma is used in the compositionality proof for BSD.
  Assuming that BSD holds for a subsystem ESi and given a trace β @ [c] @ α of the composed system,
  we can obtain a trace (β ↿ E⇘ESi⇙) @ α_i' of ESi where α_i' contains no 
  events that are confidential in ESi and (α_i' ↿ V⇘𝒱i⇙) = (α ↿ V⇘𝒱i⇙) holds.
  
 𝒱 and 𝒱i denote views on the composition and subsystem respectively.
  We assume that 𝒱 and 𝒱i are properly separated. *)
lemma BSD_in_subsystem:
"⟦ c ∈ C⇘𝒱⇙; ((β @ [c] @ α) ↿ E⇘ESi⇙) ∈ Tr⇘ESi⇙ ; BSD 𝒱i Tr⇘ESi⇙ ⟧ 
  ⟹ ∃α_i'. ( ((β ↿ E⇘ESi⇙) @ α_i') ∈ Tr⇘ESi⇙ 
  ∧ (α_i' ↿ V⇘𝒱i⇙) = (α ↿ V⇘𝒱i⇙) ∧ α_i' ↿ C⇘𝒱i⇙ = [] )"
proof (induct "length (([c] @ α) ↿ C⇘𝒱i⇙)" arbitrary: β c α)
  case 0
  (* show that ([c] @ α) ↿ E⇘ESi⇙ is a suitable choice for α_i' *)
  let ?L = "([c] @ α) ↿ E⇘ESi⇙"
  
  from 0(3) have β_E1_cα_E1_in_Tr1: "((β ↿ E⇘ESi⇙) @ (([c] @ α) ↿ E⇘ESi⇙)) ∈ Tr⇘ESi⇙"
    by (simp only: projection_concatenation_commute)
  moreover
  have "(?L ↿ V⇘𝒱i⇙) = (α ↿ V⇘𝒱i⇙)"
  proof -
    have "(?L ↿ V⇘𝒱i⇙) = ([c] @ α) ↿ V⇘𝒱i⇙"
    proof -
      from validVi have "E⇘ESi⇙ ∩ V⇘𝒱i⇙ = V⇘𝒱i⇙"
        by (simp add: isViewOn_def V_valid_def VN_disjoint_def VC_disjoint_def NC_disjoint_def 
          , auto)
      moreover
      have "(?L ↿ V⇘𝒱i⇙) = ([c] @ α) ↿ (E⇘ESi⇙ ∩ V⇘𝒱i⇙)"
        by (simp add: projection_def)
      ultimately show ?thesis
        by auto
    qed
    moreover
    have "([c] @ α) ↿ V⇘𝒱i⇙ = α ↿ V⇘𝒱i⇙"
    proof -
      have "([c] @ α) ↿ V⇘𝒱i⇙ = ([c] ↿ V⇘𝒱i⇙) @ (α ↿ V⇘𝒱i⇙)"
        by (rule projection_concatenation_commute)
      moreover
      have "([c] ↿ V⇘𝒱i⇙) = []"
      proof -
        from 0(2) have "[c] ↿ C⇘𝒱⇙ = [c]"
          by (simp add: projection_def)
        moreover
        have "[c] ↿ C⇘𝒱⇙ ↿ V⇘𝒱i⇙ = []"
        proof -
          from validVi Cv_inter_Ei_subsetof_Cvi have "C⇘𝒱⇙ ∩ V⇘𝒱i⇙ ⊆ C⇘𝒱i⇙"
            by (simp add: isViewOn_def  V_valid_def VC_disjoint_def, auto)
          moreover
          from 0(1) have "[c] ↿ C⇘𝒱i⇙ = []"
            by (simp only: projection_concatenation_commute, auto)
          ultimately have "[c] ↿ (C⇘𝒱⇙ ∩ V⇘𝒱i⇙) = []"
            by (rule projection_on_subset)
          thus ?thesis
            by (simp only: projection_def, auto)
        qed
        ultimately show ?thesis
          by auto
      qed
      ultimately show ?thesis
        by auto
    qed
    ultimately show ?thesis
      by auto
  qed
  moreover
  have "?L ↿ C⇘𝒱i⇙ = []"
  proof -
    from 0(1) have "([c] @ α) ↿ C⇘𝒱i⇙ = []"
      by auto
    hence "([c] @ α) ↿ (C⇘𝒱i⇙ ∩ E⇘ESi⇙) = []"
      by (rule projection_on_intersection)
    hence "([c] @ α) ↿ (E⇘ESi⇙ ∩ C⇘𝒱i⇙) = []"
      by (simp only: Int_commute)
    thus ?thesis
      by (simp only: projection_def, auto)                
  qed
  ultimately show ?case
    by auto
  
next
  case (Suc n)
  
  from projection_split_last[OF Suc(2)] obtain γ c_i δ
    where c_i_in_C𝒱i: "c_i ∈ C⇘𝒱i⇙"
    and   cα_is_γc_iδ: "[c] @ α = γ @ [c_i] @ δ"
    and   δ_no_C𝒱i:  "δ ↿ C⇘𝒱i⇙ = []"
    and   n_is_len_γδ_C𝒱i: "n = length ((γ @ δ) ↿ C⇘𝒱i⇙)"
    by auto
  
  let ?L1 = "((β @ γ) ↿ E⇘ESi⇙)"
  let ?L2 = "(δ ↿ E⇘ESi⇙)"

  note c_i_in_C𝒱i
  moreover
  have list_with_c_i_in_Tr1: "(?L1 @ [c_i] @ ?L2) ∈ Tr⇘ESi⇙"
  proof -
    from c_i_in_C𝒱i validVi have "[c_i] ↿ E⇘ESi⇙ = [c_i]"
      by (simp only: isViewOn_def V_valid_def VC_disjoint_def
        VN_disjoint_def NC_disjoint_def projection_def, auto)
    moreover
    from Suc(4) cα_is_γc_iδ have "((β @ γ @ [c_i] @ δ) ↿ E⇘ESi⇙) ∈ Tr⇘ESi⇙"
      by auto
    hence "(?L1 @ ([c_i] ↿ E⇘ESi⇙) @ ?L2) ∈ Tr⇘ESi⇙"
      by (simp only: projection_def, auto)
    ultimately show ?thesis
      by auto
  qed
  moreover 
  have "?L2 ↿ C⇘𝒱i⇙ = []"
  proof -
    from validVi have "⋀x. (x ∈ E⇘ESi⇙ ∧ x ∈ C⇘𝒱i⇙) = (x ∈ C⇘𝒱i⇙)"
      by (simp add: isViewOn_def V_valid_def VC_disjoint_def
        VN_disjoint_def NC_disjoint_def, auto)
    with δ_no_C𝒱i show ?thesis
      by (simp add: projection_def)
  qed            
  moreover note Suc(5)
  ultimately obtain δ'
    where δ'_1: "(?L1 @ δ') ∈ Tr⇘ESi⇙"
    and δ'_2: "δ' ↿ V⇘𝒱i⇙ = ?L2 ↿ V⇘𝒱i⇙"
    and δ'_3: "δ' ↿ C⇘𝒱i⇙ = []"
    unfolding BSD_def
    by blast
  hence δ'_2': "δ' ↿ V⇘𝒱i⇙ = δ ↿ V⇘𝒱i⇙"
  proof -
    have "?L2 ↿ V⇘𝒱i⇙ = δ ↿ V⇘𝒱i⇙"
    proof -
      from validVi have "⋀x. (x ∈ E⇘ESi⇙ ∧ x ∈ V⇘𝒱i⇙) = (x ∈ V⇘𝒱i⇙)"
        by (simp add: isViewOn_def V_valid_def VC_disjoint_def
        VN_disjoint_def NC_disjoint_def, auto)
      thus ?thesis
        by (simp add: projection_def)
    qed
    with δ'_2 show ?thesis
      by auto
  qed
  
  show ?case
  proof (cases γ) (* need to distinguish between these cases as the inductive 
      hypothesis can only be applied to one case. *)
    case Nil
    with cα_is_γc_iδ have "[c] @ α = [c_i] @ δ"
      by auto
    hence δ_is_α: "δ = α"
      by auto
    
    from δ'_1 have δ'_1': "((β ↿ E⇘ESi⇙) @ δ') ∈ Tr⇘ESi⇙"
      by (simp only: Nil, auto)
    moreover
    note δ'_2'
    moreover note δ'_3
    ultimately show ?thesis
      by (simp only: δ_is_α, auto)
  next
    case (Cons x γ')
    with cα_is_γc_iδ have γ_is_cγ': "γ = [c] @ γ'"
      by simp
    with n_is_len_γδ_C𝒱i have "n = length (([c] @ γ' @ δ) ↿ C⇘𝒱i⇙)"
      by auto
    with δ_no_C𝒱i δ'_3 have "n = length (([c] @ γ' @ δ') ↿ C⇘𝒱i⇙)"
      by (simp only: projection_concatenation_commute)
    moreover
    note Suc(3)
    moreover
    have "((β @ [c] @ (γ' @ δ')) ↿ E⇘ESi⇙) ∈ Tr⇘ESi⇙"
    proof -
      from δ'_1 validESi have "δ' = δ' ↿ E⇘ESi⇙"
      proof -
        let ?L = "(β @ γ) ↿ E⇘ESi⇙ @ δ'"
        
        from δ'_1 validESi have "∀e ∈ set ?L. e ∈ E⇘ESi⇙"
          by (simp add: ES_valid_def traces_contain_events_def)
        hence "set δ' ⊆ E⇘ESi⇙"
          by auto
        thus ?thesis
          by (simp add: list_subset_iff_projection_neutral)
      qed
      with δ'_1  have "?L1 @ δ' = (β @ γ @ δ') ↿ E⇘ESi⇙"
        by (simp only: projection_concatenation_commute, auto)
      with γ_is_cγ' δ'_1  show ?thesis
        by auto
    qed
    moreover
    note Suc(5)
    moreover note Suc(1)[of c "γ' @ δ'" β]
    ultimately obtain α_i'
      where α_i'_1: "β ↿ E⇘ESi⇙ @ α_i' ∈ Tr⇘ESi⇙"
      and α_i'_2: "α_i' ↿ V⇘𝒱i⇙ = (γ' @ δ') ↿ V⇘𝒱i⇙"
      and α_i'_3: "α_i' ↿ C⇘𝒱i⇙ = []"
      by auto
    moreover
    have "α_i' ↿ V⇘𝒱i⇙ = α ↿ V⇘𝒱i⇙"
    proof -
      have "α ↿ V⇘𝒱i⇙ = (γ' @ δ) ↿ V⇘𝒱i⇙"
      proof -
        from cα_is_γc_iδ γ_is_cγ' have "α ↿ V⇘𝒱i⇙ = (γ' @ [c_i] @ δ) ↿ V⇘𝒱i⇙"
          by simp
        with validVi c_i_in_C𝒱i show ?thesis
          by (simp only: isViewOn_def V_valid_def  VC_disjoint_def
            VN_disjoint_def NC_disjoint_def projection_concatenation_commute 
            projection_def, auto)
      qed
      moreover
      from α_i'_2 δ'_2' have "α_i' ↿ V⇘𝒱i⇙ = (γ' @ δ) ↿ V⇘𝒱i⇙"
        by (simp only: projection_concatenation_commute)
      ultimately show ?thesis
        by auto
    qed
    ultimately show ?thesis
      by auto
  qed
qed

(*
    Variant of the previous lemma with different propositions (note the lack of a confidential event c).
*)
lemma BSD_in_subsystem2:
"⟦ ((β @ α) ↿ E⇘ESi⇙) ∈ Tr⇘ESi⇙ ; BSD 𝒱i Tr⇘ESi⇙ ⟧ 
  ⟹ ∃ α_i'. ( ((β ↿ E⇘ESi⇙) @ α_i') ∈ Tr⇘ESi⇙ ∧ (α_i' ↿ V⇘𝒱i⇙) = (α ↿ V⇘𝒱i⇙) ∧ α_i' ↿ C⇘𝒱i⇙ = [] )"
proof (induct "length (α ↿ C⇘𝒱i⇙)" arbitrary: β α)
  case 0
  (* show that α ↿ E⇘ESi⇙  is a suitable choice for α_i' *)
  let ?L = "α ↿ E⇘ESi⇙"
  
  from 0(2) have β_E1_α_E1_in_Tr1: "((β ↿ E⇘ESi⇙) @ ?L) ∈ Tr⇘ESi⇙"
    by (simp only: projection_concatenation_commute)
  moreover
  have "(?L ↿ V⇘𝒱i⇙) = (α ↿ V⇘𝒱i⇙)"
    proof -
      from validVi have "E⇘ESi⇙ ∩ V⇘𝒱i⇙ = V⇘𝒱i⇙"
        by (simp add: isViewOn_def V_valid_def  VC_disjoint_def
        VN_disjoint_def NC_disjoint_def, auto)
      moreover
      have "(?L ↿ V⇘𝒱i⇙) = α ↿ (E⇘ESi⇙ ∩ V⇘𝒱i⇙)"
        by (simp add: projection_def)
      ultimately show ?thesis
        by auto
    qed
  moreover
  have "?L ↿ C⇘𝒱i⇙ = []"
  proof -
    from 0(1) have "α ↿ C⇘𝒱i⇙ = []"
      by auto
    hence "α ↿ (C⇘𝒱i⇙ ∩ E⇘ESi⇙) = []"
      by (rule projection_on_intersection)
    hence "α ↿ (E⇘ESi⇙ ∩ C⇘𝒱i⇙) = []"
      by (simp only: Int_commute)
    thus ?thesis
      by (simp only: projection_def, auto)                
  qed
  ultimately show ?case
    by auto
  
next
  case (Suc n)
  
  from projection_split_last[OF Suc(2)] obtain γ c_i δ
    where c_i_in_C𝒱i: "c_i ∈ C⇘𝒱i⇙"
    and   α_is_γc_iδ: "α = γ @ [c_i] @ δ"
    and   δ_no_C𝒱i:  "δ ↿ C⇘𝒱i⇙ = []"
    and   n_is_len_γδ_C𝒱i: "n = length ((γ @ δ) ↿ C⇘𝒱i⇙)"
    by auto
  
  let ?L1 = "((β @ γ) ↿ E⇘ESi⇙)"
  let ?L2 = "(δ ↿ E⇘ESi⇙)"


  (* first apply BSD to get rid of c_i in α *)
  note c_i_in_C𝒱i
  moreover
  have list_with_c_i_in_Tr1: "(?L1 @ [c_i] @ ?L2) ∈ Tr⇘ESi⇙"
  proof -
    from c_i_in_C𝒱i validVi have "[c_i] ↿ E⇘ESi⇙ = [c_i]"
      by (simp only: isViewOn_def V_valid_def  VC_disjoint_def
        VN_disjoint_def NC_disjoint_def projection_def, auto)
    moreover
    from Suc(3) α_is_γc_iδ have "((β @ γ @ [c_i] @ δ) ↿ E⇘ESi⇙) ∈ Tr⇘ESi⇙"
      by auto
    hence "(?L1 @ ([c_i] ↿ E⇘ESi⇙) @ ?L2) ∈ Tr⇘ESi⇙"
      by (simp only: projection_def, auto)
    ultimately show ?thesis
      by auto
  qed
  moreover 
  have "?L2 ↿ C⇘𝒱i⇙ = []"
  proof -
    from validVi have "⋀x. (x ∈ E⇘ESi⇙ ∧ x ∈ C⇘𝒱i⇙) = (x ∈ C⇘𝒱i⇙)"
      by (simp add: isViewOn_def V_valid_def  VC_disjoint_def
        VN_disjoint_def NC_disjoint_def, auto)
    with δ_no_C𝒱i show ?thesis
      by (simp add: projection_def)
  qed            
  moreover note Suc(4)
  ultimately obtain δ'
    where δ'_1: "(?L1 @ δ') ∈ Tr⇘ESi⇙"
    and δ'_2: "δ' ↿ V⇘𝒱i⇙ = ?L2 ↿ V⇘𝒱i⇙"
    and δ'_3: "δ' ↿ C⇘𝒱i⇙ = []"
    unfolding BSD_def
    by blast
  hence δ'_2': "δ' ↿ V⇘𝒱i⇙ = δ ↿ V⇘𝒱i⇙"
  proof -
    have "?L2 ↿ V⇘𝒱i⇙ = δ ↿ V⇘𝒱i⇙"
    proof -
      from validVi have "⋀x. (x ∈ E⇘ESi⇙ ∧ x ∈ V⇘𝒱i⇙) = (x ∈ V⇘𝒱i⇙)"
        by (simp add: isViewOn_def V_valid_def  VC_disjoint_def
        VN_disjoint_def NC_disjoint_def, auto)
      thus ?thesis
        by (simp add: projection_def)
    qed
    with δ'_2 show ?thesis
      by auto
  qed

  (* now that we eliminated c_i, we can apply the inductive hypothesis for ?β = β and ?α = γ @ δ' *)
  from n_is_len_γδ_C𝒱i δ_no_C𝒱i δ'_3 have "n = length ((γ @ δ') ↿ C⇘𝒱i⇙)"
    by (simp add: projection_concatenation_commute)
  moreover
  have "(β @ (γ @ δ')) ↿ E⇘ESi⇙ ∈ Tr⇘ESi⇙"
    proof -
      have "δ' = δ' ↿ E⇘ESi⇙"
        proof -
          let ?L = "(β @ γ) ↿ E⇘ESi⇙ @ δ'"
        
          from δ'_1 validESi have "∀e ∈ set ?L. e ∈ E⇘ESi⇙"
            by (simp add: ES_valid_def traces_contain_events_def)
          hence "set δ' ⊆ E⇘ESi⇙"
            by auto
          thus ?thesis
            by (simp add: list_subset_iff_projection_neutral)
        qed
      with δ'_1  have "?L1 @ δ' = (β @ γ @ δ') ↿ E⇘ESi⇙"
        by (simp only: projection_concatenation_commute, auto)
      with δ'_1  show ?thesis
        by auto
    qed
  moreover
  note Suc(4) Suc(1)[of "γ @ δ'" β] 
  ultimately obtain α_i' 
    where res1: "β ↿ E⇘ESi⇙ @ α_i' ∈ Tr⇘ESi⇙" 
    and res2: "α_i' ↿ V⇘𝒱i⇙ = (γ @ δ') ↿ V⇘𝒱i⇙"
    and res3: "α_i' ↿ C⇘𝒱i⇙ = []"
    by auto

  (* Show that the resulting α_i' is suitable *)
  have "α_i' ↿ V⇘𝒱i⇙ = α ↿ V⇘𝒱i⇙"
    proof -
      from c_i_in_C𝒱i validVi have "[c_i] ↿ V⇘𝒱i⇙ = []"
        by (simp add: isViewOn_def V_valid_def  VC_disjoint_def
        VN_disjoint_def NC_disjoint_def projection_def, auto)
      with α_is_γc_iδ δ'_2' have "α ↿ V⇘𝒱i⇙ = (γ @ δ') ↿ V⇘𝒱i⇙"
        by (simp only: projection_concatenation_commute, auto)
      with res2 show ?thesis
        by auto
    qed
  with res1 res3 show ?case
    by auto
qed

end

end