78 else f a (ffold_raw f z xs) |
78 else f a (ffold_raw f z xs) |
79 else z)" |
79 else z)" |
80 |
80 |
81 text {* Composition Quotient *} |
81 text {* Composition Quotient *} |
82 |
82 |
83 lemma list_rel_refl1: |
83 lemma list_all2_refl1: |
84 shows "(list_rel op \<approx>) r r" |
84 shows "(list_all2 op \<approx>) r r" |
85 by (rule list_rel_refl) (metis equivp_def fset_equivp) |
85 by (rule list_all2_refl) (metis equivp_def fset_equivp) |
86 |
86 |
87 lemma compose_list_refl: |
87 lemma compose_list_refl: |
88 shows "(list_rel op \<approx> OOO op \<approx>) r r" |
88 shows "(list_all2 op \<approx> OOO op \<approx>) r r" |
89 proof |
89 proof |
90 have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp]) |
90 have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp]) |
91 show "list_rel op \<approx> r r" by (rule list_rel_refl1) |
91 show "list_all2 op \<approx> r r" by (rule list_all2_refl1) |
92 with * show "(op \<approx> OO list_rel op \<approx>) r r" .. |
92 with * show "(op \<approx> OO list_all2 op \<approx>) r r" .. |
93 qed |
93 qed |
94 |
94 |
95 lemma Quotient_fset_list: |
95 lemma Quotient_fset_list: |
96 shows "Quotient (list_rel op \<approx>) (map abs_fset) (map rep_fset)" |
96 shows "Quotient (list_all2 op \<approx>) (map abs_fset) (map rep_fset)" |
97 by (fact list_quotient[OF Quotient_fset]) |
97 by (fact list_quotient[OF Quotient_fset]) |
98 |
98 |
99 lemma set_in_eq: "(\<forall>e. ((e \<in> xs) \<longleftrightarrow> (e \<in> ys))) \<equiv> xs = ys" |
99 lemma set_in_eq: "(\<forall>e. ((e \<in> xs) \<longleftrightarrow> (e \<in> ys))) \<equiv> xs = ys" |
100 by (rule eq_reflection) auto |
100 by (rule eq_reflection) auto |
101 |
101 |
103 unfolding list_eq.simps |
103 unfolding list_eq.simps |
104 by (simp only: set_map set_in_eq) |
104 by (simp only: set_map set_in_eq) |
105 |
105 |
106 |
106 |
107 lemma quotient_compose_list[quot_thm]: |
107 lemma quotient_compose_list[quot_thm]: |
108 shows "Quotient ((list_rel op \<approx>) OOO (op \<approx>)) |
108 shows "Quotient ((list_all2 op \<approx>) OOO (op \<approx>)) |
109 (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)" |
109 (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)" |
110 unfolding Quotient_def comp_def |
110 unfolding Quotient_def comp_def |
111 proof (intro conjI allI) |
111 proof (intro conjI allI) |
112 fix a r s |
112 fix a r s |
113 show "abs_fset (map abs_fset (map rep_fset (rep_fset a))) = a" |
113 show "abs_fset (map abs_fset (map rep_fset (rep_fset a))) = a" |
114 by (simp add: abs_o_rep[OF Quotient_fset] Quotient_abs_rep[OF Quotient_fset] map_id) |
114 by (simp add: abs_o_rep[OF Quotient_fset] Quotient_abs_rep[OF Quotient_fset] map_id) |
115 have b: "list_rel op \<approx> (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))" |
115 have b: "list_all2 op \<approx> (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))" |
116 by (rule list_rel_refl1) |
116 by (rule list_all2_refl1) |
117 have c: "(op \<approx> OO list_rel op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))" |
117 have c: "(op \<approx> OO list_all2 op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))" |
118 by (rule, rule equivp_reflp[OF fset_equivp]) (rule b) |
118 by (rule, rule equivp_reflp[OF fset_equivp]) (rule b) |
119 show "(list_rel op \<approx> OOO op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))" |
119 show "(list_all2 op \<approx> OOO op \<approx>) (map rep_fset (rep_fset a)) (map rep_fset (rep_fset a))" |
120 by (rule, rule list_rel_refl1) (rule c) |
120 by (rule, rule list_all2_refl1) (rule c) |
121 show "(list_rel op \<approx> OOO op \<approx>) r s = ((list_rel op \<approx> OOO op \<approx>) r r \<and> |
121 show "(list_all2 op \<approx> OOO op \<approx>) r s = ((list_all2 op \<approx> OOO op \<approx>) r r \<and> |
122 (list_rel op \<approx> OOO op \<approx>) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))" |
122 (list_all2 op \<approx> OOO op \<approx>) s s \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s))" |
123 proof (intro iffI conjI) |
123 proof (intro iffI conjI) |
124 show "(list_rel op \<approx> OOO op \<approx>) r r" by (rule compose_list_refl) |
124 show "(list_all2 op \<approx> OOO op \<approx>) r r" by (rule compose_list_refl) |
125 show "(list_rel op \<approx> OOO op \<approx>) s s" by (rule compose_list_refl) |
125 show "(list_all2 op \<approx> OOO op \<approx>) s s" by (rule compose_list_refl) |
126 next |
126 next |
127 assume a: "(list_rel op \<approx> OOO op \<approx>) r s" |
127 assume a: "(list_all2 op \<approx> OOO op \<approx>) r s" |
128 then have b: "map abs_fset r \<approx> map abs_fset s" |
128 then have b: "map abs_fset r \<approx> map abs_fset s" |
129 proof (elim pred_compE) |
129 proof (elim pred_compE) |
130 fix b ba |
130 fix b ba |
131 assume c: "list_rel op \<approx> r b" |
131 assume c: "list_all2 op \<approx> r b" |
132 assume d: "b \<approx> ba" |
132 assume d: "b \<approx> ba" |
133 assume e: "list_rel op \<approx> ba s" |
133 assume e: "list_all2 op \<approx> ba s" |
134 have f: "map abs_fset r = map abs_fset b" |
134 have f: "map abs_fset r = map abs_fset b" |
135 using Quotient_rel[OF Quotient_fset_list] c by blast |
135 using Quotient_rel[OF Quotient_fset_list] c by blast |
136 have "map abs_fset ba = map abs_fset s" |
136 have "map abs_fset ba = map abs_fset s" |
137 using Quotient_rel[OF Quotient_fset_list] e by blast |
137 using Quotient_rel[OF Quotient_fset_list] e by blast |
138 then have g: "map abs_fset s = map abs_fset ba" by simp |
138 then have g: "map abs_fset s = map abs_fset ba" by simp |
139 then show "map abs_fset r \<approx> map abs_fset s" using d f map_rel_cong by simp |
139 then show "map abs_fset r \<approx> map abs_fset s" using d f map_rel_cong by simp |
140 qed |
140 qed |
141 then show "abs_fset (map abs_fset r) = abs_fset (map abs_fset s)" |
141 then show "abs_fset (map abs_fset r) = abs_fset (map abs_fset s)" |
142 using Quotient_rel[OF Quotient_fset] by blast |
142 using Quotient_rel[OF Quotient_fset] by blast |
143 next |
143 next |
144 assume a: "(list_rel op \<approx> OOO op \<approx>) r r \<and> (list_rel op \<approx> OOO op \<approx>) s s |
144 assume a: "(list_all2 op \<approx> OOO op \<approx>) r r \<and> (list_all2 op \<approx> OOO op \<approx>) s s |
145 \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s)" |
145 \<and> abs_fset (map abs_fset r) = abs_fset (map abs_fset s)" |
146 then have s: "(list_rel op \<approx> OOO op \<approx>) s s" by simp |
146 then have s: "(list_all2 op \<approx> OOO op \<approx>) s s" by simp |
147 have d: "map abs_fset r \<approx> map abs_fset s" |
147 have d: "map abs_fset r \<approx> map abs_fset s" |
148 by (subst Quotient_rel[OF Quotient_fset]) (simp add: a) |
148 by (subst Quotient_rel[OF Quotient_fset]) (simp add: a) |
149 have b: "map rep_fset (map abs_fset r) \<approx> map rep_fset (map abs_fset s)" |
149 have b: "map rep_fset (map abs_fset r) \<approx> map rep_fset (map abs_fset s)" |
150 by (rule map_rel_cong[OF d]) |
150 by (rule map_rel_cong[OF d]) |
151 have y: "list_rel op \<approx> (map rep_fset (map abs_fset s)) s" |
151 have y: "list_all2 op \<approx> (map rep_fset (map abs_fset s)) s" |
152 by (fact rep_abs_rsp_left[OF Quotient_fset_list, OF list_rel_refl1[of s]]) |
152 by (fact rep_abs_rsp_left[OF Quotient_fset_list, OF list_all2_refl1[of s]]) |
153 have c: "(op \<approx> OO list_rel op \<approx>) (map rep_fset (map abs_fset r)) s" |
153 have c: "(op \<approx> OO list_all2 op \<approx>) (map rep_fset (map abs_fset r)) s" |
154 by (rule pred_compI) (rule b, rule y) |
154 by (rule pred_compI) (rule b, rule y) |
155 have z: "list_rel op \<approx> r (map rep_fset (map abs_fset r))" |
155 have z: "list_all2 op \<approx> r (map rep_fset (map abs_fset r))" |
156 by (fact rep_abs_rsp[OF Quotient_fset_list, OF list_rel_refl1[of r]]) |
156 by (fact rep_abs_rsp[OF Quotient_fset_list, OF list_all2_refl1[of r]]) |
157 then show "(list_rel op \<approx> OOO op \<approx>) r s" |
157 then show "(list_all2 op \<approx> OOO op \<approx>) r s" |
158 using a c pred_compI by simp |
158 using a c pred_compI by simp |
159 qed |
159 qed |
160 qed |
160 qed |
161 |
161 |
162 text {* Respectfullness *} |
162 text {* Respectfullness *} |
340 lemma [quot_respect]: |
340 lemma [quot_respect]: |
341 "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw" |
341 "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw" |
342 by (simp add: memb_def[symmetric] ffold_raw_rsp_pre) |
342 by (simp add: memb_def[symmetric] ffold_raw_rsp_pre) |
343 |
343 |
344 lemma concat_rsp_pre: |
344 lemma concat_rsp_pre: |
345 assumes a: "list_rel op \<approx> x x'" |
345 assumes a: "list_all2 op \<approx> x x'" |
346 and b: "x' \<approx> y'" |
346 and b: "x' \<approx> y'" |
347 and c: "list_rel op \<approx> y' y" |
347 and c: "list_all2 op \<approx> y' y" |
348 and d: "\<exists>x\<in>set x. xa \<in> set x" |
348 and d: "\<exists>x\<in>set x. xa \<in> set x" |
349 shows "\<exists>x\<in>set y. xa \<in> set x" |
349 shows "\<exists>x\<in>set y. xa \<in> set x" |
350 proof - |
350 proof - |
351 obtain xb where e: "xb \<in> set x" and f: "xa \<in> set xb" using d by auto |
351 obtain xb where e: "xb \<in> set x" and f: "xa \<in> set xb" using d by auto |
352 have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_rel_find_element[OF e a]) |
352 have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_all2_find_element[OF e a]) |
353 then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto |
353 then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto |
354 have "ya \<in> set y'" using b h by simp |
354 have "ya \<in> set y'" using b h by simp |
355 then have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" using c by (rule list_rel_find_element) |
355 then have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" using c by (rule list_all2_find_element) |
356 then show ?thesis using f i by auto |
356 then show ?thesis using f i by auto |
357 qed |
357 qed |
358 |
358 |
359 lemma concat_rsp[quot_respect]: |
359 lemma concat_rsp[quot_respect]: |
360 shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat" |
360 shows "(list_all2 op \<approx> OOO op \<approx> ===> op \<approx>) concat concat" |
361 proof (rule fun_relI, elim pred_compE) |
361 proof (rule fun_relI, elim pred_compE) |
362 fix a b ba bb |
362 fix a b ba bb |
363 assume a: "list_rel op \<approx> a ba" |
363 assume a: "list_all2 op \<approx> a ba" |
364 assume b: "ba \<approx> bb" |
364 assume b: "ba \<approx> bb" |
365 assume c: "list_rel op \<approx> bb b" |
365 assume c: "list_all2 op \<approx> bb b" |
366 have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof |
366 have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof |
367 fix x |
367 fix x |
368 show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof |
368 show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof |
369 assume d: "\<exists>xa\<in>set a. x \<in> set xa" |
369 assume d: "\<exists>xa\<in>set a. x \<in> set xa" |
370 show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d]) |
370 show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d]) |
371 next |
371 next |
372 assume e: "\<exists>xa\<in>set b. x \<in> set xa" |
372 assume e: "\<exists>xa\<in>set b. x \<in> set xa" |
373 have a': "list_rel op \<approx> ba a" by (rule list_rel_symp[OF list_eq_equivp, OF a]) |
373 have a': "list_all2 op \<approx> ba a" by (rule list_all2_symp[OF list_eq_equivp, OF a]) |
374 have b': "bb \<approx> ba" by (rule equivp_symp[OF list_eq_equivp, OF b]) |
374 have b': "bb \<approx> ba" by (rule equivp_symp[OF list_eq_equivp, OF b]) |
375 have c': "list_rel op \<approx> b bb" by (rule list_rel_symp[OF list_eq_equivp, OF c]) |
375 have c': "list_all2 op \<approx> b bb" by (rule list_all2_symp[OF list_eq_equivp, OF c]) |
376 show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e]) |
376 show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e]) |
377 qed |
377 qed |
378 qed |
378 qed |
379 then show "concat a \<approx> concat b" by simp |
379 then show "concat a \<approx> concat b" by simp |
380 qed |
380 qed |
381 |
381 |
382 |
382 |
383 |
383 |
384 lemma concat_rsp_unfolded: |
384 lemma concat_rsp_unfolded: |
385 "\<lbrakk>list_rel op \<approx> a ba; ba \<approx> bb; list_rel op \<approx> bb b\<rbrakk> \<Longrightarrow> concat a \<approx> concat b" |
385 "\<lbrakk>list_all2 op \<approx> a ba; ba \<approx> bb; list_all2 op \<approx> bb b\<rbrakk> \<Longrightarrow> concat a \<approx> concat b" |
386 proof - |
386 proof - |
387 fix a b ba bb |
387 fix a b ba bb |
388 assume a: "list_rel op \<approx> a ba" |
388 assume a: "list_all2 op \<approx> a ba" |
389 assume b: "ba \<approx> bb" |
389 assume b: "ba \<approx> bb" |
390 assume c: "list_rel op \<approx> bb b" |
390 assume c: "list_all2 op \<approx> bb b" |
391 have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof |
391 have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof |
392 fix x |
392 fix x |
393 show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof |
393 show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof |
394 assume d: "\<exists>xa\<in>set a. x \<in> set xa" |
394 assume d: "\<exists>xa\<in>set a. x \<in> set xa" |
395 show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d]) |
395 show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d]) |
396 next |
396 next |
397 assume e: "\<exists>xa\<in>set b. x \<in> set xa" |
397 assume e: "\<exists>xa\<in>set b. x \<in> set xa" |
398 have a': "list_rel op \<approx> ba a" by (rule list_rel_symp[OF list_eq_equivp, OF a]) |
398 have a': "list_all2 op \<approx> ba a" by (rule list_all2_symp[OF list_eq_equivp, OF a]) |
399 have b': "bb \<approx> ba" by (rule equivp_symp[OF list_eq_equivp, OF b]) |
399 have b': "bb \<approx> ba" by (rule equivp_symp[OF list_eq_equivp, OF b]) |
400 have c': "list_rel op \<approx> b bb" by (rule list_rel_symp[OF list_eq_equivp, OF c]) |
400 have c': "list_all2 op \<approx> b bb" by (rule list_all2_symp[OF list_eq_equivp, OF c]) |
401 show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e]) |
401 show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e]) |
402 qed |
402 qed |
403 qed |
403 qed |
404 then show "concat a \<approx> concat b" by simp |
404 then show "concat a \<approx> concat b" by simp |
405 qed |
405 qed |
643 lemma [quot_preserve]: |
643 lemma [quot_preserve]: |
644 "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op @ = funion" |
644 "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op @ = funion" |
645 by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset] |
645 by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset] |
646 abs_o_rep[OF Quotient_fset] map_id sup_fset_def) |
646 abs_o_rep[OF Quotient_fset] map_id sup_fset_def) |
647 |
647 |
648 lemma list_rel_app_l: |
648 lemma list_all2_app_l: |
649 assumes a: "reflp R" |
649 assumes a: "reflp R" |
650 and b: "list_rel R l r" |
650 and b: "list_all2 R l r" |
651 shows "list_rel R (z @ l) (z @ r)" |
651 shows "list_all2 R (z @ l) (z @ r)" |
652 by (induct z) (simp_all add: b rev_iffD1[OF a meta_eq_to_obj_eq[OF reflp_def]]) |
652 by (induct z) (simp_all add: b rev_iffD1[OF a meta_eq_to_obj_eq[OF reflp_def]]) |
653 |
653 |
654 lemma append_rsp2_pre0: |
654 lemma append_rsp2_pre0: |
655 assumes a:"list_rel op \<approx> x x'" |
655 assumes a:"list_all2 op \<approx> x x'" |
656 shows "list_rel op \<approx> (x @ z) (x' @ z)" |
656 shows "list_all2 op \<approx> (x @ z) (x' @ z)" |
657 using a apply (induct x x' rule: list_induct2') |
657 using a apply (induct x x' rule: list_induct2') |
658 by simp_all (rule list_rel_refl1) |
658 by simp_all (rule list_all2_refl1) |
659 |
659 |
660 lemma append_rsp2_pre1: |
660 lemma append_rsp2_pre1: |
661 assumes a:"list_rel op \<approx> x x'" |
661 assumes a:"list_all2 op \<approx> x x'" |
662 shows "list_rel op \<approx> (z @ x) (z @ x')" |
662 shows "list_all2 op \<approx> (z @ x) (z @ x')" |
663 using a apply (induct x x' arbitrary: z rule: list_induct2') |
663 using a apply (induct x x' arbitrary: z rule: list_induct2') |
664 apply (rule list_rel_refl1) |
664 apply (rule list_all2_refl1) |
665 apply (simp_all del: list_eq.simps) |
665 apply (simp_all del: list_eq.simps) |
666 apply (rule list_rel_app_l) |
666 apply (rule list_all2_app_l) |
667 apply (simp_all add: reflp_def) |
667 apply (simp_all add: reflp_def) |
668 done |
668 done |
669 |
669 |
670 lemma append_rsp2_pre: |
670 lemma append_rsp2_pre: |
671 assumes a:"list_rel op \<approx> x x'" |
671 assumes a:"list_all2 op \<approx> x x'" |
672 and b: "list_rel op \<approx> z z'" |
672 and b: "list_all2 op \<approx> z z'" |
673 shows "list_rel op \<approx> (x @ z) (x' @ z')" |
673 shows "list_all2 op \<approx> (x @ z) (x' @ z')" |
674 apply (rule list_rel_transp[OF fset_equivp]) |
674 apply (rule list_all2_transp[OF fset_equivp]) |
675 apply (rule append_rsp2_pre0) |
675 apply (rule append_rsp2_pre0) |
676 apply (rule a) |
676 apply (rule a) |
677 using b apply (induct z z' rule: list_induct2') |
677 using b apply (induct z z' rule: list_induct2') |
678 apply (simp_all only: append_Nil2) |
678 apply (simp_all only: append_Nil2) |
679 apply (rule list_rel_refl1) |
679 apply (rule list_all2_refl1) |
680 apply simp_all |
680 apply simp_all |
681 apply (rule append_rsp2_pre1) |
681 apply (rule append_rsp2_pre1) |
682 apply simp |
682 apply simp |
683 done |
683 done |
684 |
684 |
685 lemma [quot_respect]: |
685 lemma [quot_respect]: |
686 "(list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op @ op @" |
686 "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) op @ op @" |
687 proof (intro fun_relI, elim pred_compE) |
687 proof (intro fun_relI, elim pred_compE) |
688 fix x y z w x' z' y' w' :: "'a list list" |
688 fix x y z w x' z' y' w' :: "'a list list" |
689 assume a:"list_rel op \<approx> x x'" |
689 assume a:"list_all2 op \<approx> x x'" |
690 and b: "x' \<approx> y'" |
690 and b: "x' \<approx> y'" |
691 and c: "list_rel op \<approx> y' y" |
691 and c: "list_all2 op \<approx> y' y" |
692 assume aa: "list_rel op \<approx> z z'" |
692 assume aa: "list_all2 op \<approx> z z'" |
693 and bb: "z' \<approx> w'" |
693 and bb: "z' \<approx> w'" |
694 and cc: "list_rel op \<approx> w' w" |
694 and cc: "list_all2 op \<approx> w' w" |
695 have a': "list_rel op \<approx> (x @ z) (x' @ z')" using a aa append_rsp2_pre by auto |
695 have a': "list_all2 op \<approx> (x @ z) (x' @ z')" using a aa append_rsp2_pre by auto |
696 have b': "x' @ z' \<approx> y' @ w'" using b bb by simp |
696 have b': "x' @ z' \<approx> y' @ w'" using b bb by simp |
697 have c': "list_rel op \<approx> (y' @ w') (y @ w)" using c cc append_rsp2_pre by auto |
697 have c': "list_all2 op \<approx> (y' @ w') (y @ w)" using c cc append_rsp2_pre by auto |
698 have d': "(op \<approx> OO list_rel op \<approx>) (x' @ z') (y @ w)" |
698 have d': "(op \<approx> OO list_all2 op \<approx>) (x' @ z') (y @ w)" |
699 by (rule pred_compI) (rule b', rule c') |
699 by (rule pred_compI) (rule b', rule c') |
700 show "(list_rel op \<approx> OOO op \<approx>) (x @ z) (y @ w)" |
700 show "(list_all2 op \<approx> OOO op \<approx>) (x @ z) (y @ w)" |
701 by (rule pred_compI) (rule a', rule d') |
701 by (rule pred_compI) (rule a', rule d') |
702 qed |
702 qed |
703 |
703 |
704 text {* Raw theorems. Finsert, memb, singleron, sub_list *} |
704 text {* Raw theorems. Finsert, memb, singleron, sub_list *} |
705 |
705 |
1675 apply rule |
1675 apply rule |
1676 apply (rule ball_reg_right) |
1676 apply (rule ball_reg_right) |
1677 apply auto |
1677 apply auto |
1678 done |
1678 done |
1679 |
1679 |
1680 lemma list_rel_refl: |
1680 lemma list_all2_refl: |
1681 assumes q: "equivp R" |
1681 assumes q: "equivp R" |
1682 shows "(list_rel R) r r" |
1682 shows "(list_all2 R) r r" |
1683 by (rule list_rel_refl) (metis equivp_def fset_equivp q) |
1683 by (rule list_all2_refl) (metis equivp_def fset_equivp q) |
1684 |
1684 |
1685 lemma compose_list_refl2: |
1685 lemma compose_list_refl2: |
1686 assumes q: "equivp R" |
1686 assumes q: "equivp R" |
1687 shows "(list_rel R OOO op \<approx>) r r" |
1687 shows "(list_all2 R OOO op \<approx>) r r" |
1688 proof |
1688 proof |
1689 have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp]) |
1689 have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp]) |
1690 show "list_rel R r r" by (rule list_rel_refl[OF q]) |
1690 show "list_all2 R r r" by (rule list_all2_refl[OF q]) |
1691 with * show "(op \<approx> OO list_rel R) r r" .. |
1691 with * show "(op \<approx> OO list_all2 R) r r" .. |
1692 qed |
1692 qed |
1693 |
1693 |
1694 lemma quotient_compose_list_g[quot_thm]: |
1694 lemma quotient_compose_list_g[quot_thm]: |
1695 assumes q: "Quotient R Abs Rep" |
1695 assumes q: "Quotient R Abs Rep" |
1696 and e: "equivp R" |
1696 and e: "equivp R" |
1697 shows "Quotient ((list_rel R) OOO (op \<approx>)) |
1697 shows "Quotient ((list_all2 R) OOO (op \<approx>)) |
1698 (abs_fset \<circ> (map Abs)) ((map Rep) \<circ> rep_fset)" |
1698 (abs_fset \<circ> (map Abs)) ((map Rep) \<circ> rep_fset)" |
1699 unfolding Quotient_def comp_def |
1699 unfolding Quotient_def comp_def |
1700 proof (intro conjI allI) |
1700 proof (intro conjI allI) |
1701 fix a r s |
1701 fix a r s |
1702 show "abs_fset (map Abs (map Rep (rep_fset a))) = a" |
1702 show "abs_fset (map Abs (map Rep (rep_fset a))) = a" |
1703 by (simp add: abs_o_rep[OF q] Quotient_abs_rep[OF Quotient_fset] map_id) |
1703 by (simp add: abs_o_rep[OF q] Quotient_abs_rep[OF Quotient_fset] map_id) |
1704 have b: "list_rel R (map Rep (rep_fset a)) (map Rep (rep_fset a))" |
1704 have b: "list_all2 R (map Rep (rep_fset a)) (map Rep (rep_fset a))" |
1705 by (rule list_rel_refl[OF e]) |
1705 by (rule list_all2_refl[OF e]) |
1706 have c: "(op \<approx> OO list_rel R) (map Rep (rep_fset a)) (map Rep (rep_fset a))" |
1706 have c: "(op \<approx> OO list_all2 R) (map Rep (rep_fset a)) (map Rep (rep_fset a))" |
1707 by (rule, rule equivp_reflp[OF fset_equivp]) (rule b) |
1707 by (rule, rule equivp_reflp[OF fset_equivp]) (rule b) |
1708 show "(list_rel R OOO op \<approx>) (map Rep (rep_fset a)) (map Rep (rep_fset a))" |
1708 show "(list_all2 R OOO op \<approx>) (map Rep (rep_fset a)) (map Rep (rep_fset a))" |
1709 by (rule, rule list_rel_refl[OF e]) (rule c) |
1709 by (rule, rule list_all2_refl[OF e]) (rule c) |
1710 show "(list_rel R OOO op \<approx>) r s = ((list_rel R OOO op \<approx>) r r \<and> |
1710 show "(list_all2 R OOO op \<approx>) r s = ((list_all2 R OOO op \<approx>) r r \<and> |
1711 (list_rel R OOO op \<approx>) s s \<and> abs_fset (map Abs r) = abs_fset (map Abs s))" |
1711 (list_all2 R OOO op \<approx>) s s \<and> abs_fset (map Abs r) = abs_fset (map Abs s))" |
1712 proof (intro iffI conjI) |
1712 proof (intro iffI conjI) |
1713 show "(list_rel R OOO op \<approx>) r r" by (rule compose_list_refl2[OF e]) |
1713 show "(list_all2 R OOO op \<approx>) r r" by (rule compose_list_refl2[OF e]) |
1714 show "(list_rel R OOO op \<approx>) s s" by (rule compose_list_refl2[OF e]) |
1714 show "(list_all2 R OOO op \<approx>) s s" by (rule compose_list_refl2[OF e]) |
1715 next |
1715 next |
1716 assume a: "(list_rel R OOO op \<approx>) r s" |
1716 assume a: "(list_all2 R OOO op \<approx>) r s" |
1717 then have b: "map Abs r \<approx> map Abs s" |
1717 then have b: "map Abs r \<approx> map Abs s" |
1718 proof (elim pred_compE) |
1718 proof (elim pred_compE) |
1719 fix b ba |
1719 fix b ba |
1720 assume c: "list_rel R r b" |
1720 assume c: "list_all2 R r b" |
1721 assume d: "b \<approx> ba" |
1721 assume d: "b \<approx> ba" |
1722 assume e: "list_rel R ba s" |
1722 assume e: "list_all2 R ba s" |
1723 have f: "map Abs r = map Abs b" |
1723 have f: "map Abs r = map Abs b" |
1724 using Quotient_rel[OF list_quotient[OF q]] c by blast |
1724 using Quotient_rel[OF list_quotient[OF q]] c by blast |
1725 have "map Abs ba = map Abs s" |
1725 have "map Abs ba = map Abs s" |
1726 using Quotient_rel[OF list_quotient[OF q]] e by blast |
1726 using Quotient_rel[OF list_quotient[OF q]] e by blast |
1727 then have g: "map Abs s = map Abs ba" by simp |
1727 then have g: "map Abs s = map Abs ba" by simp |
1728 then show "map Abs r \<approx> map Abs s" using d f map_rel_cong by simp |
1728 then show "map Abs r \<approx> map Abs s" using d f map_rel_cong by simp |
1729 qed |
1729 qed |
1730 then show "abs_fset (map Abs r) = abs_fset (map Abs s)" |
1730 then show "abs_fset (map Abs r) = abs_fset (map Abs s)" |
1731 using Quotient_rel[OF Quotient_fset] by blast |
1731 using Quotient_rel[OF Quotient_fset] by blast |
1732 next |
1732 next |
1733 assume a: "(list_rel R OOO op \<approx>) r r \<and> (list_rel R OOO op \<approx>) s s |
1733 assume a: "(list_all2 R OOO op \<approx>) r r \<and> (list_all2 R OOO op \<approx>) s s |
1734 \<and> abs_fset (map Abs r) = abs_fset (map Abs s)" |
1734 \<and> abs_fset (map Abs r) = abs_fset (map Abs s)" |
1735 then have s: "(list_rel R OOO op \<approx>) s s" by simp |
1735 then have s: "(list_all2 R OOO op \<approx>) s s" by simp |
1736 have d: "map Abs r \<approx> map Abs s" |
1736 have d: "map Abs r \<approx> map Abs s" |
1737 by (subst Quotient_rel[OF Quotient_fset]) (simp add: a) |
1737 by (subst Quotient_rel[OF Quotient_fset]) (simp add: a) |
1738 have b: "map Rep (map Abs r) \<approx> map Rep (map Abs s)" |
1738 have b: "map Rep (map Abs r) \<approx> map Rep (map Abs s)" |
1739 by (rule map_rel_cong[OF d]) |
1739 by (rule map_rel_cong[OF d]) |
1740 have y: "list_rel R (map Rep (map Abs s)) s" |
1740 have y: "list_all2 R (map Rep (map Abs s)) s" |
1741 by (fact rep_abs_rsp_left[OF list_quotient[OF q], OF list_rel_refl[OF e, of s]]) |
1741 by (fact rep_abs_rsp_left[OF list_quotient[OF q], OF list_all2_refl[OF e, of s]]) |
1742 have c: "(op \<approx> OO list_rel R) (map Rep (map Abs r)) s" |
1742 have c: "(op \<approx> OO list_all2 R) (map Rep (map Abs r)) s" |
1743 by (rule pred_compI) (rule b, rule y) |
1743 by (rule pred_compI) (rule b, rule y) |
1744 have z: "list_rel R r (map Rep (map Abs r))" |
1744 have z: "list_all2 R r (map Rep (map Abs r))" |
1745 by (fact rep_abs_rsp[OF list_quotient[OF q], OF list_rel_refl[OF e, of r]]) |
1745 by (fact rep_abs_rsp[OF list_quotient[OF q], OF list_all2_refl[OF e, of r]]) |
1746 then show "(list_rel R OOO op \<approx>) r s" |
1746 then show "(list_all2 R OOO op \<approx>) r s" |
1747 using a c pred_compI by simp |
1747 using a c pred_compI by simp |
1748 qed |
1748 qed |
1749 qed |
1749 qed |
1750 |
1750 |
1751 no_notation |
1751 no_notation |