equal
deleted
inserted
replaced
21 lemma map_sum_id [id_simps]: |
21 lemma map_sum_id [id_simps]: |
22 "map_sum id id = id" |
22 "map_sum id id = id" |
23 by (simp add: id_def map_sum.identity fun_eq_iff) |
23 by (simp add: id_def map_sum.identity fun_eq_iff) |
24 |
24 |
25 lemma rel_sum_eq [id_simps]: |
25 lemma rel_sum_eq [id_simps]: |
26 "rel_sum (op =) (op =) = (op =)" |
26 "rel_sum (=) (=) = (=)" |
27 by (rule sum.rel_eq) |
27 by (rule sum.rel_eq) |
28 |
28 |
29 lemma reflp_rel_sum: |
29 lemma reflp_rel_sum: |
30 "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (rel_sum R1 R2)" |
30 "reflp R1 \<Longrightarrow> reflp R2 \<Longrightarrow> reflp (rel_sum R1 R2)" |
31 unfolding reflp_def split_sum_all rel_sum_simps by fast |
31 unfolding reflp_def split_sum_all rel_sum_simps by fast |