equal
deleted
inserted
replaced
1 theory IntEx2 |
1 theory IntEx2 |
2 imports "../QuotMain" Nat |
2 imports "../QuotMain" "../QuotProd" Nat |
3 (*uses |
3 (*uses |
4 ("Tools/numeral.ML") |
4 ("Tools/numeral.ML") |
5 ("Tools/numeral_syntax.ML") |
5 ("Tools/numeral_syntax.ML") |
6 ("Tools/int_arith.ML")*) |
6 ("Tools/int_arith.ML")*) |
7 begin |
7 begin |
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 id_simps) |
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]) |
204 done |
204 done |