Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: sat_solver.ML Sprache: PVS

Original von: 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:
  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:
  shows "supp () = {}"
  by (simp add: supp_def)

lemma supp_set_empty:
  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:
  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:
  fixes x  :: "bool"
  shows "supp x = {}"
  by (cases "x") (simp_all add: supp_def)

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

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

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

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

lemma supp_char:
  fixes c::"char"
  shows "(supp c) = {}"
  by (simp add: supp_def perm_char_def)

lemma supp_string:
  fixes s::"string"
  shows "(supp s) = {}"
  by (simp add: supp_def perm_string)

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

lemma fresh_unit:
  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:
  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:
  fixes a :: "'x"
  and   xs :: "'a list"
  shows "a\(rev xs) = a\xs"
  by (simp add: fresh_def supp_list_rev)

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

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

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

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

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

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

lemma fresh_bool:
  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)"
apply(induct_tac pi2)
apply(simp add: prm_eq_def)
apply(auto simp add: prm_eq_def)
apply(simp add: at2[OF at])
apply(drule_tac x="aa" in spec)
apply(drule sym)
apply(simp)
apply(simp add: at_append[OF at])
apply(simp add: at2[OF at])
apply(simp add: at_ds8_aux[OF at])
done

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)))"
apply(induct_tac pi2)
apply(simp add: prm_eq_def)
apply(auto simp add: prm_eq_def)
apply(simp add: at_append[OF at])
apply(simp add: at2[OF at] at1[OF at])
apply(drule_tac x="swap(pi1\a,pi1\b) aa" in spec)
apply(drule sym)
apply(simp)
apply(simp add: at_ds8_aux[OF at])
apply(simp add: at_rev_pi[OF at])
done

lemma at_ds10:
  fixes pi :: "'x prm"
  and   a  :: "'x"
  and   b  :: "'x"
  assumes at: "at TYPE('x)"
  and     a:  "b\(rev pi)"
  shows "([(pi\a,b)]@pi) \ (pi@[(a,b)])"
using a
apply -
apply(rule at_prm_eq_trans)
apply(rule at_ds2[OF at])
apply(simp add: at_prm_fresh[OF at] at_rev_pi[OF at])
apply(rule at_prm_eq_refl)
done

\<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"
proof -
  from  fs at4[OF at] have "infinite ((UNIV::'x set) - A)"
    by (simp add: Diff_infinite_finite)
  hence "((UNIV::'x set) - A) \ ({}::'x set)" by (force simp only:)
  then obtain c::"'x" where "c\((UNIV::'x set) - A)" by force
  then have "c\A" by simp
  then show ?thesis ..
qed

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"
  using a b
  apply(drule_tac S="UNIV::'a set" in Diff_infinite_finite)
  apply(simp add: at_def)
  apply(subgoal_tac "UNIV - S \ {}")
  apply(simp only: ex_in_conv [symmetric])
  apply(blast)
  apply(rule notI)
  apply(simp)
  done

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)"
  proof (rule_tac ccontr, drule_tac notnotD)
    assume "UNIV-{a} = ({}::'x set)"
    with inf2 have "infinite ({}::'x set)" by simp
    then show "False" by auto
  qed
  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)"
apply(auto simp only: pt_def)
apply(simp only: at1[OF at])
apply(simp only: at_append[OF at])
apply(simp only: prm_eq_def)
done

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)"
apply(simp add: fs_def)
apply(simp add: at_supp[OF at])
done

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

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)"
apply(unfold fs_def)
apply(auto simp add: supp_prod)
apply(rule fs1[OF fsa])
apply(rule fs1[OF fsb])
done

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)"
apply(unfold fs_def, rule allI)
apply(case_tac x)
apply(auto simp add: supp_nprod)
apply(rule fs1[OF fsa])
apply(rule fs1[OF fsb])
done

lemma fs_list_inst:
  assumes fs: "fs TYPE('a) TYPE('x)"
  shows "fs TYPE('a list) TYPE('x)"
apply(simp add: fs_def, rule allI)
apply(induct_tac x)
apply(simp add: supp_list_nil)
apply(simp add: supp_list_cons)
apply(rule fs1[OF fs])
done

lemma fs_option_inst:
  assumes fs: "fs TYPE('a) TYPE('x)"
  shows "fs TYPE('a option) TYPE('x)"
apply(simp add: fs_def, rule allI)
apply(case_tac x)
apply(simp add: supp_none)
apply(simp add: supp_some)
apply(rule fs1[OF fs])
done

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: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "cp TYPE('a) TYPE('x) TYPE('x)"
apply(auto simp add: cp_def pt2[OF pt,symmetric])
apply(rule pt3[OF pt])
apply(rule at_ds8[OF at])
done

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)"
apply(simp add: supp_def dj_perm_forget[OF dj])
done

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)"
apply(auto simp only: pt_def)
apply(simp_all add: perm_fun_def)
apply(simp add: pt1[OF pta] pt1[OF ptb])
apply(simp add: pt2[OF pta] pt2[OF ptb])
apply(subgoal_tac "(rev pi1) \ (rev pi2)")(*A*)
apply(simp add: pt3[OF pta] pt3[OF ptb])
(*A*)
apply(simp add: at_prm_rev_eq[OF at])
done

lemma pt_bool_inst:
  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)"
apply(simp add: pt_def)
apply(simp_all add: perm_set_def)
apply(simp add: pt1[OF pt])
apply(force simp add: pt2[OF pt] pt3[OF pt])
done

