Theory Nominal-Utils

(*<*)
theory "Nominal-Utils"
imports Nominal2.Nominal2 "HOL-Library.AList"
begin
(*>*)

chapter ‹Prelude›
text ‹Some useful Nominal lemmas. Many of these are from Launchbury.Nominal-Utils.›

section ‹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 (opaque_lifting, 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 (opaque_lifting, 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 (opaque_lifting, 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

section ‹ 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 (- , auto simp add: eqvt_def)
    by (rule ext, auto, 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 (- , auto simp add: eqvt_def)
    by(rule ext, auto, 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)

section ‹ 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)

section ‹ 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)"
 by (induct n,simp, rule ext, simp, perm_simp,simp)

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)"
  by (induct l, simp add: permute_fun_def,simp,perm_simp,auto)

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)"
  by simp

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

section ‹ 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)

section ‹ 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])

section ‹ 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

section ‹ 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)

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

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

lemma prod_cases8 [cases type]:
  obtains (fields) a b c d e f g h where "y = (a, b, c, d, e, f, g,h)"
  by (cases y, case_tac g) blast

lemma prod_induct8 [case_names fields, induct type]:
  "(⋀a b c d e f g h. P (a, b, c, d, e, f, g, h)) ⟹ P x"
  by (cases x) blast

lemma prod_cases9 [cases type]:
  obtains (fields) a b c d e f g h i where "y = (a, b, c, d, e, f, g,h,i)"
  by (cases y, case_tac h) blast

lemma prod_induct9 [case_names fields, induct type]:
  "(⋀a b c d e f g h i. P (a, b, c, d, e, f, g, h, i)) ⟹ P x"
  by (cases x) blast

named_theorems nominal_prod_simps 

named_theorems ms_fresh "Facts for helping with freshness proofs"

lemma fresh_prod2[nominal_prod_simps,ms_fresh]: "x ♯ (a,b) = (x ♯ a ∧ x ♯ b )"
  using fresh_def supp_Pair by fastforce

lemma fresh_prod3[nominal_prod_simps,ms_fresh]: "x ♯ (a,b,c) = (x ♯ a ∧ x ♯ b  ∧ x ♯ c)"
  using fresh_def supp_Pair by fastforce

lemma fresh_prod4[nominal_prod_simps,ms_fresh]: "x ♯ (a,b,c,d) = (x ♯ a ∧ x ♯ b  ∧ x ♯ c  ∧ x ♯ d)"
  using fresh_def supp_Pair by fastforce

lemma fresh_prod5[nominal_prod_simps,ms_fresh]: "x ♯ (a,b,c,d,e) = (x ♯ a ∧ x ♯ b  ∧ x ♯ c  ∧ x ♯ d ∧ x ♯ e)"
  using fresh_def supp_Pair by fastforce

lemma fresh_prod6[nominal_prod_simps,ms_fresh]: "x ♯ (a,b,c,d,e,f) = (x ♯ a ∧ x ♯ b  ∧ x ♯ c  ∧ x ♯ d ∧ x ♯ e ∧ x ♯ f)"
  using fresh_def supp_Pair by fastforce

lemma fresh_prod7[nominal_prod_simps,ms_fresh]: "x ♯ (a,b,c,d,e,f,g) = (x ♯ a ∧ x ♯ b  ∧ x ♯ c  ∧ x ♯ d ∧ x ♯ e ∧ x ♯ f ∧ x ♯ g)"
  using fresh_def supp_Pair by fastforce

lemma fresh_prod8[nominal_prod_simps,ms_fresh]: "x ♯ (a,b,c,d,e,f,g,h) = (x ♯ a ∧ x ♯ b  ∧ x ♯ c  ∧ x ♯ d ∧ x ♯ e ∧ x ♯ f ∧ x ♯ g ∧ x ♯ h )"
  using fresh_def supp_Pair by fastforce

lemma fresh_prod9[nominal_prod_simps,ms_fresh]: "x ♯ (a,b,c,d,e,f,g,h,i) = (x ♯ a ∧ x ♯ b  ∧ x ♯ c  ∧ x ♯ d ∧ x ♯ e ∧ x ♯ f ∧ x ♯ g ∧ x ♯ h ∧ x ♯ i)"
  using fresh_def supp_Pair by fastforce

lemma fresh_prod10[nominal_prod_simps,ms_fresh]: "x ♯ (a,b,c,d,e,f,g,h,i,j) = (x ♯ a ∧ x ♯ b  ∧ x ♯ c  ∧ x ♯ d ∧ x ♯ e ∧ x ♯ f ∧ x ♯ g ∧ x ♯ h ∧ x ♯ i ∧ x ♯ j)"
  using fresh_def supp_Pair by fastforce

