301 apply(simp) |
301 apply(simp) |
302 apply(case_tac "k = 0") |
302 apply(case_tac "k = 0") |
303 apply(simp_all add: left_distrib add_strict_mono) |
303 apply(simp_all add: left_distrib add_strict_mono) |
304 done |
304 done |
305 |
305 |
306 lemma int_induct_raw: |
|
307 assumes a: "P (0::nat, 0)" |
|
308 and b: "\<And>i. P i \<Longrightarrow> P (plus_raw i (1,0))" |
|
309 and c: "\<And>i. P i \<Longrightarrow> P (plus_raw i (uminus_raw (1,0)))" |
|
310 shows "P x" |
|
311 apply(case_tac x) apply(simp) |
|
312 apply(rule_tac x="b" in spec) |
|
313 apply(rule_tac Nat.induct) |
|
314 apply(rule allI) |
|
315 apply(rule_tac Nat.induct) |
|
316 using a b c apply(auto) |
|
317 done |
|
318 |
|
319 lemma int_induct: |
|
320 assumes a: "P (0::int)" |
|
321 and b: "\<And>i. P i \<Longrightarrow> P (i + 1)" |
|
322 and c: "\<And>i. P i \<Longrightarrow> P (i + (- 1))" |
|
323 shows "P x" |
|
324 using a b c by (lifting int_induct_raw) |
|
325 |
|
326 lemma zero_le_imp_eq_int_raw: |
306 lemma zero_le_imp_eq_int_raw: |
327 fixes k::"(nat \<times> nat)" |
307 fixes k::"(nat \<times> nat)" |
328 shows "less_raw (0, 0) k \<Longrightarrow> (\<exists>n > 0. k \<approx> int_of_nat_raw n)" |
308 shows "less_raw (0, 0) k \<Longrightarrow> (\<exists>n > 0. k \<approx> int_of_nat_raw n)" |
329 apply(cases k) |
309 apply(cases k) |
330 apply(simp add:int_of_nat_raw) |
310 apply(simp add:int_of_nat_raw) |
333 apply(auto) |
313 apply(auto) |
334 done |
314 done |
335 |
315 |
336 lemma zero_le_imp_eq_int: |
316 lemma zero_le_imp_eq_int: |
337 fixes k::int |
317 fixes k::int |
338 shows "0 < k \<Longrightarrow> \<exists>n > 0. k = int_of_nat n" |
318 shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n" |
339 unfolding less_int_def |
319 unfolding less_int_def int_of_nat |
340 by (lifting zero_le_imp_eq_int_raw) |
320 by (lifting zero_le_imp_eq_int_raw) |
341 |
321 |
342 lemma zmult_zless_mono2: |
322 lemma zmult_zless_mono2: |
343 fixes i j k::int |
323 fixes i j k::int |
344 assumes a: "i < j" "0 < k" |
324 assumes a: "i < j" "0 < k" |
345 shows "k * i < k * j" |
325 shows "k * i < k * j" |
346 using a |
326 using a |
347 using a |
327 using a |
348 apply(drule_tac zero_le_imp_eq_int) |
328 apply(drule_tac zero_le_imp_eq_int) |
349 apply(fold int_def) |
|
350 apply(auto simp add: zmult_zless_mono2_lemma) |
329 apply(auto simp add: zmult_zless_mono2_lemma) |
351 done |
330 done |
352 |
331 |
353 text{*The integers form an ordered integral domain*} |
332 text{*The integers form an ordered integral domain*} |
354 instance int :: ordered_idom |
333 instance int :: ordered_idom |