src/HOL/Nominal/Nominal.thy

Initial revision.

(* $Id$ *)

theory nominal 
imports Main
  uses ("nominal_package.ML") ("nominal_induct.ML") ("nominal_permeq.ML")
begin 

ML {* reset NameSpace.unique_names; *}

section {* Permutations *}
(*======================*)

types 
  'x prm = "('x \<times> 'x) list"

(* polymorphic operations for permutation and swapping*)
consts 
  perm :: "'x prm \<Rightarrow> 'a \<Rightarrow> 'a"     ("_ \<bullet> _" [80,80] 80)
  swap :: "('x \<times> 'x) \<Rightarrow> 'x \<Rightarrow> 'x"

(* permutation on sets *)
defs (overloaded)
  perm_set_def:  "pi\<bullet>(X::'a set) \<equiv> {pi\<bullet>a | a. a\<in>X}"

(* permutation on units and products *)
primrec (perm_unit)
  "pi\<bullet>()    = ()"

primrec (perm_prod)
  "pi\<bullet>(a,b) = (pi\<bullet>a,pi\<bullet>b)"

lemma perm_fst:
  "pi\<bullet>(fst x) = fst (pi\<bullet>x)"
 by (cases x, simp)

lemma perm_snd:
  "pi\<bullet>(snd x) = snd (pi\<bullet>x)"
 by (cases x, simp)

(* permutation on lists *)
primrec (perm_list)
  perm_nil_def:  "pi\<bullet>[]     = []"
  perm_cons_def: "pi\<bullet>(x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)"

lemma perm_append:
  fixes pi :: "'x prm"
  and   l1 :: "'a list"
  and   l2 :: "'a list"
  shows "pi\<bullet>(l1@l2) = (pi\<bullet>l1)@(pi\<bullet>l2)"
  by (induct l1, auto)

lemma perm_rev:
  fixes pi :: "'x prm"
  and   l  :: "'a list"
  shows "pi\<bullet>(rev l) = rev (pi\<bullet>l)"
  by (induct l, simp_all add: perm_append)

(* permutation on functions *)
defs (overloaded)
  perm_fun_def: "pi\<bullet>(f::'a\<Rightarrow>'b) \<equiv> (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"

(* permutation on bools *)
primrec (perm_bool)
  perm_true_def:  "pi\<bullet>True  = True"
  perm_false_def: "pi\<bullet>False = False"

(* permutation on options *)
primrec (perm_option)
  perm_some_def:  "pi\<bullet>Some(x) = Some(pi\<bullet>x)"
  perm_none_def:  "pi\<bullet>None    = None"

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

primrec (perm_noption)
  perm_Nsome_def:  "pi\<bullet>nSome(x) = nSome(pi\<bullet>x)"
  perm_Nnone_def:  "pi\<bullet>nNone    = nNone"

(* permutation on characters (used in strings) *)
defs (overloaded)
  perm_char_def: "pi\<bullet>(s::char) \<equiv> s"

(* permutation on ints *)
defs (overloaded)
  perm_int_def:    "pi\<bullet>(i::int) \<equiv> i"

(* permutation on nats *)
defs (overloaded)
  perm_nat_def:    "pi\<bullet>(i::nat) \<equiv> i"

section {* permutation equality *}
(*==============================*)

constdefs
  prm_eq :: "'x prm \<Rightarrow> 'x prm \<Rightarrow> bool"  (" _ \<sim> _ " [80,80] 80)
  "pi1 \<sim> pi2 \<equiv> \<forall>a::'x. pi1\<bullet>a = pi2\<bullet>a"

section {* Support, Freshness and Supports*}
(*========================================*)
constdefs
   supp :: "'a \<Rightarrow> ('x set)"  
   "supp x \<equiv> {a . (infinite {b . [(a,b)]\<bullet>x \<noteq> x})}"

   fresh :: "'x \<Rightarrow> 'a \<Rightarrow> bool" (" _ \<sharp> _" [80,80] 80)
   "a \<sharp> x \<equiv> a \<notin> supp x"

   supports :: "'x set \<Rightarrow> 'a \<Rightarrow> bool" (infixl 80)
   "S supports x \<equiv> \<forall>a b. (a\<notin>S \<and> b\<notin>S \<longrightarrow> [(a,b)]\<bullet>x=x)"

lemma supp_fresh_iff: 
  fixes x :: "'a"
  shows "(supp x) = {a::'x. \<not>a\<sharp>x}"
