# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1325591007 0
# Node ID f7c4b8e6918be60897bcf8dcd208a4a728ba2321
# Parent  9a63d90d1752eda4b81a02a1cdca2e6a114c6828
updated to explicit set type constructor (post Isabelle 3rd January)

diff -r 9a63d90d1752 -r f7c4b8e6918b LMCS-Review
--- a/LMCS-Review	Tue Jan 03 01:42:10 2012 +0000
+++ b/LMCS-Review	Tue Jan 03 11:43:27 2012 +0000
@@ -203,6 +203,18 @@
 >   of pairs. I think that the system should at the very least allow encoding
 >   this example, otherwise set-abstractions will not be very useful in
 >   practice.
+
+>> datatype trm =
+>>       Var string
+>>     | App trm trm
+>>     | Lam string trm
+>>     | Let "(string * trm) fset" trm
+>> Not a problem. Both finite sets and bags should be possible as
+>> constructors within the new package.
+>> Best regards and a happy new year!
+>> Andrei Popescu
+
+
 >
 > Detailed comments
 >
diff -r 9a63d90d1752 -r f7c4b8e6918b Nominal/Ex/LamTest.thy
--- a/Nominal/Ex/LamTest.thy	Tue Jan 03 01:42:10 2012 +0000
+++ b/Nominal/Ex/LamTest.thy	Tue Jan 03 11:43:27 2012 +0000
@@ -1658,7 +1658,7 @@
   and   S::"'a::at set"
   assumes a: "a \<notin> S" "b \<notin> S"
   shows "(a \<leftrightarrow> b) \<bullet> S = S"
-  unfolding permute_set_eq
+  unfolding permute_set_def
   using a by (auto simp add: permute_flip_at)
 
 lemma removeAll_eqvt[eqvt]:
diff -r 9a63d90d1752 -r f7c4b8e6918b Nominal/Ex/TypeSchemes1.thy
--- a/Nominal/Ex/TypeSchemes1.thy	Tue Jan 03 01:42:10 2012 +0000
+++ b/Nominal/Ex/TypeSchemes1.thy	Tue Jan 03 11:43:27 2012 +0000
@@ -2,7 +2,7 @@
 imports "../Nominal2"
 begin
 
-section {*** Type Schemes defined as two separate nominal datatypes ***}
+section {* Type Schemes defined as two separate nominal datatypes *}
 
 atom_decl name 
 
@@ -26,6 +26,40 @@
 thm tys.supp
 thm tys.fresh
 
+subsection {* Some Tests about Alpha-Equality *}
+
+lemma
+  shows "All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|b, a|}]. ((Var a) \<rightarrow> (Var b))"
+  apply(simp add: Abs_eq_iff)
+  apply(rule_tac x="0::perm" in exI)
+  apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
+  done
+
+lemma
+  shows "All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|a, b|}].((Var b) \<rightarrow> (Var a))"
+  apply(simp add: Abs_eq_iff)
+  apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
+  apply(simp add: alphas fresh_star_def supp_at_base ty.supp)
+  done
+
+lemma
+  shows "All [{|a, b, c|}].((Var a) \<rightarrow> (Var b)) = All [{|a, b|}].((Var a) \<rightarrow> (Var b))"
+  apply(simp add: Abs_eq_iff)
+  apply(rule_tac x="0::perm" in exI)
+  apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
+done
+
+lemma
+  assumes a: "a \<noteq> b"
+  shows "\<not>(All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|c|}].((Var c) \<rightarrow> (Var c)))"
+  using a
+  apply(simp add: Abs_eq_iff)
+  apply(clarify)
+  apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
+  apply auto
+  done
+
+
 subsection {* Substitution function for types and type schemes *}
 
 type_synonym 
@@ -39,10 +73,7 @@
 
 lemma lookup_eqvt[eqvt]:
   shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)"
-apply(induct Ts T rule: lookup.induct)
-apply(simp_all)
-done
-
+  by (induct Ts T rule: lookup.induct) (simp_all)
 
 nominal_primrec
   subst  :: "Subst \<Rightarrow> ty \<Rightarrow> ty" ("_<_>" [100,60] 120)
@@ -124,69 +155,14 @@
 termination (eqvt)
   by (lexicographic_order)
 
-text {* Some Tests about Alpha-Equality *}
 
