Theory AList-Utils-Nominal

theory "AList-Utils-Nominal"
imports "AList-Utils" "Nominal-Utils"
begin

subsubsection {* Freshness lemmas related to associative lists *}

lemma domA_not_fresh:
  "x ∈ domA Γ ⟹ ¬(atom x ♯ Γ)"
  by (induct Γ, auto simp add: fresh_Cons fresh_Pair)

lemma fresh_delete:
  assumes "a ♯ Γ"
  shows "a ♯ delete v Γ"
using assms
by(induct Γ)(auto simp add: fresh_Cons)

lemma fresh_star_delete:
  assumes "S ♯* Γ"
  shows "S ♯* delete v Γ"
  using assms fresh_delete unfolding fresh_star_def by fastforce

lemma fv_delete_subset:
  "fv (delete v Γ) ⊆ fv Γ"
  using fresh_delete unfolding fresh_def fv_def by auto

lemma fresh_heap_expr:
  assumes "a ♯ Γ"
  and "(x,e) ∈ set Γ"
  shows "a ♯ e"
  using assms
  by (metis fresh_list_elem fresh_Pair)

lemma fresh_heap_expr':
  assumes "a ♯ Γ"
  and "e ∈ snd ` set Γ"
  shows "a ♯ e"
  using assms
  by (induct Γ, auto simp add: fresh_Cons fresh_Pair)

lemma fresh_star_heap_expr':
  assumes "S ♯* Γ"
  and "e ∈ snd ` set Γ"
  shows "S ♯* e"
  using assms
  by (metis fresh_star_def fresh_heap_expr')

lemma fresh_map_of:
  assumes "x ∈ domA Γ"
  assumes "a ♯ Γ"
  shows "a ♯ the (map_of Γ x)"
  using assms
  by (induct Γ)(auto simp add: fresh_Cons fresh_Pair)

lemma fresh_star_map_of:
  assumes "x ∈ domA Γ"
  assumes "a ♯* Γ"
  shows "a ♯* the (map_of Γ x)"
  using assms by (simp add: fresh_star_def fresh_map_of)

lemma domA_fv_subset: "domA Γ ⊆ fv Γ"
  by (induction Γ) auto

lemma map_of_fv_subset: "x ∈ domA Γ ⟹ fv (the (map_of Γ x)) ⊆ fv Γ"
  by (induction Γ) auto

lemma map_of_Some_fv_subset: "map_of Γ x = Some e ⟹ fv e ⊆ fv Γ"
  by (metis domA_from_set map_of_fv_subset map_of_SomeD option.sel)

subsubsection {* Equivariance lemmas *}

lemma domA[eqvt]:
  "π ∙ domA Γ = domA (π ∙ Γ)"
  by (simp add: domA_def)

lemma mapCollect[eqvt]:
  "π ∙ mapCollect f m = mapCollect (π ∙ f) (π ∙ m)"
unfolding mapCollect_def
by perm_simp rule

subsubsection {* Freshness and distinctness *}

lemma fresh_distinct:
 assumes "atom ` S ♯* Γ"
 shows "S ∩ domA Γ = {}"
proof-
  { fix x
    assume "x ∈ S"
    moreover
    assume "x ∈ domA Γ"
    hence "atom x ∈ supp Γ"
      by (induct Γ)(auto simp add: supp_Cons domA_def supp_Pair supp_at_base)
    ultimately
    have False
      using assms
      by (simp add: fresh_star_def fresh_def)
  }
  thus "S ∩ domA Γ = {}" by auto
qed

lemma fresh_distinct_list:
 assumes "atom ` S ♯* l"
 shows "S ∩ set l = {}"
 using assms
 by (metis disjoint_iff_not_equal fresh_list_elem fresh_star_def image_eqI not_self_fresh)

lemma fresh_distinct_fv:
 assumes "atom ` S ♯* l"
 shows "S ∩ fv l = {}"
 using assms
 by (metis disjoint_iff_not_equal fresh_star_def fv_not_fresh image_eqI)

subsubsection {* Pure codomains *}

lemma domA_fv_pure:
  fixes Γ :: "('a::at_base × 'b::pure) list"
  shows  "fv Γ = domA Γ"
  apply (induct Γ)
  apply simp
  apply (case_tac a)
  apply (simp)
  done

lemma domA_fresh_pure:
  fixes Γ :: "('a::at_base × 'b::pure) list"
  shows  "x ∈ domA Γ ⟷ ¬(atom x ♯ Γ)"
  unfolding domA_fv_pure[symmetric]
  by (auto simp add: fv_def fresh_def)

end