216 apply(rule Quotient_rel_abs[OF Quotient_int]) |
216 apply(rule Quotient_rel_abs[OF Quotient_int]) |
217 apply(rule plus_raw_rsp_aux) |
217 apply(rule plus_raw_rsp_aux) |
218 apply(simp_all add: rep_abs_rsp_left[OF Quotient_int]) |
218 apply(simp_all add: rep_abs_rsp_left[OF Quotient_int]) |
219 done |
219 done |
220 |
220 |
221 lemma int_def: |
221 definition int_of_nat_raw: |
222 shows "of_nat m = ABS_int (m, 0)" |
222 "int_of_nat_raw m = (m :: nat, 0 :: nat)" |
223 by (induct m) (simp_all add: zero_int_def one_int_def add) |
223 |
|
224 quotient_def |
|
225 int_of_nat :: "int_of_nat :: nat \<Rightarrow> int" |
|
226 where "int_of_nat_raw" |
|
227 |
|
228 lemma[quot_respect]: |
|
229 shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw" |
|
230 by (simp add: equivp_reflp[OF int_equivp]) |
|
231 |
|
232 lemma int_def: |
|
233 shows "of_nat m = int_of_nat m" |
|
234 apply (induct m) |
|
235 apply (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add) |
|
236 done |
224 |
237 |
225 lemma le_antisym_raw: |
238 lemma le_antisym_raw: |
226 shows "less_eq_raw i j \<Longrightarrow> less_eq_raw j i \<Longrightarrow> i \<approx> j" |
239 shows "less_eq_raw i j \<Longrightarrow> less_eq_raw j i \<Longrightarrow> i \<approx> j" |
227 by (cases i, cases j) (simp) |
240 by (cases i, cases j) (simp) |
228 |
241 |
295 done |
308 done |
296 |
309 |
297 lemma int_induct_raw: |
310 lemma int_induct_raw: |
298 assumes a: "P (0::nat, 0)" |
311 assumes a: "P (0::nat, 0)" |
299 and b: "\<And>i. P i \<Longrightarrow> P (plus_raw i (1,0))" |
312 and b: "\<And>i. P i \<Longrightarrow> P (plus_raw i (1,0))" |
300 and c: "\<And>i. P i \<Longrightarrow> P (plus_raw i (minus_raw (1,0)))" |
313 and c: "\<And>i. P i \<Longrightarrow> P (plus_raw i (uminus_raw (1,0)))" |
301 shows "P x" |
314 shows "P x" |
302 apply(case_tac x) apply(simp) |
315 apply(case_tac x) apply(simp) |
303 apply(rule_tac x="b" in spec) |
316 apply(rule_tac x="b" in spec) |
304 apply(rule_tac Nat.induct) |
317 apply(rule_tac Nat.induct) |
305 apply(rule allI) |
318 apply(rule allI) |
312 and b: "\<And>i. P i \<Longrightarrow> P (i + 1)" |
325 and b: "\<And>i. P i \<Longrightarrow> P (i + 1)" |
313 and c: "\<And>i. P i \<Longrightarrow> P (i + (- 1))" |
326 and c: "\<And>i. P i \<Longrightarrow> P (i + (- 1))" |
314 shows "P x" |
327 shows "P x" |
315 using a b c by (lifting int_induct_raw) |
328 using a b c by (lifting int_induct_raw) |
316 |
329 |
317 lemma zero_le_imp_eq_int: |
330 lemma zero_le_imp_eq_int_raw: |
|
331 fixes k::"(nat \<times> nat)" |
|
332 shows "less_raw (0, 0) k \<Longrightarrow> (\<exists>n > 0. k \<approx> int_of_nat_raw n)" |
|
333 apply(cases k) |
|
334 apply(simp add:int_of_nat_raw) |
|
335 apply(auto) |
|
336 apply(rule_tac i="b" and j="a" in less_Suc_induct) |
|
337 apply(auto) |
|
338 done |
|
339 |
|
340 lemma zero_le_imp_eq_int: |
318 fixes k::int |
341 fixes k::int |
319 shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n" |
342 shows "0 < k \<Longrightarrow> \<exists>n > 0. k = int_of_nat n" |
320 sorry |
343 unfolding less_int_def |
|
344 by (lifting zero_le_imp_eq_int_raw) |
321 |
345 |
322 lemma zmult_zless_mono2: |
346 lemma zmult_zless_mono2: |
323 fixes i j k::int |
347 fixes i j k::int |
324 assumes a: "i < j" "0 < k" |
348 assumes a: "i < j" "0 < k" |
325 shows "k * i < k * j" |
349 shows "k * i < k * j" |
326 using a |
350 using a |
|
351 using a |
327 apply(drule_tac zero_le_imp_eq_int) |
352 apply(drule_tac zero_le_imp_eq_int) |
|
353 apply(fold int_def) |
328 apply(auto simp add: zmult_zless_mono2_lemma) |
354 apply(auto simp add: zmult_zless_mono2_lemma) |
329 done |
355 done |
330 |
356 |
331 text{*The integers form an ordered integral domain*} |
357 text{*The integers form an ordered integral domain*} |
332 instance int :: ordered_idom |
358 instance int :: ordered_idom |