equal
deleted
inserted
replaced
80 apply(simp add: Quotient_rel_rep[OF q2]) |
80 apply(simp add: Quotient_rel_rep[OF q2]) |
81 apply(rule allI)+ |
81 apply(rule allI)+ |
82 apply(rule sum_fun_fun[OF q1 q2]) |
82 apply(rule sum_fun_fun[OF q1 q2]) |
83 done |
83 done |
84 |
84 |
|
85 lemma sum_map_id[id_simps]: "sum_map id id \<equiv> id" |
|
86 apply (rule eq_reflection) |
|
87 apply (rule ext) |
|
88 apply (case_tac x) |
|
89 apply (auto) |
|
90 done |
|
91 |
|
92 lemma sum_rel_eq[id_simps]: "sum_rel op = op = \<equiv> op =" |
|
93 apply (rule eq_reflection) |
|
94 apply (rule ext)+ |
|
95 apply (case_tac x) |
|
96 apply auto |
|
97 apply (case_tac xa) |
|
98 apply auto |
|
99 apply (case_tac xa) |
|
100 apply auto |
|
101 done |
|
102 |
85 end |
103 end |