--- a/Nominal/Nominal2_FSet.thy	Fri Apr 30 15:34:26 2010 +0100
+++ b/Nominal/Nominal2_FSet.thy	Fri Apr 30 15:36:02 2010 +0100
@@ -15,7 +15,7 @@
   apply simp
   done
 
-instantiation FSet.fset :: (pt) pt
+instantiation fset :: (pt) pt
 begin
 
 quotient_definition
@@ -34,70 +34,64 @@
 
 end
 
-lemma permute_fset[eqvt]:
-  "(p \<bullet> {||}) = ({||} :: 'a::pt fset)"
-  "p \<bullet> finsert (x :: 'a :: pt) xs = finsert (p \<bullet> x) (p \<bullet> xs)"
+lemma permute_fset[simp, eqvt]:
+  fixes S::"('a::pt) fset"
+  shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)"
+  and "p \<bullet> finsert x S = finsert (p \<bullet> x) (p \<bullet> S)"
   by (lifting permute_list.simps)
 
 lemma fmap_eqvt[eqvt]: 
-  shows "p \<bullet> (fmap f l) = fmap (p \<bullet> f) (p \<bullet> l)"
+  shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)"
   by (lifting map_eqvt)
 
 lemma fset_to_set_eqvt[eqvt]: 
-  shows "p \<bullet> (fset_to_set x) = fset_to_set (p \<bullet> x)"
+  shows "p \<bullet> (fset_to_set S) = fset_to_set (p \<bullet> S)"
   by (lifting set_eqvt)
 
-lemma fin_fset_to_set:
-  shows "finite (fset_to_set x)"
-  by (induct x) (simp_all)
+lemma fin_fset_to_set[simp]:
+  shows "finite (fset_to_set S)"
+  by (induct S) (simp_all)
 
 lemma supp_fset_to_set:
-  "supp (fset_to_set x) = supp x"
+  shows "supp (fset_to_set S) = supp S"
   apply (simp add: supp_def)
   apply (simp add: eqvts)
   apply (simp add: fset_cong)
   done
 
+lemma supp_finsert:
+  fixes x::"'a::fs"
+  shows "supp (finsert x S) = supp x \<union> supp S"
+  apply(subst supp_fset_to_set[symmetric])
+  apply(simp add: supp_fset_to_set)
+  apply(simp add: supp_of_fin_insert)
+  apply(simp add: supp_fset_to_set)
+  done
+
+lemma supp_fempty:
+  shows "supp {||} = {}"
+  unfolding supp_def
+  by simp
+
+instance fset :: (fs) fs
+  apply (default)
+  apply (induct_tac x rule: fset_induct)
+  apply (simp add: supp_fempty)
+  apply (simp add: supp_finsert)
+  apply (simp add: finite_supp)
+  done
+
 lemma atom_fmap_cong:
-  shows "(fmap atom x = fmap atom y) = (x = y)"
+  shows "fmap atom x = fmap atom y \<longleftrightarrow> x = y"
   apply(rule inj_fmap_eq_iff)
   apply(simp add: inj_on_def)
   done
 
 lemma supp_fmap_atom:
-  shows "supp (fmap atom x) = supp x"
+  shows "supp (fmap atom S) = supp S"
   unfolding supp_def
-  apply (perm_simp)
-  apply (simp add: atom_fmap_cong)
-  done
-
-lemma supp_atom_finsert:
-  "supp (finsert (x :: atom) S) = supp x \<union> supp S"
-  apply (subst supp_fset_to_set[symmetric])
-  apply (simp add: supp_finite_atom_set)
-  apply (simp add: supp_atom_insert[OF fin_fset_to_set])
-  apply (simp add: supp_fset_to_set)
-  done
-
-lemma supp_at_finsert:
-  fixes a::"'a::at_base"
-  shows "supp (finsert a S) = supp a \<union> supp S"
-  apply (subst supp_fset_to_set[symmetric])
-  apply (simp add: supp_finite_atom_set)
-  apply (simp add: supp_at_base_insert[OF fin_fset_to_set])
-  apply (simp add: supp_fset_to_set)
-  done
-
-lemma supp_fempty:
-  "supp {||} = {}"
-  by (simp add: supp_def eqvts)
-
-instance fset :: (at_base) fs
-  apply (default)
-  apply (induct_tac x rule: fset_induct)
-  apply (simp add: supp_fempty)
-  apply (simp add: supp_at_finsert)
-  apply (simp add: supp_at_base)
+  apply(perm_simp)
+  apply(simp add: atom_fmap_cong)
   done
 
 lemma supp_at_fset:
@@ -105,8 +99,9 @@
   shows "supp S = fset_to_set (fmap atom S)"
   apply (induct S)
   apply (simp add: supp_fempty)
-  apply (simp add: supp_at_finsert)
+  apply (simp add: supp_finsert)
   apply (simp add: supp_at_base)
   done
 
+
 end