138 show "(list_all2 R OOO op \<approx>) r r" by (rule compose_list_refl[OF e]) |
138 show "(list_all2 R OOO op \<approx>) r r" by (rule compose_list_refl[OF e]) |
139 show "(list_all2 R OOO op \<approx>) s s" by (rule compose_list_refl[OF e]) |
139 show "(list_all2 R OOO op \<approx>) s s" by (rule compose_list_refl[OF e]) |
140 next |
140 next |
141 assume a: "(list_all2 R OOO op \<approx>) r s" |
141 assume a: "(list_all2 R OOO op \<approx>) r s" |
142 then have b: "map Abs r \<approx> map Abs s" |
142 then have b: "map Abs r \<approx> map Abs s" |
143 proof (elim pred_compE) |
143 proof (elim relcomppE) |
144 fix b ba |
144 fix b ba |
145 assume c: "list_all2 R r b" |
145 assume c: "list_all2 R r b" |
146 assume d: "b \<approx> ba" |
146 assume d: "b \<approx> ba" |
147 assume e: "list_all2 R ba s" |
147 assume e: "list_all2 R ba s" |
148 have f: "map Abs r = map Abs b" |
148 have f: "map Abs r = map Abs b" |
163 have b: "map Rep (map Abs r) \<approx> map Rep (map Abs s)" |
163 have b: "map Rep (map Abs r) \<approx> map Rep (map Abs s)" |
164 by (rule map_list_eq_cong[OF d]) |
164 by (rule map_list_eq_cong[OF d]) |
165 have y: "list_all2 R (map Rep (map Abs s)) s" |
165 have y: "list_all2 R (map Rep (map Abs s)) s" |
166 by (fact rep_abs_rsp_left[OF list_quotient[OF q], OF list_all2_refl'[OF e, of s]]) |
166 by (fact rep_abs_rsp_left[OF list_quotient[OF q], OF list_all2_refl'[OF e, of s]]) |
167 have c: "(op \<approx> OO list_all2 R) (map Rep (map Abs r)) s" |
167 have c: "(op \<approx> OO list_all2 R) (map Rep (map Abs r)) s" |
168 by (rule pred_compI) (rule b, rule y) |
168 by (rule relcomppI) (rule b, rule y) |
169 have z: "list_all2 R r (map Rep (map Abs r))" |
169 have z: "list_all2 R r (map Rep (map Abs r))" |
170 by (fact rep_abs_rsp[OF list_quotient[OF q], OF list_all2_refl'[OF e, of r]]) |
170 by (fact rep_abs_rsp[OF list_quotient[OF q], OF list_all2_refl'[OF e, of r]]) |
171 then show "(list_all2 R OOO op \<approx>) r s" |
171 then show "(list_all2 R OOO op \<approx>) r s" |
172 using a c pred_compI by simp |
172 using a c relcomppI by simp |
173 qed |
173 qed |
174 qed |
174 qed |
175 |
175 |
176 lemma quotient_compose_list[quot_thm]: |
176 lemma quotient_compose_list[quot_thm]: |
177 shows "Quotient ((list_all2 op \<approx>) OOO (op \<approx>)) |
177 shows "Quotient ((list_all2 op \<approx>) OOO (op \<approx>)) |
358 qed |
358 qed |
359 |
359 |
360 quotient_definition |
360 quotient_definition |
361 "concat_fset :: ('a fset) fset \<Rightarrow> 'a fset" |
361 "concat_fset :: ('a fset) fset \<Rightarrow> 'a fset" |
362 is concat |
362 is concat |
363 proof (elim pred_compE) |
363 proof (elim relcomppE) |
364 fix a b ba bb |
364 fix a b ba bb |
365 assume a: "list_all2 op \<approx> a ba" |
365 assume a: "list_all2 op \<approx> a ba" |
366 with list_symp [OF list_eq_symp] have a': "list_all2 op \<approx> ba a" by (rule sympE) |
366 with list_symp [OF list_eq_symp] have a': "list_all2 op \<approx> ba a" by (rule sympE) |
367 assume b: "ba \<approx> bb" |
367 assume b: "ba \<approx> bb" |
368 with list_eq_symp have b': "bb \<approx> ba" by (rule sympE) |
368 with list_eq_symp have b': "bb \<approx> ba" by (rule sympE) |
395 by (rule compose_list_refl, rule list_eq_equivp) |
395 by (rule compose_list_refl, rule list_eq_equivp) |
396 |
396 |
397 lemma Cons_rsp2 [quot_respect]: |
397 lemma Cons_rsp2 [quot_respect]: |
398 shows "(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) Cons Cons" |
398 shows "(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) Cons Cons" |
399 apply (auto intro!: fun_relI) |
399 apply (auto intro!: fun_relI) |
400 apply (rule_tac b="x # b" in pred_compI) |
400 apply (rule_tac b="x # b" in relcomppI) |
401 apply auto |
401 apply auto |
402 apply (rule_tac b="x # ba" in pred_compI) |
402 apply (rule_tac b="x # ba" in relcomppI) |
403 apply auto |
403 apply auto |
404 done |
404 done |
405 |
405 |
406 lemma Nil_prs2 [quot_preserve]: |
406 lemma Nil_prs2 [quot_preserve]: |
407 assumes "Quotient R Abs Rep" |
407 assumes "Quotient R Abs Rep" |
451 |
451 |
452 lemma compositional_rsp3: |
452 lemma compositional_rsp3: |
453 assumes "(R1 ===> R2 ===> R3) C C" and "(R4 ===> R5 ===> R6) C C" |
453 assumes "(R1 ===> R2 ===> R3) C C" and "(R4 ===> R5 ===> R6) C C" |
454 shows "(R1 OOO R4 ===> R2 OOO R5 ===> R3 OOO R6) C C" |
454 shows "(R1 OOO R4 ===> R2 OOO R5 ===> R3 OOO R6) C C" |
455 by (auto intro!: fun_relI) |
455 by (auto intro!: fun_relI) |
456 (metis (full_types) assms fun_relE pred_compI) |
456 (metis (full_types) assms fun_relE relcomppI) |
457 |
457 |
458 lemma append_rsp2 [quot_respect]: |
458 lemma append_rsp2 [quot_respect]: |
459 "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append" |
459 "(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append" |
460 by (intro compositional_rsp3) |
460 by (intro compositional_rsp3) |
461 (auto intro!: fun_relI simp add: append_rsp2_pre) |
461 (auto intro!: fun_relI simp add: append_rsp2_pre) |
477 have c: "(list_all2 op \<approx>) (map f y) (map f' ya)" |
477 have c: "(list_all2 op \<approx>) (map f y) (map f' ya)" |
478 using y fs |
478 using y fs |
479 by (induct y ya rule: list_induct2') |
479 by (induct y ya rule: list_induct2') |
480 (simp_all, metis apply_rsp' list_eq_def) |
480 (simp_all, metis apply_rsp' list_eq_def) |
481 show "(list_all2 op \<approx> OOO op \<approx>) (map f xa) (map f' ya)" |
481 show "(list_all2 op \<approx> OOO op \<approx>) (map f xa) (map f' ya)" |
482 by (metis a b c list_eq_def pred_compI) |
482 by (metis a b c list_eq_def relcomppI) |
483 qed |
483 qed |
484 |
484 |
485 lemma map_prs2 [quot_preserve]: |
485 lemma map_prs2 [quot_preserve]: |
486 shows "((abs_fset ---> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> abs_fset \<circ> map abs_fset) map = (id ---> rep_fset ---> abs_fset) map" |
486 shows "((abs_fset ---> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> abs_fset \<circ> map abs_fset) map = (id ---> rep_fset ---> abs_fset) map" |
487 by (auto simp add: fun_eq_iff) |
487 by (auto simp add: fun_eq_iff) |