# HG changeset patch
# User haftmann
# Date 1314513805 -7200
# Node ID 01b2732cf4ad1072be0ae3e86c2f991870ac9802
# Parent  0d32868a9732da15131f3135c1d3cbd736d9ded1
tuned

diff -r 0d32868a9732 -r 01b2732cf4ad src/HOL/Library/Cset.thy
--- a/src/HOL/Library/Cset.thy	Sun Aug 28 08:13:58 2011 +0200
+++ b/src/HOL/Library/Cset.thy	Sun Aug 28 08:43:25 2011 +0200
@@ -295,59 +295,55 @@
   "- Cset.coset xs = Cset.set xs"
   by (simp add: Cset.set_def Cset.coset_def)
 
-lemma member_cset_of:
-  "member = set_of"
-  by (rule ext)+ (simp add: member_def mem_def)
-
 lemma inter_project:
   "inf A (Cset.set xs) = Cset.set (List.filter (Cset.member A) xs)"
   "inf A (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 member_def)
-  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 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 mem_def)
-  then have "fold More_Set.remove xs (member A) = 
-    member (fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs A)"
+  have *: "\<And>x::'a. Cset.remove = (\<lambda>x. Set \<circ> More_Set.remove x \<circ> set_of)"
+    by (simp add: fun_eq_iff More_Set.remove_def)
+  have "set_of \<circ> fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> set_of) xs =
+    fold More_Set.remove xs \<circ> set_of"
+    by (rule fold_commute) (simp add: fun_eq_iff)
+  then have "fold More_Set.remove xs (set_of A) = 
+    set_of (fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> set_of) xs A)"
     by (simp add: fun_eq_iff)
   then have "inf A (Cset.coset xs) = fold Cset.remove xs A"
-    by (simp add: Diff_eq [symmetric] minus_set * member_cset_of)
+    by (simp add: Diff_eq [symmetric] minus_set *)
   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 * member_cset_of)
+    by (auto simp add: More_Set.remove_def *)
   ultimately show "inf A (Cset.coset xs) = foldr Cset.remove xs A"
     by (simp add: foldr_fold)
 qed
 
+lemma union_insert:
+  "sup (Cset.set xs) A = foldr Cset.insert xs A"
+  "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)"
+proof -
+  have *: "\<And>x::'a. Cset.insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> set_of)"
+    by (simp add: fun_eq_iff)
+  have "set_of \<circ> fold (\<lambda>x. Set \<circ> Set.insert x \<circ> set_of) xs =
+    fold Set.insert xs \<circ> set_of"
+    by (rule fold_commute) (simp add: fun_eq_iff)
+  then have "fold Set.insert xs (set_of A) =
+    set_of (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> set_of) 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 *)
+  moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y"
+    by (auto simp add: *)
+  ultimately show "sup (Cset.set xs) A = foldr Cset.insert xs A"
+    by (simp add: foldr_fold)
+  show "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)"
+    by (auto simp add: Cset.coset_def Cset.member_def)
+qed
+
 lemma subtract_remove:
   "A - Cset.set xs = foldr Cset.remove xs A"
   "A - Cset.coset xs = Cset.set (List.filter (member A) xs)"
   by (simp_all only: diff_eq compl_set compl_coset inter_project)
 
-lemma union_insert:
-  "sup (Cset.set xs) A = foldr Cset.insert xs A"
-  "sup (Cset.coset xs) A = 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 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 mem_def)
-  then have "fold Set.insert xs (member A) =
-    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 * 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: * member_cset_of)
-  ultimately show "sup (Cset.set xs) A = foldr Cset.insert xs A"
-    by (simp add: foldr_fold)
-  show "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)"
-    by (auto simp add: Cset.coset_def member_cset_of mem_def)
-qed
-
 context complete_lattice
 begin
 
diff -r 0d32868a9732 -r 01b2732cf4ad src/HOL/Library/Dlist_Cset.thy
--- a/src/HOL/Library/Dlist_Cset.thy	Sun Aug 28 08:13:58 2011 +0200
+++ b/src/HOL/Library/Dlist_Cset.thy	Sun Aug 28 08:43:25 2011 +0200
@@ -118,7 +118,7 @@
 
 end
 
-declare Cset.single_code[code]
+declare Cset.single_code [code]
 
 lemma bind_set [code]:
   "Cset.bind (Dlist_Cset.Set xs) f = fold (sup \<circ> f) (list_of_dlist xs) Cset.empty"
@@ -130,6 +130,4 @@
   by (simp add: Cset.pred_of_cset_set Dlist_Cset.Set_def)
 hide_fact (open) pred_of_cset_set
 
-export_code "Cset._" in Haskell
-
 end