Session MiniSail

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"
  by (simp add: fresh_star_def)

section ‹ Additional equivariance lemmas ›

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

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma map_of_eqvt[eqvt]:
  "π  map_of l = map_of (π  l)"
  by (induct l, simp add: permute_fun_def,simp,perm_simp,auto)

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

lemma tranclp_eqvt[eqvt]: "π  tranclp P v1 v2 = tranclp (π  P) (π  v1) (π  v2)" 
  unfolding tranclp_def by perm_simp rule

lemma rtranclp_eqvt[eqvt]: "π  rtranclp P v1 v2 = rtranclp (π  P) (π  v1) (π  v2)" 
  unfolding rtranclp_def by perm_simp rule

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

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

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

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

(* Helper lemmas provided by Christian Urban *)

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

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

section ‹ Freshness lemmas ›

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

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

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

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

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

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

section ‹ Freshness and support for subsets of variables ›

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

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

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

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

section ‹ The set of free variables of an expression ›

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

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

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

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

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

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

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

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

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

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

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

section ‹ Other useful lemmas ›

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

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

lemmas fresh_star_Cons = fresh_star_list(2)

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

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

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

lemmas image_Int[OF inj_atom, simp]

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

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

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

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

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

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

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

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

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

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

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

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

named_theorems nominal_prod_simps 

named_theorems ms_fresh "Facts for helping with freshness proofs"

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

end

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"           ( "[ _ ]ce"      )
  | CE_op "opp" "ce" "ce"  ( "[ _ _ _ ]ce"  )
  | CE_concat ce ce        ( "[ _ @@ _ ]ce" )
  | CE_fst "ce"           ( "[#1_]ce"      )
  | CE_snd "ce"           ( "[#2_]ce"      )
  | CE_len "ce"           ( "[| _ |]ce"    )

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  atom`us"
  by (simp add: image_iff)

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  atom`xs"
  by (simp add: image_iff)

lemma bv_not_in_x_atoms[simp]:
  fixes bv::bv and x::x and xs::"x set"
  shows "atom bv  atom`xs"
  by (simp add: image_iff)

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) = {}" 
  by (simp add: supp_at_base)

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"
     apply(auto,simp add: eqvt_def b_of_graph_aux_def )
  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]ce ==  [[l]v]ce )"
  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]ce == [V_lit l]ce  = ( z' : b  |  [[z']v]ce == [V_lit l]ce )"
  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 
    by (simp add: supp_at_base)
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 dx 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]ce == e  = ( z' : b  |  [[z']v]ce ==  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]ce == e  = ( z' : b'  |  [[z']v]ce == 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  "(xx')  ((x'',b,c) #Γ Γ) = (((xx')  x'',  b , (xx')  c) #Γ ((xx')  Γ ))" 
  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  "(xx')  ((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  "(xx')  ((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  "(xx')  ((x',b,c) #Γ Γ) = ((x,  b , (xx')  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 = {}"
  by (simp add: supp_def)

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"
  by (simp add: fresh_def supp_GNil)

lemma fresh_GCons[ms_fresh]: 
  fixes xs::Γ
  shows "a  (x #Γ xs)  a  x  a  xs"
  by (simp add: fresh_def supp_GCons)

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
    by (simp add: supp_set_empty)
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 "xx'" 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 "xx'" 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 = {}"
  by (simp add: supp_def)

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"
  by (simp add: fresh_def supp_DNil)

lemma fresh_DCons[ms_fresh]: 
  fixes xs::Δ
  shows "a  (x #Δ xs)  a  x  a  xs"
  by (simp add: fresh_def supp_DCons)

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'))"
       apply(auto,simp add: eqvt_def replace_in_g_graph_aux_def)
  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)"
       apply(auto,simp add: eqvt_def lookup_fun_graph_aux_def )
  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)"
          apply(auto,simp add: eqvt_def lookup_td_graph_aux_def )
  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"
       apply(auto,simp add: eqvt_def name_of_type_graph_aux_def )
  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"
     apply(auto,simp add: eqvt_def name_of_fun_graph_aux_def )
  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 
      by (metis add.commute add_minus_cancel)
    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" ("_[_::=_]vv" [1000,50,50] 1000)
  where 
    "v[x::=v']vv   subst_vv v x v'" 

lemma fresh_subst_vv_if [simp]:
  "j  t[i::=x]vv  = ((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]vv = tm"
  by (induct tm rule: v.induct) (simp_all add: fresh_at_base)

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

lemma subst_vv_commute [simp]:
  "atom j  tm  tm[i::=t]vv[j::=u]vv = tm[i::=t[j::=u]vv]vv "
  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]vv[j::=u]vv = tm[j::=u]vv[i::=t]vv"
  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]vv"
  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 )"
  by(simp add: eqvt_def subst_ev_graph_aux_def,auto)(meson e.strong_exhaust)

nominal_termination (eqvt) by lexicographic_order

