Theory Nominal-Utils

theory "Nominal-Utils"
imports "../Nominal2/Nominal2" "~~/src/HOL/Library/AList"
begin

subsubsection {* Lemmas helping with equivariance proofs *}

lemma perm_rel_lemma:
  assumes "⋀ π x y. r (π ∙ x) (π ∙ y) ⟹ r x y"
  shows "r (π ∙ x) (π ∙ y) ⟷ r x y" (is "?l ⟷ ?r")
by (metis (full_types) assms permute_minus_cancel(2))

lemma perm_rel_lemma2:
  assumes "⋀ π x y. r x y ⟹ r (π ∙ x) (π ∙ y)"
  shows "r x y ⟷ r (π ∙ x) (π ∙ y)" (is "?l ⟷ ?r")
by (metis (full_types) assms permute_minus_cancel(2))

lemma fun_eqvtI:
  assumes f_eqvt[eqvt]: "(⋀ p x. p ∙ (f x) = f (p ∙ x))"
  shows "p ∙ f = f" by perm_simp rule

lemma eqvt_at_apply:
  assumes "eqvt_at f x"
  shows "(p ∙ f) x = f x"
by (metis (hide_lams, no_types) assms eqvt_at_def permute_fun_def permute_minus_cancel(1))

lemma eqvt_at_apply':
  assumes "eqvt_at f x"
  shows "p ∙ f x = f (p ∙ x)"
by (metis (hide_lams, no_types) assms eqvt_at_def)

lemma eqvt_at_apply'':
  assumes "eqvt_at f x"
  shows "(p ∙ f) (p ∙ x) = f (p ∙ x)"
by (metis (hide_lams, no_types) assms eqvt_at_def permute_fun_def permute_minus_cancel(1))


lemma size_list_eqvt[eqvt]: "p ∙ size_list f x = size_list (p ∙ f) (p ∙ x)"
proof (induction x)
  case (Cons x xs)
  have "f x = p ∙ (f x)" by (simp add: permute_pure)
  also have "... = (p ∙ f) (p ∙ x)" by simp
  with Cons
  show ?case by (auto simp add: permute_pure)
qed simp

subsubsection {* Freshness via equivariance *}

lemma eqvt_fresh_cong1: "(⋀p x. p ∙ (f x) = f (p ∙ x)) ⟹ a ♯ x ⟹ a ♯ f x "
  apply (rule fresh_fun_eqvt_app[of f])
  apply (rule eqvtI)
  apply (rule eq_reflection)
  apply (rule ext)
  apply (metis permute_fun_def permute_minus_cancel(1))
  apply assumption
  done

lemma eqvt_fresh_cong2:
  assumes eqvt: "(⋀p x y. p ∙ (f x y) = f (p ∙ x) (p ∙ y))"
  and fresh1: "a ♯ x" and fresh2: "a ♯ y"
  shows "a ♯ f x y"
proof-
  have "eqvt (λ (x,y). f x y)"
    using eqvt
    apply -
    apply (auto simp add: eqvt_def)
    apply (rule ext)
    apply auto
    by (metis permute_minus_cancel(1))
  moreover
  have "a ♯ (x, y)" using fresh1 fresh2 by auto
  ultimately
  have "a ♯ (λ (x,y). f x y) (x, y)" by (rule fresh_fun_eqvt_app)
  thus ?thesis by simp
qed

lemma eqvt_fresh_star_cong1:
  assumes eqvt: "(⋀p x. p ∙ (f x) = f (p ∙ x))"
  and fresh1: "a ♯* x"
  shows "a ♯* f x"
  by (metis fresh_star_def eqvt_fresh_cong1 assms)

lemma eqvt_fresh_star_cong2:
  assumes eqvt: "(⋀p x y. p ∙ (f x y) = f (p ∙ x) (p ∙ y))"
  and fresh1: "a ♯* x" and fresh2: "a ♯* y"
  shows "a ♯* f x y"
  by (metis fresh_star_def eqvt_fresh_cong2 assms)

lemma eqvt_fresh_cong3:
  assumes eqvt: "(⋀p x y z. p ∙ (f x y z) = f (p ∙ x) (p ∙ y) (p ∙ z))"
  and fresh1: "a ♯ x" and fresh2: "a ♯ y" and fresh3: "a ♯ z"
  shows "a ♯ f x y z"
proof-
  have "eqvt (λ (x,y,z). f x y z)"
    using eqvt
    apply -
    apply (auto simp add: eqvt_def)
    apply (rule ext)
    apply auto
    by (metis permute_minus_cancel(1))
  moreover
  have "a ♯ (x, y, z)" using fresh1 fresh2 fresh3 by auto
  ultimately
  have "a ♯ (λ (x,y,z). f x y z) (x, y, z)" by (rule fresh_fun_eqvt_app)
  thus ?thesis by simp
