Theory Up_To_Technique

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

context WHATWHERE
begin

abbreviation SdlHPPB where "SdlHPPB ≡ Strong_dlHPP_Bisimulation"

--"define the 'reflexive part' of a relation (sets of elements which are related with themselves by the given relation)"
definition Arefl :: "('a × 'a) set => 'a set"
where
"Arefl R = {e. (e,e) ∈ R}"

lemma commonArefl_subset_commonDomain: 
"(Arefl R1 ∩ Arefl R2) ⊆ (Domain R1 ∩ Domain R2)"
  by (simp add: Arefl_def, auto)

--"define disjoint strong (d,lH,PP)-bisimulation up-to-R' for a relation R"
definition disj_dlHPP_Bisimulation_Up_To_R' :: 
  "'d => nat set => 'com Bisimulation_type 
  => 'com Bisimulation_type => bool"
where
"disj_dlHPP_Bisimulation_Up_To_R' d PP R' R ≡
  SdlHPPB d PP R' ∧ (sym R) ∧ (trans R)
  ∧ (∀(V,V') ∈ R. length V = length V') ∧
  (∀(V,V') ∈ R. ∀i < length V. 
    ((NDC d (V!i)) ∨ 
     (IDC d (V!i) (htchLoc (pp (V!i)))))) ∧
  (∀(V,V') ∈ R. ∀i < length V. ∀m1 m1' m2 α p.
    (⟨V!i,m1⟩ ->\<lhd>α\<rhd> ⟨p,m2⟩ ∧ m1 ∼⇘d,(htchLocSet PP)⇙ m1')
    --> (∃p' α' m2'. ⟨V'!i,m1'⟩ ->\<lhd>α'\<rhd> ⟨p',m2'⟩ ∧
        (stepResultsinR p p' (R ∪ R')) ∧ (α,α') ∈ (R ∪ R') ∧ 
        (dhequality_alternative d PP (pp (V!i)) m2 m2')))"

--"lemma about the transitivity of the union of symmetric and transitive relations under certain circumstances"
lemma trans_RuR': 
  assumes transR: "trans R"
  assumes symR: "sym R"
  assumes transR': "trans R'"
  assumes symR': "sym R'"
  assumes eqlenR: "∀(V,V') ∈ R. length V = length V'"
  assumes eqlenR': "∀(V,V') ∈ R'. length V = length V'"
  assumes Areflassump: "(Arefl R ∩ Arefl R') ⊆ {[]}"
  shows "trans (R ∪ R')"
proof -
 { 
   fix V V' V''
   assume p1: "(V,V') ∈ (R ∪ R')"
   assume p2: "(V',V'') ∈ (R ∪ R')"

   from p1 p2 have "(V,V'') ∈ (R ∪ R')"
     proof (auto)
         assume inR1: "(V,V') ∈ R"
         assume inR2: "(V',V'') ∈ R"
         from inR1 inR2 transR show "(V,V'') ∈ R"
           unfolding trans_def
           by blast
       next
         assume inR'1: "(V,V') ∈ R'"
         assume inR'2: "(V',V'') ∈ R'"
         assume notinR': "(V,V'') ∉ R'"
         from inR'1 inR'2 transR' have inR': "(V,V'') ∈ R'"
           unfolding trans_def
           by blast
         from notinR' inR' have "False"
           by auto
         thus "(V,V'') ∈ R" ..
       next
         assume inR1: "(V,V') ∈ R"
         assume inR'2: "(V',V'') ∈ R'"
         from inR1 symR transR have "(V,V) ∈ R ∧ (V',V') ∈ R"
           unfolding sym_def trans_def
           by blast
         hence AreflR: "{V,V'} ⊆ Arefl R" by (simp add: Arefl_def)
         from inR'2 symR' transR' have "(V',V') ∈ R' ∧ (V'',V'') ∈ R'"
           unfolding sym_def trans_def
           by blast
         hence AreflR': "{V',V''} ⊆ Arefl R'" by (simp add: Arefl_def)

         from AreflR AreflR' Areflassump have V'empt: "V' = []" 
           by (simp add: Arefl_def, blast)
         with inR'2 eqlenR' have "V' = V''" by auto
         with inR1 show "(V, V'') ∈ R" by auto
       next
         assume inR'1: "(V,V') ∈ R'"
         assume inR2: "(V',V'') ∈ R"
         from inR'1 symR' transR' have "(V,V) ∈ R' ∧ (V',V') ∈ R'"
           unfolding sym_def trans_def
           by blast
         hence AreflR': "{V,V'} ⊆ Arefl R'" by (simp add: Arefl_def)
         from inR2 symR transR have "(V',V') ∈ R ∧ (V'',V'') ∈ R"
           unfolding sym_def trans_def
           by blast
         hence AreflR: "{V',V''} ⊆ Arefl R" by (simp add: Arefl_def)

         from AreflR AreflR' Areflassump have V'empt: "V' = []" 
           by (simp add: Arefl_def, blast)
         with inR'1 eqlenR' have "V' = V" by auto
         with inR2 show "(V, V'') ∈ R" by auto
       qed        
 }
 thus ?thesis unfolding trans_def by force

qed