abbreviation 
  subst_ev_abbrev :: "e  x  v  e" ("_[_::=_]ev" [1000,50,50] 500)
  where 
    "e[x::=v']ev   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]ev)[j::=u]ev = A[i::=t[j::=u]vv]ev"
  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]ev"
  using assms apply(nominal_induct e rule:e.strong_induct)
           apply (simp add: subst_v_v_def)  
          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']ev = ea[xa::=v']ev"
proof -
  have "e[x::=v']ev = (e[x::=V_var c]ev)[c::=v']ev" using subst_ev_commute assms by simp
  also have "...  = ((c  x)  e)[c::=v']ev" using subst_ev_var_flip assms by simp
  also have "... = ((c  xa)  ea)[c::=v']ev" using assms flip_commute by metis
  also have "... = ea[xa::=v']ev"  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]ev = 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]ev) x v = subst_ev  (e[x::=v]ev) 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]ev =  e[z::= ((z1  z1')  v)]ev"
  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 )"
                      apply (simp add: eqvt_def subst_cev_graph_aux_def,auto)
  by (meson ce.strong_exhaust)

nominal_termination (eqvt) by lexicographic_order

abbreviation 
  subst_cev_abbrev :: "ce  x  v  ce" ("_[_::=_]cev" [1000,50,50] 500)
  where 
    "e[x::=v']cev   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]cev"
  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]cev) (v2 [x::=V_var y]cev)" using yf 
    by (simp add: CE_op.hyps(1) CE_op.hyps(2))
  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']cev = ea[xa::=v']cev"
proof -
  have "e[x::=v']cev = (e[x::=V_var c]cev)[c::=v']cev" using subst_ev_commute assms by simp
  also have "...  = ((c  x)  e)[c::=v']cev" using subst_ev_var_flip assms by simp
  also have "... = ((c  xa)  ea)[c::=v']cev" using assms flip_commute by metis
  also have "... = ea[xa::=v']cev"  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]ce [x::=[z]v]cev = [[z]v]ce"
  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]cev) x v  = subst_cev (e[x::=v]cev) 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]cev =  e[z::= ((z1  z1')  v)]cev"
  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 )"
                      apply (simp add: eqvt_def subst_cv_graph_aux_def,auto)
  using c.strong_exhaust by metis
nominal_termination (eqvt)  by lexicographic_order

abbreviation 
  subst_cv_abbrev :: "c  x  v  c" ("_[_::=_]cv" [1000,50,50] 1000)
  where 
    "c[x::=v']cv   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]cv"
  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]cv"
  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]cv =  c[z::=[z1']v]cv"
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]cv = c [z::=v]cv"
  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 "xz"
  shows "(c[z::=w]cv)[x::=v]cv = (c[x::=v]cv)[z::=w]cv" 
  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]cv = (CE_val (V_var x)  ==  e1 )" (is "?A = ?B")
proof -
  have "?A = (((CE_val (V_var z1))[z1::=[x]v]cev) == 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]cv)#Γ (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
   apply (simp add: fresh_GCons)+
  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]cv) #Γ Γ)"  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]cv) #Γ Γ) = (xa, b, c[z::=V_var xa]cv) #Γ Γ"
proof -
  have  "(x  xa)   ((x, b, c[z::=[x]v]cv) #Γ Γ) =  (( (x  xa)   x, b, (x  xa)   c[z::=[x]v]cv) #Γ ((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]cv) #Γ ((x  xa)   Γ))" using assms by fastforce
  also have "... =  ((xa, b,  c[z::=V_var xa]cv) #Γ ((x  xa)   Γ))" using assms subst_cv_var_flip by fastforce
  also have "... =  ((xa, b,  c[z::=V_var xa]cv) #Γ Γ)"  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]cv "
     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]cv = ca[za::=V_var cb]cv"
  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]cv = ca[za::=V_var cb]cv" using assms  by auto
  hence "c[z::=V_var cb]cv[xa::=va]cv = ca[za::=V_var cb]cv[xa::=va]cv" by simp
  moreover have "c[z::=V_var cb]cv[xa::=va]cv = c[xa::=va]cv[z::=V_var cb]cv" 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]cv[xa::=va]cv = ca[xa::=va]cv[za::=V_var cb]cv" 
    using   subst_cv_commute_full[of za va xa "V_var cb" ]  assms fresh_def v.supp by fastforce

  ultimately show "c[xa::=va]cv[z::=V_var cb]cv = ca[xa::=va]cv[za::=V_var cb]cv" 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]vv]τ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]cv "  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]cv " 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 "xz"
  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]cv = c2[z2::=v]cv"
  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]cv"
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]cv" 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]cv = 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]cv" 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]cv = 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]cv = c'[z'::=V_var z]cv[z::=V_var x]cv"  using c_of.simps fresh_Pair  z by metis
  also have "... = c'[z'::=V_var x]cv"  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]cv = c2[z2::=v]cv" and "b1=b2" and " c1 = (z1  z2)  c2"
