Theory Language_Prelims

section ‹Prelim›

text ‹ This theory contains some preliminary facts about reflective transistive closure and the comparisons of two symmetric distances, where the later is useful for Relative Security invariants›

theory Language_Prelims imports Main
begin


lemma length_1_butlast[simp]: "length xs = Suc 0 ⟹ butlast xs = []"
by (cases xs, auto)

(* The distance between two sets *)

definition "dist A B ≡ (A - B) ∪ (B - A)"

definition "distL A B ≡ (A - B)"

definition "distR A B ≡ (B - A)"

lemma distLR_int_empt[simp]:"distL A B ∩ distR A B = {} " 
  unfolding distR_def distL_def 
  by auto

lemma distLR_imp_dist:"distL A B ⊆ distL C D ∧ distR A B ⊆ distR C D ⟹ dist A B ⊆ dist C D"
  unfolding dist_def distL_def distR_def 
  by auto


lemma dist_insert: "dist A B = dist C D ⟹ dist (insert x A) (insert x B) = dist (insert x C) (insert x D)"
  unfolding dist_def by auto

lemma dist_refl[simp,intro]: "dist A A = {}"
unfolding dist_def by auto

lemma dist_empty_iff[simp]: "dist A B = {} ⟷ A = B"
unfolding dist_def by auto


lemma dist_match_grow[simp,intro]:"
        dist ls3 ls4 ⊆ dist ls1 ls2 ⟹
     x ∈ dist (insert a ls3) (insert a ls4) ⟹ 
     x ∈ dist (insert a ls1) (insert a ls2)"
  unfolding dist_def by auto

lemma dist_ignore[simp,intro]:"
     dist ls3 ls4 ⊆ dist ls1 ls2 ⟹
     x ∈ dist (insert a ls3) (insert a ls4) ⟹
     x ∈ dist ls1 ls2"

  unfolding dist_def by auto

(*cases: if x is not in either or in both, then dist (insert x A) (insert x B) = dist A B
  otherwise x is in one but not the other, then dist (insert x A) (insert x B) = dist A B - {x}
                                           hence
                                                dist (insert x A) (insert x B) ⊆ dist A B

  thus 
          dist ls3 ls4 ⊆ dist ls1 ls2 ⟹
          dist (insert a ls3) (insert a ls4) ⊆ dist ls1 ls2
*)

lemma dist_insert_su[simp,intro]: "dist (insert x A) (insert x B) ⊆ dist A B"
  unfolding dist_def by auto

lemma dist_ignore_insert[simp,intro]:"
     dist ls3 ls4 ⊆ dist ls1 ls2 ⟹
     dist (insert a ls3) (insert a ls4) ⊆ dist ls1 ls2"

  unfolding dist_def by auto

(*
lemma desired:"
        dist ls3 ls4 ⊆ dist ls1 ls2 ⟹
        dist (insert a ls3) (insert b ls4) ⊆ dist (insert a ls1) (insert b ls2)"
  ls3 = {}
  ls4 = {}
  ls1 = {a⇩1}
  ls2 = {}
  a = a⇩2
  b = a⇩1
*)

(*a sufficiently powerful premise*)
lemma dist_match_diff[simp,intro]:"
        dist ls3 ls4 ⊆ dist ls1 ls2 ⟹
        ls1 ⊂ ls3 ⟹ ls2 ⊂ ls4 ⟹
        dist (insert a ls3) (insert b ls4) ⊆ dist (insert a ls1) (insert b ls2)"
  unfolding dist_def by auto

lemma list_one[intro]:"A ≠ {a} ⟹ A ⊆ {a} ⟹ A = {}"
  by auto

lemma dist_match_grow_diff[simp,intro]:"
        dist ls3 ls4 ⊆ dist ls1 ls2 ⟹
        ls1 ⊆ ls3 ⟹ ls2 ⊆ ls4 ⟹
     x ∈ dist (insert a ls3) (insert b ls4) ⟹ 
     x ∈ dist (insert a ls1) (insert b ls2)"
  unfolding dist_def by auto

lemma dist_match_grow_diff1[simp,intro]:"dist C D ⊆ dist A B ⟹
    A ⊆ C ⟹
    B ⊆ D ⟹
    dist (insert a C) (insert b D)
    ⊆ dist (insert a A) (insert b B)" 
  using dist_match_grow_diff subsetI by auto

lemma dist_eq_grow_ab:"dist C D ⊆ dist A B ⟹
    A ⊆ C ⟹
    B ⊆ D ⟹
    dist (C ∪ a) (D ∪ b)
    ⊆ dist (A ∪ a) (B ∪ b)" 
  unfolding dist_def by auto 