apply(simp add: fresh_def)
done

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

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

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

lemma supp_list_cons:
  fixes x  :: "'a"
  and   xs :: "'a list"
  shows "supp (x#xs) = (supp x)\<union>(supp xs)"
apply(auto simp add: supp_def Collect_imp_eq Collect_neg_eq)
done

lemma supp_list_append:
  fixes xs :: "'a list"
  and   ys :: "'a list"
  shows "supp (xs@ys) = (supp xs)\<union>(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) = {}"
  apply(case_tac "x")
  apply(simp_all add: supp_def)
done

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

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

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

lemma fresh_prod:
  fixes a :: "'x"
  and   x :: "'a"
  and   y :: "'b"
  shows "a\<sharp>(x,y) = (a\<sharp>x \<and> a\<sharp>y)"
  by (simp add: fresh_def supp_prod)

lemma fresh_list_nil:
  fixes a :: "'x"
  shows "a\<sharp>([]::'a list)"
  by (simp add: fresh_def supp_list_nil) 

lemma fresh_list_cons:
  fixes a :: "'x"
  and   x :: "'a"
  and   xs :: "'a list"
  shows "a\<sharp>(x#xs) = (a\<sharp>x \<and> a\<sharp>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\<sharp>(xs@ys) = (a\<sharp>xs \<and> a\<sharp>ys)"
  by (simp add: fresh_def supp_list_append)

lemma fresh_list_rev:
  fixes a :: "'x"
  and   xs :: "'a list"
  shows "a\<sharp>(rev xs) = a\<sharp>xs"
  by (simp add: fresh_def supp_list_rev)

lemma fresh_none:
  fixes a :: "'x"
  shows "a\<sharp>None"
  apply(simp add: fresh_def supp_none)
  done

lemma fresh_some:
  fixes a :: "'x"
  and   x :: "'a"
  shows "a\<sharp>(Some x) = a\<sharp>x"
  apply(simp add: fresh_def supp_some)
  done

section {* Abstract Properties for Permutations and  Atoms *}
(*=========================================================*)

(* properties for being a permutation type *)
constdefs 
  "pt TYPE('a) TYPE('x) \<equiv> 
     (\<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 \<sim> pi2 \<longrightarrow> pi1\<bullet>x = pi2\<bullet>x)"

(* properties for being an atom type *)
constdefs 
  "at TYPE('x) \<equiv> 
     (\<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 *)
constdefs
  "disjoint TYPE('x) TYPE('y) \<equiv> 
       (\<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 *)
constdefs
  "cp TYPE ('a) TYPE('x) TYPE('y) \<equiv> 
      (\<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 *)
constdefs 
  "fs TYPE('a) TYPE('x) \<equiv> \<forall>(x::'a). finite ((supp x)::'x set)"

section {* Lemmas about the atom-type properties*}
(*==============================================*)

lemma at1: 
  fixes x::"'x"
  assumes a: "at TYPE('x)"
  shows "([]::'x prm)\<bullet>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)\<bullet>x = swap (a,b) (pi\<bullet>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 premutations *)
lemmas at_calc = at2 at1 at3

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)\<bullet>c = pi1\<bullet>(pi2\<bullet>c)"
proof (induct pi1)
  case Nil show ?case by (simp add: at1[OF at])
