384 lemma of_hypnat_mult [simp]: |
384 lemma of_hypnat_mult [simp]: |
385 "\<And>m n. of_hypnat (m * n) = of_hypnat m * of_hypnat n" |
385 "\<And>m n. of_hypnat (m * n) = of_hypnat m * of_hypnat n" |
386 by transfer (rule of_nat_mult) |
386 by transfer (rule of_nat_mult) |
387 |
387 |
388 lemma of_hypnat_less_iff [simp]: |
388 lemma of_hypnat_less_iff [simp]: |
389 "\<And>m n. (of_hypnat m < (of_hypnat n::'a::ordered_semidom star)) = (m < n)" |
389 "\<And>m n. (of_hypnat m < (of_hypnat n::'a::linordered_semidom star)) = (m < n)" |
390 by transfer (rule of_nat_less_iff) |
390 by transfer (rule of_nat_less_iff) |
391 |
391 |
392 lemma of_hypnat_0_less_iff [simp]: |
392 lemma of_hypnat_0_less_iff [simp]: |
393 "\<And>n. (0 < (of_hypnat n::'a::ordered_semidom star)) = (0 < n)" |
393 "\<And>n. (0 < (of_hypnat n::'a::linordered_semidom star)) = (0 < n)" |
394 by transfer (rule of_nat_0_less_iff) |
394 by transfer (rule of_nat_0_less_iff) |
395 |
395 |
396 lemma of_hypnat_less_0_iff [simp]: |
396 lemma of_hypnat_less_0_iff [simp]: |
397 "\<And>m. \<not> (of_hypnat m::'a::ordered_semidom star) < 0" |
397 "\<And>m. \<not> (of_hypnat m::'a::linordered_semidom star) < 0" |
398 by transfer (rule of_nat_less_0_iff) |
398 by transfer (rule of_nat_less_0_iff) |
399 |
399 |
400 lemma of_hypnat_le_iff [simp]: |
400 lemma of_hypnat_le_iff [simp]: |
401 "\<And>m n. (of_hypnat m \<le> (of_hypnat n::'a::ordered_semidom star)) = (m \<le> n)" |
401 "\<And>m n. (of_hypnat m \<le> (of_hypnat n::'a::linordered_semidom star)) = (m \<le> n)" |
402 by transfer (rule of_nat_le_iff) |
402 by transfer (rule of_nat_le_iff) |
403 |
403 |
404 lemma of_hypnat_0_le_iff [simp]: |
404 lemma of_hypnat_0_le_iff [simp]: |
405 "\<And>n. 0 \<le> (of_hypnat n::'a::ordered_semidom star)" |
405 "\<And>n. 0 \<le> (of_hypnat n::'a::linordered_semidom star)" |
406 by transfer (rule of_nat_0_le_iff) |
406 by transfer (rule of_nat_0_le_iff) |
407 |
407 |
408 lemma of_hypnat_le_0_iff [simp]: |
408 lemma of_hypnat_le_0_iff [simp]: |
409 "\<And>m. ((of_hypnat m::'a::ordered_semidom star) \<le> 0) = (m = 0)" |
409 "\<And>m. ((of_hypnat m::'a::linordered_semidom star) \<le> 0) = (m = 0)" |
410 by transfer (rule of_nat_le_0_iff) |
410 by transfer (rule of_nat_le_0_iff) |
411 |
411 |
412 lemma of_hypnat_eq_iff [simp]: |
412 lemma of_hypnat_eq_iff [simp]: |
413 "\<And>m n. (of_hypnat m = (of_hypnat n::'a::ordered_semidom star)) = (m = n)" |
413 "\<And>m n. (of_hypnat m = (of_hypnat n::'a::linordered_semidom star)) = (m = n)" |
414 by transfer (rule of_nat_eq_iff) |
414 by transfer (rule of_nat_eq_iff) |
415 |
415 |
416 lemma of_hypnat_eq_0_iff [simp]: |
416 lemma of_hypnat_eq_0_iff [simp]: |
417 "\<And>m. ((of_hypnat m::'a::ordered_semidom star) = 0) = (m = 0)" |
417 "\<And>m. ((of_hypnat m::'a::linordered_semidom star) = 0) = (m = 0)" |
418 by transfer (rule of_nat_eq_0_iff) |
418 by transfer (rule of_nat_eq_0_iff) |
419 |
419 |
420 lemma HNatInfinite_of_hypnat_gt_zero: |
420 lemma HNatInfinite_of_hypnat_gt_zero: |
421 "N \<in> HNatInfinite \<Longrightarrow> (0::'a::ordered_semidom star) < of_hypnat N" |
421 "N \<in> HNatInfinite \<Longrightarrow> (0::'a::linordered_semidom star) < of_hypnat N" |
422 by (rule ccontr, simp add: linorder_not_less) |
422 by (rule ccontr, simp add: linorder_not_less) |
423 |
423 |
424 end |
424 end |