replaced misleading Fset/fset name -- these do not stand for finite sets
authorhaftmann
Mon Nov 22 17:46:51 2010 +0100 (2010-11-22)
changeset 40672abd4e7358847
parent 40671 5e46057ba8e0
child 40673 3b9b39ac1f24
replaced misleading Fset/fset name -- these do not stand for finite sets
NEWS
src/HOL/IsaMakefile
src/HOL/Library/Cset.thy
src/HOL/Library/Dlist.thy
src/HOL/Library/Executable_Set.thy
src/HOL/Library/Fset.thy
src/HOL/Library/Library.thy
src/HOL/Quotient_Examples/FSet.thy
     1.1 --- a/NEWS	Mon Nov 22 09:37:39 2010 +0100
     1.2 +++ b/NEWS	Mon Nov 22 17:46:51 2010 +0100
     1.3 @@ -89,6 +89,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Renamed theory Fset to Cset, type Fset.fset to Cset.set, in order to
     1.8 +avoid confusion with finite sets.  INCOMPATIBILITY.
     1.9 +
    1.10  * Theory Multiset provides stable quicksort implementation of sort_key.
    1.11  
    1.12  * Quickcheck now has a configurable time limit which is set to 30 seconds
     2.1 --- a/src/HOL/IsaMakefile	Mon Nov 22 09:37:39 2010 +0100
     2.2 +++ b/src/HOL/IsaMakefile	Mon Nov 22 17:46:51 2010 +0100
     2.3 @@ -419,7 +419,7 @@
     2.4    Library/Efficient_Nat.thy Library/Enum.thy Library/Eval_Witness.thy	\
     2.5    Library/Executable_Set.thy Library/Float.thy				\
     2.6    Library/Formal_Power_Series.thy Library/Fraction_Field.thy		\
     2.7 -  Library/FrechetDeriv.thy Library/Fset.thy Library/FuncSet.thy		\
     2.8 +  Library/FrechetDeriv.thy Library/Cset.thy Library/FuncSet.thy		\
     2.9    Library/Function_Algebras.thy						\
    2.10    Library/Fundamental_Theorem_Algebra.thy Library/Glbs.thy		\
    2.11    Library/Indicator_Function.thy Library/Infinite_Set.thy		\
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Cset.thy	Mon Nov 22 17:46:51 2010 +0100
     3.3 @@ -0,0 +1,357 @@
     3.4 +
     3.5 +(* Author: Florian Haftmann, TU Muenchen *)
     3.6 +
     3.7 +header {* A dedicated set type which is executable on its finite part *}
     3.8 +
     3.9 +theory Cset
    3.10 +imports More_Set More_List
    3.11 +begin
    3.12 +
    3.13 +subsection {* Lifting *}
    3.14 +
    3.15 +typedef (open) 'a set = "UNIV :: 'a set set"
    3.16 +  morphisms member Set by rule+
    3.17 +hide_type (open) set
    3.18 +
    3.19 +lemma member_Set [simp]:
    3.20 +  "member (Set A) = A"
    3.21 +  by (rule Set_inverse) rule
    3.22 +
    3.23 +lemma Set_member [simp]:
    3.24 +  "Set (member A) = A"
    3.25 +  by (fact member_inverse)
    3.26 +
    3.27 +lemma Set_inject [simp]:
    3.28 +  "Set A = Set B \<longleftrightarrow> A = B"
    3.29 +  by (simp add: Set_inject)
    3.30 +
    3.31 +lemma set_eq_iff:
    3.32 +  "A = B \<longleftrightarrow> member A = member B"
    3.33 +  by (simp add: member_inject)
    3.34 +hide_fact (open) set_eq_iff
    3.35 +
    3.36 +lemma set_eqI:
    3.37 +  "member A = member B \<Longrightarrow> A = B"
    3.38 +  by (simp add: Cset.set_eq_iff)
    3.39 +hide_fact (open) set_eqI
    3.40 +
    3.41 +declare mem_def [simp]
    3.42 +
    3.43 +definition set :: "'a list \<Rightarrow> 'a Cset.set" where
    3.44 +  "set xs = Set (List.set xs)"
    3.45 +hide_const (open) set
    3.46 +
    3.47 +lemma member_set [simp]:
    3.48 +  "member (Cset.set xs) = set xs"
    3.49 +  by (simp add: set_def)
    3.50 +hide_fact (open) member_set
    3.51 +
    3.52 +definition coset :: "'a list \<Rightarrow> 'a Cset.set" where
    3.53 +  "coset xs = Set (- set xs)"
    3.54 +hide_const (open) coset
    3.55 +
    3.56 +lemma member_coset [simp]:
    3.57 +  "member (Cset.coset xs) = - set xs"
    3.58 +  by (simp add: coset_def)
    3.59 +hide_fact (open) member_coset
    3.60 +
    3.61 +code_datatype Cset.set Cset.coset
    3.62 +
    3.63 +lemma member_code [code]:
    3.64 +  "member (Cset.set xs) = List.member xs"
    3.65 +  "member (Cset.coset xs) = Not \<circ> List.member xs"
    3.66 +  by (simp_all add: fun_eq_iff member_def fun_Compl_def bool_Compl_def)
    3.67 +
    3.68 +lemma member_image_UNIV [simp]:
    3.69 +  "member ` UNIV = UNIV"
    3.70 +proof -
    3.71 +  have "\<And>A \<Colon> 'a set. \<exists>B \<Colon> 'a Cset.set. A = member B"
    3.72 +  proof
    3.73 +    fix A :: "'a set"
    3.74 +    show "A = member (Set A)" by simp
    3.75 +  qed
    3.76 +  then show ?thesis by (simp add: image_def)
    3.77 +qed
    3.78 +
    3.79 +definition (in term_syntax)
    3.80 +  setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
    3.81 +    \<Rightarrow> 'a Cset.set \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
    3.82 +  [code_unfold]: "setify xs = Code_Evaluation.valtermify Cset.set {\<cdot>} xs"
    3.83 +
    3.84 +notation fcomp (infixl "\<circ>>" 60)
    3.85 +notation scomp (infixl "\<circ>\<rightarrow>" 60)
    3.86 +
    3.87 +instantiation Cset.set :: (random) random
    3.88 +begin
    3.89 +
    3.90 +definition
    3.91 +  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (setify xs))"
    3.92 +
    3.93 +instance ..
    3.94 +
    3.95 +end
    3.96 +
    3.97 +no_notation fcomp (infixl "\<circ>>" 60)
    3.98 +no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
    3.99 +
   3.100 +
   3.101 +subsection {* Lattice instantiation *}
   3.102 +
   3.103 +instantiation Cset.set :: (type) boolean_algebra
   3.104 +begin
   3.105 +
   3.106 +definition less_eq_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
   3.107 +  [simp]: "A \<le> B \<longleftrightarrow> member A \<subseteq> member B"
   3.108 +
   3.109 +definition less_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
   3.110 +  [simp]: "A < B \<longleftrightarrow> member A \<subset> member B"
   3.111 +
   3.112 +definition inf_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
   3.113 +  [simp]: "inf A B = Set (member A \<inter> member B)"
   3.114 +
   3.115 +definition sup_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
   3.116 +  [simp]: "sup A B = Set (member A \<union> member B)"
   3.117 +
   3.118 +definition bot_set :: "'a Cset.set" where
   3.119 +  [simp]: "bot = Set {}"
   3.120 +
   3.121 +definition top_set :: "'a Cset.set" where
   3.122 +  [simp]: "top = Set UNIV"
   3.123 +
   3.124 +definition uminus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set" where
   3.125 +  [simp]: "- A = Set (- (member A))"
   3.126 +
   3.127 +definition minus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
   3.128 +  [simp]: "A - B = Set (member A - member B)"
   3.129 +
   3.130 +instance proof
   3.131 +qed (auto intro: Cset.set_eqI)
   3.132 +
   3.133 +end
   3.134 +
   3.135 +instantiation Cset.set :: (type) complete_lattice
   3.136 +begin
   3.137 +
   3.138 +definition Inf_set :: "'a Cset.set set \<Rightarrow> 'a Cset.set" where
   3.139 +  [simp]: "Inf_set As = Set (Inf (image member As))"
   3.140 +
   3.141 +definition Sup_set :: "'a Cset.set set \<Rightarrow> 'a Cset.set" where
   3.142 +  [simp]: "Sup_set As = Set (Sup (image member As))"
   3.143 +
   3.144 +instance proof
   3.145 +qed (auto simp add: le_fun_def le_bool_def)
   3.146 +
   3.147 +end
   3.148 +
   3.149 +
   3.150 +subsection {* Basic operations *}
   3.151 +
   3.152 +definition is_empty :: "'a Cset.set \<Rightarrow> bool" where
   3.153 +  [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)"
   3.154 +
   3.155 +lemma is_empty_set [code]:
   3.156 +  "is_empty (Cset.set xs) \<longleftrightarrow> List.null xs"
   3.157 +  by (simp add: is_empty_set)
   3.158 +hide_fact (open) is_empty_set
   3.159 +
   3.160 +lemma empty_set [code]:
   3.161 +  "bot = Cset.set []"
   3.162 +  by (simp add: set_def)
   3.163 +hide_fact (open) empty_set
   3.164 +
   3.165 +lemma UNIV_set [code]:
   3.166 +  "top = Cset.coset []"
   3.167 +  by (simp add: coset_def)
   3.168 +hide_fact (open) UNIV_set
   3.169 +
   3.170 +definition insert :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
   3.171 +  [simp]: "insert x A = Set (Set.insert x (member A))"
   3.172 +
   3.173 +lemma insert_set [code]:
   3.174 +  "insert x (Cset.set xs) = Cset.set (List.insert x xs)"
   3.175 +  "insert x (Cset.coset xs) = Cset.coset (removeAll x xs)"
   3.176 +  by (simp_all add: set_def coset_def)
   3.177 +
   3.178 +definition remove :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
   3.179 +  [simp]: "remove x A = Set (More_Set.remove x (member A))"
   3.180 +
   3.181 +lemma remove_set [code]:
   3.182 +  "remove x (Cset.set xs) = Cset.set (removeAll x xs)"
   3.183 +  "remove x (Cset.coset xs) = Cset.coset (List.insert x xs)"
   3.184 +  by (simp_all add: set_def coset_def remove_set_compl)
   3.185 +    (simp add: More_Set.remove_def)
   3.186 +
   3.187 +definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a Cset.set \<Rightarrow> 'b Cset.set" where
   3.188 +  [simp]: "map f A = Set (image f (member A))"
   3.189 +
   3.190 +lemma map_set [code]:
   3.191 +  "map f (Cset.set xs) = Cset.set (remdups (List.map f xs))"
   3.192 +  by (simp add: set_def)
   3.193 +
   3.194 +type_mapper map
   3.195 +  by (simp_all add: image_image)
   3.196 +
   3.197 +definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where
   3.198 +  [simp]: "filter P A = Set (More_Set.project P (member A))"
   3.199 +
   3.200 +lemma filter_set [code]:
   3.201 +  "filter P (Cset.set xs) = Cset.set (List.filter P xs)"
   3.202 +  by (simp add: set_def project_set)
   3.203 +
   3.204 +definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
   3.205 +  [simp]: "forall P A \<longleftrightarrow> Ball (member A) P"
   3.206 +
   3.207 +lemma forall_set [code]:
   3.208 +  "forall P (Cset.set xs) \<longleftrightarrow> list_all P xs"
   3.209 +  by (simp add: set_def list_all_iff)
   3.210 +
   3.211 +definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where
   3.212 +  [simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
   3.213 +
   3.214 +lemma exists_set [code]:
   3.215 +  "exists P (Cset.set xs) \<longleftrightarrow> list_ex P xs"
   3.216 +  by (simp add: set_def list_ex_iff)
   3.217 +
   3.218 +definition card :: "'a Cset.set \<Rightarrow> nat" where
   3.219 +  [simp]: "card A = Finite_Set.card (member A)"
   3.220 +
   3.221 +lemma card_set [code]:
   3.222 +  "card (Cset.set xs) = length (remdups xs)"
   3.223 +proof -
   3.224 +  have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
   3.225 +    by (rule distinct_card) simp
   3.226 +  then show ?thesis by (simp add: set_def)
   3.227 +qed
   3.228 +
   3.229 +lemma compl_set [simp, code]:
   3.230 +  "- Cset.set xs = Cset.coset xs"
   3.231 +  by (simp add: set_def coset_def)
   3.232 +
   3.233 +lemma compl_coset [simp, code]:
   3.234 +  "- Cset.coset xs = Cset.set xs"
   3.235 +  by (simp add: set_def coset_def)
   3.236 +
   3.237 +
   3.238 +subsection {* Derived operations *}
   3.239 +
   3.240 +lemma subset_eq_forall [code]:
   3.241 +  "A \<le> B \<longleftrightarrow> forall (member B) A"
   3.242 +  by (simp add: subset_eq)
   3.243 +
   3.244 +lemma subset_subset_eq [code]:
   3.245 +  "A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a Cset.set)"
   3.246 +  by (fact less_le_not_le)
   3.247 +
   3.248 +instantiation Cset.set :: (type) equal
   3.249 +begin
   3.250 +
   3.251 +definition [code]:
   3.252 +  "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a Cset.set)"
   3.253 +
   3.254 +instance proof
   3.255 +qed (simp add: equal_set_def set_eq [symmetric] Cset.set_eq_iff)
   3.256 +
   3.257 +end
   3.258 +
   3.259 +lemma [code nbe]:
   3.260 +  "HOL.equal (A :: 'a Cset.set) A \<longleftrightarrow> True"
   3.261 +  by (fact equal_refl)
   3.262 +
   3.263 +
   3.264 +subsection {* Functorial operations *}
   3.265 +
   3.266 +lemma inter_project [code]:
   3.267 +  "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)"
   3.268 +  "inf A (Cset.coset xs) = foldr remove xs A"
   3.269 +proof -
   3.270 +  show "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)"
   3.271 +    by (simp add: inter project_def set_def)
   3.272 +  have *: "\<And>x::'a. remove = (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member)"
   3.273 +    by (simp add: fun_eq_iff)
   3.274 +  have "member \<circ> fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs =
   3.275 +    fold More_Set.remove xs \<circ> member"
   3.276 +    by (rule fold_commute) (simp add: fun_eq_iff)
   3.277 +  then have "fold More_Set.remove xs (member A) = 
   3.278 +    member (fold (\<lambda>x. Set \<circ> More_Set.remove x \<circ> member) xs A)"
   3.279 +    by (simp add: fun_eq_iff)
   3.280 +  then have "inf A (Cset.coset xs) = fold remove xs A"
   3.281 +    by (simp add: Diff_eq [symmetric] minus_set *)
   3.282 +  moreover have "\<And>x y :: 'a. Cset.remove y \<circ> Cset.remove x = Cset.remove x \<circ> Cset.remove y"
   3.283 +    by (auto simp add: More_Set.remove_def * intro: ext)
   3.284 +  ultimately show "inf A (Cset.coset xs) = foldr remove xs A"
   3.285 +    by (simp add: foldr_fold)
   3.286 +qed
   3.287 +
   3.288 +lemma subtract_remove [code]:
   3.289 +  "A - Cset.set xs = foldr remove xs A"
   3.290 +  "A - Cset.coset xs = Cset.set (List.filter (member A) xs)"
   3.291 +  by (simp_all only: diff_eq compl_set compl_coset inter_project)
   3.292 +
   3.293 +lemma union_insert [code]:
   3.294 +  "sup (Cset.set xs) A = foldr insert xs A"
   3.295 +  "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)"
   3.296 +proof -
   3.297 +  have *: "\<And>x::'a. insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> member)"
   3.298 +    by (simp add: fun_eq_iff)
   3.299 +  have "member \<circ> fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs =
   3.300 +    fold Set.insert xs \<circ> member"
   3.301 +    by (rule fold_commute) (simp add: fun_eq_iff)
   3.302 +  then have "fold Set.insert xs (member A) =
   3.303 +    member (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> member) xs A)"
   3.304 +    by (simp add: fun_eq_iff)
   3.305 +  then have "sup (Cset.set xs) A = fold insert xs A"
   3.306 +    by (simp add: union_set *)
   3.307 +  moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y"
   3.308 +    by (auto simp add: * intro: ext)
   3.309 +  ultimately show "sup (Cset.set xs) A = foldr insert xs A"
   3.310 +    by (simp add: foldr_fold)
   3.311 +  show "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)"
   3.312 +    by (auto simp add: coset_def)
   3.313 +qed
   3.314 +
   3.315 +context complete_lattice
   3.316 +begin
   3.317 +
   3.318 +definition Infimum :: "'a Cset.set \<Rightarrow> 'a" where
   3.319 +  [simp]: "Infimum A = Inf (member A)"
   3.320 +
   3.321 +lemma Infimum_inf [code]:
   3.322 +  "Infimum (Cset.set As) = foldr inf As top"
   3.323 +  "Infimum (Cset.coset []) = bot"
   3.324 +  by (simp_all add: Inf_set_foldr Inf_UNIV)
   3.325 +
   3.326 +definition Supremum :: "'a Cset.set \<Rightarrow> 'a" where
   3.327 +  [simp]: "Supremum A = Sup (member A)"
   3.328 +
   3.329 +lemma Supremum_sup [code]:
   3.330 +  "Supremum (Cset.set As) = foldr sup As bot"
   3.331 +  "Supremum (Cset.coset []) = top"
   3.332 +  by (simp_all add: Sup_set_foldr Sup_UNIV)
   3.333 +
   3.334 +end
   3.335 +
   3.336 +
   3.337 +subsection {* Simplified simprules *}
   3.338 +
   3.339 +lemma is_empty_simp [simp]:
   3.340 +  "is_empty A \<longleftrightarrow> member A = {}"
   3.341 +  by (simp add: More_Set.is_empty_def)
   3.342 +declare is_empty_def [simp del]
   3.343 +
   3.344 +lemma remove_simp [simp]:
   3.345 +  "remove x A = Set (member A - {x})"
   3.346 +  by (simp add: More_Set.remove_def)
   3.347 +declare remove_def [simp del]
   3.348 +
   3.349 +lemma filter_simp [simp]:
   3.350 +  "filter P A = Set {x \<in> member A. P x}"
   3.351 +  by (simp add: More_Set.project_def)
   3.352 +declare filter_def [simp del]
   3.353 +
   3.354 +declare mem_def [simp del]
   3.355 +
   3.356 +
   3.357 +hide_const (open) setify is_empty insert remove map filter forall exists card
   3.358 +  Inter Union
   3.359 +
   3.360 +end
     4.1 --- a/src/HOL/Library/Dlist.thy	Mon Nov 22 09:37:39 2010 +0100
     4.2 +++ b/src/HOL/Library/Dlist.thy	Mon Nov 22 17:46:51 2010 +0100
     4.3 @@ -3,7 +3,7 @@
     4.4  header {* Lists with elements distinct as canonical example for datatype invariants *}
     4.5  
     4.6  theory Dlist
     4.7 -imports Main Fset
     4.8 +imports Main Cset
     4.9  begin
    4.10  
    4.11  section {* The type of distinct lists *}
    4.12 @@ -181,27 +181,27 @@
    4.13  
    4.14  section {* Implementation of sets by distinct lists -- canonical! *}
    4.15  
    4.16 -definition Set :: "'a dlist \<Rightarrow> 'a fset" where
    4.17 -  "Set dxs = Fset.Set (list_of_dlist dxs)"
    4.18 +definition Set :: "'a dlist \<Rightarrow> 'a Cset.set" where
    4.19 +  "Set dxs = Cset.set (list_of_dlist dxs)"
    4.20  
    4.21 -definition Coset :: "'a dlist \<Rightarrow> 'a fset" where
    4.22 -  "Coset dxs = Fset.Coset (list_of_dlist dxs)"
    4.23 +definition Coset :: "'a dlist \<Rightarrow> 'a Cset.set" where
    4.24 +  "Coset dxs = Cset.coset (list_of_dlist dxs)"
    4.25  
    4.26  code_datatype Set Coset
    4.27  
    4.28  declare member_code [code del]
    4.29 -declare is_empty_Set [code del]
    4.30 -declare empty_Set [code del]
    4.31 -declare UNIV_Set [code del]
    4.32 -declare insert_Set [code del]
    4.33 -declare remove_Set [code del]
    4.34 -declare compl_Set [code del]
    4.35 -declare compl_Coset [code del]
    4.36 -declare map_Set [code del]
    4.37 -declare filter_Set [code del]
    4.38 -declare forall_Set [code del]
    4.39 -declare exists_Set [code del]
    4.40 -declare card_Set [code del]
    4.41 +declare Cset.is_empty_set [code del]
    4.42 +declare Cset.empty_set [code del]
    4.43 +declare Cset.UNIV_set [code del]
    4.44 +declare insert_set [code del]
    4.45 +declare remove_set [code del]
    4.46 +declare compl_set [code del]
    4.47 +declare compl_coset [code del]
    4.48 +declare map_set [code del]
    4.49 +declare filter_set [code del]
    4.50 +declare forall_set [code del]
    4.51 +declare exists_set [code del]
    4.52 +declare card_set [code del]
    4.53  declare inter_project [code del]
    4.54  declare subtract_remove [code del]
    4.55  declare union_insert [code del]
    4.56 @@ -209,31 +209,31 @@
    4.57  declare Supremum_sup [code del]
    4.58  
    4.59  lemma Set_Dlist [simp]:
    4.60 -  "Set (Dlist xs) = Fset (set xs)"
    4.61 -  by (rule fset_eqI) (simp add: Set_def)
    4.62 +  "Set (Dlist xs) = Cset.Set (set xs)"
    4.63 +  by (rule Cset.set_eqI) (simp add: Set_def)
    4.64  
    4.65  lemma Coset_Dlist [simp]:
    4.66 -  "Coset (Dlist xs) = Fset (- set xs)"
    4.67 -  by (rule fset_eqI) (simp add: Coset_def)
    4.68 +  "Coset (Dlist xs) = Cset.Set (- set xs)"
    4.69 +  by (rule Cset.set_eqI) (simp add: Coset_def)
    4.70  
    4.71  lemma member_Set [simp]:
    4.72 -  "Fset.member (Set dxs) = List.member (list_of_dlist dxs)"
    4.73 +  "Cset.member (Set dxs) = List.member (list_of_dlist dxs)"
    4.74    by (simp add: Set_def member_set)
    4.75  
    4.76  lemma member_Coset [simp]:
    4.77 -  "Fset.member (Coset dxs) = Not \<circ> List.member (list_of_dlist dxs)"
    4.78 +  "Cset.member (Coset dxs) = Not \<circ> List.member (list_of_dlist dxs)"
    4.79    by (simp add: Coset_def member_set not_set_compl)
    4.80  
    4.81  lemma Set_dlist_of_list [code]:
    4.82 -  "Fset.Set xs = Set (dlist_of_list xs)"
    4.83 -  by (rule fset_eqI) simp
    4.84 +  "Cset.set xs = Set (dlist_of_list xs)"
    4.85 +  by (rule Cset.set_eqI) simp
    4.86  
    4.87  lemma Coset_dlist_of_list [code]:
    4.88 -  "Fset.Coset xs = Coset (dlist_of_list xs)"
    4.89 -  by (rule fset_eqI) simp
    4.90 +  "Cset.coset xs = Coset (dlist_of_list xs)"
    4.91 +  by (rule Cset.set_eqI) simp
    4.92  
    4.93  lemma is_empty_Set [code]:
    4.94 -  "Fset.is_empty (Set dxs) \<longleftrightarrow> null dxs"
    4.95 +  "Cset.is_empty (Set dxs) \<longleftrightarrow> null dxs"
    4.96    by (simp add: null_def List.null_def member_set)
    4.97  
    4.98  lemma bot_code [code]:
    4.99 @@ -245,58 +245,58 @@
   4.100    by (simp add: empty_def)
   4.101  
   4.102  lemma insert_code [code]:
   4.103 -  "Fset.insert x (Set dxs) = Set (insert x dxs)"
   4.104 -  "Fset.insert x (Coset dxs) = Coset (remove x dxs)"
   4.105 +  "Cset.insert x (Set dxs) = Set (insert x dxs)"
   4.106 +  "Cset.insert x (Coset dxs) = Coset (remove x dxs)"
   4.107    by (simp_all add: insert_def remove_def member_set not_set_compl)
   4.108  
   4.109  lemma remove_code [code]:
   4.110 -  "Fset.remove x (Set dxs) = Set (remove x dxs)"
   4.111 -  "Fset.remove x (Coset dxs) = Coset (insert x dxs)"
   4.112 +  "Cset.remove x (Set dxs) = Set (remove x dxs)"
   4.113 +  "Cset.remove x (Coset dxs) = Coset (insert x dxs)"
   4.114    by (auto simp add: insert_def remove_def member_set not_set_compl)
   4.115  
   4.116  lemma member_code [code]:
   4.117 -  "Fset.member (Set dxs) = member dxs"
   4.118 -  "Fset.member (Coset dxs) = Not \<circ> member dxs"
   4.119 +  "Cset.member (Set dxs) = member dxs"
   4.120 +  "Cset.member (Coset dxs) = Not \<circ> member dxs"
   4.121    by (simp_all add: member_def)
   4.122  
   4.123  lemma compl_code [code]:
   4.124    "- Set dxs = Coset dxs"
   4.125    "- Coset dxs = Set dxs"
   4.126 -  by (rule fset_eqI, simp add: member_set not_set_compl)+
   4.127 +  by (rule Cset.set_eqI, simp add: member_set not_set_compl)+
   4.128  
   4.129  lemma map_code [code]:
   4.130 -  "Fset.map f (Set dxs) = Set (map f dxs)"
   4.131 -  by (rule fset_eqI) (simp add: member_set)
   4.132 +  "Cset.map f (Set dxs) = Set (map f dxs)"
   4.133 +  by (rule Cset.set_eqI) (simp add: member_set)
   4.134    
   4.135  lemma filter_code [code]:
   4.136 -  "Fset.filter f (Set dxs) = Set (filter f dxs)"
   4.137 -  by (rule fset_eqI) (simp add: member_set)
   4.138 +  "Cset.filter f (Set dxs) = Set (filter f dxs)"
   4.139 +  by (rule Cset.set_eqI) (simp add: member_set)
   4.140  
   4.141  lemma forall_Set [code]:
   4.142 -  "Fset.forall P (Set xs) \<longleftrightarrow> list_all P (list_of_dlist xs)"
   4.143 +  "Cset.forall P (Set xs) \<longleftrightarrow> list_all P (list_of_dlist xs)"
   4.144    by (simp add: member_set list_all_iff)
   4.145  
   4.146  lemma exists_Set [code]:
   4.147 -  "Fset.exists P (Set xs) \<longleftrightarrow> list_ex P (list_of_dlist xs)"
   4.148 +  "Cset.exists P (Set xs) \<longleftrightarrow> list_ex P (list_of_dlist xs)"
   4.149    by (simp add: member_set list_ex_iff)
   4.150  
   4.151  lemma card_code [code]:
   4.152 -  "Fset.card (Set dxs) = length dxs"
   4.153 +  "Cset.card (Set dxs) = length dxs"
   4.154    by (simp add: length_def member_set distinct_card)
   4.155  
   4.156  lemma inter_code [code]:
   4.157 -  "inf A (Set xs) = Set (filter (Fset.member A) xs)"
   4.158 -  "inf A (Coset xs) = foldr Fset.remove xs A"
   4.159 +  "inf A (Set xs) = Set (filter (Cset.member A) xs)"
   4.160 +  "inf A (Coset xs) = foldr Cset.remove xs A"
   4.161    by (simp_all only: Set_def Coset_def foldr_def inter_project list_of_dlist_filter)
   4.162  
   4.163  lemma subtract_code [code]:
   4.164 -  "A - Set xs = foldr Fset.remove xs A"
   4.165 -  "A - Coset xs = Set (filter (Fset.member A) xs)"
   4.166 +  "A - Set xs = foldr Cset.remove xs A"
   4.167 +  "A - Coset xs = Set (filter (Cset.member A) xs)"
   4.168    by (simp_all only: Set_def Coset_def foldr_def subtract_remove list_of_dlist_filter)
   4.169  
   4.170  lemma union_code [code]:
   4.171 -  "sup (Set xs) A = foldr Fset.insert xs A"
   4.172 -  "sup (Coset xs) A = Coset (filter (Not \<circ> Fset.member A) xs)"
   4.173 +  "sup (Set xs) A = foldr Cset.insert xs A"
   4.174 +  "sup (Coset xs) A = Coset (filter (Not \<circ> Cset.member A) xs)"
   4.175    by (simp_all only: Set_def Coset_def foldr_def union_insert list_of_dlist_filter)
   4.176  
   4.177  context complete_lattice
     5.1 --- a/src/HOL/Library/Executable_Set.thy	Mon Nov 22 09:37:39 2010 +0100
     5.2 +++ b/src/HOL/Library/Executable_Set.thy	Mon Nov 22 17:46:51 2010 +0100
     5.3 @@ -12,7 +12,7 @@
     5.4  text {*
     5.5    This is just an ad-hoc hack which will rarely give you what you want.
     5.6    For the moment, whenever you need executable sets, consider using
     5.7 -  type @{text fset} from theory @{text Fset}.
     5.8 +  type @{text fset} from theory @{text Cset}.
     5.9  *}
    5.10  
    5.11  declare mem_def [code del]
     6.1 --- a/src/HOL/Library/Fset.thy	Mon Nov 22 09:37:39 2010 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,347 +0,0 @@
     6.4 -
     6.5 -(* Author: Florian Haftmann, TU Muenchen *)
     6.6 -
     6.7 -header {* A set type which is executable on its finite part *}
     6.8 -
     6.9 -theory Fset
    6.10 -imports More_Set More_List
    6.11 -begin
    6.12 -
    6.13 -subsection {* Lifting *}
    6.14 -
    6.15 -typedef (open) 'a fset = "UNIV :: 'a set set"
    6.16 -  morphisms member Fset by rule+
    6.17 -
    6.18 -lemma member_Fset [simp]:
    6.19 -  "member (Fset A) = A"
    6.20 -  by (rule Fset_inverse) rule
    6.21 -
    6.22 -lemma Fset_member [simp]:
    6.23 -  "Fset (member A) = A"
    6.24 -  by (fact member_inverse)
    6.25 -
    6.26 -lemma Fset_inject [simp]:
    6.27 -  "Fset A = Fset B \<longleftrightarrow> A = B"
    6.28 -  by (simp add: Fset_inject)
    6.29 -
    6.30 -lemma fset_eq_iff:
    6.31 -  "A = B \<longleftrightarrow> member A = member B"
    6.32 -  by (simp add: member_inject)
    6.33 -
    6.34 -lemma fset_eqI:
    6.35 -  "member A = member B \<Longrightarrow> A = B"
    6.36 -  by (simp add: fset_eq_iff)
    6.37 -
    6.38 -declare mem_def [simp]
    6.39 -
    6.40 -definition Set :: "'a list \<Rightarrow> 'a fset" where
    6.41 -  "Set xs = Fset (set xs)"
    6.42 -
    6.43 -lemma member_Set [simp]:
    6.44 -  "member (Set xs) = set xs"
    6.45 -  by (simp add: Set_def)
    6.46 -
    6.47 -definition Coset :: "'a list \<Rightarrow> 'a fset" where
    6.48 -  "Coset xs = Fset (- set xs)"
    6.49 -
    6.50 -lemma member_Coset [simp]:
    6.51 -  "member (Coset xs) = - set xs"
    6.52 -  by (simp add: Coset_def)
    6.53 -
    6.54 -code_datatype Set Coset
    6.55 -
    6.56 -lemma member_code [code]:
    6.57 -  "member (Set xs) = List.member xs"
    6.58 -  "member (Coset xs) = Not \<circ> List.member xs"
    6.59 -  by (simp_all add: fun_eq_iff member_def fun_Compl_def bool_Compl_def)
    6.60 -
    6.61 -lemma member_image_UNIV [simp]:
    6.62 -  "member ` UNIV = UNIV"
    6.63 -proof -
    6.64 -  have "\<And>A \<Colon> 'a set. \<exists>B \<Colon> 'a fset. A = member B"
    6.65 -  proof
    6.66 -    fix A :: "'a set"
    6.67 -    show "A = member (Fset A)" by simp
    6.68 -  qed
    6.69 -  then show ?thesis by (simp add: image_def)
    6.70 -qed
    6.71 -
    6.72 -definition (in term_syntax)
    6.73 -  setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
    6.74 -    \<Rightarrow> 'a fset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
    6.75 -  [code_unfold]: "setify xs = Code_Evaluation.valtermify Set {\<cdot>} xs"
    6.76 -
    6.77 -notation fcomp (infixl "\<circ>>" 60)
    6.78 -notation scomp (infixl "\<circ>\<rightarrow>" 60)
    6.79 -
    6.80 -instantiation fset :: (random) random
    6.81 -begin
    6.82 -
    6.83 -definition
    6.84 -  "Quickcheck.random i = Quickcheck.random i \<circ>\<rightarrow> (\<lambda>xs. Pair (setify xs))"
    6.85 -
    6.86 -instance ..
    6.87 -
    6.88 -end
    6.89 -
    6.90 -no_notation fcomp (infixl "\<circ>>" 60)
    6.91 -no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
    6.92 -
    6.93 -
    6.94 -subsection {* Lattice instantiation *}
    6.95 -
    6.96 -instantiation fset :: (type) boolean_algebra
    6.97 -begin
    6.98 -
    6.99 -definition less_eq_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
   6.100 -  [simp]: "A \<le> B \<longleftrightarrow> member A \<subseteq> member B"
   6.101 -
   6.102 -definition less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
   6.103 -  [simp]: "A < B \<longleftrightarrow> member A \<subset> member B"
   6.104 -
   6.105 -definition inf_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
   6.106 -  [simp]: "inf A B = Fset (member A \<inter> member B)"
   6.107 -
   6.108 -definition sup_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
   6.109 -  [simp]: "sup A B = Fset (member A \<union> member B)"
   6.110 -
   6.111 -definition bot_fset :: "'a fset" where
   6.112 -  [simp]: "bot = Fset {}"
   6.113 -
   6.114 -definition top_fset :: "'a fset" where
   6.115 -  [simp]: "top = Fset UNIV"
   6.116 -
   6.117 -definition uminus_fset :: "'a fset \<Rightarrow> 'a fset" where
   6.118 -  [simp]: "- A = Fset (- (member A))"
   6.119 -
   6.120 -definition minus_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
   6.121 -  [simp]: "A - B = Fset (member A - member B)"
   6.122 -
   6.123 -instance proof
   6.124 -qed (auto intro: fset_eqI)
   6.125 -
   6.126 -end
   6.127 -
   6.128 -instantiation fset :: (type) complete_lattice
   6.129 -begin
   6.130 -
   6.131 -definition Inf_fset :: "'a fset set \<Rightarrow> 'a fset" where
   6.132 -  [simp]: "Inf_fset As = Fset (Inf (image member As))"
   6.133 -
   6.134 -definition Sup_fset :: "'a fset set \<Rightarrow> 'a fset" where
   6.135 -  [simp]: "Sup_fset As = Fset (Sup (image member As))"
   6.136 -
   6.137 -instance proof
   6.138 -qed (auto simp add: le_fun_def le_bool_def)
   6.139 -
   6.140 -end
   6.141 -
   6.142 -
   6.143 -subsection {* Basic operations *}
   6.144 -
   6.145 -definition is_empty :: "'a fset \<Rightarrow> bool" where
   6.146 -  [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)"
   6.147 -
   6.148 -lemma is_empty_Set [code]:
   6.149 -  "is_empty (Set xs) \<longleftrightarrow> List.null xs"
   6.150 -  by (simp add: is_empty_set)
   6.151 -
   6.152 -lemma empty_Set [code]:
   6.153 -  "bot = Set []"
   6.154 -  by (simp add: Set_def)
   6.155 -
   6.156 -lemma UNIV_Set [code]:
   6.157 -  "top = Coset []"
   6.158 -  by (simp add: Coset_def)
   6.159 -
   6.160 -definition insert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
   6.161 -  [simp]: "insert x A = Fset (Set.insert x (member A))"
   6.162 -
   6.163 -lemma insert_Set [code]:
   6.164 -  "insert x (Set xs) = Set (List.insert x xs)"
   6.165 -  "insert x (Coset xs) = Coset (removeAll x xs)"
   6.166 -  by (simp_all add: Set_def Coset_def)
   6.167 -
   6.168 -definition remove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
   6.169 -  [simp]: "remove x A = Fset (More_Set.remove x (member A))"
   6.170 -
   6.171 -lemma remove_Set [code]:
   6.172 -  "remove x (Set xs) = Set (removeAll x xs)"
   6.173 -  "remove x (Coset xs) = Coset (List.insert x xs)"
   6.174 -  by (simp_all add: Set_def Coset_def remove_set_compl)
   6.175 -    (simp add: More_Set.remove_def)
   6.176 -
   6.177 -definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" where
   6.178 -  [simp]: "map f A = Fset (image f (member A))"
   6.179 -
   6.180 -lemma map_Set [code]:
   6.181 -  "map f (Set xs) = Set (remdups (List.map f xs))"
   6.182 -  by (simp add: Set_def)
   6.183 -
   6.184 -type_mapper map
   6.185 -  by (simp_all add: image_image)
   6.186 -
   6.187 -definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
   6.188 -  [simp]: "filter P A = Fset (More_Set.project P (member A))"
   6.189 -
   6.190 -lemma filter_Set [code]:
   6.191 -  "filter P (Set xs) = Set (List.filter P xs)"
   6.192 -  by (simp add: Set_def project_set)
   6.193 -
   6.194 -definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
   6.195 -  [simp]: "forall P A \<longleftrightarrow> Ball (member A) P"
   6.196 -
   6.197 -lemma forall_Set [code]:
   6.198 -  "forall P (Set xs) \<longleftrightarrow> list_all P xs"
   6.199 -  by (simp add: Set_def list_all_iff)
   6.200 -
   6.201 -definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
   6.202 -  [simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
   6.203 -
   6.204 -lemma exists_Set [code]:
   6.205 -  "exists P (Set xs) \<longleftrightarrow> list_ex P xs"
   6.206 -  by (simp add: Set_def list_ex_iff)
   6.207 -
   6.208 -definition card :: "'a fset \<Rightarrow> nat" where
   6.209 -  [simp]: "card A = Finite_Set.card (member A)"
   6.210 -
   6.211 -lemma card_Set [code]:
   6.212 -  "card (Set xs) = length (remdups xs)"
   6.213 -proof -
   6.214 -  have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
   6.215 -    by (rule distinct_card) simp
   6.216 -  then show ?thesis by (simp add: Set_def)
   6.217 -qed
   6.218 -
   6.219 -lemma compl_Set [simp, code]:
   6.220 -  "- Set xs = Coset xs"
   6.221 -  by (simp add: Set_def Coset_def)
   6.222 -
   6.223 -lemma compl_Coset [simp, code]:
   6.224 -  "- Coset xs = Set xs"
   6.225 -  by (simp add: Set_def Coset_def)
   6.226 -
   6.227 -
   6.228 -subsection {* Derived operations *}
   6.229 -
   6.230 -lemma subfset_eq_forall [code]:
   6.231 -  "A \<le> B \<longleftrightarrow> forall (member B) A"
   6.232 -  by (simp add: subset_eq)
   6.233 -
   6.234 -lemma subfset_subfset_eq [code]:
   6.235 -  "A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a fset)"
   6.236 -  by (fact less_le_not_le)
   6.237 -
   6.238 -instantiation fset :: (type) equal
   6.239 -begin
   6.240 -
   6.241 -definition [code]:
   6.242 -  "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a fset)"
   6.243 -
   6.244 -instance proof
   6.245 -qed (simp add: equal_fset_def set_eq [symmetric] fset_eq_iff)
   6.246 -
   6.247 -end
   6.248 -
   6.249 -lemma [code nbe]:
   6.250 -  "HOL.equal (A :: 'a fset) A \<longleftrightarrow> True"
   6.251 -  by (fact equal_refl)
   6.252 -
   6.253 -
   6.254 -subsection {* Functorial operations *}
   6.255 -
   6.256 -lemma inter_project [code]:
   6.257 -  "inf A (Set xs) = Set (List.filter (member A) xs)"
   6.258 -  "inf A (Coset xs) = foldr remove xs A"
   6.259 -proof -
   6.260 -  show "inf A (Set xs) = Set (List.filter (member A) xs)"
   6.261 -    by (simp add: inter project_def Set_def)
   6.262 -  have *: "\<And>x::'a. remove = (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member)"
   6.263 -    by (simp add: fun_eq_iff)
   6.264 -  have "member \<circ> fold (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member) xs =
   6.265 -    fold More_Set.remove xs \<circ> member"
   6.266 -    by (rule fold_commute) (simp add: fun_eq_iff)
   6.267 -  then have "fold More_Set.remove xs (member A) = 
   6.268 -    member (fold (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member) xs A)"
   6.269 -    by (simp add: fun_eq_iff)
   6.270 -  then have "inf A (Coset xs) = fold remove xs A"
   6.271 -    by (simp add: Diff_eq [symmetric] minus_set *)
   6.272 -  moreover have "\<And>x y :: 'a. Fset.remove y \<circ> Fset.remove x = Fset.remove x \<circ> Fset.remove y"
   6.273 -    by (auto simp add: More_Set.remove_def * intro: ext)
   6.274 -  ultimately show "inf A (Coset xs) = foldr remove xs A"
   6.275 -    by (simp add: foldr_fold)
   6.276 -qed
   6.277 -
   6.278 -lemma subtract_remove [code]:
   6.279 -  "A - Set xs = foldr remove xs A"
   6.280 -  "A - Coset xs = Set (List.filter (member A) xs)"
   6.281 -  by (simp_all only: diff_eq compl_Set compl_Coset inter_project)
   6.282 -
   6.283 -lemma union_insert [code]:
   6.284 -  "sup (Set xs) A = foldr insert xs A"
   6.285 -  "sup (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)"
   6.286 -proof -
   6.287 -  have *: "\<And>x::'a. insert = (\<lambda>x. Fset \<circ> Set.insert x \<circ> member)"
   6.288 -    by (simp add: fun_eq_iff)
   6.289 -  have "member \<circ> fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs =
   6.290 -    fold Set.insert xs \<circ> member"
   6.291 -    by (rule fold_commute) (simp add: fun_eq_iff)
   6.292 -  then have "fold Set.insert xs (member A) =
   6.293 -    member (fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs A)"
   6.294 -    by (simp add: fun_eq_iff)
   6.295 -  then have "sup (Set xs) A = fold insert xs A"
   6.296 -    by (simp add: union_set *)
   6.297 -  moreover have "\<And>x y :: 'a. Fset.insert y \<circ> Fset.insert x = Fset.insert x \<circ> Fset.insert y"
   6.298 -    by (auto simp add: * intro: ext)
   6.299 -  ultimately show "sup (Set xs) A = foldr insert xs A"
   6.300 -    by (simp add: foldr_fold)
   6.301 -  show "sup (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)"
   6.302 -    by (auto simp add: Coset_def)
   6.303 -qed
   6.304 -
   6.305 -context complete_lattice
   6.306 -begin
   6.307 -
   6.308 -definition Infimum :: "'a fset \<Rightarrow> 'a" where
   6.309 -  [simp]: "Infimum A = Inf (member A)"
   6.310 -
   6.311 -lemma Infimum_inf [code]:
   6.312 -  "Infimum (Set As) = foldr inf As top"
   6.313 -  "Infimum (Coset []) = bot"
   6.314 -  by (simp_all add: Inf_set_foldr Inf_UNIV)
   6.315 -
   6.316 -definition Supremum :: "'a fset \<Rightarrow> 'a" where
   6.317 -  [simp]: "Supremum A = Sup (member A)"
   6.318 -
   6.319 -lemma Supremum_sup [code]:
   6.320 -  "Supremum (Set As) = foldr sup As bot"
   6.321 -  "Supremum (Coset []) = top"
   6.322 -  by (simp_all add: Sup_set_foldr Sup_UNIV)
   6.323 -
   6.324 -end
   6.325 -
   6.326 -
   6.327 -subsection {* Simplified simprules *}
   6.328 -
   6.329 -lemma is_empty_simp [simp]:
   6.330 -  "is_empty A \<longleftrightarrow> member A = {}"
   6.331 -  by (simp add: More_Set.is_empty_def)
   6.332 -declare is_empty_def [simp del]
   6.333 -
   6.334 -lemma remove_simp [simp]:
   6.335 -  "remove x A = Fset (member A - {x})"
   6.336 -  by (simp add: More_Set.remove_def)
   6.337 -declare remove_def [simp del]
   6.338 -
   6.339 -lemma filter_simp [simp]:
   6.340 -  "filter P A = Fset {x \<in> member A. P x}"
   6.341 -  by (simp add: More_Set.project_def)
   6.342 -declare filter_def [simp del]
   6.343 -
   6.344 -declare mem_def [simp del]
   6.345 -
   6.346 -
   6.347 -hide_const (open) setify is_empty insert remove map filter forall exists card
   6.348 -  Inter Union
   6.349 -
   6.350 -end
     7.1 --- a/src/HOL/Library/Library.thy	Mon Nov 22 09:37:39 2010 +0100
     7.2 +++ b/src/HOL/Library/Library.thy	Mon Nov 22 17:46:51 2010 +0100
     7.3 @@ -20,7 +20,7 @@
     7.4    Formal_Power_Series
     7.5    Fraction_Field
     7.6    FrechetDeriv
     7.7 -  Fset
     7.8 +  Cset
     7.9    FuncSet
    7.10    Function_Algebras
    7.11    Fundamental_Theorem_Algebra
     8.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Mon Nov 22 09:37:39 2010 +0100
     8.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Mon Nov 22 17:46:51 2010 +0100
     8.3 @@ -25,7 +25,7 @@
     8.4    unfolding reflp_def symp_def transp_def
     8.5    by auto
     8.6  
     8.7 -text {* Fset type *}
     8.8 +text {* Cset type *}
     8.9  
    8.10  quotient_type
    8.11    'a fset = "'a list" / "list_eq"