--- a/Quot/Nominal/Nominal2_Eqvt.thy	Mon Feb 08 11:56:22 2010 +0100
+++ b/Quot/Nominal/Nominal2_Eqvt.thy	Mon Feb 08 13:12:55 2010 +0100
@@ -2,6 +2,7 @@
     Authors:    Brian Huffman, Christian Urban
 
     Equivariance, Supp and Fresh Lemmas for Operators. 
+    (Contains most, but not all such lemmas.)
 *)
 theory Nominal2_Eqvt
 imports Nominal2_Base
@@ -76,7 +77,7 @@
 
 lemma the_eqvt:
   assumes unique: "\<exists>!x. P x"
-  shows "p \<bullet> (THE x. P x) = (THE x. p \<bullet> P (- p \<bullet> x))"
+  shows "(p \<bullet> (THE x. P x)) = (THE x. p \<bullet> P (- p \<bullet> x))"
   apply(rule the1_equality [symmetric])
   apply(simp add: ex1_eqvt2[symmetric])
   apply(simp add: permute_bool_def unique)
@@ -86,9 +87,14 @@
 
 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:
   shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
-  unfolding mem_def permute_fun_def by simp
+  unfolding mem_permute_iff permute_bool_def by simp
 
 lemma not_mem_eqvt:
   shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)"
@@ -229,7 +235,7 @@
 lemmas [eqvt] = 
   (* connectives *)
   eq_eqvt if_eqvt imp_eqvt disj_eqvt conj_eqvt Not_eqvt 
-  True_eqvt False_eqvt ex_eqvt all_eqvt
+  True_eqvt False_eqvt ex_eqvt all_eqvt ex1_eqvt
   imp_eqvt [folded induct_implies_def]
 
   (* nominal *)
@@ -237,12 +243,12 @@
   permute_pure
 
   (* datatypes *)
-  permute_prod.simps
+  permute_prod.simps append_eqvt rev_eqvt set_eqvt
   fst_eqvt snd_eqvt
 
   (* sets *)
-  empty_eqvt UNIV_eqvt union_eqvt inter_eqvt
-  Diff_eqvt Compl_eqvt insert_eqvt
+  empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt
+  Diff_eqvt Compl_eqvt insert_eqvt Collect_eqvt
 
 thm eqvts
 thm eqvts_raw