equal
deleted
inserted
replaced
200 show "0 \<noteq> (1::int)" |
200 show "0 \<noteq> (1::int)" |
201 by (lifting one_zero_distinct) |
201 by (lifting one_zero_distinct) |
202 qed |
202 qed |
203 |
203 |
204 |
204 |
|
205 lemma plus_raw_rsp_lo: |
|
206 "\<And>a b c d. a \<approx> b \<Longrightarrow> c \<approx> d \<Longrightarrow> plus_raw a c \<approx> plus_raw b d" |
|
207 by auto |
|
208 |
205 lemma add: |
209 lemma add: |
206 "(ABS_int (x,y)) + (ABS_int (u,v)) = |
210 "(ABS_int (x,y)) + (ABS_int (u,v)) = |
207 (ABS_int (x+u, y+v))" |
211 (ABS_int (x+u, y+v))" |
208 apply(simp add: plus_int_def) |
212 apply(simp add: plus_int_def) |
209 sorry |
213 apply(fold plus_raw.simps) |
|
214 apply(rule Quotient_rel_abs[OF Quotient_int]) |
|
215 apply(rule plus_raw_rsp_lo) |
|
216 apply(simp_all add: rep_abs_rsp_left[OF Quotient_int]) |
|
217 done |
210 |
218 |
211 lemma int_def: "of_nat m = ABS_int (m, 0)" |
219 lemma int_def: "of_nat m = ABS_int (m, 0)" |
212 apply(induct m) |
220 apply(induct m) |
213 apply(simp add: zero_int_def) |
221 apply(simp add: zero_int_def) |
214 apply(simp add: one_int_def add) |
222 apply(simp add: one_int_def add) |