next
  case (Cons x xs)
  assume i: "(xs @ pi2)\<bullet>c  =  xs\<bullet>(pi2\<bullet>c)"
  have "(x#xs)@pi2 = x#(xs@pi2)" by simp
  thus ?case using i 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)\<bullet>(pi\<bullet>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\<bullet>((rev pi)\<bullet>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\<bullet>x) = y"
  shows   "x=(rev pi)\<bullet>y"
proof -
  from a have "y=(pi\<bullet>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)\<bullet>x) = y"
  shows   "x=pi\<bullet>y"
proof -
  from a have "y=((rev pi)\<bullet>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\<bullet>x = pi\<bullet>y) = (x=y)"
proof 
  assume "pi\<bullet>x = pi\<bullet>y" 
  hence  "x=(rev pi)\<bullet>(pi\<bullet>y)" by (rule at_bij1[OF at]) 
  thus "x=y" by (simp only: at_rev_pi[OF at])
next
  assume "x=y"
  thus "pi\<bullet>x = pi\<bullet>y" by simp
qed

lemma at_supp:
  fixes x :: "'x"
  assumes at: "at TYPE('x)"
  shows "supp x = {x}"
proof (simp add: supp_def Collect_conj_eq Collect_imp_eq at_calc[OF at], auto)
  assume f: "finite {b::'x. b \<noteq> x}"
  have a1: "{b::'x. b \<noteq> x} = UNIV-{x}" by force
  have a2: "infinite (UNIV::'x set)" by (rule at4[OF at])
  from f a1 a2 show False by force
qed

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

lemma at_prm_fresh[rule_format]:
  fixes c :: "'x"
  and   pi:: "'x prm"
  assumes at: "at TYPE('x)"
  shows "c\<sharp>pi \<longrightarrow> pi\<bullet>c = c"
apply(induct pi)
apply(simp add: at1[OF at]) 
apply(force simp add: fresh_list_cons at2[OF at] fresh_prod at_fresh[OF at] at3[OF at])
done

lemma at_prm_rev_eq:
  fixes pi1 :: "'x prm"
  and   pi2 :: "'x prm"
  assumes at: "at TYPE('x)"
  shows a: "((rev pi1) \<sim> (rev pi2)) = (pi1 \<sim> pi2)"
proof (simp add: prm_eq_def, auto)
  fix x
  assume "\<forall>x::'x. (rev pi1)\<bullet>x = (rev pi2)\<bullet>x"
  hence "(rev (pi1::'x prm))\<bullet>(pi2\<bullet>(x::'x)) = (rev (pi2::'x prm))\<bullet>(pi2\<bullet>x)" by simp
  hence "(rev (pi1::'x prm))\<bullet>((pi2::'x prm)\<bullet>x) = (x::'x)" by (simp add: at_rev_pi[OF at])
  hence "(pi2::'x prm)\<bullet>x = (pi1::'x prm)\<bullet>x" by (simp add: at_bij2[OF at])
  thus "pi1 \<bullet> x  =  pi2 \<bullet> x" by simp
next
  fix x
  assume "\<forall>x::'x. pi1\<bullet>x = pi2\<bullet>x"
  hence "(pi1::'x prm)\<bullet>((rev pi2)\<bullet>x) = (pi2::'x prm)\<bullet>((rev pi2)\<bullet>(x::'x))" by simp
  hence "(pi1::'x prm)\<bullet>((rev pi2)\<bullet>(x::'x)) = x" by (simp add: at_pi_rev[OF at])
  hence "(rev pi2)\<bullet>x = (rev pi1)\<bullet>(x::'x)" by (simp add: at_bij1[OF at])
  thus "(rev pi1)\<bullet>x = (rev pi2)\<bullet>(x::'x)" by simp
qed
  
lemma at_prm_rev_eq1:
  fixes pi1 :: "'x prm"
  and   pi2 :: "'x prm"
  assumes at: "at TYPE('x)"
  shows "pi1 \<sim> pi2 \<Longrightarrow> (rev pi1) \<sim> (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)] \<sim> []"
  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 "(pi@[((rev pi)\<bullet>a,(rev pi)\<bullet>b)]) \<sim> ([(a,b)]@pi)"
  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)] \<sim> [(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)\<bullet>b)]) \<sim> ([(pi\<bullet>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)] \<sim> [(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)] \<sim> [(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) \<sim> []"
  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\<bullet>(swap (a,b) c) = swap (pi\<bullet>a,pi\<bullet>b) (pi\<bullet>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) \<sim> ((pi1\<bullet>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)) \<sim> ((rev pi1)@(rev (pi1\<bullet>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\<bullet>a,pi1\<bullet>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

--"there always exists an atom not being in a finite set"
lemma ex_in_inf:
  fixes   A::"'x set"
  assumes at: "at TYPE('x)"
  and     fs: "finite A"
  shows "\<exists>c::'x. c\<notin>A"
proof -
  from  fs at4[OF at] have "infinite ((UNIV::'x set) - A)" 
    by (simp add: Diff_infinite_finite)
  hence "((UNIV::'x set) - A) \<noteq> ({}::'x set)" by (force simp only:)
  hence "\<exists>c::'x. c\<in>((UNIV::'x set) - A)" by force
  thus "\<exists>c::'x. c\<notin>A" by force
qed

--"there always exists a fresh name for an object with finite support"
lemma at_exists_fresh: 
  fixes  x :: "'a"
  assumes at: "at TYPE('x)"
  and     fs: "finite ((supp x)::'x set)"
  shows "\<exists>c::'x. c\<sharp>x"
  by (simp add: fresh_def, rule ex_in_inf[OF at, OF fs])

--"the at-props imply the pt-props"
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 add: prm_eq_def)
done

section {* finite support properties *}
(*===================================*)

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

lemma fs_at_inst:
  fixes a :: "'x"
  assumes at: "at TYPE('x)"
  shows "fs TYPE('x) TYPE('x)"
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\<times>'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_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_bool_inst:
  shows "fs TYPE(bool) TYPE('x)"
apply(simp add: fs_def, rule allI)
apply(simp add: supp_bool)
done

lemma fs_int_inst:
  shows "fs TYPE(int) TYPE('x)"
apply(simp add: fs_def, rule allI)
apply(simp add: supp_int)
done

section {* Lemmas about the permutation properties *}
(*=================================================*)

lemma pt1:
  fixes x::"'a"
  assumes a: "pt TYPE('a) TYPE('x)"
  shows "([]::'x prm)\<bullet>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)\<bullet>x = pi1\<bullet>(pi2\<bullet>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 \<sim> pi2 \<Longrightarrow> pi1\<bullet>x = pi2\<bullet>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 \<sim> pi2 \<Longrightarrow> (rev pi1)\<bullet>x = (rev pi2)\<bullet>x"
  by (rule pt3[OF pt], simp add: at_prm_rev_eq[OF at])

section {* composition properties *}
(* ============================== *)
lemma cp1:
  fixes pi1::"'x prm"
  and   pi2::"'y prm"
  and   x  ::"'a"
  assumes cp: "cp TYPE ('a) TYPE('x) TYPE('y)"
  shows "pi1\<bullet>(pi2\<bullet>x) = (pi1\<bullet>pi2)\<bullet>(pi1\<bullet>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 {* permutation type instances *}
(* ===================================*)

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_list_nil: 
  fixes xs :: "'a list"
  assumes pt: "pt TYPE('a) TYPE ('x)"
  shows "([]::'x prm)\<bullet>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)\<bullet>xs = pi1\<bullet>(pi2\<bullet>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 \<sim> pi2  \<Longrightarrow> pi1\<bullet>xs = pi2\<bullet>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_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 \<times> '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_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\<Rightarrow>'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) \<sim> (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_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_bool_inst:
  shows  "pt TYPE(bool) TYPE('x)"
  apply(auto simp add: pt_def)
  apply(case_tac "x=True", simp add: perm_bool_def, simp add: perm_bool_def)+
  done

lemma pt_prm_inst:
  assumes at: "at TYPE('x)"
  shows  "pt TYPE('x prm) TYPE('x)"
apply(rule pt_list_inst)
apply(rule pt_prod_inst)
apply(rule at_pt_inst[OF at])+
done

section {* further lemmas for permutation types *}
(*==============================================*)

lemma pt_rev_pi:
  fixes pi :: "'x prm"
  and   x  :: "'a"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE('x)"
  shows "(rev pi)\<bullet>(pi\<bullet>x) = x"
proof -
  have "((rev pi)@pi) \<sim> ([]::'x prm)" by (simp add: at_ds7[OF at])
  hence "((rev pi)@pi)\<bullet>(x::'a) = ([]::'x prm)\<bullet>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\<bullet>((rev pi)\<bullet>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\<bullet>x) = y"
  shows   "x=(rev pi)\<bullet>y"
proof -
  from a have "y=(pi\<bullet>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)\<bullet>y"
  shows   "(pi\<bullet>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\<bullet>x = pi\<bullet>y) = (x=y)"
proof 
  assume "pi\<bullet>x = pi\<bullet>y" 
  hence  "x=(rev pi)\<bullet>(pi\<bullet>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\<bullet>x = pi\<bullet>y" by simp
qed

lemma pt_bij3:
  fixes pi :: "'x prm"
  and   x  :: "'a"
  and   y  :: "'a"
  assumes a:  "x=y"
  shows "(pi\<bullet>x = pi\<bullet>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\<bullet>x = pi\<bullet>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)]\<bullet>([(a,b)]\<bullet>x) = x"
  by (rule pt_bij2[OF pt, OF at], simp)

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\<bullet>x)\<in>X) = (x\<in>((rev pi)\<bullet>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\<in>(pi\<bullet>X)) = (((rev pi)\<bullet>x)\<in>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\<bullet>x)\<in>(pi\<bullet>X)) = (x\<in>X)"
  by (simp add: perm_set_def pt_set_bij1[OF pt, OF at] pt_bij[OF pt, OF at])

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\<in>X"
  shows "(pi\<bullet>x)\<in>(pi\<bullet>X)"
  using a by (simp add: pt_set_bij[OF pt, OF at])

lemma pt_set_bij3:
  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\<bullet>(x\<in>X) = (x\<in>X)"
apply(case_tac "x\<in>X = True")
apply(auto)
done

lemma pt_list_set_pi:
  fixes pi :: "'x prm"
  and   xs :: "'a list"
  assumes pt: "pt TYPE('a) TYPE('x)"
  shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)"
by (induct xs, auto simp add: perm_set_def pt1[OF pt])

-- "some helper lemmas for the pt_perm_supp_ineq lemma"
lemma Collect_permI: 
  fixes pi :: "'x prm"
  and   x  :: "'a"
  assumes a: "\<forall>x. (P1 x = P2 x)" 
  shows "{pi\<bullet>x| x. P1 x} = {pi\<bullet>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\<bullet>x| x::'x. P x} = {x::'x. P ((rev pi)\<bullet>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\<bullet>x = pi\<bullet>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\<bullet>X) = finite X"
proof -
  have image: "(pi\<bullet>X) = (perm pi ` X)" by (force simp only: perm_set_def)
  show ?thesis
  proof (rule iffI)
    assume "finite (pi\<bullet>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\<bullet>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\<bullet>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\<bullet>((supp x)::'y set)) = supp (pi\<bullet>x)" (is "?LHS = ?RHS")
proof -
  have "?LHS = {pi\<bullet>a | a. infinite {b. [(a,b)]\<bullet>x \<noteq> x}}" by (simp add: supp_def perm_set_def)
  also have "\<dots> = {pi\<bullet>a | a. infinite {pi\<bullet>b | b. [(a,b)]\<bullet>x \<noteq> x}}" 
  proof (rule Collect_permI, rule allI, rule iffI)
    fix a
    assume "infinite {b::'y. [(a,b)]\<bullet>x  \<noteq> x}"
    hence "infinite (pi\<bullet>{b::'y. [(a,b)]\<bullet>x \<noteq> x})" by (simp add: pt_set_infinite_ineq[OF ptb, OF at])
    thus "infinite {pi\<bullet>b |b::'y. [(a,b)]\<bullet>x  \<noteq> x}" by (simp add: perm_set_def)
  next
    fix a
    assume "infinite {pi\<bullet>b |b::'y. [(a,b)]\<bullet>x \<noteq> x}"
    hence "infinite (pi\<bullet>{b::'y. [(a,b)]\<bullet>x \<noteq> x})" by (simp add: perm_set_def)
    thus "infinite {b::'y. [(a,b)]\<bullet>x  \<noteq> x}" 
      by (simp add: pt_set_infinite_ineq[OF ptb, OF at])
  qed
  also have "\<dots> = {a. infinite {b::'y. [((rev pi)\<bullet>a,(rev pi)\<bullet>b)]\<bullet>x \<noteq> x}}" 
    by (simp add: pt_set_eq_ineq[OF ptb, OF at])
  also have "\<dots> = {a. infinite {b. pi\<bullet>([((rev pi)\<bullet>a,(rev pi)\<bullet>b)]\<bullet>x) \<noteq> (pi\<bullet>x)}}"
    by (simp add: pt_bij[OF pta, OF at])
  also have "\<dots> = {a. infinite {b. [(a,b)]\<bullet>(pi\<bullet>x) \<noteq> (pi\<bullet>x)}}"
  proof (rule Collect_cong, rule Infinite_cong, rule Collect_cong)
    fix a::"'y" and b::"'y"
    have "pi\<bullet>(([((rev pi)\<bullet>a,(rev pi)\<bullet>b)])\<bullet>x) = [(a,b)]\<bullet>(pi\<bullet>x)"
      by (simp add: cp1[OF cp] pt_pi_rev[OF ptb, OF at])
    thus "(pi\<bullet>([((rev pi)\<bullet>a,(rev pi)\<bullet>b)]\<bullet>x) \<noteq>  pi\<bullet>x) = ([(a,b)]\<bullet>(pi\<bullet>x) \<noteq> pi\<bullet>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\<bullet>((supp x)::'x set)) = supp (pi\<bullet>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\<bullet>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\<sharp>(pi\<bullet>x) = ((rev pi)\<bullet>a)\<sharp>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\<bullet>a)\<sharp>x = a\<sharp>((rev pi)\<bullet>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\<bullet>a)\<sharp>(pi\<bullet>x) = a\<sharp>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\<sharp>(pi\<bullet>x) = ((rev pi)\<bullet>a)\<sharp>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\<bullet>a)\<sharp>x = a\<sharp>((rev pi)\<bullet>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\<bullet>a)\<sharp>(pi\<bullet>x) = a\<sharp>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\<sharp>x"
  shows "(pi\<bullet>a)\<sharp>(pi\<bullet>x)"
using a by (simp add: 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: "\<not>(a\<sharp>x)"
  and     a2: "b\<sharp>x"
  shows "[(a,b)]\<bullet>x \<noteq> x"
proof
  assume neg: "[(a,b)]\<bullet>x = x"
  from a1 have a1':"a\<in>(supp x)" by (simp add: fresh_def) 
  from a2 have a2':"b\<notin>(supp x)" by (simp add: fresh_def) 
  from a1' a2' have a3: "a\<noteq>b" by force
  from a1' have "([(a,b)]\<bullet>a)\<in>([(a,b)]\<bullet>(supp x))" 
    by (simp only: pt_set_bij[OF at_pt_inst[OF at], OF at])
  hence "b\<in>([(a,b)]\<bullet>(supp x))" by (simp add: at_append[OF at] at_calc[OF at])
  hence "b\<in>(supp ([(a,b)]\<bullet>x))" by (simp add: pt_perm_supp[OF pt,OF at])
  with a2' neg show False by simp
qed

-- "three helper lemmas for the perm_fresh_fresh-lemma"
lemma comprehension_neg_UNIV: "{b. \<not> P b} = UNIV - {b. P b}"
  by (auto)

lemma infinite_or_neg_infinite:
  assumes h:"infinite (UNIV::'a set)"
  shows "infinite {b::'a. P b} \<or> infinite {b::'a. \<not> P b}"
proof (subst comprehension_neg_UNIV, case_tac "finite {b. P b}")
  assume j:"finite {b::'a. P b}"
  have "infinite ((UNIV::'a set) - {b::'a. P b})"
    using Diff_infinite_finite[OF j h] by auto
  thus "infinite {b::'a. P b} \<or> infinite (UNIV - {b::'a. P b})" ..
next
  assume j:"infinite {b::'a. P b}"
  thus "infinite {b::'a. P b} \<or> infinite (UNIV - {b::'a. P b})" by simp
qed

--"the co-set of a finite set is infinte"
lemma finite_infinite:
  assumes a: "finite {b::'x. P b}"
  and     b: "infinite (UNIV::'x set)"        
  shows "infinite {b. \<not>P b}"
  using a and infinite_or_neg_infinite[OF b] by simp

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\<sharp>x" and a2: "b\<sharp>x" 
  shows "[(a,b)]\<bullet>x=x"
proof (cases "a=b")
  assume c1: "a=b"
  have "[(a,a)] \<sim> []" by (rule at_ds1[OF at])
  hence "[(a,b)] \<sim> []" using c1 by simp
  hence "[(a,b)]\<bullet>x=([]::'x prm)\<bullet>x" by (rule pt3[OF pt])
  thus ?thesis by (simp only: pt1[OF pt])
next
  assume c2: "a\<noteq>b"
  from a1 have f1: "finite {c. [(a,c)]\<bullet>x \<noteq> x}" by (simp add: fresh_def supp_def)
  from a2 have f2: "finite {c. [(b,c)]\<bullet>x \<noteq> x}" by (simp add: fresh_def supp_def)
  from f1 and f2 have f3: "finite {c. perm [(a,c)] x \<noteq> x \<or> perm [(b,c)] x \<noteq> x}" 
    by (force simp only: Collect_disj_eq)
  have "infinite {c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}" 
    by (simp add: finite_infinite[OF f3,OF at4[OF at], simplified])
  hence "infinite ({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b})" 
    by (force dest: Diff_infinite_finite)
  hence "({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b}) \<noteq> {}" 
    by (auto iff del: finite_Diff_insert Diff_eq_empty_iff)
  hence "\<exists>c. c\<in>({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b})" by (force)
  then obtain c 
    where eq1: "[(a,c)]\<bullet>x = x" 
      and eq2: "[(b,c)]\<bullet>x = x" 
      and ineq: "a\<noteq>c \<and> b\<noteq>c"
    by (force)
  hence "[(a,c)]\<bullet>([(b,c)]\<bullet>([(a,c)]\<bullet>x)) = x" by simp 
  hence eq3: "[(a,c),(b,c),(a,c)]\<bullet>x = x" by (simp add: pt2[OF pt,symmetric])
  from c2 ineq have "[(a,c),(b,c),(a,c)] \<sim> [(a,b)]" by (simp add: at_ds3[OF at])
  hence "[(a,c),(b,c),(a,c)]\<bullet>x = [(a,b)]\<bullet>x" by (rule pt3[OF pt])
  thus ?thesis using eq3 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\<bullet>(pi1\<bullet>x) = (pi2\<bullet>pi1)\<bullet>(pi2\<bullet>x)" 
proof -
  have "(pi2@pi1) \<sim> ((pi2\<bullet>pi1)@pi2)" by (rule at_ds8)
  hence "(pi2@pi1)\<bullet>x = ((pi2\<bullet>pi1)@pi2)\<bullet>x" by (rule pt3[OF pt])
  thus ?thesis by (simp add: pt2[OF pt])
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)\<bullet>((rev pi1)\<bullet>x) = (rev pi1)\<bullet>(rev (pi1\<bullet>pi2)\<bullet>x)" 
proof -
  have "((rev pi2)@(rev pi1)) \<sim> ((rev pi1)@(rev (pi1\<bullet>pi2)))" by (rule at_ds9[OF at])
  hence "((rev pi2)@(rev pi1))\<bullet>x = ((rev pi1)@(rev (pi1\<bullet>pi2)))\<bullet>x" by (rule pt3[OF pt])
  thus ?thesis by (simp add: pt2[OF pt])
qed

section {* facts about supports *}
(*==============================*)

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

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 "op supports_def", intro strip)
  fix a b
  assume "(a::'x)\<notin>(supp x) \<and> (b::'x)\<notin>(supp x)"
  hence "a\<sharp>x" and "b\<sharp>x" by (auto simp add: fresh_def)
  thus "[(a,b)]\<bullet>x = x" by (rule pt_fresh_fresh[OF pt, OF at])
qed

lemma supp_is_subset:
  fixes S :: "'x set"
  and   x :: "'a"
  assumes a1: "S supports x"
  and     a2: "finite S"
  shows "(supp x)\<subseteq>S"
proof (rule ccontr)
  assume "\<not>(supp x \<subseteq> S)"
  hence "\<exists>a. a\<in>(supp x) \<and> a\<notin>S" by force
  then obtain a where b1: "a\<in>supp x" and b2: "a\<notin>S" by force
  from a1 b2 have "\<forall>b. (b\<notin>S \<longrightarrow> ([(a,b)]\<bullet>x = x))" by (unfold "op supports_def", force)
  with a1 have "{b. [(a,b)]\<bullet>x \<noteq> x}\<subseteq>S" by (unfold "op supports_def", force)
  with a2 have "finite {b. [(a,b)]\<bullet>x \<noteq> x}" by (simp add: finite_subset)
  hence "a\<notin>(supp x)" by (unfold supp_def, auto)
  with b1 show False by simp
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)\<subseteq>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) = (\<Inter> {S. finite S \<and> S supports x})"
proof (rule equalityI)
  show "((supp x)::'x set) \<subseteq> (\<Inter> {S. finite S \<and> S supports x})"
  proof (clarify)
    fix S c
    assume b: "c\<in>((supp x)::'x set)" and "finite (S::'x set)" and "S supports x"
    hence  "((supp x)::'x set)\<subseteq>S" by (simp add: supp_is_subset) 
    with b show "c\<in>S" by force
  qed
