# HG changeset patch
# User haftmann
# Date 1314428545 -7200
# Node ID 9ab8c88449a4c7b932f645b07d1db9969d536e15
# Parent  ddfd934e19bbab5f892e054fe303aaca5cec0301# Parent  c0fd385a41f40af2d6911440bc82f7020c693332
adapted to changes in Cset.thy

diff -r ddfd934e19bb -r 9ab8c88449a4 doc-src/Classes/Thy/document/Classes.tex
--- a/doc-src/Classes/Thy/document/Classes.tex	Fri Aug 26 15:11:33 2011 -0700
+++ b/doc-src/Classes/Thy/document/Classes.tex	Sat Aug 27 09:02:25 2011 +0200
@@ -1167,13 +1167,13 @@
 mult{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Integer\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Integer{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 mult{\isaliteral{5F}{\isacharunderscore}}int\ i\ j\ {\isaliteral{3D}{\isacharequal}}\ i\ {\isaliteral{2B}{\isacharplus}}\ j{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 \isanewline
+neutral{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+neutral{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\isanewline
 instance\ Semigroup\ Integer\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
 \ \ mult\ {\isaliteral{3D}{\isacharequal}}\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 \isanewline
-neutral{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Integer{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-neutral{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
 instance\ Monoidl\ Integer\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
 \ \ neutral\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
@@ -1231,8 +1231,8 @@
 \ \ val\ pow{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoid\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\isanewline
 \ \ val\ pow{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ group\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\isanewline
 \ \ val\ mult{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}int\isanewline
+\ \ val\ neutral{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\isanewline
 \ \ val\ semigroup{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ semigroup\isanewline
-\ \ val\ neutral{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\isanewline
 \ \ val\ monoidl{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ monoidl\isanewline
 \ \ val\ monoid{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ monoid\isanewline
 \ \ val\ inverse{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ IntInf{\isaliteral{2E}{\isachardot}}int\isanewline
@@ -1273,9 +1273,9 @@
 \isanewline
 fun\ mult{\isaliteral{5F}{\isacharunderscore}}int\ i\ j\ {\isaliteral{3D}{\isacharequal}}\ IntInf{\isaliteral{2E}{\isachardot}}{\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{2C}{\isacharcomma}}\ j{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 \isanewline
-val\ semigroup{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}mult\ {\isaliteral{3D}{\isacharequal}}\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ semigroup{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+val\ neutral{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 \isanewline
-val\ neutral{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+val\ semigroup{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}mult\ {\isaliteral{3D}{\isacharequal}}\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3A}{\isacharcolon}}\ IntInf{\isaliteral{2E}{\isachardot}}int\ semigroup{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 \isanewline
 val\ monoidl{\isaliteral{5F}{\isacharunderscore}}int\ {\isaliteral{3D}{\isacharequal}}\isanewline
 \ \ {\isaliteral{7B}{\isacharbraceleft}}semigroup{\isaliteral{5F}{\isacharunderscore}}monoidl\ {\isaliteral{3D}{\isacharequal}}\ semigroup{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{2C}{\isacharcomma}}\ neutral\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3A}{\isacharcolon}}\isanewline
@@ -1368,12 +1368,12 @@
 \isanewline
 def\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}i{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\ j{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}{\isaliteral{3A}{\isacharcolon}}\ BigInt\ {\isaliteral{3D}{\isacharequal}}\ i\ {\isaliteral{2B}{\isacharplus}}\ j\isanewline
 \isanewline
+def\ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3A}{\isacharcolon}}\ BigInt\ {\isaliteral{3D}{\isacharequal}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\isanewline
 implicit\ def\ semigroup{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3A}{\isacharcolon}}\ semigroup{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ new\ semigroup{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
 \ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}mult{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\isanewline
 {\isaliteral{7D}{\isacharbraceright}}\isanewline
 \isanewline
-def\ neutral{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3A}{\isacharcolon}}\ BigInt\ {\isaliteral{3D}{\isacharequal}}\ BigInt{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\isanewline
 implicit\ def\ monoidl{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{3A}{\isacharcolon}}\ monoidl{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ new\ monoidl{\isaliteral{5B}{\isacharbrackleft}}BigInt{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
 \ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}neutral{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{5F}{\isacharunderscore}}int\isanewline
 \ \ val\ {\isaliteral{60}{\isacharbackquote}}Example{\isaliteral{2E}{\isachardot}}mult{\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{3A}{\isacharcolon}}\ BigInt{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ mult{\isaliteral{5F}{\isacharunderscore}}int{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{29}{\isacharparenright}}\isanewline
diff -r ddfd934e19bb -r 9ab8c88449a4 doc-src/Codegen/Thy/document/Introduction.tex
--- a/doc-src/Codegen/Thy/document/Introduction.tex	Fri Aug 26 15:11:33 2011 -0700
+++ b/doc-src/Codegen/Thy/document/Introduction.tex	Sat Aug 27 09:02:25 2011 +0200
@@ -413,13 +413,13 @@
 mult{\isaliteral{5F}{\isacharunderscore}}nat\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ n\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 mult{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ n\ {\isaliteral{3D}{\isacharequal}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ n\ {\isaliteral{28}{\isacharparenleft}}mult{\isaliteral{5F}{\isacharunderscore}}nat\ m\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 \isanewline
+neutral{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+neutral{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3D}{\isacharequal}}\ Suc\ Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\isanewline
 instance\ Semigroup\ Nat\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
 \ \ mult\ {\isaliteral{3D}{\isacharequal}}\ mult{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 \isanewline
-neutral{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-neutral{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3D}{\isacharequal}}\ Suc\ Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
-\isanewline
 instance\ Monoid\ Nat\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline
 \ \ neutral\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 {\isaliteral{7D}{\isacharbraceright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
@@ -462,8 +462,8 @@
 \ \ val\ neutral\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoid\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\isanewline
 \ \ val\ pow\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ monoid\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\isanewline
 \ \ val\ mult{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\isanewline
+\ \ val\ neutral{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}\ nat\isanewline
 \ \ val\ semigroup{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}\ nat\ semigroup\isanewline
-\ \ val\ neutral{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}\ nat\isanewline
 \ \ val\ monoid{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}\ nat\ monoid\isanewline
 \ \ val\ bexp\ {\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ nat\isanewline
 end\ {\isaliteral{3D}{\isacharequal}}\ struct\isanewline
@@ -486,9 +486,9 @@
 fun\ mult{\isaliteral{5F}{\isacharunderscore}}nat\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ n\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\isanewline
 \ \ {\isaliteral{7C}{\isacharbar}}\ mult{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ n\ {\isaliteral{3D}{\isacharequal}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ n\ {\isaliteral{28}{\isacharparenleft}}mult{\isaliteral{5F}{\isacharunderscore}}nat\ m\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 \isanewline
-val\ semigroup{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}mult\ {\isaliteral{3D}{\isacharequal}}\ mult{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3A}{\isacharcolon}}\ nat\ semigroup{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+val\ neutral{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{3D}{\isacharequal}}\ Suc\ Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 \isanewline
-val\ neutral{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}\ nat\ {\isaliteral{3D}{\isacharequal}}\ Suc\ Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+val\ semigroup{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}mult\ {\isaliteral{3D}{\isacharequal}}\ mult{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{3A}{\isacharcolon}}\ nat\ semigroup{\isaliteral{3B}{\isacharsemicolon}}\isanewline
 \isanewline
 val\ monoid{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}semigroup{\isaliteral{5F}{\isacharunderscore}}monoid\ {\isaliteral{3D}{\isacharequal}}\ semigroup{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{2C}{\isacharcomma}}\ neutral\ {\isaliteral{3D}{\isacharequal}}\ neutral{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{7D}{\isacharbraceright}}\isanewline
 \ \ {\isaliteral{3A}{\isacharcolon}}\ nat\ monoid{\isaliteral{3B}{\isacharsemicolon}}\isanewline
diff -r ddfd934e19bb -r 9ab8c88449a4 src/HOL/Library/Cset.thy
--- a/src/HOL/Library/Cset.thy	Fri Aug 26 15:11:33 2011 -0700
+++ b/src/HOL/Library/Cset.thy	Sat Aug 27 09:02:25 2011 +0200
@@ -10,16 +10,27 @@
 subsection {* Lifting *}
 
 typedef (open) 'a set = "UNIV :: 'a set set"
-  morphisms member Set by rule+
+  morphisms set_of Set by rule+
 hide_type (open) set
 
+lemma set_of_Set [simp]:
+  "set_of (Set A) = A"
+  by (rule Set_inverse) rule
+
+lemma Set_set_of [simp]:
+  "Set (set_of A) = A"
+  by (fact set_of_inverse)
+
+definition member :: "'a Cset.set \<Rightarrow> 'a \<Rightarrow> bool" where
+  "member A x \<longleftrightarrow> x \<in> set_of A"
+
+lemma member_set_of:
+  "set_of = member"
+  by (rule ext)+ (simp add: member_def mem_def)
+
 lemma member_Set [simp]:
-  "member (Set A) = A"
-  by (rule Set_inverse) rule
-
-lemma Set_member [simp]:
-  "Set (member A) = A"
-  by (fact member_inverse)
+  "member (Set A) x \<longleftrightarrow> x \<in> A"
+  by (simp add: member_def)
 
 lemma Set_inject [simp]:
   "Set A = Set B \<longleftrightarrow> A = B"
@@ -27,7 +38,7 @@
 
 lemma set_eq_iff:
   "A = B \<longleftrightarrow> member A = member B"
-  by (simp add: member_inject)
+  by (auto simp add: fun_eq_iff set_of_inject [symmetric] member_def mem_def)
 hide_fact (open) set_eq_iff
 
 lemma set_eqI:
@@ -41,16 +52,16 @@
 begin
 
 definition less_eq_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
-  [simp]: "A \<le> B \<longleftrightarrow> member A \<subseteq> member B"
+  [simp]: "A \<le> B \<longleftrightarrow> set_of A \<subseteq> set_of B"
 
 definition less_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
-  [simp]: "A < B \<longleftrightarrow> member A \<subset> member B"
+  [simp]: "A < B \<longleftrightarrow> set_of A \<subset> set_of B"
 
 definition inf_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
-  [simp]: "inf A B = Set (member A \<inter> member B)"
+  [simp]: "inf A B = Set (set_of A \<inter> set_of B)"
 
 definition sup_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
-  [simp]: "sup A B = Set (member A \<union> member B)"
+  [simp]: "sup A B = Set (set_of A \<union> set_of B)"
 
 definition bot_set :: "'a Cset.set" where
   [simp]: "bot = Set {}"
@@ -59,13 +70,13 @@
   [simp]: "top = Set UNIV"
 
 definition uminus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set" where
-  [simp]: "- A = Set (- (member A))"
+  [simp]: "- A = Set (- (set_of A))"
 
 definition minus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
-  [simp]: "A - B = Set (member A - member B)"
+  [simp]: "A - B = Set (set_of A - set_of B)"
 
 instance proof
-qed (auto intro: Cset.set_eqI)
+qed (auto intro!: Cset.set_eqI simp add: member_def mem_def)
 
 end
 
@@ -73,16 +84,19 @@
 begin
 
 definition Inf_set :: "'a Cset.set set \<Rightarrow> 'a Cset.set" where
-  [simp]: "Inf_set As = Set (Inf (image member As))"
+  [simp]: "Inf_set As = Set (Inf (image set_of As))"
 
 definition Sup_set :: "'a Cset.set set \<Rightarrow> 'a Cset.set" where
-  [simp]: "Sup_set As = Set (Sup (image member As))"
+  [simp]: "Sup_set As = Set (Sup (image set_of As))"
 
 instance proof
-qed (auto simp add: le_fun_def le_bool_def)
+qed (auto simp add: le_fun_def)
 
 end
 
+instance Cset.set :: (type) complete_boolean_algebra proof
+qed (unfold INF_def SUP_def, auto)
+
 
 subsection {* Basic operations *}
 
@@ -93,40 +107,40 @@
 hide_const (open) UNIV
 
 definition is_empty :: "'a Cset.set \<Rightarrow> bool" where
-  [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)"
+  [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (set_of A)"
 
 definition insert :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
-  [simp]: "insert x A = Set (Set.insert x (member A))"
+  [simp]: "insert x A = Set (Set.insert x (set_of A))"
 
 definition remove :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
-  [simp]: "remove x A = Set (More_Set.remove x (member A))"
+  [simp]: "remove x A = Set (More_Set.remove x (set_of A))"
 
 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a Cset.set \<Rightarrow> 'b Cset.set" where
-  [simp]: "map f A = Set (image f (member A))"
+  [simp]: "map f A = Set (image f (set_of A))"
 
 enriched_type map: map
   by (simp_all add: fun_eq_iff image_compose)
 
 definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
-  [simp]: "filter P A = Set (More_Set.project P (member A))"
+  [simp]: "filter P A = Set (More_Set.project P (set_of A))"
 
 definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
-  [simp]: "forall P A \<longleftrightarrow> Ball (member A) P"
+  [simp]: "forall P A \<longleftrightarrow> Ball (set_of A) P"
 
 definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
-  [simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
+  [simp]: "exists P A \<longleftrightarrow> Bex (set_of A) P"
 
 definition card :: "'a Cset.set \<Rightarrow> nat" where
-  [simp]: "card A = Finite_Set.card (member A)"
+  [simp]: "card A = Finite_Set.card (set_of A)"
   
 context complete_lattice
 begin
 
 definition Infimum :: "'a Cset.set \<Rightarrow> 'a" where
-  [simp]: "Infimum A = Inf (member A)"
+  [simp]: "Infimum A = Inf (set_of A)"
 
 definition Supremum :: "'a Cset.set \<Rightarrow> 'a" where
-  [simp]: "Supremum A = Sup (member A)"
+  [simp]: "Supremum A = Sup (set_of A)"
 
 end
 
@@ -140,134 +154,138 @@
 
 text {* conversion from @{typ "'a Predicate.pred"} *}
 
-definition pred_of_cset :: "'a Cset.set \<Rightarrow> 'a Predicate.pred"
-where [code del]: "pred_of_cset = Predicate.Pred \<circ> Cset.member"
+definition pred_of_cset :: "'a Cset.set \<Rightarrow> 'a Predicate.pred" where
+  [code del]: "pred_of_cset = Predicate.Pred \<circ> Cset.member"
 
-definition of_pred :: "'a Predicate.pred \<Rightarrow> 'a Cset.set"
-where "of_pred = Cset.Set \<circ> Predicate.eval"
+definition of_pred :: "'a Predicate.pred \<Rightarrow> 'a Cset.set" where
+  "of_pred = Cset.Set \<circ> Collect \<circ> Predicate.eval"
 
-definition of_seq :: "'a Predicate.seq \<Rightarrow> 'a Cset.set"
-where "of_seq = of_pred \<circ> Predicate.pred_of_seq"
+definition of_seq :: "'a Predicate.seq \<Rightarrow> 'a Cset.set" where 
+  "of_seq = of_pred \<circ> Predicate.pred_of_seq"
 
 text {* monad operations *}
 
 definition single :: "'a \<Rightarrow> 'a Cset.set" where
   "single a = Set {a}"
 
-definition bind :: "'a Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Cset.set) \<Rightarrow> 'b Cset.set"
-                (infixl "\<guillemotright>=" 70)
-  where "A \<guillemotright>= f = Set (\<Union>x \<in> member A. member (f x))"
+definition bind :: "'a Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Cset.set) \<Rightarrow> 'b Cset.set" (infixl "\<guillemotright>=" 70) where
+  "A \<guillemotright>= f = (SUP x : set_of A. f x)"
+
 
 subsection {* Simplified simprules *}
 
-lemma empty_simp [simp]: "member Cset.empty = {}"
-  by(simp)
+lemma empty_simp [simp]: "member Cset.empty = bot"
+  by (simp add: fun_eq_iff bot_apply)
 
-lemma UNIV_simp [simp]: "member Cset.UNIV = UNIV"
-  by simp
+lemma UNIV_simp [simp]: "member Cset.UNIV = top"
+  by (simp add: fun_eq_iff top_apply)
 
 lemma is_empty_simp [simp]:
-  "is_empty A \<longleftrightarrow> member A = {}"
+  "is_empty A \<longleftrightarrow> set_of A = {}"
   by (simp add: More_Set.is_empty_def)
 declare is_empty_def [simp del]
 
 lemma remove_simp [simp]:
-  "remove x A = Set (member A - {x})"
+  "remove x A = Set (set_of A - {x})"
   by (simp add: More_Set.remove_def)
 declare remove_def [simp del]
 
 lemma filter_simp [simp]:
-  "filter P A = Set {x \<in> member A. P x}"
+  "filter P A = Set {x \<in> set_of A. P x}"
   by (simp add: More_Set.project_def)
 declare filter_def [simp del]
 
-lemma member_set [simp]:
-  "member (Cset.set xs) = set xs"
+lemma set_of_set [simp]:
+  "set_of (Cset.set xs) = set xs"
   by (simp add: set_def)
-hide_fact (open) member_set set_def
+hide_fact (open) set_def
 
 lemma set_simps [simp]:
   "Cset.set [] = Cset.empty"
   "Cset.set (x # xs) = insert x (Cset.set xs)"
 by(simp_all add: Cset.set_def)
 
-lemma member_SUPR [simp]:
+lemma member_SUP [simp]:
   "member (SUPR A f) = SUPR A (member \<circ> f)"
-unfolding SUPR_def by simp
+  by (auto simp add: fun_eq_iff SUP_apply member_def, unfold SUP_def, auto)
 
 lemma member_bind [simp]:
-  "member (P \<guillemotright>= f) = member (SUPR (member P) f)"
-by (simp add: bind_def Cset.set_eq_iff)
+  "member (P \<guillemotright>= f) = SUPR (set_of P) (member \<circ> f)"
+  by (simp add: bind_def Cset.set_eq_iff)
 
 lemma member_single [simp]:
-  "member (single a) = {a}"
-by(simp add: single_def)
+  "member (single a) = (\<lambda>x. x \<in> {a})"
+  by (simp add: single_def fun_eq_iff)
 
 lemma single_sup_simps [simp]:
   shows single_sup: "sup (single a) A = insert a A"
   and sup_single: "sup A (single a) = insert a A"
-by(auto simp add: Cset.set_eq_iff)
+  by (auto simp add: Cset.set_eq_iff single_def)
 
 lemma single_bind [simp]:
   "single a \<guillemotright>= B = B a"
-by(simp add: bind_def single_def)
+  by (simp add: Cset.set_eq_iff SUP_insert single_def)
 
 lemma bind_bind:
   "(A \<guillemotright>= B) \<guillemotright>= C = A \<guillemotright>= (\<lambda>x. B x \<guillemotright>= C)"
-by(simp add: bind_def)
-
+  by (simp add: bind_def, simp only: SUP_def image_image, simp)
+ 
 lemma bind_single [simp]:
   "A \<guillemotright>= single = A"
-by(simp add: bind_def single_def)
+  by (simp add: Cset.set_eq_iff SUP_apply fun_eq_iff single_def member_def)
 
 lemma bind_const: "A \<guillemotright>= (\<lambda>_. B) = (if Cset.is_empty A then Cset.empty else B)"
-by(auto simp add: Cset.set_eq_iff)
+  by (auto simp add: Cset.set_eq_iff fun_eq_iff)
 
 lemma empty_bind [simp]:
   "Cset.empty \<guillemotright>= f = Cset.empty"
-by(simp add: Cset.set_eq_iff)
+  by (simp add: Cset.set_eq_iff fun_eq_iff bot_apply)
 
 lemma member_of_pred [simp]:
-  "member (of_pred P) = {x. Predicate.eval P x}"
-by(simp add: of_pred_def Collect_def)
+  "member (of_pred P) = (\<lambda>x. x \<in> {x. Predicate.eval P x})"
+  by (simp add: of_pred_def fun_eq_iff)
 
 lemma member_of_seq [simp]:
-  "member (of_seq xq) = {x. Predicate.member xq x}"
-by(simp add: of_seq_def eval_member)
+  "member (of_seq xq) = (\<lambda>x. x \<in> {x. Predicate.member xq x})"
+  by (simp add: of_seq_def eval_member)
 
 lemma eval_pred_of_cset [simp]: 
   "Predicate.eval (pred_of_cset A) = Cset.member A"
-by(simp add: pred_of_cset_def)
+  by (simp add: pred_of_cset_def)
 
 subsection {* Default implementations *}
 
 lemma set_code [code]:
-  "Cset.set = foldl (\<lambda>A x. insert x A) Cset.empty"
-proof(rule ext, rule Cset.set_eqI)
-  fix xs
-  show "member (Cset.set xs) = member (foldl (\<lambda>A x. insert x A) Cset.empty xs)"
-    by(induct xs rule: rev_induct)(simp_all)
+  "Cset.set = (\<lambda>xs. fold insert xs Cset.empty)"
+proof (rule ext, rule Cset.set_eqI)
+  fix xs :: "'a list"
+  show "member (Cset.set xs) = member (fold insert xs Cset.empty)"
+    by (simp add: fold_commute_apply [symmetric, where ?h = Set and ?g = Set.insert]
+      fun_eq_iff Cset.set_def union_set [symmetric])
 qed
 
 lemma single_code [code]:
   "single a = insert a Cset.empty"
-by(simp add: Cset.single_def)
+  by (simp add: Cset.single_def)
 
 lemma of_pred_code [code]:
   "of_pred (Predicate.Seq f) = (case f () of
      Predicate.Empty \<Rightarrow> Cset.empty
    | Predicate.Insert x P \<Rightarrow> Cset.insert x (of_pred P)
    | Predicate.Join P xq \<Rightarrow> sup (of_pred P) (of_seq xq))"
-by(auto split: seq.split 
-        simp add: Predicate.Seq_def of_pred_def eval_member Cset.set_eq_iff)
+  apply (auto split: seq.split simp add: Predicate.Seq_def of_pred_def Cset.set_eq_iff sup_apply eval_member [symmetric] member_def [symmetric] Collect_def mem_def member_set_of)
+  apply (unfold Set.insert_def Collect_def sup_apply member_set_of)
+  apply simp_all
+  done
 
 lemma of_seq_code [code]:
   "of_seq Predicate.Empty = Cset.empty"
   "of_seq (Predicate.Insert x P) = Cset.insert x (of_pred P)"
   "of_seq (Predicate.Join P xq) = sup (of_pred P) (of_seq xq)"
-by(auto simp add: of_seq_def of_pred_def Cset.set_eq_iff)
-
-declare mem_def [simp del]
+  apply (auto simp add: of_seq_def of_pred_def Cset.set_eq_iff mem_def Collect_def)
+  apply (unfold Set.insert_def Collect_def sup_apply member_set_of)
+  apply simp_all
+  done
 
 no_notation bind (infixl "\<guillemotright>=" 70)
 
@@ -275,7 +293,7 @@
   Inter Union bind single of_pred of_seq
 
 hide_fact (open) set_def pred_of_cset_def of_pred_def of_seq_def single_def 
-  bind_def empty_simp UNIV_simp member_set set_simps member_SUPR member_bind 
+  bind_def empty_simp UNIV_simp set_simps member_bind 
   member_single single_sup_simps single_sup sup_single single_bind
   bind_bind bind_single bind_const empty_bind member_of_pred member_of_seq
   eval_pred_of_cset set_code single_code of_pred_code of_seq_code
diff -r ddfd934e19bb -r 9ab8c88449a4 src/HOL/Library/List_Cset.thy
--- a/src/HOL/Library/List_Cset.thy	Fri Aug 26 15:11:33 2011 -0700
+++ b/src/HOL/Library/List_Cset.thy	Sat Aug 27 09:02:25 2011 +0200
@@ -14,9 +14,13 @@
   "coset xs = Set (- set xs)"
 hide_const (open) coset
 
+lemma set_of_coset [simp]:
+  "set_of (List_Cset.coset xs) = - set xs"
+  by (simp add: coset_def)
+
 lemma member_coset [simp]:
-  "member (List_Cset.coset xs) = - set xs"
-  by (simp add: coset_def)
+  "member (List_Cset.coset xs) = (\<lambda>x. x \<in> - set xs)"
+  by (simp add: coset_def fun_eq_iff)
 hide_fact (open) member_coset
 
 code_datatype Cset.set List_Cset.coset
@@ -24,18 +28,7 @@
 lemma member_code [code]:
   "member (Cset.set xs) = List.member xs"
   "member (List_Cset.coset xs) = Not \<circ> List.member xs"
-  by (simp_all add: fun_eq_iff member_def fun_Compl_def bool_Compl_def)
-
-lemma member_image_UNIV [simp]:
-  "member ` UNIV = UNIV"
-proof -
-  have "\<And>A \<Colon> 'a set. \<exists>B \<Colon> 'a Cset.set. A = member B"
-  proof
-    fix A :: "'a set"
-    show "A = member (Set A)" by simp
-  qed
-  then show ?thesis by (simp add: image_def)
-qed
+  by (simp_all add: fun_eq_iff member_def fun_Compl_def member_set)
 
 definition (in term_syntax)
   setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
@@ -124,12 +117,12 @@
 lemma Infimum_inf [code]:
   "Infimum (Cset.set As) = foldr inf As top"
   "Infimum (List_Cset.coset []) = bot"
-  by (simp_all add: Inf_set_foldr Inf_UNIV)
+  by (simp_all add: Inf_set_foldr)
 
 lemma Supremum_sup [code]:
   "Supremum (Cset.set As) = foldr sup As bot"
   "Supremum (List_Cset.coset []) = top"
-  by (simp_all add: Sup_set_foldr Sup_UNIV)
+  by (simp_all add: Sup_set_foldr)
 
 end
 
@@ -140,29 +133,26 @@
 hide_fact (open) single_set
 
 lemma bind_set [code]:
-  "Cset.bind (Cset.set xs) f = foldl (\<lambda>A x. sup A (f x)) (Cset.set []) xs"
-proof(rule sym)
-  show "foldl (\<lambda>A x. sup A (f x)) (Cset.set []) xs = Cset.bind (Cset.set xs) f"
-    by(induct xs rule: rev_induct)(auto simp add: Cset.bind_def Cset.set_def)
-qed
-hide_fact (open) bind_set
+  "Cset.bind (Cset.set xs) f = fold (sup \<circ> f) xs (Cset.set [])"
+  by (simp add: Cset.bind_def SUPR_set_fold)
 
 lemma pred_of_cset_set [code]:
   "pred_of_cset (Cset.set xs) = foldr sup (map Predicate.single xs) bot"
 proof -
   have "pred_of_cset (Cset.set xs) = Predicate.Pred (\<lambda>x. x \<in> set xs)"
-    by(auto simp add: Cset.pred_of_cset_def mem_def)
+    by (simp add: Cset.pred_of_cset_def member_code member_set)
   moreover have "foldr sup (map Predicate.single xs) bot = \<dots>"
-    by(induct xs)(auto simp add: bot_pred_def simp del: mem_def intro: pred_eqI, simp)
-  ultimately show ?thesis by(simp)
+    by (induct xs) (auto simp add: bot_pred_def simp del: mem_def intro: pred_eqI, simp)
+  ultimately show ?thesis by simp
 qed
 hide_fact (open) pred_of_cset_set
 
+
 subsection {* Derived operations *}
 
 lemma subset_eq_forall [code]:
   "A \<le> B \<longleftrightarrow> Cset.forall (member B) A"
-  by (simp add: subset_eq)
+  by (simp add: subset_eq member_def)
 
 lemma subset_subset_eq [code]:
   "A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a Cset.set)"
@@ -175,7 +165,7 @@
   "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a Cset.set)"
 
 instance proof
-qed (simp add: equal_set_def set_eq [symmetric] Cset.set_eq_iff)
+qed (simp add: equal_set_def set_eq [symmetric] Cset.set_eq_iff fun_eq_iff member_def)
 
 end
 
@@ -186,14 +176,18 @@
 
 subsection {* Functorial operations *}
 
+lemma member_cset_of:
+  "member = set_of"
+  by (rule ext)+ (simp add: member_def)
+
 lemma inter_project [code]:
   "inf A (Cset.set xs) = Cset.set (List.filter (Cset.member A) xs)"
   "inf A (List_Cset.coset xs) = foldr Cset.remove xs A"
 proof -
   show "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)"
-    by (simp add: inter project_def Cset.set_def)
+    by (simp add: inter project_def Cset.set_def member_cset_of)
   have *: "\<And>x::'a. Cset.remove = (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member)"
-    by (simp add: fun_eq_iff More_Set.remove_def)
+    by (simp add: fun_eq_iff More_Set.remove_def member_cset_of)
   have "member \<circ> fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs =
     fold More_Set.remove xs \<circ> member"
     by (rule fold_commute) (simp add: fun_eq_iff)
@@ -201,9 +195,9 @@
     member (fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs A)"
     by (simp add: fun_eq_iff)
   then have "inf A (List_Cset.coset xs) = fold Cset.remove xs A"
-    by (simp add: Diff_eq [symmetric] minus_set *)
+    by (simp add: Diff_eq [symmetric] minus_set * member_cset_of)
   moreover have "\<And>x y :: 'a. Cset.remove y \<circ> Cset.remove x = Cset.remove x \<circ> Cset.remove y"
-    by (auto simp add: More_Set.remove_def * intro: ext)
+    by (auto simp add: More_Set.remove_def * member_cset_of intro: ext)
   ultimately show "inf A (List_Cset.coset xs) = foldr Cset.remove xs A"
     by (simp add: foldr_fold)
 qed
@@ -218,7 +212,7 @@
   "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \<circ> member A) xs)"
 proof -
   have *: "\<And>x::'a. Cset.insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> member)"
-    by (simp add: fun_eq_iff)
+    by (simp add: fun_eq_iff member_cset_of)
   have "member \<circ> fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs =
     fold Set.insert xs \<circ> member"
     by (rule fold_commute) (simp add: fun_eq_iff)
@@ -226,15 +220,15 @@
     member (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs A)"
     by (simp add: fun_eq_iff)
   then have "sup (Cset.set xs) A = fold Cset.insert xs A"
-    by (simp add: union_set *)
+    by (simp add: union_set * member_cset_of)
   moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y"
-    by (auto simp add: * intro: ext)
+    by (auto simp add: * member_cset_of intro: ext)
   ultimately show "sup (Cset.set xs) A = foldr Cset.insert xs A"
     by (simp add: foldr_fold)
   show "sup (List_Cset.coset xs) A = List_Cset.coset (List.filter (Not \<circ> member A) xs)"
-    by (auto simp add: coset_def)
+    by (auto simp add: coset_def member_cset_of)
 qed
 
 declare mem_def[simp del]
 
-end
\ No newline at end of file
+end
diff -r ddfd934e19bb -r 9ab8c88449a4 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Fri Aug 26 15:11:33 2011 -0700
+++ b/src/HOL/Quotient.thy	Sat Aug 27 09:02:25 2011 +0200
@@ -35,12 +35,11 @@
 definition
   Respects :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set"
 where
-  "Respects R x = R x x"
+  "Respects R = {x. R x x}"
 
 lemma in_respects:
   shows "x \<in> Respects R \<longleftrightarrow> R x x"
-  unfolding mem_def Respects_def
-  by simp
+  unfolding Respects_def by simp
 
 subsection {* Function map and function relation *}
 
@@ -268,14 +267,14 @@
   by (auto simp add: in_respects)
 
 lemma ball_reg_right:
-  assumes a: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x"
+  assumes a: "\<And>x. x \<in> R \<Longrightarrow> P x \<longrightarrow> Q x"
   shows "All P \<longrightarrow> Ball R Q"
-  using a by (metis Collect_def Collect_mem_eq)
+  using a by (metis Collect_mem_eq)
 
 lemma bex_reg_left:
-  assumes a: "\<And>x. R x \<Longrightarrow> Q x \<longrightarrow> P x"
+  assumes a: "\<And>x. x \<in> R \<Longrightarrow> Q x \<longrightarrow> P x"
   shows "Bex R Q \<longrightarrow> Ex P"
-  using a by (metis Collect_def Collect_mem_eq)
+  using a by (metis Collect_mem_eq)
 
 lemma ball_reg_left:
   assumes a: "equivp R"
@@ -327,16 +326,16 @@
   using a b by metis
 
 lemma ball_reg:
-  assumes a: "!x :: 'a. (R x --> P x --> Q x)"
+  assumes a: "!x :: 'a. (x \<in> R --> P x --> Q x)"
   and     b: "Ball R P"
   shows "Ball R Q"
-  using a b by (metis Collect_def Collect_mem_eq)
+  using a b by (metis Collect_mem_eq)
 
 lemma bex_reg:
-  assumes a: "!x :: 'a. (R x --> P x --> Q x)"
+  assumes a: "!x :: 'a. (x \<in> R --> P x --> Q x)"
   and     b: "Bex R P"
   shows "Bex R Q"
-  using a b by (metis Collect_def Collect_mem_eq)
+  using a b by (metis Collect_mem_eq)
 
 
 lemma ball_all_comm:
@@ -599,16 +598,6 @@
   shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let"
   by (auto intro!: fun_relI elim: fun_relE)
 
-lemma mem_rsp:
-  shows "(R1 ===> (R1 ===> R2) ===> R2) op \<in> op \<in>"
-  by (auto intro!: fun_relI elim: fun_relE simp add: mem_def)
-
-lemma mem_prs:
-  assumes a1: "Quotient R1 Abs1 Rep1"
-  and     a2: "Quotient R2 Abs2 Rep2"
-  shows "(Rep1 ---> (Abs1 ---> Rep2) ---> Abs2) op \<in> = op \<in>"
-  by (simp add: fun_eq_iff mem_def Quotient_abs_rep[OF a1] Quotient_abs_rep[OF a2])
-
 lemma id_rsp:
   shows "(R ===> R) id id"
   by (auto intro: fun_relI)
@@ -686,8 +675,8 @@
 declare [[map set = (vimage, set_rel)]]
 
 lemmas [quot_thm] = fun_quotient
-lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp mem_rsp id_rsp
-lemmas [quot_preserve] = if_prs o_prs let_prs mem_prs id_prs
+lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp
+lemmas [quot_preserve] = if_prs o_prs let_prs id_prs
 lemmas [quot_equiv] = identity_equivp