lemma Up_To_Technique:
"[| disj_dlHPP_Bisimulation_Up_To_R' d PP R' R; 
  Arefl R ∩ Arefl R' ⊆ {[]} |]
  ==> SdlHPPB d PP (R ∪ R')"
proof (simp add: disj_dlHPP_Bisimulation_Up_To_R'_def 
    Strong_dlHPP_Bisimulation_def, auto)
  assume symR': "sym R'"
  assume symR: "sym R"
  with symR' show "sym (R ∪ R')"
    by (simp add: sym_def)
next
  assume symR': "sym R'"
  assume symR: "sym R"
  assume transR': "trans R'"
  assume transR: "trans R"
  assume eqlenR': "∀(V, V')∈R'. length V = length V'"
  assume eqlenR: "∀(V, V')∈R. length V = length V'"
  assume areflassump: "Arefl R ∩ Arefl R' ⊆ {[]}"
  from symR' symR transR' transR eqlenR' eqlenR areflassump trans_RuR'
  show "trans (R ∪ R')" 
    by blast
  --"condition about IDC and NDC and equal length already proven above by auto tactic!"
next
  fix V V' i m1 m1' m2 α p
  assume inR: "(V,V') ∈ R"
  assume irange: "i < length V"
  assume step: "⟨V!i,m1⟩ ->\<lhd>α\<rhd> ⟨p,m2⟩"
  assume dhequal: "m1 ∼⇘d,(htchLocSet PP)⇙ m1'"
  assume disjBisimUpTo: "∀(V,V')∈R. ∀i < length V. ∀m1 m1' m2 α p.
    ⟨V!i,m1⟩ ->\<lhd>α\<rhd> ⟨p,m2⟩ ∧ m1 ∼⇘d,(htchLocSet PP)⇙ m1' -->
    (∃p' α' m2'. ⟨V'!i,m1'⟩ ->\<lhd>α'\<rhd> ⟨p',m2'⟩ ∧
    stepResultsinR p p' (R ∪ R') ∧ ((α, α') ∈ R ∨ (α, α') ∈ R') ∧
    dhequality_alternative d PP (pp (V!i)) m2 m2')"
  from inR irange step dhequal disjBisimUpTo show "∃p' α' m2'.
    ⟨V'!i,m1'⟩ ->\<lhd>α'\<rhd> ⟨p',m2'⟩ ∧ stepResultsinR p p' (R ∪ R') ∧
    ((α,α') ∈ R ∨ (α,α') ∈ R') ∧ 
    dhequality_alternative d PP (pp (V!i)) m2 m2'"
    by blast
next
  fix V V' i m1 m1' m2 α p
  assume inR': "(V,V') ∈ R'"
  assume irange: "i < length V"
  assume step: "⟨V!i,m1⟩ ->\<lhd>α\<rhd> ⟨p,m2⟩"
  assume dhequal: "m1 ∼⇘d,(htchLocSet PP)⇙ m1'"
  assume disjBisimUpTo: "∀(V,V')∈R'. ∀i < length V. ∀m1 m1' m2 α p.
    ⟨V!i,m1⟩ ->\<lhd>α\<rhd> ⟨p,m2⟩ ∧ m1 ∼⇘d,(htchLocSet PP)⇙ m1' -->
    (∃p' α' m2'. ⟨V'!i,m1'⟩ ->\<lhd>α'\<rhd> ⟨p',m2'⟩ ∧
    stepResultsinR p p' R' ∧ (α, α') ∈ R' ∧
    dhequality_alternative d PP (pp (V!i)) m2 m2')"
  from inR' irange step dhequal disjBisimUpTo show "∃p' α' m2'.
    ⟨V'!i,m1'⟩ ->\<lhd>α'\<rhd> ⟨p',m2'⟩ ∧ stepResultsinR p p' (R ∪ R') ∧
    ((α,α') ∈ R ∨ (α,α') ∈ R') ∧ 
    dhequality_alternative d PP (pp (V!i)) m2 m2'"
    by (simp add: stepResultsinR_def,fastforce)
qed

  
lemma Union_Strong_dlHPP_Bisim:
"[| SdlHPPB d PP R; SdlHPPB d PP R'; 
  Arefl R ∩ Arefl R' ⊆ {[]} |]
  ==> SdlHPPB d PP (R ∪ R')"
by (rule Up_To_Technique, simp_all add: 
  disj_dlHPP_Bisimulation_Up_To_R'_def 
  Strong_dlHPP_Bisimulation_def stepResultsinR_def, fastforce)


lemma adding_emptypair_keeps_SdlHPPB:
  assumes SdlHPP: "SdlHPPB d PP R"
  shows "SdlHPPB d PP (R ∪ {([],[])})"
proof -
  have SdlHPPemp: "SdlHPPB d PP {([],[])}"
    by (simp add: Strong_dlHPP_Bisimulation_def sym_def trans_def)

  have commonDom: "Domain R ∩ Domain {([],[])} ⊆ {[]}"
    by auto

  with commonArefl_subset_commonDomain have Areflassump:
    "Arefl R ∩ Arefl {([],[])} ⊆ {[]}"
    by force

  with SdlHPP SdlHPPemp Union_Strong_dlHPP_Bisim show 
    "SdlHPPB d PP (R ∪ {([],[])})"
    by force
qed

end

end