qed

lemma eqvt_fresh_star_cong3:
  assumes eqvt: "(⋀p x y z. p ∙ (f x y z) = f (p ∙ x) (p ∙ y) (p ∙ z))"
  and fresh1: "a ♯* x" and fresh2: "a ♯* y" and fresh3: "a ♯* z"
  shows "a ♯* f x y z"
  by (metis fresh_star_def eqvt_fresh_cong3 assms)

subsubsection {* Additional simplification rules *}

lemma not_self_fresh[simp]: "atom x ♯ x ⟷ False"
  by (metis fresh_at_base(2))

lemma fresh_star_singleton: "{ x } ♯* e ⟷ x ♯ e"
  by (simp add: fresh_star_def)

subsubsection {* Additional equivariance lemmas *}

lemma eqvt_cases:
  fixes f x π
  assumes eqvt: "⋀x. π ∙ f x = f (π ∙ x)"
  obtains "f x" "f (π ∙ x)" | "¬ f x " " ¬ f (π ∙ x)"
  using assms[symmetric]
   by (cases "f x") auto

lemma range_eqvt: "π ∙ range Y = range (π ∙ Y)"
  unfolding image_eqvt UNIV_eqvt ..

lemma case_option_eqvt[eqvt]:
  "π ∙ case_option d f x = case_option (π ∙ d) (π ∙ f) (π ∙ x)"
  by(cases x)(simp_all)

lemma supp_option_eqvt:
  "supp (case_option d f x) ⊆ supp d ∪ supp f ∪ supp x"
  apply (cases x)
  apply (auto simp add: supp_Some )
  apply (metis (mono_tags) Un_iff subsetCE supp_fun_app)
  done

lemma funpow_eqvt[simp,eqvt]:
  "π ∙ ((f :: 'a ⇒ 'a::pt) ^^ n) = (π ∙ f) ^^ (π ∙ n)"
 apply (induct n)
 apply simp
 apply (rule ext)
 apply simp
 apply perm_simp
 apply simp
 done

lemma delete_eqvt[eqvt]:
  "π ∙ AList.delete x Γ = AList.delete (π ∙ x) (π ∙ Γ)"
by (induct Γ, auto)

lemma restrict_eqvt[eqvt]:
  "π ∙ AList.restrict S Γ = AList.restrict (π ∙ S) (π ∙ Γ)"
unfolding AList.restrict_eq by perm_simp rule

lemma supp_restrict:
  "supp (AList.restrict S Γ) ⊆ supp Γ"
 by (induction Γ) (auto simp add: supp_Pair supp_Cons)

lemma clearjunk_eqvt[eqvt]:
  "π ∙ AList.clearjunk Γ = AList.clearjunk (π ∙ Γ)"
  by (induction Γ rule: clearjunk.induct) auto

lemma map_ran_eqvt[eqvt]:
  "π ∙ map_ran f Γ = map_ran (π ∙ f) (π ∙ Γ)"
by (induct Γ, auto)

lemma dom_perm:
  "dom (π ∙ f) = π ∙ (dom f)"
  unfolding dom_def by (perm_simp) (simp)

lemmas dom_perm_rev[simp,eqvt] = dom_perm[symmetric]

lemma ran_perm[simp]:
  "π ∙ (ran f) = ran (π ∙ f)"
  unfolding ran_def by (perm_simp) (simp)

lemma map_add_eqvt[eqvt]:
  "π ∙ (m1 ++ m2) = (π ∙ m1) ++ (π ∙ m2)"
  unfolding map_add_def
  by (perm_simp, rule)

lemma map_of_eqvt[eqvt]:
  "π ∙ map_of l = map_of (π ∙ l)"
  apply (induct l)
  apply (simp add: permute_fun_def)
  apply simp
  apply perm_simp
  apply auto
  done

lemma concat_eqvt[eqvt]: "π ∙ concat l = concat (π ∙ l)"
  by (induction l)(auto simp add: append_eqvt)

lemma tranclp_eqvt[eqvt]: "π ∙ tranclp P v⇩1 v⇩2 = tranclp (π ∙ P) (π ∙ v⇩1) (π ∙ v⇩2)" 
  unfolding tranclp_def by perm_simp rule

lemma rtranclp_eqvt[eqvt]: "π ∙ rtranclp P v⇩1 v⇩2 = rtranclp (π ∙ P) (π ∙ v⇩1) (π ∙ v⇩2)" 
  unfolding rtranclp_def by perm_simp rule

lemma Set_filter_eqvt[eqvt]: "π ∙ Set.filter P S = Set.filter (π ∙ P) (π ∙ S)"
  unfolding Set.filter_def
  by perm_simp rule

