178 |
178 |
179 instance int :: comm_ring_1 |
179 instance int :: comm_ring_1 |
180 proof |
180 proof |
181 fix i j k :: int |
181 fix i j k :: int |
182 show "(i + j) + k = i + (j + k)" |
182 show "(i + j) + k = i + (j + k)" |
183 by (lifting plus_assoc_raw) |
183 by (lifting plus_assoc_raw) |
184 show "i + j = j + i" |
184 show "i + j = j + i" |
185 by (lifting plus_sym_raw) |
185 by (lifting plus_sym_raw) |
186 show "0 + i = (i::int)" |
186 show "0 + i = (i::int)" |
187 by (lifting plus_zero_raw) |
187 by (lifting plus_zero_raw) |
188 show "- i + i = 0" |
188 show "- i + i = 0" |
199 by (lifting times_plus_comm_raw) |
199 by (lifting times_plus_comm_raw) |
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 lemma plus_raw_rsp_aux: |
205 lemma plus_raw_rsp_lo: |
205 assumes a: "a \<approx> b" "c \<approx> d" |
206 "\<And>a b c d. a \<approx> b \<Longrightarrow> c \<approx> d \<Longrightarrow> plus_raw a c \<approx> plus_raw b d" |
206 shows "plus_raw a c \<approx> plus_raw b d" |
207 by auto |
207 using a |
|
208 by (cases a, cases b, cases c, cases d) |
|
209 (simp) |
208 |
210 |
209 lemma add: |
211 lemma add: |
210 "(ABS_int (x,y)) + (ABS_int (u,v)) = |
212 "(ABS_int (x,y)) + (ABS_int (u,v)) = |
211 (ABS_int (x+u, y+v))" |
213 (ABS_int (x + u, y + v))" |
212 apply(simp add: plus_int_def) |
214 apply(simp add: plus_int_def) |
213 apply(fold plus_raw.simps) |
215 apply(fold plus_raw.simps) |
214 apply(rule Quotient_rel_abs[OF Quotient_int]) |
216 apply(rule Quotient_rel_abs[OF Quotient_int]) |
215 apply(rule plus_raw_rsp_lo) |
217 apply(rule plus_raw_rsp_aux) |
216 apply(simp_all add: rep_abs_rsp_left[OF Quotient_int]) |
218 apply(simp_all add: rep_abs_rsp_left[OF Quotient_int]) |
217 done |
219 done |
218 |
220 |
219 lemma int_def: "of_nat m = ABS_int (m, 0)" |
221 lemma int_def: |
220 apply(induct m) |
222 shows "of_nat m = ABS_int (m, 0)" |
221 apply(simp add: zero_int_def) |
223 by (induct m) (simp_all add: zero_int_def one_int_def add) |
222 apply(simp add: one_int_def add) |
|
223 done |
|
224 |
224 |
225 lemma le_antisym_raw: |
225 lemma le_antisym_raw: |
226 shows "less_eq_raw i j \<Longrightarrow> less_eq_raw j i \<Longrightarrow> i \<approx> j" |
226 shows "less_eq_raw i j \<Longrightarrow> less_eq_raw j i \<Longrightarrow> i \<approx> j" |
227 by (cases i, cases j) (simp) |
227 by (cases i, cases j) (simp) |
228 |
228 |
282 qed |
282 qed |
283 |
283 |
284 abbreviation |
284 abbreviation |
285 "less_raw i j \<equiv> less_eq_raw i j \<and> \<not>(i \<approx> j)" |
285 "less_raw i j \<equiv> less_eq_raw i j \<and> \<not>(i \<approx> j)" |
286 |
286 |
287 |
287 lemma zmult_zless_mono2_lemma: |
288 lemma test: |
288 fixes i j::int |
289 "\<lbrakk>less_raw i j; less_raw (0, 0) k\<rbrakk> |
289 and k::nat |
290 \<Longrightarrow> less_raw (times_raw k i) (times_raw k j)" |
290 shows "i < j \<Longrightarrow> 0 < k \<Longrightarrow> of_nat k * i < of_nat k * j" |
291 apply(cases i, cases j, cases k) |
291 apply(induct "k") |
292 apply(simp only: less_eq_raw.simps times_raw.simps) |
|
293 apply(simp) |
292 apply(simp) |
294 apply(rename_tac u v w x y z) |
293 apply(case_tac "k = 0") |
295 apply(rule conjI) |
294 apply(simp_all add: left_distrib add_strict_mono) |
296 apply(subgoal_tac "y*u + y*x \<le> y*w + y*v & z*v \<le> y*v") |
295 done |
297 apply(simp add: ) |
296 |
|
297 lemma zero_le_imp_eq_int: |
|
298 fixes k::int |
|
299 shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n" |
298 sorry |
300 sorry |
299 |
301 |
|
302 lemma zmult_zless_mono2: |
|
303 fixes i j k::int |
|
304 assumes a: "i < j" "0 < k" |
|
305 shows "k * i < k * j" |
|
306 using a |
|
307 apply(drule_tac zero_le_imp_eq_int) |
|
308 apply(auto simp add: zmult_zless_mono2_lemma) |
|
309 done |
300 |
310 |
301 text{*The integers form an ordered integral domain*} |
311 text{*The integers form an ordered integral domain*} |
302 instance int :: ordered_idom |
312 instance int :: ordered_idom |
303 proof |
313 proof |
304 fix i j k :: int |
314 fix i j k :: int |
305 show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j" |
315 show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j" |
306 unfolding less_int_def by (lifting test) |
316 by (rule zmult_zless_mono2) |
307 show "\<bar>i\<bar> = (if i < 0 then -i else i)" |
317 show "\<bar>i\<bar> = (if i < 0 then -i else i)" |
308 by (simp only: abs_int_def) |
318 by (simp only: abs_int_def) |
309 show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)" |
319 show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)" |
310 by (simp only: sgn_int_def) |
320 by (simp only: sgn_int_def) |
311 qed |
321 qed |