equal
deleted
inserted
replaced
292 apply(simp) |
292 apply(simp) |
293 apply(case_tac "k = 0") |
293 apply(case_tac "k = 0") |
294 apply(simp_all add: left_distrib add_strict_mono) |
294 apply(simp_all add: left_distrib add_strict_mono) |
295 done |
295 done |
296 |
296 |
|
297 lemma int_induct_raw: |
|
298 assumes a: "P (0::nat, 0)" |
|
299 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)))" |
|
301 shows "P x" |
|
302 apply(case_tac x) apply(simp) |
|
303 apply(rule_tac x="b" in spec) |
|
304 apply(rule_tac Nat.induct) |
|
305 apply(rule allI) |
|
306 apply(rule_tac Nat.induct) |
|
307 using a b c apply(auto) |
|
308 done |
|
309 |
|
310 lemma int_induct: |
|
311 assumes a: "P (0::int)" |
|
312 and b: "\<And>i. P i \<Longrightarrow> P (i + 1)" |
|
313 and c: "\<And>i. P i \<Longrightarrow> P (i + (- 1))" |
|
314 shows "P x" |
|
315 using a b c by (lifting int_induct_raw) |
|
316 |
297 lemma zero_le_imp_eq_int: |
317 lemma zero_le_imp_eq_int: |
298 fixes k::int |
318 fixes k::int |
299 shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n" |
319 shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n" |
300 sorry |
320 sorry |
301 |
321 |