# 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

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 = pi∙x"

(* overloaded permutation operations *)
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) = (pi∙x, pi∙y)"

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

primrec perm_option :: "'x prm ⇒ 'a option ⇒ 'a option" where
some_eqvt:  "perm_option pi (Some x) = Some (pi∙x)"
| 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 (pi∙x)"
| 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 (pi∙x) (pi∙y)"

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 "pi∙P"
using a by (simp add: perm_bool)

lemma perm_boolE:
assumes a: "pi∙P"
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 (pi∙b) then (pi∙c1) else (pi∙c2))"
by (simp add: perm_fun_def)

lemma imp_eqvt:
shows "pi∙(A⟶B) = ((pi∙A)⟶(pi∙B))"
by (simp add: perm_bool)

lemma conj_eqvt:
shows "pi∙(A∧B) = ((pi∙A)∧(pi∙B))"
by (simp add: perm_bool)

lemma disj_eqvt:
shows "pi∙(A∨B) = ((pi∙A)∨(pi∙B))"
by (simp add: perm_bool)

lemma neg_eqvt:
shows "pi∙(¬ A) = (¬ (pi∙A))"
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∙(X∪Y)) = (pi∙X) ∪ (pi∙Y)"
by (auto simp add: perm_set_def)

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

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

lemma snd_eqvt:
"pi∙(snd x) = snd (pi∙x)"
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) = (pi∙l1)@(pi∙l2)"
by (induct l1) auto

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

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

(* permutation on characters and strings *)
lemma perm_string:
fixes s::"string"
shows "pi∙s = 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. pi1∙a = pi2∙a)"

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. (a∉S ∧ b∉S ⟶ [(a,b)]∙x=x))"

(* lemmas about supp *)
lemma supp_fresh_iff:
fixes x :: "'a"
shows "(supp x) = {a::'x. ¬a♯x}"
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) = (a♯x ∧ a♯y)"
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) = (a♯x ∧ a♯xs)"
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) = (a♯xs ∧ a♯ys)"
by (simp add: fresh_def supp_list_append)

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

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

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

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

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

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

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