next
  show "(\<Inter> {S. finite S \<and> S supports x}) \<subseteq> ((supp x)::'x set)"
  proof (clarify, simp)
    fix c
    assume d: "\<forall>(S::'x set). finite S \<and> S supports x \<longrightarrow> c\<in>S"
    have "((supp x)::'x set) supports x" by (rule supp_supports[OF pt, OF at])
    with d fs1[OF fs] show "c\<in>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: "\<forall>S'. (finite S' \<and> S' supports x) \<longrightarrow> S\<subseteq>S'"
  shows "S = (supp x)"
proof (rule equalityI)
  show "((supp x)::'x set)\<subseteq>S" using a1 a2 by (rule supp_is_subset)
next
  have s1: "((supp x)::'x set) supports x" by (rule supp_supports[OF pt, OF at])
  have "((supp x)::'x set)\<subseteq>S" using a1 a2 by (rule supp_is_subset)
  hence "finite ((supp x)::'x set)" using a2 by (simp add: finite_subset)
  with s1 a3 show "S\<subseteq>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: "\<forall>x\<in>X. (\<forall>(a::'x) (b::'x). a\<notin>S\<and>b\<notin>S \<longrightarrow> ([(a,b)]\<bullet>x)\<in>X)"
  shows  "S supports X"
