Theory Nominal

theory Nominal 
  imports "HOL-Library.Infinite_Set" "HOL-Library.Old_Datatype"

keywords
  "atom_decl" :: thy_decl and
  "nominal_datatype" :: thy_defn and
  "equivariance" :: thy_decl and
  "nominal_primrec" "nominal_inductive" "nominal_inductive2" :: thy_goal_defn and
  "avoids"
begin

declare [[typedef_overloaded]]


section ‹Permutations›
(*======================*)

type_synonym 
  'x prm = "('x × 'x) list"

(* polymorphic constants for permutation and swapping *)
consts 
  perm :: "'x prm  'a  'a"     (infixr  80)
  swap :: "('x × 'x)  'x  'x"

(* a "private" copy of the option type used in the abstraction function *)
datatype 'a noption = nSome 'a | nNone

datatype_compat noption

(* a "private" copy of the product type used in the nominal induct method *)
datatype ('a, 'b) nprod = nPair 'a 'b

datatype_compat nprod

(* an auxiliary constant for the decision procedure involving *) 
(* permutations (to avoid loops when using perm-compositions)  *)
definition
  "perm_aux pi x = pix"

(* overloaded permutation operations *)
overloading
  perm_fun     "perm :: 'x prm  ('a'b)  ('a'b)"   (unchecked)
  perm_bool    "perm :: 'x prm  bool  bool"           (unchecked)
  perm_set     "perm :: 'x prm  'a set  'a set"       (unchecked)
  perm_unit    "perm :: 'x prm  unit  unit"           (unchecked)
  perm_prod    "perm :: 'x prm  ('a×'b)  ('a×'b)"    (unchecked)
  perm_list    "perm :: 'x prm  'a list  'a list"     (unchecked)
  perm_option  "perm :: 'x prm  'a option  'a option" (unchecked)
  perm_char    "perm :: 'x prm  char  char"           (unchecked)
  perm_nat     "perm :: 'x prm  nat  nat"             (unchecked)
  perm_int     "perm :: 'x prm  int  int"             (unchecked)

  perm_noption  "perm :: 'x prm  'a noption  'a noption"   (unchecked)
  perm_nprod    "perm :: 'x prm  ('a, 'b) nprod  ('a, 'b) nprod" (unchecked)
begin

definition perm_fun :: "'x prm  ('a  'b)  'a  'b" where
  "perm_fun pi f = (λx. pi  f (rev pi  x))"

definition perm_bool :: "'x prm  bool  bool" where
  "perm_bool pi b = b"

definition perm_set :: "'x prm  'a set  'a set" where
  "perm_set pi X = {pi  x | x. x  X}"

primrec perm_unit :: "'x prm  unit  unit"  where 
  "perm_unit pi () = ()"
  
primrec perm_prod :: "'x prm  ('a×'b)  ('a×'b)" where
  "perm_prod pi (x, y) = (pix, piy)"

primrec perm_list :: "'x prm  'a list  'a list" where
  nil_eqvt:  "perm_list pi []     = []"
| cons_eqvt: "perm_list pi (x#xs) = (pix)#(pixs)"

primrec perm_option :: "'x prm  'a option  'a option" where
  some_eqvt:  "perm_option pi (Some x) = Some (pix)"
| none_eqvt:  "perm_option pi None     = None"

definition perm_char :: "'x prm  char  char" where
  "perm_char pi c = c"

definition perm_nat :: "'x prm  nat  nat" where
  "perm_nat pi i = i"

definition perm_int :: "'x prm  int  int" where
  "perm_int pi i = i"

primrec perm_noption :: "'x prm  'a noption  'a noption" where
  nsome_eqvt:  "perm_noption pi (nSome x) = nSome (pix)"
| nnone_eqvt:  "perm_noption pi nNone     = nNone"

primrec perm_nprod :: "'x prm  ('a, 'b) nprod  ('a, 'b) nprod" where
  "perm_nprod pi (nPair x y) = nPair (pix) (piy)"

end

(* permutations on booleans *)
lemmas perm_bool = perm_bool_def

lemma true_eqvt [simp]:
  "pi  True  True"
  by (simp add: perm_bool_def)

lemma false_eqvt [simp]:
  "pi  False  False"
  by (simp add: perm_bool_def)

lemma perm_boolI:
  assumes a: "P"
  shows "piP"
  using a by (simp add: perm_bool)

lemma perm_boolE:
  assumes a: "piP"
  shows "P"
  using a by (simp add: perm_bool)

lemma if_eqvt:
  fixes pi::"'a prm"
  shows "pi(if b then c1 else c2) = (if (pib) then (pic1) else (pic2))"
  by (simp add: perm_fun_def)

lemma imp_eqvt:
  shows "pi(AB) = ((piA)(piB))"
  by (simp add: perm_bool)

lemma conj_eqvt:
  shows "pi(AB) = ((piA)(piB))"
  by (simp add: perm_bool)

lemma disj_eqvt:
  shows "pi(AB) = ((piA)(piB))"
  by (simp add: perm_bool)

lemma neg_eqvt:
  shows "pi(¬ A) = (¬ (piA))"
  by (simp add: perm_bool)

(* permutation on sets *)
lemma empty_eqvt[simp]:
  shows "pi{} = {}"
  by (simp add: perm_set_def)

lemma union_eqvt:
  shows "(pi(XY)) = (piX)  (piY)"
  by (auto simp add: perm_set_def)

lemma insert_eqvt:
  shows "pi(insert x X) = insert (pix) (piX)"
  by (auto simp add: perm_set_def)

(* permutations on products *)
lemma fst_eqvt:
  "pi(fst x) = fst (pix)"
 by (cases x) simp

lemma snd_eqvt:
  "pi(snd x) = snd (pix)"
 by (cases x) simp

(* permutation on lists *)
lemma append_eqvt:
  fixes pi :: "'x prm"
  and   l1 :: "'a list"
  and   l2 :: "'a list"
  shows "pi(l1@l2) = (pil1)@(pil2)"
  by (induct l1) auto

lemma rev_eqvt:
  fixes pi :: "'x prm"
  and   l  :: "'a list"
  shows "pi(rev l) = rev (pil)"
  by (induct l) (simp_all add: append_eqvt)

lemma set_eqvt:
  fixes pi :: "'x prm"
  and   xs :: "'a list"
  shows "pi(set xs) = set (pixs)"
by (induct xs) (auto simp add: empty_eqvt insert_eqvt)

(* permutation on characters and strings *)
lemma perm_string:
  fixes s::"string"
  shows "pis = s"
  by (induct s)(auto simp add: perm_char_def)


section ‹permutation equality›
(*==============================*)

definition prm_eq :: "'x prm  'x prm  bool" (‹ _  _ › [80,80] 80) where
  "pi1  pi2  (a::'x. pi1a = pi2a)"

section ‹Support, Freshness and Supports›
(*========================================*)
definition supp :: "'a  ('x set)" where  
   "supp x = {a . (infinite {b . [(a,b)]x  x})}"

definition fresh :: "'x  'a  bool" (‹_  _› [80,80] 80) where
   "a  x  a  supp x"

definition supports :: "'x set  'a  bool" (infixl supports 80) where
   "S supports x  (a b. (aS  bS  [(a,b)]x=x))"

(* lemmas about supp *)
lemma supp_fresh_iff: 
  fixes x :: "'a"
  shows "(supp x) = {a::'x. ¬ax}"
  by (simp add: fresh_def)

lemma supp_unit[simp]:
  shows "supp () = {}"
  by (simp add: supp_def)

lemma supp_set_empty[simp]:
  shows "supp {} = {}"
  by (force simp add: supp_def empty_eqvt)

lemma supp_prod: 
  fixes x :: "'a"
  and   y :: "'b"
  shows "(supp (x,y)) = (supp x)(supp y)"
  by  (force simp add: supp_def Collect_imp_eq Collect_neg_eq)

lemma supp_nprod: 
  fixes x :: "'a"
  and   y :: "'b"
  shows "(supp (nPair x y)) = (supp x)(supp y)"
  by  (force simp add: supp_def Collect_imp_eq Collect_neg_eq)

lemma supp_list_nil[simp]:
  shows "supp [] = {}"
  by (simp add: supp_def)

lemma supp_list_cons:
  fixes x  :: "'a"
  and   xs :: "'a list"
  shows "supp (x#xs) = (supp x)(supp xs)"
  by (auto simp add: supp_def Collect_imp_eq Collect_neg_eq)

lemma supp_list_append:
  fixes xs :: "'a list"
  and   ys :: "'a list"
  shows "supp (xs@ys) = (supp xs)(supp ys)"
  by (induct xs) (auto simp add: supp_list_nil supp_list_cons)

lemma supp_list_rev:
  fixes xs :: "'a list"
  shows "supp (rev xs) = (supp xs)"
  by (induct xs, auto simp add: supp_list_append supp_list_cons supp_list_nil)

lemma supp_bool[simp]:
  fixes x  :: "bool"
  shows "supp x = {}"
  by (cases "x") (simp_all add: supp_def)

lemma supp_some[simp]:
  fixes x :: "'a"
  shows "supp (Some x) = (supp x)"
  by (simp add: supp_def)

lemma supp_none[simp]:
  fixes x :: "'a"
  shows "supp (None) = {}"
  by (simp add: supp_def)

lemma supp_int[simp]:
  fixes i::"int"
  shows "supp (i) = {}"
  by (simp add: supp_def perm_int_def)

lemma supp_nat[simp]:
  fixes n::"nat"
  shows "(supp n) = {}"
  by (simp add: supp_def perm_nat_def)

lemma supp_char[simp]:
  fixes c::"char"
  shows "(supp c) = {}"
  by (simp add: supp_def perm_char_def)
  
lemma supp_string[simp]:
  fixes s::"string"
  shows "(supp s) = {}"
  by (simp add: supp_def perm_string)

(* lemmas about freshness *)
lemma fresh_set_empty[simp]:
  shows "a{}"
  by (simp add: fresh_def supp_set_empty)

lemma fresh_unit[simp]:
  shows "a()"
  by (simp add: fresh_def supp_unit)

lemma fresh_prod:
  fixes a :: "'x"
  and   x :: "'a"
  and   y :: "'b"
  shows "a(x,y) = (ax  ay)"
  by (simp add: fresh_def supp_prod)

lemma fresh_list_nil[simp]:
  fixes a :: "'x"
  shows "a[]"
  by (simp add: fresh_def supp_list_nil) 

lemma fresh_list_cons:
  fixes a :: "'x"
  and   x :: "'a"
  and   xs :: "'a list"
  shows "a(x#xs) = (ax  axs)"
  by (simp add: fresh_def supp_list_cons)

lemma fresh_list_append:
  fixes a :: "'x"
  and   xs :: "'a list"
  and   ys :: "'a list"
  shows "a(xs@ys) = (axs  ays)"
  by (simp add: fresh_def supp_list_append)

lemma fresh_list_rev[simp]:
  fixes a :: "'x"
  and   xs :: "'a list"
  shows "a(rev xs) = axs"
  by (simp add: fresh_def supp_list_rev)

lemma fresh_none[simp]:
  fixes a :: "'x"
  shows "aNone"
  by (simp add: fresh_def supp_none)

lemma fresh_some[simp]:
  fixes a :: "'x"
  and   x :: "'a"
  shows "a(Some x) = ax"
  by (simp add: fresh_def supp_some)

lemma fresh_int[simp]:
  fixes a :: "'x"
  and   i :: "int"
  shows "ai"
  by (simp add: fresh_def supp_int)

lemma fresh_nat[simp]:
  fixes a :: "'x"
  and   n :: "nat"
  shows "an"
  by (simp add: fresh_def supp_nat)

lemma fresh_char[simp]:
  fixes a :: "'x"
  and   c :: "char"
  shows "ac"
  by (simp add: fresh_def supp_char)

lemma fresh_string[simp]:
  fixes a :: "'x"
  and   s :: "string"
  shows "as"
  by (simp add: fresh_def supp_string)

lemma fresh_bool[simp]:
  fixes a :: "'x"
  and   b :: "bool"
  shows "ab"
  by (simp add: fresh_def supp_bool)

text ‹Normalization of freshness results; cf.\ nominal_induct›
lemma fresh_unit_elim: 
  shows "(a()  PROP C)  PROP C"
  by (simp add: fresh_def supp_unit)

lemma fresh_prod_elim: 
  shows "(a(x,y)  PROP C)  (ax  ay  PROP C)"
  by rule (simp_all add: fresh_prod)

(* this rule needs to be added before the fresh_prodD is *)
(* added to the simplifier with mksimps                  *) 
lemma [simp]:
  shows "ax1  ax2  a(x1,x2)"
  by (simp add: fresh_prod)

lemma fresh_prodD:
  shows "a(x,y)  ax"
  and   "a(x,y)  ay"
  by (simp_all add: fresh_prod)

ML val mksimps_pairs = (const_nameNominal.fresh, @{thms fresh_prodD}) :: mksimps_pairs;
declaration fn _ =>
  Simplifier.map_ss (Simplifier.set_mksimps (mksimps mksimps_pairs))

section ‹Abstract Properties for Permutations and  Atoms›
(*=========================================================*)