lemma Sigma_eqvt'[eqvt]: "π ∙ Sigma = Sigma"
  apply (rule ext)
  apply (rule ext)
  apply (subst permute_fun_def)
  apply (subst permute_fun_def)
  unfolding Sigma_def
  apply perm_simp
  apply (simp add: permute_self)
  done

lemma override_on_eqvt[eqvt]:
  "π ∙ (override_on m1 m2 S) = override_on (π ∙ m1) (π ∙ m2) (π ∙ S)"
  by (auto simp add: override_on_def )

lemma card_eqvt[eqvt]:
  "π ∙ (card S) = card (π ∙ S)"
by (cases "finite S", induct rule: finite_induct) (auto simp add: card_insert_if mem_permute_iff permute_pure)

(* Helper lemmas provided by Christian Urban *)

lemma Projl_permute:
  assumes a: "∃y. f = Inl y"
  shows "(p ∙ (Sum_Type.projl f)) = Sum_Type.projl (p ∙ f)"
using a by auto

lemma Projr_permute:
  assumes a: "∃y. f = Inr y"
  shows "(p ∙ (Sum_Type.projr f)) = Sum_Type.projr (p ∙ f)"
using a by auto


subsubsection {* Freshness lemmas *}

lemma fresh_list_elem:
  assumes "a ♯ Γ"
  and "e ∈ set Γ"
  shows "a ♯ e"
using assms
by(induct Γ)(auto simp add: fresh_Cons)

lemma set_not_fresh:
  "x ∈ set L ⟹ ¬(atom x ♯ L)"
  by (metis fresh_list_elem not_self_fresh)

lemma pure_fresh_star[simp]: "a ♯* (x :: 'a :: pure)"
  by (simp add: fresh_star_def pure_fresh)

lemma supp_set_mem: "x ∈ set L ⟹ supp x ⊆ supp L"
  by (induct L) (auto simp add: supp_Cons)

lemma set_supp_mono: "set L ⊆ set L2 ⟹ supp L ⊆ supp L2"
  by (induct L)(auto simp add: supp_Cons supp_Nil dest:supp_set_mem)

lemma fresh_star_at_base:
  fixes x :: "'a :: at_base"
  shows "S ♯* x ⟷ atom x ∉ S"
  by (metis fresh_at_base(2) fresh_star_def)


subsubsection {* Freshness and support for subsets of variables *}

lemma supp_mono: "finite (B::'a::fs set) ⟹ A ⊆ B ⟹ supp A ⊆ supp B"
  by (metis infinite_super subset_Un_eq supp_of_finite_union)

lemma fresh_subset:
  "finite B ⟹ x ♯ (B :: 'a::at_base set) ⟹ A ⊆ B ⟹ x ♯ A"
  by (auto dest:supp_mono simp add: fresh_def)

lemma fresh_star_subset:
  "finite B ⟹ x ♯* (B :: 'a::at_base set) ⟹ A ⊆ B ⟹ x ♯* A"
  by (metis fresh_star_def fresh_subset)

lemma fresh_star_set_subset:
  "x ♯* (B :: 'a::at_base list) ⟹ set A ⊆ set B ⟹ x ♯* A"
  by (metis fresh_star_set fresh_star_subset[OF finite_set])

subsubsection {* The set of free variables of an expression *}

definition fv :: "'a::pt ⇒ 'b::at_base set"
  where "fv e = {v. atom v ∈ supp e}"

lemma fv_eqvt[simp,eqvt]: "π ∙ (fv e) = fv (π ∙ e)"
  unfolding fv_def by simp

lemma fv_Nil[simp]: "fv [] = {}"
  by (auto simp add: fv_def supp_Nil)
lemma fv_Cons[simp]: "fv (x # xs) = fv x ∪ fv xs"
  by (auto simp add: fv_def supp_Cons)
lemma fv_Pair[simp]: "fv (x, y) = fv x ∪ fv y"
  by (auto simp add: fv_def supp_Pair)
lemma fv_append[simp]: "fv (x @ y) = fv x ∪ fv y"
  by (auto simp add: fv_def supp_append)
lemma fv_at_base[simp]: "fv a = {a::'a::at_base}"
  by (auto simp add: fv_def supp_at_base)
lemma fv_pure[simp]: "fv (a::'a::pure) = {}"
  by (auto simp add: fv_def pure_supp)

lemma fv_set_at_base[simp]: "fv (l :: ('a :: at_base) list) = set l"
  by (induction l) auto

lemma flip_not_fv: "a ∉ fv x ⟹ b ∉ fv x ⟹ (a ↔ b) ∙ x = x"
  by (metis flip_def fresh_def fv_def mem_Collect_eq swap_fresh_fresh)

lemma fv_not_fresh: "atom x ♯ e ⟷ x ∉ fv e"
  unfolding fv_def fresh_def by blast