lemma fresh_prod12[nominal_prod_simps,ms_fresh]: "x ♯ (a,b,c,d,e,f,g,h,i,j,k,l) = (x ♯ a ∧ x ♯ b  ∧ x ♯ c  ∧ x ♯ d ∧ x ♯ e ∧ x ♯ f ∧ x ♯ g ∧ x ♯ h ∧ x ♯ i ∧ x ♯ j ∧ x ♯ k ∧ x ♯ l)"
  using fresh_def supp_Pair by fastforce

lemmas fresh_prodN = fresh_Pair fresh_prod3  fresh_prod4  fresh_prod5 fresh_prod6 fresh_prod7 fresh_prod8 fresh_prod9 fresh_prod10 fresh_prod12

lemma fresh_prod2I:
  fixes x and x1 and x2
  assumes "x ♯ x1" and "x ♯ x2" 
  shows "x ♯ (x1,x2)" using fresh_prod2 assms by auto

lemma fresh_prod3I:
  fixes x and x1 and x2 and x3 
  assumes "x ♯ x1" and "x ♯ x2" and "x ♯ x3" 
  shows "x ♯ (x1,x2,x3)" using fresh_prod3 assms by auto

lemma fresh_prod4I:
  fixes x and x1 and x2 and x3 and x4
  assumes "x ♯ x1" and "x ♯ x2" and "x ♯ x3" and "x ♯ x4" 
  shows "x ♯ (x1,x2,x3,x4)" using fresh_prod4 assms by auto

lemma fresh_prod5I:
  fixes x and x1 and x2 and x3 and x4 and x5
  assumes "x ♯ x1" and "x ♯ x2" and "x ♯ x3" and "x ♯ x4" and "x ♯ x5"
  shows "x ♯ (x1,x2,x3,x4,x5)" using fresh_prod5 assms by auto

lemma flip_collapse[simp]:
  fixes b1::"'a::pt" and bv1::"'b::at" and bv2::"'b::at"
  assumes "atom bv2 ♯ b1" and "atom c ♯ (bv1,bv2,b1)" and "bv1 ≠ bv2" 
  shows "(bv2 ↔ c) ∙ (bv1 ↔ bv2) ∙ b1 = (bv1 ↔ c) ∙ b1"
proof - 
  have "c  ≠ bv1" and "bv2 ≠ bv1" using assms by auto+
  hence "(bv2 ↔ c) + (bv1 ↔ bv2) + (bv2 ↔ c) =  (bv1 ↔ c)" using flip_triple[of c bv1 bv2] flip_commute by metis
  hence "(bv2 ↔ c)  ∙ (bv1 ↔ bv2)  ∙ (bv2 ↔ c) ∙ b1 =  (bv1 ↔ c) ∙ b1" using permute_plus by metis
  thus ?thesis using assms flip_fresh_fresh by force
qed

lemma triple_eqvt[simp]:
  "p ∙ (x, b,c) = (p ∙ x,  p ∙ b , p ∙ c)"
proof - 
  have "(x,b,c) = (x,(b,c))" by simp
  thus ?thesis using Pair_eqvt by simp
qed

lemma lst_fst:
  fixes x::"'a::at" and t1::"'b::fs" and  x'::"'a::at" and t2::"'c::fs" 
  assumes " ([[atom x]]lst. (t1,t2) = [[atom x']]lst. (t1',t2'))"
  shows " ([[atom x]]lst. t1 = [[atom x']]lst. t1')"
proof - 
  have "(∀c. atom c ♯ (t2,t2') ⟶ atom c ♯ (x, x', t1, t1') ⟶ (x ↔ c) ∙ t1 = (x' ↔ c) ∙ t1')" 
  proof(rule,rule,rule)
    fix c::'a
    assume "atom c ♯  (t2,t2')" and "atom c ♯ (x, x', t1, t1')" 
    hence "atom c ♯ (x, x', (t1,t2), (t1',t2'))"  using fresh_prod2 by simp
    thus  " (x ↔ c) ∙ t1 = (x' ↔ c) ∙ t1'" using assms Abs1_eq_iff_all(3) Pair_eqvt by simp
  qed
  thus ?thesis using Abs1_eq_iff_all(3)[of x t1 x' t1' "(t2,t2')"] by simp
qed

