# 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 (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

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"

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)

"π ∙ (m1 ++ m2) = (π ∙ m1) ++ (π ∙ m2)"
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)"
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
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

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

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

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

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 = "()"])
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

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

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

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


# Theory Syntax

(*<*)
theory Syntax
imports "Nominal2.Nominal2" "Nominal-Utils"
begin
(*>*)

chapter ‹Syntax›

text ‹Syntax of MiniSail programs and the contexts we use in judgements.›

section ‹Program Syntax›

subsection ‹AST Datatypes›

type_synonym num_nat = nat

atom_decl x  (* Immutable variables*)
atom_decl u  (* Mutable variables *)
atom_decl bv  (* Basic-type variables *)

type_synonym f = string  (* Function name *)
type_synonym dc = string (* Data constructor *)
type_synonym tyid = string

text ‹Basic types. Types without refinement constraints›
nominal_datatype "b" =
B_int | B_bool | B_id tyid
| B_pair b b  ("[ _ , _ ]⇧b")
| B_unit | B_bitvec | B_var bv
| B_app tyid b

nominal_datatype bit = BitOne | BitZero

text  ‹ Literals ›
nominal_datatype "l" =
L_num "int" | L_true | L_false | L_unit  | L_bitvec "bit list"

text  ‹ Values. We include a type identifier, tyid, in the literal for constructors
to make typing and well-formedness checking easier ›

nominal_datatype "v" =
V_lit "l"        ( "[ _ ]⇧v")
| V_var "x"        ( "[ _ ]⇧v")
| V_pair "v" "v"   ( "[ _ , _ ]⇧v")
| V_cons tyid dc "v"
| V_consp tyid dc b "v"

text ‹ Binary Operations ›
nominal_datatype "opp" = Plus ( "plus") | LEq ("leq") | Eq ("eq")

text ‹ Expressions ›
nominal_datatype "e" =
AE_val "v"           ( "[ _ ]⇧e"       )
| AE_app "f" "v"       ( "[ _ ( _ ) ]⇧e" )
| AE_appP  "f" "b" "v" ( "[_ [ _ ] ( _ )]⇧e" )
| AE_op "opp" "v" "v"  ( "[ _ _ _ ]⇧e"  )
| AE_concat v v        ( "[ _ @@ _ ]⇧e" )
| AE_fst "v"           ( "[#1_ ]⇧e"    )
| AE_snd "v"           ( "[#2_ ]⇧e"     )
| AE_mvar "u"          ( "[ _ ]⇧e"      )
| AE_len "v"           ( "[| _ |]⇧e"    )
| AE_split "v" "v"     ( "[ _ / _ ]⇧e"  )

text ‹ Expressions for constraints›
nominal_datatype "ce" =
CE_val "v"           ( "[ _ ]⇧c⇧e"      )
| CE_op "opp" "ce" "ce"  ( "[ _ _ _ ]⇧c⇧e"  )
| CE_concat ce ce        ( "[ _ @@ _ ]⇧c⇧e" )
| CE_fst "ce"           ( "[#1_]⇧c⇧e"      )
| CE_snd "ce"           ( "[#2_]⇧c⇧e"      )
| CE_len "ce"           ( "[| _ |]⇧c⇧e"    )

text  ‹ Constraints ›
nominal_datatype "c" =
C_true          ( "TRUE" [] 50 )
| C_false         ( "FALSE" [] 50 )
| C_conj "c" "c"  ("_  AND  _ " [50, 50] 50)
| C_disj "c" "c"  ("_ OR _ " [50,50] 50)
| C_not "c"       ( "¬ _ " [] 50 )
| C_imp "c" "c"   ("_  IMP  _ " [50, 50] 50)
| C_eq "ce" "ce"  ("_  ==  _ " [50, 50] 50)

text  ‹ Refined types ›
nominal_datatype "τ" =
T_refined_type  x::x b c::c   binds x in c   ("⦃ _ : _  | _ ⦄" [50, 50] 1000)

text ‹ Statements ›

nominal_datatype
s =
AS_val v                             ( "[_]⇧s")
| AS_let x::x  e s::s binds x in s     ( "(LET _ = _ IN _)")
| AS_let2 x::x τ  s s::s binds x in s  ( "(LET _ : _ = _ IN _)")
| AS_if v s s                          ( "(IF _ THEN _ ELSE _)" [0, 61, 0] 61)
| AS_var u::u τ v s::s  binds u in s   ( "(VAR _ : _ = _ IN _)")
| AS_assign u  v                       ( "(_ ::= _)")
| AS_match v branch_list               ( "(MATCH _ WITH { _ })")
| AS_while s s                         ( "(WHILE _ DO { _ } )" [0, 0] 61)
| AS_seq s s                           ( "( _ ;; _ )"  [1000, 61] 61)
| AS_assert c s                        ( "(ASSERT _ IN _ )" )
and branch_s =
AS_branch dc x::x s::s binds x in s  ( "( _ _ ⇒ _ )")
and branch_list =
AS_final  branch_s                   ( "{ _ }" )
| AS_cons  branch_s branch_list        ( "( _ | _  )")

text ‹ Function and union type definitions ›

nominal_datatype "fun_typ"  =
AF_fun_typ x::x "b" c::c τ::τ s::s binds x in c τ s

nominal_datatype "fun_typ_q" =
AF_fun_typ_some bv::bv ft::fun_typ binds bv in ft
| AF_fun_typ_none fun_typ

nominal_datatype "fun_def" =  AF_fundef f fun_typ_q

nominal_datatype "type_def" =
AF_typedef string "(string * τ) list"
|  AF_typedef_poly string bv::bv dclist::"(string * τ) list"  binds bv in dclist

lemma check_typedef_poly:
"AF_typedef_poly ''option'' bv [ (''None'', ⦃ zz : B_unit | TRUE ⦄), (''Some'', ⦃ zz : B_var bv | TRUE ⦄) ] =
AF_typedef_poly ''option'' bv2 [ (''None'', ⦃ zz : B_unit | TRUE ⦄), (''Some'', ⦃ zz : B_var bv2 | TRUE ⦄) ]"
by auto

nominal_datatype "var_def" =  AV_def u τ v

text  ‹ Programs ›
nominal_datatype "p" =
AP_prog "type_def list" "fun_def list" "var_def list" "s" ("PROG _ _ _ _")

declare l.supp [simp] v.supp [simp]  e.supp [simp] s_branch_s_branch_list.supp [simp]  τ.supp [simp] c.supp [simp] b.supp[simp]

subsection ‹Lemmas›

text ‹These lemmas deal primarily with freshness and alpha-equivalence›

subsubsection ‹Atoms›

lemma x_not_in_u_atoms[simp]:
fixes u::u and x::x and us::"u set"
shows "atom x ∉ atomus"

lemma x_fresh_u[simp]:
fixes u::u and x::x
shows "atom x ♯ u"
by auto

lemma x_not_in_b_set[simp]:
fixes  x::x and bs::"bv fset"
shows "atom x ∉ supp bs"
by(induct bs,auto, simp add: supp_finsert supp_at_base)

lemma x_fresh_b[simp]:
fixes  x::x and b::b
shows "atom x ♯ b"
apply (induct b rule: b.induct, auto simp: pure_supp)
using pure_supp fresh_def by blast+

lemma x_fresh_bv[simp]:
fixes  x::x and bv::bv
shows "atom x ♯ bv"
using fresh_def supp_at_base by auto

lemma u_not_in_x_atoms[simp]:
fixes u::u and x::x and xs::"x set"
shows "atom u ∉ atomxs"

lemma bv_not_in_x_atoms[simp]:
fixes bv::bv and x::x and xs::"x set"
shows "atom bv ∉ atomxs"

lemma u_not_in_b_atoms[simp]:
fixes b :: b and u::u
shows "atom u ∉ supp b"
by (induct b rule: b.induct,auto simp: pure_supp supp_at_base)

lemma u_not_in_b_set[simp]:
fixes  u::u and bs::"bv fset"
shows "atom u ∉ supp bs"
by(induct bs, auto simp add: supp_at_base supp_finsert)

lemma u_fresh_b[simp]:
fixes  x::u and b::b
shows "atom x ♯ b"
by(induct b rule: b.induct, auto simp: pure_fresh )

lemma supp_b_v_disjoint:
fixes x::x and bv::bv
shows "supp (V_var x) ∩ supp (B_var bv) = {}"

lemma supp_b_u_disjoint[simp]:
fixes b::b and u::u
shows "supp u ∩ supp b = {}"
by(nominal_induct b rule:b.strong_induct,(auto simp add: pure_supp b.supp supp_at_base)+)

lemma u_fresh_bv[simp]:
fixes  u::u and b::bv
shows "atom u ♯ b"
using fresh_at_base by simp

subsubsection ‹Basic Types›

nominal_function b_of :: "τ ⇒ b" where
"b_of ⦃ z : b | c ⦄ = b"
by (meson τ.exhaust)
nominal_termination (eqvt)  by lexicographic_order

lemma supp_b_empty[simp]:
fixes b :: b and x::x
shows "atom x ∉ supp b"
by (induct b rule: b.induct, auto simp: pure_supp supp_at_base x_not_in_b_set)

lemma flip_b_id[simp]:
fixes x::x and b::b
shows "(x ↔ x') ∙ b = b"
by(rule flip_fresh_fresh, auto simp add: fresh_def)

lemma flip_x_b_cancel[simp]:
fixes x::x and y::x  and b::b and bv::bv
shows "(x ↔ y) ∙ b = b" and "(x ↔ y) ∙ bv = bv"
using flip_b_id  apply simp
by (metis b.eq_iff(7) b.perm_simps(7) flip_b_id)

lemma flip_bv_x_cancel[simp]:
fixes bv::bv and z::bv and x::x
shows "(bv ↔ z) ∙ x = x" using flip_fresh_fresh[of bv x z] fresh_at_base by auto

lemma flip_bv_u_cancel[simp]:
fixes bv::bv and z::bv and x::u
shows "(bv ↔ z) ∙ x = x" using flip_fresh_fresh[of bv x z] fresh_at_base by auto

subsubsection ‹Literals›

lemma supp_bitvec_empty:
fixes bv::"bit list"
shows "supp bv = {}"
proof(induct bv)
case Nil
then show ?case using supp_Nil by auto
next
case (Cons a bv)
then show ?case using supp_Cons  bit.supp
by (metis (mono_tags, hide_lams) bit.strong_exhaust l.supp(5) sup_bot.right_neutral)
qed

lemma bitvec_pure[simp]:
fixes bv::"bit list" and x::x
shows "atom x ♯ bv" using fresh_def supp_bitvec_empty by auto

lemma supp_l_empty[simp]:
fixes l:: l
shows "supp (V_lit l) = {}"
by(nominal_induct l rule: l.strong_induct,
auto simp add: l.strong_exhaust pure_supp v.fv_defs supp_bitvec_empty)

lemma type_l_nosupp[simp]:
fixes x::x and l::l
shows "atom x ∉ supp (⦃ z : b  |  [[z]⇧v]⇧c⇧e ==  [[l]⇧v]⇧c⇧e ⦄)"
using supp_at_base supp_l_empty ce.supp(1) c.supp τ.supp by force

lemma flip_bitvec0:
fixes x::"bit list"
assumes "atom c ♯ (z, x, z')"
shows "(z ↔ c) ∙ x = (z' ↔ c) ∙ x"
proof -
have "atom z ♯ x" and "atom z' ♯ x"
using flip_fresh_fresh assms supp_bitvec_empty fresh_def by blast+
moreover have "atom c ♯ x" using  supp_bitvec_empty fresh_def by auto
ultimately show ?thesis  using assms flip_fresh_fresh by metis
qed

lemma flip_bitvec:
assumes "atom c ♯ (z, L_bitvec x, z')"
shows "(z ↔ c) ∙ x = (z' ↔ c) ∙ x"
proof -
have "atom z ♯ x" and "atom z' ♯ x"
using flip_fresh_fresh assms supp_bitvec_empty fresh_def by blast+
moreover have "atom c ♯ x" using  supp_bitvec_empty fresh_def by auto
ultimately show ?thesis  using assms flip_fresh_fresh by metis
qed

lemma type_l_eq:
shows "⦃ z : b  |  [[z]⇧v]⇧c⇧e == [V_lit l]⇧c⇧e ⦄ = (⦃ z' : b  |  [[z']⇧v]⇧c⇧e == [V_lit l]⇧c⇧e ⦄)"
by(auto,nominal_induct l rule: l.strong_induct,auto, metis permute_pure, auto simp add: flip_bitvec)

lemma flip_l_eq:
fixes x::l
shows "(z ↔ c) ∙ x = (z' ↔ c) ∙ x"
proof -
have "atom z ♯ x" and "atom c ♯ x" and "atom z' ♯ x"
using flip_fresh_fresh fresh_def supp_l_empty by fastforce+
thus ?thesis using flip_fresh_fresh by metis
qed

lemma flip_l_eq1:
fixes x::l
assumes  "(z ↔ c) ∙ x = (z' ↔ c) ∙ x'"
shows "x' = x"
proof -
have "atom z ♯ x" and "atom c ♯ x'" and "atom c ♯ x" and "atom z' ♯ x'"
using flip_fresh_fresh fresh_def supp_l_empty by fastforce+
thus ?thesis using flip_fresh_fresh assms by metis
qed

subsubsection ‹Types›

lemma flip_base_eq:
fixes b::b and x::x and y::x
shows "(x ↔ y) ∙ b = b"
using b.fresh  by (simp add: flip_fresh_fresh fresh_def)

text ‹ Obtain an alpha-equivalent type where the bound variable is fresh in some term t ›
lemma has_fresh_z0:
fixes t::"'b::fs"
shows "∃z. atom z ♯ (c',t) ∧ (⦃z' : b | c' ⦄) = (⦃ z : b | (z ↔ z' ) ∙ c' ⦄)"
proof -
obtain z::x where fr: "atom z ♯ (c',t)" using obtain_fresh by blast
moreover hence "(⦃ z' : b | c' ⦄) = (⦃ z : b | (z ↔ z') ∙ c' ⦄)"
using τ.eq_iff Abs1_eq_iff
by (metis flip_commute flip_fresh_fresh fresh_PairD(1))
ultimately show ?thesis by fastforce
qed

lemma has_fresh_z:
fixes t::"'b::fs"
shows "∃z b c. atom z ♯ t ∧ τ = ⦃ z : b | c ⦄"
proof -
obtain z' and b and c' where teq: "τ =  (⦃ z' : b | c' ⦄)" using τ.exhaust by blast
obtain z::x where fr: "atom z ♯ (t,c')" using obtain_fresh by blast
hence "(⦃ z' : b | c' ⦄) = (⦃ z : b | (z ↔ z') ∙ c' ⦄)"  using τ.eq_iff Abs1_eq_iff
flip_commute flip_fresh_fresh fresh_PairD(1)  by (metis fresh_PairD(2))
hence "atom z ♯ t ∧ τ = (⦃ z : b | (z ↔ z') ∙ c' ⦄)" using fr teq by force
thus ?thesis using teq fr by fast
qed

lemma obtain_fresh_z:
fixes t::"'b::fs"
obtains z and b and c where "atom z ♯ t ∧ τ = ⦃ z : b | c ⦄"
using has_fresh_z by blast

lemma has_fresh_z2:
fixes t::"'b::fs"
shows "∃z c. atom z ♯ t ∧ τ = ⦃ z : b_of τ | c ⦄"
proof -
obtain z and b and c where "atom z ♯ t ∧ τ = ⦃ z : b | c ⦄" using obtain_fresh_z by metis
moreover then have "b_of τ = b" using τ.eq_iff by simp
ultimately show ?thesis using obtain_fresh_z τ.eq_iff by auto
qed

lemma obtain_fresh_z2:
fixes t::"'b::fs"
obtains z and  c where "atom z ♯ t ∧ τ = ⦃ z : b_of τ | c ⦄"
using has_fresh_z2 by blast

subsubsection ‹Values›

lemma u_notin_supp_v[simp]:
fixes u::u and v::v
shows "atom u ∉ supp v"
proof(nominal_induct v rule: v.strong_induct)
case (V_lit l)
then show ?case  using supp_l_empty by auto
next
case (V_var x)
then show ?case
next
case (V_pair v1 v2)
then show ?case by auto
next
case (V_cons tyid list v)
then show ?case using pure_supp by auto
next
case (V_consp tyid list b v)
then show ?case using pure_supp by auto
qed

lemma u_fresh_xv[simp]:
fixes u::u and x::x and v::v
shows "atom u ♯  (x,v)"
proof -
have "atom u ♯ x" using fresh_def by fastforce
moreover have "atom u ♯ v" using fresh_def u_notin_supp_v by metis
ultimately show ?thesis using fresh_prod2 by auto
qed

