Impressum Nominal.thy Sprache: Isabelle

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 \<open>Permutations\<close>
(*======================*)

type_synonym
  'x prm = "('x \<times> '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 *)
overloading
  perm_fun    \<equiv> "perm :: 'x prm \<Rightarrow> ('a\<Rightarrow>'b) \<Rightarrow> ('a\<Rightarrow>'b)"   (unchecked)
  perm_bool   \<equiv> "perm :: 'x prm \<Rightarrow> bool \<Rightarrow> bool"           (unchecked)
  perm_set    \<equiv> "perm :: 'x prm \<Rightarrow> 'a set \<Rightarrow> 'a set"       (unchecked)
  perm_unit   \<equiv> "perm :: 'x prm \<Rightarrow> unit \<Rightarrow> unit"           (unchecked)
  perm_prod   \<equiv> "perm :: 'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)"    (unchecked)
  perm_list   \<equiv> "perm :: 'x prm \<Rightarrow> 'a list \<Rightarrow> 'a list"     (unchecked)
  perm_option \<equiv> "perm :: 'x prm \<Rightarrow> 'a option \<Rightarrow> 'a option" (unchecked)
  perm_char   \<equiv> "perm :: 'x prm \<Rightarrow> char \<Rightarrow> char"           (unchecked)
  perm_nat    \<equiv> "perm :: 'x prm \<Rightarrow> nat \<Rightarrow> nat"             (unchecked)
  perm_int    \<equiv> "perm :: 'x prm \<Rightarrow> int \<Rightarrow> int"             (unchecked)

  perm_noption \<equiv> "perm :: 'x prm \<Rightarrow> 'a noption \<Rightarrow> 'a noption"   (unchecked)
  perm_nprod   \<equiv> "perm :: 'x prm \<Rightarrow> ('a, 'b) nprod \<Rightarrow> ('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 \<open>permutation equality\<close>
(*==============================*)

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

section \<open>Support, Freshness and Supports\<close>
(*========================================*)
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 \<open>Normalization of freshness results; cf.\ \<open>nominal_induct\<close>\<close>
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 \<open>
  val mksimps_pairs = (\<^const_name>\<open>Nominal.fresh\<close>, @{thms fresh_prodD}) :: mksimps_pairs;
\<close>
declaration \<open>fn _ =>
  Simplifier.map_ss (Simplifier.set_mksimps (mksimps mksimps_pairs))
\<close>

section \<open>Abstract Properties for Permutations and  Atoms\<close>
(*=========================================================*)

