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