using a
apply(auto simp add: "op 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\<notin>S"
  shows "a\<sharp>x"
proof (simp add: fresh_def)
  have "(supp x)\<subseteq>S" using a1 a2 by (rule supp_is_subset)
  thus "a\<notin>(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 (simp add: "op supports_def", intro strip)
  fix a b
  assume "a\<notin>X \<and> b\<notin>X"
  thus "[(a,b)]\<bullet>X = X" by (force simp add: perm_set_def at_calc[OF at])
qed

lemma at_fin_set_supp:
  fixes X::"'x set"
  assumes at: "at TYPE('x)"
  and     fs: "finite X"
  shows "(supp X) = X"
proof -
  have pt_set: "pt TYPE('x set) TYPE('x)" 
    by (rule pt_set_inst[OF at_pt_inst[OF at]])
  have X_supports_X: "X supports X" by (rule at_fin_set_supports[OF at])
  show ?thesis using  pt_set at X_supports_X fs
  proof (rule supp_is_least_supports[symmetric])
    show "\<forall>S'. finite S' \<and> S' supports X \<longrightarrow> X \<subseteq> S'"
    proof (auto)
      fix S'::"'x set" and x::"'x"
      assume f: "finite S'"
      and    s: "S' supports X"
      and    e1: "x\<in>X"
      show "x\<in>S'"
      proof (rule ccontr)
	assume e2: "x\<notin>S'"
	have "\<exists>b. b\<notin>(X\<union>S')" by (force intro: ex_in_inf[OF at] simp only: fs f)
	then obtain b where b1: "b\<notin>X" and b2: "b\<notin>S'" by (auto)
	from s e2 b2 have c1: "[(x,b)]\<bullet>X=X" by (simp add: "op supports_def")
	from e1 b1 have c2: "[(x,b)]\<bullet>X\<noteq>X" by (force simp add: perm_set_def at_calc[OF at])
	show "False" using c1 c2 by simp
      qed
    qed
  qed
qed

section {* Permutations acting on Functions *}
(*==========================================*)

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


--"sometimes pt_fun_app_eq does to much; this lemma 'corrects it'"
lemma pt_perm:
  fixes x  :: "'a"
  and   pi1 :: "'x prm"
  and   pi2 :: "'x prm"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     at: "at TYPE ('x)"
  shows "(pi1\<bullet>perm pi2)(pi1\<bullet>x) = pi1\<bullet>(pi2\<bullet>x)" 
  by (simp add: pt_fun_app_eq[OF pt, OF at])


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

-- "two helper lemmas for the equivariance of functions"
lemma pt_swap_eq_aux:
  fixes   y :: "'a"
  and    pi :: "'x prm"
  assumes pt: "pt TYPE('a) TYPE('x)"
  and     a: "\<forall>(a::'x) (b::'x). [(a,b)]\<bullet>y = y"
  shows "pi\<bullet>y = y"
proof(induct pi)
    case Nil show ?case by (simp add: pt1[OF pt])
  next
    case (Cons x xs)
    have "\<exists>a b. x=(a,b)" by force
    then obtain a b where p: "x=(a,b)" by force
    assume i: "xs\<bullet>y = y"
    have "x#xs = [x]@xs" by simp
    hence "(x#xs)\<bullet>y = ([x]@xs)\<bullet>y" by simp
    hence "(x#xs)\<bullet>y = [x]\<bullet>(xs\<bullet>y)" by (simp only: pt2[OF pt])
    thus ?case using a i p by (force)
  qed

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

lemma pt_eqvt_fun1a:
  fixes f     :: "'a\<Rightarrow>'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 "\<forall>(pi::'x prm). pi\<bullet>f = f" 
proof (intro strip)
  fix pi