equal
deleted
inserted
replaced
82 apply(simp add: expand_fun_eq) |
82 apply(simp add: expand_fun_eq) |
83 apply(simp add: Quotient_abs_rep[OF q2]) |
83 apply(simp add: Quotient_abs_rep[OF q2]) |
84 done |
84 done |
85 |
85 |
86 lemma sum_map_id[id_simps]: |
86 lemma sum_map_id[id_simps]: |
87 shows "sum_map id id \<equiv> id" |
87 shows "sum_map id id = id" |
88 apply (rule eq_reflection) |
88 by (simp add: expand_fun_eq split_sum_all) |
89 apply (simp add: expand_fun_eq split_sum_all) |
|
90 done |
|
91 |
89 |
92 lemma sum_rel_eq[id_simps]: |
90 lemma sum_rel_eq[id_simps]: |
93 shows "sum_rel (op =) (op =) \<equiv> (op =)" |
91 shows "sum_rel (op =) (op =) = (op =)" |
94 apply (rule eq_reflection) |
92 by (simp add: expand_fun_eq split_sum_all) |
95 apply(simp add: expand_fun_eq split_sum_all) |
|
96 done |
|
97 |
93 |
98 end |
94 end |