Theory Up_To_Technique

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

context Strong_Security
begin

― ‹define d-bisimulation 'up to' union of strong d-Bisimulations›
definition d_Bisimulation_Up_To_USdB :: 
"'d ⇒ 'com Bisimulation_type ⇒ bool"
where
"d_Bisimulation_Up_To_USdB d R ≡ 
  (sym R) ∧ (∀(V,V') ∈ R. length V = length V') ∧
  (∀(V,V') ∈ R. ∀i < length V. ∀m1 m1' W m2.
  ⟨V!i,m1⟩ → ⟨W,m2⟩ ∧ (m1 =⇘d⇙ m1')
  ⟶ (∃W' m2'. ⟨V'!i,m1'⟩ → ⟨W',m2'⟩ 
    ∧ (W,W') ∈ (R ∪ (≈⇘d⇙)) ∧ (m2 =⇘d⇙ m2')))" 

lemma UpTo_aux: "⋀V V' m1 m1' m2 W i. ⟦ d_Bisimulation_Up_To_USdB d R;
  i < length V; (V,V') ∈ R; ⟨V!i,m1⟩ → ⟨W,m2⟩; m1 =⇘d⇙ m1' ⟧
  ⟹ (∃W' m2'. ⟨V'!i,m1'⟩ → ⟨W',m2'⟩ 
  ∧ (W,W') ∈ (R ∪ (≈⇘d⇙)) ∧ (m2 =⇘d⇙ m2'))"
  by (simp add: d_Bisimulation_Up_To_USdB_def, fastforce)

lemma RuUSdBeqlen: 
"⟦ d_Bisimulation_Up_To_USdB d R; 
  (V,V') ∈ (R ∪ (≈⇘d⇙)) ⟧
  ⟹ length V = length V'"
by (auto, simp add: d_Bisimulation_Up_To_USdB_def, auto, 
  rule USdBeqlen, auto)

lemma Up_To_Technique: 
  assumes upToR: "d_Bisimulation_Up_To_USdB d R"
  shows "R ⊆ ≈⇘d⇙"
proof -
  define S where "S = R ∪ (≈⇘d⇙)"
  from S_def have "R ⊆ S"
    by auto
  moreover 
  have "S ⊆ (≈⇘d⇙)"
  proof (simp add: USdB_def, auto, rule_tac x="S" in exI, auto,
      simp add: Strong_d_Bisimulation_def, auto)
      ― ‹show symmetry›
    show symS: "sym S" 
    proof -
      from upToR
      have Rsym: "sym R"
        by (simp add: d_Bisimulation_Up_To_USdB_def)
      with USdBsym have Usym: 
        "sym (R ∪ (≈⇘d⇙))"
        by (metis sym_Un)
      with S_def show ?thesis
        by simp
    qed
  next 
    fix V V'
    assume inS: "(V,V') ∈ S" 
      ― ‹show equal length (by definition)›
    from inS S_def upToR RuUSdBeqlen
    show eqlen: "length V = length V'"             
      by simp
  next
      ― ‹show general bisimulation property›
    fix V V' W m1 m1' m2 i
    assume inS: "(V,V') ∈ S" 
    assume irange: "i < length V"
    assume stepV: "⟨V!i,m1⟩ → ⟨W,m2⟩" 
    assume dequal: "m1 =⇘d⇙ m1'"
    
    from inS show "∃W' m2'. ⟨V'!i,m1'⟩ → ⟨W',m2'⟩ ∧
      (W,W') ∈ S ∧ m2 =⇘d⇙ m2'"
    proof (simp add: S_def, auto)
      assume firstcase: "(V,V') ∈ R" 

      with upToR dequal irange stepV
        UpTo_aux[of "d" "R" "i" "V" "V'" "m1" "W" "m2" "m1'"]
      show "∃W' m2'. ⟨V'!i,m1'⟩ → ⟨W',m2'⟩ ∧
        ((W,W') ∈ R ∨ W ≈⇘d⇙ W') ∧ m2 =⇘d⇙ m2'"
        by (auto simp add: S_def)
    next         
      assume secondcase: "V ≈⇘d⇙ V'"
      
      from USdB_Strong_d_Bisimulation upToR 
        secondcase dequal irange stepV
        strongdB_aux[of "d" "≈⇘d⇙" "i" "V" "V'" "m1" "W" "m2" "m1'"]
      show "∃W' m2'. ⟨V'!i,m1'⟩ → ⟨W',m2'⟩ ∧
        ((W,W') ∈ R ∨ W ≈⇘d⇙ W') ∧ m2 =⇘d⇙ m2'"   
        by auto
    qed
  qed
                    
  ultimately show ?thesis by auto
qed

end

end