--- a/Nominal-General/Nominal2_Eqvt.thy	Sat Sep 04 06:48:14 2010 +0800
+++ b/Nominal-General/Nominal2_Eqvt.thy	Sat Sep 04 07:28:35 2010 +0800
@@ -24,17 +24,19 @@
 section {* eqvt lemmas *}
 
 lemmas [eqvt] =
-  conj_eqvt Not_eqvt ex_eqvt imp_eqvt
+  conj_eqvt Not_eqvt ex_eqvt all_eqvt imp_eqvt
   imp_eqvt[folded induct_implies_def]
   uminus_eqvt
 
   (* nominal *)
-  supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt 
+  supp_eqvt fresh_eqvt fresh_star_eqvt add_perm_eqvt atom_eqvt 
   swap_eqvt flip_eqvt
 
   (* datatypes *)
   Pair_eqvt permute_list.simps
 
+  (* sets *)
+  mem_eqvt insert_eqvt
 
 text {* helper lemmas for the perm_simp *}
 
@@ -99,15 +101,6 @@
   shows "p \<bullet> (A \<or> B) = ((p \<bullet> A) \<or> (p \<bullet> B))"
   by (simp add: permute_bool_def)
 
-lemma Not_eqvt[eqvt]:
-  shows "p \<bullet> (\<not> A) \<longleftrightarrow> \<not> (p \<bullet> A)"
-  by (simp add: permute_bool_def)
-
-lemma all_eqvt[eqvt]:
-  shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)"
-  unfolding permute_fun_def permute_bool_def
-  by (auto, drule_tac x="p \<bullet> x" in spec, simp)
-
 lemma all_eqvt2:
   shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))"
   by (perm_simp add: permute_minus_cancel) (rule refl)
@@ -137,16 +130,6 @@
 
 section {* Set Operations *}
 
-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
-
-lemma mem_eqvt[eqvt]:
-  shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
-  unfolding mem_def
-  by (perm_simp) (rule refl)
-
 lemma not_mem_eqvt:
   shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)"
   by (perm_simp) (rule refl)
@@ -210,10 +193,6 @@
   unfolding Compl_eq_Diff_UNIV
   by (perm_simp) (rule refl)
 
-lemma insert_eqvt[eqvt]:
-  shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"
-  unfolding permute_set_eq_image image_insert ..
-
 lemma image_eqvt:
   shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
   unfolding permute_set_eq_image
@@ -303,16 +282,6 @@
   unfolding split_def
   by (perm_simp) (rule refl)
 
-section {* Units *}
-
-lemma supp_unit:
-  shows "supp () = {}"
-  by (simp add: supp_def)
-
-lemma fresh_unit:
-  shows "a \<sharp> ()"
-  by (simp add: fresh_def supp_unit)
-
 
 section {* Test cases *}