--- a/Nominal/Nominal2_Base.thy	Tue Jan 03 01:42:10 2012 +0000
+++ b/Nominal/Nominal2_Base.thy	Tue Jan 03 11:43:27 2012 +0000
@@ -430,25 +430,33 @@
 
 subsection {* Permutations for sets *}
 
+instantiation "set" :: (pt) pt
+begin
+
+definition
+  "p \<bullet> X = {p \<bullet> x | x. x \<in> X}" 
+
+instance
+apply default
+apply (auto simp add: permute_set_def)
+done
+
+end
+
 lemma permute_set_eq:
-  fixes x::"'a::pt"
-  shows "(p \<bullet> X) = {p \<bullet> x | x. x \<in> X}"
-  unfolding permute_fun_def
-  unfolding permute_bool_def
-  apply(auto simp add: mem_def)
-  apply(rule_tac x="- p \<bullet> x" in exI)
-  apply(simp)
-  done
+  shows "p \<bullet> X = {x. - p \<bullet> x \<in> X}"
+unfolding permute_set_def
+by (auto) (metis permute_minus_cancel(1))
 
 lemma permute_set_eq_image:
   shows "p \<bullet> X = permute p ` X"
-  unfolding permute_set_eq by auto
+  unfolding permute_set_def by auto
 
 lemma permute_set_eq_vimage:
   shows "p \<bullet> X = permute (- p) -` X"
-  unfolding permute_fun_def permute_bool_def
-  unfolding vimage_def Collect_def mem_def ..
-
+  unfolding permute_set_eq vimage_def
+  by simp
+  
 lemma permute_finite [simp]:
   shows "finite (p \<bullet> X) = finite X"
   unfolding permute_set_eq_vimage
@@ -457,36 +465,36 @@
 lemma swap_set_not_in:
   assumes a: "a \<notin> S" "b \<notin> S"
   shows "(a \<rightleftharpoons> b) \<bullet> S = S"
-  unfolding permute_set_eq
+  unfolding permute_set_def
   using a by (auto simp add: swap_atom)
 
 lemma swap_set_in:
   assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b"
   shows "(a \<rightleftharpoons> b) \<bullet> S \<noteq> S"
-  unfolding permute_set_eq
+  unfolding permute_set_def
   using a by (auto simp add: swap_atom)
 
 lemma swap_set_in_eq:
   assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b"
   shows "(a \<rightleftharpoons> b) \<bullet> S = (S - {a}) \<union> {b}"
-  unfolding permute_set_eq
+  unfolding permute_set_def
   using a by (auto simp add: swap_atom)
 
 lemma swap_set_both_in:
   assumes a: "a \<in> S" "b \<in> S"
   shows "(a \<rightleftharpoons> b) \<bullet> S = S"
-  unfolding permute_set_eq
+  unfolding permute_set_def
   using a by (auto simp add: swap_atom)
 
 lemma mem_permute_iff:
   shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
-  unfolding mem_def permute_fun_def permute_bool_def
-  by simp
+  unfolding permute_set_def
+  by auto
 
 lemma empty_eqvt:
   shows "p \<bullet> {} = {}"
-  unfolding empty_def Collect_def
-  by (simp add: permute_fun_def permute_bool_def)
+  unfolding permute_set_def
+  by (simp)
 
 lemma insert_eqvt:
   shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"
@@ -665,6 +673,9 @@
 instance "fun" :: (pure, pure) pure
 by default (simp add: permute_fun_def permute_pure)
 
+instance set :: (pure) pure
+by default (simp add: permute_set_def permute_pure)
+
 instance prod :: (pure, pure) pure
 by default (induct_tac x, simp add: permute_pure)
 
@@ -879,12 +890,13 @@
 
 lemma mem_eqvt [eqvt]:
   shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
-  unfolding mem_def
-  by (rule permute_fun_app_eq)
+  unfolding permute_bool_def permute_set_def
+  by (auto)
 
 lemma Collect_eqvt [eqvt]:
   shows "p \<bullet> {x. P x} = {x. (p \<bullet> P) x}"
-  unfolding Collect_def permute_fun_def ..
+  unfolding permute_set_eq permute_fun_def
+  by (auto simp add: permute_bool_def)
 
 lemma inter_eqvt [eqvt]:
   shows "p \<bullet> (A \<inter> B) = (p \<bullet> A) \<inter> (p \<bullet> B)"
@@ -1871,7 +1883,7 @@
 proof -
   { fix a b
     have "\<forall>x \<in> S. (a \<rightleftharpoons> b) \<bullet> x = x \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> S = S"
-      unfolding permute_set_eq by force
+      unfolding permute_set_def by force
   }
   then show "(\<Union>x \<in> S. supp x) supports S"
     unfolding supports_def 
@@ -2491,7 +2503,7 @@
     using at_set_avoiding2[of "{a}" "c" "x"] assms a by blast
   have c: "(p \<bullet> a) \<sharp> c" using p1
     unfolding fresh_star_def Ball_def 
-    by(erule_tac x="p \<bullet> a" in allE) (simp add: permute_set_eq)
+    by(erule_tac x="p \<bullet> a" in allE) (simp add: permute_set_def)
   hence "p \<bullet> a \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast
   then show "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p" by blast
 qed
@@ -2506,7 +2518,7 @@
 proof (induct)
   case empty
   have "(\<forall>b \<in> {}. 0 \<bullet> b = p \<bullet> b) \<and> supp (0::perm) \<subseteq> {} \<union> p \<bullet> {}"
-    by (simp add: permute_set_eq supp_perm)
+    by (simp add: permute_set_def supp_perm)
   then show "\<exists>q. (\<forall>b \<in> {}. q \<bullet> b = p \<bullet> b) \<and> supp q \<subseteq> {} \<union> p \<bullet> {}" by blast
 next
   case (insert a bs)