--- a/Nominal/Nominal2_FSet.thy	Sat Aug 28 13:41:31 2010 +0800
+++ b/Nominal/Nominal2_FSet.thy	Sat Aug 28 18:15:23 2010 +0800
@@ -5,20 +5,16 @@
         FSet 
 begin
 
-lemma "p \<bullet> {} = {}"
-apply(perm_simp)
-by simp
-
 lemma permute_rsp_fset[quot_respect]:
-  "(op = ===> list_eq ===> list_eq) permute permute"
-  apply (simp add: eqvts[symmetric])
-  apply clarify
-  apply (subst permute_minus_cancel(1)[symmetric, of "xb"])
-  apply (subst mem_eqvt[symmetric])
-  apply (subst (2) permute_minus_cancel(1)[symmetric, of "xb"])
-  apply (subst mem_eqvt[symmetric])
-  apply (erule_tac x="- x \<bullet> xb" in allE)
-  apply simp
+  shows "(op = ===> list_eq ===> list_eq) permute permute"
+  apply(simp)
+  apply(clarify)
+  apply(simp add: eqvts[symmetric])  
+  apply(subst permute_minus_cancel(1)[symmetric, of "xb"])
+  apply(subst mem_eqvt[symmetric])
+  apply(subst (2) permute_minus_cancel(1)[symmetric, of "xb"])
+  apply(subst mem_eqvt[symmetric])
+  apply(simp)
   done
 
 instantiation fset :: (pt) pt
@@ -40,29 +36,14 @@
 
 end
 
-lemma "p \<bullet> {} = {}"
-apply(perm_simp)
-by simp
-
 lemma permute_fset[simp]:
   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 "p \<bullet> {} = {}"
-apply(perm_simp)
-by simp
-
-ML {* @{term "{}"} ; @{term "{||}"} *}
-
 declare permute_fset[eqvt]
 
-lemma "p \<bullet> {} = {}"
-apply(perm_simp)
-by simp
-
-
 lemma fmap_eqvt[eqvt]: 
   shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)"
   by (lifting map_eqvt)
@@ -80,6 +61,11 @@
   unfolding supp_def
   by (perm_simp) (simp add: fset_cong)
 
+lemma supp_fempty:
+  shows "supp {||} = {}"
+  unfolding supp_def
+  by simp
+
 lemma supp_finsert:
   fixes x::"'a::fs"
   shows "supp (finsert x S) = supp x \<union> supp S"
@@ -89,10 +75,6 @@
   apply(simp add: supp_fset_to_set)
   done
 
-lemma supp_fempty:
-  shows "supp {||} = {}"
-  unfolding supp_def
-  by simp
 
 instance fset :: (fs) fs
   apply (default)
@@ -125,8 +107,9 @@
   done
 
 lemma fresh_star_atom:
-  "fset_to_set s \<sharp>* (a :: _ :: at_base) \<Longrightarrow> atom a \<sharp> fset_to_set s"
-  apply (induct s)
+  fixes a::"'a::at_base"
+  shows "fset_to_set S \<sharp>* a \<Longrightarrow> atom a \<sharp> fset_to_set S"
+  apply (induct S)
   apply (simp add: fresh_set_empty)
   apply simp
   apply (unfold fresh_def)
@@ -140,8 +123,4 @@
   apply auto
   done
 
-lemma "p \<bullet> {} = {}"
-apply(perm_simp)
-by simp
-
 end