# HG changeset patch
# User huffman
# Date 1334568297 -7200
# Node ID 04e7d09ade7a0e9f182f117232fdf210324b0024
# Parent  be6dd389639df181502747c52ce8239892e7ce00
tuned some proofs;
removed duplicate lemma zero_le_imp_of_nat

diff -r be6dd389639d -r 04e7d09ade7a src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sun Apr 15 20:51:07 2012 +0200
+++ b/src/HOL/Nat.thy	Mon Apr 16 11:24:57 2012 +0200
@@ -1373,26 +1373,24 @@
 context linordered_semidom
 begin
 
-lemma zero_le_imp_of_nat: "0 \<le> of_nat m"
-  by (induct m) simp_all
+lemma of_nat_0_le_iff [simp]: "0 \<le> of_nat n"
+  by (induct n) simp_all
 
-lemma less_imp_of_nat_less: "m < n \<Longrightarrow> of_nat m < of_nat n"
-  apply (induct m n rule: diff_induct, simp_all)
-  apply (rule add_pos_nonneg [OF zero_less_one zero_le_imp_of_nat])
-  done
-
-lemma of_nat_less_imp_less: "of_nat m < of_nat n \<Longrightarrow> m < n"
-  apply (induct m n rule: diff_induct, simp_all)
-  apply (insert zero_le_imp_of_nat)
-  apply (force simp add: not_less [symmetric])
-  done
+lemma of_nat_less_0_iff [simp]: "\<not> of_nat m < 0"
+  by (simp add: not_less)
 
 lemma of_nat_less_iff [simp]: "of_nat m < of_nat n \<longleftrightarrow> m < n"
-  by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
+  by (induct m n rule: diff_induct, simp_all add: add_pos_nonneg)
 
 lemma of_nat_le_iff [simp]: "of_nat m \<le> of_nat n \<longleftrightarrow> m \<le> n"
   by (simp add: not_less [symmetric] linorder_not_less [symmetric])
 
+lemma less_imp_of_nat_less: "m < n \<Longrightarrow> of_nat m < of_nat n"
+  by simp
+
+lemma of_nat_less_imp_less: "of_nat m < of_nat n \<Longrightarrow> m < n"
+  by simp
+
 text{*Every @{text linordered_semidom} has characteristic zero.*}
 
 subclass semiring_char_0 proof
@@ -1400,18 +1398,12 @@
 
 text{*Special cases where either operand is zero*}
 
-lemma of_nat_0_le_iff [simp]: "0 \<le> of_nat n"
-  by (rule of_nat_le_iff [of 0, simplified])
-
 lemma of_nat_le_0_iff [simp, no_atp]: "of_nat m \<le> 0 \<longleftrightarrow> m = 0"
   by (rule of_nat_le_iff [of _ 0, simplified])
 
 lemma of_nat_0_less_iff [simp]: "0 < of_nat n \<longleftrightarrow> 0 < n"
   by (rule of_nat_less_iff [of 0, simplified])
 
-lemma of_nat_less_0_iff [simp]: "\<not> of_nat m < 0"
-  by (rule of_nat_less_iff [of _ 0, simplified])
-
 end
 
 context ring_1
diff -r be6dd389639d -r 04e7d09ade7a src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Sun Apr 15 20:51:07 2012 +0200
+++ b/src/HOL/RealDef.thy	Mon Apr 16 11:24:57 2012 +0200
@@ -1251,7 +1251,7 @@
 by (simp add: real_of_nat_def)
 
 lemma real_of_nat_ge_zero [iff]: "0 \<le> real (n::nat)"
-by (simp add: real_of_nat_def zero_le_imp_of_nat)
+by (simp add: real_of_nat_def)
 
 lemma real_of_nat_Suc_gt_zero: "0 < real (Suc n)"
 by (simp add: real_of_nat_def del: of_nat_Suc)
diff -r be6dd389639d -r 04e7d09ade7a src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sun Apr 15 20:51:07 2012 +0200
+++ b/src/HOL/Transcendental.thy	Mon Apr 16 11:24:57 2012 +0200
@@ -421,7 +421,7 @@
          order_trans [OF norm_setsum]
          real_setsum_nat_ivl_bounded2
          mult_nonneg_nonneg
-         zero_le_imp_of_nat
+         of_nat_0_le_iff
          zero_le_power K)
       apply (rule le_Kn, simp)
       done