(* properties for being a permutation type *)
definition
  "pt TYPE('a) TYPE('x) \
     (\<forall>(x::'a). ([]::'x prm)\<bullet>x = x) \<and>
     (\<forall>(pi1::'x prm) (pi2::'x prm) (x::'a). (pi1@pi2)\<bullet>x = pi1\<bullet>(pi2\<bullet>x)) \<and>
     (\<forall>(pi1::'x prm) (pi2::'x prm) (x::'a). pi1 \<triangleq> pi2 \<longrightarrow> pi1\<bullet>x = pi2\<bullet>x)"

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

(* property of two atom-types being disjoint *)
definition
  "disjoint TYPE('x) TYPE('y) \
       (\<forall>(pi::'x prm)(x::'y). pi\<bullet>x = x) \<and>
       (\<forall>(pi::'y prm)(x::'x). pi\<bullet>x = x)"

(* composition property of two permutation on a type 'a *)
definition
  "cp TYPE ('a) TYPE('x) TYPE('y) \
      (\<forall>(pi2::'y prm) (pi1::'x prm) (x::'a) . pi1\<bullet>(pi2\<bullet>x) = (pi1\<bullet>pi2)\<bullet>(pi1\<bullet>x))"

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

section \<open>Lemmas about the atom-type properties\<close>
(*==============================================*)

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)"
    by(simp add: prm_eq_def)
  show "\a l. (pi1 @ l) \ (pi1 \ l @ pi1) \
        (pi1 @ a # l) \<triangleq> (pi1 \<bullet> (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)

\<comment> \<open>there always exists an atom that is not being in a finite set\<close>
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 \<open>there always exists a fresh name for an object with finite support\<close>
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

\<comment> \<open>the at-props imply the pt-props\<close>
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 \<open>finite support properties\<close>
(*===================================*)

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 \<open>Lemmas about the permutation properties\<close>
(*=================================================*)

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 \<open>composition properties\<close>
(* ============================== *)
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 \<open>disjointness properties\<close>
(*=================================*)
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 \<open>permutation type instances\<close>
(* ===================================*)

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 \<open>further lemmas for permutation types\<close>
(*==============================================*)

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

\<comment> \<open>some helper lemmas for the pt_perm_supp_ineq lemma\<close>
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)

\<comment> \<open>the co-set of a finite set is infinte\<close>
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 \<open>equivariance for some connectives\<close>
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 pi\x)))"
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 \<open>facts about supports\<close>
(*==============================*)

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) \ a\S" by force
  then obtain a where b1: "a\supp x" and b2: "a\S" by force
  from a1 b2 have "\b. (b\S \ ([(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 "a\x" and "b\x" 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 "c\S" 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 \ c\S"
    have "((supp x)::'x set) supports x" by (rule supp_supports[OF pt, OF at])
    with d fs1[OF fs] show "c\supp 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) \ S\S'"
  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 "S\supp 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: "\x\X. (\(a::'x) (b::'x). a\S\b\S \ ([(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: "a\S"
  shows "a\x"
  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. a\X \ b\X \ [(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:"\b\X. P(b)"
  shows "infinite {b\X. 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: "a\X"
    hence "\b\(UNIV-X). [(a,b)]\X\X"
      by (auto simp add: perm_set_def at_calc[OF at])
    with inf have "infinite {b\(UNIV-X). [(a,b)]\X\X}" by (rule infinite_Collection)
    hence "infinite {b. [(a,b)]\X\X}" 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 \<open>Permutations acting on Functions\<close>
(*==========================================*)

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) = (pi\f)(pi\x)"
  by (simp add: perm_fun_def pt_rev_pi[OF pt, OF at])

\<comment> \<open>sometimes pt_fun_app_eq does too much; this lemma 'corrects it'\<close>
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 "(pi1\perm pi2)(pi1\x) = pi1\(pi2\x)"
  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 "(pi\f = f) = (\ x. pi\(f x) = f (pi\x))" (is "?LHS = ?RHS")
proof
  assume a: "?LHS"
  show "?RHS"
  proof
    fix x
    have "pi\(f x) = (pi\f)(pi\x)" by (simp add: pt_fun_app_eq[OF pt, OF at])
    also have "\ = f (pi\x)" using a by simp
    finally show "pi\(f x) = f (pi\x)" by simp
  qed
next
  assume b: "?RHS"
  show "?LHS"
  proof (rule ccontr)
    assume "(pi\f) \ f"
    hence "\x. (pi\f) x \ f x" by (simp add: fun_eq_iff)
    then obtain x where b1: "(pi\f) x \ f x" by force
    from b have "pi\(f ((rev pi)\x)) = f (pi\((rev pi)\x))" by force
    hence "(pi\f)(pi\((rev pi)\x)) = f (pi\((rev pi)\x))"
      by (simp add: pt_fun_app_eq[OF pt, OF at])
    hence "(pi\f) x = f x" by (simp add: pt_pi_rev[OF pt, OF at])
    with b1 show "False" by simp
  qed
qed

\<comment> \<open>two helper lemmas for the equivariance of functions\<close>
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 "pi\y = y"
proof(induct pi)
  case Nil show ?case by (simp add: pt1[OF pt])
next
  case (Cons x xs)
  have ih: "xs\y = 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)]\(xs\y)" 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. pi\y = 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). pi\f = 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). pi\f = 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). pi\f = 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). pi\f = 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(pi\x)"
proof (intro strip)
  fix pi x
  from a have b: "\(pi::'x prm). pi\f = f" by (simp add: pt_eqvt_fun1[OF pta, OF ptb, OF at])
  have "(pi::'x prm)\(f x) = (pi\f)(pi\x)" by (simp add: pt_fun_app_eq[OF pta, OF at])
  with b show "(pi::'x prm)\(f x) = f (pi\x)" 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(pi\x)"
--> --------------------

--> maximum size reached

--> --------------------

quality83%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.60Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.