renamed theory Code_Set to Fset
authorhaftmann
Mon Jun 29 12:18:55 2009 +0200 (2009-06-29)
changeset 31849431d8588bcad
parent 31848 e5ab21d14974
child 31850 e81d0f04ffdf
renamed theory Code_Set to Fset
src/HOL/IsaMakefile
src/HOL/Library/Code_Set.thy
src/HOL/Library/Fset.thy
src/HOL/Library/Library.thy
src/HOL/ex/Codegenerator_Candidates.thy
     1.1 --- a/src/HOL/IsaMakefile	Mon Jun 29 12:18:54 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Jun 29 12:18:55 2009 +0200
     1.3 @@ -319,7 +319,7 @@
     1.4    Library/Abstract_Rat.thy \
     1.5    Library/BigO.thy Library/ContNotDenum.thy Library/Efficient_Nat.thy	\
     1.6    Library/Euclidean_Space.thy Library/Sum_Of_Squares.thy Library/positivstellensatz.ML	\
     1.7 -  Library/Code_Set.thy  Library/Convex_Euclidean_Space.thy \
     1.8 +  Library/Fset.thy  Library/Convex_Euclidean_Space.thy \
     1.9    Library/sum_of_squares.ML Library/Glbs.thy Library/normarith.ML \
    1.10    Library/Executable_Set.thy Library/Infinite_Set.thy			\
    1.11    Library/FuncSet.thy Library/Permutations.thy Library/Determinants.thy\
     2.1 --- a/src/HOL/Library/Code_Set.thy	Mon Jun 29 12:18:54 2009 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,224 +0,0 @@
     2.4 -
     2.5 -(* Author: Florian Haftmann, TU Muenchen *)
     2.6 -
     2.7 -header {* Executable finite sets *}
     2.8 -
     2.9 -theory Code_Set
    2.10 -imports List_Set
    2.11 -begin
    2.12 -
    2.13 -lemma foldl_apply_inv:
    2.14 -  assumes "\<And>x. g (h x) = x"
    2.15 -  shows "foldl f (g s) xs = g (foldl (\<lambda>s x. h (f (g s) x)) s xs)"
    2.16 -  by (rule sym, induct xs arbitrary: s) (simp_all add: assms)
    2.17 -
    2.18 -declare mem_def [simp]
    2.19 -
    2.20 -subsection {* Lifting *}
    2.21 -
    2.22 -datatype 'a fset = Fset "'a set"
    2.23 -
    2.24 -primrec member :: "'a fset \<Rightarrow> 'a set" where
    2.25 -  "member (Fset A) = A"
    2.26 -
    2.27 -lemma Fset_member [simp]:
    2.28 -  "Fset (member A) = A"
    2.29 -  by (cases A) simp
    2.30 -
    2.31 -definition Set :: "'a list \<Rightarrow> 'a fset" where
    2.32 -  "Set xs = Fset (set xs)"
    2.33 -
    2.34 -lemma member_Set [simp]:
    2.35 -  "member (Set xs) = set xs"
    2.36 -  by (simp add: Set_def)
    2.37 -
    2.38 -code_datatype Set
    2.39 -
    2.40 -
    2.41 -subsection {* Basic operations *}
    2.42 -
    2.43 -definition is_empty :: "'a fset \<Rightarrow> bool" where
    2.44 -  [simp]: "is_empty A \<longleftrightarrow> List_Set.is_empty (member A)"
    2.45 -
    2.46 -lemma is_empty_Set [code]:
    2.47 -  "is_empty (Set xs) \<longleftrightarrow> null xs"
    2.48 -  by (simp add: is_empty_set)
    2.49 -
    2.50 -definition empty :: "'a fset" where
    2.51 -  [simp]: "empty = Fset {}"
    2.52 -
    2.53 -lemma empty_Set [code]:
    2.54 -  "empty = Set []"
    2.55 -  by (simp add: Set_def)
    2.56 -
    2.57 -definition insert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
    2.58 -  [simp]: "insert x A = Fset (Set.insert x (member A))"
    2.59 -
    2.60 -lemma insert_Set [code]:
    2.61 -  "insert x (Set xs) = Set (List_Set.insert x xs)"
    2.62 -  by (simp add: Set_def insert_set)
    2.63 -
    2.64 -definition remove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
    2.65 -  [simp]: "remove x A = Fset (List_Set.remove x (member A))"
    2.66 -
    2.67 -lemma remove_Set [code]:
    2.68 -  "remove x (Set xs) = Set (remove_all x xs)"
    2.69 -  by (simp add: Set_def remove_set)
    2.70 -
    2.71 -definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" where
    2.72 -  [simp]: "map f A = Fset (image f (member A))"
    2.73 -
    2.74 -lemma map_Set [code]:
    2.75 -  "map f (Set xs) = Set (remdups (List.map f xs))"
    2.76 -  by (simp add: Set_def)
    2.77 -
    2.78 -definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
    2.79 -  [simp]: "filter P A = Fset (List_Set.project P (member A))"
    2.80 -
    2.81 -lemma filter_Set [code]:
    2.82 -  "filter P (Set xs) = Set (List.filter P xs)"
    2.83 -  by (simp add: Set_def project_set)
    2.84 -
    2.85 -definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
    2.86 -  [simp]: "forall P A \<longleftrightarrow> Ball (member A) P"
    2.87 -
    2.88 -lemma forall_Set [code]:
    2.89 -  "forall P (Set xs) \<longleftrightarrow> list_all P xs"
    2.90 -  by (simp add: Set_def ball_set)
    2.91 -
    2.92 -definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
    2.93 -  [simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
    2.94 -
    2.95 -lemma exists_Set [code]:
    2.96 -  "exists P (Set xs) \<longleftrightarrow> list_ex P xs"
    2.97 -  by (simp add: Set_def bex_set)
    2.98 -
    2.99 -
   2.100 -subsection {* Derived operations *}
   2.101 -
   2.102 -lemma member_exists [code]:
   2.103 -  "member A y \<longleftrightarrow> exists (\<lambda>x. y = x) A"
   2.104 -  by simp
   2.105 -
   2.106 -definition subfset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
   2.107 -  [simp]: "subfset_eq A B \<longleftrightarrow> member A \<subseteq> member B"
   2.108 -
   2.109 -lemma subfset_eq_forall [code]:
   2.110 -  "subfset_eq A B \<longleftrightarrow> forall (\<lambda>x. member B x) A"
   2.111 -  by (simp add: subset_eq)
   2.112 -
   2.113 -definition subfset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
   2.114 -  [simp]: "subfset A B \<longleftrightarrow> member A \<subset> member B"
   2.115 -
   2.116 -lemma subfset_subfset_eq [code]:
   2.117 -  "subfset A B \<longleftrightarrow> subfset_eq A B \<and> \<not> subfset_eq B A"
   2.118 -  by (simp add: subset)
   2.119 -
   2.120 -lemma eq_fset_subfset_eq [code]:
   2.121 -  "eq_class.eq A B \<longleftrightarrow> subfset_eq A B \<and> subfset_eq B A"
   2.122 -  by (cases A, cases B) (simp add: eq set_eq)
   2.123 -
   2.124 -definition inter :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
   2.125 -  [simp]: "inter A B = Fset (project (member A) (member B))"
   2.126 -
   2.127 -lemma inter_project [code]:
   2.128 -  "inter A B = filter (member A) B"
   2.129 -  by (simp add: inter)
   2.130 -
   2.131 -
   2.132 -subsection {* Functorial operations *}
   2.133 -
   2.134 -definition union :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
   2.135 -  [simp]: "union A B = Fset (member A \<union> member B)"
   2.136 -
   2.137 -lemma union_insert [code]:
   2.138 -  "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
   2.139 -proof -
   2.140 -  have "foldl (\<lambda>A x. Set.insert x A) (member A) xs =
   2.141 -    member (foldl (\<lambda>A x. Fset (Set.insert x (member A))) A xs)"
   2.142 -    by (rule foldl_apply_inv) simp
   2.143 -  then show ?thesis by (simp add: union_set)
   2.144 -qed
   2.145 -
   2.146 -definition subtract :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
   2.147 -  [simp]: "subtract A B = Fset (member B - member A)"
   2.148 -
   2.149 -lemma subtract_remove [code]:
   2.150 -  "subtract (Set xs) A = foldl (\<lambda>A x. remove x A) A xs"
   2.151 -proof -
   2.152 -  have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs =
   2.153 -    member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)"
   2.154 -    by (rule foldl_apply_inv) simp
   2.155 -  then show ?thesis by (simp add: minus_set)
   2.156 -qed
   2.157 -
   2.158 -definition Inter :: "'a fset fset \<Rightarrow> 'a fset" where
   2.159 -  [simp]: "Inter A = Fset (Set.Inter (member ` member A))"
   2.160 -
   2.161 -lemma Inter_inter [code]:
   2.162 -  "Inter (Set (A # As)) = foldl inter A As"
   2.163 -proof -
   2.164 -  note Inter_image_eq [simp del] set_map [simp del] set.simps [simp del]
   2.165 -  have "foldl (op \<inter>) (member A) (List.map member As) = 
   2.166 -    member (foldl (\<lambda>B A. Fset (member B \<inter> A)) A (List.map member As))"
   2.167 -    by (rule foldl_apply_inv) simp
   2.168 -  then show ?thesis
   2.169 -    by (simp add: Inter_set image_set inter_def_raw inter foldl_map)
   2.170 -qed
   2.171 -
   2.172 -definition Union :: "'a fset fset \<Rightarrow> 'a fset" where
   2.173 -  [simp]: "Union A = Fset (Set.Union (member ` member A))"
   2.174 -
   2.175 -lemma Union_union [code]:
   2.176 -  "Union (Set As) = foldl union empty As"
   2.177 -proof -
   2.178 -  note Union_image_eq [simp del] set_map [simp del]
   2.179 -  have "foldl (op \<union>) (member empty) (List.map member As) = 
   2.180 -    member (foldl (\<lambda>B A. Fset (member B \<union> A)) empty (List.map member As))"
   2.181 -    by (rule foldl_apply_inv) simp
   2.182 -  then show ?thesis
   2.183 -    by (simp add: Union_set image_set union_def_raw foldl_map)
   2.184 -qed
   2.185 -
   2.186 -
   2.187 -subsection {* Misc operations *}
   2.188 -
   2.189 -lemma size_fset [code]:
   2.190 -  "fset_size f A = 0"
   2.191 -  "size A = 0"
   2.192 -  by (cases A, simp) (cases A, simp)
   2.193 -
   2.194 -lemma fset_case_code [code]:
   2.195 -  "fset_case f A = f (member A)"
   2.196 -  by (cases A) simp
   2.197 -
   2.198 -lemma fset_rec_code [code]:
   2.199 -  "fset_rec f A = f (member A)"
   2.200 -  by (cases A) simp
   2.201 -
   2.202 -
   2.203 -subsection {* Simplified simprules *}
   2.204 -
   2.205 -lemma is_empty_simp [simp]:
   2.206 -  "is_empty A \<longleftrightarrow> member A = {}"
   2.207 -  by (simp add: List_Set.is_empty_def)
   2.208 -declare is_empty_def [simp del]
   2.209 -
   2.210 -lemma remove_simp [simp]:
   2.211 -  "remove x A = Fset (member A - {x})"
   2.212 -  by (simp add: List_Set.remove_def)
   2.213 -declare remove_def [simp del]
   2.214 -
   2.215 -lemma filter_simp [simp]:
   2.216 -  "filter P A = Fset {x \<in> member A. P x}"
   2.217 -  by (simp add: List_Set.project_def)
   2.218 -declare filter_def [simp del]
   2.219 -
   2.220 -lemma inter_simp [simp]:
   2.221 -  "inter A B = Fset (member A \<inter> member B)"
   2.222 -  by (simp add: inter)
   2.223 -declare inter_def [simp del]
   2.224 -
   2.225 -declare mem_def [simp del]
   2.226 -
   2.227 -end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Fset.thy	Mon Jun 29 12:18:55 2009 +0200
     3.3 @@ -0,0 +1,240 @@
     3.4 +
     3.5 +(* Author: Florian Haftmann, TU Muenchen *)
     3.6 +
     3.7 +header {* Executable finite sets *}
     3.8 +
     3.9 +theory Fset
    3.10 +imports List_Set
    3.11 +begin
    3.12 +
    3.13 +lemma foldl_apply_inv:
    3.14 +  assumes "\<And>x. g (h x) = x"
    3.15 +  shows "foldl f (g s) xs = g (foldl (\<lambda>s x. h (f (g s) x)) s xs)"
    3.16 +  by (rule sym, induct xs arbitrary: s) (simp_all add: assms)
    3.17 +
    3.18 +declare mem_def [simp]
    3.19 +
    3.20 +
    3.21 +subsection {* Lifting *}
    3.22 +
    3.23 +datatype 'a fset = Fset "'a set"
    3.24 +
    3.25 +primrec member :: "'a fset \<Rightarrow> 'a set" where
    3.26 +  "member (Fset A) = A"
    3.27 +
    3.28 +lemma Fset_member [simp]:
    3.29 +  "Fset (member A) = A"
    3.30 +  by (cases A) simp
    3.31 +
    3.32 +definition Set :: "'a list \<Rightarrow> 'a fset" where
    3.33 +  "Set xs = Fset (set xs)"
    3.34 +
    3.35 +lemma member_Set [simp]:
    3.36 +  "member (Set xs) = set xs"
    3.37 +  by (simp add: Set_def)
    3.38 +
    3.39 +code_datatype Set
    3.40 +
    3.41 +
    3.42 +subsection {* Basic operations *}
    3.43 +
    3.44 +definition is_empty :: "'a fset \<Rightarrow> bool" where
    3.45 +  [simp]: "is_empty A \<longleftrightarrow> List_Set.is_empty (member A)"
    3.46 +
    3.47 +lemma is_empty_Set [code]:
    3.48 +  "is_empty (Set xs) \<longleftrightarrow> null xs"
    3.49 +  by (simp add: is_empty_set)
    3.50 +
    3.51 +definition empty :: "'a fset" where
    3.52 +  [simp]: "empty = Fset {}"
    3.53 +
    3.54 +lemma empty_Set [code]:
    3.55 +  "empty = Set []"
    3.56 +  by (simp add: Set_def)
    3.57 +
    3.58 +definition insert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
    3.59 +  [simp]: "insert x A = Fset (Set.insert x (member A))"
    3.60 +
    3.61 +lemma insert_Set [code]:
    3.62 +  "insert x (Set xs) = Set (List_Set.insert x xs)"
    3.63 +  by (simp add: Set_def insert_set)
    3.64 +
    3.65 +definition remove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
    3.66 +  [simp]: "remove x A = Fset (List_Set.remove x (member A))"
    3.67 +
    3.68 +lemma remove_Set [code]:
    3.69 +  "remove x (Set xs) = Set (remove_all x xs)"
    3.70 +  by (simp add: Set_def remove_set)
    3.71 +
    3.72 +definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" where
    3.73 +  [simp]: "map f A = Fset (image f (member A))"
    3.74 +
    3.75 +lemma map_Set [code]:
    3.76 +  "map f (Set xs) = Set (remdups (List.map f xs))"
    3.77 +  by (simp add: Set_def)
    3.78 +
    3.79 +definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
    3.80 +  [simp]: "filter P A = Fset (List_Set.project P (member A))"
    3.81 +
    3.82 +lemma filter_Set [code]:
    3.83 +  "filter P (Set xs) = Set (List.filter P xs)"
    3.84 +  by (simp add: Set_def project_set)
    3.85 +
    3.86 +definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
    3.87 +  [simp]: "forall P A \<longleftrightarrow> Ball (member A) P"
    3.88 +
    3.89 +lemma forall_Set [code]:
    3.90 +  "forall P (Set xs) \<longleftrightarrow> list_all P xs"
    3.91 +  by (simp add: Set_def ball_set)
    3.92 +
    3.93 +definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
    3.94 +  [simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
    3.95 +
    3.96 +lemma exists_Set [code]:
    3.97 +  "exists P (Set xs) \<longleftrightarrow> list_ex P xs"
    3.98 +  by (simp add: Set_def bex_set)
    3.99 +
   3.100 +definition card :: "'a fset \<Rightarrow> nat" where
   3.101 +  [simp]: "card A = Finite_Set.card (member A)"
   3.102 +
   3.103 +lemma card_Set [code]:
   3.104 +  "card (Set xs) = length (remdups xs)"
   3.105 +proof -
   3.106 +  have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
   3.107 +    by (rule distinct_card) simp
   3.108 +  then show ?thesis by (simp add: Set_def card_def)
   3.109 +qed
   3.110 +
   3.111 +
   3.112 +subsection {* Derived operations *}
   3.113 +
   3.114 +lemma member_exists [code]:
   3.115 +  "member A y \<longleftrightarrow> exists (\<lambda>x. y = x) A"
   3.116 +  by simp
   3.117 +
   3.118 +definition subfset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
   3.119 +  [simp]: "subfset_eq A B \<longleftrightarrow> member A \<subseteq> member B"
   3.120 +
   3.121 +lemma subfset_eq_forall [code]:
   3.122 +  "subfset_eq A B \<longleftrightarrow> forall (\<lambda>x. member B x) A"
   3.123 +  by (simp add: subset_eq)
   3.124 +
   3.125 +definition subfset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
   3.126 +  [simp]: "subfset A B \<longleftrightarrow> member A \<subset> member B"
   3.127 +
   3.128 +lemma subfset_subfset_eq [code]:
   3.129 +  "subfset A B \<longleftrightarrow> subfset_eq A B \<and> \<not> subfset_eq B A"
   3.130 +  by (simp add: subset)
   3.131 +
   3.132 +lemma eq_fset_subfset_eq [code]:
   3.133 +  "eq_class.eq A B \<longleftrightarrow> subfset_eq A B \<and> subfset_eq B A"
   3.134 +  by (cases A, cases B) (simp add: eq set_eq)
   3.135 +
   3.136 +definition inter :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
   3.137 +  [simp]: "inter A B = Fset (project (member A) (member B))"
   3.138 +
   3.139 +lemma inter_project [code]:
   3.140 +  "inter A B = filter (member A) B"
   3.141 +  by (simp add: inter)
   3.142 +
   3.143 +
   3.144 +subsection {* Functorial operations *}
   3.145 +
   3.146 +definition union :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
   3.147 +  [simp]: "union A B = Fset (member A \<union> member B)"
   3.148 +
   3.149 +lemma union_insert [code]:
   3.150 +  "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
   3.151 +proof -
   3.152 +  have "foldl (\<lambda>A x. Set.insert x A) (member A) xs =
   3.153 +    member (foldl (\<lambda>A x. Fset (Set.insert x (member A))) A xs)"
   3.154 +    by (rule foldl_apply_inv) simp
   3.155 +  then show ?thesis by (simp add: union_set)
   3.156 +qed
   3.157 +
   3.158 +definition subtract :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
   3.159 +  [simp]: "subtract A B = Fset (member B - member A)"
   3.160 +
   3.161 +lemma subtract_remove [code]:
   3.162 +  "subtract (Set xs) A = foldl (\<lambda>A x. remove x A) A xs"
   3.163 +proof -
   3.164 +  have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs =
   3.165 +    member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)"
   3.166 +    by (rule foldl_apply_inv) simp
   3.167 +  then show ?thesis by (simp add: minus_set)
   3.168 +qed
   3.169 +
   3.170 +definition Inter :: "'a fset fset \<Rightarrow> 'a fset" where
   3.171 +  [simp]: "Inter A = Fset (Set.Inter (member ` member A))"
   3.172 +
   3.173 +lemma Inter_inter [code]:
   3.174 +  "Inter (Set (A # As)) = foldl inter A As"
   3.175 +proof -
   3.176 +  note Inter_image_eq [simp del] set_map [simp del] set.simps [simp del]
   3.177 +  have "foldl (op \<inter>) (member A) (List.map member As) = 
   3.178 +    member (foldl (\<lambda>B A. Fset (member B \<inter> A)) A (List.map member As))"
   3.179 +    by (rule foldl_apply_inv) simp
   3.180 +  then show ?thesis
   3.181 +    by (simp add: Inter_set image_set inter_def_raw inter foldl_map)
   3.182 +qed
   3.183 +
   3.184 +definition Union :: "'a fset fset \<Rightarrow> 'a fset" where
   3.185 +  [simp]: "Union A = Fset (Set.Union (member ` member A))"
   3.186 +
   3.187 +lemma Union_union [code]:
   3.188 +  "Union (Set As) = foldl union empty As"
   3.189 +proof -
   3.190 +  note Union_image_eq [simp del] set_map [simp del]
   3.191 +  have "foldl (op \<union>) (member empty) (List.map member As) = 
   3.192 +    member (foldl (\<lambda>B A. Fset (member B \<union> A)) empty (List.map member As))"
   3.193 +    by (rule foldl_apply_inv) simp
   3.194 +  then show ?thesis
   3.195 +    by (simp add: Union_set image_set union_def_raw foldl_map)
   3.196 +qed
   3.197 +
   3.198 +
   3.199 +subsection {* Misc operations *}
   3.200 +
   3.201 +lemma size_fset [code]:
   3.202 +  "fset_size f A = 0"
   3.203 +  "size A = 0"
   3.204 +  by (cases A, simp) (cases A, simp)
   3.205 +
   3.206 +lemma fset_case_code [code]:
   3.207 +  "fset_case f A = f (member A)"
   3.208 +  by (cases A) simp
   3.209 +
   3.210 +lemma fset_rec_code [code]:
   3.211 +  "fset_rec f A = f (member A)"
   3.212 +  by (cases A) simp
   3.213 +
   3.214 +
   3.215 +subsection {* Simplified simprules *}
   3.216 +
   3.217 +lemma is_empty_simp [simp]:
   3.218 +  "is_empty A \<longleftrightarrow> member A = {}"
   3.219 +  by (simp add: List_Set.is_empty_def)
   3.220 +declare is_empty_def [simp del]
   3.221 +
   3.222 +lemma remove_simp [simp]:
   3.223 +  "remove x A = Fset (member A - {x})"
   3.224 +  by (simp add: List_Set.remove_def)
   3.225 +declare remove_def [simp del]
   3.226 +
   3.227 +lemma filter_simp [simp]:
   3.228 +  "filter P A = Fset {x \<in> member A. P x}"
   3.229 +  by (simp add: List_Set.project_def)
   3.230 +declare filter_def [simp del]
   3.231 +
   3.232 +lemma inter_simp [simp]:
   3.233 +  "inter A B = Fset (member A \<inter> member B)"
   3.234 +  by (simp add: inter)
   3.235 +declare inter_def [simp del]
   3.236 +
   3.237 +declare mem_def [simp del]
   3.238 +
   3.239 +
   3.240 +hide (open) const is_empty empty insert remove map filter forall exists card
   3.241 +  subfset_eq subfset inter union subtract Inter Union
   3.242 +
   3.243 +end
     4.1 --- a/src/HOL/Library/Library.thy	Mon Jun 29 12:18:54 2009 +0200
     4.2 +++ b/src/HOL/Library/Library.thy	Mon Jun 29 12:18:55 2009 +0200
     4.3 @@ -10,7 +10,6 @@
     4.4    Char_ord
     4.5    Code_Char_chr
     4.6    Code_Integer
     4.7 -  Code_Set
     4.8    Coinductive_List
     4.9    Commutative_Ring
    4.10    Continuity
    4.11 @@ -28,6 +27,7 @@
    4.12    Formal_Power_Series
    4.13    Fraction_Field
    4.14    FrechetDeriv
    4.15 +  Fset
    4.16    FuncSet
    4.17    Fundamental_Theorem_Algebra
    4.18    Infinite_Set
     5.1 --- a/src/HOL/ex/Codegenerator_Candidates.thy	Mon Jun 29 12:18:54 2009 +0200
     5.2 +++ b/src/HOL/ex/Codegenerator_Candidates.thy	Mon Jun 29 12:18:55 2009 +0200
     5.3 @@ -8,7 +8,7 @@
     5.4    Complex_Main
     5.5    AssocList
     5.6    Binomial
     5.7 -  Code_Set
     5.8 +  Fset
     5.9    Commutative_Ring
    5.10    Enum
    5.11    List_Prefix