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 |
73 |
74 text {* Composition Quotient *} |
74 text {* Composition Quotient *} |
75 |
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 |
76 lemma compose_list_refl: |
80 lemma compose_list_refl: |
77 shows "(list_rel op \<approx> OOO op \<approx>) r r" |
81 shows "(list_rel op \<approx> OOO op \<approx>) r r" |
78 proof |
82 proof |
79 show c: "list_rel op \<approx> r r" by (rule list_rel_refl) (metis equivp_def fset_equivp) |
83 show c: "list_rel op \<approx> r r" by (rule list_rel_refl) |
80 have d: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp]) |
84 have d: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp]) |
81 show b: "(op \<approx> OO list_rel op \<approx>) r r" by (rule pred_compI) (rule d, rule c) |
85 show b: "(op \<approx> OO list_rel op \<approx>) r r" by (rule pred_compI) (rule d, rule c) |
82 qed |
86 qed |
83 |
|
84 lemma list_rel_refl: |
|
85 shows "(list_rel op \<approx>) r r" |
|
86 by (rule list_rel_refl)(metis equivp_def fset_equivp) |
|
87 |
87 |
88 lemma Quotient_fset_list: |
88 lemma Quotient_fset_list: |
89 shows "Quotient (list_rel op \<approx>) (map abs_fset) (map rep_fset)" |
89 shows "Quotient (list_rel op \<approx>) (map abs_fset) (map rep_fset)" |
90 by (fact list_quotient[OF Quotient_fset]) |
90 by (fact list_quotient[OF Quotient_fset]) |
91 |
91 |
121 fix b ba |
121 fix b ba |
122 assume c: "list_rel op \<approx> r b" |
122 assume c: "list_rel op \<approx> r b" |
123 assume d: "b \<approx> ba" |
123 assume d: "b \<approx> ba" |
124 assume e: "list_rel op \<approx> ba s" |
124 assume e: "list_rel op \<approx> ba s" |
125 have f: "map abs_fset r = map abs_fset b" |
125 have f: "map abs_fset r = map abs_fset b" |
126 by (metis Quotient_rel[OF Quotient_fset_list] c) |
126 using Quotient_rel[OF Quotient_fset_list] c by blast |
127 have g: "map abs_fset s = map abs_fset ba" |
127 have "map abs_fset ba = map abs_fset s" |
128 by (metis Quotient_rel[OF Quotient_fset_list] e) |
128 using Quotient_rel[OF Quotient_fset_list] e by blast |
129 show "map abs_fset r \<approx> map abs_fset s" using d f g map_rel_cong by simp |
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 |
130 qed |
131 qed |
131 then show "abs_fset (map abs_fset r) = abs_fset (map abs_fset s)" |
132 then show "abs_fset (map abs_fset r) = abs_fset (map abs_fset s)" |
132 by (metis Quotient_rel[OF Quotient_fset]) |
133 using Quotient_rel[OF Quotient_fset] by blast |
133 next |
134 next |
134 assume a: "(list_rel op \<approx> OOO op \<approx>) r r \<and> (list_rel op \<approx> OOO op \<approx>) s s |
135 assume a: "(list_rel op \<approx> OOO op \<approx>) r r \<and> (list_rel op \<approx> OOO op \<approx>) s s |
135 \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s)" |
136 \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s)" |
136 then have s: "(list_rel op \<approx> OOO op \<approx>) s s" by simp |
137 then have s: "(list_rel op \<approx> OOO op \<approx>) s s" by simp |
137 have d: "map abs_fset r \<approx> map abs_fset s" |
138 have d: "map abs_fset r \<approx> map abs_fset s" |
254 lemma memb_commute_ffold_raw: |
255 lemma memb_commute_ffold_raw: |
255 "rsp_fold f \<Longrightarrow> memb h b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (delete_raw b h))" |
256 "rsp_fold f \<Longrightarrow> memb h b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (delete_raw b h))" |
256 apply (induct b) |
257 apply (induct b) |
257 apply (simp_all add: not_memb_nil) |
258 apply (simp_all add: not_memb_nil) |
258 apply (auto) |
259 apply (auto) |
259 apply (simp_all add: memb_delete_raw not_memb_delete_raw_ident rsp_fold_def memb_cons_iff) |
260 apply (simp_all add: memb_delete_raw not_memb_delete_raw_ident rsp_fold_def memb_cons_iff) |
260 done |
261 done |
261 |
262 |
262 lemma ffold_raw_rsp_pre: |
263 lemma ffold_raw_rsp_pre: |
263 "\<forall>e. memb e a = memb e b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b" |
264 "\<forall>e. memb e a = memb e b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b" |
264 apply (induct a arbitrary: b) |
265 apply (induct a arbitrary: b) |
484 translations |
485 translations |
485 "{|x, xs|}" == "CONST finsert x {|xs|}" |
486 "{|x, xs|}" == "CONST finsert x {|xs|}" |
486 "{|x|}" == "CONST finsert x {||}" |
487 "{|x|}" == "CONST finsert x {||}" |
487 |
488 |
488 quotient_definition |
489 quotient_definition |
489 fin ("_ |\<in>| _" [50, 51] 50) |
490 fin (infix "|\<in>|" 50) |
490 where |
491 where |
491 "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb" |
492 "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb" |
492 |
493 |
493 abbreviation |
494 abbreviation |
494 fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50) |
495 fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) |
495 where |
496 where |
496 "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)" |
497 "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)" |
497 |
498 |
498 section {* Other constants on the Quotient Type *} |
499 section {* Other constants on the Quotient Type *} |
499 |
500 |
546 "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert" |
547 "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert" |
547 by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset] |
548 by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset] |
548 abs_o_rep[OF Quotient_fset] map_id finsert_def) |
549 abs_o_rep[OF Quotient_fset] map_id finsert_def) |
549 |
550 |
550 lemma [quot_preserve]: |
551 lemma [quot_preserve]: |
551 "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> abs_fset \<circ> map abs_fset) op @ = funion" |
552 "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op @ = funion" |
552 by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset] |
553 by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset] |
553 abs_o_rep[OF Quotient_fset] map_id sup_fset_def) |
554 abs_o_rep[OF Quotient_fset] map_id sup_fset_def) |
554 |
555 |
555 lemma list_rel_app_l: |
556 lemma list_rel_app_l: |
556 assumes a: "reflp R" |
557 assumes a: "reflp R" |
557 and b: "list_rel R l r" |
558 and b: "list_rel R l r" |
558 shows "list_rel R (z @ l) (z @ r)" |
559 shows "list_rel R (z @ l) (z @ r)" |
559 by (induct z) (simp_all add: b, metis a reflp_def) |
560 by (induct z) (simp_all add: b rev_iffD1[OF a meta_eq_to_obj_eq[OF reflp_def]]) |
560 |
561 |
561 lemma append_rsp2_pre0: |
562 lemma append_rsp2_pre0: |
562 assumes a:"list_rel op \<approx> x x'" |
563 assumes a:"list_rel op \<approx> x x'" |
563 shows "list_rel op \<approx> (x @ z) (x' @ z)" |
564 shows "list_rel op \<approx> (x @ z) (x' @ z)" |
564 using a apply (induct x x' rule: list_induct2') |
565 using a apply (induct x x' rule: list_induct2') |
565 apply simp_all |
566 by simp_all (rule list_rel_refl) |
566 apply (rule list_rel_refl) |
|
567 done |
|
568 |
567 |
569 lemma append_rsp2_pre1: |
568 lemma append_rsp2_pre1: |
570 assumes a:"list_rel op \<approx> x x'" |
569 assumes a:"list_rel op \<approx> x x'" |
571 shows "list_rel op \<approx> (z @ x) (z @ x')" |
570 shows "list_rel op \<approx> (z @ x) (z @ x')" |
572 using a apply (induct x x' arbitrary: z rule: list_induct2') |
571 using a apply (induct x x' arbitrary: z rule: list_induct2') |
670 |
669 |
671 lemma fcard_raw_suc_memb: |
670 lemma fcard_raw_suc_memb: |
672 assumes a: "fcard_raw A = Suc n" |
671 assumes a: "fcard_raw A = Suc n" |
673 shows "\<exists>a. memb a A" |
672 shows "\<exists>a. memb a A" |
674 using a |
673 using a |
675 apply (induct A) |
674 by (induct A) (auto simp add: memb_def) |
676 apply simp |
|
677 apply (rule_tac x="a" in exI) |
|
678 apply (simp add: memb_def) |
|
679 done |
|
680 |
675 |
681 lemma memb_card_not_0: |
676 lemma memb_card_not_0: |
682 assumes a: "memb a A" |
677 assumes a: "memb a A" |
683 shows "\<not>(fcard_raw A = 0)" |
678 shows "\<not>(fcard_raw A = 0)" |
684 proof - |
679 proof - |
779 apply (simp_all only: memb_cons_iff) |
774 apply (simp_all only: memb_cons_iff) |
780 apply (case_tac [!] "a = aa") |
775 apply (case_tac [!] "a = aa") |
781 apply (simp_all) |
776 apply (simp_all) |
782 apply (case_tac "memb a A") |
777 apply (case_tac "memb a A") |
783 apply (auto simp add: memb_def)[2] |
778 apply (auto simp add: memb_def)[2] |
784 apply (case_tac "list_eq2 (a # A) A") |
|
785 apply (metis list_eq2.intros(3) list_eq2.intros(6)) |
|
786 apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6)) |
779 apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6)) |
787 apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6)) |
780 apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6)) |
788 apply (auto simp add: list_eq2_refl not_memb_delete_raw_ident) |
781 apply (auto simp add: list_eq2_refl not_memb_delete_raw_ident) |
789 done |
782 done |
790 |
783 |
796 |
789 |
797 lemma delete_raw_rsp: |
790 lemma delete_raw_rsp: |
798 "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" |
799 by (simp add: memb_def[symmetric] memb_delete_raw) |
792 by (simp add: memb_def[symmetric] memb_delete_raw) |
800 |
793 |
801 lemma list_eq2_equiv_aux: |
|
802 assumes a: "fcard_raw l = n" |
|
803 and b: "l \<approx> r" |
|
804 shows "list_eq2 l r" |
|
805 using a b |
|
806 proof (induct n arbitrary: l r) |
|
807 case 0 |
|
808 have "fcard_raw l = 0" by fact |
|
809 then have "\<forall>x. \<not> memb x l" using memb_card_not_0[of _ l] by auto |
|
810 then have z: "l = []" using no_memb_nil by auto |
|
811 then have "r = []" using `l \<approx> r` by simp |
|
812 then show ?case using z list_eq2_refl by simp |
|
813 next |
|
814 case (Suc m) |
|
815 have b: "l \<approx> r" by fact |
|
816 have d: "fcard_raw l = Suc m" by fact |
|
817 have "\<exists>a. memb a l" by (rule fcard_raw_suc_memb[OF d]) |
|
818 then obtain a where e: "memb a l" by auto |
|
819 then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b by auto |
|
820 have f: "fcard_raw (delete_raw l a) = m" using fcard_raw_delete[of l a] e d by simp |
|
821 have g: "delete_raw l a \<approx> delete_raw r a" using delete_raw_rsp[OF b] by simp |
|
822 have g': "list_eq2 (delete_raw l a) (delete_raw r a)" by (rule Suc.hyps[OF f g]) |
|
823 have h: "list_eq2 (a # delete_raw l a) (a # delete_raw r a)" by (rule list_eq2.intros(5)[OF g']) |
|
824 have i: "list_eq2 l (a # delete_raw l a)" by (rule list_eq2.intros(3)[OF memb_delete_list_eq2[OF e]]) |
|
825 have "list_eq2 l (a # delete_raw r a)" by (rule list_eq2.intros(6)[OF i h]) |
|
826 then show ?case using list_eq2.intros(6)[OF _ memb_delete_list_eq2[OF e']] by simp |
|
827 qed |
|
828 |
|
829 lemma list_eq2_equiv: |
794 lemma list_eq2_equiv: |
830 "(l \<approx> r) \<longleftrightarrow> (list_eq2 l r)" |
795 "(l \<approx> r) \<longleftrightarrow> (list_eq2 l r)" |
831 proof |
796 proof |
832 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 |
833 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 |
834 qed |
829 qed |
835 |
830 |
836 text {* Lifted theorems *} |
831 text {* Lifted theorems *} |
837 |
832 |
838 lemma not_fin_fnil: "x |\<notin>| {||}" |
833 lemma not_fin_fnil: "x |\<notin>| {||}" |
971 show "P {||}" by (rule prem1) |
962 show "P {||}" by (rule prem1) |
972 next |
963 next |
973 case (finsert x S) |
964 case (finsert x S) |
974 have asm: "P S" by fact |
965 have asm: "P S" by fact |
975 show "P (finsert x S)" |
966 show "P (finsert x S)" |
976 proof(cases "x |\<in>| S") |
967 by (cases "x |\<in>| S") (simp_all add: asm prem2) |
977 case True |
|
978 have "x |\<in>| S" by fact |
|
979 then show "P (finsert x S)" using asm by simp |
|
980 next |
|
981 case False |
|
982 have "x |\<notin>| S" by fact |
|
983 then show "P (finsert x S)" using prem2 asm by simp |
|
984 qed |
|
985 qed |
968 qed |
986 |
969 |
987 lemma fset_induct2: |
970 lemma fset_induct2: |
988 "P {||} {||} \<Longrightarrow> |
971 "P {||} {||} \<Longrightarrow> |
989 (\<And>x xs. x |\<notin>| xs \<Longrightarrow> P (finsert x xs) {||}) \<Longrightarrow> |
972 (\<And>x xs. x |\<notin>| xs \<Longrightarrow> P (finsert x xs) {||}) \<Longrightarrow> |