-lemma
-  shows "All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|b, a|}]. ((Var a) \<rightarrow> (Var b))"
-  apply(simp add: Abs_eq_iff)
-  apply(rule_tac x="0::perm" in exI)
-  apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
-  done
-
-lemma
-  shows "All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|a, b|}].((Var b) \<rightarrow> (Var a))"
-  apply(simp add: Abs_eq_iff)
-  apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
-  apply(simp add: alphas fresh_star_def supp_at_base ty.supp)
-  done
-
-lemma
-  shows "All [{|a, b, c|}].((Var a) \<rightarrow> (Var b)) = All [{|a, b|}].((Var a) \<rightarrow> (Var b))"
-  apply(simp add: Abs_eq_iff)
-  apply(rule_tac x="0::perm" in exI)
-  apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
-done
+subsection {* Generalisation of types and type-schemes*}
 
-lemma
-  assumes a: "a \<noteq> b"
-  shows "\<not>(All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|c|}].((Var c) \<rightarrow> (Var c)))"
-  using a
-  apply(simp add: Abs_eq_iff)
-  apply(clarify)
-  apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
-  apply auto
-  done
-
-
-text {* HERE *}
-
-fun 
-  compose::"Subst \<Rightarrow> Subst \<Rightarrow> Subst" ("_ \<circ> _" [100,100] 100)
+fun
+  subst_dom_pi :: "Subst \<Rightarrow> perm \<Rightarrow> Subst" ("_|_")
 where
-  "\<theta>\<^isub>1 \<circ> [] = \<theta>\<^isub>1"
-| "\<theta>\<^isub>1 \<circ> ((X,T)#\<theta>\<^isub>2) = (X,\<theta>\<^isub>1<T>)#(\<theta>\<^isub>1 \<circ> \<theta>\<^isub>2)"
-
-lemma compose_eqvt:
-  fixes  \<theta>1 \<theta>2::"Subst"
-  shows "(p \<bullet> (\<theta>1 \<circ> \<theta>2)) = ((p \<bullet> \<theta>1) \<circ> (p \<bullet> \<theta>2))"
-apply(induct \<theta>2) 
-apply(auto simp add: subst.eqvt)
-done
-
-lemma compose_ty:
-  fixes  \<theta>1 :: "Subst"
-  and    \<theta>2 :: "Subst"
-  and    T :: "ty"
-  shows "\<theta>1<\<theta>2<T>> = (\<theta>1\<circ>\<theta>2)<T>"
-proof (induct T rule: ty.induct)
-  case (Var X) 
-  have "\<theta>1<lookup \<theta>2 X> = lookup (\<theta>1\<circ>\<theta>2) X" 
-    by (induct \<theta>2) (auto)
-  then show ?case by simp
-next
-  case (Fun T1 T2)
-  then show ?case by simp
-qed
+  "[]|p = []"
+| "((X,T)#\<theta>)|p = (p \<bullet> X, T)#(\<theta>|p)" 
 
 fun
   subst_subst :: "Subst \<Rightarrow> Subst \<Rightarrow> Subst" ("_<_>"  [100,60] 120)
@@ -194,12 +170,6 @@
   "\<theta><[]> = []"
 | "\<theta> <((X,T)#\<theta>')> = (X,\<theta><T>)#(\<theta><\<theta>'>)"
 
-lemma redundant1:
-  fixes \<theta>1::"Subst"
-  and   \<theta>2::"Subst"
-  shows "\<theta>1 \<circ> \<theta>2 = (\<theta>1<\<theta>2>)@\<theta>1"
-by (induct \<theta>2) (auto)
-
 fun
   dom :: "Subst \<Rightarrow> name fset"
 where
@@ -207,38 +177,24 @@
 | "dom ((X,T)#\<theta>) = {|X|} |\<union>| dom \<theta>"
 
 lemma dom_eqvt[eqvt]:
-  shows "(p \<bullet> dom \<theta>) = dom (p \<bullet> \<theta>)"
-apply(induct \<theta> rule: dom.induct)
-apply(simp_all)
-done
+  shows "p \<bullet> (dom \<theta>) = dom (p \<bullet> \<theta>)"
+by (induct \<theta>) (auto)
 
-lemma dom_compose:
-  shows "dom (\<theta>1 \<circ> \<theta>2) = dom \<theta>1 |\<union>| dom \<theta>2"
-apply(induct rule: dom.induct)
-apply(simp)
-apply(simp)
-by (metis sup_commute union_insert_fset)
-
-lemma redundant3:
-  fixes \<theta>1::"Subst"
-  and   \<theta>2::"Subst"
+lemma dom_subst:
+  fixes \<theta>1 \<theta>2::"Subst"
   shows "dom (\<theta>2<\<theta>1>) = (dom \<theta>1)"
 by (induct \<theta>1) (auto)
 
 lemma dom_pi:
