68 | "ffold_raw f z (a # A) = |
68 | "ffold_raw f z (a # A) = |
69 (if (rsp_fold f) then |
69 (if (rsp_fold f) then |
70 if memb a A then ffold_raw f z A |
70 if memb a A then ffold_raw f z A |
71 else f a (ffold_raw f z A) |
71 else f a (ffold_raw f z A) |
72 else z)" |
72 else z)" |
|
73 |
|
74 text {* Composition Quotient *} |
|
75 |
|
76 lemma list_rel_refl: |
|
77 shows "(list_rel op \<approx>) r r" |
|
78 by (rule list_rel_refl) (metis equivp_def fset_equivp) |
|
79 |
|
80 lemma compose_list_refl: |
|
81 shows "(list_rel op \<approx> OOO op \<approx>) r r" |
|
82 proof |
|
83 show c: "list_rel op \<approx> r r" by (rule list_rel_refl) |
|
84 have d: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp]) |
|
85 show b: "(op \<approx> OO list_rel op \<approx>) r r" by (rule pred_compI) (rule d, rule c) |
|
86 qed |
|
87 |
|
88 lemma Quotient_fset_list: |
|
89 shows "Quotient (list_rel op \<approx>) (map abs_fset) (map rep_fset)" |
|
90 by (fact list_quotient[OF Quotient_fset]) |
|
91 |
|
92 lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B" |
|
93 by (rule eq_reflection) auto |
|
94 |
|
95 lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba" |
|
96 unfolding list_eq.simps |
|
97 by (simp only: set_map set_in_eq) |
|
98 |
|
99 lemma quotient_compose_list[quot_thm]: |
|
100 shows "Quotient ((list_rel op \<approx>) OOO (op \<approx>)) |
|
101 (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)" |
|
102 unfolding Quotient_def comp_def |
|
103 proof (intro conjI allI) |
|
104 fix a r s |
|
105 show "abs_fset (map abs_fset (map rep_fset (rep_fset a))) = a" |
|
106 by (simp add: abs_o_rep[OF Quotient_fset] Quotient_abs_rep[OF Quotient_fset] map_id) |
|
107 have b: "list_rel op \<approx> (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))" |
|
108 by (rule list_rel_refl) |
|
109 have c: "(op \<approx> OO list_rel op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))" |
|
110 by (rule, rule equivp_reflp[OF fset_equivp]) (rule b) |
|
111 show "(list_rel op \<approx> OOO op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))" |
|
112 by (rule, rule list_rel_refl) (rule c) |
|
113 show "(list_rel op \<approx> OOO op \<approx>) r s = ((list_rel op \<approx> OOO op \<approx>) r r \<and> |
|
114 (list_rel op \<approx> OOO op \<approx>) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))" |
|
115 proof (intro iffI conjI) |
|
116 show "(list_rel op \<approx> OOO op \<approx>) r r" by (rule compose_list_refl) |
|
117 show "(list_rel op \<approx> OOO op \<approx>) s s" by (rule compose_list_refl) |
|
118 next |
|
119 assume a: "(list_rel op \<approx> OOO op \<approx>) r s" |
|
120 then have b: "map abs_fset r \<approx> map abs_fset s" proof (elim pred_compE) |
|
121 fix b ba |
|
122 assume c: "list_rel op \<approx> r b" |
|
123 assume d: "b \<approx> ba" |
|
124 assume e: "list_rel op \<approx> ba s" |
|
125 have f: "map abs_fset r = map abs_fset b" |
|
126 using Quotient_rel[OF Quotient_fset_list] c by blast |
|
127 have "map abs_fset ba = map abs_fset s" |
|
128 using Quotient_rel[OF Quotient_fset_list] e by blast |
|
129 then have g: "map abs_fset s = map abs_fset ba" by simp |
|
130 then show "map abs_fset r \<approx> map abs_fset s" using d f map_rel_cong by simp |
|
131 qed |
|
132 then show "abs_fset (map abs_fset r) = abs_fset (map abs_fset s)" |
|
133 using Quotient_rel[OF Quotient_fset] by blast |
|
134 next |
|
135 assume a: "(list_rel op \<approx> OOO op \<approx>) r r \<and> (list_rel op \<approx> OOO op \<approx>) s s |
|
136 \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s)" |
|
137 then have s: "(list_rel op \<approx> OOO op \<approx>) s s" by simp |
|
138 have d: "map abs_fset r \<approx> map abs_fset s" |
|
139 by (subst Quotient_rel[OF Quotient_fset]) (simp add: a) |
|
140 have b: "map rep_fset (map abs_fset r) \<approx> map rep_fset (map abs_fset s)" |
|
141 by (rule map_rel_cong[OF d]) |
|
142 have y: "list_rel op \<approx> (map rep_fset (map abs_fset s)) s" |
|
143 by (fact rep_abs_rsp_left[OF Quotient_fset_list, OF list_rel_refl[of s]]) |
|
144 have c: "(op \<approx> OO list_rel op \<approx>) (map rep_fset (map abs_fset r)) s" |
|
145 by (rule pred_compI) (rule b, rule y) |
|
146 have z: "list_rel op \<approx> r (map rep_fset (map abs_fset r))" |
|
147 by (fact rep_abs_rsp[OF Quotient_fset_list, OF list_rel_refl[of r]]) |
|
148 then show "(list_rel op \<approx> OOO op \<approx>) r s" |
|
149 using a c pred_compI by simp |
|
150 qed |
|
151 qed |
73 |
152 |
74 text {* Respectfullness *} |
153 text {* Respectfullness *} |
75 |
154 |
76 lemma [quot_respect]: |
155 lemma [quot_respect]: |
77 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @" |
156 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @" |
214 done |
293 done |
215 |
294 |
216 lemma [quot_respect]: |
295 lemma [quot_respect]: |
217 "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw" |
296 "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw" |
218 by (simp add: memb_def[symmetric] ffold_raw_rsp_pre) |
297 by (simp add: memb_def[symmetric] ffold_raw_rsp_pre) |
|
298 |
|
299 lemma concat_rsp_pre: |
|
300 assumes a: "list_rel op \<approx> x x'" |
|
301 and b: "x' \<approx> y'" |
|
302 and c: "list_rel op \<approx> y' y" |
|
303 and d: "\<exists>x\<in>set x. xa \<in> set x" |
|
304 shows "\<exists>x\<in>set y. xa \<in> set x" |
|
305 proof - |
|
306 obtain xb where e: "xb \<in> set x" and f: "xa \<in> set xb" using d by auto |
|
307 have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_rel_find_element[OF e a]) |
|
308 then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto |
|
309 have j: "ya \<in> set y'" using b h by simp |
|
310 have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" by (rule list_rel_find_element[OF j c]) |
|
311 then show ?thesis using f i by auto |
|
312 qed |
|
313 |
|
314 lemma [quot_respect]: |
|
315 shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat" |
|
316 proof (rule fun_relI, elim pred_compE) |
|
317 fix a b ba bb |
|
318 assume a: "list_rel op \<approx> a ba" |
|
319 assume b: "ba \<approx> bb" |
|
320 assume c: "list_rel op \<approx> bb b" |
|
321 have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof |
|
322 fix x |
|
323 show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof |
|
324 assume d: "\<exists>xa\<in>set a. x \<in> set xa" |
|
325 show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d]) |
|
326 next |
|
327 assume e: "\<exists>xa\<in>set b. x \<in> set xa" |
|
328 have a': "list_rel op \<approx> ba a" by (rule list_rel_symp[OF list_eq_equivp, OF a]) |
|
329 have b': "bb \<approx> ba" by (rule equivp_symp[OF list_eq_equivp, OF b]) |
|
330 have c': "list_rel op \<approx> b bb" by (rule list_rel_symp[OF list_eq_equivp, OF c]) |
|
331 show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e]) |
|
332 qed |
|
333 qed |
|
334 then show "concat a \<approx> concat b" by simp |
|
335 qed |
219 |
336 |
220 text {* Distributive lattice with bot *} |
337 text {* Distributive lattice with bot *} |
221 |
338 |
222 lemma sub_list_not_eq: |
339 lemma sub_list_not_eq: |
223 "(sub_list x y \<and> \<not> list_eq x y) = (sub_list x y \<and> \<not> sub_list y x)" |
340 "(sub_list x y \<and> \<not> list_eq x y) = (sub_list x y \<and> \<not> sub_list y x)" |
373 fin (infix "|\<in>|" 50) |
490 fin (infix "|\<in>|" 50) |
374 where |
491 where |
375 "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb" |
492 "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb" |
376 |
493 |
377 abbreviation |
494 abbreviation |
378 fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50) |
495 fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) |
379 where |
496 where |
380 "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)" |
497 "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)" |
381 |
498 |
382 section {* Augmenting an fset -- @{const finsert} *} |
499 section {* Other constants on the Quotient Type *} |
|
500 |
|
501 quotient_definition |
|
502 "fcard :: 'a fset \<Rightarrow> nat" |
|
503 is |
|
504 "fcard_raw" |
|
505 |
|
506 quotient_definition |
|
507 "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
|
508 is |
|
509 "map" |
|
510 |
|
511 quotient_definition |
|
512 "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" |
|
513 is "delete_raw" |
|
514 |
|
515 quotient_definition |
|
516 "fset_to_set :: 'a fset \<Rightarrow> 'a set" |
|
517 is "set" |
|
518 |
|
519 quotient_definition |
|
520 "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" |
|
521 is "ffold_raw" |
|
522 |
|
523 quotient_definition |
|
524 "fconcat :: ('a fset) fset \<Rightarrow> 'a fset" |
|
525 is |
|
526 "concat" |
|
527 |
|
528 text {* Compositional Respectfullness and Preservation *} |
|
529 |
|
530 lemma [quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []" |
|
531 by (fact compose_list_refl) |
|
532 |
|
533 lemma [quot_preserve]: "(abs_fset \<circ> map f) [] = abs_fset []" |
|
534 by simp |
|
535 |
|
536 lemma [quot_respect]: |
|
537 "(op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op # op #" |
|
538 apply auto |
|
539 apply (simp add: set_in_eq) |
|
540 apply (rule_tac b="x # b" in pred_compI) |
|
541 apply auto |
|
542 apply (rule_tac b="x # ba" in pred_compI) |
|
543 apply auto |
|
544 done |
|
545 |
|
546 lemma [quot_preserve]: |
|
547 "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert" |
|
548 by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset] |
|
549 abs_o_rep[OF Quotient_fset] map_id finsert_def) |
|
550 |
|
551 lemma [quot_preserve]: |
|
552 "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op @ = funion" |
|
553 by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset] |
|
554 abs_o_rep[OF Quotient_fset] map_id sup_fset_def) |
|
555 |
|
556 lemma list_rel_app_l: |
|
557 assumes a: "reflp R" |
|
558 and b: "list_rel R l r" |
|
559 shows "list_rel R (z @ l) (z @ r)" |
|
560 by (induct z) (simp_all add: b rev_iffD1[OF a meta_eq_to_obj_eq[OF reflp_def]]) |
|
561 |
|
562 lemma append_rsp2_pre0: |
|
563 assumes a:"list_rel op \<approx> x x'" |
|
564 shows "list_rel op \<approx> (x @ z) (x' @ z)" |
|
565 using a apply (induct x x' rule: list_induct2') |
|
566 by simp_all (rule list_rel_refl) |
|
567 |
|
568 lemma append_rsp2_pre1: |
|
569 assumes a:"list_rel op \<approx> x x'" |
|
570 shows "list_rel op \<approx> (z @ x) (z @ x')" |
|
571 using a apply (induct x x' arbitrary: z rule: list_induct2') |
|
572 apply (rule list_rel_refl) |
|
573 apply (simp_all del: list_eq.simps) |
|
574 apply (rule list_rel_app_l) |
|
575 apply (simp_all add: reflp_def) |
|
576 done |
|
577 |
|
578 lemma append_rsp2_pre: |
|
579 assumes a:"list_rel op \<approx> x x'" |
|
580 and b: "list_rel op \<approx> z z'" |
|
581 shows "list_rel op \<approx> (x @ z) (x' @ z')" |
|
582 apply (rule list_rel_transp[OF fset_equivp]) |
|
583 apply (rule append_rsp2_pre0) |
|
584 apply (rule a) |
|
585 using b apply (induct z z' rule: list_induct2') |
|
586 apply (simp_all only: append_Nil2) |
|
587 apply (rule list_rel_refl) |
|
588 apply simp_all |
|
589 apply (rule append_rsp2_pre1) |
|
590 apply simp |
|
591 done |
|
592 |
|
593 lemma [quot_respect]: |
|
594 "(list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op @ op @" |
|
595 proof (intro fun_relI, elim pred_compE) |
|
596 fix x y z w x' z' y' w' :: "'a list list" |
|
597 assume a:"list_rel op \<approx> x x'" |
|
598 and b: "x' \<approx> y'" |
|
599 and c: "list_rel op \<approx> y' y" |
|
600 assume aa: "list_rel op \<approx> z z'" |
|
601 and bb: "z' \<approx> w'" |
|
602 and cc: "list_rel op \<approx> w' w" |
|
603 have a': "list_rel op \<approx> (x @ z) (x' @ z')" using a aa append_rsp2_pre by auto |
|
604 have b': "x' @ z' \<approx> y' @ w'" using b bb by simp |
|
605 have c': "list_rel op \<approx> (y' @ w') (y @ w)" using c cc append_rsp2_pre by auto |
|
606 have d': "(op \<approx> OO list_rel op \<approx>) (x' @ z') (y @ w)" |
|
607 by (rule pred_compI) (rule b', rule c') |
|
608 show "(list_rel op \<approx> OOO op \<approx>) (x @ z) (y @ w)" |
|
609 by (rule pred_compI) (rule a', rule d') |
|
610 qed |
|
611 |
|
612 text {* Raw theorems. Finsert, memb, singleron, sub_list *} |
383 |
613 |
384 lemma nil_not_cons: |
614 lemma nil_not_cons: |
385 shows "\<not> ([] \<approx> x # xs)" |
615 shows "\<not> ([] \<approx> x # xs)" |
386 and "\<not> (x # xs \<approx> [])" |
616 and "\<not> (x # xs \<approx> [])" |
387 by auto |
617 by auto |
396 |
626 |
397 lemma memb_consI2: |
627 lemma memb_consI2: |
398 shows "memb x xs \<Longrightarrow> memb x (y # xs)" |
628 shows "memb x xs \<Longrightarrow> memb x (y # xs)" |
399 by (simp add: memb_def) |
629 by (simp add: memb_def) |
400 |
630 |
401 section {* Singletons *} |
|
402 |
|
403 lemma singleton_list_eq: |
631 lemma singleton_list_eq: |
404 shows "[x] \<approx> [y] \<longleftrightarrow> x = y" |
632 shows "[x] \<approx> [y] \<longleftrightarrow> x = y" |
405 by (simp add: id_simps) auto |
633 by (simp add: id_simps) auto |
406 |
634 |
407 section {* sub_list *} |
|
408 |
|
409 lemma sub_list_cons: |
635 lemma sub_list_cons: |
410 "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)" |
636 "sub_list (x # xs) ys = (memb x ys \<and> sub_list xs ys)" |
411 by (auto simp add: memb_def sub_list_def) |
637 by (auto simp add: memb_def sub_list_def) |
412 |
638 |
413 section {* Cardinality of finite sets *} |
639 text {* Cardinality of finite sets *} |
414 |
|
415 quotient_definition |
|
416 "fcard :: 'a fset \<Rightarrow> nat" |
|
417 is |
|
418 "fcard_raw" |
|
419 |
640 |
420 lemma fcard_raw_0: |
641 lemma fcard_raw_0: |
421 shows "fcard_raw xs = 0 \<longleftrightarrow> xs \<approx> []" |
642 shows "fcard_raw xs = 0 \<longleftrightarrow> xs \<approx> []" |
422 by (induct xs) (auto simp add: memb_def) |
643 by (induct xs) (auto simp add: memb_def) |
423 |
|
424 |
644 |
425 lemma fcard_raw_not_memb: |
645 lemma fcard_raw_not_memb: |
426 shows "\<not> memb x xs \<longleftrightarrow> fcard_raw (x # xs) = Suc (fcard_raw xs)" |
646 shows "\<not> memb x xs \<longleftrightarrow> fcard_raw (x # xs) = Suc (fcard_raw xs)" |
427 by auto |
647 by auto |
428 |
648 |
449 |
669 |
450 lemma fcard_raw_suc_memb: |
670 lemma fcard_raw_suc_memb: |
451 assumes a: "fcard_raw A = Suc n" |
671 assumes a: "fcard_raw A = Suc n" |
452 shows "\<exists>a. memb a A" |
672 shows "\<exists>a. memb a A" |
453 using a |
673 using a |
454 apply (induct A) |
674 by (induct A) (auto simp add: memb_def) |
455 apply simp |
|
456 apply (rule_tac x="a" in exI) |
|
457 apply (simp add: memb_def) |
|
458 done |
|
459 |
675 |
460 lemma memb_card_not_0: |
676 lemma memb_card_not_0: |
461 assumes a: "memb a A" |
677 assumes a: "memb a A" |
462 shows "\<not>(fcard_raw A = 0)" |
678 shows "\<not>(fcard_raw A = 0)" |
463 proof - |
679 proof - |
464 have "\<not>(\<forall>x. \<not> memb x A)" using a by auto |
680 have "\<not>(\<forall>x. \<not> memb x A)" using a by auto |
465 then have "\<not>A \<approx> []" using none_memb_nil[of A] by simp |
681 then have "\<not>A \<approx> []" using none_memb_nil[of A] by simp |
466 then show ?thesis using fcard_raw_0[of A] by simp |
682 then show ?thesis using fcard_raw_0[of A] by simp |
467 qed |
683 qed |
468 |
684 |
469 section {* fmap *} |
685 text {* fmap *} |
470 |
|
471 quotient_definition |
|
472 "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
|
473 is |
|
474 "map" |
|
475 |
686 |
476 lemma map_append: |
687 lemma map_append: |
477 "map f (xs @ ys) \<approx> (map f xs) @ (map f ys)" |
688 "map f (xs @ ys) \<approx> (map f xs) @ (map f ys)" |
478 by simp |
689 by simp |
479 |
690 |
524 |
735 |
525 lemma fcard_raw_delete: |
736 lemma fcard_raw_delete: |
526 "fcard_raw (delete_raw xs y) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)" |
737 "fcard_raw (delete_raw xs y) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)" |
527 by (simp add: fdelete_raw_filter fcard_raw_delete_one) |
738 by (simp add: fdelete_raw_filter fcard_raw_delete_one) |
528 |
739 |
529 |
|
530 |
|
531 |
|
532 |
|
533 lemma finter_raw_empty: |
740 lemma finter_raw_empty: |
534 "finter_raw l [] = []" |
741 "finter_raw l [] = []" |
535 by (induct l) (simp_all add: not_memb_nil) |
742 by (induct l) (simp_all add: not_memb_nil) |
536 |
743 |
537 section {* Constants on the Quotient Type *} |
|
538 |
|
539 quotient_definition |
|
540 "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" |
|
541 is "delete_raw" |
|
542 |
|
543 quotient_definition |
|
544 "fset_to_set :: 'a fset \<Rightarrow> 'a set" |
|
545 is "set" |
|
546 |
|
547 quotient_definition |
|
548 "ffold :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" |
|
549 is "ffold_raw" |
|
550 |
|
551 lemma set_cong: |
744 lemma set_cong: |
552 shows "(set x = set y) = (x \<approx> y)" |
745 shows "(set x = set y) = (x \<approx> y)" |
553 by auto |
746 by auto |
554 |
747 |
555 lemma inj_map_eq_iff: |
748 lemma inj_map_eq_iff: |
556 "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)" |
749 "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)" |
557 by (simp add: expand_set_eq[symmetric] inj_image_eq_iff) |
750 by (simp add: expand_set_eq[symmetric] inj_image_eq_iff) |
558 |
|
559 quotient_definition |
|
560 "fconcat :: ('a fset) fset \<Rightarrow> 'a fset" |
|
561 is |
|
562 "concat" |
|
563 |
|
564 |
751 |
565 text {* alternate formulation with a different decomposition principle |
752 text {* alternate formulation with a different decomposition principle |
566 and a proof of equivalence *} |
753 and a proof of equivalence *} |
567 |
754 |
568 inductive |
755 inductive |
602 |
789 |
603 lemma delete_raw_rsp: |
790 lemma delete_raw_rsp: |
604 "xs \<approx> ys \<Longrightarrow> delete_raw xs x \<approx> delete_raw ys x" |
791 "xs \<approx> ys \<Longrightarrow> delete_raw xs x \<approx> delete_raw ys x" |
605 by (simp add: memb_def[symmetric] memb_delete_raw) |
792 by (simp add: memb_def[symmetric] memb_delete_raw) |
606 |
793 |
607 lemma list_eq2_equiv_aux: |
|
608 assumes a: "fcard_raw l = n" |
|
609 and b: "l \<approx> r" |
|
610 shows "list_eq2 l r" |
|
611 using a b |
|
612 proof (induct n arbitrary: l r) |
|
613 case 0 |
|
614 have "fcard_raw l = 0" by fact |
|
615 then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto |
|
616 then have z: "l = []" using no_memb_nil by auto |
|
617 then have "r = []" using `l \<approx> r` by simp |
|
618 then show ?case using z list_eq2_refl by simp |
|
619 next |
|
620 case (Suc m) |
|
621 have b: "l \<approx> r" by fact |
|
622 have d: "fcard_raw l = Suc m" by fact |
|
623 have "\<exists>a. memb a l" by (rule fcard_raw_suc_memb[OF d]) |
|
624 then obtain a where e: "memb a l" by auto |
|
625 then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b by auto |
|
626 have f: "fcard_raw (delete_raw l a) = m" using fcard_raw_delete[of l a] e d by simp |
|
627 have g: "delete_raw l a \<approx> delete_raw r a" using delete_raw_rsp[OF b] by simp |
|
628 have g': "list_eq2 (delete_raw l a) (delete_raw r a)" by (rule Suc.hyps[OF f g]) |
|
629 have h: "list_eq2 (a # delete_raw l a) (a # delete_raw r a)" by (rule list_eq2.intros(5)[OF g']) |
|
630 have i: "list_eq2 l (a # delete_raw l a)" by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]]) |
|
631 have "list_eq2 l (a # delete_raw r a)" by (rule list_eq2.intros(6)[OF i h]) |
|
632 then show ?case using list_eq2.intros(6)[OF _ memb_delete_list_eq2[OF e']] by simp |
|
633 qed |
|
634 |
|
635 lemma list_eq2_equiv: |
794 lemma list_eq2_equiv: |
636 "(l \<approx> r) \<longleftrightarrow> (list_eq2 l r)" |
795 "(l \<approx> r) \<longleftrightarrow> (list_eq2 l r)" |
637 proof |
796 proof |
638 show "list_eq2 l r \<Longrightarrow> l \<approx> r" by (induct rule: list_eq2.induct) auto |
797 show "list_eq2 l r \<Longrightarrow> l \<approx> r" by (induct rule: list_eq2.induct) auto |
639 show "l \<approx> r \<Longrightarrow> list_eq2 l r" using list_eq2_equiv_aux by blast |
798 next |
|
799 { |
|
800 fix n |
|
801 assume a: "fcard_raw l = n" and b: "l \<approx> r" |
|
802 have "list_eq2 l r" |
|
803 using a b |
|
804 proof (induct n arbitrary: l r) |
|
805 case 0 |
|
806 have "fcard_raw l = 0" by fact |
|
807 then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto |
|
808 then have z: "l = []" using no_memb_nil by auto |
|
809 then have "r = []" using `l \<approx> r` by simp |
|
810 then show ?case using z list_eq2_refl by simp |
|
811 next |
|
812 case (Suc m) |
|
813 have b: "l \<approx> r" by fact |
|
814 have d: "fcard_raw l = Suc m" by fact |
|
815 have "\<exists>a. memb a l" by (rule fcard_raw_suc_memb[OF d]) |
|
816 then obtain a where e: "memb a l" by auto |
|
817 then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b by auto |
|
818 have f: "fcard_raw (delete_raw l a) = m" using fcard_raw_delete[of l a] e d by simp |
|
819 have g: "delete_raw l a \<approx> delete_raw r a" using delete_raw_rsp[OF b] by simp |
|
820 have g': "list_eq2 (delete_raw l a) (delete_raw r a)" by (rule Suc.hyps[OF f g]) |
|
821 have h: "list_eq2 (a # delete_raw l a) (a # delete_raw r a)" by (rule list_eq2.intros(5)[OF g']) |
|
822 have i: "list_eq2 l (a # delete_raw l a)" |
|
823 by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]]) |
|
824 have "list_eq2 l (a # delete_raw r a)" by (rule list_eq2.intros(6)[OF i h]) |
|
825 then show ?case using list_eq2.intros(6)[OF _ memb_delete_list_eq2[OF e']] by simp |
|
826 qed |
|
827 } |
|
828 then show "l \<approx> r \<Longrightarrow> list_eq2 l r" by blast |
640 qed |
829 qed |
641 |
830 |
642 section {* lifted part *} |
831 text {* Lifted theorems *} |
643 |
832 |
644 lemma not_fin_fnil: "x |\<notin>| {||}" |
833 lemma not_fin_fnil: "x |\<notin>| {||}" |
645 by (lifting not_memb_nil) |
834 by (lifting not_memb_nil) |
646 |
835 |
647 lemma fin_finsert_iff[simp]: |
836 lemma fin_finsert_iff[simp]: |
909 and "\<And>xs1 xs2 xs3. \<lbrakk>xs1 = xs2; P xs1 xs2; xs2 = xs3; P xs2 xs3\<rbrakk> \<Longrightarrow> P xs1 xs3" |
1087 and "\<And>xs1 xs2 xs3. \<lbrakk>xs1 = xs2; P xs1 xs2; xs2 = xs3; P xs2 xs3\<rbrakk> \<Longrightarrow> P xs1 xs3" |
910 shows "P x1 x2" |
1088 shows "P x1 x2" |
911 using assms |
1089 using assms |
912 by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]]) |
1090 by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]]) |
913 |
1091 |
|
1092 text {* concat *} |
|
1093 |
|
1094 lemma fconcat_empty: |
|
1095 shows "fconcat {||} = {||}" |
|
1096 by (lifting concat.simps(1)) |
|
1097 |
|
1098 lemma fconcat_insert: |
|
1099 shows "fconcat (finsert x S) = x |\<union>| fconcat S" |
|
1100 by (lifting concat.simps(2)) |
|
1101 |
|
1102 lemma "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys" |
|
1103 by (lifting concat_append) |
|
1104 |
914 ML {* |
1105 ML {* |
915 fun dest_fsetT (Type ("FSet.fset", [T])) = T |
1106 fun dest_fsetT (Type ("FSet.fset", [T])) = T |
916 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
1107 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
917 *} |
1108 *} |
918 |
1109 |