Theory Parallel_Composition

(*
Title: Strong-Security
Authors: Sylvia Grewe, Alexander Lux, Heiko Mantel, Jens Sauer
*)
theory Parallel_Composition
imports Up_To_Technique
begin

context Strong_Security
begin

theorem parallel_composition:
  assumes eqlen: "length V = length V'"
  assumes partsrelated: "∀i < length V. [V!i] ≈⇘d⇙ [V'!i]"
  shows "V ≈⇘d⇙ V'"
proof -
  define R where "R = {(V,V'). length V = length V' 
    ∧ (∀i < length V. [V!i] ≈⇘d⇙ [V'!i])}"
  from eqlen partsrelated have inR: "(V,V') ∈ R"
    by (simp add: R_def)
  
  have "d_Bisimulation_Up_To_USdB d R"
    proof (simp add: d_Bisimulation_Up_To_USdB_def, auto)
      from USdBsym show "sym R" 
        by (simp add: R_def sym_def)
    next
      fix V V'
      assume "(V,V') ∈ R"
      with USdBeqlen show "length V = length V'" 
        by (simp add: R_def)
    next
      fix V V' i m1 m1' RS m2
      assume inR: "(V,V') ∈ R"
      assume irange: "i < length V"
      assume step: "⟨V!i,m1⟩ → ⟨RS,m2⟩"
      assume dequal: "m1 =⇘d⇙ m1'"

      from inR have Vassump:
        "length V = length V' ∧ (∀i < length V. [V!i] ≈⇘d⇙ [V'!i])"
        by (simp add: R_def)

      with step dequal USdB_Strong_d_Bisimulation irange 
      strongdB_aux[of "d" "≈⇘d⇙" "0" "[V!i]" "[V'!i]" "m1" "RS" "m2" "m1'"] 
      show "∃RS' m2'. ⟨V'!i,m1'⟩ → ⟨RS',m2'⟩ ∧
        ((RS,RS') ∈ R ∨ RS ≈⇘d⇙ RS') ∧ m2 =⇘d⇙ m2'"
        by (simp, fastforce)
    qed

    hence "R ⊆ (≈⇘d⇙)"
      by (rule Up_To_Technique)

    with inR show ?thesis by auto
qed



lemma parallel_decomposition:
  assumes related: "V ≈⇘d⇙ V'"
  shows "∀i < length V. [V!i] ≈⇘d⇙ [V'!i]"
proof -
  define R where "R = {(C,C'). ∃i W W'. W ≈⇘d⇙ W' ∧ i < length W 
    ∧ C = [W!i] ∧ C' = [W'!i]}"

  with related have inR: "∀i < length V. ([V!i],[V'!i]) ∈ R"
    by auto
  have "d_Bisimulation_Up_To_USdB d R"
    proof (simp add: d_Bisimulation_Up_To_USdB_def, auto)
      from USdBsym USdBeqlen show "sym R"
        by (simp add: sym_def R_def, metis)
    next
      fix C C'
      assume "(C,C') ∈ R"
      with USdBeqlen show "length C = length C'" 
        by (simp add: R_def, auto)
    next
      fix C C' i m1 m1' RS m2
      assume inR: "(C,C') ∈ R"
      assume irange: "i < length C"
      assume step: "⟨C!i,m1⟩ → ⟨RS,m2⟩"
      assume dequal: "m1 =⇘d⇙ m1'"

     from inR obtain j W W' where Rassump: 
       "W ≈⇘d⇙ W' ∧ j < length W ∧ C = [W!j] ∧ C' = [W'!j]"
       by (simp add: R_def, auto)

     with irange have i0: "i = 0" by auto

     from Rassump i0 strongdB_aux[of "d" "≈⇘d⇙" "j" "W" "W'" 
       "m1" "RS" "m2" "m1'"] 
       USdB_Strong_d_Bisimulation step dequal
     show "∃RS' m2'. ⟨C'!i,m1'⟩ → ⟨RS',m2'⟩ 
       ∧ ((RS,RS') ∈ R ∨ RS ≈⇘d⇙ RS') ∧ m2 =⇘d⇙ m2'"
       by auto
   qed

   hence "R ⊆ (≈⇘d⇙)"
     by (rule Up_To_Technique)

   with inR show ?thesis
     by auto

qed

lemma USdB_comp_head_tail:
  assumes relatedhead: "[c] ≈⇘d⇙ [c']"
  assumes relatedtail: "V ≈⇘d⇙ V'"
  shows "(c#V) ≈⇘d⇙ (c'#V')"
proof -
  from relatedtail USdBeqlen have eqlen: "length (c#V) = length (c'#V')"
    by force
  
  from relatedtail parallel_decomposition have singleV: 
    "∀i < length V. [V!i] ≈⇘d⇙ [V'!i]"
    by force

  with relatedhead have intermediate:
    "∀i < length (c#V). [(c#V)!i] ≈⇘d⇙ [(c'#V')!i]"
    by (auto, case_tac i, auto)
      
  with eqlen parallel_composition
  show ?thesis
    by blast
qed
       
lemma USdB_decomp_head_tail:
  assumes relatedlist: "(c#V) ≈⇘d⇙ (c'#V')"
  shows "[c] ≈⇘d⇙ [c'] ∧ V ≈⇘d⇙ V'"
proof auto
  from relatedlist USdBeqlen[of "c#V" "c'#V'"] 
  have eqlen: "length V = length V'" 
    by auto
  
  from relatedlist parallel_decomposition[of "c#V" "c'#V'" "d"]
  have intermediate:
    "∀i < length (c#V). [(c#V)!i] ≈⇘d⇙ [(c'#V')!i]"
    by auto
  thus "[c] ≈⇘d⇙ [c']"
    by force

  from intermediate eqlen show "V ≈⇘d⇙ V'"
  proof (case_tac V)
    assume Vcase1: "V = []"
    with eqlen have "V' = []" by auto
    with Vcase1 trivialpair_in_USdB show "V ≈⇘d⇙ V'" 
      by auto
  next
    fix c1 W
    assume Vcase2: "V = c1#W"
    hence Vlen: "length V > 0" by auto
    
    from intermediate have intermediate_aux:
      "⋀i. i < length V
      ⟹ [V!i] ≈⇘d⇙ [V'!i]"
      by force
    
    with parallel_composition[of "V" "V'"] eqlen
    show "V ≈⇘d⇙ V'"
      by blast
    
  qed
qed


end


end