lemma dist_eq_grow:"
dist C D ⊆ dist A B ⟹ A ⊆ C ⟹ B ⊆ D ⟹
dist (C ∪ a) (D ∪ a) ⊆ dist (A ∪ a) (B ∪ a)"
  using dist_eq_grow_ab by metis

lemma dist_ignore_grow:"
dist C D ⊆ dist A B ⟹ A ⊆ C ⟹ B ⊆ D ⟹
dist (C ∪ a) (D ∪ a) ⊆ dist A B"
  unfolding dist_def by auto


(*distL intros*)

lemma distL_insert: "distL A B = distL C D ⟹ distL (insert x A) (insert x B) = distL (insert x C) (insert x D)"
  unfolding distL_def by auto

lemma distL_refl[simp,intro]: "distL A A = {}"
unfolding distL_def by auto

lemma distL_insert_su[simp,intro]: "distL (insert x A) (insert x B) ⊆ distL A B"
  unfolding distL_def by auto


(*distR intros*)
lemma distR_insert: "distR A B = distR C D ⟹ distR (insert x A) (insert x B) = distR (insert x C) (insert x D)"
  unfolding distR_def by auto

lemma distR_refl[simp,intro]: "distR A A = {}"
unfolding distR_def by auto

lemma distR_insert_su[simp,intro]: "distR (insert x A) (insert x B) ⊆ distR A B"
unfolding distR_def by auto




lemma insert_null_grow[simp]:"a ∈ ls3 ⟹ insert a ls3 = ls3" by auto

lemma distL_match_grow_aux:"distL ls3 ls4 ⊆ distL ls1 ls2 ⟹
ls1 ⊂ ls3 ⟹ls2 ⊂ ls4 ⟹
        distL (insert a ls3) (insert b ls4)
     ⊆ distL (insert a ls1) (insert b ls2)"
  unfolding distL_def
  apply (cases "a=b")
  subgoal by blast
  subgoal
    apply (cases "a ∈ ls3", cases "b ∈ ls4")  
    apply simp
      apply (cases "b ∈ ls2")
    by (cases "b ∈ ls2", auto) . 



lemma distR_match_grow_aux:"distR ls3 ls4 ⊆ distR ls1 ls2 ⟹
ls1 ⊂ ls3 ⟹ls2 ⊂ ls4 ⟹
        distR (insert a ls3) (insert b ls4)
     ⊆ distR (insert a ls1) (insert b ls2)"

unfolding distR_def
  apply (cases "a=b")
  subgoal by blast
  subgoal
    apply (cases "b ∈ ls2")  
      apply (cases "a ∈ ls2")
    by (cases "a ∈ ls4", auto) .

lemma distL_match_grow: "distL ls3 ls4 ⊆ distL ls1 ls2 ⟹
ls1 ⊆ ls3 ⟹ls2 ⊆ ls4 ⟹ (ls1 = ls3 ⟷ ls2 = ls4) ⟹
        distL (insert a ls3) (insert b ls4)
     ⊆ distL (insert a ls1) (insert b ls2)"
  apply(cases "ls1 = ls3")
  subgoal by (metis Diff_mono Set.insert_mono distL_def)
  subgoal apply(cases "ls2 = ls4") by (simp add: distL_match_grow_aux)+ .


lemma distR_match_grow:"distR ls3 ls4 ⊆ distR ls1 ls2 ⟹
ls1 ⊆ ls3 ⟹ls2 ⊆ ls4 ⟹ (ls1 = ls3 ⟷ ls2 = ls4) ⟹
        distR (insert a ls3) (insert b ls4)
     ⊆ distR (insert a ls1) (insert b ls2)"
  apply(cases "ls1 = ls3")
  subgoal by (metis Diff_mono Set.insert_mono distR_def)
  subgoal apply(cases "ls2 = ls4") by (simp add: distR_match_grow_aux)+ .

definition Dist where "Dist ls1 ls2 ls3 ls4 =
 (Language_Prelims.dist ls3 ls4 ⊆ Language_Prelims.dist ls1 ls2 ∧ ls1 ⊆ ls3 ∧ ls2 ⊆ ls4)"

lemmas Dist_defs = Dist_def dist_def

lemma Dist_neq[simp]:"Dist ls1 ls2 ls3 ls4 ⟹ ls3 ≠ ls4 ⟹ ls1 ≠ ls2"
  unfolding Dist_def by auto

lemma Dist_eq[simp]:"Dist A B A B" by (simp add: Dist_def)
(*istate*)
lemma Dist_emp[simp]:"Dist {} {} {} {}" by (simp add: Dist_def)

