src/HOL/Nat.thy
changeset 47489 04e7d09ade7a
parent 47255 30a1692557b0
child 47988 e4b69e10b990
     1.1 --- a/src/HOL/Nat.thy	Sun Apr 15 20:51:07 2012 +0200
     1.2 +++ b/src/HOL/Nat.thy	Mon Apr 16 11:24:57 2012 +0200
     1.3 @@ -1373,26 +1373,24 @@
     1.4  context linordered_semidom
     1.5  begin
     1.6  
     1.7 -lemma zero_le_imp_of_nat: "0 \<le> of_nat m"
     1.8 -  by (induct m) simp_all
     1.9 +lemma of_nat_0_le_iff [simp]: "0 \<le> of_nat n"
    1.10 +  by (induct n) simp_all
    1.11  
    1.12 -lemma less_imp_of_nat_less: "m < n \<Longrightarrow> of_nat m < of_nat n"
    1.13 -  apply (induct m n rule: diff_induct, simp_all)
    1.14 -  apply (rule add_pos_nonneg [OF zero_less_one zero_le_imp_of_nat])
    1.15 -  done
    1.16 -
    1.17 -lemma of_nat_less_imp_less: "of_nat m < of_nat n \<Longrightarrow> m < n"
    1.18 -  apply (induct m n rule: diff_induct, simp_all)
    1.19 -  apply (insert zero_le_imp_of_nat)
    1.20 -  apply (force simp add: not_less [symmetric])
    1.21 -  done
    1.22 +lemma of_nat_less_0_iff [simp]: "\<not> of_nat m < 0"
    1.23 +  by (simp add: not_less)
    1.24  
    1.25  lemma of_nat_less_iff [simp]: "of_nat m < of_nat n \<longleftrightarrow> m < n"
    1.26 -  by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
    1.27 +  by (induct m n rule: diff_induct, simp_all add: add_pos_nonneg)
    1.28  
    1.29  lemma of_nat_le_iff [simp]: "of_nat m \<le> of_nat n \<longleftrightarrow> m \<le> n"
    1.30    by (simp add: not_less [symmetric] linorder_not_less [symmetric])
    1.31  
    1.32 +lemma less_imp_of_nat_less: "m < n \<Longrightarrow> of_nat m < of_nat n"
    1.33 +  by simp
    1.34 +
    1.35 +lemma of_nat_less_imp_less: "of_nat m < of_nat n \<Longrightarrow> m < n"
    1.36 +  by simp
    1.37 +
    1.38  text{*Every @{text linordered_semidom} has characteristic zero.*}
    1.39  
    1.40  subclass semiring_char_0 proof
    1.41 @@ -1400,18 +1398,12 @@
    1.42  
    1.43  text{*Special cases where either operand is zero*}
    1.44  
    1.45 -lemma of_nat_0_le_iff [simp]: "0 \<le> of_nat n"
    1.46 -  by (rule of_nat_le_iff [of 0, simplified])
    1.47 -
    1.48  lemma of_nat_le_0_iff [simp, no_atp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0"
    1.49    by (rule of_nat_le_iff [of _ 0, simplified])
    1.50  
    1.51  lemma of_nat_0_less_iff [simp]: "0 < of_nat n \<longleftrightarrow> 0 < n"
    1.52    by (rule of_nat_less_iff [of 0, simplified])
    1.53  
    1.54 -lemma of_nat_less_0_iff [simp]: "\<not> of_nat m < 0"
    1.55 -  by (rule of_nat_less_iff [of _ 0, simplified])
    1.56 -
    1.57  end
    1.58  
    1.59  context ring_1