equal
deleted
inserted
replaced
14 sum_map |
14 sum_map |
15 where |
15 where |
16 "sum_map f1 f2 (Inl a) = Inl (f1 a)" |
16 "sum_map f1 f2 (Inl a) = Inl (f1 a)" |
17 | "sum_map f1 f2 (Inr a) = Inr (f2 a)" |
17 | "sum_map f1 f2 (Inr a) = Inr (f2 a)" |
18 |
18 |
19 declare [[map * = (sum_map, sum_rel)]] |
19 declare [[map "+" = (sum_map, sum_rel)]] |
|
20 |
20 |
21 |
21 lemma sum_equivp[quot_equiv]: |
22 lemma sum_equivp[quot_equiv]: |
22 assumes a: "equivp R1" |
23 assumes a: "equivp R1" |
23 assumes b: "equivp R2" |
24 assumes b: "equivp R2" |
24 shows "equivp (sum_rel R1 R2)" |
25 shows "equivp (sum_rel R1 R2)" |