equal
deleted
inserted
replaced
192 using a |
192 using a |
193 by (cases a, cases b, cases c, cases d) |
193 by (cases a, cases b, cases c, cases d) |
194 (simp) |
194 (simp) |
195 |
195 |
196 lemma add: |
196 lemma add: |
197 "(ABS_int (x,y)) + (ABS_int (u,v)) = |
197 "(abs_int (x,y)) + (abs_int (u,v)) = |
198 (ABS_int (x + u, y + v))" |
198 (abs_int (x + u, y + v))" |
199 apply(simp add: plus_int_def) |
199 apply(simp add: plus_int_def) |
200 apply(fold plus_raw.simps) |
200 apply(fold plus_raw.simps) |
201 apply(rule Quotient_rel_abs[OF Quotient_int]) |
201 apply(rule Quotient_rel_abs[OF Quotient_int]) |
202 apply(rule plus_raw_rsp_aux) |
202 apply(rule plus_raw_rsp_aux) |
203 apply(simp_all add: rep_abs_rsp_left[OF Quotient_int]) |
203 apply(simp_all add: rep_abs_rsp_left[OF Quotient_int]) |