text ‹ Part of an effort to make the proofs across inductive cases more uniform by distilling
the non-uniform parts into lemmas like this›
lemma v_flip_eq:
fixes v::v and va::v and x::x and c::x
assumes "atom c ♯ (v, va)" and "atom c ♯ (x, xa, v, va)" and "(x ↔ c) ∙ v = (xa ↔ c) ∙ va"
shows "((v = V_lit l ⟶ (∃l'. va = V_lit l' ∧  (x ↔ c) ∙ l = (xa ↔ c) ∙ l'))) ∧
((v = V_var y ⟶ (∃y'. va = V_var y' ∧  (x ↔ c) ∙ y = (xa ↔ c) ∙ y'))) ∧
((v = V_pair vone vtwo ⟶ (∃v1' v2'. va = V_pair v1' v2' ∧  (x ↔ c) ∙ vone = (xa ↔ c) ∙ v1' ∧  (x ↔ c) ∙ vtwo = (xa ↔ c) ∙ v2'))) ∧
((v = V_cons tyid dc vone ⟶ (∃v1'. va = V_cons tyid dc v1'∧  (x ↔ c) ∙ vone = (xa ↔ c) ∙ v1'))) ∧
((v = V_consp tyid dc b vone ⟶ (∃v1'. va = V_consp tyid dc b v1'∧  (x ↔ c) ∙ vone = (xa ↔ c) ∙ v1')))"
using assms proof(nominal_induct v rule:v.strong_induct)
case (V_lit l)
then show ?case  using assms v.perm_simps
empty_iff flip_def fresh_def fresh_permute_iff supp_l_empty swap_fresh_fresh v.fresh
by (metis permute_swap_cancel2 v.distinct)
next
case (V_var x)
then show ?case  using assms v.perm_simps
empty_iff flip_def fresh_def fresh_permute_iff supp_l_empty swap_fresh_fresh v.fresh
by (metis permute_swap_cancel2 v.distinct)
next
case (V_pair v1 v2)
have " (V_pair v1 v2 = V_pair vone vtwo ⟶ (∃v1' v2'. va = V_pair v1' v2' ∧ (x ↔ c) ∙ vone = (xa ↔ c) ∙ v1' ∧ (x ↔ c) ∙ vtwo = (xa ↔ c) ∙ v2'))" proof
assume "V_pair v1 v2= V_pair vone vtwo"
thus  "(∃v1' v2'. va = V_pair v1' v2' ∧ (x ↔ c) ∙ vone = (xa ↔ c) ∙ v1' ∧ (x ↔ c) ∙ vtwo = (xa ↔ c) ∙ v2')"
using V_pair assms
by (metis (no_types, hide_lams) flip_def permute_swap_cancel v.perm_simps(3))
qed
thus ?case using V_pair by auto
next
case (V_cons tyid dc v1)
have " (V_cons tyid dc v1 = V_cons tyid dc vone ⟶ (∃ v1'. va = V_cons tyid dc  v1' ∧ (x ↔ c) ∙ vone = (xa ↔ c) ∙ v1'))" proof
assume as: "V_cons tyid dc v1 = V_cons tyid dc  vone"
hence "(x ↔ c) ∙  (V_cons tyid dc  vone) =  V_cons tyid dc ((x ↔ c) ∙ vone)" proof -
have "(x ↔ c)  ∙ dc = dc" using pure_permute_id  by metis
moreover have "(x ↔ c)  ∙ tyid = tyid" using pure_permute_id  by metis
ultimately show ?thesis using v.perm_simps(4) by simp
qed
then obtain v1' where "(xa ↔ c) ∙ va = V_cons tyid dc v1' ∧ (x ↔ c) ∙ vone = v1'" using assms V_cons
using as by fastforce
hence " va = V_cons tyid dc ((xa ↔ c) ∙ v1') ∧ (x ↔ c) ∙ vone = v1'" using permute_flip_cancel empty_iff flip_def fresh_def supp_b_empty swap_fresh_fresh
by (metis pure_fresh v.perm_simps(4))

thus  "(∃v1'. va = V_cons tyid dc  v1' ∧ (x ↔ c) ∙ vone = (xa ↔ c) ∙ v1')"
using V_cons assms by simp
qed
thus ?case using V_cons by auto
next
case (V_consp tyid dc b v1)
have " (V_consp tyid dc b v1 = V_consp tyid dc b vone ⟶ (∃ v1'. va = V_consp tyid dc  b v1' ∧ (x ↔ c) ∙ vone = (xa ↔ c) ∙ v1'))" proof
assume as: "V_consp tyid dc b v1 = V_consp tyid dc b vone"
hence "(x ↔ c) ∙  (V_consp tyid dc  b vone) =  V_consp tyid dc b ((x ↔ c) ∙ vone)" proof -
have "(x ↔ c)  ∙ dc = dc" using pure_permute_id  by metis
moreover have "(x ↔ c)  ∙ tyid = tyid" using pure_permute_id  by metis
ultimately show ?thesis using v.perm_simps(4) by simp
qed
then obtain v1' where "(xa ↔ c) ∙ va = V_consp tyid dc b v1' ∧ (x ↔ c) ∙ vone = v1'" using assms V_consp
using as by fastforce
hence " va = V_consp tyid dc b ((xa ↔ c) ∙ v1') ∧ (x ↔ c) ∙ vone = v1'" using permute_flip_cancel empty_iff flip_def fresh_def supp_b_empty swap_fresh_fresh
pure_fresh v.perm_simps
by (metis (mono_tags, hide_lams))
thus   "(∃v1'. va = V_consp tyid dc  b v1' ∧ (x ↔ c) ∙ vone = (xa ↔ c) ∙ v1')"
using V_consp assms by simp
qed
thus ?case using V_consp by auto
qed

lemma flip_eq:
fixes x::x and xa::x and s::"'a::fs" and sa::"'a::fs"
assumes "(∀c. atom c ♯ (s, sa) ⟶ atom c ♯ (x, xa, s, sa) ⟶ (x ↔ c) ∙ s = (xa ↔ c) ∙ sa)" and "x ≠ xa"
shows "(x ↔ xa) ∙ s = sa"
proof -
have  " ([[atom x]]lst. s = [[atom xa]]lst. sa)" using assms Abs1_eq_iff_all by simp
hence  "(xa = x ∧ sa = s ∨ xa ≠ x ∧ sa = (xa ↔ x) ∙ s ∧ atom xa ♯ s)" using assms Abs1_eq_iff[of xa sa x s] by simp
thus ?thesis using assms
by (metis flip_commute)
qed

lemma  swap_v_supp:
fixes v::v and d::x and z::x
assumes "atom d ♯ v"
shows "supp ((z ↔ d ) ∙ v) ⊆ supp v - { atom z } ∪ { atom d}"
using assms
proof(nominal_induct v rule:v.strong_induct)
case (V_lit l)
then show ?case using l.supp by (metis supp_l_empty empty_subsetI l.strong_exhaust pure_supp supp_eqvt v.supp)
next
case (V_var x)
hence "d ≠ x" using fresh_def by fastforce
thus ?case apply(cases "z = x")  using   supp_at_base V_var ‹d≠x› by fastforce+
next
case (V_cons tyid dc v)
show ?case using v.supp(4) pure_supp
using V_cons.hyps V_cons.prems fresh_def by auto
next
case (V_consp tyid dc b v)
show ?case using v.supp(4) pure_supp
using V_consp.hyps V_consp.prems fresh_def by auto
qed(force+)

subsubsection ‹Expressions›

lemma  swap_e_supp:
fixes e::e and d::x and z::x
assumes "atom d ♯ e"
shows "supp ((z ↔ d ) ∙ e) ⊆ supp e - { atom z } ∪ { atom d}"
using assms
proof(nominal_induct e rule:e.strong_induct)
case (AE_val v)
then show ?case using swap_v_supp by simp
next
case (AE_app f v)
then show ?case using swap_v_supp  by (simp add: pure_supp)
next
case (AE_appP b f v)
hence df: "atom d ♯ v" using fresh_def e.supp by force
have  "supp ((z ↔ d ) ∙ (AE_appP b f v)) =  supp (AE_appP b f ((z ↔ d ) ∙ v))" using  e.supp
by (metis b.eq_iff(3) b.perm_simps(3) e.perm_simps(3) flip_b_id)
also have "... = supp b ∪ supp f ∪ supp ((z ↔ d ) ∙ v)" using e.supp by auto
also have "... ⊆  supp b ∪ supp f ∪ supp v  - { atom z } ∪ { atom d}" using swap_v_supp[OF df] pure_supp  by auto
finally show ?case using e.supp by auto
next
case (AE_op opp v1 v2)
hence df: "atom d ♯ v1 ∧ atom d ♯ v2" using fresh_def e.supp by force
have "((z ↔ d ) ∙ (AE_op opp v1 v2)) = AE_op opp ((z ↔ d ) ∙ v1) ((z ↔ d ) ∙ v2)" using
e.perm_simps flip_commute opp.perm_simps AE_op opp.strong_exhaust  pure_supp
by (metis (full_types))

hence "supp ((z ↔ d) ∙ AE_op opp v1 v2) = supp (AE_op opp ((z ↔ d) ∙v1)  ((z ↔ d) ∙v2))" by simp
also have "... = supp  ((z ↔ d) ∙v1) ∪ supp  ((z ↔ d) ∙v2)" using e.supp
by (metis (mono_tags, hide_lams) opp.strong_exhaust opp.supp sup_bot.left_neutral)
also have "... ⊆ (supp v1 -  { atom z } ∪ { atom d}) ∪  (supp v2 - { atom z } ∪ { atom d})" using swap_v_supp AE_op df by blast
finally show ?case using e.supp opp.supp by blast
next
case (AE_fst v)
then show ?case   using swap_v_supp by auto
next
case (AE_snd v)
then show ?case   using swap_v_supp by auto
next
case (AE_mvar u)
then show ?case using
Diff_empty Diff_insert0 Un_upper1 atom_x_sort flip_def flip_fresh_fresh fresh_def set_eq_subset supp_eqvt swap_set_in_eq
by (metis sort_of_atom_eq)
next
case (AE_len v)
then show ?case   using swap_v_supp by auto
next
case (AE_concat v1 v2)
then show ?case   using swap_v_supp by auto
next
case (AE_split v1 v2)
then show ?case   using swap_v_supp by auto
qed

lemma  swap_ce_supp:
fixes e::ce and d::x and z::x
assumes "atom d ♯ e"
shows "supp ((z ↔ d ) ∙ e) ⊆ supp e - { atom z } ∪ { atom d}"
using assms
proof(nominal_induct e rule:ce.strong_induct)
case (CE_val v)
then show ?case using swap_v_supp ce.fresh ce.supp by simp
next
case (CE_op opp v1 v2)
hence df: "atom d ♯ v1 ∧ atom d ♯ v2" using fresh_def e.supp by force
have "((z ↔ d ) ∙ (CE_op opp v1 v2)) = CE_op opp ((z ↔ d ) ∙ v1) ((z ↔ d ) ∙ v2)" using
ce.perm_simps flip_commute opp.perm_simps CE_op opp.strong_exhaust x_fresh_b pure_supp
by (metis (full_types))

hence "supp ((z ↔ d) ∙ CE_op opp v1 v2) = supp (CE_op opp ((z ↔ d) ∙v1)  ((z ↔ d) ∙v2))" by simp
also have "... = supp  ((z ↔ d) ∙v1) ∪ supp  ((z ↔ d) ∙v2)" using ce.supp
by (metis (mono_tags, hide_lams) opp.strong_exhaust opp.supp sup_bot.left_neutral)
also have "... ⊆ (supp v1 -  { atom z } ∪ { atom d}) ∪  (supp v2 - { atom z } ∪ { atom d})" using swap_v_supp CE_op df by blast
finally show ?case using ce.supp opp.supp by blast
next
case (CE_fst v)
then show ?case   using ce.supp ce.fresh swap_v_supp by auto
next
case (CE_snd v)
then show ?case   using ce.supp ce.fresh swap_v_supp by auto
next
case (CE_len v)
then show ?case   using ce.supp ce.fresh swap_v_supp by auto
next
case (CE_concat v1 v2)
then show ?case using ce.supp ce.fresh swap_v_supp ce.perm_simps
proof -
have "∀x v xa. ¬ atom (x::x) ♯ (v::v) ∨ supp ((xa ↔ x) ∙ v) ⊆ supp v - {atom xa} ∪ {atom x}"
by (meson swap_v_supp) (* 0.0 ms *)
then show ?thesis
using CE_concat ce.supp by auto
qed
qed

lemma  swap_c_supp:
fixes c::c and d::x and z::x
assumes "atom d ♯ c"
shows "supp ((z ↔ d ) ∙ c) ⊆ supp c - { atom z } ∪ { atom d}"
using assms
proof(nominal_induct c rule:c.strong_induct)
case (C_eq e1 e2)
then show ?case using swap_ce_supp by auto
qed(auto+)

lemma type_e_eq:
assumes "atom z ♯ e" and "atom z' ♯ e"
shows "⦃ z : b  |  [[z]⇧v]⇧c⇧e == e ⦄ = (⦃ z' : b  |  [[z']⇧v]⇧c⇧e ==  e ⦄)"
by (auto,metis (full_types) assms(1) assms(2) flip_fresh_fresh fresh_PairD(1) fresh_PairD(2))

lemma type_e_eq2:
assumes "atom z ♯ e" and "atom z' ♯ e" and "b=b'"
shows "⦃ z : b  |  [[z]⇧v]⇧c⇧e == e ⦄ = (⦃ z' : b'  |  [[z']⇧v]⇧c⇧e == e ⦄)"
using assms type_e_eq by fast

lemma e_flip_eq:
fixes e::e and ea::e
assumes "atom c ♯ (e, ea)" and "atom c ♯ (x, xa, e, ea)" and "(x ↔ c) ∙ e = (xa ↔ c) ∙ ea"
shows "(e = AE_val w ⟶ (∃w'. ea = AE_val w' ∧ (x ↔ c) ∙ w = (xa ↔ c) ∙ w')) ∨
(e = AE_op opp v1 v2 ⟶ (∃v1' v2'. ea = AS_op opp v1' v2' ∧ (x ↔ c) ∙ v1 = (xa ↔ c) ∙ v1') ∧ (x ↔ c) ∙ v2 = (xa ↔ c) ∙ v2') ∨
(e = AE_fst v ⟶ (∃v'. ea = AE_fst v' ∧ (x ↔ c) ∙ v = (xa ↔ c) ∙ v')) ∨
(e = AE_snd v ⟶ (∃v'. ea = AE_snd v' ∧ (x ↔ c) ∙ v = (xa ↔ c) ∙ v')) ∨
(e = AE_len v ⟶ (∃v'. ea = AE_len v' ∧ (x ↔ c) ∙ v = (xa ↔ c) ∙ v')) ∨
(e = AE_concat v1 v2 ⟶ (∃v1' v2'. ea = AS_concat v1' v2' ∧ (x ↔ c) ∙ v1 = (xa ↔ c) ∙ v1') ∧ (x ↔ c) ∙ v2 = (xa ↔ c) ∙ v2') ∨
(e = AE_app f v ⟶ (∃v'. ea = AE_app f  v' ∧ (x ↔ c) ∙ v = (xa ↔ c) ∙ v'))"
by (metis assms e.perm_simps permute_flip_cancel2)

lemma fresh_opp_all:
fixes opp::opp
shows "z ♯ opp"
using e.fresh opp.exhaust opp.fresh  by metis

lemma fresh_e_opp_all:
shows "(z ♯ v1 ∧ z ♯ v2) = z ♯ AE_op opp v1 v2"
using e.fresh opp.exhaust opp.fresh fresh_opp_all by simp

lemma fresh_e_opp:
fixes z::x
assumes "atom z ♯ v1 ∧ atom z ♯ v2"
shows "atom z ♯ AE_op opp v1 v2"
using e.fresh opp.exhaust opp.fresh opp.supp  by (metis assms)

subsubsection ‹Statements›

lemma branch_s_flip_eq:
fixes v::v and va::v
assumes "atom c ♯ (v, va)" and "atom c ♯ (x, xa, v, va)" and "(x ↔ c) ∙ s = (xa ↔ c) ∙ sa"
shows "(s = AS_val w ⟶ (∃w'. sa = AS_val w' ∧ (x ↔ c) ∙ w = (xa ↔ c) ∙ w')) ∨
(s = AS_seq s1 s2 ⟶ (∃s1' s2'. sa = AS_seq s1' s2' ∧ (x ↔ c) ∙ s1 = (xa ↔ c) ∙ s1') ∧ (x ↔ c) ∙ s2 = (xa ↔ c) ∙ s2') ∨
(s = AS_if v s1 s2 ⟶ (∃v' s1' s2'. sa = AS_if seq s1' s2' ∧ (x ↔ c) ∙ s1 = (xa ↔ c) ∙ s1') ∧ (x ↔ c) ∙ s2 = (xa ↔ c) ∙ s2' ∧ (x ↔ c) ∙ c = (xa ↔ c) ∙ v')"
by (metis assms s_branch_s_branch_list.perm_simps permute_flip_cancel2)

section ‹Context Syntax›

subsection ‹Datatypes›

text ‹Type and function/type definition contexts›
type_synonym Φ = "fun_def list"
type_synonym Θ = "type_def list"
type_synonym ℬ = "bv fset"

datatype Γ =
GNil
| GCons "x*b*c" Γ  (infixr "#⇩Γ" 65)

datatype Δ =
DNil  ("[]⇩Δ")
| DCons "u*τ" Δ  (infixr "#⇩Δ" 65)

subsection ‹Functions and Lemmas›

lemma Γ_induct [case_names GNil GCons] : "P GNil ⟹ (⋀x b c Γ'. P Γ' ⟹ P ((x,b,c) #⇩Γ Γ')) ⟹ P Γ"
proof(induct Γ rule:Γ.induct)
case GNil
then show ?case by auto
next
case (GCons x1 x2)
then obtain x and b and c where "x1=(x,b,c)"  using prod_cases3 by blast
then show ?case using GCons by presburger
qed

instantiation Δ ::  pt
begin

primrec permute_Δ
where
DNil_eqvt:  "p ∙ DNil = DNil"
| DCons_eqvt: "p ∙ (x #⇩Δ xs) = p ∙ x #⇩Δ p ∙ (xs::Δ)"

instance  by standard (induct_tac [!] x, simp_all)
end

lemmas [eqvt] =  permute_Δ.simps

lemma Δ_induct [case_names DNil DCons] : "P DNil ⟹ (⋀u t Δ'. P Δ' ⟹ P ((u,t) #⇩Δ Δ')) ⟹ P Δ"
proof(induct Δ rule: Δ.induct)
case DNil
then show ?case by auto
next
case (DCons x1 x2)
then obtain u and t  where "x1=(u,t)"  by fastforce
then show ?case using DCons by presburger
qed

lemma Φ_induct [case_names PNil PConsNone PConsSome] : "P [] ⟹ (⋀f x b c τ s' Φ'. P Φ' ⟹ P ((AF_fundef f (AF_fun_typ_none (AF_fun_typ x b c τ s'))) # Φ')) ⟹
(⋀f bv x b c τ s' Φ'. P Φ' ⟹ P ((AF_fundef f (AF_fun_typ_some bv (AF_fun_typ x b c τ s'))) # Φ'))  ⟹ P Φ"
proof(induct Φ rule: list.induct)
case Nil
then show ?case by auto
next
case (Cons x1 x2)
then obtain f and t where ft: "x1 = (AF_fundef f t)"
by (meson fun_def.exhaust)
then show ?case proof(nominal_induct t rule:fun_typ_q.strong_induct)
case (AF_fun_typ_some bv ft)
then show ?case using Cons ft
by (metis fun_typ.exhaust)
next
case (AF_fun_typ_none ft)
then show ?case using Cons ft
by (metis fun_typ.exhaust)
qed
qed

lemma Θ_induct [case_names TNil AF_typedef AF_typedef_poly] : "P [] ⟹ (⋀tid dclist Θ'. P Θ' ⟹ P ((AF_typedef tid dclist) # Θ')) ⟹
(⋀tid bv dclist Θ'. P Θ' ⟹ P ((AF_typedef_poly tid bv dclist ) # Θ'))  ⟹ P Θ"
proof(induct Θ rule: list.induct)
case Nil
then show ?case by auto
next
case (Cons td T)
show ?case by(cases td rule: type_def.exhaust, (simp add: Cons)+)
qed

instantiation Γ ::  pt
begin

primrec permute_Γ
where
GNil_eqvt:  "p ∙ GNil = GNil"
| GCons_eqvt: "p ∙ (x #⇩Γ xs) = p ∙ x #⇩Γ p ∙ (xs::Γ)"

instance by standard (induct_tac [!] x, simp_all)
end

lemmas [eqvt] =  permute_Γ.simps

lemma G_cons_eqvt[simp]:
fixes Γ::Γ
shows "p ∙ ((x,b,c) #⇩Γ Γ) = ((p ∙ x,  p ∙ b , p ∙ c) #⇩Γ (p ∙ Γ ))" (is "?A = ?B" )
using Cons_eqvt triple_eqvt  supp_b_empty by simp

lemma G_cons_flip[simp]:
fixes  x::x and Γ::Γ
shows  "(x↔x') ∙ ((x'',b,c) #⇩Γ Γ) = (((x↔x') ∙ x'',  b , (x↔x') ∙ c) #⇩Γ ((x↔x') ∙ Γ ))"
using Cons_eqvt triple_eqvt  supp_b_empty by auto

lemma G_cons_flip_fresh[simp]:
fixes  x::x and Γ::Γ
assumes  "atom x ♯ (c,Γ)" and "atom x' ♯ (c,Γ)"
shows  "(x↔x') ∙ ((x',b,c) #⇩Γ Γ) = ((x,  b , c) #⇩Γ Γ )"
using G_cons_flip flip_fresh_fresh assms by force

lemma G_cons_flip_fresh2[simp]:
fixes  x::x and Γ::Γ
assumes  "atom x ♯ (c,Γ)" and "atom x' ♯ (c,Γ)"
shows  "(x↔x') ∙ ((x,b,c) #⇩Γ Γ) = ((x',  b , c) #⇩Γ Γ )"
using G_cons_flip flip_fresh_fresh assms by force

lemma G_cons_flip_fresh3[simp]:
fixes  x::x and Γ::Γ
assumes  "atom x ♯ Γ" and "atom x' ♯ Γ"
shows  "(x↔x') ∙ ((x',b,c) #⇩Γ Γ) = ((x,  b , (x↔x') ∙ c) #⇩Γ Γ )"
using G_cons_flip flip_fresh_fresh assms by force

lemma neq_GNil_conv: "(xs ≠ GNil) = (∃y ys. xs = y #⇩Γ ys)"
by (induct xs) auto

nominal_function toList :: "Γ ⇒ (x*b*c) list" where
"toList GNil = []"
| "toList (GCons xbc G) = xbc#(toList G)"
apply (auto, simp add: eqvt_def toList_graph_aux_def )
using neq_GNil_conv surj_pair by metis
nominal_termination (eqvt)
by lexicographic_order

nominal_function toSet :: "Γ ⇒ (x*b*c) set" where
"toSet GNil = {}"
| "toSet (GCons xbc G) = {xbc} ∪ (toSet G)"
apply (auto,simp add: eqvt_def toSet_graph_aux_def )
using neq_GNil_conv surj_pair by metis
nominal_termination (eqvt)
by lexicographic_order

nominal_function append_g :: "Γ ⇒ Γ ⇒ Γ" (infixr "@" 65) where
"append_g GNil g = g"
| "append_g (xbc #⇩Γ g1) g2 = (xbc #⇩Γ (g1@g2))"
apply (auto,simp add: eqvt_def append_g_graph_aux_def )
using neq_GNil_conv surj_pair by metis
nominal_termination (eqvt) by lexicographic_order

nominal_function dom  ::  "Γ ⇒ x set"  where
"dom Γ = (fst (toSet Γ))"
apply auto
unfolding  eqvt_def dom_graph_aux_def lfp_eqvt toSet.eqvt by simp
nominal_termination (eqvt) by lexicographic_order

text ‹ Use of this is sometimes mixed in with use of freshness and support for the context however it makes it clear
that for immutable variables, the context is self-supporting'›

nominal_function atom_dom  ::  "Γ ⇒ atom set"  where
"atom_dom Γ  = atom(dom  Γ)"
apply auto
unfolding  eqvt_def atom_dom_graph_aux_def lfp_eqvt toSet.eqvt by simp
nominal_termination (eqvt) by lexicographic_order

subsection ‹Immutable Variable Context Lemmas›

lemma append_GNil[simp]:
"GNil @ G = G"
by simp

lemma append_g_toSetU [simp]: "toSet (G1@G2) = toSet G1 ∪ toSet G2"
by(induct G1, auto+)

lemma supp_GNil:
shows "supp GNil = {}"

lemma supp_GCons:
fixes xs::Γ
shows "supp (x #⇩Γ xs) = supp x ∪ supp xs"
by (simp add: supp_def Collect_imp_eq Collect_neg_eq)

lemma atom_dom_eq[simp]:
fixes G::Γ
shows  "atom_dom ((x, b, c) #⇩Γ G) = atom_dom ((x, b, c') #⇩Γ G)"
using atom_dom.simps toSet.simps by simp

lemma dom_append[simp]:
"atom_dom (Γ@Γ') = atom_dom Γ ∪ atom_dom Γ'"
using image_Un append_g_toSetU atom_dom.simps dom.simps by metis

lemma dom_cons[simp]:
"atom_dom ((x,b,c) #⇩Γ G) = { atom x } ∪ atom_dom G"
using image_Un append_g_toSetU atom_dom.simps by auto

lemma fresh_GNil[ms_fresh]:
shows "a ♯ GNil"

lemma fresh_GCons[ms_fresh]:
fixes xs::Γ
shows "a ♯ (x #⇩Γ xs) ⟷ a ♯ x ∧ a ♯ xs"

lemma dom_supp_g[simp]:
"atom_dom G ⊆ supp G"
apply(induct G rule: Γ_induct,simp)
using supp_at_base supp_Pair atom_dom.simps supp_GCons by fastforce

lemma fresh_append_g[ms_fresh]:
fixes xs::Γ
shows "a ♯ (xs @ ys) ⟷ a ♯ xs ∧ a ♯ ys"
by (induct xs) (simp_all add: fresh_GNil fresh_GCons)

lemma append_g_assoc:
fixes xs::Γ
shows  "(xs @ ys) @ zs = xs @ (ys @ zs)"
by (induct xs) simp_all

lemma append_g_inside:
fixes xs::Γ
shows "xs @ (x #⇩Γ ys) = (xs @ (x #⇩Γ GNil)) @ ys"
by(induct xs,auto+)

lemma finite_Γ:
"finite (toSet Γ)"
by(induct Γ rule: Γ_induct,auto)

lemma supp_Γ:
"supp Γ = supp (toSet Γ)"
proof(induct Γ rule: Γ_induct)
case GNil
then show ?case using supp_GNil toSet.simps
next
case (GCons x b c Γ')
then show ?case using  supp_GCons toSet.simps finite_Γ supp_of_finite_union
using supp_of_finite_insert by fastforce
qed

lemma supp_of_subset:
fixes G::"('a::fs set)"
assumes "finite G" and "finite G'" and "G ⊆ G'"
shows "supp G ⊆ supp G'"
using supp_of_finite_sets assms  by (metis subset_Un_eq supp_of_finite_union)

lemma supp_weakening:
assumes "toSet G ⊆ toSet G'"
shows "supp G ⊆ supp G'"
using supp_Γ finite_Γ by (simp add: supp_of_subset assms)

lemma fresh_weakening[ms_fresh]:
assumes "toSet G ⊆ toSet G'" and "x ♯ G'"
shows "x ♯ G"
proof(rule ccontr)
assume "¬ x ♯ G"
hence "x ∈ supp G" using fresh_def by auto
hence "x ∈ supp G'" using supp_weakening assms by auto
thus False using fresh_def assms by auto
qed

instance Γ :: fs
by (standard, induct_tac x, simp_all add: supp_GNil supp_GCons  finite_supp)

lemma fresh_gamma_elem:
fixes Γ::Γ
assumes "a ♯ Γ"
and "e ∈ toSet Γ"
shows "a ♯ e"
using assms by(induct Γ,auto simp add: fresh_GCons)

lemma fresh_gamma_append:
fixes xs::Γ
shows "a ♯ (xs @ ys) ⟷ a ♯ xs ∧ a ♯ ys"
by (induct xs, simp_all add: fresh_GNil fresh_GCons)

lemma supp_triple[simp]:
shows "supp (x, y, z) = supp x ∪ supp y ∪ supp z"
proof -
have "supp (x,y,z) = supp (x,(y,z))"  by auto
hence "supp (x,y,z) = supp x ∪ (supp y  ∪ supp z)" using supp_Pair by metis
thus ?thesis by auto
qed

lemma supp_append_g:
fixes xs::Γ
shows "supp (xs @ ys) = supp xs ∪ supp ys"
by(induct xs,auto simp add: supp_GNil supp_GCons )

lemma fresh_in_g[simp]:
fixes Γ::Γ and x'::x
shows "atom x' ♯ Γ' @ (x, b0, c0) #⇩Γ Γ = (atom x' ∉ supp Γ' ∪ supp x ∪ supp b0 ∪ supp c0 ∪ supp Γ)"
proof -
have  "atom x' ♯ Γ' @ (x, b0, c0) #⇩Γ Γ = (atom x' ∉ supp (Γ' @((x,b0,c0) #⇩Γ Γ)))"
using fresh_def by auto
also have "... = (atom x' ∉ supp Γ' ∪ supp ((x,b0,c0) #⇩Γ Γ))" using supp_append_g by fast
also have "... = (atom x' ∉ supp Γ' ∪ supp x ∪ supp b0 ∪ supp c0 ∪ supp Γ)" using supp_GCons supp_append_g supp_triple  by auto
finally show ?thesis by fast
qed

lemma fresh_suffix[ms_fresh]:
fixes Γ::Γ
assumes "atom x ♯ Γ'@Γ"
shows "atom x ♯ Γ"
using assms by(induct  Γ' rule: Γ_induct, auto simp add: append_g.simps fresh_GCons)

lemma not_GCons_self [simp]:
fixes xs::Γ
shows "xs ≠ x #⇩Γ xs"
by (induct xs) auto

lemma not_GCons_self2 [simp]:
fixes xs::Γ
shows "x #⇩Γ xs ≠ xs"
by (rule not_GCons_self [symmetric])

lemma fresh_restrict:
fixes y::x and Γ::Γ
assumes  "atom y ♯  (Γ' @ (x, b, c) #⇩Γ Γ)"
shows "atom y ♯ (Γ'@Γ)"
using assms by(induct Γ' rule: Γ_induct, auto simp add:fresh_GCons fresh_GNil  )

lemma fresh_dom_free:
assumes "atom x ♯ Γ"
shows "(x,b,c) ∉ toSet Γ"
using assms proof(induct Γ rule: Γ_induct)
case GNil
then show ?case by auto
next
case (GCons x' b' c' Γ')
hence "x≠x'" using fresh_def fresh_GCons fresh_Pair supp_at_base by blast
moreover have "atom x ♯ Γ'" using fresh_GCons GCons by auto
ultimately show ?case using toSet.simps GCons by auto
qed

lemma Γ_set_intros: "x ∈ toSet ( x #⇩Γ xs)" and "y ∈ toSet xs ⟹ y ∈ toSet (x #⇩Γ xs)"
by simp+

lemma fresh_dom_free2:
assumes "atom x ∉ atom_dom Γ"
shows "(x,b,c) ∉ toSet Γ"
using assms proof(induct Γ rule: Γ_induct)
case GNil
then show ?case by auto
next
case (GCons x' b' c' Γ')
hence "x≠x'" using fresh_def fresh_GCons fresh_Pair supp_at_base by auto
moreover have "atom x ∉ atom_dom Γ'" using fresh_GCons GCons by auto
ultimately show ?case using toSet.simps GCons by auto
qed

subsection ‹Mutable Variable Context Lemmas›

lemma supp_DNil:
shows "supp DNil = {}"

lemma supp_DCons:
fixes xs::Δ
shows "supp (x #⇩Δ xs) = supp x ∪ supp xs"
by (simp add: supp_def Collect_imp_eq Collect_neg_eq)

lemma fresh_DNil[ms_fresh]:
shows "a ♯ DNil"

lemma fresh_DCons[ms_fresh]:
fixes xs::Δ
shows "a ♯ (x #⇩Δ xs) ⟷ a ♯ x ∧ a ♯ xs"

instance Δ :: fs
by (standard, induct_tac x, simp_all add: supp_DNil supp_DCons  finite_supp)

subsection ‹Lookup Functions›

nominal_function lookup :: "Γ ⇒ x ⇒ (b*c) option" where
"lookup GNil x = None"
| "lookup ((x,b,c)#⇩ΓG) y = (if x=y then Some (b,c) else lookup G y)"
by (auto,simp add: eqvt_def lookup_graph_aux_def, metis neq_GNil_conv surj_pair)
nominal_termination (eqvt) by lexicographic_order

nominal_function replace_in_g :: "Γ ⇒ x ⇒ c ⇒ Γ"  ("_[_⟼_]" [1000,0,0] 200) where
"replace_in_g GNil _ _ = GNil"
| "replace_in_g ((x,b,c)#⇩ΓG) x' c' = (if x=x' then ((x,b,c')#⇩ΓG) else (x,b,c)#⇩Γ(replace_in_g G x' c'))"
using surj_pair Γ.exhaust by metis
nominal_termination (eqvt) by lexicographic_order

text ‹ Functions for looking up data-constructors in the Pi context ›

nominal_function lookup_fun :: "Φ ⇒ f  ⇒ fun_def option" where
"lookup_fun [] g = None"
|  "lookup_fun ((AF_fundef f ft)#Π) g = (if (f=g) then Some (AF_fundef f ft) else lookup_fun Π g)"
by (metis fun_def.exhaust neq_Nil_conv)
nominal_termination (eqvt)  by lexicographic_order

nominal_function lookup_td :: "Θ ⇒ string  ⇒ type_def option" where
"lookup_td [] g = None"
|  "lookup_td ((AF_typedef s lst ) # (Θ::Θ)) g = (if (s = g) then Some (AF_typedef s lst ) else lookup_td Θ g)"
|  "lookup_td ((AF_typedef_poly s bv lst ) # (Θ::Θ)) g = (if (s = g) then Some (AF_typedef_poly s bv lst ) else lookup_td Θ g)"
by (metis type_def.exhaust neq_Nil_conv)
nominal_termination (eqvt)  by lexicographic_order

nominal_function name_of_type  ::"type_def ⇒ f "  where
"name_of_type (AF_typedef f _ ) = f"
| "name_of_type (AF_typedef_poly f _ _) = f"
using type_def.exhaust by blast
nominal_termination (eqvt)  by lexicographic_order

nominal_function name_of_fun  ::"fun_def ⇒ f "  where
"name_of_fun  (AF_fundef f ft) = f"
using fun_def.exhaust by blast
nominal_termination (eqvt)  by lexicographic_order

nominal_function remove2 :: "'a::pt ⇒ 'a list ⇒ 'a list" where
"remove2 x [] = []" |
"remove2 x (y # xs) = (if x = y then xs else y # remove2 x xs)"
by (simp add: eqvt_def remove2_graph_aux_def,auto+,meson list.exhaust)
nominal_termination (eqvt)  by lexicographic_order

nominal_function base_for_lit :: "l ⇒ b" where
"base_for_lit (L_true) = B_bool "
| "base_for_lit (L_false) = B_bool "
| "base_for_lit (L_num n) = B_int "
| "base_for_lit (L_unit) = B_unit "
| "base_for_lit (L_bitvec v) = B_bitvec"
apply (auto simp: eqvt_def base_for_lit_graph_aux_def )
using l.strong_exhaust by blast
nominal_termination (eqvt) by lexicographic_order

lemma neq_DNil_conv: "(xs ≠ DNil) = (∃y ys. xs = y #⇩Δ ys)"
by (induct xs) auto

nominal_function setD :: "Δ ⇒ (u*τ) set" where
"setD DNil = {}"
| "setD (DCons xbc G) = {xbc} ∪ (setD G)"
apply (auto,simp add: eqvt_def setD_graph_aux_def )
using neq_DNil_conv surj_pair by metis
nominal_termination (eqvt) by lexicographic_order

lemma eqvt_triple:
fixes y::"'a::at" and ya::"'a::at" and xa::"'c::at" and va::"'d::fs" and s::s and sa::s and f::"s*'c*'d ⇒ s"
assumes "atom y ♯ (xa, va)" and "atom ya ♯ (xa, va)" and
"∀c. atom c ♯ (s, sa) ⟶ atom c ♯ (y, ya, s, sa) ⟶ (y ↔ c) ∙ s = (ya ↔ c) ∙ sa"
and "eqvt_at f (s,xa,va)" and "eqvt_at f (sa,xa,va)" and
"atom c ♯ (s, va, xa, sa)" and "atom c ♯ (y, ya, f (s, xa, va), f (sa, xa, va))"
shows "(y ↔ c) ∙ f (s, xa, va) =  (ya ↔ c) ∙ f (sa, xa, va)"
proof -
have " (y ↔ c) ∙ f (s, xa, va) = f ( (y ↔ c) ∙ (s,xa,va))" using assms eqvt_at_def by metis
also have "... = f ( (y ↔ c) ∙ s, (y ↔ c) ∙ xa ,(y ↔ c) ∙ va)" by auto
also have "... = f ( (ya ↔ c) ∙ sa, (ya ↔ c) ∙ xa ,(ya ↔ c) ∙ va)" proof -
have " (y ↔ c) ∙ s = (ya ↔ c) ∙ sa" using assms Abs1_eq_iff_all by auto
moreover have  "((y ↔ c) ∙ xa) =  ((ya ↔ c) ∙ xa)" using assms flip_fresh_fresh fresh_prodN by metis
moreover have  "((y ↔ c) ∙ va) =  ((ya ↔ c) ∙ va)" using assms flip_fresh_fresh fresh_prodN by metis
ultimately show ?thesis by auto
qed
also have "... =  f ( (ya ↔ c) ∙ (sa,xa,va))" by auto
finally show ?thesis using assms eqvt_at_def by metis
qed

section ‹Functions for bit list/vectors›

inductive split :: "int ⇒ bit list ⇒ bit list * bit list ⇒ bool" where
"split 0 xs ([], xs)"
| "split m xs (ys,zs) ⟹ split (m+1) (x#xs) ((x # ys), zs)"
equivariance split
nominal_inductive split .

lemma split_concat:
assumes "split n v (v1,v2)"
shows "v = append v1 v2"
using assms proof(induct "(v1,v2)" arbitrary: v1 v2 rule: split.inducts)
case 1
then show ?case by auto
next
case (2 m xs ys zs x)
then show ?case by auto
qed

lemma split_n:
assumes "split n v (v1,v2)"
shows "0 ≤ n ∧ n ≤ int (length v)"
using assms proof(induct rule: split.inducts)
case (1 xs)
then show ?case by auto
next
case (2 m xs ys zs x)
then show ?case by auto
qed

lemma split_length:
assumes "split n v (v1,v2)"
shows "n = int (length v1)"
using assms proof(induct  "(v1,v2)" arbitrary: v1 v2 rule: split.inducts)
case (1 xs)
then show ?case by auto
next
case (2 m xs ys zs x)
then show ?case by auto
qed

lemma obtain_split:
assumes "0 ≤ n" and "n ≤ int (length bv)"
shows "∃ bv1 bv2. split n bv (bv1 , bv2)"
using assms proof(induct bv arbitrary: n)
case Nil
then show ?case using split.intros by auto
next
case (Cons b bv)
show ?case proof(cases "n = 0")
case True
then show ?thesis using split.intros by auto
next
case False
then obtain m where m:"n=m+1" using Cons
moreover have "0 ≤ m" using False m Cons by linarith
then obtain bv1 and bv2 where "split m bv (bv1 , bv2)" using Cons m by force
hence "split n (b # bv) ((b#bv1), bv2)" using m split.intros by auto
then show ?thesis by auto
qed
qed

end

# Theory IVSubst

(*<*)
theory IVSubst
imports  Syntax
begin
(*>*)

chapter ‹Immutable Variable Substitution›

text ‹Substitution involving immutable variables. We define a class and instances for all
of the term forms›

section ‹Class›

class has_subst_v = fs +
fixes subst_v :: "'a::fs ⇒ x ⇒ v ⇒ 'a::fs"   ("_[_::=_]⇩v" [1000,50,50] 1000)
assumes fresh_subst_v_if:  "y ♯ (subst_v a x v)  ⟷ (atom x ♯ a ∧ y ♯ a) ∨ (y ♯ v ∧ (y ♯ a ∨ y = atom x))"
and    forget_subst_v[simp]:  "atom x ♯ a ⟹ subst_v a  x v = a"
and    subst_v_id[simp]:      "subst_v a x (V_var x) = a"
and    eqvt[simp,eqvt]:       "(p::perm) ∙ (subst_v a x v) = (subst_v  (p ∙ a) (p ∙x) (p ∙v))"
and    flip_subst_v[simp]:    "atom x ♯ c ⟹ ((x ↔ z) ∙ c) = c[z::=[x]⇧v]⇩v"
and    subst_v_simple_commute[simp]: "atom x ♯ c ⟹(c[z::=[x]⇧v]⇩v)[x::=b]⇩v = c[z::=b]⇩v"
begin

lemma subst_v_flip_eq_one:
fixes z1::x and z2::x and x1::x and x2::x
assumes "[[atom z1]]lst. c1 = [[atom z2]]lst. c2"
and "atom x1 ♯ (z1,z2,c1,c2)"
shows "(c1[z1::=[x1]⇧v]⇩v) = (c2[z2::=[x1]⇧v]⇩v)"
proof -
have "(c1[z1::=[x1]⇧v]⇩v) = (x1 ↔ z1) ∙ c1" using assms flip_subst_v by auto
moreover have  "(c2[z2::=[x1]⇧v]⇩v) = (x1 ↔ z2) ∙ c2" using assms flip_subst_v by auto
ultimately show ?thesis using Abs1_eq_iff_all(3)[of z1 c1 z2 c2 z1]  assms
by (metis Abs1_eq_iff_fresh(3) flip_commute)
qed

lemma subst_v_flip_eq_two:
fixes z1::x and z2::x and x1::x and x2::x
assumes "[[atom z1]]lst. c1 = [[atom z2]]lst. c2"
shows "(c1[z1::=b]⇩v) = (c2[z2::=b]⇩v)"
proof -
obtain x::x where *:"atom x ♯ (z1,z2,c1,c2)" using obtain_fresh by metis
hence "(c1[z1::=[x]⇧v]⇩v) = (c2[z2::=[x]⇧v]⇩v)" using subst_v_flip_eq_one[OF assms, of x] by metis
hence "(c1[z1::=[x]⇧v]⇩v)[x::=b]⇩v = (c2[z2::=[x]⇧v]⇩v)[x::=b]⇩v" by auto
thus ?thesis using subst_v_simple_commute * fresh_prod4 by metis
qed

lemma subst_v_flip_eq_three:
assumes "[[atom z1]]lst. c1 = [[atom z1']]lst. c1'"  and "atom x ♯ c1" and "atom x' ♯ (x,z1,z1', c1, c1')"
shows   "(x ↔ x') ∙ (c1[z1::=[x]⇧v]⇩v) =  c1'[z1'::=[x']⇧v]⇩v"
proof -
have "atom x' ♯ c1[z1::=[x]⇧v]⇩v" using assms fresh_subst_v_if by simp
hence "(x ↔ x') ∙ (c1[z1::=[x]⇧v]⇩v) = c1[z1::=[x]⇧v]⇩v[x::=[x']⇧v]⇩v" using flip_subst_v[of x' "c1[z1::=[x]⇧v]⇩v" x] flip_commute by metis
also have "... = c1[z1::=[x']⇧v]⇩v" using subst_v_simple_commute fresh_prod4 assms by auto
also have "... = c1'[z1'::=[x']⇧v]⇩v" using subst_v_flip_eq_one[of z1 c1 z1' c1' x'] using  assms by auto
finally show ?thesis by auto
qed

end

section ‹Values›

nominal_function
subst_vv :: "v ⇒ x ⇒ v ⇒ v" where
"subst_vv (V_lit l) x v = V_lit l"
| "subst_vv (V_var y) x v = (if x = y then v else V_var y)"
| "subst_vv (V_cons tyid c v') x v  = V_cons tyid c (subst_vv v' x v)"
| "subst_vv (V_consp tyid c b v') x v  = V_consp tyid c b (subst_vv v' x v)"
| "subst_vv (V_pair v1 v2) x v = V_pair (subst_vv v1 x v ) (subst_vv v2 x v )"
by(auto simp: eqvt_def subst_vv_graph_aux_def, metis v.strong_exhaust)
nominal_termination (eqvt) by lexicographic_order

abbreviation
subst_vv_abbrev :: "v ⇒ x ⇒ v ⇒ v" ("_[_::=_]⇩v⇩v" [1000,50,50] 1000)
where
"v[x::=v']⇩v⇩v  ≡ subst_vv v x v'"

lemma fresh_subst_vv_if [simp]:
"j ♯ t[i::=x]⇩v⇩v  = ((atom i ♯ t ∧ j ♯ t) ∨ (j ♯ x ∧ (j ♯ t ∨ j = atom i)))"
using supp_l_empty apply (induct t rule: v.induct,auto simp add: subst_vv.simps fresh_def, auto)
by (simp add: supp_at_base |metis b.supp supp_b_empty  )+

lemma forget_subst_vv [simp]: "atom a ♯ tm ⟹ tm[a::=x]⇩v⇩v = tm"
by (induct tm rule: v.induct) (simp_all add: fresh_at_base)

lemma subst_vv_id [simp]: "tm[a::=V_var a]⇩v⇩v  = tm"
by (induct tm rule: v.induct) simp_all

lemma subst_vv_commute [simp]:
"atom j ♯ tm ⟹ tm[i::=t]⇩v⇩v[j::=u]⇩v⇩v = tm[i::=t[j::=u]⇩v⇩v]⇩v⇩v "
by (induct tm rule: v.induct) (auto simp: fresh_Pair)

lemma subst_vv_commute_full [simp]:
"atom j ♯ t ⟹ atom i ♯ u ⟹ i ≠ j ⟹ tm[i::=t]⇩v⇩v[j::=u]⇩v⇩v = tm[j::=u]⇩v⇩v[i::=t]⇩v⇩v"
by (induct tm rule: v.induct) auto

lemma subst_vv_var_flip[simp]:
fixes v::v
assumes "atom y ♯ v"
shows "(y ↔ x) ∙ v = v [x::=V_var y]⇩v⇩v"
using assms apply(induct v rule:v.induct)
apply auto
using  l.fresh l.perm_simps l.strong_exhaust supp_l_empty permute_pure permute_list.simps fresh_def flip_fresh_fresh apply fastforce
using permute_pure apply blast+
done

instantiation v :: has_subst_v
begin

definition
"subst_v = subst_vv"

instance proof
fix j::atom and i::x and  x::v and t::v
show  "(j ♯ subst_v t i x) = ((atom i ♯ t ∧ j ♯ t) ∨ (j ♯ x ∧ (j ♯ t ∨ j = atom i)))"
using fresh_subst_vv_if[of j t i x] subst_v_v_def by metis

fix a::x and tm::v and x::v
show "atom a ♯ tm ⟹ subst_v tm a x  = tm"
using forget_subst_vv subst_v_v_def by simp

fix a::x and tm::v
show "subst_v tm a (V_var a) = tm" using subst_vv_id  subst_v_v_def by simp

fix p::perm and x1::x and v::v and t1::v
show "p ∙ subst_v t1 x1 v  = subst_v  (p ∙ t1) (p ∙ x1) (p ∙ v)"
using   subst_v_v_def by simp

fix x::x and c::v and z::x
show "atom x ♯ c ⟹ ((x ↔ z) ∙ c) = c[z::=[x]⇧v]⇩v"
using  subst_v_v_def by simp

fix x::x and c::v and z::x
show  "atom x ♯ c ⟹ c[z::=[x]⇧v]⇩v[x::=v]⇩v = c[z::=v]⇩v"
using  subst_v_v_def by simp
qed

end

section ‹Expressions›

nominal_function subst_ev :: "e ⇒ x ⇒ v  ⇒ e" where
"subst_ev  ( (AE_val v') ) x v = ( (AE_val (subst_vv v' x v)) )"
| "subst_ev  ( (AE_app f v') ) x v  = ( (AE_app f (subst_vv v' x v )) )"
| "subst_ev  ( (AE_appP f b v') ) x v = ( (AE_appP f b (subst_vv v' x v )) )"
| "subst_ev  ( (AE_op opp v1 v2) ) x v  = ( (AE_op opp (subst_vv v1 x v ) (subst_vv v2 x v )) )"
| "subst_ev  [#1 v']⇧e x v = [#1 (subst_vv v' x v )]⇧e"
| "subst_ev  [#2 v']⇧e x v = [#2 (subst_vv v' x v )]⇧e"
| "subst_ev  ( (AE_mvar u)) x v = AE_mvar u"
| "subst_ev  [| v' |]⇧e x v = [| (subst_vv  v' x v ) |]⇧e"
| "subst_ev  ( AE_concat v1 v2) x v = AE_concat (subst_vv v1 x v ) (subst_vv v2 x v )"
| "subst_ev  ( AE_split v1 v2) x v = AE_split (subst_vv v1 x v ) (subst_vv v2 x v )"

nominal_termination (eqvt) by lexicographic_order

abbreviation
subst_ev_abbrev :: "e ⇒ x ⇒ v ⇒ e" ("_[_::=_]⇩e⇩v" [1000,50,50] 500)
where
"e[x::=v']⇩e⇩v  ≡ subst_ev e x v' "

lemma size_subst_ev [simp]: "size ( subst_ev A i x) = size A"
apply (nominal_induct A avoiding: i x rule: e.strong_induct)
by auto

lemma forget_subst_ev [simp]: "atom a ♯ A ⟹ subst_ev A a x  = A"
apply (nominal_induct A avoiding: a x rule: e.strong_induct)
by (auto simp: fresh_at_base)

lemma subst_ev_id [simp]: "subst_ev A a (V_var a)  = A"
by (nominal_induct A avoiding: a rule: e.strong_induct) (auto simp: fresh_at_base)

lemma fresh_subst_ev_if [simp]:
"j ♯ (subst_ev A i x ) = ((atom i ♯ A ∧ j ♯ A) ∨ (j ♯ x ∧ (j ♯ A ∨ j = atom i)))"
apply (induct A rule: e.induct)
unfolding subst_ev.simps fresh_subst_vv_if apply auto+
using pure_fresh fresh_opp_all apply metis+
done

lemma subst_ev_commute [simp]:
"atom j ♯ A ⟹ (A[i::=t]⇩e⇩v)[j::=u]⇩e⇩v = A[i::=t[j::=u]⇩v⇩v]⇩e⇩v"
by (nominal_induct A avoiding: i j t u rule: e.strong_induct) (auto simp: fresh_at_base)

lemma subst_ev_var_flip[simp]:
fixes e::e and y::x and x::x
assumes "atom y ♯ e"
shows "(y ↔ x) ∙ e = e [x::=V_var y]⇩e⇩v"
using assms apply(nominal_induct e rule:e.strong_induct)
apply (metis (mono_tags, lifting) b.eq_iff b.perm_simps e.fresh e.perm_simps flip_b_id subst_ev.simps subst_vv_var_flip)
apply (metis (mono_tags, lifting) b.eq_iff b.perm_simps e.fresh e.perm_simps flip_b_id subst_ev.simps subst_vv_var_flip)
subgoal for x
apply (rule_tac y=x in  opp.strong_exhaust)
using  subst_vv_var_flip flip_def by (simp add: flip_def permute_pure)+
using  subst_vv_var_flip flip_def by (simp add: flip_def permute_pure)+

lemma subst_ev_flip:
fixes e::e and ea::e and c::x
assumes "atom c ♯ (e, ea)" and "atom c ♯ (x, xa, e, ea)" and "(x ↔ c) ∙ e = (xa ↔ c) ∙ ea"
shows "e[x::=v']⇩e⇩v = ea[xa::=v']⇩e⇩v"
proof -
have "e[x::=v']⇩e⇩v = (e[x::=V_var c]⇩e⇩v)[c::=v']⇩e⇩v" using subst_ev_commute assms by simp
also have "...  = ((c ↔ x) ∙ e)[c::=v']⇩e⇩v" using subst_ev_var_flip assms by simp
also have "... = ((c ↔ xa) ∙ ea)[c::=v']⇩e⇩v" using assms flip_commute by metis
also have "... = ea[xa::=v']⇩e⇩v"  using subst_ev_var_flip assms  by simp
finally show ?thesis by auto
qed

lemma subst_ev_var[simp]:
"(AE_val (V_var x))[x::=[z]⇧v]⇩e⇩v = AE_val (V_var z)"
by auto

instantiation e :: has_subst_v
begin

definition
"subst_v = subst_ev"

instance proof
fix j::atom and i::x and  x::v and t::e
show  "(j ♯ subst_v t i x) = ((atom i ♯ t ∧ j ♯ t) ∨ (j ♯ x ∧ (j ♯ t ∨ j = atom i)))"
using fresh_subst_ev_if[of j t i x] subst_v_e_def by metis

fix a::x and tm::e and x::v
show "atom a ♯ tm ⟹ subst_v tm a x  = tm"
using forget_subst_ev subst_v_e_def by simp

fix a::x and tm::e
show "subst_v tm a (V_var a) = tm" using subst_ev_id  subst_v_e_def by simp

fix p::perm and x1::x and v::v and t1::e
show "p ∙ subst_v t1 x1 v  = subst_v  (p ∙ t1) (p ∙ x1) (p ∙ v)"
using subst_ev_commute  subst_v_e_def by simp

fix x::x and c::e and z::x
show "atom x ♯ c ⟹ ((x ↔ z) ∙ c) = c[z::=[x]⇧v]⇩v"
using  subst_v_e_def by simp

fix x::x and c::e and z::x
show  "atom x ♯ c ⟹ c[z::=[x]⇧v]⇩v[x::=v]⇩v = c[z::=v]⇩v"
using  subst_v_e_def by simp
qed
end

lemma subst_ev_commute_full:
fixes e::e and w::v and v::v
assumes "atom z ♯ v" and "atom x ♯ w" and "x ≠ z"
shows "subst_ev  (e[z::=w]⇩e⇩v) x v = subst_ev  (e[x::=v]⇩e⇩v) z w"
using assms by(nominal_induct e rule: e.strong_induct,simp+)

lemma subst_ev_v_flip1[simp]:
fixes e::e
assumes "atom z1 ♯ (z,e)" and "atom z1' ♯ (z,e)"
shows"(z1 ↔ z1') ∙ e[z::=v]⇩e⇩v =  e[z::= ((z1 ↔ z1') ∙ v)]⇩e⇩v"
using assms proof(nominal_induct e rule:e.strong_induct)
qed  (simp add: flip_def fresh_Pair swap_fresh_fresh)+

section ‹Expressions in Constraints›

nominal_function subst_cev :: "ce ⇒ x ⇒ v  ⇒ ce" where
"subst_cev ( (CE_val v') ) x v = ( (CE_val (subst_vv  v' x v )) )"
| "subst_cev ( (CE_op opp v1 v2) ) x v = ( (CE_op opp (subst_cev  v1 x v ) (subst_cev v2 x v )) )"
| "subst_cev ( (CE_fst v')) x v = CE_fst (subst_cev  v' x v )"
| "subst_cev ( (CE_snd v')) x v = CE_snd (subst_cev  v' x v )"
| "subst_cev ( (CE_len v')) x v = CE_len (subst_cev  v' x v )"
| "subst_cev ( CE_concat v1 v2) x v = CE_concat (subst_cev v1 x v ) (subst_cev v2 x v )"
by (meson ce.strong_exhaust)

nominal_termination (eqvt) by lexicographic_order

abbreviation
subst_cev_abbrev :: "ce ⇒ x ⇒ v ⇒ ce" ("_[_::=_]⇩c⇩e⇩v" [1000,50,50] 500)
where
"e[x::=v']⇩c⇩e⇩v  ≡ subst_cev  e x v'"

lemma size_subst_cev [simp]: "size ( subst_cev A i x ) = size A"
by (nominal_induct A avoiding: i x rule: ce.strong_induct,auto)

lemma forget_subst_cev [simp]: "atom a ♯ A ⟹ subst_cev A a x  = A"
by (nominal_induct A avoiding: a x rule: ce.strong_induct, auto simp: fresh_at_base)

lemma subst_cev_id [simp]: "subst_cev A a (V_var a)  = A"
by (nominal_induct A avoiding: a rule: ce.strong_induct) (auto simp: fresh_at_base)

lemma fresh_subst_cev_if [simp]:
"j ♯ (subst_cev A i x ) = ((atom i ♯ A ∧ j ♯ A) ∨ (j ♯ x ∧ (j ♯ A ∨ j = atom i)))"
proof(nominal_induct A avoiding: i x rule: ce.strong_induct)
case (CE_op opp v1 v2)
then show ?case  using fresh_subst_vv_if subst_ev.simps e.supp pure_fresh opp.fresh
fresh_e_opp
using fresh_opp_all by auto
qed(auto)+

lemma subst_cev_commute [simp]:
"atom j ♯ A ⟹ (subst_cev (subst_cev A i t ) j u) = subst_cev A i (subst_vv t j u )"
by (nominal_induct A avoiding: i j t u rule: ce.strong_induct) (auto simp: fresh_at_base)

lemma subst_cev_var_flip[simp]:
fixes e::ce and y::x and x::x
assumes "atom y ♯ e"
shows "(y ↔ x) ∙ e = e [x::=V_var y]⇩c⇩e⇩v"
using assms proof(nominal_induct e rule:ce.strong_induct)
case (CE_val v)
then show ?case using subst_vv_var_flip by auto
next
case (CE_op opp v1 v2)
hence yf: "atom y ♯ v1 ∧ atom y ♯ v2" using ce.fresh by blast
have " (y ↔ x) ∙ (CE_op opp v1 v2 ) = CE_op ((y ↔ x) ∙ opp) ( (y ↔ x) ∙ v1 ) ( (y ↔ x) ∙ v2)"
using opp.perm_simps ce.perm_simps permute_pure ce.fresh opp.strong_exhaust by presburger
also have "... = CE_op ((y ↔ x) ∙ opp) (v1[x::=V_var y]⇩c⇩e⇩v) (v2 [x::=V_var y]⇩c⇩e⇩v)" using yf
finally show ?case using subst_cev.simps  opp.perm_simps  opp.strong_exhaust
by (metis (full_types))
qed( (auto simp add: permute_pure subst_vv_var_flip)+)

lemma subst_cev_flip:
fixes e::ce and ea::ce and c::x
assumes "atom c ♯ (e, ea)" and "atom c ♯ (x, xa, e, ea)" and "(x ↔ c) ∙ e = (xa ↔ c) ∙ ea"
shows "e[x::=v']⇩c⇩e⇩v = ea[xa::=v']⇩c⇩e⇩v"
proof -
have "e[x::=v']⇩c⇩e⇩v = (e[x::=V_var c]⇩c⇩e⇩v)[c::=v']⇩c⇩e⇩v" using subst_ev_commute assms by simp
also have "...  = ((c ↔ x) ∙ e)[c::=v']⇩c⇩e⇩v" using subst_ev_var_flip assms by simp
also have "... = ((c ↔ xa) ∙ ea)[c::=v']⇩c⇩e⇩v" using assms flip_commute by metis
also have "... = ea[xa::=v']⇩c⇩e⇩v"  using subst_ev_var_flip assms  by simp
finally show ?thesis by auto
qed

lemma subst_cev_var[simp]:
fixes z::x and x::x
shows  "[[x]⇧v]⇧c⇧e [x::=[z]⇧v]⇩c⇩e⇩v = [[z]⇧v]⇧c⇧e"
by auto

instantiation ce :: has_subst_v
begin

definition
"subst_v = subst_cev"

instance proof
fix j::atom and i::x and  x::v and t::ce
show  "(j ♯ subst_v t i x) = ((atom i ♯ t ∧ j ♯ t) ∨ (j ♯ x ∧ (j ♯ t ∨ j = atom i)))"
using fresh_subst_cev_if[of j t i x] subst_v_ce_def by metis

fix a::x and tm::ce and x::v
show "atom a ♯ tm ⟹ subst_v tm a x  = tm"
using forget_subst_cev subst_v_ce_def by simp

fix a::x and tm::ce
show "subst_v tm a (V_var a) = tm" using subst_cev_id  subst_v_ce_def by simp

fix p::perm and x1::x and v::v and t1::ce
show "p ∙ subst_v t1 x1 v  = subst_v  (p ∙ t1) (p ∙ x1) (p ∙ v)"
using subst_cev_commute  subst_v_ce_def by simp

fix x::x and c::ce and z::x
show "atom x ♯ c ⟹ ((x ↔ z) ∙ c) = c [z::=V_var x]⇩v"
using  subst_v_ce_def by simp

fix x::x and c::ce and z::x
show  "atom x ♯ c ⟹ c [z::=V_var x]⇩v[x::=v]⇩v = c[z::=v]⇩v"
using  subst_v_ce_def by simp
qed

end

lemma subst_cev_commute_full:
fixes e::ce and w::v and v::v
assumes "atom z ♯ v" and "atom x ♯ w" and "x ≠ z"
shows "subst_cev (e[z::=w]⇩c⇩e⇩v) x v  = subst_cev (e[x::=v]⇩c⇩e⇩v) z w "
using assms by(nominal_induct e rule: ce.strong_induct,simp+)

lemma subst_cev_v_flip1[simp]:
fixes e::ce
assumes "atom z1 ♯ (z,e)" and "atom z1' ♯ (z,e)"
shows"(z1 ↔ z1') ∙ e[z::=v]⇩c⇩e⇩v =  e[z::= ((z1 ↔ z1') ∙ v)]⇩c⇩e⇩v"
using assms apply(nominal_induct e rule:ce.strong_induct)
by (simp add: flip_def fresh_Pair swap_fresh_fresh)+

section ‹Constraints›

nominal_function subst_cv :: "c ⇒ x ⇒ v  ⇒ c" where
"subst_cv (C_true) x v = C_true"
|  "subst_cv (C_false) x v = C_false"
|  "subst_cv (C_conj c1 c2) x v = C_conj (subst_cv c1 x v ) (subst_cv c2 x v )"
|  "subst_cv (C_disj c1 c2) x v = C_disj (subst_cv c1 x v ) (subst_cv c2 x v )"
|  "subst_cv (C_imp c1 c2) x v = C_imp (subst_cv c1 x v ) (subst_cv c2 x v )"
|  "subst_cv (e1 == e2) x v = ((subst_cev e1 x v ) == (subst_cev e2 x v ))"
|  "subst_cv (C_not c) x v = C_not (subst_cv c x v )"
using c.strong_exhaust by metis
nominal_termination (eqvt)  by lexicographic_order

abbreviation
subst_cv_abbrev :: "c ⇒ x ⇒ v ⇒ c" ("_[_::=_]⇩c⇩v" [1000,50,50] 1000)
where
"c[x::=v']⇩c⇩v  ≡ subst_cv c x v'"

lemma size_subst_cv [simp]: "size ( subst_cv A i x ) = size A"
by (nominal_induct A avoiding: i x rule: c.strong_induct,auto)

lemma forget_subst_cv [simp]: "atom a ♯ A ⟹ subst_cv A a x  = A"
by (nominal_induct A avoiding: a x rule: c.strong_induct, auto simp: fresh_at_base)

lemma subst_cv_id [simp]: "subst_cv A a (V_var a)  = A"
by (nominal_induct A avoiding: a rule: c.strong_induct) (auto simp: fresh_at_base)

lemma fresh_subst_cv_if [simp]:
"j ♯ (subst_cv A i x ) ⟷ (atom i ♯ A ∧ j ♯ A) ∨ (j ♯ x ∧ (j ♯ A ∨ j = atom i))"
by (nominal_induct A avoiding: i x rule: c.strong_induct, (auto simp add: pure_fresh)+)

lemma subst_cv_commute [simp]:
"atom j ♯ A ⟹ (subst_cv (subst_cv A i t ) j u ) = subst_cv A i (subst_vv t j u )"
by (nominal_induct A avoiding: i j t u rule: c.strong_induct) (auto simp: fresh_at_base)

lemma let_s_size [simp]: "size s ≤ size (AS_let x e s)"
apply (nominal_induct s avoiding: e x rule: s_branch_s_branch_list.strong_induct(1))
apply auto
done

lemma subst_cv_var_flip[simp]:
fixes c::c
assumes "atom y ♯ c"
shows "(y ↔ x) ∙ c = c[x::=V_var y]⇩c⇩v"
using assms by(nominal_induct c rule:c.strong_induct,(simp add: flip_subst_v subst_v_ce_def)+)

instantiation c :: has_subst_v
begin

definition
"subst_v = subst_cv"

instance proof
fix j::atom and i::x and  x::v and t::c
show  "(j ♯ subst_v t i x) = ((atom i ♯ t ∧ j ♯ t) ∨ (j ♯ x ∧ (j ♯ t ∨ j = atom i)))"
using fresh_subst_cv_if[of j t i x] subst_v_c_def by metis

fix a::x and tm::c and x::v
show "atom a ♯ tm ⟹ subst_v tm a x  = tm"
using forget_subst_cv subst_v_c_def by simp

fix a::x and tm::c
show "subst_v tm a (V_var a) = tm" using subst_cv_id  subst_v_c_def by simp

fix p::perm and x1::x and v::v and t1::c
show "p ∙ subst_v t1 x1 v  = subst_v  (p ∙ t1) (p ∙ x1) (p ∙ v)"
using subst_cv_commute  subst_v_c_def by simp

fix x::x and c::c and z::x
show "atom x ♯ c ⟹ ((x ↔ z) ∙ c) = c[z::=[x]⇧v]⇩v"
using subst_cv_var_flip subst_v_c_def by simp

fix x::x and c::c and z::x
show  "atom x ♯ c ⟹ c[z::=[x]⇧v]⇩v[x::=v]⇩v = c[z::=v]⇩v"
using subst_cv_var_flip subst_v_c_def by simp
qed

end

lemma subst_cv_var_flip1[simp]:
fixes c::c
assumes "atom y ♯ c"
shows "(x ↔ y) ∙ c = c[x::=V_var y]⇩c⇩v"
using subst_cv_var_flip flip_commute
by (metis assms)

lemma subst_cv_v_flip3[simp]:
fixes c::c
assumes "atom z1 ♯ c" and "atom z1' ♯ c"
shows"(z1 ↔ z1') ∙ c[z::=[z1]⇧v]⇩c⇩v =  c[z::=[z1']⇧v]⇩c⇩v"
proof -
consider "z1' = z" | "z1 = z" | "atom z1 ♯ z ∧ atom z1' ♯ z" by force
then show ?thesis proof(cases)
case 1
then show ?thesis using 1 assms by auto
next
case 2
then show ?thesis using 2 assms by auto
next
case 3
then show ?thesis using assms by auto
qed
qed

lemma subst_cv_v_flip[simp]:
fixes c::c
assumes "atom x ♯ c"
shows "((x ↔ z) ∙ c)[x::=v]⇩c⇩v = c [z::=v]⇩c⇩v"
using assms subst_v_c_def by auto

lemma subst_cv_commute_full:
fixes c::c
assumes "atom z ♯ v" and "atom x ♯ w" and "x≠z"
shows "(c[z::=w]⇩c⇩v)[x::=v]⇩c⇩v = (c[x::=v]⇩c⇩v)[z::=w]⇩c⇩v"
using assms proof(nominal_induct c rule: c.strong_induct)
case (C_eq e1 e2)
then show ?case using subst_cev_commute_full by simp
qed(force+)

lemma subst_cv_eq[simp]:
assumes  "atom z1 ♯ e1"
shows "(CE_val (V_var z1)  ==  e1 )[z1::=[x]⇧v]⇩c⇩v = (CE_val (V_var x)  ==  e1 )" (is "?A = ?B")
proof -
have "?A = (((CE_val (V_var z1))[z1::=[x]⇧v]⇩c⇩e⇩v) == e1)" using subst_cv.simps assms by simp
thus ?thesis by simp
qed

section ‹Variable Context›

text ‹The idea of this substitution is to remove x from the context. We really want to add the condition
that x is fresh in v but this causes problems with proofs.›

nominal_function subst_gv :: "Γ ⇒ x ⇒ v  ⇒ Γ" where
"subst_gv GNil  x v = GNil"
| "subst_gv ((y,b,c) #⇩Γ Γ) x v  = (if x = y then Γ else ((y,b,c[x::=v]⇩c⇩v)#⇩Γ (subst_gv  Γ x v )))"
proof(goal_cases)
case 1
then show ?case  by(simp add: eqvt_def subst_gv_graph_aux_def )
next
case (3 P x)
then show ?case by (metis neq_GNil_conv prod_cases3)
qed(fast+)
nominal_termination (eqvt) by lexicographic_order

abbreviation
subst_gv_abbrev :: "Γ ⇒ x ⇒ v ⇒ Γ" ("_[_::=_]⇩Γ⇩v" [1000,50,50] 1000)
where
"g[x::=v]⇩Γ⇩v  ≡ subst_gv g x v"

lemma size_subst_gv [simp]: "size ( subst_gv G i x ) ≤ size G"
by (induct G,auto)

lemma forget_subst_gv [simp]: "atom a ♯ G ⟹ subst_gv G a x = G"
apply (induct G ,auto)
using fresh_GCons fresh_PairD(1) not_self_fresh apply blast
done

lemma fresh_subst_gv: "atom a ♯ G ⟹ atom a ♯ v ⟹ atom a ♯ subst_gv G x v"
proof(induct G)
case GNil
then show ?case by auto
next
case (GCons xbc G)
obtain x' and b' and c' where xbc: "xbc = (x',b',c')" using prod_cases3 by blast
show ?case proof(cases "x=x'")
case True
have "atom a ♯ G" using GCons fresh_GCons by blast
thus ?thesis using subst_gv.simps(2)[of  x' b' c' G] GCons xbc True by presburger
next
case False
then show ?thesis using subst_gv.simps(2)[of  x' b' c' G] GCons xbc False fresh_GCons by simp
qed
qed

lemma subst_gv_flip:
fixes x::x and xa::x and z::x and c::c and b::b and Γ::Γ
assumes "atom xa ♯ ((x, b, c[z::=[x]⇧v]⇩c⇩v) #⇩Γ Γ)"  and "atom xa ♯ Γ" and "atom x ♯ Γ" and "atom x ♯ (z, c)" and "atom xa ♯ (z, c)"
shows "(x ↔ xa) ∙  ((x, b, c[z::=[x]⇧v]⇩c⇩v) #⇩Γ Γ) = (xa, b, c[z::=V_var xa]⇩c⇩v) #⇩Γ Γ"
proof -
have  "(x ↔ xa) ∙  ((x, b, c[z::=[x]⇧v]⇩c⇩v) #⇩Γ Γ) =  (( (x ↔ xa) ∙  x, b, (x ↔ xa) ∙  c[z::=[x]⇧v]⇩c⇩v) #⇩Γ ((x ↔ xa) ∙  Γ))"
using subst Cons_eqvt flip_fresh_fresh using G_cons_flip by simp
also have "... = ((xa, b, (x ↔ xa) ∙ c[z::=[x]⇧v]⇩c⇩v) #⇩Γ ((x ↔ xa) ∙  Γ))" using assms by fastforce
also have "... =  ((xa, b,  c[z::=V_var xa]⇩c⇩v) #⇩Γ ((x ↔ xa) ∙  Γ))" using assms subst_cv_var_flip by fastforce
also have "... =  ((xa, b,  c[z::=V_var xa]⇩c⇩v) #⇩Γ Γ)"  using assms flip_fresh_fresh by blast
finally show ?thesis by simp
qed

section ‹Types›

nominal_function subst_tv :: "τ ⇒ x ⇒ v ⇒ τ" where
"atom z ♯ (x,v) ⟹ subst_tv  ⦃ z : b | c ⦄ x v  = ⦃ z : b | c[x::=v]⇩c⇩v ⦄"
apply (simp add: eqvt_def subst_tv_graph_aux_def )
apply auto
subgoal for P a aa b
apply(rule_tac y=a and c="(aa,b)" in τ.strong_exhaust)
by (auto simp: eqvt_at_def fresh_star_def fresh_Pair fresh_at_base)
apply (auto simp: eqvt_at_def fresh_star_def fresh_Pair fresh_at_base)
proof -
fix z :: x and c :: c and za :: x and xa :: x and va :: v and ca :: c and cb :: x
assume a1: "atom za ♯ va"  and  a2: "atom z ♯ va" and a3: "∀cb. atom cb ♯ c ∧ atom cb ♯ ca ⟶ cb ≠ z ∧ cb ≠ za ⟶ c[z::=V_var cb]⇩c⇩v = ca[za::=V_var cb]⇩c⇩v"
assume a4: "atom cb ♯ c" and a5: "atom cb ♯ ca" and a6: "cb ≠ z" and a7: "cb ≠ za" and "atom cb ♯ va" and a8: "za ≠ xa" and a9: "z ≠ xa"
assume a10:"cb ≠ xa"
note assms = a10 a9 a8 a7 a6 a5 a4 a3 a2 a1

have "c[z::=V_var cb]⇩c⇩v = ca[za::=V_var cb]⇩c⇩v" using assms  by auto
hence "c[z::=V_var cb]⇩c⇩v[xa::=va]⇩c⇩v = ca[za::=V_var cb]⇩c⇩v[xa::=va]⇩c⇩v" by simp
moreover have "c[z::=V_var cb]⇩c⇩v[xa::=va]⇩c⇩v = c[xa::=va]⇩c⇩v[z::=V_var cb]⇩c⇩v" using   subst_cv_commute_full[of z va xa "V_var cb" ]  assms fresh_def v.supp by fastforce
moreover  have "ca[za::=V_var cb]⇩c⇩v[xa::=va]⇩c⇩v = ca[xa::=va]⇩c⇩v[za::=V_var cb]⇩c⇩v"
using   subst_cv_commute_full[of za va xa "V_var cb" ]  assms fresh_def v.supp by fastforce

ultimately show "c[xa::=va]⇩c⇩v[z::=V_var cb]⇩c⇩v = ca[xa::=va]⇩c⇩v[za::=V_var cb]⇩c⇩v" by simp
qed

nominal_termination (eqvt) by lexicographic_order

abbreviation
subst_tv_abbrev :: "τ ⇒ x ⇒ v ⇒ τ" ("_[_::=_]⇩τ⇩v" [1000,50,50] 1000)
where
"t[x::=v]⇩τ⇩v  ≡ subst_tv t x v"

lemma size_subst_tv [simp]: "size ( subst_tv A i x ) = size A"
proof (nominal_induct A avoiding: i x  rule: τ.strong_induct)
case (T_refined_type x' b' c')
then show ?case by auto
qed

lemma forget_subst_tv [simp]: "atom a ♯ A ⟹ subst_tv A a x  = A"
apply (nominal_induct A avoiding: a x rule: τ.strong_induct)
apply(auto simp: fresh_at_base)
done

lemma subst_tv_id [simp]: "subst_tv A a (V_var a) = A"
by (nominal_induct A avoiding: a rule: τ.strong_induct) (auto simp: fresh_at_base)

lemma fresh_subst_tv_if [simp]:
"j ♯ (subst_tv A i x ) ⟷ (atom i ♯ A ∧ j ♯ A) ∨ (j ♯ x ∧ (j ♯ A ∨ j = atom i))"
apply (nominal_induct A avoiding: i x rule: τ.strong_induct)
using fresh_def supp_b_empty x_fresh_b by auto

lemma subst_tv_commute [simp]:
"atom y ♯ τ ⟹ (τ[x::= t]⇩τ⇩v)[y::=v]⇩τ⇩v = τ[x::= t[y::=v]⇩v⇩v]⇩τ⇩v "
by (nominal_induct τ avoiding: x y t v rule: τ.strong_induct) (auto simp: fresh_at_base)

lemma subst_tv_var_flip [simp]:
fixes x::x and xa::x and τ::τ
assumes "atom xa ♯ τ"
shows "(x ↔ xa) ∙ τ = τ[x::=V_var xa]⇩τ⇩v"
proof -
obtain z::x and b and c where zbc: "atom z ♯ (x,xa, V_var xa) ∧ τ = ⦃ z : b | c ⦄"
using obtain_fresh_z   by (metis prod.inject subst_tv.cases)
hence "atom xa ∉ supp c - { atom z }" using τ.supp[of z b c] fresh_def supp_b_empty assms
by  auto
moreover have "xa ≠ z" using zbc fresh_prod3 by force
ultimately have xaf: "atom xa ♯ c" using fresh_def by auto
have "(x ↔ xa) ∙ τ = ⦃ z : b | (x ↔ xa) ∙ c ⦄"
by (metis τ.perm_simps empty_iff flip_at_base_simps(3) flip_fresh_fresh fresh_PairD(1) fresh_PairD(2) fresh_def not_self_fresh supp_b_empty v.fresh(2) zbc)
also have "... =  ⦃ z : b | c[x::=V_var xa]⇩c⇩v ⦄"  using subst_cv_v_flip xaf
by (metis permute_flip_cancel permute_flip_cancel2 subst_cv_var_flip)
finally show ?thesis using subst_tv.simps zbc
using fresh_PairD(1) not_self_fresh by force
qed

instantiation τ :: has_subst_v
begin

definition
"subst_v = subst_tv"

instance proof
fix j::atom and i::x and  x::v and t::τ
show  "(j ♯ subst_v t i x) = ((atom i ♯ t ∧ j ♯ t) ∨ (j ♯ x ∧ (j ♯ t ∨ j = atom i)))"

proof(nominal_induct t avoiding: i x rule:τ.strong_induct)
case (T_refined_type z b c)
hence " j ♯ ⦃ z : b  | c ⦄[i::=x]⇩v  =  j ♯ ⦃ z : b  | c[i::=x]⇩c⇩v ⦄" using subst_tv.simps subst_v_τ_def fresh_Pair by simp
also have "...  = (atom i ♯ ⦃ z : b  | c ⦄ ∧ j ♯ ⦃ z : b  | c ⦄ ∨ j ♯ x ∧ (j ♯ ⦃ z : b  | c ⦄ ∨ j = atom i))"
unfolding τ.fresh using subst_v_c_def fresh_subst_v_if
using T_refined_type.hyps(1) T_refined_type.hyps(2) x_fresh_b by auto
finally show ?case by auto
qed

fix a::x and tm::τ and x::v
show "atom a ♯ tm ⟹ subst_v tm a x  = tm"
apply(nominal_induct tm avoiding: a x rule:τ.strong_induct)
using subst_v_c_def forget_subst_v subst_tv.simps subst_v_τ_def fresh_Pair by simp

fix a::x and tm::τ
show "subst_v tm a (V_var a) = tm"
apply(nominal_induct tm avoiding: a rule:τ.strong_induct)
using subst_v_c_def forget_subst_v subst_tv.simps subst_v_τ_def fresh_Pair by simp

fix p::perm and x1::x and v::v and t1::τ
show "p ∙ subst_v t1 x1 v  = subst_v  (p ∙ t1) (p ∙ x1) (p ∙ v)"
apply(nominal_induct tm avoiding: a x rule:τ.strong_induct)
using subst_v_c_def forget_subst_v subst_tv.simps subst_v_τ_def fresh_Pair by simp

fix x::x and c::τ and z::x
show "atom x ♯ c ⟹ ((x ↔ z) ∙ c) = c[z::=[x]⇧v]⇩v"
apply(nominal_induct c avoiding: z x rule:τ.strong_induct)
using subst_v_c_def flip_subst_v subst_tv.simps subst_v_τ_def fresh_Pair by auto

fix x::x and c::τ and z::x
show  "atom x ♯ c ⟹ c[z::=[x]⇧v]⇩v[x::=v]⇩v = c[z::=v]⇩v"
apply(nominal_induct c avoiding:  x v z rule:τ.strong_induct)
using subst_v_c_def  subst_tv.simps subst_v_τ_def fresh_Pair
by (metis flip_commute subst_tv_commute subst_tv_var_flip subst_v_τ_def subst_vv.simps(2))
qed

end

lemma subst_tv_commute_full:
fixes c::τ
assumes "atom z ♯ v" and "atom x ♯ w" and "x≠z"
shows "(c[z::=w]⇩τ⇩v)[x::=v]⇩τ⇩v = (c[x::=v]⇩τ⇩v)[z::=w]⇩τ⇩v"
using assms proof(nominal_induct c avoiding: x v z w rule: τ.strong_induct)
case (T_refined_type x1a x2a x3a)
then show ?case using subst_cv_commute_full by simp
qed

lemma type_eq_subst_eq:
fixes v::v and c1::c
assumes "⦃ z1 : b1  |  c1 ⦄ = ⦃ z2 : b2  |  c2 ⦄"
shows "c1[z1::=v]⇩c⇩v = c2[z2::=v]⇩c⇩v"
using subst_v_flip_eq_two[of z1 c1 z2 c2 v] τ.eq_iff assms subst_v_c_def by simp

text ‹Extract constraint from a type. We cannot just project out the constraint as this would
mean alpha-equivalent types give different answers ›

nominal_function c_of :: "τ ⇒ x ⇒ c" where
"atom z ♯ x ⟹ c_of (T_refined_type z b c) x = c[z::=[x]⇧v]⇩c⇩v"
proof(goal_cases)
case 1
then show ?case using eqvt_def c_of_graph_aux_def by force
next
case (2 x y)
then show ?case using eqvt_def c_of_graph_aux_def by force
next
case (3 P x)
then obtain x1::τ and x2::x where *:"x = (x1,x2)" by force
obtain z' and b' and c' where "x1 = ⦃ z' : b' | c' ⦄ ∧ atom z' ♯ x2" using obtain_fresh_z by metis
then show ?case  using 3 * by auto
next
case (4 z1 x1 b1 c1 z2 x2 b2 c2)
then show ?case using subst_v_flip_eq_two τ.eq_iff   by (metis prod.inject type_eq_subst_eq)
qed

nominal_termination (eqvt) by lexicographic_order

lemma c_of_eq:
shows  "c_of ⦃ x : b | c ⦄ x = c"
proof(nominal_induct "⦃ x : b | c ⦄" avoiding: x rule: τ.strong_induct)
case (T_refined_type x' c')
moreover hence "c_of ⦃ x' : b | c' ⦄ x = c'[x'::=V_var x]⇩c⇩v" using c_of.simps by auto
moreover have "⦃ x' : b  | c' ⦄ = ⦃ x : b  | c ⦄" using T_refined_type  τ.eq_iff by metis
moreover have "c'[x'::=V_var x]⇩c⇩v = c" using  T_refined_type Abs1_eq_iff flip_subst_v subst_v_c_def
by (metis subst_cv_id)
ultimately show ?case by auto
qed

lemma obtain_fresh_z_c_of:
fixes t::"'b::fs"
obtains z  where "atom z ♯ t ∧ τ = ⦃ z : b_of τ | c_of τ z ⦄"
proof -
obtain z and c where "atom z ♯ t ∧ τ = ⦃ z : b_of τ | c ⦄" using obtain_fresh_z2 by metis
moreover hence "c = c_of τ z" using c_of.simps using c_of_eq by metis
ultimately show ?thesis
using that by auto
qed

lemma c_of_fresh:
fixes x::x
assumes  "atom x ♯ (t,z)"
shows "atom x ♯ c_of t z"
proof -
obtain z' and c' where z:"t = ⦃ z' : b_of t | c' ⦄ ∧ atom z' ♯ (x,z)" using obtain_fresh_z_c_of by metis
hence *:"c_of t z = c'[z'::=V_var z]⇩c⇩v" using c_of.simps fresh_Pair by metis
have "(atom x ♯ c' ∨ atom x ∈ set [atom z']) ∧ atom x ♯ b_of t" using τ.fresh assms z fresh_Pair by metis
hence "atom x ♯ c'" using fresh_Pair z fresh_at_base(2) by fastforce
moreover have "atom x ♯ V_var z" using assms fresh_Pair v.fresh by metis
ultimately show ?thesis using assms fresh_subst_v_if[of "atom x" c' z' "V_var z"] subst_v_c_def * by metis
qed

lemma c_of_switch:
fixes z::x
assumes "atom z ♯ t"
shows "(c_of t z)[z::=V_var x]⇩c⇩v = c_of t x"
proof -
obtain z' and c' where z:"t = ⦃ z' : b_of t | c' ⦄ ∧ atom z' ♯ (x,z)" using obtain_fresh_z_c_of by metis
hence "(atom z ♯ c' ∨ atom z ∈ set [atom z']) ∧ atom z ♯ b_of t" using τ.fresh[of "atom z" z' "b_of t" c'] assms by metis
moreover have " atom z ∉ set [atom z']" using z fresh_Pair by force
ultimately have  **:"atom z ♯ c'" using fresh_Pair z fresh_at_base(2) by metis

have "(c_of t z)[z::=V_var x]⇩c⇩v = c'[z'::=V_var z]⇩c⇩v[z::=V_var x]⇩c⇩v"  using c_of.simps fresh_Pair  z by metis
also have "... = c'[z'::=V_var x]⇩c⇩v"  using subst_v_simple_commute subst_v_c_def assms c_of.simps z  ** by metis
finally show ?thesis using c_of.simps[of z' x "b_of t" c']  fresh_Pair z by metis
qed

lemma type_eq_subst_eq1:
fixes v::v and c1::c
assumes "⦃ z1 : b1  |  c1 ⦄ = (⦃ z2 : b2  |  c2 ⦄)" and "atom z1 ♯ c2"
shows "c1[z1::=v]⇩c⇩v = c2[z2::=v]⇩c⇩v" and "b1=b2" and " c1 = (z1 ↔ z2) ∙ c2"
proof -
show "c1[z1::=v]⇩c⇩v = c2[z2::=v]⇩c⇩v" using type_eq_subst_eq assms by blast
show "b1=b2" using τ.eq_iff assms by blast
have "z1 = z2 ∧ c1 = c2 ∨ z1 ≠ z2 ∧ c1 = (z1 ↔ z2) ∙ c2 ∧ atom z1 ♯ c2"
using τ.eq_iff Abs1_eq_iff[of z1 c1 z2 c2] assms by blast
thus  "c1 = (z1 ↔ z2) ∙ c2" by auto
qed

lemma type_eq_subst_eq2:
fixes v::v and c1::c
assumes "⦃ z1 : b1  |  c1 ⦄ = (⦃ z2 : b2  |  c2 ⦄)"
shows "c1[z1::=v]⇩c⇩v = c2[z2::=v]⇩c⇩v" and "b1=b2" and "[[atom z1]]lst. c1 = [[atom z2]]lst. c2"
proof -
show "c1[z1::=v]⇩c⇩v = c2[z2::=v]⇩c⇩v" using type_eq_subst_eq assms by blast
show "b1=b2" using τ.eq_iff assms by blast
show  "[[atom z1]]lst. c1 = [[atom z2]]lst. c2"
using τ.eq_iff assms by auto
qed

lemma type_eq_subst_eq3:
fixes v::v and c1::c
assumes "⦃ z1 : b1  |  c1 ⦄ = (⦃ z2 : b2  |  c2 ⦄)" and "atom z1 ♯ c2"
shows "c1 = c2[z2::=V_var z1]⇩c⇩v" and "b1=b2"
using type_eq_subst_eq1 assms  subst_v_c_def
by (metis subst_cv_var_flip)+

lemma type_eq_flip:
assumes "atom x ♯ c"
shows "⦃ z : b  | c ⦄ = ⦃ x : b | (x ↔ z ) ∙ c ⦄"
using τ.eq_iff Abs1_eq_iff assms
by (metis (no_types, lifting) flip_fresh_fresh)

lemma c_of_true:
"c_of ⦃ z' : B_bool  | TRUE ⦄ x = C_true"
proof(nominal_induct "⦃ z' : B_bool  | TRUE ⦄" avoiding: x rule:τ.strong_induct)
case (T_refined_type x1a x3a)
hence "⦃ z' : B_bool  | TRUE ⦄ = ⦃ x1a : B_bool  | x3a ⦄" using τ.eq_iff by metis
then show ?case using subst_cv.simps c_of.simps T_refined_type
type_eq_subst_eq3
by (metis type_eq_subst_eq)
qed

lemma type_eq_subst:
assumes "atom x ♯ c"
shows "⦃ z : b  | c ⦄ = ⦃ x : b | c[z::=[x]⇧v]⇩c⇩v ⦄"
using τ.eq_iff Abs1_eq_iff assms
using subst_cv_var_flip type_eq_flip by auto

lemma type_e_subst_fresh:
fixes x::x and z::x
assumes "atom z ♯ (x,v)" and "atom x ♯ e"
shows "⦃ z : b  | CE_val (V_var z)  ==  e  ⦄[x::=v]⇩τ⇩v = ⦃ z : b  | CE_val (V_var z)  ==  e  ⦄"
using assms subst_tv.simps subst_cv.simps forget_subst_cev by simp

lemma type_v_subst_fresh:
fixes x::x and z::x
assumes "atom z ♯ (x,v)" and "atom x ♯ v'"
shows "⦃ z : b  | CE_val (V_var z)  ==  CE_val v'  ⦄[x::=v]⇩τ⇩v = ⦃ z : b  | CE_val (V_var z)  ==  CE_val v'  ⦄"
using assms subst_tv.simps subst_cv.simps  by simp

lemma subst_tbase_eq:
"b_of τ = b_of τ[x::=v]⇩τ⇩v"
proof -
obtain z and b and c where zbc: "τ = ⦃ z:b|c⦄ ∧ atom z ♯ (x,v)" using τ.exhaust
by (metis prod.inject subst_tv.cases)
hence "b_of ⦃ z:b|c⦄ = b_of ⦃ z:b|c⦄[x::=v]⇩τ⇩v" using subst_tv.simps by simp
thus ?thesis using zbc by blast
qed

lemma subst_tv_if:
assumes "atom z1 ♯ (x,v)" and "atom z' ♯ (x,v)"
shows "⦃ z1 : b  | CE_val (v'[x::=v]⇩v⇩v)  ==  CE_val (V_lit l)   IMP  (c'[x::=v]⇩c⇩v)[z'::=[z1]⇧v]⇩c⇩v  ⦄ =
⦃ z1 : b  | CE_val v'           ==  CE_val (V_lit l)   IMP  c'[z'::=[z1]⇧v]⇩c⇩v  ⦄[x::=v]⇩τ⇩v"
using subst_cv_commute_full[of z' v x "V_var z1" c']  subst_tv.simps subst_vv.simps(1) subst_ev.simps  subst_cv.simps assms
by simp

lemma subst_tv_tid:
assumes "atom za ♯ (x,v)"
shows "⦃ za : B_id tid  | TRUE ⦄ = ⦃ za : B_id tid   | TRUE ⦄[x::=v]⇩τ⇩v"
using assms subst_tv.simps subst_cv.simps by presburger

lemma b_of_subst:
"b_of (τ[x::=v]⇩τ⇩v) = b_of τ"
proof -
obtain z b c where *:"τ = ⦃ z : b | c ⦄ ∧ atom z ♯ (x,v)" using obtain_fresh_z by metis
thus ?thesis  using subst_tv.simps * by auto
qed

lemma subst_tv_flip:
assumes "τ'[x::=v]⇩τ⇩v = τ" and "atom x ♯ (v,τ)" and "atom x' ♯ (v,τ)"
shows "((x' ↔ x) ∙ τ')[x'::=v]⇩τ⇩v = τ"
proof -
have "(x' ↔ x) ∙ v = v ∧ (x' ↔ x) ∙ τ = τ" using assms flip_fresh_fresh by auto
thus ?thesis using subst_tv.eqvt[of  "(x' ↔ x)"  τ' x v ] assms by auto
qed

lemma subst_cv_true:
"⦃ z : B_id tid  | TRUE ⦄ = ⦃ z : B_id tid  | TRUE ⦄[x::=v]⇩τ⇩v"
proof -
obtain za::x where "atom za ♯ (x,v)" using obtain_fresh by auto
hence "⦃ z : B_id tid   | TRUE ⦄ = ⦃ za: B_id tid | TRUE ⦄" using τ.eq_iff Abs1_eq_iff by fastforce
moreover have  "⦃ za : B_id tid   | TRUE ⦄ = ⦃ za : B_id tid   | TRUE ⦄[x::=v]⇩τ⇩v"
using subst_cv.simps subst_tv.simps  by (simp add: ‹atom za ♯ (x, v)›)
ultimately show ?thesis by argo
qed

lemma t_eq_supp:
assumes "(⦃ z : b | c ⦄) = (⦃  z1 : b1 | c1 ⦄)"
shows "supp c - { atom z } = supp c1 - { atom z1 }"
proof -
have "supp c - { atom z } ∪ supp b = supp c1 - { atom z1 } ∪ supp b1" using τ.supp assms
by (metis list.set(1) list.simps(15) sup_bot.right_neutral supp_b_empty)
moreover have "supp b = supp b1" using assms  τ.eq_iff by simp
moreover have "atom z1 ∉ supp b1 ∧ atom z ∉ supp b" using  supp_b_empty by simp
ultimately show ?thesis
by (metis τ.eq_iff τ.supp assms b.supp(1) list.set(1) list.set(2) sup_bot.right_neutral)
qed

lemma fresh_t_eq:
fixes x::x
assumes  "(⦃ z : b  | c ⦄) = (⦃ zz : b | cc ⦄)" and "atom x ♯ c" and "x ≠ zz"
shows "atom x ♯ cc"
proof -
have "supp c - { atom z } ∪ supp b = supp cc - { atom zz } ∪ supp b" using τ.supp assms
by (metis list.set(1) list.simps(15) sup_bot.right_neutral supp_b_empty)
moreover have "atom x ∉ supp c" using assms fresh_def by blast
ultimately have "atom x ∉ supp cc - { atom zz } ∪ supp b" by force
hence "atom x ∉ supp cc" using assms by simp
thus ?thesis using fresh_def by auto
qed

section ‹Mutable Variable Context›

nominal_function subst_dv :: "Δ ⇒ x ⇒ v ⇒ Δ" where
"subst_dv  DNil x v = DNil"
| "subst_dv ((u,t) #⇩Δ Δ) x v  = ((u,t[x::=v]⇩τ⇩v) #⇩Δ (subst_dv Δ x v ))"
apply (simp add: eqvt_def subst_dv_graph_aux_def,auto )
using delete_aux.elims by (metis Δ.exhaust surj_pair)
nominal_termination (eqvt) by lexicographic_order

abbreviation
subst_dv_abbrev :: "Δ ⇒ x ⇒ v ⇒ Δ" ("_[_::=_]⇩Δ⇩v" [1000,50,50] 1000)
where
"Δ[x::=v]⇩Δ⇩v  ≡ subst_dv Δ x v "

nominal_function dmap :: "(u*τ ⇒ u*τ) ⇒ Δ ⇒ Δ" where
"dmap f DNil  = DNil"
| "dmap  f ((u,t)#⇩ΔΔ)  = (f (u,t) #⇩Δ (dmap f Δ ))"
apply (simp add: eqvt_def dmap_graph_aux_def,auto )
using delete_aux.elims by (metis Δ.exhaust surj_pair)
nominal_termination (eqvt) by lexicographic_order

lemma subst_dv_iff:
"Δ[x::=v]⇩Δ⇩v = dmap (λ(u,t). (u, t[x::=v]⇩τ⇩v)) Δ"
by(induct Δ, auto)

lemma size_subst_dv [simp]: "size ( subst_dv G i x) ≤ size G"
by (induct G,auto)

lemma forget_subst_dv [simp]: "atom a ♯ G ⟹ subst_dv G a x = G"
apply (induct G ,auto)
using fresh_DCons fresh_PairD(1) not_self_fresh apply fastforce
done

lemma subst_dv_member:
assumes "(u,τ) ∈ setD Δ"
shows  "(u, τ[x::=v]⇩τ⇩v) ∈ setD (Δ[x::=v]⇩Δ⇩v)"
using assms  by(induct Δ rule: Δ_induct,auto)

lemma fresh_subst_dv:
fixes x::x
assumes "atom xa ♯ Δ" and "atom xa ♯ v"
shows "atom xa ♯Δ[x::=v]⇩Δ⇩v"
using assms proof(induct Δ rule:Δ_induct)
case DNil
then show ?case by auto
next
case (DCons u t  Δ)
then show ?case using subst_dv.simps  subst_v_τ_def fresh_DCons fresh_Pair by simp
qed

lemma fresh_subst_dv_if:
fixes j::atom and i::x and  x::v and t::Δ
assumes "j ♯ t ∧ j ♯ x"
shows  "(j ♯ subst_dv t i x)"
using assms proof(induct t rule: Δ_induct)
case DNil
then show ?case using subst_gv.simps fresh_GNil by auto
next
case (DCons u' t'  D')
then show ?case unfolding subst_dv.simps using fresh_DCons fresh_subst_tv_if fresh_Pair by metis
qed

section ‹Statements›

text ‹ Using ideas from proofs at top of AFP/Launchbury/Substitution.thy.
Subproofs borrowed from there; hence the apply style proofs. ›

nominal_function (default "case_sum (λx. Inl undefined) (case_sum (λx. Inl undefined) (λx. Inr undefined))")
subst_sv :: "s ⇒ x ⇒ v  ⇒ s"
and subst_branchv :: "branch_s ⇒ x ⇒ v  ⇒ branch_s"
and subst_branchlv :: "branch_list ⇒ x ⇒ v ⇒ branch_list" where
"subst_sv ( (AS_val v') ) x v = (AS_val (subst_vv v' x v  ))"
| "atom y ♯ (x,v) ⟹ subst_sv  (AS_let y  e s) x v = (AS_let y  (e[x::=v]⇩e⇩v) (subst_sv s x v ))"
| "atom y ♯ (x,v) ⟹ subst_sv (AS_let2 y t s1 s2) x v = (AS_let2 y (t[x::=v]⇩τ⇩v) (subst_sv s1 x v ) (subst_sv s2 x v ))"
| " subst_sv (AS_match v'  cs) x v = AS_match  (v'[x::=v]⇩v⇩v)  (subst_branchlv cs x v )"
| "subst_sv (AS_assign y v') x v = AS_assign y (subst_vv v' x v )"
| "subst_sv ( (AS_if v' s1 s2) ) x v = (AS_if (subst_vv v' x v ) (subst_sv s1 x v ) (subst_sv s2 x v ) )"
| "atom u ♯ (x,v) ⟹ subst_sv (AS_var u τ v' s) x v = AS_var u (subst_tv τ x v ) (subst_vv v' x v ) (subst_sv s x v ) "
| "subst_sv (AS_while s1 s2) x v = AS_while (subst_sv s1 x v ) (subst_sv s2 x v )"
| "subst_sv (AS_seq s1 s2) x v = AS_seq (subst_sv s1 x v ) (subst_sv s2 x v )"
| "subst_sv (AS_assert c s) x v = AS_assert (subst_cv c x v) (subst_sv s x v)"
| "atom x1 ♯ (x,v) ⟹  subst_branchv (AS_branch dc x1 s1 ) x v  = AS_branch dc x1 (subst_sv s1 x v )"

| "subst_branchlv (AS_final cs) x v = AS_final (subst_branchv  cs x v )"
| "subst_branchlv (AS_cons cs css) x v = AS_cons (subst_branchv cs x v ) (subst_branchlv css x v )"
apply (auto,simp add: eqvt_def subst_sv_subst_branchv_subst_branchlv_graph_aux_def )
proof(goal_cases)

have eqvt_at_proj: "⋀ s xa va . eqvt_at subst_sv_subst_branchv_subst_branchlv_sumC (Inl (s, xa, va)) ⟹
eqvt_at (λa. projl (subst_sv_subst_branchv_subst_branchlv_sumC (Inl a))) (s, xa, va)"
apply(rule)
apply(subst Projl_permute)
apply(thin_tac _)+
apply (case_tac "Ex1 (subst_sv_subst_branchv_subst_branchlv_graph (Inl (s,xa,va)))")
apply simp
apply(auto)[1]
apply (erule_tac x="x" in allE)
apply simp
apply(cases rule: subst_sv_subst_branchv_subst_branchlv_graph.cases)
apply(assumption)
apply(rule_tac x="Sum_Type.projl x" in exI,clarify,rule the1_equality,blast,simp (no_asm) only: sum.sel)+
apply blast +

apply(simp)+
done

{
case (1 P x')
then show ?case proof(cases x')
case (Inl a) thus P
proof(cases a)
case (fields aa bb cc)
thus P using Inl 1 s_branch_s_branch_list.strong_exhaust fresh_star_insert by metis
qed
next
case (Inr b) thus P
proof(cases b)
case (Inl a) thus P proof(cases a)
case (fields aa bb cc)
then show ?thesis  using Inr Inl 1 s_branch_s_branch_list.strong_exhaust fresh_star_insert by metis
qed
next
case Inr2: (Inr b) thus P proof(cases b)
case (fields aa bb cc)
then show ?thesis  using Inr Inr2 1 s_branch_s_branch_list.strong_exhaust fresh_star_insert by metis
qed
qed
qed
next
case (2 y s ya xa va sa c)
thus ?case using eqvt_triple eqvt_at_proj by blast
next
case (3 y s2 ya xa va s1a s2a c)
thus ?case using eqvt_triple eqvt_at_proj by blast
next
case (4 u xa va s ua sa c)
moreover have "atom u ♯ (xa, va) ∧ atom ua ♯ (xa, va)"
using fresh_Pair u_fresh_xv by auto
ultimately show ?case using eqvt_triple[of u xa va ua s sa]  subst_sv_def eqvt_at_proj by metis
next
case (5 x1 s1 x1a xa va s1a c)
thus ?case using eqvt_triple eqvt_at_proj by blast
}
qed
nominal_termination (eqvt) by lexicographic_order

abbreviation
subst_sv_abbrev :: "s ⇒ x ⇒ v ⇒ s" ("_[_::=_]⇩s⇩v" [1000,50,50] 1000)
where
"s[x::=v]⇩s⇩v  ≡ subst_sv s x v"

abbreviation
subst_branchv_abbrev :: "branch_s ⇒ x ⇒ v ⇒ branch_s" ("_[_::=_]⇩s⇩v" [1000,50,50] 1000)
where
"s[x::=v]⇩s⇩v  ≡ subst_branchv s x v"

lemma size_subst_sv [simp]:  "size (subst_sv A i x ) = size A" and  "size (subst_branchv B i x ) = size B"  and  "size (subst_branchlv C i x ) = size C"
by(nominal_induct A and B and C avoiding: i x rule: s_branch_s_branch_list.strong_induct,auto)

lemma forget_subst_sv [simp]: shows  "atom a ♯ A ⟹ subst_sv A a x = A" and "atom a ♯ B ⟹ subst_branchv B a x = B" and "atom a ♯ C ⟹ subst_branchlv C a x  = C"
by (nominal_induct A and B and C avoiding: a x rule: s_branch_s_branch_list.strong_induct,auto simp: fresh_at_base)

lemma subst_sv_id [simp]: "subst_sv A a (V_var a) = A" and "subst_branchv B a (V_var a) = B" and  "subst_branchlv C a (V_var a)  = C"
proof(nominal_induct A and B and C avoiding: a  rule: s_branch_s_branch_list.strong_induct)
case (AS_let x option e s)
then show ?case
by (metis (no_types, lifting) fresh_Pair not_None_eq subst_ev_id subst_sv.simps(2) subst_sv.simps(3) subst_tv_id v.fresh(2))
next
case (AS_match v branch_s)
then show ?case using fresh_Pair not_None_eq subst_ev_id subst_sv.simps subst_sv.simps subst_tv_id v.fresh subst_vv_id
by metis
qed(auto)+

lemma fresh_subst_sv_if_rl:
shows
"(atom x ♯ s ∧ j ♯ s) ∨ (j ♯ v ∧ (j ♯ s ∨ j = atom x)) ⟹ j ♯ (subst_sv s x v )" and
"(atom x ♯ cs ∧ j ♯ cs) ∨ (j ♯ v ∧ (j ♯ cs ∨ j = atom x)) ⟹ j ♯ (subst_branchv cs x v)" and
"(atom x ♯ css ∧ j ♯ css) ∨ (j ♯ v ∧ (j ♯ css ∨ j = atom x)) ⟹ j ♯ (subst_branchlv css x v )"
apply(nominal_induct s and cs and css avoiding: v x rule: s_branch_s_branch_list.strong_induct)
using pure_fresh by force+

lemma fresh_subst_sv_if_lr:
shows  "j ♯ (subst_sv s x v) ⟹ (atom x ♯ s ∧ j ♯ s) ∨ (j ♯ v ∧ (j ♯ s ∨ j = atom x))" and
"j ♯ (subst_branchv cs x v) ⟹ (atom x ♯ cs ∧ j ♯ cs) ∨ (j ♯ v ∧ (j ♯ cs ∨ j = atom x))" and
"j ♯ (subst_branchlv css x v ) ⟹ (atom x ♯ css ∧ j ♯ css) ∨ (j ♯ v ∧ (j ♯ css ∨ j = atom x))"
proof(nominal_induct s and cs and css avoiding: v x rule: s_branch_s_branch_list.strong_induct)
case (AS_branch list x s )
then show ?case using s_branch_s_branch_list.fresh fresh_Pair list.distinct(1) list.set_cases pure_fresh set_ConsD subst_branchv.simps by metis
next
case (AS_let y e s')
thus ?case proof(cases "atom x ♯  (AS_let y e s')")
case True
hence "subst_sv (AS_let y  e s') x v  =  (AS_let y e s')" using forget_subst_sv by simp
hence "j ♯  (AS_let y  e s')" using AS_let by argo
then show ?thesis using True by blast
next
case False
have "subst_sv (AS_let y  e s') x v  = AS_let y  (e[x::=v]⇩e⇩v) (s'[x::=v]⇩s⇩v)" using subst_sv.simps(2) AS_let by force
hence "((j ♯ s'[x::=v]⇩s⇩v ∨ j ∈ set [atom y]) ∧ j ♯ None ∧ j ♯ e[x::=v]⇩e⇩v)" using s_branch_s_branch_list.fresh AS_let
then show ?thesis using  AS_let  fresh_None fresh_subst_ev_if list.discI list.set_cases s_branch_s_branch_list.fresh set_ConsD
by metis
qed
next
case (AS_let2 y τ s1 s2)
thus ?case proof(cases "atom x ♯  (AS_let2 y τ s1 s2)")
case True
hence "subst_sv  (AS_let2 y τ s1 s2)  x v =  (AS_let2 y τ s1 s2)" using forget_subst_sv by simp
hence "j ♯  (AS_let2 y τ s1 s2)" using AS_let2 by argo
then show ?thesis using True by blast
next
case False
have "subst_sv (AS_let2 y τ s1 s2) x v  = AS_let2 y (τ[x::=v]⇩τ⇩v) (s1[x::=v]⇩s⇩v) (s2[x::=v]⇩s⇩v)" using subst_sv.simps AS_let2 by force
then show ?thesis using  AS_let2
fresh_subst_tv_if list.discI list.set_cases s_branch_s_branch_list.fresh(4) set_ConsD by auto
qed
qed(auto)+

lemma fresh_subst_sv_if[simp]:
fixes x::x and v::v
shows "j ♯ (subst_sv s x v) ⟷ (atom x ♯ s ∧ j ♯ s) ∨ (j ♯ v ∧ (j ♯ s ∨ j = atom x))" and
"j ♯ (subst_branchv cs x v) ⟷ (atom x ♯ cs ∧ j ♯ cs) ∨ (j ♯ v ∧ (j ♯ cs ∨ j = atom x))"
using fresh_subst_sv_if_lr fresh_subst_sv_if_rl by metis+

lemma subst_sv_commute [simp]:
fixes A::s and t::v and j::x and i::x
shows  "atom j ♯ A ⟹ (subst_sv (subst_sv A i t)  j u ) = subst_sv A i (subst_vv t j u )" and
"atom j ♯ B ⟹ (subst_branchv  (subst_branchv B i t ) j u ) = subst_branchv B i (subst_vv t j u )" and
"atom j ♯ C ⟹ (subst_branchlv  (subst_branchlv C i t) j u ) = subst_branchlv C i (subst_vv t j u   ) "
apply(nominal_induct A and B and C avoiding: i j t u rule: s_branch_s_branch_list.strong_induct)
by(auto simp: fresh_at_base)

lemma c_eq_perm:
assumes "( (atom z)  ⇌ (atom z') )  ∙ c = c'" and "atom z'  ♯ c"
shows "⦃ z : b | c ⦄ = ⦃ z' : b | c' ⦄"
using τ.eq_iff Abs1_eq_iff(3)
by (metis Nominal2_Base.swap_commute assms(1) assms(2) flip_def swap_fresh_fresh)

lemma subst_sv_flip:
fixes s::s and sa::s and v'::v
assumes "atom c ♯ (s, sa)" and "atom c ♯ (v',x, xa, s, sa)" "atom x ♯ v'" and "atom xa ♯ v'" and "(x ↔ c) ∙ s = (xa ↔ c) ∙ sa"
shows "s[x::=v']⇩s⇩v = sa[xa::=v']⇩s⇩v"
proof -
have "atom x ♯ (s[x::=v']⇩s⇩v)" and xafr: "atom xa ♯ (sa[xa::=v']⇩s⇩v)"
and  "atom c ♯ ( s[x::=v']⇩s⇩v, sa[xa::=v']⇩s⇩v)" using assms using  fresh_subst_sv_if assms  by( blast+ ,force)

hence "s[x::=v']⇩s⇩v = (x ↔ c) ∙ (s[x::=v']⇩s⇩v)"  by (simp add: flip_fresh_fresh fresh_Pair)
also have " ... = ((x ↔ c) ∙ s)[ ((x ↔ c) ∙ x) ::= ((x ↔ c) ∙ v') ]⇩s⇩v" using subst_sv_subst_branchv_subst_branchlv.eqvt  by blast
also have "... = ((xa ↔ c) ∙ sa)[ ((x ↔ c) ∙ x) ::= ((x ↔ c) ∙ v') ]⇩s⇩v" using assms by presburger
also have "... = ((xa ↔ c) ∙ sa)[ ((xa ↔ c) ∙ xa) ::= ((xa ↔ c) ∙ v') ]⇩s⇩v" using assms
by (metis flip_at_simps(1) flip_fresh_fresh fresh_PairD(1))
also have "... =  (xa ↔ c) ∙ (sa[xa::=v']⇩s⇩v)" using subst_sv_subst_branchv_subst_branchlv.eqvt  by presburger
also have "... = sa[xa::=v']⇩s⇩v" using xafr assms by (simp add: flip_fresh_fresh fresh_Pair)
finally show ?thesis by simp
qed

lemma if_type_eq:
fixes Γ::Γ and v::v and z1::x
assumes "atom z1' ♯ (v, ca, (x, b, c) #⇩Γ Γ,  (CE_val v  ==  CE_val (V_lit ll) IMP  ca[za::=[z1]⇧v]⇩c⇩v ))" and "atom z1 ♯ v"
and "atom z1 ♯ (za,ca)" and "atom z1' ♯ (za,ca)"
shows "(⦃ z1' : ba  | CE_val v  ==  CE_val (V_lit ll)   IMP  ca[za::=[z1']⇧v]⇩c⇩v  ⦄) = ⦃ z1 : ba  | CE_val v  ==  CE_val (V_lit ll) IMP  ca[za::=[z1]⇧v]⇩c⇩v  ⦄"
proof -
have "atom z1' ♯ (CE_val v  ==  CE_val (V_lit ll) IMP  ca[za::=[z1]⇧v]⇩c⇩v )" using assms fresh_prod4 by blast
moreover hence "(CE_val v  ==  CE_val (V_lit ll)   IMP  ca[za::=[z1']⇧v]⇩c⇩v) = (z1' ↔ z1) ∙ (CE_val v  ==  CE_val (V_lit ll)   IMP  ca[za::=[z1]⇧v]⇩c⇩v )"
proof -
have "(z1' ↔ z1) ∙ (CE_val v  ==  CE_val (V_lit ll)   IMP  ca[za::=[z1]⇧v]⇩c⇩v ) = ( (z1' ↔ z1) ∙ (CE_val v  ==  CE_val (V_lit ll)) IMP  ((z1' ↔ z1) ∙ ca[za::=[z1]⇧v]⇩c⇩v ))"
by auto
also have "... = ((CE_val v  ==  CE_val (V_lit ll))   IMP  ((z1' ↔ z1) ∙ ca[za::=[z1]⇧v]⇩c⇩v ))"
using ‹atom z1 ♯ v› assms
by (metis (mono_tags) ‹atom z1' ♯ (CE_val v == CE_val (V_lit ll) IMP ca[za::=[z1]⇧v]⇩c⇩v )› c.fresh(6) c.fresh(7) ce.fresh(1) flip_at_simps(2) flip_fresh_fresh fresh_at_base_permute_iff fresh_def supp_l_empty v.fresh(1))
also have "... =  ((CE_val v  ==  CE_val (V_lit ll))   IMP  (ca[za::=[z1']⇧v]⇩c⇩v ))"
using assms   by fastforce
finally show ?thesis by auto
qed
ultimately show ?thesis
using τ.eq_iff Abs1_eq_iff(3)[of z1' "CE_val v  ==  CE_val (V_lit ll) IMP  ca[za::=[z1']⇧v]⇩c⇩v"
z1 "CE_val v  ==  CE_val (V_lit ll)   IMP ca[za::=[z1]⇧v]⇩c⇩v"] by blast
qed

lemma subst_sv_var_flip:
fixes x::x and s::s and z::x
shows "atom x ♯ s ⟹ ((x ↔ z) ∙ s) = s[z::=[x]⇧v]⇩s⇩v" and
"atom x ♯ cs ⟹ ((x ↔ z) ∙ cs) = subst_branchv cs z [x]⇧v" and
"atom x ♯ css ⟹ ((x ↔ z) ∙ css) = subst_branchlv css z [x]⇧v"
apply(nominal_induct s and cs and css avoiding: z x rule: s_branch_s_branch_list.strong_induct)
using [[simproc del: alpha_lst]]
apply (auto  ) (* This unpacks subst, perm *)
using  subst_tv_var_flip  flip_fresh_fresh v.fresh s_branch_s_branch_list.fresh
subst_v_τ_def subst_v_v_def subst_vv_var_flip subst_v_e_def subst_ev_var_flip pure_fresh   apply auto
defer 1 (* Sometimes defering hard goals to the end makes it easier to finish *)
using x_fresh_u   apply blast (* Next two involve u and flipping with x *)
defer 1
using x_fresh_u   apply blast
defer 1
using x_fresh_u Abs1_eq_iff'(3) flip_fresh_fresh
using x_fresh_u Abs1_eq_iff'(3) flip_fresh_fresh
fix a::x