-  shows "(p \<bullet> (dom \<theta>)) = dom (map (\<lambda>(X, T). (p \<bullet> X, T)) \<theta>)"
-apply(induct \<theta>)
-apply(auto)
-done
+  shows "dom (\<theta>|p) = dom (p \<bullet> \<theta>)"
+by (induct \<theta>) (auto)
 
 lemma dom_fresh_lookup:
   fixes \<theta>::"Subst"
-  assumes "\<forall>X \<in> fset (dom \<theta>). atom X \<sharp> name"
-  shows "lookup \<theta> name = Var name"
+  assumes "\<forall>Y \<in> fset (dom \<theta>). atom Y \<sharp> X"
+  shows "lookup \<theta> X = Var X"
 using assms
-apply(induct \<theta>)
-apply(auto simp add: fresh_at_base)
-done 
+by (induct \<theta>) (auto simp add: fresh_at_base)
 
 lemma dom_fresh_ty:
   fixes \<theta>::"Subst"
@@ -246,30 +202,20 @@
   assumes "\<forall>X \<in> fset (dom \<theta>). atom X \<sharp> T"
   shows "\<theta><T> = T"
 using assms
-apply(induct T rule: ty.induct)
-apply(auto simp add: ty.fresh dom_fresh_lookup)
-done 
+by (induct T rule: ty.induct) (auto simp add: ty.fresh dom_fresh_lookup)
 
 lemma dom_fresh_subst:
   fixes \<theta> \<theta>'::"Subst"
   assumes "\<forall>X \<in> fset (dom \<theta>). atom X \<sharp> \<theta>'"
   shows "\<theta><\<theta>'> = \<theta>'"
 using assms
