72 |
72 |
73 lemma sum_Inl_prs[quot_preserve]: |
73 lemma sum_Inl_prs[quot_preserve]: |
74 assumes q1: "Quotient R1 Abs1 Rep1" |
74 assumes q1: "Quotient R1 Abs1 Rep1" |
75 assumes q2: "Quotient R2 Abs2 Rep2" |
75 assumes q2: "Quotient R2 Abs2 Rep2" |
76 shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl" |
76 shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl" |
77 apply(simp add: ext_iff) |
77 apply(simp add: fun_eq_iff) |
78 apply(simp add: Quotient_abs_rep[OF q1]) |
78 apply(simp add: Quotient_abs_rep[OF q1]) |
79 done |
79 done |
80 |
80 |
81 lemma sum_Inr_prs[quot_preserve]: |
81 lemma sum_Inr_prs[quot_preserve]: |
82 assumes q1: "Quotient R1 Abs1 Rep1" |
82 assumes q1: "Quotient R1 Abs1 Rep1" |
83 assumes q2: "Quotient R2 Abs2 Rep2" |
83 assumes q2: "Quotient R2 Abs2 Rep2" |
84 shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr" |
84 shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr" |
85 apply(simp add: ext_iff) |
85 apply(simp add: fun_eq_iff) |
86 apply(simp add: Quotient_abs_rep[OF q2]) |
86 apply(simp add: Quotient_abs_rep[OF q2]) |
87 done |
87 done |
88 |
88 |
89 lemma sum_map_id[id_simps]: |
89 lemma sum_map_id[id_simps]: |
90 shows "sum_map id id = id" |
90 shows "sum_map id id = id" |
91 by (simp add: ext_iff split_sum_all) |
91 by (simp add: fun_eq_iff split_sum_all) |
92 |
92 |
93 lemma sum_rel_eq[id_simps]: |
93 lemma sum_rel_eq[id_simps]: |
94 shows "sum_rel (op =) (op =) = (op =)" |
94 shows "sum_rel (op =) (op =) = (op =)" |
95 by (simp add: ext_iff split_sum_all) |
95 by (simp add: fun_eq_iff split_sum_all) |
96 |
96 |
97 end |
97 end |