2 (* Author: Florian Haftmann, TU Muenchen *)
4 header {* Executable finite sets *}
10 declare mem_def [simp]
12 subsection {* Lifting *}
14 datatype 'a fset = Fset "'a set"
16 primrec member :: "'a fset \<Rightarrow> 'a set" where
19 lemma member_inject [simp]:
20 "member A = member B \<Longrightarrow> A = B"
21 by (cases A, cases B) simp
23 lemma Fset_member [simp]:
27 definition Set :: "'a list \<Rightarrow> 'a fset" where
28 "Set xs = Fset (set xs)"
30 lemma member_Set [simp]:
31 "member (Set xs) = set xs"
32 by (simp add: Set_def)
34 definition Coset :: "'a list \<Rightarrow> 'a fset" where
35 "Coset xs = Fset (- set xs)"
37 lemma member_Coset [simp]:
38 "member (Coset xs) = - set xs"
39 by (simp add: Coset_def)
41 code_datatype Set Coset
43 lemma member_code [code]:
44 "member (Set xs) y \<longleftrightarrow> List.member y xs"
45 "member (Coset xs) y \<longleftrightarrow> \<not> List.member y xs"
46 by (simp_all add: mem_iff fun_Compl_def bool_Compl_def)
48 lemma member_image_UNIV [simp]:
49 "member ` UNIV = UNIV"
51 have "\<And>A \<Colon> 'a set. \<exists>B \<Colon> 'a fset. A = member B"
54 show "A = member (Fset A)" by simp
56 then show ?thesis by (simp add: image_def)
60 subsection {* Lattice instantiation *}
62 instantiation fset :: (type) boolean_algebra
65 definition less_eq_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
66 [simp]: "A \<le> B \<longleftrightarrow> member A \<subseteq> member B"
68 definition less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
69 [simp]: "A < B \<longleftrightarrow> member A \<subset> member B"
71 definition inf_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
72 [simp]: "inf A B = Fset (member A \<inter> member B)"
74 definition sup_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
75 [simp]: "sup A B = Fset (member A \<union> member B)"
77 definition bot_fset :: "'a fset" where
78 [simp]: "bot = Fset {}"
80 definition top_fset :: "'a fset" where
81 [simp]: "top = Fset UNIV"
83 definition uminus_fset :: "'a fset \<Rightarrow> 'a fset" where
84 [simp]: "- A = Fset (- (member A))"
86 definition minus_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
87 [simp]: "A - B = Fset (member A - member B)"
94 instantiation fset :: (type) complete_lattice
97 definition Inf_fset :: "'a fset set \<Rightarrow> 'a fset" where
98 [simp, code del]: "Inf_fset As = Fset (Inf (image member As))"
100 definition Sup_fset :: "'a fset set \<Rightarrow> 'a fset" where
101 [simp, code del]: "Sup_fset As = Fset (Sup (image member As))"
104 qed (auto simp add: le_fun_def le_bool_def)
108 subsection {* Basic operations *}
110 definition is_empty :: "'a fset \<Rightarrow> bool" where
111 [simp]: "is_empty A \<longleftrightarrow> List_Set.is_empty (member A)"
113 lemma is_empty_Set [code]:
114 "is_empty (Set xs) \<longleftrightarrow> null xs"
115 by (simp add: is_empty_set)
117 lemma empty_Set [code]:
121 lemma UNIV_Set [code]:
125 definition insert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
126 [simp]: "insert x A = Fset (Set.insert x (member A))"
128 lemma insert_Set [code]:
129 "insert x (Set xs) = Set (List_Set.insert x xs)"
130 "insert x (Coset xs) = Coset (remove_all x xs)"
131 by (simp_all add: Set_def Coset_def insert_set insert_set_compl)
133 definition remove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
134 [simp]: "remove x A = Fset (List_Set.remove x (member A))"
136 lemma remove_Set [code]:
137 "remove x (Set xs) = Set (remove_all x xs)"
138 "remove x (Coset xs) = Coset (List_Set.insert x xs)"
139 by (simp_all add: Set_def Coset_def remove_set remove_set_compl)
141 definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" where
142 [simp]: "map f A = Fset (image f (member A))"
144 lemma map_Set [code]:
145 "map f (Set xs) = Set (remdups (List.map f xs))"
146 by (simp add: Set_def)
148 definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
149 [simp]: "filter P A = Fset (List_Set.project P (member A))"
151 lemma filter_Set [code]:
152 "filter P (Set xs) = Set (List.filter P xs)"
153 by (simp add: Set_def project_set)
155 definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
156 [simp]: "forall P A \<longleftrightarrow> Ball (member A) P"
158 lemma forall_Set [code]:
159 "forall P (Set xs) \<longleftrightarrow> list_all P xs"
160 by (simp add: Set_def ball_set)
162 definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
163 [simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
165 lemma exists_Set [code]:
166 "exists P (Set xs) \<longleftrightarrow> list_ex P xs"
167 by (simp add: Set_def bex_set)
169 definition card :: "'a fset \<Rightarrow> nat" where
170 [simp]: "card A = Finite_Set.card (member A)"
172 lemma card_Set [code]:
173 "card (Set xs) = length (remdups xs)"
175 have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
176 by (rule distinct_card) simp
177 then show ?thesis by (simp add: Set_def card_def)
181 subsection {* Derived operations *}
183 lemma subfset_eq_forall [code]:
184 "A \<le> B \<longleftrightarrow> forall (member B) A"
185 by (simp add: subset_eq)
187 lemma subfset_subfset_eq [code]:
188 "A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a fset)"
189 by (fact less_le_not_le)
191 lemma eq_fset_subfset_eq [code]:
192 "eq_class.eq A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a fset)"
193 by (cases A, cases B) (simp add: eq set_eq)
196 subsection {* Functorial operations *}
198 lemma inter_project [code]:
199 "inf A (Set xs) = Set (List.filter (member A) xs)"
200 "inf A (Coset xs) = foldl (\<lambda>A x. remove x A) A xs"
202 show "inf A (Set xs) = Set (List.filter (member A) xs)"
203 by (simp add: inter project_def Set_def)
204 have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs =
205 member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)"
206 by (rule foldl_apply_inv) simp
207 then show "inf A (Coset xs) = foldl (\<lambda>A x. remove x A) A xs"
208 by (simp add: Diff_eq [symmetric] minus_set)
211 lemma subtract_remove [code]:
212 "A - Set xs = foldl (\<lambda>A x. remove x A) A xs"
213 "A - Coset xs = Set (List.filter (member A) xs)"
215 have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs =
216 member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)"
217 by (rule foldl_apply_inv) simp
218 then show "A - Set xs = foldl (\<lambda>A x. remove x A) A xs"
219 by (simp add: minus_set)
220 show "A - Coset xs = Set (List.filter (member A) xs)"
221 by (auto simp add: Coset_def Set_def)
224 lemma union_insert [code]:
225 "sup (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
226 "sup (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)"
228 have "foldl (\<lambda>A x. Set.insert x A) (member A) xs =
229 member (foldl (\<lambda>A x. Fset (Set.insert x (member A))) A xs)"
230 by (rule foldl_apply_inv) simp
231 then show "sup (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
232 by (simp add: union_set)
233 show "sup (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)"
234 by (auto simp add: Coset_def)
237 context complete_lattice
240 definition Infimum :: "'a fset \<Rightarrow> 'a" where
241 [simp]: "Infimum A = Inf (member A)"
243 lemma Infimum_inf [code]:
244 "Infimum (Set As) = foldl inf top As"
245 "Infimum (Coset []) = bot"
246 by (simp_all add: Inf_set_fold Inf_UNIV)
248 definition Supremum :: "'a fset \<Rightarrow> 'a" where
249 [simp]: "Supremum A = Sup (member A)"
251 lemma Supremum_sup [code]:
252 "Supremum (Set As) = foldl sup bot As"
253 "Supremum (Coset []) = top"
254 by (simp_all add: Sup_set_fold Sup_UNIV)
259 subsection {* Misc operations *}
261 lemma size_fset [code]:
264 by (cases A, simp) (cases A, simp)
266 lemma fset_case_code [code]:
267 "fset_case f A = f (member A)"
270 lemma fset_rec_code [code]:
271 "fset_rec f A = f (member A)"
275 subsection {* Simplified simprules *}
277 lemma is_empty_simp [simp]:
278 "is_empty A \<longleftrightarrow> member A = {}"
279 by (simp add: List_Set.is_empty_def)
280 declare is_empty_def [simp del]
282 lemma remove_simp [simp]:
283 "remove x A = Fset (member A - {x})"
284 by (simp add: List_Set.remove_def)
285 declare remove_def [simp del]
287 lemma filter_simp [simp]:
288 "filter P A = Fset {x \<in> member A. P x}"
289 by (simp add: List_Set.project_def)
290 declare filter_def [simp del]
292 declare mem_def [simp del]
295 hide (open) const is_empty insert remove map filter forall exists card