-apply(induct \<theta>')
-apply(auto simp add: fresh_Pair fresh_Cons dom_fresh_ty)
-done 
-
-
-abbreviation
-  "sub_list" :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<subseteq> _" [60,60] 60) 
-where
-  "xs\<^isub>1 \<subseteq> xs\<^isub>2 \<equiv> \<forall>x. x \<in> set xs\<^isub>1 \<longrightarrow> x \<in> set xs\<^isub>2"
+by (induct \<theta>') (auto simp add: fresh_Pair fresh_Cons dom_fresh_ty)
 
 
 definition
-  generalises3 :: "ty \<Rightarrow> tys \<Rightarrow> bool" ("_ \<prec>\<prec>\<prec>\<prec> _")
+  generalises :: "ty \<Rightarrow> tys \<Rightarrow> bool" ("_ \<prec>\<prec> _")
 where
-  " T \<prec>\<prec>\<prec>\<prec> S \<longleftrightarrow> (\<exists>\<theta> Xs T'. S = All [Xs].T'\<and> T = \<theta><T'> \<and> dom \<theta> = Xs)"
+  "T \<prec>\<prec> S \<longleftrightarrow> (\<exists>\<theta> Xs T'. S = All [Xs].T'\<and> T = \<theta><T'> \<and> dom \<theta> = Xs)"
 
 
 lemma lookup_fresh:
@@ -277,40 +223,34 @@
   assumes a: "atom X \<sharp> \<theta>"
   shows "lookup \<theta> X = Var X"
   using a
-  apply (induct \<theta>)
-  apply (auto simp add: fresh_Cons fresh_Pair fresh_at_base)
-  done
+  by (induct \<theta>) (auto simp add: fresh_Cons fresh_Pair fresh_at_base)
 
 lemma lookup_dom:
   fixes X::"name"
-  assumes a: "X |\<notin>| dom \<theta>"
+  assumes "X |\<notin>| dom \<theta>"
   shows "lookup \<theta> X = Var X"
-  using a
-  apply (induct \<theta>)
-  apply(auto)
-  done
+  using assms
+  by (induct \<theta>) (auto)
 
 lemma w1: 
-  "\<theta><map (\<lambda>(X, y). (p \<bullet> X, y)) \<theta>'> = map (\<lambda>(X, y). (p \<bullet> X, y)) (\<theta><\<theta>'>)"
-apply(induct \<theta>')
-apply(auto)
-done
+  shows "\<theta><\<theta>'|p> = (\<theta><\<theta>'>)|p"
+  by (induct \<theta>')(auto)
 
 lemma w2:
   assumes "name |\<in>| dom \<theta>'" 
   shows "\<theta><lookup \<theta>' name> = lookup (\<theta><\<theta>'>) name"
 using assms
 apply(induct \<theta>')
-apply(auto)
-by (metis notin_empty_fset)
+apply(auto simp add: notin_empty_fset)
+done
 
 lemma w3:
   assumes "name |\<in>| dom \<theta>" 
-  shows "lookup \<theta> name = lookup (map (\<lambda>(X, y). (p \<bullet> X, y)) \<theta>) (p \<bullet> name)"
+  shows "lookup \<theta> name = lookup (\<theta>|p) (p \<bullet> name)"
 using assms
 apply(induct \<theta>)
-apply(auto)
-by (metis notin_empty_fset)
+apply(auto simp add: notin_empty_fset)
+done
 
 lemma fresh_lookup:
   fixes X Y::"name"
@@ -320,13 +260,13 @@
   using assms
   apply (induct \<theta>)
   apply (auto simp add: fresh_Cons fresh_Pair fresh_at_base ty.fresh)
-done
+  done
 
 lemma test:
   fixes \<theta> \<theta>'::"Subst"
   and T::"ty"
   assumes "(p \<bullet> atom ` fset (dom \<theta>')) \<sharp>* \<theta>" "supp All [dom \<theta>'].T \<sharp>* p"
-  shows "\<theta><\<theta>'<T>> = \<theta><map (\<lambda>(X, y). (p \<bullet> X, y)) \<theta>'><\<theta><p \<bullet> T>>"
+  shows "\<theta><\<theta>'<T>> = \<theta><\<theta>'|p><\<theta><p \<bullet> T>>"
 using assms
 apply(induct T rule: ty.induct)
 defer
@@ -341,7 +281,7 @@
 apply(simp add: w1)
 apply(simp add: w2)
 apply(subst w3[symmetric])
-apply(simp add:redundant3)
+apply(simp add: dom_subst)
 apply(simp)
 apply(perm_simp)
 apply(rotate_tac 2)
@@ -354,18 +294,17 @@
 apply(subst dom_fresh_ty)
 apply(auto)[1]
 apply(rule fresh_lookup)
-apply(simp add: redundant3)
-apply(simp add: dom_pi[symmetric])
+apply(simp add: dom_subst)
+apply(simp add: dom_pi)
 apply(perm_simp)
 apply(rotate_tac 2)
 apply(drule_tac p="p" in permute_boolI)
 apply(perm_simp)
 apply(simp add: fresh_at_base)
 apply (metis in_fset)
-apply(simp add: redundant3)
+apply(simp add: dom_subst)
 apply(simp add: dom_pi[symmetric])
 apply(perm_simp)
-apply metis
 apply(subst supp_perm_eq)
 apply(simp add: supp_at_base fresh_star_def)
 apply (smt Diff_iff atom_eq_iff image_iff insertI1 notin_fset)
@@ -373,8 +312,8 @@
 done
 
 lemma
-  shows "T \<prec>\<prec>\<prec>\<prec> S \<Longrightarrow> \<theta><T> \<prec>\<prec>\<prec>\<prec> \<theta><S>"
-unfolding generalises3_def
+  shows "T \<prec>\<prec> S \<Longrightarrow> \<theta><T> \<prec>\<prec> \<theta><S>"
+unfolding generalises_def
 apply(erule exE)+
 apply(erule conjE)+
 apply(rule_tac t="S" and s="All [Xs].T'" in subst)
@@ -401,17 +340,18 @@
 apply(subst substs.simps)
 apply(perm_simp)
 apply(simp)
-apply(rule_tac x="\<theta><map (\<lambda>(X, T). (p \<bullet> X, T)) \<theta>'>" in exI)
+apply(rule_tac x="\<theta><\<theta>'|p>" in exI)
 apply(rule_tac x="p \<bullet> Xs" in exI)
 apply(rule_tac x="\<theta><p \<bullet> T'>" in exI)
 apply(rule conjI)
 apply(simp)
 apply(rule conjI)
 defer
-apply(simp add: redundant3)
-apply(simp add: dom_pi[symmetric])
+apply(simp add: dom_subst)
+apply(simp add: dom_pi dom_eqvt[symmetric])
 apply(rule_tac t="T" and s="\<theta>'<T'>" in subst)
 apply(simp)
+apply(simp)
 apply(rule test)
 apply(perm_simp)
 apply(rotate_tac 2)
@@ -420,5 +360,19 @@
 apply(auto simp add: fresh_star_def)
 done
 
+lemma 
+  "T \<prec>\<prec>  All [Xs].T' \<longleftrightarrow> (\<exists>\<theta>. T = \<theta><T'> \<and> dom \<theta> = Xs)"
+apply(auto)
+defer
+unfolding generalises_def
+apply(auto)[1]
+apply(auto)[1]
+apply(drule sym)
+apply(simp add: Abs_eq_iff2)
+apply(simp add: alphas)
+apply(auto)
+apply(rule_tac x="map (\<lambda>(X, T). (p \<bullet> X, T)) \<theta>" in exI)
+apply(auto)
+oops
 
 end
diff -r 9a63d90d1752 -r f7c4b8e6918b Nominal/Ex/TypeSchemes2.thy
--- a/Nominal/Ex/TypeSchemes2.thy	Tue Jan 03 01:42:10 2012 +0000
+++ b/Nominal/Ex/TypeSchemes2.thy	Tue Jan 03 11:43:27 2012 +0000
@@ -265,7 +265,7 @@
   apply (subgoal_tac "p \<bullet> supp (subst \<theta>' T) \<subseteq> p \<bullet> supp (\<theta>', T)")
   apply (erule subsetD)
   apply (simp add: supp_eqvt)
-  apply (metis le_eqvt permute_boolI)
+  apply (metis permute_pure subset_eqvt)
   apply (rule perm_supp_eq)
   apply (simp add: fresh_def fresh_star_def)
   apply blast
@@ -307,7 +307,4 @@
   apply auto
   done
 
-
-
-
 end
diff -r 9a63d90d1752 -r f7c4b8e6918b Nominal/Nominal2_Abs.thy
--- a/Nominal/Nominal2_Abs.thy	Tue Jan 03 01:42:10 2012 +0000
+++ b/Nominal/Nominal2_Abs.thy	Tue Jan 03 11:43:27 2012 +0000
@@ -365,7 +365,7 @@
   then have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto
   from * have "\<forall>b \<in> as. p \<bullet> b = p' \<bullet> b" by blast
   then have zb: "p \<bullet> as = p' \<bullet> as" 
-    apply(auto simp add: permute_set_eq)
+    apply(auto simp add: permute_set_def)
     apply(rule_tac x="xa" in exI)
     apply(simp)
     done
@@ -800,7 +800,7 @@
   moreover
   { assume *: "a \<noteq> b" and **: "Abs_set {a} x = Abs_set {b} y"
     have #: "a \<sharp> Abs_set {b} y" by (simp add: **[symmetric] Abs_fresh_iff)
-    have "Abs_set {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_set {b} y)" by (simp add: permute_set_eq assms)
+    have "Abs_set {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_set {b} y)" by (simp add: permute_set_def assms)
     also have "\<dots> = Abs_set {b} y"
       by (rule swap_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
     also have "\<dots> = Abs_set {a} x" using ** by simp
@@ -809,7 +809,7 @@
   moreover 
   { assume *: "a \<noteq> b" and **: "x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y"
     have "Abs_set {a} x = Abs_set {a} ((a \<rightleftharpoons> b) \<bullet> y)" using ** by simp
-    also have "\<dots> = (a \<rightleftharpoons> b) \<bullet> Abs_set {b} y" by (simp add: permute_set_eq assms)
+    also have "\<dots> = (a \<rightleftharpoons> b) \<bullet> Abs_set {b} y" by (simp add: permute_set_def assms)
     also have "\<dots> = Abs_set {b} y"
       by (rule swap_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
     finally have "Abs_set {a} x = Abs_set {b} y" .
@@ -824,7 +824,7 @@
   moreover
   { assume *: "a \<noteq> b" and **: "Abs_res {a} x = Abs_res {b} y"
     have #: "a \<sharp> Abs_res {b} y" by (simp add: **[symmetric] Abs_fresh_iff)
-    have "Abs_res {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_res {b} y)" by (simp add: permute_set_eq assms)
+    have "Abs_res {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_res {b} y)" by (simp add: permute_set_def assms)
     also have "\<dots> = Abs_res {b} y"
       by (rule swap_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
     also have "\<dots> = Abs_res {a} x" using ** by simp
@@ -833,7 +833,7 @@
   moreover 
   { assume *: "a \<noteq> b" and **: "x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y"
     have "Abs_res {a} x = Abs_res {a} ((a \<rightleftharpoons> b) \<bullet> y)" using ** by simp
-    also have "\<dots> = (a \<rightleftharpoons> b) \<bullet> Abs_res {b} y" by (simp add: permute_set_eq assms)
+    also have "\<dots> = (a \<rightleftharpoons> b) \<bullet> Abs_res {b} y" by (simp add: permute_set_def assms)
     also have "\<dots> = Abs_res {b} y"
       by (rule swap_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
     finally have "Abs_res {a} x = Abs_res {b} y" .
diff -r 9a63d90d1752 -r f7c4b8e6918b Nominal/Nominal2_Base.thy
--- 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)