equal
deleted
inserted
replaced
74 using q1 q2 |
74 using q1 q2 |
75 unfolding Quotient_def |
75 unfolding Quotient_def |
76 apply(blast)+ |
76 apply(blast)+ |
77 done |
77 done |
78 |
78 |
79 lemma sum_map_id[id_simps]: |
79 lemma sum_map_id[id_simps]: |
80 shows "sum_map id id \<equiv> id" |
80 shows "sum_map id id = id" |
81 apply (rule eq_reflection) |
|
82 apply (rule ext) |
81 apply (rule ext) |
83 apply (case_tac x) |
82 apply (case_tac x) |
84 apply (auto) |
83 apply (auto) |
85 done |
84 done |
86 |
85 |
87 lemma sum_rel_eq[id_simps]: |
86 lemma sum_rel_eq[id_simps]: |
88 "sum_rel op = op = \<equiv> op =" |
87 "(sum_rel op = op =) = op =" |
89 apply (rule eq_reflection) |
|
90 apply (rule ext)+ |
88 apply (rule ext)+ |
91 apply (case_tac x) |
89 apply (case_tac x) |
92 apply auto |
90 apply auto |
93 apply (case_tac xa) |
91 apply (case_tac xa) |
94 apply auto |
92 apply auto |