--- a/Nominal-General/Nominal2_Eqvt.thy	Sun Nov 14 10:02:30 2010 +0000
+++ b/Nominal-General/Nominal2_Eqvt.thy	Sun Nov 14 11:05:22 2010 +0000
@@ -33,10 +33,13 @@
   swap_eqvt flip_eqvt
 
   (* datatypes *)
-  Pair_eqvt permute_list.simps
+  Pair_eqvt permute_list.simps 
 
   (* sets *)
-  mem_eqvt insert_eqvt
+  mem_eqvt empty_eqvt insert_eqvt set_eqvt
+
+  (* fsets *)
+  permute_fset fset_eqvt
 
 text {* helper lemmas for the perm_simp *}
 
@@ -79,7 +82,7 @@
 apply(simp)
 done
 
-section {* Logical Operators *}
+subsection {* Equivariance of Logical Operators *}
 
 lemma eq_eqvt[eqvt]:
   shows "p \<bullet> (x = y) \<longleftrightarrow> (p \<bullet> x) = (p \<bullet> y)"
@@ -128,7 +131,7 @@
   apply(rule theI'[OF unique])
   done
 
-section {* Set Operations *}
+subsection {* Equivariance Set Operations *}
 
 lemma not_mem_eqvt:
   shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)"
@@ -152,11 +155,6 @@
   unfolding Ball_def
   by (perm_simp) (rule refl)
 
-lemma empty_eqvt[eqvt]:
-  shows "p \<bullet> {} = {}"
-  unfolding empty_def
-  by (perm_simp) (rule refl)
-
 lemma supp_set_empty:
   shows "supp {} = {}"
   unfolding supp_def
@@ -223,7 +221,7 @@
   shows "supp (set xs) = supp xs"
 apply(induct xs)
 apply(simp add: supp_set_empty supp_Nil)
-apply(simp add: supp_Cons supp_of_fin_insert)
+apply(simp add: supp_Cons supp_of_finite_insert)
 done
 
 
@@ -253,21 +251,19 @@
   shows "a \<sharp> rev xs \<longleftrightarrow> a \<sharp> xs"
   by (induct xs) (auto simp add: fresh_append fresh_Cons fresh_Nil)
 
-lemma set_eqvt[eqvt]:
-  shows "p \<bullet> (set xs) = set (p \<bullet> xs)"
-  by (induct xs) (simp_all add: empty_eqvt insert_eqvt)
-
-(* needs finite support premise
-lemma supp_set:
-  fixes x :: "'a::pt"
-  shows "supp (set xs) = supp xs"
-*)
-
 lemma map_eqvt[eqvt]: 
   shows "p \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> xs)"
   by (induct xs) (simp_all, simp only: permute_fun_app_eq)
 
-section {* Product Operations *}
+
+subsection {* Equivariance for fsets *} 
+
+lemma map_fset_eqvt[eqvt]: 
+  shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"
+  by (lifting map_eqvt)
+
+
+subsection {* Product Operations *}
 
 lemma fst_eqvt[eqvt]:
   "p \<bullet> (fst x) = fst (p \<bullet> x)"
@@ -379,7 +375,7 @@
 ML {* Nominal_ThmDecls.is_eqvt @{context} @{term "supp"} *}
 
 
-section {* Automatic equivariance procedure for inductive definitions *}
+section {* automatic equivariance procedure for inductive definitions *}
 
 use "nominal_eqvt.ML"