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 →⊲α p,m2  m1 ∼⇘d,(htchLocSet PP)m1')
     (p' α' m2'. V'!i,m1' →⊲α' 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 →⊲α p,m2"
  assume dhequal: "m1 ∼⇘d,(htchLocSet PP)m1'"
  assume disjBisimUpTo: "(V,V')R'. i < length V. m1 m1' m2 α p.
    V!i,m1 →⊲α p,m2  m1 ∼⇘d,(htchLocSet PP)m1' 
    (p' α' m2'. V'!i,m1' →⊲α' 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' →⊲α' 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