171 with insert show P . |
171 with insert show P . |
172 qed |
172 qed |
173 qed |
173 qed |
174 |
174 |
175 |
175 |
176 section {* Functorial structure *} |
176 subsection {* Functorial structure *} |
177 |
177 |
178 enriched_type map: map |
178 enriched_type map: map |
179 by (simp_all add: List.map.id remdups_map_remdups fun_eq_iff dlist_eq_iff) |
179 by (simp_all add: List.map.id remdups_map_remdups fun_eq_iff dlist_eq_iff) |
180 |
180 |
181 |
181 |
182 section {* Implementation of sets by distinct lists -- canonical! *} |
|
183 |
|
184 definition Set :: "'a dlist \<Rightarrow> 'a Cset.set" where |
|
185 "Set dxs = Cset.set (list_of_dlist dxs)" |
|
186 |
|
187 definition Coset :: "'a dlist \<Rightarrow> 'a Cset.set" where |
|
188 "Coset dxs = Cset.coset (list_of_dlist dxs)" |
|
189 |
|
190 code_datatype Set Coset |
|
191 |
|
192 declare member_code [code del] |
|
193 declare Cset.is_empty_set [code del] |
|
194 declare Cset.empty_set [code del] |
|
195 declare Cset.UNIV_set [code del] |
|
196 declare insert_set [code del] |
|
197 declare remove_set [code del] |
|
198 declare compl_set [code del] |
|
199 declare compl_coset [code del] |
|
200 declare map_set [code del] |
|
201 declare filter_set [code del] |
|
202 declare forall_set [code del] |
|
203 declare exists_set [code del] |
|
204 declare card_set [code del] |
|
205 declare inter_project [code del] |
|
206 declare subtract_remove [code del] |
|
207 declare union_insert [code del] |
|
208 declare Infimum_inf [code del] |
|
209 declare Supremum_sup [code del] |
|
210 |
|
211 lemma Set_Dlist [simp]: |
|
212 "Set (Dlist xs) = Cset.Set (set xs)" |
|
213 by (rule Cset.set_eqI) (simp add: Set_def) |
|
214 |
|
215 lemma Coset_Dlist [simp]: |
|
216 "Coset (Dlist xs) = Cset.Set (- set xs)" |
|
217 by (rule Cset.set_eqI) (simp add: Coset_def) |
|
218 |
|
219 lemma member_Set [simp]: |
|
220 "Cset.member (Set dxs) = List.member (list_of_dlist dxs)" |
|
221 by (simp add: Set_def member_set) |
|
222 |
|
223 lemma member_Coset [simp]: |
|
224 "Cset.member (Coset dxs) = Not \<circ> List.member (list_of_dlist dxs)" |
|
225 by (simp add: Coset_def member_set not_set_compl) |
|
226 |
|
227 lemma Set_dlist_of_list [code]: |
|
228 "Cset.set xs = Set (dlist_of_list xs)" |
|
229 by (rule Cset.set_eqI) simp |
|
230 |
|
231 lemma Coset_dlist_of_list [code]: |
|
232 "Cset.coset xs = Coset (dlist_of_list xs)" |
|
233 by (rule Cset.set_eqI) simp |
|
234 |
|
235 lemma is_empty_Set [code]: |
|
236 "Cset.is_empty (Set dxs) \<longleftrightarrow> null dxs" |
|
237 by (simp add: null_def List.null_def member_set) |
|
238 |
|
239 lemma bot_code [code]: |
|
240 "bot = Set empty" |
|
241 by (simp add: empty_def) |
|
242 |
|
243 lemma top_code [code]: |
|
244 "top = Coset empty" |
|
245 by (simp add: empty_def) |
|
246 |
|
247 lemma insert_code [code]: |
|
248 "Cset.insert x (Set dxs) = Set (insert x dxs)" |
|
249 "Cset.insert x (Coset dxs) = Coset (remove x dxs)" |
|
250 by (simp_all add: insert_def remove_def member_set not_set_compl) |
|
251 |
|
252 lemma remove_code [code]: |
|
253 "Cset.remove x (Set dxs) = Set (remove x dxs)" |
|
254 "Cset.remove x (Coset dxs) = Coset (insert x dxs)" |
|
255 by (auto simp add: insert_def remove_def member_set not_set_compl) |
|
256 |
|
257 lemma member_code [code]: |
|
258 "Cset.member (Set dxs) = member dxs" |
|
259 "Cset.member (Coset dxs) = Not \<circ> member dxs" |
|
260 by (simp_all add: member_def) |
|
261 |
|
262 lemma compl_code [code]: |
|
263 "- Set dxs = Coset dxs" |
|
264 "- Coset dxs = Set dxs" |
|
265 by (rule Cset.set_eqI, simp add: member_set not_set_compl)+ |
|
266 |
|
267 lemma map_code [code]: |
|
268 "Cset.map f (Set dxs) = Set (map f dxs)" |
|
269 by (rule Cset.set_eqI) (simp add: member_set) |
|
270 |
|
271 lemma filter_code [code]: |
|
272 "Cset.filter f (Set dxs) = Set (filter f dxs)" |
|
273 by (rule Cset.set_eqI) (simp add: member_set) |
|
274 |
|
275 lemma forall_Set [code]: |
|
276 "Cset.forall P (Set xs) \<longleftrightarrow> list_all P (list_of_dlist xs)" |
|
277 by (simp add: member_set list_all_iff) |
|
278 |
|
279 lemma exists_Set [code]: |
|
280 "Cset.exists P (Set xs) \<longleftrightarrow> list_ex P (list_of_dlist xs)" |
|
281 by (simp add: member_set list_ex_iff) |
|
282 |
|
283 lemma card_code [code]: |
|
284 "Cset.card (Set dxs) = length dxs" |
|
285 by (simp add: length_def member_set distinct_card) |
|
286 |
|
287 lemma inter_code [code]: |
|
288 "inf A (Set xs) = Set (filter (Cset.member A) xs)" |
|
289 "inf A (Coset xs) = foldr Cset.remove xs A" |
|
290 by (simp_all only: Set_def Coset_def foldr_def inter_project list_of_dlist_filter) |
|
291 |
|
292 lemma subtract_code [code]: |
|
293 "A - Set xs = foldr Cset.remove xs A" |
|
294 "A - Coset xs = Set (filter (Cset.member A) xs)" |
|
295 by (simp_all only: Set_def Coset_def foldr_def subtract_remove list_of_dlist_filter) |
|
296 |
|
297 lemma union_code [code]: |
|
298 "sup (Set xs) A = foldr Cset.insert xs A" |
|
299 "sup (Coset xs) A = Coset (filter (Not \<circ> Cset.member A) xs)" |
|
300 by (simp_all only: Set_def Coset_def foldr_def union_insert list_of_dlist_filter) |
|
301 |
|
302 context complete_lattice |
|
303 begin |
|
304 |
|
305 lemma Infimum_code [code]: |
|
306 "Infimum (Set As) = foldr inf As top" |
|
307 by (simp only: Set_def Infimum_inf foldr_def inf.commute) |
|
308 |
|
309 lemma Supremum_code [code]: |
|
310 "Supremum (Set As) = foldr sup As bot" |
|
311 by (simp only: Set_def Supremum_sup foldr_def sup.commute) |
|
312 |
|
313 end |
|
314 |
|
315 |
|
316 hide_const (open) member fold foldr empty insert remove map filter null member length fold |
182 hide_const (open) member fold foldr empty insert remove map filter null member length fold |
317 |
183 |
318 end |
184 end |