67 assumes q1: "Quotient R1 Abs1 Rep1" |
67 assumes q1: "Quotient R1 Abs1 Rep1" |
68 assumes q2: "Quotient R2 Abs2 Rep2" |
68 assumes q2: "Quotient R2 Abs2 Rep2" |
69 shows "(R2 ===> sum_rel R1 R2) Inr Inr" |
69 shows "(R2 ===> sum_rel R1 R2) Inr Inr" |
70 by simp |
70 by simp |
71 |
71 |
72 lemma sum_Inl_prs[quot_respect]: |
72 lemma sum_Inl_prs[quot_preserve]: |
73 assumes q1: "Quotient R1 Abs1 Rep1" |
73 assumes q1: "Quotient R1 Abs1 Rep1" |
74 assumes q2: "Quotient R2 Abs2 Rep2" |
74 assumes q2: "Quotient R2 Abs2 Rep2" |
75 shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl" |
75 shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl" |
76 apply(simp add: expand_fun_eq) |
76 apply(simp add: expand_fun_eq) |
77 apply(simp add: Quotient_abs_rep[OF q1]) |
77 apply(simp add: Quotient_abs_rep[OF q1]) |
78 done |
78 done |
79 |
79 |
80 lemma sum_Inr_prs[quot_respect]: |
80 lemma sum_Inr_prs[quot_preserve]: |
81 assumes q1: "Quotient R1 Abs1 Rep1" |
81 assumes q1: "Quotient R1 Abs1 Rep1" |
82 assumes q2: "Quotient R2 Abs2 Rep2" |
82 assumes q2: "Quotient R2 Abs2 Rep2" |
83 shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr" |
83 shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr" |
84 apply(simp add: expand_fun_eq) |
84 apply(simp add: expand_fun_eq) |
85 apply(simp add: Quotient_abs_rep[OF q2]) |
85 apply(simp add: Quotient_abs_rep[OF q2]) |