53 lemma sum_equivp [quot_equiv]: |
53 lemma sum_equivp [quot_equiv]: |
54 "equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (sum_rel R1 R2)" |
54 "equivp R1 \<Longrightarrow> equivp R2 \<Longrightarrow> equivp (sum_rel R1 R2)" |
55 by (blast intro: equivpI sum_reflp sum_symp sum_transp elim: equivpE) |
55 by (blast intro: equivpI sum_reflp sum_symp sum_transp elim: equivpE) |
56 |
56 |
57 lemma sum_quotient [quot_thm]: |
57 lemma sum_quotient [quot_thm]: |
58 assumes q1: "Quotient R1 Abs1 Rep1" |
58 assumes q1: "Quotient3 R1 Abs1 Rep1" |
59 assumes q2: "Quotient R2 Abs2 Rep2" |
59 assumes q2: "Quotient3 R2 Abs2 Rep2" |
60 shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)" |
60 shows "Quotient3 (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)" |
61 apply (rule QuotientI) |
61 apply (rule Quotient3I) |
62 apply (simp_all add: sum_map.compositionality comp_def sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2 |
62 apply (simp_all add: sum_map.compositionality comp_def sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2 |
63 Quotient_abs_rep [OF q1] Quotient_rel_rep [OF q1] Quotient_abs_rep [OF q2] Quotient_rel_rep [OF q2]) |
63 Quotient3_abs_rep [OF q1] Quotient3_rel_rep [OF q1] Quotient3_abs_rep [OF q2] Quotient3_rel_rep [OF q2]) |
64 using Quotient_rel [OF q1] Quotient_rel [OF q2] |
64 using Quotient3_rel [OF q1] Quotient3_rel [OF q2] |
65 apply (simp add: sum_rel_unfold comp_def split: sum.split) |
65 apply (simp add: sum_rel_unfold comp_def split: sum.split) |
66 done |
66 done |
67 |
67 |
68 declare [[map sum = (sum_rel, sum_quotient)]] |
68 declare [[mapQ3 sum = (sum_rel, sum_quotient)]] |
69 |
69 |
70 lemma sum_Inl_rsp [quot_respect]: |
70 lemma sum_Inl_rsp [quot_respect]: |
71 assumes q1: "Quotient R1 Abs1 Rep1" |
71 assumes q1: "Quotient3 R1 Abs1 Rep1" |
72 assumes q2: "Quotient R2 Abs2 Rep2" |
72 assumes q2: "Quotient3 R2 Abs2 Rep2" |
73 shows "(R1 ===> sum_rel R1 R2) Inl Inl" |
73 shows "(R1 ===> sum_rel R1 R2) Inl Inl" |
74 by auto |
74 by auto |
75 |
75 |
76 lemma sum_Inr_rsp [quot_respect]: |
76 lemma sum_Inr_rsp [quot_respect]: |
77 assumes q1: "Quotient R1 Abs1 Rep1" |
77 assumes q1: "Quotient3 R1 Abs1 Rep1" |
78 assumes q2: "Quotient R2 Abs2 Rep2" |
78 assumes q2: "Quotient3 R2 Abs2 Rep2" |
79 shows "(R2 ===> sum_rel R1 R2) Inr Inr" |
79 shows "(R2 ===> sum_rel R1 R2) Inr Inr" |
80 by auto |
80 by auto |
81 |
81 |
82 lemma sum_Inl_prs [quot_preserve]: |
82 lemma sum_Inl_prs [quot_preserve]: |
83 assumes q1: "Quotient R1 Abs1 Rep1" |
83 assumes q1: "Quotient3 R1 Abs1 Rep1" |
84 assumes q2: "Quotient R2 Abs2 Rep2" |
84 assumes q2: "Quotient3 R2 Abs2 Rep2" |
85 shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl" |
85 shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl" |
86 apply(simp add: fun_eq_iff) |
86 apply(simp add: fun_eq_iff) |
87 apply(simp add: Quotient_abs_rep[OF q1]) |
87 apply(simp add: Quotient3_abs_rep[OF q1]) |
88 done |
88 done |
89 |
89 |
90 lemma sum_Inr_prs [quot_preserve]: |
90 lemma sum_Inr_prs [quot_preserve]: |
91 assumes q1: "Quotient R1 Abs1 Rep1" |
91 assumes q1: "Quotient3 R1 Abs1 Rep1" |
92 assumes q2: "Quotient R2 Abs2 Rep2" |
92 assumes q2: "Quotient3 R2 Abs2 Rep2" |
93 shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr" |
93 shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr" |
94 apply(simp add: fun_eq_iff) |
94 apply(simp add: fun_eq_iff) |
95 apply(simp add: Quotient_abs_rep[OF q2]) |
95 apply(simp add: Quotient3_abs_rep[OF q2]) |
96 done |
96 done |
97 |
97 |
98 end |
98 end |