lemma fresh_fv: "finite (fv e :: 'a set) ⟹  atom (x :: ('a::at_base)) ♯ (fv e :: 'a set) ⟷ atom x ♯ e"
  unfolding fv_def fresh_def
  by (auto simp add: supp_finite_set_at_base)

lemma finite_fv[simp]: "finite (fv (e::'a::fs) :: ('b::at_base) set)"
proof-
  have "finite (supp e)" by (metis finite_supp)
  hence "finite (atom -` supp e :: 'b set)" 
    apply (rule finite_vimageI)
    apply (rule inj_onI)
    apply (simp)
    done
  moreover
  have "(atom -` supp e  :: 'b set) = fv e"   unfolding fv_def by auto
  ultimately
  show ?thesis by simp
qed

definition fv_list :: "'a::fs ⇒ 'b::at_base list"
  where "fv_list e = (SOME l. set l = fv e)"

lemma set_fv_list[simp]: "set (fv_list e) = (fv e :: ('b::at_base) set)"
proof-
  have "finite (fv e :: 'b set)" by (rule finite_fv)
  from finite_list[OF finite_fv]
  obtain l where "set l = (fv e :: 'b set)"..
  thus ?thesis
    unfolding fv_list_def by (rule someI)
qed

lemma fresh_fv_list[simp]:
  "a ♯ (fv_list e :: 'b::at_base list) ⟷ a ♯ (fv e :: 'b::at_base set)"
proof-
  have "a ♯ (fv_list e :: 'b::at_base list) ⟷ a ♯ set (fv_list e :: 'b::at_base list)"
    by (rule fresh_set[symmetric])
  also have "… ⟷ a ♯ (fv e :: 'b::at_base set)" by simp
  finally show ?thesis.
qed


subsubsection {* Other useful lemmas *}

lemma pure_permute_id: "permute p = (λ x. (x::'a::pure))"
  by rule (simp add: permute_pure)

lemma supp_set_elem_finite:
  assumes "finite S"
  and "(m::'a::fs) ∈ S"
  and "y ∈ supp m"
  shows "y ∈ supp S"
  using assms supp_of_finite_sets
  by auto

lemmas fresh_star_Cons = fresh_star_list(2)

lemma mem_permute_set: 
  shows "x ∈ p ∙ S ⟷ (- p ∙ x) ∈ S"
  by (metis mem_permute_iff permute_minus_cancel(2))

lemma flip_set_both_not_in:
  assumes "x ∉ S" and "x' ∉ S"
  shows "((x' ↔ x) ∙ S) = S"
  unfolding permute_set_def
  by (auto) (metis assms flip_at_base_simps(3))+

lemma inj_atom: "inj atom" by (metis atom_eq_iff injI)

lemmas image_Int[OF inj_atom, simp]

lemma eqvt_uncurry: "eqvt f ⟹ eqvt (case_prod f)"
  unfolding eqvt_def
  by perm_simp simp

lemma supp_fun_app_eqvt2:
  assumes a: "eqvt f"
  shows "supp (f x y) ⊆ supp x ∪ supp y"
proof-
  from supp_fun_app_eqvt[OF eqvt_uncurry [OF a]]
  have "supp (case_prod f (x,y)) ⊆ supp (x,y)".
  thus ?thesis by (simp add: supp_Pair)
qed

lemma supp_fun_app_eqvt3:
  assumes a: "eqvt f"
  shows "supp (f x y z) ⊆ supp x ∪ supp y ∪ supp z"
proof-
  from supp_fun_app_eqvt2[OF eqvt_uncurry [OF a]]
  have "supp (case_prod f (x,y) z) ⊆ supp (x,y) ∪ supp z".
  thus ?thesis by (simp add: supp_Pair)
qed

(* Fighting eta-contraction *)
lemma permute_0[simp]: "permute 0 = (λ x. x)"
  by auto
lemma permute_comp[simp]: "permute x ∘ permute y = permute (x + y)" by auto

lemma map_permute: "map (permute p) = permute p"
  apply rule
  apply (induct_tac x)
  apply auto
  done

lemma fresh_star_restrictA[intro]: "a ♯* Γ ⟹ a ♯* AList.restrict V Γ"
  by (induction Γ) (auto simp add: fresh_star_Cons)

 

(* Unused. Still submit? *)
lemma Abs_lst_Nil_eq[simp]: "[[]]lst. (x::'a::fs) = [xs]lst. x' ⟷ (([],x) = (xs, x'))"
  apply rule
  apply (frule Abs_lst_fcb2[where f = "λ x y _ . (x,y)" and as = "[]" and bs = "xs" and c = "()"])
  apply (auto simp add: fresh_star_def)
  done

(* Unused. Still submit? *)
lemma Abs_lst_Nil_eq2[simp]: "[xs]lst. (x::'a::fs) = [[]]lst. x' ⟷ ((xs,x) = ([], x'))"
  by (subst eq_commute) auto



end