Theory NU_Fresh

(*<*)
theory NU_Fresh
imports NU_Disagreement
begin
(*>*)

section ‹Freshness›

text ‹
Defines the freshness relation and shows facts about its behaviour under swappings.
›

type_synonym fresh_envs = "(string × string) set"

inductive fresh :: "fresh_envs ⇒ string ⇒ trm ⇒ bool" (" _ ⊢ _ ♯ _" [80,80,80] 80) 
  where
  fresh_abst_ab[intro!]: "⟦nabla ⊢ a ♯ t; a≠b⟧ ⟹ nabla ⊢ a ♯ Abst b t" |
  fresh_abst_aa[intro!]: "nabla ⊢ a ♯ Abst a t" |
  fresh_unit[intro!]:    "nabla ⊢ a ♯ Unit" |
  fresh_atom[intro!]:    "a ≠ b ⟹ nabla ⊢ a ♯ Atom b" |
  fresh_susp[intro!]:    "(swapas (rev pi) a,X) ∈ nabla ⟹ nabla ⊢ a ♯ Susp pi X" |
  fresh_paar[intro!]:    "⟦nabla ⊢ a ♯ t1; nabla ⊢ a ♯ t2⟧ ⟹ nabla ⊢ a ♯ Paar t1 t2" |
  fresh_func[intro!]:    "nabla ⊢ a ♯ t ⟹ nabla ⊢ a ♯ Func F t"

inductive_cases Fresh_elims:
  "nabla ⊢ a ♯ Abst b t"
  "nabla ⊢ a ♯ Unit"
  "nabla ⊢ a ♯ Atom b"
  "nabla ⊢ a ♯ Susp pi X"
  "nabla ⊢ a ♯ Paar t1 t2"
  "nabla ⊢ a ♯ Func F t"

lemma fresh_swap_eqvt: 
  assumes "nabla ⊢ a ♯ t"
  shows "nabla ⊢ swapas pi a ♯ swap pi t"
  using assms
  by (induct arbitrary: pi rule: fresh.induct)
(auto simp add: swapas_append dest: swapas_rev_pi_a)


lemma fresh_swap_left: 
  assumes "nabla ⊢ a ♯ swap pi t"
  shows "nabla ⊢ swapas (rev pi) a ♯ t"
  using assms
proof(induct t arbitrary: a pi)
  case (Abst x1 t)
  have "nabla ⊢ a ♯ swap pi (Abst x1 t)" by fact
  then have "(nabla ⊢ a ♯ swap pi t ∧ a ≠ swapas pi x1) ∨ (a = swapas pi x1)"
    by (metis Fresh_elims(1) swap.simps(4))
  moreover {
    assume as: "nabla ⊢ a ♯ swap pi t ∧ a ≠ swapas pi x1" 
    have "nabla ⊢ swapas (rev pi) a ♯ Abst x1 t"
      using Abst.hyps as by auto 
  }
  moreover {
    assume as: "a = swapas pi x1"
    then have "nabla ⊢ swapas (rev pi) a ♯ Abst x1 t"
      by (simp add: fresh_abst_aa)      
  } 
  ultimately show "nabla ⊢ swapas (rev pi) a ♯ Abst x1 t" 
    by argo
next
  case (Susp x1 x2)
  have "nabla ⊢ a ♯ swap pi (Susp x1 x2)" by fact
  have "(swapas (rev x1) (swapas (rev pi) a), x2) ∈ nabla"
    by (metis Fresh_elims(4) Susp rev_append swap.simps(3) swapas_append) 
  then show "nabla ⊢ swapas (rev pi) a ♯ Susp x1 x2"
    by (simp add: fresh_susp)
next
  case (Atom x)
  have "nabla ⊢ a ♯ swap pi (Atom x)" by fact
  then have "swapas pi x ≠ a" by (auto elim: Fresh_elims)
  then have "x ≠ swapas (rev pi) a" using swapas_rev_pi_b by blast  
  then show "nabla ⊢ swapas (rev pi) a ♯ Atom x"
    by (simp add: fresh_atom) 
qed (auto elim: Fresh_elims)

lemma fresh_swap_right: 
  assumes "nabla ⊢ swapas (rev pi) a ♯ t"
  shows "nabla ⊢ a ♯ swap pi t"
  using assms fresh_swap_eqvt[of nabla ‹swapas (rev pi) a› t pi] 
    swapas_rev_swapas_id[of pi a] by simp

lemma fresh_weak: 
  assumes "nabla1 ⊢ a ♯ t"
  shows "(nabla1 ∪ nabla2) ⊢ a ♯ t"
  using assms
  by(induct rule: fresh.induct)(auto)

lemma ds_empty_fresh_1:
  assumes "ds pi1 pi2 = {}"
  shows "nabla ⊢ swapas pi1 a ♯ t ⟹ nabla ⊢ swapas pi2 a ♯ t"
  using assms ds_swapas_eq by simp

lemma ds_empty_fresh_2:
  assumes "ds pi1 pi2 = {}"
  shows "nabla ⊢ a ♯ swap pi1 t ⟹ nabla ⊢ a ♯ swap pi2 t"
  using assms 
proof-
  assume assm1: "nabla ⊢ a ♯ swap pi1 t"
  have i: "swapas (rev pi1) a = swapas (rev pi2) a"
    using assms ds_swapas_eq swapas_rev_pi_a by metis
  with assms have ii: "nabla ⊢ swapas (rev pi2) a ♯ t"
    using fresh_swap_left[OF assm1] i by simp
  show ?thesis 
    using fresh_swap_right[OF ii] by simp
qed


(*<*)
end 
(*>*)