lemma lst_snd:
  fixes x::"'a::at" and t1::"'b::fs" and  x'::"'a::at" and t2::"'c::fs" 
  assumes " ([[atom x]]lst. (t1,t2) = [[atom x']]lst. (t1',t2'))"
  shows " ([[atom x]]lst. t2 = [[atom x']]lst. t2')"
proof - 
  have "(∀c. atom c ♯ (t1,t1') ⟶ atom c ♯ (x, x', t2, t2') ⟶ (x ↔ c) ∙ t2 = (x' ↔ c) ∙ t2')" 
  proof(rule,rule,rule)
    fix c::'a
    assume "atom c ♯  (t1,t1')" and "atom c ♯ (x, x', t2, t2')" 
    hence "atom c ♯ (x, x', (t1,t2), (t1',t2'))"  using fresh_prod2 by simp
    thus  " (x ↔ c) ∙ t2 = (x' ↔ c) ∙ t2'" using assms Abs1_eq_iff_all(3) Pair_eqvt by simp
  qed
  thus ?thesis using Abs1_eq_iff_all(3)[of x t2 x' t2' "(t1,t1')"] by simp
qed

lemma lst_head_cons_pair:
  fixes y1::"'a ::at" and y2::"'a::at" and x1::"'b::fs" and x2::"'b::fs" and xs1::"('b::fs) list" and xs2::"('b::fs) list"
  assumes "[[atom y1]]lst. (x1 # xs1) = [[atom y2]]lst. (x2 # xs2)"
  shows "[[atom y1]]lst. (x1,xs1) = [[atom y2]]lst. (x2,xs2)"
proof(subst  Abs1_eq_iff_all(3)[of y1 "(x1,xs1)"  y2 "(x2,xs2)"],rule,rule,rule)
  fix c::'a
  assume "atom c ♯ (x1#xs1,x2#xs2)" and "atom c ♯ (y1, y2, (x1, xs1), x2, xs2)" 
  thus  "(y1 ↔ c) ∙ (x1, xs1) = (y2 ↔ c) ∙ (x2, xs2)"  using assms Abs1_eq_iff_all(3) by auto
qed

lemma lst_head_cons_neq_nil:
  fixes y1::"'a ::at" and y2::"'a::at" and x1::"'b::fs" and x2::"'b::fs" and xs1::"('b::fs) list" and xs2::"('b::fs) list"
  assumes "[[atom y1]]lst. (x1 # xs1) = [[atom y2]]lst. (xs2)"
  shows "xs2 ≠ []"
proof
  assume as:"xs2 = []"
  thus  False using Abs1_eq_iff(3)[of y1 "x1#xs1" y2 Nil]  assms as by auto
qed

lemma lst_head_cons:
  fixes y1::"'a ::at" and y2::"'a::at" and x1::"'b::fs" and x2::"'b::fs" and xs1::"('b::fs) list" and xs2::"('b::fs) list"
  assumes "[[atom y1]]lst. (x1 # xs1) = [[atom y2]]lst. (x2 # xs2)"
  shows "[[atom y1]]lst. x1  = [[atom y2]]lst. x2" and "[[atom y1]]lst. xs1  = [[atom y2]]lst. xs2"
  using lst_head_cons_pair lst_fst lst_snd assms by metis+

lemma lst_pure:
  fixes x1::"'a ::at" and t1::"'b::pure" and  x2::"'a ::at" and t2::"'b::pure" 
  assumes "[[atom x1]]lst. t1 = [[atom x2]]lst. t2"
  shows "t1=t2"
  using assms Abs1_eq_iff_all(3) pure_fresh flip_fresh_fresh 
  by (metis Abs1_eq(3) permute_pure)

lemma lst_supp:
 assumes "[[atom x1]]lst. t1 = [[atom x2]]lst. t2"
 shows "supp t1 - {atom x1} = supp t2 - {atom x2}"
proof -
 have "supp ([[atom x1]]lst.t1) = supp ([[atom x2]]lst.t2)" using assms by auto
 thus ?thesis using Abs_finite_supp  
   by (metis assms empty_set list.simps(15) supp_lst.simps)
qed

lemma lst_supp_subset:
   assumes "[[atom x1]]lst. t1 = [[atom x2]]lst. t2" and "supp t1 ⊆ {atom x1} ∪ B"
   shows "supp t2 ⊆ {atom x2} ∪ B"
  using assms lst_supp by fast

lemma projl_inl_eqvt:
  fixes π :: perm
  shows   "π ∙ (projl (Inl x)) = projl (Inl (π ∙ x))"
unfolding projl_def Inl_eqvt by simp

end