lemma pt_unit_inst:
  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)"
  apply(auto simp add: pt_def)
  apply(rule pt1[OF pta])
  apply(rule pt1[OF ptb])
  apply(rule pt2[OF pta])
  apply(rule pt2[OF ptb])
  apply(rule pt3[OF pta],assumption)
  apply(rule pt3[OF ptb],assumption)
  done

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

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)"
apply(induct_tac xs)
apply(simp_all add: pt2[OF pt])
done

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"
apply(induct_tac xs)
apply(simp_all add: prm_eq_def pt3[OF pt])
done

lemma pt_list_inst:
  assumes pt: "pt TYPE('a) TYPE('x)"
  shows  "pt TYPE('a list) TYPE('x)"
apply(auto simp only: pt_def)
apply(rule pt_list_nil[OF pt])
apply(rule pt_list_append[OF pt])
apply(rule pt_list_prm_eq[OF pt],assumption)
done

lemma pt_option_inst:
  assumes pta: "pt TYPE('a) TYPE('x)"
  shows  "pt TYPE('a option) TYPE('x)"
apply(auto simp only: pt_def)
apply(case_tac "x")
apply(simp_all add: pt1[OF pta])
apply(case_tac "x")
apply(simp_all add: pt2[OF pta])
apply(case_tac "x")
apply(simp_all add: pt3[OF pta])
done

lemma pt_noption_inst:
  assumes pta: "pt TYPE('a) TYPE('x)"
  shows  "pt TYPE('a noption) TYPE('x)"
apply(auto simp only: pt_def)
apply(case_tac "x")
apply(simp_all add: pt1[OF pta])
apply(case_tac "x")
apply(simp_all add: pt2[OF pta])
apply(case_tac "x")
apply(simp_all add: pt3[OF pta])
done

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)"
  apply(auto simp add: pt_def)
  apply(case_tac x)
  apply(simp add: pt1[OF pta] pt1[OF ptb])
  apply(case_tac x)
  apply(simp add: pt2[OF pta] pt2[OF ptb])
  apply(case_tac x)
  apply(simp add: pt3[OF pta] pt3[OF ptb])
  done

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"
apply(simp add: pt2[OF pt,symmetric])
apply(rule trans)
apply(rule pt3[OF pt])
apply(rule at_ds5'[OF at])
apply(rule pt1[OF pt])
done

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"
apply(rule trans)
apply(rule pt3[OF pt])
apply(rule at_ds1[OF at])
apply(rule pt1[OF pt])
done

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])

(* FIXME: is this lemma needed anywhere? *)
lemma pt_set_bij3:
  fixes pi :: "'x prm"
  and   x  :: "'a"
  and   X  :: "'a set"
  shows "pi\(x\X) = (x\X)"
by (simp add: perm_bool)

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)}"
apply(auto simp add: perm_set_def pt_rev_pi[OF pt, OF at])
apply(rule_tac x="(rev pi)\x" in exI)
apply(simp add: pt_pi_rev[OF pt, OF at])
done

\<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)"
apply(rule pt_perm_supp_ineq)
apply(rule pt)
apply(rule at_pt_inst)
apply(rule at)+
apply(rule cp_pt_inst)
apply(rule pt)
apply(rule at)
done

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)"
apply(simp add: pt_perm_supp[OF pt, OF at, symmetric])
apply(simp add: pt_set_finite_ineq[OF at_pt_inst[OF at], OF at])
apply(rule f)
done

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"
apply(simp add: fresh_def)
apply(simp add: pt_set_bij1[OF ptb, OF at])
apply(simp add: pt_perm_supp_ineq[OF pta, OF ptb, OF at, OF cp])
done

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)"
apply(simp add: fresh_def)
apply(simp add: pt_set_bij1[OF ptb, OF at])
apply(simp add: pt_perm_supp_ineq[OF pta, OF ptb, OF at, OF cp])
done

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"
apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
apply(simp add: pt_rev_pi[OF ptb, OF at])
done

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"
apply(rule pt_fresh_left_ineq)
apply(rule pt)
apply(rule at_pt_inst)
apply(rule at)+
apply(rule cp_pt_inst)
apply(rule pt)
apply(rule at)
done

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)"
apply(rule pt_fresh_right_ineq)
apply(rule pt)
apply(rule at_pt_inst)
apply(rule at)+
apply(rule cp_pt_inst)
apply(rule pt)
apply(rule at)
done

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"
apply(rule pt_fresh_bij_ineq)
apply(rule pt)
apply(rule at_pt_inst)
apply(rule at)+
apply(rule cp_pt_inst)
apply(rule pt)
apply(rule at)
done

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)))"
apply(auto simp add: perm_bool perm_fun_def)
apply(drule_tac x="pi\x" in spec)
apply(simp add: pt_rev_pi[OF pt, OF at])
done

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)))"
apply(auto simp add: perm_bool perm_fun_def)
apply(rule_tac x="pi\x" in exI)
apply(simp add: pt_rev_pi[OF pt, OF at])
done

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)))"
  apply(rule the1_equality [symmetric])
  apply(simp add: pt_ex1_eqvt[OF pt at,symmetric])
  apply(simp add: perm_bool unique)
  apply(simp add: perm_bool pt_rev_pi [OF pt at])
  apply(rule theI'[OF unique])
  done

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"
using a
apply(auto simp add: supports_def)
apply(simp add: pt_set_bij1a[OF pt, OF at])
apply(force simp add: pt_swap_bij[OF pt, OF at])
apply(simp add: pt_set_bij1a[OF pt, OF at])
done

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"
proof (simp add: fresh_def)
  have "(supp x)\S" using a1 a2 by (rule supp_is_subset)
  thus "a\(supp x)" using a3 by force
qed

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 a1 a2
  apply auto
  apply (subgoal_tac "infinite (X - {b\X. P b})")
  apply (simp add: set_diff_eq)
  apply (simp add: Diff_infinite_finite)
  done

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"
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.208 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.