(*<*)
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
  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, opaque_lifting) 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
  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, opaque_lifting) 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, opaque_lifting))   
    thus   "(∃v1'. va = V_consp tyid dc b v1' ∧ (x ↔ c) ∙ vone = (xa ↔ c) ∙ v1')"
      using V_consp assms by simp     
  qed
  thus ?case using V_consp by auto
qed

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

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

subsubsection ‹Expressions›

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

  hence "supp ((z ↔ d) ∙ AE_op opp v1 v2) = supp (AE_op opp ((z ↔ d) ∙v1) ((z ↔ d) ∙v2))" by simp
  also have "... = supp ((z ↔ d) ∙v1) ∪ supp ((z ↔ d) ∙v2)" using e.supp 
    by (metis (mono_tags, opaque_lifting) 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, opaque_lifting) 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 B = "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) #_\<Gamma> Γ')) ==> 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 #_\<Delta> xs) = p ∙ x #_\<Delta> 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) #_\<Delta> Δ')) ==> 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 #_\<Gamma> xs) = p ∙ x #_\<Gamma> 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) #_\<Gamma> Γ) = ((p ∙ x, p ∙ b , p ∙ c) #_\<Gamma> (p ∙ Γ ))" (is "?A = ?B" )
  using Cons_eqvt triple_eqvt  supp_b_empty by simp

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

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

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

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

lemma neq_GNil_conv: "(xs ≠ GNil) = (∃y ys. xs = y #_\<Gamma> 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 #_\<Gamma> g1) g2 = (xbc #_\<Gamma> (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
  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 #_\<Gamma> 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) #_\<Gamma> G) = atom_dom ((x, b, c') #_\<Gamma> 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) #_\<Gamma> 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 #_\<Gamma> 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 #_\<Gamma> ys) = (xs @ (x #_\<Gamma> 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) #_\<Gamma> Γ = (atom x' ∉ supp Γ' ∪ supp x ∪ supp b0 ∪ supp c0 ∪ supp Γ)"
proof - 
  have  "atom x' ♯ Γ' @ (x, b0, c0) #_\<Gamma> Γ = (atom x' ∉ supp (Γ' @((x,b0,c0) #_\<Gamma> Γ)))"
    using fresh_def by auto
  also have "... = (atom x' ∉ supp Γ' ∪ supp ((x,b0,c0) #_\<Gamma> Γ))" 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 #_\<Gamma> xs"
  by (induct xs) auto

lemma not_GCons_self2 [simp]: 
  fixes xs::Γ
  shows "x #_\<Gamma> xs ≠ xs"
  by (rule not_GCons_self [symmetric])

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

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

lemma Γ_set_intros: "x ∈ toSet ( x #_\<Gamma> xs)" and "y ∈ toSet xs ==> y ∈ toSet (x #_\<Gamma> xs)"
  by simp+

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

subsection ‹Mutable Variable Context Lemmas›

lemma supp_DNil: 
  shows "supp DNil = {}"
  by (simp add: supp_def)

lemma supp_DCons: 
  fixes xs::Δ
  shows "supp (x #_\<Delta> 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 #_\<Delta> 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)#_\<Gamma>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)#_\<Gamma>G) x' c' = (if x=x' then ((x,b,c')#_\<Gamma>G) else (x,b,c)#_\<Gamma>(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 #_\<Delta> 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