lemma fresh_bool[simp]:
fixes a :: "'x"
and   b :: "bool"
shows "a♯b"
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) ≡ (a♯x ⟹ a♯y ⟹ 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 "a♯x1 ⟹ a♯x2 ⟹ a♯(x1,x2)"
by (simp add: fresh_prod)

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

ML ‹
val mksimps_pairs = (\<^const_name>‹Nominal.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∙(pi2∙x)) ∧
(∀(pi1::'x prm) (pi2::'x prm) (x::'a). pi1 ≜ pi2 ⟶ pi1∙x = pi2∙x)"

(* 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) (pi∙x)) ∧
(∀(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). pi∙x = x) ∧
(∀(pi::'y prm)(x::'x). pi∙x = 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∙(pi2∙x) = (pi1∙pi2)∙(pi1∙x))"

(* 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) (pi∙x)"
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   "⟦a≠c; b≠c⟧ ⟹ [(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∙(pi2∙c)"
proof (induct pi1)
case Nil show ?case by (simp add: at1[OF at])
next
case (Cons x xs)
have "(xs@pi2)∙c  =  xs∙(pi2∙c)" 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)∙(pi∙c) = 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:  "(pi∙x) = y"
shows   "x=(rev pi)∙y"
proof -
from a have "y=(pi∙x)" 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=pi∙y"
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 "(pi∙x = pi∙y) = (x=y)"
proof
assume "pi∙x = pi∙y"
hence  "x=(rev pi)∙(pi∙y)" by (rule at_bij1[OF at])
thus "x=y" by (simp only: at_rev_pi[OF at])
next
assume "x=y"
thus "pi∙x = pi∙y" 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 "(a♯b) = (a≠b)"
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: "c♯pi"
shows "∀(a,b)∈set pi. c≠a ∧ c≠b"
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. c≠a ∧ c≠b"
shows "pi∙c = 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: "c♯pi"
shows "pi∙c = 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))∙(pi2∙x)" 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 "pi1∙x  =  pi2∙x" by simp
next
fix x
assume "∀x::'x. pi1∙x = pi2∙x"
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)]) ≜ ([(pi∙a,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 (pi∙a,pi∙b) (pi∙c)"
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) ≜ ((pi1∙pi2)@pi1)"
proof(induct pi2)
show "(pi1 @ []) ≜ (pi1 ∙ [] @ pi1)"
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 (pi1∙pi2)))"
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 "([(pi∙a,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 "c∉A"
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. c♯x"
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  "c♯x"
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). a≠b"
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 "a≠b" by blast
then show "∃(b::'x). a≠b" 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∙(pi2∙x)"
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 ⟹ pi1∙x = pi2∙x"
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∙(pi2∙x) = (pi1∙pi2)∙(pi1∙x)"
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 "pi∙x=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 "pi∙x=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 "pi2∙pi1=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∙(pi2∙x) = (pi2)∙(pi1∙x)"
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 "a♯b"
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∙(pi2∙xs)"
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  ⟹ pi1∙xs = pi2∙xs"
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)∙(pi∙x) = 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:  "(pi∙x) = y"
shows   "x=(rev pi)∙y"
proof -
from a have "y=(pi∙x)" 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   "(pi∙x)=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 "(pi∙x = pi∙y) = (x=y)"
proof
assume "pi∙x = pi∙y"
hence  "x=(rev pi)∙(pi∙y)" 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 "pi∙x = pi∙y" 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) = (pi∙x = pi∙y)"
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 "(pi∙x = pi∙y)"
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:  "pi∙x = pi∙y"
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} = a♯x"
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 "((pi∙x)∈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∈(pi∙X)) = (((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 "((pi∙x)∈(pi∙X)) = (x∈X)"
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∙(x∈X)=((pi∙x)∈(pi∙X))"
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:  "x∈X"
shows "(pi∙x)∈(pi∙X)"
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 "(pi∙x)∈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∙(X⊆Y)) = ((pi∙X)⊆(pi∙Y))"
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) = (pi∙X) - (pi∙Y)"
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 "{pi∙x| x. P1 x} = {pi∙x| 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 "{pi∙x| 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 "pi∙x = pi∙y"
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 (pi∙X) = finite X"
proof -
have image: "(pi∙X) = (perm pi ` X)" by (force simp only: perm_set_def)
show ?thesis
proof (rule iffI)
assume "finite (pi∙X)"
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 (pi∙X)" 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 (pi∙X) = 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 (pi∙x)" (is "?LHS = ?RHS")
proof -
have "?LHS = {pi∙a | a. infinite {b. [(a,b)]∙x ≠ x}}" by (simp add: supp_def perm_set_def)
also have "… = {pi∙a | a. infinite {pi∙b | 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 {pi∙b |b::'y. [(a,b)]∙x  ≠ x}" by (simp add: perm_set_def)
next
fix a
assume "infinite {pi∙b |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) ≠ (pi∙x)}}"
by (simp add: pt_bij[OF pta, OF at])
also have "… = {a. infinite {b. [(a,b)]∙(pi∙x) ≠ (pi∙x)}}"
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)]∙(pi∙x)"
by (simp add: cp1[OF cp] pt_pi_rev[OF ptb, OF at])
thus "(pi∙([((rev pi)∙a,(rev pi)∙b)]∙x) ≠  pi∙x) = ([(a,b)]∙(pi∙x) ≠ pi∙x)" 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 (pi∙x)"
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 (pi∙x))::'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♯(pi∙x) = ((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 "(pi∙a)♯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 "(pi∙a)♯(pi∙x) = a♯x"
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♯(pi∙x) = ((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 "(pi∙a)♯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 "(pi∙a)♯(pi∙x) = a♯x"
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:  "a♯x"
shows "(pi∙a)♯(pi∙x)"
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:  "(pi∙a)♯(pi∙x)"
shows  "a♯x"
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∙(a♯x) = (pi∙a)♯(pi∙x)"
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: "¬(a♯x)"
and     a2: "b♯x"
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: "a≠b" 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: "c≠a" and  a2: "a♯x" and a3: "c♯x"
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: "a♯pi"
and     h2: "a♯x"
shows "a♯(pi∙x)"
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♯(pi∙x)"  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: "c♯x"
shows "c♯(pi∙x)"
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∙(c♯x) = (pi∙c)♯(pi∙x)"
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: "a♯x" and a2: "b♯x"
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: "a≠b"
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: "a≠c ∧ b≠c"
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. a♯x ∧ b♯x"
shows "pi∙x=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). a♯x ∧ b♯x" by fact
have ih: "(∀(a,b)∈set pi. a♯x ∧ b♯x) ⟹ pi∙x=x" by fact
obtain a b where e: "ab=(a,b)" by (cases ab) (auto)
from a have a': "a♯x" "b♯x" using e by auto
have "(ab#pi)∙x = ([(a,b)]@pi)∙x" using e by simp
also have "… = [(a,b)]∙(pi∙x)" 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∙(pi1∙x) = (pi2∙pi1)∙(pi2∙x)"
proof -
have "(pi2@pi1) ≜ ((pi2∙pi1)@pi2)" by (rule at_ds8 [OF at])
hence "(pi2@pi1)∙x = ((pi2∙pi1)@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 "(pi2∙pi1)∙x = pi2∙(pi1∙((rev pi2)∙x))"
proof -
have "pi2∙(pi1∙((rev pi2)∙x)) = (pi2∙pi1)∙(pi2∙((rev pi2)∙x))"
by (rule pt_perm_compose[OF pt, OF at])
also have "… = (pi2∙pi1)∙x" by (simp add: pt_pi_rev[OF pt, OF at])
finally have "pi2∙(pi1∙((rev pi2)∙x)) = (pi2∙pi1)∙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 (pi1∙pi2)∙x)"
proof -
have "((rev pi2)@(rev pi1)) ≜ ((rev pi1)@(rev (pi1∙pi2)))" by (rule at_ds9[OF at])
hence "((rev pi2)@(rev pi1))∙x = ((rev pi1)@(rev (pi1∙pi2)))∙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)```