(* properties for being a permutation type *)
definition
  "pt TYPE('a) TYPE('x)  
     ((x::'a). ([]::'x prm)x = x)  
     ((pi1::'x prm) (pi2::'x prm) (x::'a). (pi1@pi2)x = pi1(pi2x))  
     ((pi1::'x prm) (pi2::'x prm) (x::'a). pi1  pi2  pi1x = pi2x)"

(* properties for being an atom type *)
definition
  "at TYPE('x)  
     ((x::'x). ([]::'x prm)x = x) 
     ((a::'x) (b::'x) (pi::'x prm) (x::'x). ((a,b)#(pi::'x prm))x = swap (a,b) (pix))  
     ((a::'x) (b::'x) (c::'x). swap (a,b) c = (if a=c then b else (if b=c then a else c)))  
     (infinite (UNIV::'x set))"

(* property of two atom-types being disjoint *)
definition
  "disjoint TYPE('x) TYPE('y)  
       ((pi::'x prm)(x::'y). pix = x)  
       ((pi::'y prm)(x::'x). pix = x)"

(* composition property of two permutation on a type 'a *)
definition
  "cp TYPE ('a) TYPE('x) TYPE('y)  
      ((pi2::'y prm) (pi1::'x prm) (x::'a) . pi1(pi2x) = (pi1pi2)(pi1x))" 

(* property of having finite support *)
definition
  "fs TYPE('a) TYPE('x)  (x::'a). finite ((supp x)::'x set)"

section ‹Lemmas about the atom-type properties›
(*==============================================*)

lemma at1: 
  fixes x::"'x"
  assumes a: "at TYPE('x)"
  shows "([]::'x prm)x = x"
  using a by (simp add: at_def)

lemma at2: 
  fixes a ::"'x"
  and   b ::"'x"
  and   x ::"'x"
  and   pi::"'x prm"
  assumes a: "at TYPE('x)"
  shows "((a,b)#pi)x = swap (a,b) (pix)"
  using a by (simp only: at_def)

lemma at3: 
  fixes a ::"'x"
  and   b ::"'x"
  and   c ::"'x"
  assumes a: "at TYPE('x)"
  shows "swap (a,b) c = (if a=c then b else (if b=c then a else c))"
  using a by (simp only: at_def)

(* rules to calculate simple permutations *)
lemmas at_calc = at2 at1 at3

lemma at_swap_simps:
  fixes a ::"'x"
  and   b ::"'x"
  assumes a: "at TYPE('x)"
  shows "[(a,b)]a = b"
  and   "[(a,b)]b = a"
  and   "ac; bc  [(a,b)]c = c"
  using a by (simp_all add: at_calc)

lemma at4: 
  assumes a: "at TYPE('x)"
  shows "infinite (UNIV::'x set)"
  using a by (simp add: at_def)

lemma at_append:
  fixes pi1 :: "'x prm"
  and   pi2 :: "'x prm"
  and   c   :: "'x"
  assumes at: "at TYPE('x)" 
  shows "(pi1@pi2)c = pi1(pi2c)"
proof (induct pi1)
  case Nil show ?case by (simp add: at1[OF at])
next
  case (Cons x xs)
  have "(xs@pi2)c  =  xs(pi2c)" by fact
  also have "(x#xs)@pi2 = x#(xs@pi2)" by simp
  ultimately show ?case by (cases "x", simp add:  at2[OF at])
qed
 
lemma at_swap:
  fixes a :: "'x"
  and   b :: "'x"
  and   c :: "'x"
  assumes at: "at TYPE('x)" 
  shows "swap (a,b) (swap (a,b) c) = c"
  by (auto simp add: at3[OF at])

lemma at_rev_pi:
  fixes pi :: "'x prm"
  and   c  :: "'x"
  assumes at: "at TYPE('x)"
  shows "(rev pi)(pic) = c"
proof(induct pi)
  case Nil show ?case by (simp add: at1[OF at])
next
  case (Cons x xs) thus ?case 
    by (cases "x", simp add: at2[OF at] at_append[OF at] at1[OF at] at_swap[OF at])
qed

lemma at_pi_rev:
  fixes pi :: "'x prm"
  and   x  :: "'x"
  assumes at: "at TYPE('x)"
  shows "pi((rev pi)x) = x"
  by (rule at_rev_pi[OF at, of "rev pi" _,simplified])

lemma at_bij1: 
  fixes pi :: "'x prm"
  and   x  :: "'x"
  and   y  :: "'x"
  assumes at: "at TYPE('x)"
  and     a:  "(pix) = y"
  shows   "x=(rev pi)y"
proof -
  from a have "y=(pix)" by (rule sym)
  thus ?thesis by (simp only: at_rev_pi[OF at])
qed

lemma at_bij2: 
  fixes pi :: "'x prm"
  and   x  :: "'x"
  and   y  :: "'x"
  assumes at: "at TYPE('x)"
  and     a:  "((rev pi)x) = y"
  shows   "x=piy"
proof -
  from a have "y=((rev pi)x)" by (rule sym)
  thus ?thesis by (simp only: at_pi_rev[OF at])
qed

lemma at_bij:
  fixes pi :: "'x prm"
  and   x  :: "'x"
  and   y  :: "'x"
  assumes at: "at TYPE('x)"
  shows "(pix = piy) = (x=y)"
proof 
  assume "pix = piy" 
  hence  "x=(rev pi)(piy)" by (rule at_bij1[OF at]) 
  thus "x=y" by (simp only: at_rev_pi[OF at])
next
  assume "x=y"
  thus "pix = piy" by simp
qed

lemma at_supp:
  fixes x :: "'x"
  assumes at: "at TYPE('x)"
  shows "supp x = {x}"
by(auto simp: supp_def Collect_conj_eq Collect_imp_eq at_calc[OF at] at4[OF at])

lemma at_fresh:
  fixes a :: "'x"
  and   b :: "'x"
  assumes at: "at TYPE('x)"
  shows "(ab) = (ab)" 
  by (simp add: at_supp[OF at] fresh_def)

lemma at_prm_fresh1:
  fixes c :: "'x"
  and   pi:: "'x prm"
  assumes at: "at TYPE('x)"
  and     a: "cpi" 
  shows "(a,b)set pi. ca  cb"
using a by (induct pi) (auto simp add: fresh_list_cons fresh_prod at_fresh[OF at])

lemma at_prm_fresh2:
  fixes c :: "'x"
  and   pi:: "'x prm"
  assumes at: "at TYPE('x)"
  and     a: "(a,b)set pi. ca  cb" 
  shows "pic = c"
using a  by(induct pi) (auto simp add: at1[OF at] at2[OF at] at3[OF at])

lemma at_prm_fresh:
  fixes c :: "'x"
  and   pi:: "'x prm"
  assumes at: "at TYPE('x)"
  and     a: "cpi" 
  shows "pic = c"
by (rule at_prm_fresh2[OF at], rule at_prm_fresh1[OF at, OF a])

lemma at_prm_rev_eq:
  fixes pi1 :: "'x prm"
  and   pi2 :: "'x prm"
  assumes at: "at TYPE('x)"
  shows "((rev pi1)  (rev pi2)) = (pi1  pi2)"
proof (simp add: prm_eq_def, auto)
  fix x
  assume "x::'x. (rev pi1)x = (rev pi2)x"
  hence "(rev (pi1::'x prm))(pi2(x::'x)) = (rev (pi2::'x prm))(pi2x)" by simp
  hence "(rev (pi1::'x prm))((pi2::'x prm)x) = (x::'x)" by (simp add: at_rev_pi[OF at])
  hence "(pi2::'x prm)x = (pi1::'x prm)x" by (simp add: at_bij2[OF at])
  thus "pi1x  =  pi2x" by simp
next
  fix x
  assume "x::'x. pi1x = pi2x"
  hence "(pi1::'x prm)((rev pi2)x) = (pi2::'x prm)((rev pi2)(x::'x))" by simp
  hence "(pi1::'x prm)((rev pi2)(x::'x)) = x" by (simp add: at_pi_rev[OF at])
  hence "(rev pi2)x = (rev pi1)(x::'x)" by (simp add: at_bij1[OF at])
  thus "(rev pi1)x = (rev pi2)(x::'x)" by simp
qed

lemma at_prm_eq_append:
  fixes pi1 :: "'x prm"
  and   pi2 :: "'x prm"
  and   pi3 :: "'x prm"
  assumes at: "at TYPE('x)"
  and     a: "pi1  pi2"
  shows "(pi3@pi1)  (pi3@pi2)"
using a by (simp add: prm_eq_def at_append[OF at] at_bij[OF at])

lemma at_prm_eq_append':
  fixes pi1 :: "'x prm"
  and   pi2 :: "'x prm"
  and   pi3 :: "'x prm"
  assumes at: "at TYPE('x)"
  and     a: "pi1  pi2"
  shows "(pi1@pi3)  (pi2@pi3)"
using a by (simp add: prm_eq_def at_append[OF at])

lemma at_prm_eq_trans:
  fixes pi1 :: "'x prm"
  and   pi2 :: "'x prm"
  and   pi3 :: "'x prm"
  assumes a1: "pi1  pi2"
  and     a2: "pi2  pi3"  
  shows "pi1  pi3"
using a1 a2 by (auto simp add: prm_eq_def)
  
lemma at_prm_eq_refl:
  fixes pi :: "'x prm"
  shows "pi  pi"
by (simp add: prm_eq_def)

lemma at_prm_rev_eq1:
  fixes pi1 :: "'x prm"
  and   pi2 :: "'x prm"
  assumes at: "at TYPE('x)"
  shows "pi1  pi2  (rev pi1)  (rev pi2)"
  by (simp add: at_prm_rev_eq[OF at])

lemma at_ds1:
  fixes a  :: "'x"
  assumes at: "at TYPE('x)"
  shows "[(a,a)]  []"
  by (force simp add: prm_eq_def at_calc[OF at])

lemma at_ds2: 
  fixes pi :: "'x prm"
  and   a  :: "'x"
  and   b  :: "'x"
  assumes at: "at TYPE('x)"
  shows "([(a,b)]@pi)  (pi@[((rev pi)a,(rev pi)b)])"
  by (force simp add: prm_eq_def at_append[OF at] at_bij[OF at] at_pi_rev[OF at] 
      at_rev_pi[OF at] at_calc[OF at])

lemma at_ds3: 
  fixes a  :: "'x"
  and   b  :: "'x"
  and   c  :: "'x"
  assumes at: "at TYPE('x)"
  and     a:  "distinct [a,b,c]"
  shows "[(a,c),(b,c),(a,c)]  [(a,b)]"
  using a by (force simp add: prm_eq_def at_calc[OF at])

lemma at_ds4: 
  fixes a  :: "'x"
  and   b  :: "'x"
  and   pi  :: "'x prm"
  assumes at: "at TYPE('x)"
  shows "(pi@[(a,(rev pi)b)])  ([(pia,b)]@pi)"
  by (force simp add: prm_eq_def at_append[OF at] at_calc[OF at] at_bij[OF at] 
      at_pi_rev[OF at] at_rev_pi[OF at])

lemma at_ds5: 
  fixes a  :: "'x"
  and   b  :: "'x"
  assumes at: "at TYPE('x)"
  shows "[(a,b)]  [(b,a)]"
  by (force simp add: prm_eq_def at_calc[OF at])

lemma at_ds5': 
  fixes a  :: "'x"
  and   b  :: "'x"
  assumes at: "at TYPE('x)"
  shows "[(a,b),(b,a)]  []"
  by (force simp add: prm_eq_def at_calc[OF at])

lemma at_ds6: 
  fixes a  :: "'x"
  and   b  :: "'x"
  and   c  :: "'x"
  assumes at: "at TYPE('x)"
  and     a: "distinct [a,b,c]"
  shows "[(a,c),(a,b)]  [(b,c),(a,c)]"
  using a by (force simp add: prm_eq_def at_calc[OF at])

lemma at_ds7:
  fixes pi :: "'x prm"
  assumes at: "at TYPE('x)"
  shows "((rev pi)@pi)  []"
  by (simp add: prm_eq_def at1[OF at] at_append[OF at] at_rev_pi[OF at])

lemma at_ds8_aux:
  fixes pi :: "'x prm"
  and   a  :: "'x"
  and   b  :: "'x"
  and   c  :: "'x"
  assumes at: "at TYPE('x)"
  shows "pi(swap (a,b) c) = swap (pia,pib) (pic)"
  by (force simp add: at_calc[OF at] at_bij[OF at])

lemma at_ds8: 
  fixes pi1 :: "'x prm"
  and   pi2 :: "'x prm"
  and   a  :: "'x"
  and   b  :: "'x"
  assumes at: "at TYPE('x)"
  shows "(pi1@pi2)  ((pi1pi2)@pi1)"
proof(induct pi2)
  show "(pi1 @ [])  (pi1  [] @ pi1)"
    by(simp add: prm_eq_def)
  show "a l. (pi1 @ l)  (pi1  l @ pi1)  
        (pi1 @ a # l)  (pi1  (a # l) @ pi1) "
    by(auto simp add: prm_eq_def at at2 at_append at_ds8_aux)
qed

lemma at_ds9: 
  fixes pi1 :: "'x prm"
  and   pi2 :: "'x prm"
  and   a  :: "'x"
  and   b  :: "'x"
  assumes at: "at TYPE('x)"
  shows " ((rev pi2)@(rev pi1))  ((rev pi1)@(rev (pi1pi2)))"
  using at at_ds8 at_prm_rev_eq1 rev_append by fastforce

lemma at_ds10:
  fixes pi :: "'x prm"
  and   a  :: "'x"
  and   b  :: "'x"
  assumes "at TYPE('x)"
  and     "b(rev pi)"
  shows "([(pia,b)]@pi)  (pi@[(a,b)])"
  by (metis assms at_bij1 at_ds2 at_prm_fresh)

― ‹there always exists an atom that is not being in a finite set›
lemma ex_in_inf:
  fixes   A::"'x set"
  assumes at: "at TYPE('x)"
  and     fs: "finite A"
  obtains c::"'x" where "cA"
  using at at4 ex_new_if_finite fs by blast

text ‹there always exists a fresh name for an object with finite support›
lemma at_exists_fresh': 
  fixes  x :: "'a"
  assumes at: "at TYPE('x)"
  and     fs: "finite ((supp x)::'x set)"
  shows "c::'x. cx"
  by (auto simp add: fresh_def intro: ex_in_inf[OF at, OF fs])

lemma at_exists_fresh: 
  fixes  x :: "'a"
  assumes at: "at TYPE('x)"
  and     fs: "finite ((supp x)::'x set)"
  obtains c::"'x" where  "cx"
  by (auto intro: ex_in_inf[OF at, OF fs] simp add: fresh_def)

lemma at_finite_select: 
  fixes S::"'a set"
  assumes a: "at TYPE('a)"
  and     b: "finite S" 
  shows "x. x  S"
  by (meson a b ex_in_inf) 

lemma at_different:
  assumes at: "at TYPE('x)"
  shows "(b::'x). ab"
proof -
  have "infinite (UNIV::'x set)" by (rule at4[OF at])
  hence inf2: "infinite (UNIV-{a})" by (rule infinite_remove)
  have "(UNIV-{a})  ({}::'x set)"
    by (metis finite.emptyI inf2) 
  hence "(b::'x). b(UNIV-{a})" by blast
  then obtain b::"'x" where mem2: "b(UNIV-{a})" by blast
  from mem2 have "ab" by blast
  then show "(b::'x). ab" by blast
qed

― ‹the at-props imply the pt-props›
lemma at_pt_inst:
  assumes at: "at TYPE('x)"
  shows "pt TYPE('x) TYPE('x)"
  using at at_append at_def prm_eq_def pt_def by fastforce

section ‹finite support properties›
(*===================================*)

lemma fs1:
  fixes x :: "'a"
  assumes a: "fs TYPE('a) TYPE('x)"
  shows "finite ((supp x)::'x set)"
  using a by (simp add: fs_def)

lemma fs_at_inst:
  fixes a :: "'x"
  assumes at: "at TYPE('x)"
  shows "fs TYPE('x) TYPE('x)"
  by (simp add: at at_supp fs_def)

lemma fs_unit_inst:
  shows "fs TYPE(unit) TYPE('x)"
  by(simp add: fs_def supp_unit)

lemma fs_prod_inst:
  assumes fsa: "fs TYPE('a) TYPE('x)"
  and     fsb: "fs TYPE('b) TYPE('x)"
  shows "fs TYPE('a×'b) TYPE('x)"
  by (simp add: assms fs1 supp_prod fs_def)


lemma fs_nprod_inst:
  assumes fsa: "fs TYPE('a) TYPE('x)"
  and     fsb: "fs TYPE('b) TYPE('x)"
  shows "fs TYPE(('a,'b) nprod) TYPE('x)"
  unfolding fs_def by (metis assms finite_Un fs_def nprod.exhaust supp_nprod)

lemma fs_list_inst:
  assumes "fs TYPE('a) TYPE('x)"
  shows "fs TYPE('a list) TYPE('x)"
  unfolding fs_def
  by (clarify, induct_tac x) (auto simp: fs1 assms supp_list_cons)

lemma fs_option_inst:
  assumes fs: "fs TYPE('a) TYPE('x)"
  shows "fs TYPE('a option) TYPE('x)"
  unfolding fs_def
  by (metis assms finite.emptyI fs1 option.exhaust supp_none supp_some)

section ‹Lemmas about the permutation properties›
(*=================================================*)

lemma pt1:
  fixes x::"'a"
  assumes a: "pt TYPE('a) TYPE('x)"
  shows "([]::'x prm)x = x"
  using a by (simp add: pt_def)

lemma pt2: 
  fixes pi1::"'x prm"
  and   pi2::"'x prm"
  and   x  ::"'a"
  assumes a: "pt TYPE('a) TYPE('x)"
  shows "(pi1@pi2)x = pi1(pi2x)"
  using a by (simp add: pt_def)

lemma pt3:
  fixes pi1::"'x prm"
  and   pi2::"'x prm"
  and   x  ::"'a"
  assumes a: "pt TYPE('a) TYPE('x)"
  shows "pi1  pi2  pi1x = pi2x"
  using a by (simp add: pt_def)

lemma pt3_rev:
  fixes pi1::"'x prm"
  and   pi2::"'x prm"
  and   x  ::"'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "pi1  pi2  (rev pi1)x = (rev pi2)x"
  by (rule pt3[OF pt], simp add: at_prm_rev_eq[OF at])

section ‹composition properties›
(* ============================== *)
lemma cp1:
  fixes pi1::"'x prm"
  and   pi2::"'y prm"
  and   x  ::"'a"
  assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)"
  shows "pi1(pi2x) = (pi1pi2)(pi1x)"
  using cp by (simp add: cp_def)

lemma cp_pt_inst:
  assumes "pt TYPE('a) TYPE('x)"
  and     "at TYPE('x)"
  shows "cp TYPE('a) TYPE('x) TYPE('x)"
  using assms at_ds8 cp_def pt2 pt3 by fastforce

section ‹disjointness properties›
(*=================================*)
lemma dj_perm_forget:
  fixes pi::"'y prm"
  and   x ::"'x"
  assumes dj: "disjoint TYPE('x) TYPE('y)"
  shows "pix=x" 
  using dj by (simp_all add: disjoint_def)

lemma dj_perm_set_forget:
  fixes pi::"'y prm"
  and   x ::"'x set"
  assumes dj: "disjoint TYPE('x) TYPE('y)"
  shows "pix=x" 
  using dj by (simp_all add: perm_set_def disjoint_def)

lemma dj_perm_perm_forget:
  fixes pi1::"'x prm"
  and   pi2::"'y prm"
  assumes dj: "disjoint TYPE('x) TYPE('y)"
  shows "pi2pi1=pi1"
  using dj by (induct pi1, auto simp add: disjoint_def)

lemma dj_cp:
  fixes pi1::"'x prm"
  and   pi2::"'y prm"
  and   x  ::"'a"
  assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)"
  and     dj: "disjoint TYPE('y) TYPE('x)"
  shows "pi1(pi2x) = (pi2)(pi1x)"
  by (simp add: cp1[OF cp] dj_perm_perm_forget[OF dj])

lemma dj_supp:
  fixes a::"'x"
  assumes dj: "disjoint TYPE('x) TYPE('y)"
  shows "(supp a) = ({}::'y set)"
  by (simp add: supp_def dj_perm_forget[OF dj])

lemma at_fresh_ineq:
  fixes a :: "'x"
  and   b :: "'y"
  assumes dj: "disjoint TYPE('y) TYPE('x)"
  shows "ab" 
  by (simp add: fresh_def dj_supp[OF dj])

section ‹permutation type instances›
(* ===================================*)

lemma pt_fun_inst:
  assumes pta: "pt TYPE('a) TYPE('x)"
  and     ptb: "pt TYPE('b) TYPE('x)"
  and     at:  "at TYPE('x)"
  shows  "pt TYPE('a'b) TYPE('x)"
  unfolding pt_def using assms
  by (auto simp add: perm_fun_def pt1 pt2 ptb pt3 pt3_rev)

lemma pt_bool_inst[simp]:
  shows  "pt TYPE(bool) TYPE('x)"
  by (simp add: pt_def perm_bool_def)

lemma pt_set_inst:
  assumes pt: "pt TYPE('a) TYPE('x)"
  shows  "pt TYPE('a set) TYPE('x)"
  unfolding pt_def
  by(auto simp add: perm_set_def  pt1[OF pt] pt2[OF pt] pt3[OF pt])

lemma pt_unit_inst[simp]:
  shows "pt TYPE(unit) TYPE('x)"
  by (simp add: pt_def)

lemma pt_prod_inst:
  assumes pta: "pt TYPE('a) TYPE('x)"
  and     ptb: "pt TYPE('b) TYPE('x)"
shows  "pt TYPE('a × 'b) TYPE('x)"
  using assms pt1 pt2 pt3
  by(auto simp add: pt_def)

lemma pt_list_nil: 
  fixes xs :: "'a list"
  assumes pt: "pt TYPE('a) TYPE ('x)"
  shows "([]::'x prm)xs = xs" 
  by (induct xs) (simp_all add: pt1[OF pt])

lemma pt_list_append: 
  fixes pi1 :: "'x prm"
  and   pi2 :: "'x prm"
  and   xs  :: "'a list"
  assumes pt: "pt TYPE('a) TYPE ('x)"
  shows "(pi1@pi2)xs = pi1(pi2xs)"
  by (induct xs) (simp_all add: pt2[OF pt])

lemma pt_list_prm_eq: 
  fixes pi1 :: "'x prm"
  and   pi2 :: "'x prm"
  and   xs  :: "'a list"
  assumes pt: "pt TYPE('a) TYPE ('x)"
  shows "pi1  pi2   pi1xs = pi2xs"
  by (induct xs) (simp_all add: pt3[OF pt])

lemma pt_list_inst:
  assumes pt: "pt TYPE('a) TYPE('x)"
  shows  "pt TYPE('a list) TYPE('x)"
  by (simp add: pt pt_def pt_list_append pt_list_nil pt_list_prm_eq)

lemma pt_option_inst:
  assumes pta: "pt TYPE('a) TYPE('x)"
  shows  "pt TYPE('a option) TYPE('x)"
proof -
  have "([]::('x × _) list)  x = x" for x :: "'a option"
    by (metis assms none_eqvt not_None_eq pt1 some_eqvt)
  moreover have "(pi1 @ pi2)  x = pi1  pi2  x"
    for pi1 pi2 :: "('x × 'x) list" and x :: "'a option"
    by (metis assms none_eqvt option.collapse pt2 some_eqvt)
  moreover have "pi1  x = pi2  x"
    if "pi1  pi2" for pi1 pi2 :: "('x × 'x) list" and x :: "'a option"
    using that pt3[OF pta] by (metis none_eqvt not_Some_eq some_eqvt)
  ultimately show ?thesis
    by (auto simp add: pt_def)
qed

lemma pt_noption_inst:
  assumes pta: "pt TYPE('a) TYPE('x)"
  shows  "pt TYPE('a noption) TYPE('x)"
proof -
  have "([]::('x × _) list)  x = x" for x :: "'a noption"
    by (metis assms nnone_eqvt noption.exhaust nsome_eqvt pt1)
  moreover have "(pi1 @ pi2)  x = pi1  pi2  x"
    for pi1 pi2 :: "('x × 'x) list" and x :: "'a noption"
    using pt2[OF pta]
    by (metis nnone_eqvt noption.exhaust nsome_eqvt)
  moreover have "pi1  x = pi2  x"
    if "pi1  pi2"
    for pi1 pi2 :: "('x × 'x) list"
      and x :: "'a noption"
    using that pt3[OF pta] by (metis nnone_eqvt noption.exhaust nsome_eqvt)
  ultimately show ?thesis
    by (auto simp add: pt_def)
qed

lemma pt_nprod_inst:
  assumes pta: "pt TYPE('a) TYPE('x)"
  and     ptb: "pt TYPE('b) TYPE('x)"
  shows  "pt TYPE(('a,'b) nprod) TYPE('x)"
proof -
  have "([]::('x × _) list)  x = x"
    for x :: "('a, 'b) nprod"
    by (metis assms(1) nprod.exhaust perm_nprod.simps pt1 ptb)
  moreover have "(pi1 @ pi2)  x = pi1  pi2  x"
    for pi1 pi2 :: "('x × 'x) list" and x :: "('a, 'b) nprod"
    using pt2[OF pta] pt2[OF ptb]
    by (metis nprod.exhaust perm_nprod.simps)
  moreover have "pi1  x = pi2  x"
    if "pi1  pi2" for pi1 pi2 :: "('x × 'x) list" and x :: "('a, 'b) nprod"
    using that pt3[OF pta] pt3[OF ptb] by (smt (verit) nprod.exhaust perm_nprod.simps)
  ultimately show ?thesis
    by (auto simp add: pt_def)
qed


section ‹further lemmas for permutation types›
(*==============================================*)

lemma pt_rev_pi:
  fixes pi :: "'x prm"
  and   x  :: "'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "(rev pi)(pix) = x"
proof -
  have "((rev pi)@pi)  ([]::'x prm)" by (simp add: at_ds7[OF at])
  hence "((rev pi)@pi)(x::'a) = ([]::'x prm)x" by (simp add: pt3[OF pt]) 
  thus ?thesis by (simp add: pt1[OF pt] pt2[OF pt])
qed

lemma pt_pi_rev:
  fixes pi :: "'x prm"
  and   x  :: "'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "pi((rev pi)x) = x"
  by (simp add: pt_rev_pi[OF pt, OF at,of "rev pi" "x",simplified])

lemma pt_bij1: 
  fixes pi :: "'x prm"
  and   x  :: "'a"
  and   y  :: "'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  and     a:  "(pix) = y"
  shows   "x=(rev pi)y"
proof -
  from a have "y=(pix)" by (rule sym)
  thus ?thesis by (simp only: pt_rev_pi[OF pt, OF at])
qed

lemma pt_bij2: 
  fixes pi :: "'x prm"
  and   x  :: "'a"
  and   y  :: "'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  and     a:  "x = (rev pi)y"
  shows   "(pix)=y"
  using a by (simp add: pt_pi_rev[OF pt, OF at])

lemma pt_bij:
  fixes pi :: "'x prm"
  and   x  :: "'a"
  and   y  :: "'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "(pix = piy) = (x=y)"
proof 
  assume "pix = piy" 
  hence  "x=(rev pi)(piy)" by (rule pt_bij1[OF pt, OF at]) 
  thus "x=y" by (simp only: pt_rev_pi[OF pt, OF at])
next
  assume "x=y"
  thus "pix = piy" by simp
qed

lemma pt_eq_eqvt:
  fixes pi :: "'x prm"
  and   x  :: "'a"
  and   y  :: "'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "pi(x=y) = (pix = piy)"
  using pt at
  by (auto simp add: pt_bij perm_bool)

lemma pt_bij3:
  fixes pi :: "'x prm"
  and   x  :: "'a"
  and   y  :: "'a"
  assumes a:  "x=y"
  shows "(pix = piy)"
  using a by simp 

lemma pt_bij4:
  fixes pi :: "'x prm"
  and   x  :: "'a"
  and   y  :: "'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  and     a:  "pix = piy"
  shows "x = y"
  using a by (simp add: pt_bij[OF pt, OF at])

lemma pt_swap_bij:
  fixes a  :: "'x"
  and   b  :: "'x"
  and   x  :: "'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "[(a,b)]([(a,b)]x) = x"
  by (rule pt_bij2[OF pt, OF at], simp)

lemma pt_swap_bij':
  fixes a  :: "'x"
  and   b  :: "'x"
  and   x  :: "'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "[(a,b)]([(b,a)]x) = x"
  by (metis assms at_ds5 pt_def pt_swap_bij)

lemma pt_swap_bij'':
  fixes a  :: "'x"
  and   x  :: "'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "[(a,a)]x = x"
  by (metis assms at_ds1 pt_def)

lemma supp_singleton:
  shows "supp {x} = supp x"
  by (force simp add: supp_def perm_set_def)

lemma fresh_singleton:
  shows "a{x} = ax"
  by (simp add: fresh_def supp_singleton)

lemma pt_set_bij1:
  fixes pi :: "'x prm"
  and   x  :: "'a"
  and   X  :: "'a set"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "((pix)X) = (x((rev pi)X))"
  by (force simp add: perm_set_def pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])

lemma pt_set_bij1a:
  fixes pi :: "'x prm"
  and   x  :: "'a"
  and   X  :: "'a set"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "(x(piX)) = (((rev pi)x)X)"
  by (force simp add: perm_set_def pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])

lemma pt_set_bij:
  fixes pi :: "'x prm"
  and   x  :: "'a"
  and   X  :: "'a set"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "((pix)(piX)) = (xX)"
  by (simp add: perm_set_def pt_bij[OF pt, OF at])

lemma pt_in_eqvt:
  fixes pi :: "'x prm"
  and   x  :: "'a"
  and   X  :: "'a set"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "pi(xX)=((pix)(piX))"
using assms
by (auto simp add:  pt_set_bij perm_bool)

lemma pt_set_bij2:
  fixes pi :: "'x prm"
  and   x  :: "'a"
  and   X  :: "'a set"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  and     a:  "xX"
  shows "(pix)(piX)"
  using a by (simp add: pt_set_bij[OF pt, OF at])

lemma pt_set_bij2a:
  fixes pi :: "'x prm"
  and   x  :: "'a"
  and   X  :: "'a set"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  and     a:  "x((rev pi)X)"
  shows "(pix)X"
  using a by (simp add: pt_set_bij1[OF pt, OF at])

lemma pt_subseteq_eqvt:
  fixes pi :: "'x prm"
  and   Y  :: "'a set"
  and   X  :: "'a set"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "(pi(XY)) = ((piX)(piY))"
by (auto simp add: perm_set_def perm_bool pt_bij[OF pt, OF at])

lemma pt_set_diff_eqvt:
  fixes X::"'a set"
  and   Y::"'a set"
  and   pi::"'x prm"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "pi(X - Y) = (piX) - (piY)"
  by (auto simp add: perm_set_def pt_bij[OF pt, OF at])

lemma pt_Collect_eqvt:
  fixes pi::"'x prm"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "pi{x::'a. P x} = {x. P ((rev pi)x)}"
proof -
  have "y. x = pi  y  P y"
    if "P (rev pi  x)" for x
    using that by (metis at pt pt_pi_rev)
  then show ?thesis
    by (auto simp add: perm_set_def pt_rev_pi [OF assms])
qed

― ‹some helper lemmas for the pt_perm_supp_ineq lemma›
lemma Collect_permI: 
  fixes pi :: "'x prm"
  and   x  :: "'a"
  assumes a: "x. (P1 x = P2 x)" 
  shows "{pix| x. P1 x} = {pix| x. P2 x}"
  using a by force

lemma Infinite_cong:
  assumes a: "X = Y"
  shows "infinite X = infinite Y"
  using a by (simp)

lemma pt_set_eq_ineq:
  fixes pi :: "'y prm"
  assumes pt: "pt TYPE('x) TYPE('y)"
  and     at: "at TYPE('y)"
  shows "{pix| x::'x. P x} = {x::'x. P ((rev pi)x)}"
  by (force simp only: pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])

lemma pt_inject_on_ineq:
  fixes X  :: "'y set"
  and   pi :: "'x prm"
  assumes pt: "pt TYPE('y) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "inj_on (perm pi) X"
proof (unfold inj_on_def, intro strip)
  fix x::"'y" and y::"'y"
  assume "pix = piy"
  thus "x=y" by (simp add: pt_bij[OF pt, OF at])
qed

lemma pt_set_finite_ineq: 
  fixes X  :: "'x set"
  and   pi :: "'y prm"
  assumes pt: "pt TYPE('x) TYPE('y)"
  and     at: "at TYPE('y)"
  shows "finite (piX) = finite X"
proof -
  have image: "(piX) = (perm pi ` X)" by (force simp only: perm_set_def)
  show ?thesis
  proof (rule iffI)
    assume "finite (piX)"
    hence "finite (perm pi ` X)" using image by (simp)
    thus "finite X" using pt_inject_on_ineq[OF pt, OF at] by (rule finite_imageD)
  next
    assume "finite X"
    hence "finite (perm pi ` X)" by (rule finite_imageI)
    thus "finite (piX)" using image by (simp)
  qed
qed

lemma pt_set_infinite_ineq: 
  fixes X  :: "'x set"
  and   pi :: "'y prm"
  assumes pt: "pt TYPE('x) TYPE('y)"
  and     at: "at TYPE('y)"
  shows "infinite (piX) = infinite X"
using pt at by (simp add: pt_set_finite_ineq)

lemma pt_perm_supp_ineq:
  fixes  pi  :: "'x prm"
  and    x   :: "'a"
  assumes pta: "pt TYPE('a) TYPE('x)"
  and     ptb: "pt TYPE('y) TYPE('x)"
  and     at:  "at TYPE('x)"
  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  shows "(pi((supp x)::'y set)) = supp (pix)" (is "?LHS = ?RHS")
proof -
  have "?LHS = {pia | a. infinite {b. [(a,b)]x  x}}" by (simp add: supp_def perm_set_def)
  also have " = {pia | a. infinite {pib | b. [(a,b)]x  x}}" 
  proof (rule Collect_permI, rule allI, rule iffI)
    fix a
    assume "infinite {b::'y. [(a,b)]x   x}"
    hence "infinite (pi{b::'y. [(a,b)]x  x})" by (simp add: pt_set_infinite_ineq[OF ptb, OF at])
    thus "infinite {pib |b::'y. [(a,b)]x   x}" by (simp add: perm_set_def)
  next
    fix a
    assume "infinite {pib |b::'y. [(a,b)]x  x}"
    hence "infinite (pi{b::'y. [(a,b)]x  x})" by (simp add: perm_set_def)
    thus "infinite {b::'y. [(a,b)]x   x}" 
      by (simp add: pt_set_infinite_ineq[OF ptb, OF at])
  qed
  also have " = {a. infinite {b::'y. [((rev pi)a,(rev pi)b)]x  x}}" 
    by (simp add: pt_set_eq_ineq[OF ptb, OF at])
  also have " = {a. infinite {b. pi([((rev pi)a,(rev pi)b)]x)  (pix)}}"
    by (simp add: pt_bij[OF pta, OF at])
  also have " = {a. infinite {b. [(a,b)](pix)  (pix)}}"
  proof (rule Collect_cong, rule Infinite_cong, rule Collect_cong)
    fix a::"'y" and b::"'y"
    have "pi(([((rev pi)a,(rev pi)b)])x) = [(a,b)](pix)"
      by (simp add: cp1[OF cp] pt_pi_rev[OF ptb, OF at])
    thus "(pi([((rev pi)a,(rev pi)b)]x)   pix) = ([(a,b)](pix)  pix)" by simp
  qed
  finally show "?LHS = ?RHS" by (simp add: supp_def) 
qed

lemma pt_perm_supp:
  fixes  pi  :: "'x prm"
  and    x   :: "'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "(pi((supp x)::'x set)) = supp (pix)"
  by (rule pt_perm_supp_ineq) (auto simp: assms at_pt_inst cp_pt_inst)

lemma pt_supp_finite_pi:
  fixes  pi  :: "'x prm"
  and    x   :: "'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  and     f: "finite ((supp x)::'x set)"
  shows "finite ((supp (pix))::'x set)"
  by (metis at at_pt_inst f pt pt_perm_supp pt_set_finite_ineq)

lemma pt_fresh_left_ineq:  
  fixes  pi :: "'x prm"
  and     x :: "'a"
  and     a :: "'y"
  assumes pta: "pt TYPE('a) TYPE('x)"
  and     ptb: "pt TYPE('y) TYPE('x)"
  and     at:  "at TYPE('x)"
  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  shows "a(pix) = ((rev pi)a)x"
  using pt_perm_supp_ineq[OF pta, OF ptb, OF at, OF cp] pt_set_bij1[OF ptb, OF at]
  by (simp add: fresh_def)

lemma pt_fresh_right_ineq:  
  fixes  pi :: "'x prm"
  and     x :: "'a"
  and     a :: "'y"
  assumes pta: "pt TYPE('a) TYPE('x)"
  and     ptb: "pt TYPE('y) TYPE('x)"
  and     at:  "at TYPE('x)"
  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  shows "(pia)x = a((rev pi)x)"
  by (simp add: assms pt_fresh_left_ineq)

lemma pt_fresh_bij_ineq:
  fixes  pi :: "'x prm"
  and     x :: "'a"
  and     a :: "'y"
  assumes pta: "pt TYPE('a) TYPE('x)"
  and     ptb: "pt TYPE('y) TYPE('x)"
  and     at:  "at TYPE('x)"
  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  shows "(pia)(pix) = ax"
  using assms pt_bij1 pt_fresh_right_ineq by fastforce

lemma pt_fresh_left:  
  fixes  pi :: "'x prm"
  and     x :: "'a"
  and     a :: "'x"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "a(pix) = ((rev pi)a)x"
  by (simp add: assms at_pt_inst cp_pt_inst pt_fresh_left_ineq)

lemma pt_fresh_right:  
  fixes  pi :: "'x prm"
  and     x :: "'a"
  and     a :: "'x"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "(pia)x = a((rev pi)x)"
  by (simp add: assms at_pt_inst cp_pt_inst pt_fresh_right_ineq)

lemma pt_fresh_bij:
  fixes  pi :: "'x prm"
  and     x :: "'a"
  and     a :: "'x"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "(pia)(pix) = ax"
  by (metis assms pt_bij1 pt_fresh_right)

lemma pt_fresh_bij1:
  fixes  pi :: "'x prm"
  and     x :: "'a"
  and     a :: "'x"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  and     a:  "ax"
  shows "(pia)(pix)"
using a by (simp add: pt_fresh_bij[OF pt, OF at])

lemma pt_fresh_bij2:
  fixes  pi :: "'x prm"
  and     x :: "'a"
  and     a :: "'x"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  and     a:  "(pia)(pix)"
  shows  "ax"
using a by (simp add: pt_fresh_bij[OF pt, OF at])

lemma pt_fresh_eqvt:
  fixes  pi :: "'x prm"
  and     x :: "'a"
  and     a :: "'x"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "pi(ax) = (pia)(pix)"
  by (simp add: perm_bool pt_fresh_bij[OF pt, OF at])

lemma pt_perm_fresh1:
  fixes a :: "'x"
  and   b :: "'x"
  and   x :: "'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE ('x)"
  and     a1: "¬(ax)"
  and     a2: "bx"
  shows "[(a,b)]x  x"
proof
  assume neg: "[(a,b)]x = x"
  from a1 have a1':"a(supp x)" by (simp add: fresh_def) 
  from a2 have a2':"b(supp x)" by (simp add: fresh_def) 
  from a1' a2' have a3: "ab" by force
  from a1' have "([(a,b)]a)([(a,b)](supp x))" 
    by (simp only: pt_set_bij[OF at_pt_inst[OF at], OF at])
  hence "b([(a,b)](supp x))" by (simp add: at_calc[OF at])
  hence "b(supp ([(a,b)]x))" by (simp add: pt_perm_supp[OF pt,OF at])
  with a2' neg show False by simp
qed

(* the next two lemmas are needed in the proof *)
(* of the structural induction principle       *)
lemma pt_fresh_aux:
  fixes a::"'x"
  and   b::"'x"
  and   c::"'x"
  and   x::"'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE ('x)"
  assumes a1: "ca" and  a2: "ax" and a3: "cx"
  shows "c([(a,b)]x)"
using a1 a2 a3 by (simp_all add: pt_fresh_left[OF pt, OF at] at_calc[OF at])

lemma pt_fresh_perm_app:
  fixes pi :: "'x prm" 
  and   a  :: "'x"
  and   x  :: "'y"
  assumes pt: "pt TYPE('y) TYPE('x)"
  and     at: "at TYPE('x)"
  and     h1: "api"
  and     h2: "ax"
  shows "a(pix)"
using assms
proof -
  have "a(rev pi)"using h1 by (simp add: fresh_list_rev)
  then have "(rev pi)a = a" by (simp add: at_prm_fresh[OF at])
  then have "((rev pi)a)x" using h2 by simp
  thus "a(pix)"  by (simp add: pt_fresh_right[OF pt, OF at])
qed

lemma pt_fresh_perm_app_ineq:
  fixes pi::"'x prm"
  and   c::"'y"
  and   x::"'a"
  assumes pta: "pt TYPE('a) TYPE('x)"
  and     ptb: "pt TYPE('y) TYPE('x)"
  and     at:  "at TYPE('x)"
  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  and     dj:  "disjoint TYPE('y) TYPE('x)"
  assumes a: "cx"
  shows "c(pix)"
using a by (simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj])

lemma pt_fresh_eqvt_ineq:
  fixes pi::"'x prm"
  and   c::"'y"
  and   x::"'a"
  assumes pta: "pt TYPE('a) TYPE('x)"
  and     ptb: "pt TYPE('y) TYPE('x)"
  and     at:  "at TYPE('x)"
  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  and     dj:  "disjoint TYPE('y) TYPE('x)"
  shows "pi(cx) = (pic)(pix)"
by (simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj] perm_bool)

― ‹the co-set of a finite set is infinte›
lemma finite_infinite:
  assumes a: "finite {b::'x. P b}"
  and     b: "infinite (UNIV::'x set)"        
  shows "infinite {b. ¬P b}"
proof -
  from a b have "infinite (UNIV - {b::'x. P b})" by (simp add: Diff_infinite_finite)
  moreover 
  have "{b::'x. ¬P b} = UNIV - {b::'x. P b}" by auto
  ultimately show "infinite {b::'x. ¬P b}" by simp
qed 

lemma pt_fresh_fresh:
  fixes   x :: "'a"
  and     a :: "'x"
  and     b :: "'x"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE ('x)"
  and     a1: "ax" and a2: "bx" 
  shows "[(a,b)]x=x"
proof (cases "a=b")
  assume "a=b"
  hence "[(a,b)]  []" by (simp add: at_ds1[OF at])
  hence "[(a,b)]x=([]::'x prm)x" by (rule pt3[OF pt])
  thus ?thesis by (simp only: pt1[OF pt])
next
  assume c2: "ab"
  from a1 have f1: "finite {c. [(a,c)]x  x}" by (simp add: fresh_def supp_def)
  from a2 have f2: "finite {c. [(b,c)]x  x}" by (simp add: fresh_def supp_def)
  from f1 and f2 have f3: "finite {c. perm [(a,c)] x  x  perm [(b,c)] x  x}" 
    by (force simp only: Collect_disj_eq)
  have "infinite {c. [(a,c)]x = x  [(b,c)]x = x}" 
    by (simp add: finite_infinite[OF f3,OF at4[OF at], simplified])
  hence "infinite ({c. [(a,c)]x = x  [(b,c)]x = x}-{a,b})" 
    by (force dest: Diff_infinite_finite)
  hence "({c. [(a,c)]x = x  [(b,c)]x = x}-{a,b})  {}"
    by (metis finite_set set_empty2)
  hence "c. c({c. [(a,c)]x = x  [(b,c)]x = x}-{a,b})" by (force)
  then obtain c 
    where eq1: "[(a,c)]x = x" 
      and eq2: "[(b,c)]x = x" 
      and ineq: "ac  bc"
    by (force)
  hence "[(a,c)]([(b,c)]([(a,c)]x)) = x" by simp 
  hence eq3: "[(a,c),(b,c),(a,c)]x = x" by (simp add: pt2[OF pt,symmetric])
  from c2 ineq have "[(a,c),(b,c),(a,c)]  [(a,b)]" by (simp add: at_ds3[OF at])
  hence "[(a,c),(b,c),(a,c)]x = [(a,b)]x" by (rule pt3[OF pt])
  thus ?thesis using eq3 by simp
qed

lemma pt_pi_fresh_fresh:
  fixes   x :: "'a"
  and     pi :: "'x prm"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE ('x)"
  and     a:  "(a,b)set pi. ax  bx" 
  shows "pix=x"
using a
proof (induct pi)
  case Nil
  show "([]::'x prm)x = x" by (rule pt1[OF pt])
next
  case (Cons ab pi)
  have a: "(a,b)set (ab#pi). ax  bx" by fact
  have ih: "((a,b)set pi. ax  bx)  pix=x" by fact
  obtain a b where e: "ab=(a,b)" by (cases ab) (auto)
  from a have a': "ax" "bx" using e by auto
  have "(ab#pi)x = ([(a,b)]@pi)x" using e by simp
  also have " = [(a,b)](pix)" by (simp only: pt2[OF pt])
  also have " = [(a,b)]x" using ih a by simp
  also have " = x" using a' by (simp add: pt_fresh_fresh[OF pt, OF at])
  finally show "(ab#pi)x = x" by simp
qed

lemma pt_perm_compose:
  fixes pi1 :: "'x prm"
  and   pi2 :: "'x prm"
  and   x  :: "'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "pi2(pi1x) = (pi2pi1)(pi2x)" 
proof -
  have "(pi2@pi1)  ((pi2pi1)@pi2)" by (rule at_ds8 [OF at])
  hence "(pi2@pi1)x = ((pi2pi1)@pi2)x" by (rule pt3[OF pt])
  thus ?thesis by (simp add: pt2[OF pt])
qed

lemma pt_perm_compose':
  fixes pi1 :: "'x prm"
  and   pi2 :: "'x prm"
  and   x  :: "'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "(pi2pi1)x = pi2(pi1((rev pi2)x))" 
proof -
  have "pi2(pi1((rev pi2)x)) = (pi2pi1)(pi2((rev pi2)x))"
    by (rule pt_perm_compose[OF pt, OF at])
  also have " = (pi2pi1)x" by (simp add: pt_pi_rev[OF pt, OF at])
  finally have "pi2(pi1((rev pi2)x)) = (pi2pi1)x" by simp
  thus ?thesis by simp
qed

lemma pt_perm_compose_rev:
  fixes pi1 :: "'x prm"
  and   pi2 :: "'x prm"
  and   x  :: "'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "(rev pi2)((rev pi1)x) = (rev pi1)(rev (pi1pi2)x)" 
proof -
  have "((rev pi2)@(rev pi1))  ((rev pi1)@(rev (pi1pi2)))" by (rule at_ds9[OF at])
  hence "((rev pi2)@(rev pi1))x = ((rev pi1)@(rev (pi1pi2)))x" by (rule pt3[OF pt])
  thus ?thesis by (simp add: pt2[OF pt])
qed

section ‹equivariance for some connectives›
lemma pt_all_eqvt:
  fixes  pi :: "'x prm"
  and     x :: "'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "pi((x::'a). P x) = ((x::'a). pi(P ((rev pi)x)))"
  by (smt (verit, ccfv_threshold) assms pt_bij1 true_eqvt)

lemma pt_ex_eqvt:
  fixes  pi :: "'x prm"
  and     x :: "'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
shows "pi((x::'a). P x) = ((x::'a). pi(P ((rev pi)x)))"
proof -
  have "x. P x  P (rev pi  pi  x)"
    by (simp add: assms(1) at pt_rev_pi)
  then show ?thesis
    by(auto simp add: perm_bool perm_fun_def)
qed

lemma pt_ex1_eqvt:
  fixes  pi :: "'x prm"
  and     x :: "'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows  "(pi(∃!x. P (x::'a))) = (∃!x. pi(P (rev pix)))"
unfolding Ex1_def
by (simp add: pt_ex_eqvt[OF pt at] conj_eqvt pt_all_eqvt[OF pt at] 
              imp_eqvt pt_eq_eqvt[OF pt at] pt_pi_rev[OF pt at])

lemma pt_the_eqvt:
  fixes  pi :: "'x prm"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  and     unique: "∃!x. P x"
  shows "pi(THE(x::'a). P x) = (THE(x::'a). pi(P ((rev pi)x)))"
  by (smt (verit, best) assms perm_bool_def pt_rev_pi theI_unique unique)

section ‹facts about supports›
(*==============================*)

lemma supports_subset:
  fixes x  :: "'a"
  and   S1 :: "'x set"
  and   S2 :: "'x set"
  assumes  a: "S1 supports x"
  and      b: "S1  S2"
  shows "S2 supports x"
  using a b
  by (force simp add: supports_def)

lemma supp_is_subset:
  fixes S :: "'x set"
  and   x :: "'a"
  assumes a1: "S supports x"
  and     a2: "finite S"
  shows "(supp x)S"
proof (rule ccontr)
  assume "¬(supp x  S)"
  hence "a. a(supp x)  aS" by force
  then obtain a where b1: "asupp x" and b2: "aS" by force
  from a1 b2 have "b. (bS  ([(a,b)]x = x))" by (unfold supports_def, force)
  hence "{b. [(a,b)]x  x}S" by force
  with a2 have "finite {b. [(a,b)]x  x}" by (simp add: finite_subset)
  hence "a(supp x)" by (unfold supp_def, auto)
  with b1 show False by simp
qed

lemma supp_supports:
  fixes x :: "'a"
  assumes  pt: "pt TYPE('a) TYPE('x)"
  and      at: "at TYPE ('x)"
  shows "((supp x)::'x set) supports x"
proof (unfold supports_def, intro strip)
  fix a b
  assume "(a::'x)(supp x)  (b::'x)(supp x)"
  hence "ax" and "bx" by (auto simp add: fresh_def)
  thus "[(a,b)]x = x" by (rule pt_fresh_fresh[OF pt, OF at])
qed

lemma supports_finite:
  fixes S :: "'x set"
  and   x :: "'a"
  assumes a1: "S supports x"
  and     a2: "finite S"
  shows "finite ((supp x)::'x set)"
proof -
  have "(supp x)S" using a1 a2 by (rule supp_is_subset)
  thus ?thesis using a2 by (simp add: finite_subset)
qed
  
lemma supp_is_inter:
  fixes  x :: "'a"
  assumes  pt: "pt TYPE('a) TYPE('x)"
  and      at: "at TYPE ('x)"
  and      fs: "fs TYPE('a) TYPE('x)"
  shows "((supp x)::'x set) = ({S. finite S  S supports x})"
proof (rule equalityI)
  show "((supp x)::'x set)  ({S. finite S  S supports x})"
  proof (clarify)
    fix S c
    assume b: "c((supp x)::'x set)" and "finite (S::'x set)" and "S supports x"
    hence  "((supp x)::'x set)S" by (simp add: supp_is_subset) 
    with b show "cS" by force
  qed
next
  show "({S. finite S  S supports x})  ((supp x)::'x set)"
  proof (clarify, simp)
    fix c
    assume d: "(S::'x set). finite S  S supports x  cS"
    have "((supp x)::'x set) supports x" by (rule supp_supports[OF pt, OF at])
    with d fs1[OF fs] show "csupp x" by force
  qed
qed
    
lemma supp_is_least_supports:
  fixes S :: "'x set"
  and   x :: "'a"
  assumes  pt: "pt TYPE('a) TYPE('x)"
  and      at: "at TYPE ('x)"
  and      a1: "S supports x"
  and      a2: "finite S"
  and      a3: "S'. (S' supports x)  SS'"
  shows "S = (supp x)"
proof (rule equalityI)
  show "((supp x)::'x set)S" using a1 a2 by (rule supp_is_subset)
next
  have "((supp x)::'x set) supports x" by (rule supp_supports[OF pt, OF at])
  with a3 show "Ssupp x" by force
qed

lemma supports_set:
  fixes S :: "'x set"
  and   X :: "'a set"
  assumes  pt: "pt TYPE('a) TYPE('x)"
  and      at: "at TYPE ('x)"
  and      a: "xX. ((a::'x) (b::'x). aSbS  ([(a,b)]x)X)"
shows  "S supports X"
proof -
  have "x  X"
    if "a  S" "b  S" and "x  [(a, b)]  X" for a b x
    using that by (metis a assms(1) at pt_pi_rev pt_set_bij1a)
  moreover have "x  [(a, b)]  X"
    if "a  S" "b  S" and "x  X" for a b x
    using that by (simp add: a assms(1) at pt_set_bij1a)
  ultimately show ?thesis
    by (meson subsetI subset_antisym supports_def)
qed

lemma supports_fresh:
  fixes S :: "'x set"
  and   a :: "'x"
  and   x :: "'a"
  assumes a1: "S supports x"
  and     a2: "finite S"
  and     a3: "aS"
  shows "ax"
  by (meson assms fresh_def in_mono supp_is_subset)

lemma at_fin_set_supports:
  fixes X::"'x set"
  assumes at: "at TYPE('x)"
  shows "X supports X"
proof -
  have "a b. aX  bX  [(a,b)]X = X"
    by (auto simp add: perm_set_def at_calc[OF at])
  then show ?thesis by (simp add: supports_def)
qed

lemma infinite_Collection:
  assumes a1:"infinite X"
  and     a2:"bX. P(b)"
  shows "infinite {bX. P(b)}"
  using assms rev_finite_subset by fastforce

lemma at_fin_set_supp:
  fixes X::"'x set" 
  assumes at: "at TYPE('x)"
  and     fs: "finite X"
  shows "(supp X) = X"
proof (rule subset_antisym)
  show "(supp X)  X" using at_fin_set_supports[OF at] using fs by (simp add: supp_is_subset)
next
  have inf: "infinite (UNIV-X)" using at4[OF at] fs by (auto simp add: Diff_infinite_finite)
  { fix a::"'x"
    assume asm: "aX"
    hence "b(UNIV-X). [(a,b)]XX"
      by (auto simp add: perm_set_def at_calc[OF at])
    with inf have "infinite {b(UNIV-X). [(a,b)]XX}" by (rule infinite_Collection)
    hence "infinite {b. [(a,b)]XX}" by (rule_tac infinite_super, auto)
    hence "a(supp X)" by (simp add: supp_def)
  }
  then show "X(supp X)" by blast
qed

lemma at_fin_set_fresh:
  fixes X::"'x set" 
  assumes at: "at TYPE('x)"
  and     fs: "finite X"
  shows "(x  X) = (x  X)"
  by (simp add: at_fin_set_supp fresh_def at fs)


section ‹Permutations acting on Functions›
(*==========================================*)

lemma pt_fun_app_eq:
  fixes f  :: "'a'b"
  and   x  :: "'a"
  and   pi :: "'x prm"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "pi(f x) = (pif)(pix)"
  by (simp add: perm_fun_def pt_rev_pi[OF pt, OF at])


― ‹sometimes pt_fun_app_eq does too much; this lemma 'corrects it'›
lemma pt_perm:
  fixes x  :: "'a"
  and   pi1 :: "'x prm"
  and   pi2 :: "'x prm"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE ('x)"
  shows "(pi1perm pi2)(pi1x) = pi1(pi2x)" 
  by (simp add: pt_fun_app_eq[OF pt, OF at])


lemma pt_fun_eq:
  fixes f  :: "'a'b"
  and   pi :: "'x prm"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "(pif = f) = ( x. pi(f x) = f (pix))" (is "?LHS = ?RHS")
proof
  assume a: "?LHS"
  show "?RHS"
  proof
    fix x
    have "pi(f x) = (pif)(pix)" by (simp add: pt_fun_app_eq[OF pt, OF at])
    also have " = f (pix)" using a by simp
    finally show "pi(f x) = f (pix)" by simp
  qed
next
  assume b: "?RHS"
  show "?LHS"
  proof (rule ccontr)
    assume "(pif)  f"
    hence "x. (pif) x  f x" by (simp add: fun_eq_iff)
    then obtain x where b1: "(pif) x  f x" by force
    from b have "pi(f ((rev pi)x)) = f (pi((rev pi)x))" by force
    hence "(pif)(pi((rev pi)x)) = f (pi((rev pi)x))" 
      by (simp add: pt_fun_app_eq[OF pt, OF at])
    hence "(pif) x = f x" by (simp add: pt_pi_rev[OF pt, OF at])
    with b1 show "False" by simp
  qed
qed

― ‹two helper lemmas for the equivariance of functions›
lemma pt_swap_eq_aux:
  fixes   y :: "'a"
  and    pi :: "'x prm"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     a: "(a::'x) (b::'x). [(a,b)]y = y"
  shows "piy = y"
proof(induct pi)
  case Nil show ?case by (simp add: pt1[OF pt])
next
  case (Cons x xs)
  have ih: "xsy = y" by fact
  obtain a b where p: "x=(a,b)" by force
  have "((a,b)#xs)y = ([(a,b)]@xs)y" by simp
  also have " = [(a,b)](xsy)" by (simp only: pt2[OF pt])
  finally show ?case using a ih p by simp
qed

lemma pt_swap_eq:
  fixes   y :: "'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  shows "((a::'x) (b::'x). [(a,b)]y = y) = (pi::'x prm. piy = y)"
  by (force intro: pt_swap_eq_aux[OF pt])

lemma pt_eqvt_fun1a:
  fixes f     :: "'a'b"
  assumes pta: "pt TYPE('a) TYPE('x)"
  and     ptb: "pt TYPE('b) TYPE('x)"
  and     at:  "at TYPE('x)"
  and     a:   "((supp f)::'x set)={}"
  shows "(pi::'x prm). pif = f" 
proof (intro strip)
  fix pi
  have "a b. a((supp f)::'x set)  b((supp f)::'x set)  (([(a,b)]f) = f)" 
    by (intro strip, fold fresh_def, 
      simp add: pt_fresh_fresh[OF pt_fun_inst[OF pta, OF ptb, OF at],OF at])
  with a have "(a::'x) (b::'x). ([(a,b)]f) = f" by force
  hence "(pi::'x prm). pif = f" 
    by (simp add: pt_swap_eq[OF pt_fun_inst[OF pta, OF ptb, OF at]])
  thus "(pi::'x prm)f = f" by simp
qed

lemma pt_eqvt_fun1b:
  fixes f     :: "'a'b"
  assumes a: "(pi::'x prm). pif = f"
  shows "((supp f)::'x set)={}"
using a by (simp add: supp_def)

lemma pt_eqvt_fun1:
  fixes f     :: "'a'b"
  assumes pta: "pt TYPE('a) TYPE('x)"
  and     ptb: "pt TYPE('b) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "(((supp f)::'x set)={}) = ((pi::'x prm). pif = f)" (is "?LHS = ?RHS")
by (rule iffI, simp add: pt_eqvt_fun1a[OF pta, OF ptb, OF at], simp add: pt_eqvt_fun1b)

lemma pt_eqvt_fun2a:
  fixes f     :: "'a'b"
  assumes pta: "pt TYPE('a) TYPE('x)"
  and     ptb: "pt TYPE('b) TYPE('x)"
  and     at: "at TYPE('x)"
  assumes a: "((supp f)::'x set)={}"
  shows "(pi::'x prm) (x::'a). pi(f x) = f(pix)" 
proof (intro strip)
  fix pi x
  from a have b: "(pi::'x prm). pif = f" by (simp add: pt_eqvt_fun1[OF pta, OF ptb, OF at]) 
  have "(pi::'x prm)(f x) = (pif)(pix)" by (simp add: pt_fun_app_eq[OF pta, OF at]) 
  with b show "(pi::'x prm)(f x) = f (pix)" by force 
qed

lemma pt_eqvt_fun2b:
  fixes f     :: "'a'b"
  assumes pt1: "pt TYPE('a) TYPE('x)"
  and     pt2: "pt TYPE('b) TYPE('x)"
  and     at: "at TYPE('x)"
  assumes a: "(pi::'x prm) (x::'a). pi(f x) = f(pix)"
  shows "((supp f)::'x set)={}"
proof -
  from a have "(pi::'x prm). pif = f" by (simp add: pt_fun_eq[OF pt1, OF at, symmetric])
  thus ?thesis by (simp add: supp_def)
qed

lemma pt_eqvt_fun2:
  fixes f     :: "'a'b"
  assumes pta: "pt TYPE('a) TYPE('x)"
  and     ptb: "pt TYPE('b) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "(((supp f)::'x set)={}) = ((pi::'x prm) (x::'a). pi(f x) = f(pix))" 
by (rule iffI, 
    simp add: pt_eqvt_fun2a[OF pta, OF ptb, OF at], 
    simp add: pt_eqvt_fun2b[OF pta, OF ptb, OF at])

lemma pt_supp_fun_subset:
  fixes f :: "'a'b"
  assumes pta: "pt TYPE('a) TYPE('x)"
  and     ptb: "pt TYPE('b) TYPE('x)"
  and     at: "at TYPE('x)" 
  and     f1: "finite ((supp f)::'x set)"
  and     f2: "finite ((supp x)::'x set)"
  shows "supp (f x)  (((supp f)(supp x))::'x set)"
proof -
  have s1: "((supp f)((supp x)::'x set)) supports (f x)"
  proof (simp add: supports_def, fold fresh_def, auto)
    fix a::"'x" and b::"'x"
    assume "af" and "bf"
    hence a1: "[(a,b)]f = f" 
      by (rule pt_fresh_fresh[OF pt_fun_inst[OF pta, OF ptb, OF at], OF at])
    assume "ax" and "bx"
    hence a2: "[(a,b)]x = x" by (rule pt_fresh_fresh[OF pta, OF at])
    from a1 a2 show "[(a,b)](f x) = (f x)" by (simp add: pt_fun_app_eq[OF pta, OF at])
  qed
  from f1 f2 have "finite ((supp f)((supp x)::'x set))" by force
  with s1 show ?thesis by (rule supp_is_subset)
qed
      
lemma pt_empty_supp_fun_subset:
  fixes f :: "'a'b"
  assumes pta: "pt TYPE('a) TYPE('x)"
  and     ptb: "pt TYPE('b) TYPE('x)"
  and     at:  "at TYPE('x)" 
  and     e:   "(supp f)=({}::'x set)"
  shows "supp (f x)  ((supp x)::'x set)"
proof (unfold supp_def, auto)
  fix a::"'x"
  assume a1: "finite {b. [(a, b)]x  x}"
  assume "infinite {b. [(a, b)](f x)  f x}"
  hence a2: "infinite {b. f ([(a, b)]x)  f x}" using e
    by (simp add: pt_eqvt_fun2[OF pta, OF ptb, OF at])
  have a3: "{b. f ([(a,b)]x)  f x}{b. [(a,b)]x  x}" by force
  from a1 a2 a3 show False by (force dest: finite_subset)
qed

section ‹Facts about the support of finite sets of finitely supported things›
(*=============================================================================*)

definition X_to_Un_supp :: "('a set)  'x set" where
  "X_to_Un_supp X  xX. ((supp x)::'x set)"

lemma UNION_f_eqvt:
  fixes X::"('a set)"
  and   f::"'a  'x set"
  and   pi::"'x prm"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "pi(xX. f x) = (x(piX). (pif) x)"
proof -
  have pt_x: "pt TYPE('x) TYPE('x)" by (force intro: at_pt_inst at)
  show ?thesis
  proof -
    have "x. (u. x = pi  u  u  X)  pi  z  (pi  f) x"
      if "y  X" and "z  f y" for y z
      using that by (metis assms at_pt_inst pt_fun_app_eq pt_set_bij)
    moreover have "u. x = pi  u  (xX. u  f x)"
      if "x  (pi  f) (pi  y)" and "y  X" for x y
      using that by (metis at at_pi_rev pt pt_fun_app_eq pt_set_bij1a pt_x)
    ultimately show ?thesis
      by (auto simp: perm_set_def)
  qed
qed

lemma X_to_Un_supp_eqvt:
  fixes X::"('a set)"
  and   pi::"'x prm"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "pi(X_to_Un_supp X) = ((X_to_Un_supp (piX))::'x set)"
  by (metis UNION_f_eqvt X_to_Un_supp_def assms pt_fun_eq pt_perm_supp)

lemma Union_supports_set:
  fixes X::"('a set)"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "(xX. ((supp x)::'x set)) supports X"
  by (simp add: assms fresh_def pt_fresh_fresh supports_set)

lemma Union_of_fin_supp_sets:
  fixes X::"('a set)"
  assumes fs: "fs TYPE('a) TYPE('x)" 
  and     fi: "finite X"   
  shows "finite (xX. ((supp x)::'x set))"
using fi by (induct, auto simp add: fs1[OF fs])

lemma Union_included_in_supp:
  fixes X::"('a set)"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  and     fs: "fs TYPE('a) TYPE('x)" 
  and     fi: "finite X"
  shows "(xX. ((supp x)::'x set))  supp X"
proof -
  have "supp ((X_to_Un_supp X)::'x set)  ((supp X)::'x set)"  
  proof (rule pt_empty_supp_fun_subset)
    show "supp (λa. X_to_Un_supp (a::'a set)::'x set) = ({}::'x set)"
    by (simp add: X_to_Un_supp_eqvt at at_pt_inst pt pt_eqvt_fun2b pt_set_inst)
  qed (use assms at_pt_inst pt_set_inst in auto)
  hence "supp (xX. ((supp x)::'x set))  ((supp X)::'x set)" by (simp add: X_to_Un_supp_def)
  moreover
  have "supp (xX. ((supp x)::'x set)) = (xX. ((supp x)::'x set))"
    using Union_of_fin_supp_sets at at_fin_set_supp fi fs by auto
  ultimately show ?thesis by force
qed

lemma supp_of_fin_sets:
  fixes X::"('a set)"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  and     fs: "fs TYPE('a) TYPE('x)" 
  and     fi: "finite X"
  shows "(supp X) = (xX. ((supp x)::'x set))"
proof (rule equalityI)
  have "finite ( (supp ` X)::'x set)"
    using Union_of_fin_supp_sets fi fs by blast
  then show "(supp X::'x set)   (supp ` X)"
    by (metis Union_supports_set at pt supp_is_subset)
next
  show "(xX. (supp x::'x set))  supp X"
    by (simp add: Union_included_in_supp at fi fs pt)
qed

lemma supp_fin_union:
  fixes X::"('a set)"
  and   Y::"('a set)"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  and     fs: "fs TYPE('a) TYPE('x)" 
  and     f1: "finite X"
  and     f2: "finite Y"
  shows "(supp (XY)) = (supp X)((supp Y)::'x set)"
using f1 f2 by (force simp add: supp_of_fin_sets[OF pt, OF at, OF fs])

lemma supp_fin_insert:
  fixes X::"('a set)"
  and   x::"'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  and     fs: "fs TYPE('a) TYPE('x)" 
  and     f:  "finite X"
  shows "(supp (insert x X)) = (supp x)((supp X)::'x set)"
proof -
  have "(supp (insert x X)) = ((supp ({x}(X::'a set)))::'x set)" by simp
  also have " = (supp {x})(supp X)"
    by (rule supp_fin_union[OF pt, OF at, OF fs], simp_all add: f)
  finally show "(supp (insert x X)) = (supp x)((supp X)::'x set)" 
    by (simp add: supp_singleton)
qed

lemma fresh_fin_union:
  fixes X::"('a set)"
  and   Y::"('a set)"
  and   a::"'x"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  and     fs: "fs TYPE('a) TYPE('x)" 
  and     f1: "finite X"
  and     f2: "finite Y"
  shows "a(XY) = (aX  aY)"
  by (simp add: assms fresh_def supp_fin_union)

lemma fresh_fin_insert:
  fixes X::"('a set)"
  and   x::"'a"
  and   a::"'x"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  and     fs: "fs TYPE('a) TYPE('x)" 
  and     f:  "finite X"
  shows "a(insert x X) = (ax  aX)"
  by (simp add: assms fresh_def supp_fin_insert)

lemma fresh_fin_insert1:
  fixes X::"('a set)"
  and   x::"'a"
  and   a::"'x"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  and     fs: "fs TYPE('a) TYPE('x)" 
  and     f:  "finite X"
  and     a1:  "ax"
  and     a2:  "aX"
  shows "a(insert x X)"
  using a1 a2
  by (simp add: fresh_fin_insert[OF pt, OF at, OF fs, OF f])

lemma pt_list_set_supp:
  fixes xs :: "'a list"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  and     fs: "fs TYPE('a) TYPE('x)"
  shows "supp (set xs) = ((supp xs)::'x set)"
proof -
  have "supp (set xs) = (x(set xs). ((supp x)::'x set))"
    by (rule supp_of_fin_sets[OF pt, OF at, OF fs], rule finite_set)
  also have "(x(set xs). ((supp x)::'x set)) = (supp xs)"
  proof(induct xs)
    case Nil show ?case by (simp add: supp_list_nil)
  next
    case (Cons h t) thus ?case by (simp add: supp_list_cons)
  qed
  finally show ?thesis by simp
qed
    
lemma pt_list_set_fresh:
  fixes a :: "'x"
  and   xs :: "'a list"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  and     fs: "fs TYPE('a) TYPE('x)"
  shows "a(set xs) = axs"
by (simp add: fresh_def pt_list_set_supp[OF pt, OF at, OF fs])


section ‹generalisation of freshness to lists and sets of atoms›
(*================================================================*)
 
consts
  fresh_star :: "'b  'a  bool" (‹_ ♯* _› [100,100] 100)

overloading fresh_star_set  "fresh_star :: 'b set  'a  bool"
begin
  definition fresh_star_set: "xs♯*c  x::'bxs. x(c::'a)"
end

overloading frsh_star_list  "fresh_star :: 'b list  'a  bool"
begin
  definition fresh_star_list: "xs♯*c  x::'bset xs. x(c::'a)"
end

lemmas fresh_star_def = fresh_star_list fresh_star_set

lemma fresh_star_prod_set:
  fixes xs::"'a set"
  shows "xs♯*(a,b) = (xs♯*a  xs♯*b)"
by (auto simp add: fresh_star_def fresh_prod)

lemma fresh_star_prod_list:
  fixes xs::"'a list"
  shows "xs♯*(a,b) = (xs♯*a  xs♯*b)"
  by (auto simp add: fresh_star_def fresh_prod)

lemmas fresh_star_prod = fresh_star_prod_list fresh_star_prod_set

lemma fresh_star_set_eq: "set xs ♯* c = xs ♯* c"
  by (simp add: fresh_star_def)

lemma fresh_star_Un_elim:
  "((S  T) ♯* c  PROP C)  (S ♯* c  T ♯* c  PROP C)"
proof
  assume §: "(S  T) ♯* c  PROP C" and c: "S ♯* c" "T ♯* c"
  show "PROP C"
    using c by (intro §) (metis Un_iff fresh_star_set)
qed (auto simp: fresh_star_def)

lemma fresh_star_insert_elim:
  "(insert x S ♯* c  PROP C)  (x  c  S ♯* c  PROP C)"
  by rule (simp_all add: fresh_star_def)

lemma fresh_star_empty_elim:
  "({} ♯* c  PROP C)  PROP C"
  by (simp add: fresh_star_def)

text ‹Normalization of freshness results; see \ nominal_induct›

lemma fresh_star_unit_elim: 
  shows "((a::'a set)♯*()  PROP C)  PROP C"
  and "((b::'a list)♯*()  PROP C)  PROP C"
  by (simp_all add: fresh_star_def fresh_def supp_unit)

lemma fresh_star_prod_elim: 
  shows "((a::'a set)♯*(x,y)  PROP C)  (a♯*x  a♯*y  PROP C)"
  and "((b::'a list)♯*(x,y)  PROP C)  (b♯*x  b♯*y  PROP C)"
  by (rule, simp_all add: fresh_star_prod)+


lemma pt_fresh_star_bij_ineq:
  fixes  pi :: "'x prm"
  and     x :: "'a"
  and     a :: "'y set"
  and     b :: "'y list"
  assumes pta: "pt TYPE('a) TYPE('x)"
  and     ptb: "pt TYPE('y) TYPE('x)"
  and     at:  "at TYPE('x)"
  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  shows "(pia)♯*(pix) = a♯*x"
  and   "(pib)♯*(pix) = b♯*x"
  unfolding fresh_star_def
proof -
  have "y  x" if "zpi  a. z  pi  x" and "y  a" for y
    using that by (meson assms at pt_fresh_bij_ineq pt_set_bij2)
  moreover have "y  pi  x" if "za. z  x" and "y  pi  a" for y
    using that by (simp add: assms pt_fresh_left_ineq pt_set_bij1a)
  moreover have "y  x"
    if "zset (pi  b). z  pi  x" and "y  set b" for y
    using that by (metis at cp pt_fresh_bij_ineq pt_set_bij pta ptb set_eqvt)
  moreover have "y  pi  x"
    if "zset b. z  x" and "y  set (pi  b)" for y
    using that by (metis at cp pt_fresh_left_ineq pt_set_bij1a pta ptb set_eqvt)
  ultimately show "(xapi  a. xa  pi  x) = (xaa. xa  x)" "(xaset (pi  b). xa  pi  x) = (xaset b. xa  x)"
    by blast+
qed


lemma pt_fresh_star_bij:
  fixes  pi :: "'x prm"
  and     x :: "'a"
  and     a :: "'x set"
  and     b :: "'x list"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "(pia)♯*(pix) = a♯*x"
  and   "(pib)♯*(pix) = b♯*x"
proof (rule pt_fresh_star_bij_ineq)
  show "(pi  b) ♯* (pi  x) = b ♯* x"
  by (simp add: at at_pt_inst cp_pt_inst pt pt_fresh_star_bij_ineq)
qed (auto simp: at pt at_pt_inst cp_pt_inst)

lemma pt_fresh_star_eqvt:
  fixes  pi :: "'x prm"
  and     x :: "'a"
  and     a :: "'x set"
  and     b :: "'x list"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "pi(a♯*x) = (pia)♯*(pix)"
  and   "pi(b♯*x) = (pib)♯*(pix)"
  by (simp_all add: perm_bool pt_fresh_star_bij[OF pt, OF at])

lemma pt_fresh_star_eqvt_ineq:
  fixes pi::"'x prm"
  and   a::"'y set"
  and   b::"'y list"
  and   x::"'a"
  assumes pta: "pt TYPE('a) TYPE('x)"
  and     ptb: "pt TYPE('y) TYPE('x)"
  and     at:  "at TYPE('x)"
  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  and     dj:  "disjoint TYPE('y) TYPE('x)"
  shows "pi(a♯*x) = (pia)♯*(pix)"
  and   "pi(b♯*x) = (pib)♯*(pix)"
  by (simp_all add: pt_fresh_star_bij_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj] perm_bool)

lemma pt_freshs_freshs:
  assumes pt: "pt TYPE('a) TYPE('x)"
  and at: "at TYPE ('x)"
  and pi: "set (pi::'x prm)  Xs × Ys"
  and Xs: "Xs ♯* (x::'a)"
  and Ys: "Ys ♯* x"
  shows "pix = x"
  using pi
proof (induct pi)
  case Nil
  show ?case by (simp add: pt1 [OF pt])
next
  case (Cons p pi)
  obtain a b where p: "p = (a, b)" by (cases p)
  with Cons Xs Ys have "a  x" "b  x"
    by (simp_all add: fresh_star_def)
  with Cons p show ?case
    by (simp add: pt_fresh_fresh [OF pt at]
      pt2 [OF pt, of "[(a, b)]" pi, simplified])
qed

lemma pt_fresh_star_pi: 
  fixes x::"'a"
  and   pi::"'x prm"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  and     a: "((supp x)::'x set)♯* pi"
  shows "pix = x"
using a
apply(induct pi)
  apply (simp add: assms(1) pt1)
apply(auto simp add: fresh_star_def fresh_list_cons fresh_prod pt1[OF pt])
  by (metis Cons_eq_append_conv append_self_conv2 assms(1) at at_fresh fresh_def pt2 pt_fresh_fresh)

section ‹Infrastructure lemmas for strong rule inductions›
(*==========================================================*)

text ‹
  For every set of atoms, there is another set of atoms
  avoiding a finitely supported c and there is a permutation
  which 'translates' between both sets.
›

lemma at_set_avoiding_aux:
  fixes Xs::"'a set"
  and   As::"'a set"
  assumes at: "at TYPE('a)"
  and     b: "Xs  As"
  and     c: "finite As"
  and     d: "finite ((supp c)::'a set)"
  shows "(pi::'a prm). (piXs)♯*c  (piXs)  As = {}  set pi  Xs × (piXs)"
proof -
  from b c have "finite Xs" by (simp add: finite_subset)
  then show ?thesis using b 
  proof (induct)
    case empty
    have "({}::'a set)♯*c" by (simp add: fresh_star_def)
    moreover
    have "({}::'a set)  As = {}" by simp
    moreover
    have "set ([]::'a prm)  {} × {}" by simp
    ultimately show ?case by (simp add: empty_eqvt)
  next
    case (insert x Xs)
    then have ih: "pi. (piXs)♯*c  (piXs)  As = {}  set pi  Xs × (piXs)" by simp
    then obtain pi where a1: "(piXs)♯*c" and a2: "(piXs)  As = {}" and 
      a4: "set pi  Xs × (piXs)" by blast
    have b: "xXs" by fact
    have d1: "finite As" by fact
    have d2: "finite Xs" by fact
    have d3: "({x}  Xs)  As" using insert(4) by simp
    from d d1 d2
    obtain y::"'a" where fr: "y(c,piXs,As)" 
      apply(rule_tac at_exists_fresh[OF at, where x="(c,piXs,As)"])
      apply(auto simp add: supp_prod at_supp[OF at] at_fin_set_supp[OF at]
        pt_supp_finite_pi[OF pt_set_inst[OF at_pt_inst[OF at]] at])
      done
    have "({y}(piXs))♯*c" using a1 fr by (simp add: fresh_star_def)
    moreover
    have "({y}(piXs))As = {}" using a2 d1 fr 
      by (simp add: fresh_prod at_fin_set_fresh[OF at])
    moreover
    have "pix=x" using a4 b a2 d3 
      by (rule_tac at_prm_fresh2[OF at]) (auto)
    then have "set ((pix,y)#pi)  ({x}  Xs) × ({y}(piXs))" using a4 by auto
    moreover
    have "(((pix,y)#pi)({x}  Xs)) = {y}(piXs)"
    proof -
      have eq: "[(pix,y)](piXs) = (piXs)" 
      proof -
        have "(pix)(piXs)" using b d2 
          by (simp add: pt_fresh_bij [OF pt_set_inst [OF at_pt_inst [OF at]], OF at]
            at_fin_set_fresh [OF at])
        moreover
        have "y(piXs)" using fr by simp
        ultimately show "[(pix,y)](piXs) = (piXs)" 
          by (simp add: pt_fresh_fresh[OF pt_set_inst
            [OF at_pt_inst[OF at]], OF at])
      qed
      have "(((pix,y)#pi)({x}Xs)) = ([(pix,y)](pi({x}Xs)))"
        by (simp add: pt2[symmetric, OF pt_set_inst [OF at_pt_inst[OF at]]])
      also have " = {y}([(pix,y)](piXs))" 
        by (simp only: union_eqvt perm_set_def at_calc[OF at])(auto)
      finally show "(((pix,y)#pi)({x}  Xs)) = {y}(piXs)" using eq by simp
    qed
    ultimately 
    show ?case by (rule_tac x="(pix,y)#pi" in exI) (auto)
  qed
qed

lemma at_set_avoiding:
  fixes Xs::"'a set"
  assumes at: "at TYPE('a)"
  and     a: "finite Xs"
  and     b: "finite ((supp c)::'a set)"
  obtains pi::"'a prm" where "(piXs)♯*c" and "set pi  Xs × (piXs)"
using a b at_set_avoiding_aux[OF at, where Xs="Xs" and As="Xs" and c="c"]
by (blast)

section ‹composition instances›
(* ============================= *)

lemma cp_list_inst:
  assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
  shows "cp TYPE ('a list) TYPE('x) TYPE('y)"
using c1
apply(clarsimp simp add: cp_def)
  by (induct_tac x) auto

lemma cp_set_inst:
  assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
  shows "cp TYPE ('a set) TYPE('x) TYPE('y)"
  using c1
  unfolding cp_def perm_set_def
  by (smt (verit) Collect_cong mem_Collect_eq)


lemma cp_option_inst:
  assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
  shows "cp TYPE ('a option) TYPE('x) TYPE('y)"
  using c1 unfolding cp_def by (metis none_eqvt not_None_eq some_eqvt)

lemma cp_noption_inst:
  assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
  shows "cp TYPE ('a noption) TYPE('x) TYPE('y)"
  using c1 unfolding cp_def
  by (metis nnone_eqvt noption.exhaust nsome_eqvt)

lemma cp_unit_inst:
  shows "cp TYPE (unit) TYPE('x) TYPE('y)"
  by (simp add: cp_def)

lemma cp_bool_inst:
  shows "cp TYPE (bool) TYPE('x) TYPE('y)"
  apply(clarsimp simp add: cp_def)
  by (induct_tac x) auto

lemma cp_prod_inst:
  assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
  and     c2: "cp TYPE ('b) TYPE('x) TYPE('y)"
  shows "cp TYPE ('a×'b) TYPE('x) TYPE('y)"
using c1 c2
  by (simp add: cp_def)

lemma cp_fun_inst:
  assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
  and     c2: "cp TYPE ('b) TYPE('x) TYPE('y)"
  and     pt: "pt TYPE ('y) TYPE('x)"
  and     at: "at TYPE ('x)"
  shows "cp TYPE ('a'b) TYPE('x) TYPE('y)"
  using c1 c2
  by(auto simp add: cp_def perm_fun_def fun_eq_iff at pt pt_list_inst pt_prod_inst pt_rev_pi rev_eqvt)


section ‹Andy's freshness lemma›
(*================================*)

lemma freshness_lemma:
  fixes h :: "'x'a"
  assumes pta: "pt TYPE('a) TYPE('x)"
  and     at:  "at TYPE('x)" 
  and     f1:  "finite ((supp h)::'x set)"
  and     a: "a::'x. a(h,h a)"
  shows  "fr::'a. a::'x. ah  (h a) = fr"
proof -
  have ptb: "pt TYPE('x) TYPE('x)" by (simp add: at_pt_inst[OF at]) 
  have ptc: "pt TYPE('x'a) TYPE('x)" by (simp add: pt_fun_inst[OF ptb, OF pta, OF at]) 
  from a obtain a0 where a1: "a0h" and a2: "a0(h a0)" by (force simp add: fresh_prod)
  show ?thesis
  proof
    let ?fr = "h (a0::'x)"
    show "(a::'x). (ah  ((h a) = ?fr))" 
    proof (intro strip)
      fix a
      assume a3: "(a::'x)h"
      show "h (a::'x) = h a0"
      proof (cases "a=a0")
        case True thus "h (a::'x) = h a0" by simp
      next
        case False 
        assume "aa0"
        hence c1: "a((supp a0)::'x set)" by  (simp add: fresh_def[symmetric] at_fresh[OF at])
        have c2: "a((supp h)::'x set)" using a3 by (simp add: fresh_def)
        from c1 c2 have c3: "a((supp h)((supp a0)::'x set))" by force
        have f2: "finite ((supp a0)::'x set)" by (simp add: at_supp[OF at])
        from f1 f2 have "((supp (h a0))::'x set)((supp h)(supp a0))"
          by (simp add: pt_supp_fun_subset[OF ptb, OF pta, OF at])
        hence "a((supp (h a0))::'x set)" using c3 by force
        hence "a(h a0)" by (simp add: fresh_def) 
        with a2 have d1: "[(a0,a)](h a0) = (h a0)" by (rule pt_fresh_fresh[OF pta, OF at])
        from a1 a3 have d2: "[(a0,a)]h = h" by (rule pt_fresh_fresh[OF ptc, OF at])
        from d1 have "h a0 = [(a0,a)](h a0)" by simp
        also have "= ([(a0,a)]h)([(a0,a)]a0)" by (simp add: pt_fun_app_eq[OF ptb, OF at])
        also have " = h ([(a0,a)]a0)" using d2 by simp
        also have " = h a" by (simp add: at_calc[OF at])
        finally show "h a = h a0" by simp
      qed
    qed
  qed
qed

lemma freshness_lemma_unique:
  fixes h :: "'x'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)" 
  and     f1: "finite ((supp h)::'x set)"
  and     a: "(a::'x). a(h,h a)"
  shows  "∃!(fr::'a). (a::'x). ah  (h a) = fr"
proof (rule ex_ex1I)
  from pt at f1 a show "fr::'a. a::'x. ah  h a = fr" by (simp add: freshness_lemma)
next
  fix fr1 fr2
  assume b1: "a::'x. ah  h a = fr1"
  assume b2: "a::'x. ah  h a = fr2"
  from a obtain a where "(a::'x)h" by (force simp add: fresh_prod) 
  with b1 b2 have "h a = fr1  h a = fr2" by force
  thus "fr1 = fr2" by force
qed

― ‹packaging the freshness lemma into a function›
definition fresh_fun :: "('x'a)'a" where
  "fresh_fun (h)  THE fr. ((a::'x). ah  (h a) = fr)"

lemma fresh_fun_app:
  fixes h :: "'x'a"
  and   a :: "'x"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)" 
  and     f1: "finite ((supp h)::'x set)"
  and     a: "(a::'x). a(h,h a)"
  and     b: "ah"
  shows "(fresh_fun h) = (h a)"
proof (unfold fresh_fun_def, rule the_equality)
  show "(a'::'x). a'h  h a' = h a"
  proof (intro strip)
    fix a'::"'x"
    assume c: "a'h"
    from pt at f1 a have "(fr::'a). (a::'x). ah  (h a) = fr" by (rule freshness_lemma)
    with b c show "h a' = h a" by force
  qed
next
  fix fr::"'a"
  assume "a. ah  h a = fr"
  with b show "fr = h a" by force
qed

lemma fresh_fun_app':
  fixes h :: "'x'a"
  and   a :: "'x"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)" 
  and     f1: "finite ((supp h)::'x set)"
  and     a: "ah" "ah a"
  shows "(fresh_fun h) = (h a)"
  by (meson assms fresh_fun_app fresh_prod pt)

lemma fresh_fun_equiv_ineq:
  fixes h :: "'y'a"
  and   pi:: "'x prm"
  assumes pta: "pt TYPE('a) TYPE('x)"
  and     ptb: "pt TYPE('y) TYPE('x)"
  and     ptb':"pt TYPE('a) TYPE('y)"
  and     at:  "at TYPE('x)" 
  and     at': "at TYPE('y)"
  and     cpa: "cp TYPE('a) TYPE('x) TYPE('y)"
  and     cpb: "cp TYPE('y) TYPE('x) TYPE('y)"
  and     f1: "finite ((supp h)::'y set)"
  and     a1: "(a::'y). a(h,h a)"
  shows "pi(fresh_fun h) = fresh_fun(pih)" (is "?LHS = ?RHS")
proof -
  have ptd: "pt TYPE('y) TYPE('y)" by (simp add: at_pt_inst[OF at']) 
  have ptc: "pt TYPE('y'a) TYPE('x)" by (simp add: pt_fun_inst[OF ptb, OF pta, OF at]) 
  have cpc: "cp TYPE('y'a) TYPE ('x) TYPE ('y)" by (rule cp_fun_inst[OF cpb cpa ptb at])
  have f2: "finite ((supp (pih))::'y set)"
  proof -
    from f1 have "finite (pi((supp h)::'y set))"
      by (simp add: pt_set_finite_ineq[OF ptb, OF at])
    thus ?thesis
      by (simp add: pt_perm_supp_ineq[OF ptc, OF ptb, OF at, OF cpc])
  qed
  from a1 obtain a' where c0: "a'(h,h a')" by force
  hence c1: "a'h" and c2: "a'(h a')" by (simp_all add: fresh_prod)
  have c3: "(pia')(pih)" using c1
  by (simp add: pt_fresh_bij_ineq[OF ptc, OF ptb, OF at, OF cpc])
  have c4: "(pia')(pih) (pia')"
  proof -
    from c2 have "(pia')(pi(h a'))"
      by (simp add: pt_fresh_bij_ineq[OF pta, OF ptb, OF at,OF cpa])
    thus ?thesis by (simp add: pt_fun_app_eq[OF ptb, OF at])
  qed
  have a2: "(a::'y). a(pih,(pih) a)" using c3 c4 by (force simp add: fresh_prod)
  have d1: "?LHS = pi(h a')" using c1 a1 by (simp add: fresh_fun_app[OF ptb', OF at', OF f1])
  have d2: "?RHS = (pih) (pia')" using c3 a2 
    by (simp add: fresh_fun_app[OF ptb', OF at', OF f2])
  show ?thesis using d1 d2 by (simp add: pt_fun_app_eq[OF ptb, OF at])
qed

lemma fresh_fun_equiv:
  fixes h :: "'x'a"
  and   pi:: "'x prm"
  assumes pta: "pt TYPE('a) TYPE('x)"
  and     at:  "at TYPE('x)" 
  and     f1:  "finite ((supp h)::'x set)"
  and     a1: "(a::'x). a(h,h a)"
  shows "pi(fresh_fun h) = fresh_fun(pih)" (is "?LHS = ?RHS")
proof -
  have ptb: "pt TYPE('x) TYPE('x)" by (simp add: at_pt_inst[OF at]) 
  have ptc: "pt TYPE('x'a) TYPE('x)" by (simp add: pt_fun_inst[OF ptb, OF pta, OF at]) 
  have f2: "finite ((supp (pih))::'x set)"
  proof -
    from f1 have "finite (pi((supp h)::'x set))" by (simp add: pt_set_finite_ineq[OF ptb, OF at])
    thus ?thesis by (simp add: pt_perm_supp[OF ptc, OF at])
  qed
  from a1 obtain a' where c0: "a'(h,h a')" by force
  hence c1: "a'h" and c2: "a'(h a')" by (simp_all add: fresh_prod)
  have c3: "(pia')(pih)" using c1 by (simp add: pt_fresh_bij[OF ptc, OF at])
  have c4: "(pia')(pih) (pia')"
  proof -
    from c2 have "(pia')(pi(h a'))" by (simp add: pt_fresh_bij[OF pta, OF at])
    thus ?thesis by (simp add: pt_fun_app_eq[OF ptb, OF at])
  qed
  have a2: "(a::'x). a(pih,(pih) a)" using c3 c4 by (force simp add: fresh_prod)
  have d1: "?LHS = pi(h a')" using c1 a1 by (simp add: fresh_fun_app[OF pta, OF at, OF f1])
  have d2: "?RHS = (pih) (pia')" using c3 a2 by (simp add: fresh_fun_app[OF pta, OF at, OF f2])
  show ?thesis using d1 d2 by (simp add: pt_fun_app_eq[OF ptb, OF at])
qed

lemma fresh_fun_supports:
  fixes h :: "'x'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)" 
  and     f1: "finite ((supp h)::'x set)"
  and     a: "(a::'x). a(h,h a)"
  shows "((supp h)::'x set) supports (fresh_fun h)"
  by(simp flip: fresh_def add: supports_def assms at_pt_inst fresh_fun_equiv pt_fresh_fresh pt_fun_inst)
  
section ‹Abstraction function›
(*==============================*)

lemma pt_abs_fun_inst:
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "pt TYPE('x('a noption)) TYPE('x)"
  by (simp add: at at_pt_inst pt pt_fun_inst pt_noption_inst)

definition abs_fun :: "'x'a('x('a noption))" ([_]._› [100,100] 100) where 
  "[a].x  (λb. (if b=a then nSome(x) else (if bx then nSome([(a,b)]x) else nNone)))"

(* FIXME: should be called perm_if and placed close to the definition of permutations on bools *)
lemma abs_fun_if: 
  fixes pi :: "'x prm"
  and   x  :: "'a"
  and   y  :: "'a"
  and   c  :: "bool"
  shows "pi(if c then x else y) = (if c then (pix) else (piy))"   
  by force

lemma abs_fun_pi_ineq:
  fixes a  :: "'y"
  and   x  :: "'a"
  and   pi :: "'x prm"
  assumes pta: "pt TYPE('a) TYPE('x)"
  and     ptb: "pt TYPE('y) TYPE('x)"
  and     at:  "at TYPE('x)"
  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
shows "pi([a].x) = [(pia)].(pix)"
  unfolding fun_eq_iff
proof
  fix y
  have "(((rev pi)y) = a) = (y = pia)"
    by (metis at pt_rev_pi ptb)
  moreover
  have "(((rev pi)y)x) = (y(pix))"
    by (simp add: assms pt_fresh_left_ineq)
  moreover
  have "pi([(a,(rev pi)y)]x) = [(pia,y)](pix)"
    using assms cp1[OF cp] by (simp add: pt_pi_rev)
  ultimately
  show "(pi  [a].x) y = ([(pi  a)].(pi  x)) y"
    by (simp add: abs_fun_def perm_fun_def)
qed

lemma abs_fun_pi:
  fixes a  :: "'x"
  and   x  :: "'a"
  and   pi :: "'x prm"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "pi([a].x) = [(pia)].(pix)"
  by (simp add: abs_fun_pi_ineq at at_pt_inst cp_pt_inst pt)

lemma abs_fun_eq1: 
  fixes x  :: "'a"
  and   y  :: "'a"
  and   a  :: "'x"
  shows "([a].x = [a].y) = (x = y)"
  by (metis abs_fun_def noption.inject)

lemma abs_fun_eq2:
  fixes x  :: "'a"
  and   y  :: "'a"
  and   a  :: "'x"
  and   b  :: "'x"
  assumes pt: "pt TYPE('a) TYPE('x)"
      and at: "at TYPE('x)"
      and a1: "ab" 
      and a2: "[a].x = [b].y" 
  shows "x=[(a,b)]y  ay"
proof -
  from a2 have "c::'x. ([a].x) c = ([b].y) c" by (force simp add: fun_eq_iff)
  hence "([a].x) a = ([b].y) a" by simp
  hence a3: "nSome(x) = ([b].y) a" by (simp add: abs_fun_def)
  show "x=[(a,b)]y  ay"
  proof (cases "ay")
    assume a4: "ay"
    hence "x=[(b,a)]y" using a3 a1 by (simp add: abs_fun_def)
    moreover
    have "[(a,b)]y = [(b,a)]y" by (rule pt3[OF pt], rule at_ds5[OF at])
    ultimately show ?thesis using a4 by simp
  next
    assume "¬ay"
    hence "nSome(x) = nNone" using a1 a3 by (simp add: abs_fun_def)
    hence False by simp
    thus ?thesis by simp
  qed
qed

lemma abs_fun_eq3: 
  fixes x  :: "'a"
  and   y  :: "'a"
  and   a   :: "'x"
  and   b   :: "'x"
  assumes pt: "pt TYPE('a) TYPE('x)"
      and at: "at TYPE('x)"
      and a1: "ab" 
      and a2: "x=[(a,b)]y" 
      and a3: "ay" 
  shows "[a].x =[b].y"
proof -
  show ?thesis 
  proof (simp only: abs_fun_def fun_eq_iff, intro strip)
    fix c::"'x"
    let ?LHS = "if c=a then nSome(x) else if cx then nSome([(a,c)]x) else nNone"
    and ?RHS = "if c=b then nSome(y) else if cy then nSome([(b,c)]y) else nNone"
    show "?LHS=?RHS"
    proof -
      have "(c=a)  (c=b)  (ca  cb)" by blast
      moreover  ― ‹case c=a›
      { have "nSome(x) = nSome([(a,b)]y)" using a2 by simp
        also have " = nSome([(b,a)]y)" by (simp, rule pt3[OF pt], rule at_ds5[OF at])
        finally have "nSome(x) = nSome([(b,a)]y)" by simp
        moreover
        assume "c=a"
        ultimately have "?LHS=?RHS" using a1 a3 by simp
      }
      moreover  ― ‹case c=b›
      { have a4: "y=[(a,b)]x" using a2 by (simp only: pt_swap_bij[OF pt, OF at])
        hence "a([(a,b)]x)" using a3 by simp
        hence "bx" by (simp add: at_calc[OF at] pt_fresh_left[OF pt, OF at])
        moreover
        assume "c=b"
        ultimately have "?LHS=?RHS" using a1 a4 by simp
      }
      moreover  ― ‹case c≠a ∧ c≠b›
      { assume a5: "ca  cb"
        moreover 
        have "cx = cy" using a2 a5 by (force simp add: at_calc[OF at] pt_fresh_left[OF pt, OF at])
        moreover 
        have "cy  [(a,c)]x = [(b,c)]y" 
        proof (intro strip)
          assume a6: "cy"
          have "[(a,c),(b,c),(a,c)]  [(a,b)]" using a1 a5 by (force intro: at_ds3[OF at])
          hence "[(a,c)]([(b,c)]([(a,c)]y)) = [(a,b)]y" 
            by (simp add: pt2[OF pt, symmetric] pt3[OF pt])
          hence "[(a,c)]([(b,c)]y) = [(a,b)]y" using a3 a6 
            by (simp add: pt_fresh_fresh[OF pt, OF at])
          hence "[(a,c)]([(b,c)]y) = x" using a2 by simp
          hence "[(b,c)]y = [(a,c)]x" by (drule_tac pt_bij1[OF pt, OF at], simp)
          thus "[(a,c)]x = [(b,c)]y" by simp
        qed
        ultimately have "?LHS=?RHS" by simp
      }
      ultimately show "?LHS = ?RHS" by blast
    qed
  qed
qed
        
(* alpha equivalence *)
lemma abs_fun_eq: 
  fixes x  :: "'a"
  and   y  :: "'a"
  and   a  :: "'x"
  and   b  :: "'x"
  assumes pt: "pt TYPE('a) TYPE('x)"
      and at: "at TYPE('x)"
  shows "([a].x = [b].y) = ((a=b  x=y)(ab  x=[(a,b)]y  ay))"
proof (rule iffI)
  assume b: "[a].x = [b].y"
  show "(a=b  x=y)(ab  x=[(a,b)]y  ay)"
  proof (cases "a=b")
    case True with b show ?thesis by (simp add: abs_fun_eq1)
  next
    case False with b show ?thesis by (simp add: abs_fun_eq2[OF pt, OF at])
  qed
next
  assume "(a=b  x=y)(ab  x=[(a,b)]y  ay)"
  thus "[a].x = [b].y"
  proof
    assume "a=b  x=y" thus ?thesis by simp
  next
    assume "ab  x=[(a,b)]y  ay" 
    thus ?thesis by (simp add: abs_fun_eq3[OF pt, OF at])
  qed
qed

(* symmetric version of alpha-equivalence *)
lemma abs_fun_eq': 
  fixes x  :: "'a"
  and   y  :: "'a"
  and   a  :: "'x"
  and   b  :: "'x"
  assumes pt: "pt TYPE('a) TYPE('x)"
      and at: "at TYPE('x)"
  shows "([a].x = [b].y) = ((a=b  x=y)(ab  [(b,a)]x=y  bx))"
by (auto simp add: abs_fun_eq[OF pt, OF at] pt_swap_bij'[OF pt, OF at] 
                   pt_fresh_left[OF pt, OF at] 
                   at_calc[OF at])

(* alpha_equivalence with a fresh name *)
lemma abs_fun_fresh: 
  fixes x :: "'a"
  and   y :: "'a"
  and   c :: "'x"
  and   a :: "'x"
  and   b :: "'x"
  assumes pt: "pt TYPE('a) TYPE('x)"
      and at: "at TYPE('x)"
      and fr: "ca" "cb" "cx" "cy" 
  shows "([a].x = [b].y) = ([(a,c)]x = [(b,c)]y)"
proof (rule iffI)
  assume eq0: "[a].x = [b].y"
  show "[(a,c)]x = [(b,c)]y"
  proof (cases "a=b")
    case True then show ?thesis using eq0 by (simp add: pt_bij[OF pt, OF at] abs_fun_eq[OF pt, OF at])
  next
    case False 
    have ineq: "ab" by fact
    with eq0 have eq: "x=[(a,b)]y" and fr': "ay" by (simp_all add: abs_fun_eq[OF pt, OF at])
    from eq have "[(a,c)]x = [(a,c)][(a,b)]y" by (simp add: pt_bij[OF pt, OF at])
    also have " = ([(a,c)][(a,b)])([(a,c)]y)" by (rule pt_perm_compose[OF pt, OF at])
    also have " = [(c,b)]y" using ineq fr fr' 
      by (simp add: pt_fresh_fresh[OF pt, OF at] at_calc[OF at])
    also have " = [(b,c)]y" by (rule pt3[OF pt], rule at_ds5[OF at])
    finally show ?thesis by simp
  qed
next
  assume eq: "[(a,c)]x = [(b,c)]y"
  thus "[a].x = [b].y"
  proof (cases "a=b")
    case True then show ?thesis using eq by (simp add: pt_bij[OF pt, OF at] abs_fun_eq[OF pt, OF at])
  next
    case False
    have ineq: "ab" by fact
    from fr have "([(a,c)]c)([(a,c)]x)" by (simp add: pt_fresh_bij[OF pt, OF at])
    hence "a([(b,c)]y)" using eq fr by (simp add: at_calc[OF at])
    hence fr0: "ay" using ineq fr by (simp add: pt_fresh_left[OF pt, OF at] at_calc[OF at])
    from eq have "x = (rev [(a,c)])([(b,c)]y)" by (rule pt_bij1[OF pt, OF at])
    also have " = [(a,c)]([(b,c)]y)" by simp
    also have " = ([(a,c)][(b,c)])([(a,c)]y)" by (rule pt_perm_compose[OF pt, OF at])
    also have " = [(b,a)]y" using ineq fr fr0  
      by (simp add: pt_fresh_fresh[OF pt, OF at] at_calc[OF at])
    also have " = [(a,b)]y" by (rule pt3[OF pt], rule at_ds5[OF at])
    finally show ?thesis using ineq fr0 by (simp add: abs_fun_eq[OF pt, OF at])
  qed
qed

lemma abs_fun_fresh': 
  fixes x :: "'a"
  and   y :: "'a"
  and   c :: "'x"
  and   a :: "'x"
  and   b :: "'x"
  assumes pt: "pt TYPE('a) TYPE('x)"
      and at: "at TYPE('x)"
      and as: "[a].x = [b].y"
      and fr: "ca" "cb" "cx" "cy" 
  shows "x = [(a,c)][(b,c)]y"
  using assms by (metis abs_fun_fresh pt_swap_bij)

lemma abs_fun_supp_approx:
  fixes x :: "'a"
  and   a :: "'x"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "((supp ([a].x))::'x set)  (supp (x,a))"
proof 
  fix c
  assume "c((supp ([a].x))::'x set)"
  hence "infinite {b. [(c,b)]([a].x)  [a].x}" by (simp add: supp_def)
  hence "infinite {b. [([(c,b)]a)].([(c,b)]x)  [a].x}" by (simp add: abs_fun_pi[OF pt, OF at])
  moreover
  have "{b. [([(c,b)]a)].([(c,b)]x)  [a].x}  {b. ([(c,b)]x,[(c,b)]a)  (x, a)}" by force
  ultimately have "infinite {b. ([(c,b)]x,[(c,b)]a)  (x, a)}" by (simp add: infinite_super)
  thus "c(supp (x,a))" by (simp add: supp_def)
qed

lemma abs_fun_finite_supp:
  fixes x :: "'a"
  and   a :: "'x"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  and     f:  "finite ((supp x)::'x set)"
  shows "finite ((supp ([a].x))::'x set)"
proof -
  from f have "finite ((supp (x,a))::'x set)" by (simp add: supp_prod at_supp[OF at])
  moreover
  have "((supp ([a].x))::'x set)  (supp (x,a))" by (rule abs_fun_supp_approx[OF pt, OF at])
  ultimately show ?thesis by (simp add: finite_subset)
qed

lemma fresh_abs_funI1:
  fixes  x :: "'a"
  and    a :: "'x"
  and    b :: "'x"
  assumes pt:  "pt TYPE('a) TYPE('x)"
  and     at:   "at TYPE('x)"
  and f:  "finite ((supp x)::'x set)"
  and a1: "bx" 
  and a2: "ab"
  shows "b([a].x)"
  proof -
    have "c::'x. c(b,a,x,[a].x)" 
    proof (rule at_exists_fresh'[OF at], auto simp add: supp_prod at_supp[OF at] f)
      show "finite ((supp ([a].x))::'x set)" using f
        by (simp add: abs_fun_finite_supp[OF pt, OF at])        
    qed
    then obtain c where fr1: "cb"
                  and   fr2: "ca"
                  and   fr3: "cx"
                  and   fr4: "c([a].x)"
                  by (force simp add: fresh_prod at_fresh[OF at])
    have e: "[(c,b)]([a].x) = [a].([(c,b)]x)" using a2 fr1 fr2 
      by (force simp add: abs_fun_pi[OF pt, OF at] at_calc[OF at])
    from fr4 have "([(c,b)]c) ([(c,b)]([a].x))"
      by (simp add: pt_fresh_bij[OF pt_abs_fun_inst[OF pt, OF at], OF at])
    hence "b([a].([(c,b)]x))" using fr1 fr2 e  
      by (simp add: at_calc[OF at])
    thus ?thesis using a1 fr3 
      by (simp add: pt_fresh_fresh[OF pt, OF at])
qed

lemma fresh_abs_funE:
  fixes a :: "'x"
  and   b :: "'x"
  and   x :: "'a"
  assumes pt:  "pt TYPE('a) TYPE('x)"
  and     at:  "at TYPE('x)"
  and     f:  "finite ((supp x)::'x set)"
  and     a1: "b([a].x)" 
  and     a2: "ba" 
  shows "bx"
proof -
  have "c::'x. c(b,a,x,[a].x)"
  proof (rule at_exists_fresh'[OF at], auto simp add: supp_prod at_supp[OF at] f)
    show "finite ((supp ([a].x))::'x set)" using f
      by (simp add: abs_fun_finite_supp[OF pt, OF at])  
  qed
  then obtain c where fr1: "bc"
                and   fr2: "ca"
                and   fr3: "cx"
                and   fr4: "c([a].x)" by (force simp add: fresh_prod at_fresh[OF at])
  have "[a].x = [(b,c)]([a].x)" using a1 fr4 
    by (simp add: pt_fresh_fresh[OF pt_abs_fun_inst[OF pt, OF at], OF at])
  hence "[a].x = [a].([(b,c)]x)" using fr2 a2 
    by (force simp add: abs_fun_pi[OF pt, OF at] at_calc[OF at])
  hence b: "([(b,c)]x) = x" by (simp add: abs_fun_eq1)
  from fr3 have "([(b,c)]c)([(b,c)]x)" 
    by (simp add: pt_fresh_bij[OF pt, OF at]) 
  thus ?thesis using b fr1 by (simp add: at_calc[OF at])
qed

lemma fresh_abs_funI2:
  fixes a :: "'x"
  and   x :: "'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  and     f: "finite ((supp x)::'x set)"
  shows "a([a].x)"
proof -
  have "c::'x. c(a,x)"
    by  (rule at_exists_fresh'[OF at], auto simp add: supp_prod at_supp[OF at] f) 
  then obtain c where fr1: "ac" and fr1_sym: "ca" 
                and   fr2: "cx" by (force simp add: fresh_prod at_fresh[OF at])
  have "c([a].x)" using f fr1 fr2 by (simp add: fresh_abs_funI1[OF pt, OF at])
  hence "([(c,a)]c)([(c,a)]([a].x))" using fr1  
    by (simp only: pt_fresh_bij[OF pt_abs_fun_inst[OF pt, OF at], OF at])
  hence a: "a([c].([(c,a)]x))" using fr1_sym 
    by (simp add: abs_fun_pi[OF pt, OF at] at_calc[OF at])
  have "[c].([(c,a)]x) = ([a].x)" using fr1_sym fr2 
    by (simp add: abs_fun_eq[OF pt, OF at])
  thus ?thesis using a by simp
qed

lemma fresh_abs_fun_iff: 
  fixes a :: "'x"
  and   b :: "'x"
  and   x :: "'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  and     f: "finite ((supp x)::'x set)"
  shows "(b([a].x)) = (b=a  bx)" 
  by (auto  dest: fresh_abs_funE[OF pt, OF at,OF f] 
           intro: fresh_abs_funI1[OF pt, OF at,OF f] 
                  fresh_abs_funI2[OF pt, OF at,OF f])

lemma abs_fun_supp: 
  fixes a :: "'x"
  and   x :: "'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  and     f: "finite ((supp x)::'x set)"
  shows "supp ([a].x) = (supp x)-{a}"
 by (force simp add: supp_fresh_iff fresh_abs_fun_iff[OF pt, OF at, OF f])

(* maybe needs to be better stated as supp intersection supp *)
lemma abs_fun_supp_ineq: 
  fixes a :: "'y"
  and   x :: "'a"
  assumes pta: "pt TYPE('a) TYPE('x)"
  and     ptb: "pt TYPE('y) TYPE('x)"
  and     at:  "at TYPE('x)"
  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  and     dj:  "disjoint TYPE('y) TYPE('x)"
shows "((supp ([a].x))::'x set) = (supp x)"
unfolding supp_def
  using abs_fun_pi_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj]
  by (smt (verit, ccfv_threshold) Collect_cong abs_fun_eq1)

lemma fresh_abs_fun_iff_ineq: 
  fixes a :: "'y"
  and   b :: "'x"
  and   x :: "'a"
  assumes pta: "pt TYPE('a) TYPE('x)"
  and     ptb: "pt TYPE('y) TYPE('x)"
  and     at:  "at TYPE('x)"
  and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  and     dj:  "disjoint TYPE('y) TYPE('x)"
  shows "b([a].x) = bx" 
  by (simp add: fresh_def abs_fun_supp_ineq[OF pta, OF ptb, OF at, OF cp, OF dj])

section ‹abstraction type for the parsing in nominal datatype›
(*==============================================================*)

inductive_set ABS_set :: "('x('a noption)) set"
  where
  ABS_in: "(abs_fun a x)ABS_set"

definition "ABS = ABS_set"

typedef ('x, 'a) ABS («_»_› [1000,1000] 1000) =
    "ABS::('x('a noption)) set"
  morphisms Rep_ABS Abs_ABS
  unfolding ABS_def
proof 
  fix x::"'a" and a::"'x"
  show "(abs_fun a x) ABS_set" by (rule ABS_in)
qed


section ‹lemmas for deciding permutation equations›
(*===================================================*)

lemma perm_aux_fold:
  shows "perm_aux pi x = pix" by (simp only: perm_aux_def)

lemma pt_perm_compose_aux:
  fixes pi1 :: "'x prm"
  and   pi2 :: "'x prm"
  and   x  :: "'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "pi2(pi1x) = perm_aux (pi2pi1) (pi2x)" 
proof -
  have "(pi2@pi1)  ((pi2pi1)@pi2)" by (rule at_ds8[OF at])
  hence "(pi2@pi1)x = ((pi2pi1)@pi2)x" by (rule pt3[OF pt])
  thus ?thesis by (simp add: pt2[OF pt] perm_aux_def)
qed  

lemma cp1_aux:
  fixes pi1::"'x prm"
  and   pi2::"'y prm"
  and   x  ::"'a"
  assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)"
  shows "pi1(pi2x) = perm_aux (pi1pi2) (pi1x)"
  using cp by (simp add: cp_def perm_aux_def)

lemma perm_eq_app:
  fixes f  :: "'a'b"
  and   x  :: "'a"
  and   pi :: "'x prm"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "(pi(f x)=y) = ((pif)(pix)=y)"
  by (simp add: pt_fun_app_eq[OF pt, OF at])

lemma perm_eq_lam:
  fixes f  :: "'a'b"
  and   x  :: "'a"
  and   pi :: "'x prm"
  shows "((pi(λx. f x))=y) = ((λx. (pi(f ((rev pi)x))))=y)"
  by (simp add: perm_fun_def)

section ‹test›
lemma at_prm_eq_compose:
  fixes pi1 :: "'x prm"
  and   pi2 :: "'x prm"
  and   pi3 :: "'x prm"
  assumes at: "at TYPE('x)"
  and     a: "pi1  pi2"
  shows "(pi3pi1)  (pi3pi2)"
proof -
  have pt: "pt TYPE('x) TYPE('x)" by (rule at_pt_inst[OF at])
  have pt_prm: "pt TYPE('x prm) TYPE('x)" 
    by (rule pt_list_inst[OF pt_prod_inst[OF pt, OF pt]])  
  from a show ?thesis
    by (auto simp add: prm_eq_def at pt pt_perm_compose')
qed

(************************)
(* Various eqvt-lemmas  *)

lemma Zero_nat_eqvt[simp]:
  shows "pi(0::nat) = 0" 
by (auto simp add: perm_nat_def)

lemma One_nat_eqvt[simp]:
  shows "pi(1::nat) = 1"
by (simp add: perm_nat_def)

lemma Suc_eqvt:
  shows "pi(Suc x) = Suc (pix)" 
by (auto simp add: perm_nat_def)

lemma numeral_nat_eqvt: 
 shows "pi((numeral n)::nat) = numeral n" 
by (simp add: perm_nat_def perm_int_def)

lemma max_nat_eqvt:
  fixes x::"nat"
  shows "pi(max x y) = max (pix) (piy)" 
by (simp add:perm_nat_def) 

lemma min_nat_eqvt:
  fixes x::"nat"
  shows "pi(min x y) = min (pix) (piy)" 
by (simp add:perm_nat_def) 

lemma plus_nat_eqvt:
  fixes x::"nat"
  shows "pi(x + y) = (pix) + (piy)" 
by (simp add:perm_nat_def) 

lemma minus_nat_eqvt:
  fixes x::"nat"
  shows "pi(x - y) = (pix) - (piy)" 
by (simp add:perm_nat_def) 

lemma mult_nat_eqvt:
  fixes x::"nat"
  shows "pi(x * y) = (pix) * (piy)" 
by (simp add:perm_nat_def) 

lemma div_nat_eqvt:
  fixes x::"nat"
  shows "pi(x div y) = (pix) div (piy)" 
by (simp add:perm_nat_def) 

lemma Zero_int_eqvt[simp]:
  shows "pi(0::int) = 0" 
by (auto simp add: perm_int_def)

lemma One_int_eqvt[simp]:
  shows "pi(1::int) = 1"
by (simp add: perm_int_def)

lemma numeral_int_eqvt[simp]: 
 shows "pi((numeral n)::int) = numeral n"
  using perm_int_def by blast 

lemma neg_numeral_int_eqvt[simp]:
  shows "pi((- numeral n)::int) = - numeral n"
  by (simp add: perm_int_def)

lemma max_int_eqvt:
  fixes x::"int"
  shows "pi(max (x::int) y) = max (pix) (piy)" 
  by (simp add:perm_int_def) 

lemma min_int_eqvt:
  fixes x::"int"
  shows "pi(min x y) = min (pix) (piy)" 
  by (simp add:perm_int_def) 

lemma plus_int_eqvt:
  fixes x::"int"
  shows "pi(x + y) = (pix) + (piy)" 
  by (simp add:perm_int_def) 

lemma minus_int_eqvt:
  fixes x::"int"
  shows "pi(x - y) = (pix) - (piy)" 
  by (simp add:perm_int_def) 

lemma mult_int_eqvt:
  fixes x::"int"
  shows "pi(x * y) = (pix) * (piy)" 
by (simp add:perm_int_def) 

lemma div_int_eqvt:
  fixes x::"int"
  shows "pi(x div y) = (pix) div (piy)" 
  by (simp add:perm_int_def) 

(*******************************************************)
(* Setup of the theorem attributes eqvt and eqvt_force *)
ML_file ‹nominal_thmdecls.ML›
setup "NominalThmDecls.setup"

lemmas [eqvt] = 
  (* connectives *)
  if_eqvt imp_eqvt disj_eqvt conj_eqvt neg_eqvt 
  true_eqvt false_eqvt
  imp_eqvt [folded HOL.induct_implies_def]
  
  (* datatypes *)
  perm_unit.simps
  perm_list.simps append_eqvt
  perm_prod.simps
  fst_eqvt snd_eqvt
  perm_option.simps

  (* nats *)
  Suc_eqvt Zero_nat_eqvt One_nat_eqvt min_nat_eqvt max_nat_eqvt
  plus_nat_eqvt minus_nat_eqvt mult_nat_eqvt div_nat_eqvt
  
  (* ints *)
  Zero_int_eqvt One_int_eqvt min_int_eqvt max_int_eqvt
  plus_int_eqvt minus_int_eqvt mult_int_eqvt div_int_eqvt
  
  (* sets *)
  union_eqvt empty_eqvt insert_eqvt set_eqvt
  
 
(* the lemmas numeral_nat_eqvt numeral_int_eqvt do not conform with the *)
(* usual form of an eqvt-lemma, but they are needed for analysing       *)
(* permutations on nats and ints *)
lemmas [eqvt_force] = numeral_nat_eqvt numeral_int_eqvt neg_numeral_int_eqvt

(***************************************)
(* setup for the individial atom-kinds *)
(* and nominal datatypes               *)
ML_file ‹nominal_atoms.ML›

(************************************************************)
(* various tactics for analysing permutations, supports etc *)
ML_file ‹nominal_permeq.ML›

method_setup perm_simp =
  NominalPermeq.perm_simp_meth
  ‹simp rules and simprocs for analysing permutations›

method_setup perm_simp_debug =
  NominalPermeq.perm_simp_meth_debug
  ‹simp rules and simprocs for analysing permutations including debugging facilities›

method_setup perm_extend_simp =
  NominalPermeq.perm_extend_simp_meth
  ‹tactic for deciding equalities involving permutations›

method_setup perm_extend_simp_debug =
  NominalPermeq.perm_extend_simp_meth_debug
  ‹tactic for deciding equalities involving permutations including debugging facilities›

method_setup supports_simp =
  NominalPermeq.supports_meth
  ‹tactic for deciding whether something supports something else›

method_setup supports_simp_debug =
  NominalPermeq.supports_meth_debug
  ‹tactic for deciding whether something supports something else including debugging facilities›

method_setup finite_guess =
  NominalPermeq.finite_guess_meth
  ‹tactic for deciding whether something has finite support›

method_setup finite_guess_debug =
  NominalPermeq.finite_guess_meth_debug
  ‹tactic for deciding whether something has finite support including debugging facilities›

method_setup fresh_guess =
  NominalPermeq.fresh_guess_meth
  ‹tactic for deciding whether an atom is fresh for something›

method_setup fresh_guess_debug =
  NominalPermeq.fresh_guess_meth_debug
  ‹tactic for deciding whether an atom is fresh for something including debugging facilities›

(*****************************************************************)
(* tactics for generating fresh names and simplifying fresh_funs *)
ML_file ‹nominal_fresh_fun.ML›

method_setup generate_fresh = Args.type_name {proper = true, strict = true} >>
    (fn s => fn ctxt => SIMPLE_METHOD (generate_fresh_tac ctxt s)) "generate a name fresh for all the variables in the goal"

method_setup fresh_fun_simp = Scan.lift (Args.parens (Args.$$$ "no_asm") >> K true || Scan.succeed false) >>
    (fn b => fn ctxt => SIMPLE_METHOD' (fresh_fun_tac ctxt b)) "delete one inner occurrence of fresh_fun"


(************************************************)
(* main file for constructing nominal datatypes *)
lemma allE_Nil: assumes "x. P x" obtains "P []"
  using assms ..

ML_file ‹nominal_datatype.ML›

(******************************************************)
(* primitive recursive functions on nominal datatypes *)
ML_file ‹nominal_primrec.ML›

(****************************************************)
(* inductive definition involving nominal datatypes *)
ML_file ‹nominal_inductive.ML›
ML_file ‹nominal_inductive2.ML›

(*****************************************)
(* setup for induction principles method *)
ML_file ‹nominal_induct.ML›
method_setup nominal_induct =
  NominalInduct.nominal_induct_method
  ‹nominal induction›

end