(*for match*)
lemma Dist_match[intro]:"Dist ls1 ls2 ls3 ls4 ⟹ Dist (insert a ls1) (insert b ls2) (insert a ls3) (insert b ls4)"
  by (metis Dist_def Set.insert_mono dist_match_grow_diff1)

lemma Dist_match_un[intro]:"Dist ls1 ls2 ls3 ls4 ⟹ Dist (ls1 ∪ a) (ls2 ∪ b) (ls3 ∪ a) (ls4 ∪ b)"
  unfolding Dist_def by (metis dist_eq_grow_ab subset_refl sup_mono)

(*for ignore*)
lemma Dist_ignore[intro]:"Dist ls1 ls2 ls3 ls4 ⟹ Dist ls1 ls2 (insert a ls3) (insert a ls4)"
  by (meson Dist_def dist_insert_su dual_order.trans subset_insertI)

lemma Dist_ignore_un[intro]:"Dist ls1 ls2 ls3 ls4 ⟹ Dist ls1 ls2 (ls3 ∪ a) (ls4 ∪ a)"
  unfolding Dist_def by (simp add: dist_ignore_grow le_supI1)

(* Various reflexive-transitive closure operators *)

inductive
  star :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool"
for r where
refl:  "star r x x" |
step:  "r x y ⟹ star r y z ⟹ star r x z"

hide_fact (open) refl step  ― ‹names too generic›

lemma star_trans:
  "star r x y ⟹ star r y z ⟹ star r x z"
proof(induction rule: star.induct)
  case refl thus ?case .
next
  case step thus ?case by (metis star.step)
qed

lemmas star_induct =
  star.induct[of "r:: 'a*'b ⇒ 'a*'b ⇒ bool", split_format(complete)]

lemmas star_induct4 =
  star.induct[of "r:: 'a*'b'*'c*'d ⇒ 'a*'b'*'c*'d ⇒ bool", split_format(complete)]

declare star.refl[simp,intro]

lemma star_step1[simp, intro]: "r x y ⟹ star r x y"
by(metis star.refl star.step)

code_pred star .

(* *)

inductive
  starn :: "('a ⇒ 'a ⇒ bool) ⇒ nat ⇒ 'a ⇒ 'a ⇒ bool"
for r where
refl:  "starn r 0 x x" |
step:  "r x y ⟹ starn r n y z ⟹ starn r (Suc n)x z"

hide_fact (open) refl step  ― ‹names too generic›

lemma starn_trans:
  "starn r m x y ⟹ starn r n y z ⟹ starn r (m+n) x z"
proof(induction rule: starn.induct)
  case refl thus ?case by simp
next
  case step thus ?case by simp (metis starn.step)
qed

lemmas starn_induct =
  starn.induct[of "r:: 'a*'b ⇒ 'a*'b ⇒ bool", split_format(complete)]

declare starn.refl[simp,intro]

lemma starn_step1[simp, intro]: "r x y ⟹ starn r (Suc 0) x y"
by(metis starn.refl starn.step)

code_pred starn .

lemma star_starn: "star r x y ⟹ ∃n. starn r n x y"
by (induct rule: star.induct, auto intro: starn.intros)

lemma starn_star: "starn r n x y ⟹ star r x y"
by (induct rule: starn.induct, auto intro: star.intros)

lemma star_iff_starn: "star r x y ⟷ (∃n. starn r n x y)"
by (meson star_starn starn_star)

(* *)

inductive
  starl :: "('a ⇒ 'c ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'c list ⇒ 'a ⇒ bool"
for r where
refl:  "starl r x [] x" |
step:  "r x c y ⟹ starl r y cs z ⟹ starl r x (c#cs) z"

hide_fact (open) refl step  ― ‹names too generic›

lemma starl_trans:
  "starl r x cs y ⟹ starl r y ds z ⟹ starl r x (cs @ ds) z"
proof(induction rule: starl.induct)
  case refl thus ?case by simp
next
  case step thus ?case by simp (metis starl.step)
qed

lemmas starl_induct =
  starl.induct[of "r:: 'a*'b ⇒ 'clist ⇒ 'a*'b ⇒ bool", split_format(complete)]

declare starl.refl[simp,intro]

lemma starl_step1[simp, intro]: "r x c y ⟹ starl r x [c] y"
by(metis starl.refl starl.step)

lemma starl_snoc:
  "starl r x cs y ⟹ r y c z ⟹ starl r x (cs @ [c]) z"
by (simp add: starl_trans)

code_pred starl .

definition "final r x ≡ ∀y. ¬ r x y"

lemma final_star_eq: "final r x ⟹ star r x y ⟹ x = y"
by (metis final_def star.cases)

definition "lfinal r x ≡ ∀y cs. ¬ r x cs y"


end