64 by simp |
64 by simp |
65 |
65 |
66 section {* Augmenting a set -- @{const finsert} *} |
66 section {* Augmenting a set -- @{const finsert} *} |
67 |
67 |
68 lemma nil_not_cons: |
68 lemma nil_not_cons: |
69 shows "\<not>[] \<approx> x # xs" |
69 shows |
|
70 "\<not>[] \<approx> x # xs" |
|
71 "\<not>x # xs \<approx> []" |
70 by auto |
72 by auto |
71 |
73 |
72 lemma memb_cons_iff: |
74 lemma memb_cons_iff: |
73 shows "memb x (y # xs) = (x = y \<or> memb x xs)" |
75 shows "memb x (y # xs) = (x = y \<or> memb x xs)" |
74 by (induct xs) (auto simp add: memb_def) |
76 by (induct xs) (auto simp add: memb_def) |
130 apply(induct a arbitrary: b) |
132 apply(induct a arbitrary: b) |
131 apply(auto simp add: memb_def) |
133 apply(auto simp add: memb_def) |
132 apply(metis) |
134 apply(metis) |
133 apply(drule_tac x="[x \<leftarrow> b. x \<noteq> a1]" in meta_spec) |
135 apply(drule_tac x="[x \<leftarrow> b. x \<noteq> a1]" in meta_spec) |
134 apply(simp add: fcard_raw_delete_one) |
136 apply(simp add: fcard_raw_delete_one) |
135 apply(metis Suc_pred' fcard_raw_gt_0 fcard_raw_delete_one memb_def) |
137 apply(metis Suc_pred'[OF fcard_raw_gt_0] fcard_raw_delete_one memb_def) |
136 done |
138 done |
137 |
139 |
138 lemma fcard_raw_rsp[quot_respect]: |
140 lemma fcard_raw_rsp[quot_respect]: |
139 "(op \<approx> ===> op =) fcard_raw fcard_raw" |
141 "(op \<approx> ===> op =) fcard_raw fcard_raw" |
140 by (simp add: fcard_raw_rsp_aux) |
142 by (simp add: fcard_raw_rsp_aux) |
251 |
253 |
252 lemma funion_sym_pre: |
254 lemma funion_sym_pre: |
253 "a @ b \<approx> b @ a" |
255 "a @ b \<approx> b @ a" |
254 by auto |
256 by auto |
255 |
257 |
256 |
|
257 lemma append_rsp[quot_respect]: |
258 lemma append_rsp[quot_respect]: |
258 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @" |
259 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @" |
259 by (auto) |
260 by (auto) |
|
261 |
|
262 lemma set_cong: "(set x = set y) = (x \<approx> y)" |
|
263 apply rule |
|
264 apply simp_all |
|
265 apply (induct x y rule: list_induct2') |
|
266 apply simp_all |
|
267 apply auto |
|
268 done |
|
269 |
|
270 lemma inj_map_eq_iff: |
|
271 "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)" |
|
272 by (simp add: expand_set_eq[symmetric] inj_image_eq_iff) |
|
273 |
260 |
274 |
261 |
275 |
262 |
276 |
263 section {* lifted part *} |
277 section {* lifted part *} |
264 |
278 |
275 lemma finsert_absorb[simp]: |
289 lemma finsert_absorb[simp]: |
276 shows "x |\<in>| S \<Longrightarrow> finsert x S = S" |
290 shows "x |\<in>| S \<Longrightarrow> finsert x S = S" |
277 by (lifting memb_absorb) |
291 by (lifting memb_absorb) |
278 |
292 |
279 lemma fempty_not_finsert[simp]: |
293 lemma fempty_not_finsert[simp]: |
280 shows "{||} \<noteq> finsert x S" |
294 "{||} \<noteq> finsert x S" |
|
295 "finsert x S \<noteq> {||}" |
281 by (lifting nil_not_cons) |
296 by (lifting nil_not_cons) |
282 |
297 |
283 lemma finsert_left_comm: |
298 lemma finsert_left_comm: |
284 "finsert a (finsert b S) = finsert b (finsert a S)" |
299 "finsert a (finsert b S) = finsert b (finsert a S)" |
285 by (lifting cons_left_comm) |
300 by (lifting cons_left_comm) |
292 shows "{|x|} = {|y|} \<longleftrightarrow> x = y" |
307 shows "{|x|} = {|y|} \<longleftrightarrow> x = y" |
293 by (lifting singleton_list_eq) |
308 by (lifting singleton_list_eq) |
294 |
309 |
295 text {* fset_to_set *} |
310 text {* fset_to_set *} |
296 |
311 |
297 lemma fset_to_set_simps: |
312 lemma fset_to_set_simps[simp]: |
298 "fset_to_set {||} = {}" |
313 "fset_to_set {||} = {}" |
299 "fset_to_set (finsert (h :: 'b) t) = insert h (fset_to_set t)" |
314 "fset_to_set (finsert (h :: 'b) t) = insert h (fset_to_set t)" |
300 by (lifting list2set_thm) |
315 by (lifting list2set_thm) |
301 |
316 |
302 lemma in_fset_to_set: |
317 lemma in_fset_to_set: |
304 by (lifting memb_def[symmetric]) |
319 by (lifting memb_def[symmetric]) |
305 |
320 |
306 lemma none_in_fempty: |
321 lemma none_in_fempty: |
307 "(\<forall>a. a \<notin> fset_to_set A) = (A = {||})" |
322 "(\<forall>a. a \<notin> fset_to_set A) = (A = {||})" |
308 by (lifting none_mem_nil) |
323 by (lifting none_mem_nil) |
|
324 |
|
325 lemma fset_cong: |
|
326 "(fset_to_set x = fset_to_set y) = (x = y)" |
|
327 by (lifting set_cong) |
309 |
328 |
310 text {* fcard *} |
329 text {* fcard *} |
311 |
330 |
312 lemma fcard_fempty [simp]: |
331 lemma fcard_fempty [simp]: |
313 shows "fcard {||} = 0" |
332 shows "fcard {||} = 0" |
343 |
362 |
344 lemma fset_exhaust[case_names fempty finsert, cases type: fset]: |
363 lemma fset_exhaust[case_names fempty finsert, cases type: fset]: |
345 shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" |
364 shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" |
346 by (lifting list.exhaust) |
365 by (lifting list.exhaust) |
347 |
366 |
348 lemma fset_induct[case_names fempty finsert]: |
367 lemma fset_induct_weak[case_names fempty finsert]: |
349 shows "\<lbrakk>P {||}; \<And>x S. P S \<Longrightarrow> P (finsert x S)\<rbrakk> \<Longrightarrow> P S" |
368 shows "\<lbrakk>P {||}; \<And>x S. P S \<Longrightarrow> P (finsert x S)\<rbrakk> \<Longrightarrow> P S" |
350 by (lifting list.induct) |
369 by (lifting list.induct) |
351 |
370 |
352 lemma fset_induct2[case_names fempty finsert, induct type: fset]: |
371 lemma fset_induct[case_names fempty finsert, induct type: fset]: |
353 assumes prem1: "P {||}" |
372 assumes prem1: "P {||}" |
354 and prem2: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (finsert x S)" |
373 and prem2: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (finsert x S)" |
355 shows "P S" |
374 shows "P S" |
356 proof(induct S rule: fset_induct) |
375 proof(induct S rule: fset_induct_weak) |
357 case fempty |
376 case fempty |
358 show "P {||}" by (rule prem1) |
377 show "P {||}" by (rule prem1) |
359 next |
378 next |
360 case (finsert x S) |
379 case (finsert x S) |
361 have asm: "P S" by fact |
380 have asm: "P S" by fact |
369 have "x |\<notin>| S" by fact |
388 have "x |\<notin>| S" by fact |
370 then show "P (finsert x S)" using prem2 asm by simp |
389 then show "P (finsert x S)" using prem2 asm by simp |
371 qed |
390 qed |
372 qed |
391 qed |
373 |
392 |
374 |
393 lemma fset_induct2: |
|
394 "P {||} {||} \<Longrightarrow> |
|
395 (\<And>x xs. x |\<notin>| xs \<Longrightarrow> P (finsert x xs) {||}) \<Longrightarrow> |
|
396 (\<And>y ys. y |\<notin>| ys \<Longrightarrow> P {||} (finsert y ys)) \<Longrightarrow> |
|
397 (\<And>x xs y ys. \<lbrakk>P xs ys; x |\<notin>| xs; y |\<notin>| ys\<rbrakk> \<Longrightarrow> P (finsert x xs) (finsert y ys)) \<Longrightarrow> |
|
398 P xsa ysa" |
|
399 apply (induct xsa arbitrary: ysa) |
|
400 apply (induct_tac x rule: fset_induct) |
|
401 apply simp_all |
|
402 apply (induct_tac xa rule: fset_induct) |
|
403 apply simp_all |
|
404 done |
|
405 |
|
406 (* fmap *) |
|
407 lemma fmap_simps[simp]: |
|
408 "fmap (f :: 'a \<Rightarrow> 'b) {||} = {||}" |
|
409 "fmap f (finsert x xs) = finsert (f x) (fmap f xs)" |
|
410 by (lifting map.simps) |
|
411 |
|
412 lemma fmap_set_image: |
|
413 "fset_to_set (fmap f fs) = f ` (fset_to_set fs)" |
|
414 apply (induct fs) |
|
415 apply (simp_all) |
|
416 done |
|
417 |
|
418 lemma inj_fmap_eq_iff: |
|
419 "inj f \<Longrightarrow> (fmap f l = fmap f m) = (l = m)" |
|
420 by (lifting inj_map_eq_iff) |
|
421 |
|
422 ML {* |
|
423 fun dest_fsetT (Type ("FSet.fset", [T])) = T |
|
424 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
|
425 *} |
375 |
426 |
376 end |
427 end |