proof -
  show "c1[z1::=v]cv = c2[z2::=v]cv" 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]cv = c2[z2::=v]cv" and "b1=b2" and "[[atom z1]]lst. c1 = [[atom z2]]lst. c2"
proof -
  show "c1[z1::=v]cv = c2[z2::=v]cv" 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]cv" 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]cv "
  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]vv)  ==  CE_val (V_lit l)   IMP  (c'[x::=v]cv)[z'::=[z1]v]cv   = 
          z1 : b  | CE_val v'           ==  CE_val (V_lit l)   IMP  c'[z'::=[z1]v]cv  [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
  apply (simp add: fresh_DCons)+
  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]ev) (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]vv)  (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(simp add: eqvt_at_def)
    apply(rule)
    apply(subst Projl_permute)
     apply(thin_tac _)+
     apply (simp add: subst_sv_subst_branchv_subst_branchlv_sumC_def)
     apply (simp add: THE_default_def)
     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" ("_[_::=_]sv" [1000,50,50] 1000)
  where 
    "s[x::=v]sv   subst_sv s x v" 

abbreviation 
  subst_branchv_abbrev :: "branch_s  x  v  branch_s" ("_[_::=_]sv" [1000,50,50] 1000)
  where 
    "s[x::=v]sv   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]ev) (s'[x::=v]sv)" using subst_sv.simps(2) AS_let by force
    hence "((j  s'[x::=v]sv  j  set [atom y])  j  None  j  e[x::=v]ev)" using s_branch_s_branch_list.fresh AS_let 
      by (simp add: fresh_None)
    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]sv) (s2[x::=v]sv)" 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']sv = sa[xa::=v']sv"
proof - 
  have "atom x  (s[x::=v']sv)" and xafr: "atom xa  (sa[xa::=v']sv)" 
    and  "atom c  ( s[x::=v']sv, sa[xa::=v']sv)" using assms using  fresh_subst_sv_if assms  by( blast+ ,force)

  hence "s[x::=v']sv = (x  c)  (s[x::=v']sv)"  by (simp add: flip_fresh_fresh fresh_Pair)
  also have " ... = ((x  c)  s)[ ((x  c)  x) ::= ((x  c)  v') ]sv" using subst_sv_subst_branchv_subst_branchlv.eqvt  by blast
  also have "... = ((xa  c)  sa)[ ((x  c)  x) ::= ((x  c)  v') ]sv" using assms by presburger
  also have "... = ((xa  c)  sa)[ ((xa  c)  xa) ::= ((xa  c)  v') ]sv" using assms 
    by (metis flip_at_simps(1) flip_fresh_fresh fresh_PairD(1))
  also have "... =  (xa  c)  (sa[xa::=v']sv)" using subst_sv_subst_branchv_subst_branchlv.eqvt  by presburger
  also have "... = sa[xa::=v']sv" 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]cv ))" 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]cv  ) =  z1 : ba  | CE_val v  ==  CE_val (V_lit ll) IMP  ca[za::=[z1]v]cv  "
proof -
  have "atom z1'  (CE_val v  ==  CE_val (V_lit ll) IMP  ca[za::=[z1]v]cv )" using assms fresh_prod4 by blast
  moreover hence "(CE_val v  ==  CE_val (V_lit ll)   IMP  ca[za::=[z1']v]cv) = (z1'  z1)  (CE_val v  ==  CE_val (V_lit ll)   IMP  ca[za::=[z1]v]cv )"
  proof -
    have "(z1'  z1)  (CE_val v  ==  CE_val (V_lit ll)   IMP  ca[za::=[z1]v]cv ) = ( (z1'  z1)  (CE_val v  ==  CE_val (V_lit ll)) IMP  ((z1'  z1)  ca[za::=[z1]v]cv ))"
      by auto
    also have "... = ((CE_val v  ==  CE_val (V_lit ll))   IMP  ((z1'  z1)  ca[za::=[z1]v]cv ))"
      using ‹atom z1  v assms 
      by (metis (mono_tags) ‹atom z1'  (CE_val v == CE_val (V_lit ll) IMP ca[za::=[z1]v]cv ) 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]cv ))"
      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]cv" 
        z1 "CE_val v  ==  CE_val (V_lit ll)   IMP ca[za::=[z1]v]cv"] 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]sv" 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 
   apply (simp add: subst_v_c_def)
  using x_fresh_u Abs1_eq_iff'(3) flip_fresh_fresh  
  by (simp add: flip_fresh_fresh)

instantiation s :: has_subst_v
begin

definition 
  "subst_v = subst_sv"

instance proof
  fix j::atom and i::x and  x::v and t::s
  show  "(j  subst_v t i x) = ((atom i  t  j  t)  (j  x  (j  t  j = atom i)))"
    using fresh_subst_sv_if subst_v_s_def by auto

  fix a::x