# HG changeset patch
# User huffman
# Date 1274147999 25200
# Node ID 71c8973a604b7c65100a98eec0a21b83b0670368
# Parent  e78d1e06d855f77927b337ef091fda32b3ff767c
declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)

diff -r e78d1e06d855 -r 71c8973a604b src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Mon May 17 18:51:25 2010 -0700
+++ b/src/HOL/Big_Operators.thy	Mon May 17 18:59:59 2010 -0700
@@ -673,7 +673,7 @@
   proof induct
     case empty thus ?case by simp
   next
-    case (insert x A) thus ?case by (auto simp: add_nonneg_nonneg)
+    case (insert x A) thus ?case by auto
   qed
 next
   case False thus ?thesis by (simp add: setsum_def)
diff -r e78d1e06d855 -r 71c8973a604b src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Mon May 17 18:51:25 2010 -0700
+++ b/src/HOL/Groups.thy	Mon May 17 18:59:59 2010 -0700
@@ -605,7 +605,7 @@
   then show ?thesis by simp
 qed
 
-lemma add_nonneg_nonneg:
+lemma add_nonneg_nonneg [simp]:
   assumes "0 \<le> a" and "0 \<le> b" shows "0 \<le> a + b"
 proof -
   have "0 + 0 \<le> a + b" 
diff -r e78d1e06d855 -r 71c8973a604b src/HOL/NSA/NSCA.thy
--- a/src/HOL/NSA/NSCA.thy	Mon May 17 18:51:25 2010 -0700
+++ b/src/HOL/NSA/NSCA.thy	Mon May 17 18:59:59 2010 -0700
@@ -279,13 +279,9 @@
   "\<lbrakk>x \<in> Infinitesimal; y \<in> Infinitesimal\<rbrakk> \<Longrightarrow> HComplex x y \<in> Infinitesimal"
 apply (rule Infinitesimal_hcmod_iff [THEN iffD2])
 apply (simp add: hcmod_i)
-apply (rule Infinitesimal_sqrt)
 apply (rule Infinitesimal_add)
 apply (erule Infinitesimal_hrealpow, simp)
 apply (erule Infinitesimal_hrealpow, simp)
-apply (rule add_nonneg_nonneg)
-apply (rule zero_le_power2)
-apply (rule zero_le_power2)
 done
 
 lemma hcomplex_Infinitesimal_iff:
diff -r e78d1e06d855 -r 71c8973a604b src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon May 17 18:51:25 2010 -0700
+++ b/src/HOL/Nat.thy	Mon May 17 18:59:59 2010 -0700
@@ -1294,15 +1294,11 @@
 begin
 
 lemma zero_le_imp_of_nat: "0 \<le> of_nat m"
-  apply (induct m, simp_all)
-  apply (erule order_trans)
-  apply (rule ord_le_eq_trans [OF _ add_commute])
-  apply (rule less_add_one [THEN less_imp_le])
-  done
+  by (induct m) 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 (insert add_less_le_mono [OF zero_less_one zero_le_imp_of_nat], force)
+  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"
diff -r e78d1e06d855 -r 71c8973a604b src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Mon May 17 18:51:25 2010 -0700
+++ b/src/HOL/RealDef.thy	Mon May 17 18:59:59 2010 -0700
@@ -1620,14 +1620,6 @@
      "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
 by (rule sum_power2_eq_zero_iff)
 
-text {* FIXME: declare this [simp] for all types, or not at all *}
-lemma realpow_two_le_add_order [simp]: "(0::real) \<le> u ^ 2 + v ^ 2"
-by (rule sum_power2_ge_zero)
-
-text {* FIXME: declare this [simp] for all types, or not at all *}
-lemma realpow_two_le_add_order2 [simp]: "(0::real) \<le> u ^ 2 + v ^ 2 + w ^ 2"
-by (intro add_nonneg_nonneg zero_le_power2)
-
 lemma real_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))"
 by (rule_tac y = 0 in order_trans, auto)
 
diff -r e78d1e06d855 -r 71c8973a604b src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Mon May 17 18:51:25 2010 -0700
+++ b/src/HOL/Rings.thy	Mon May 17 18:59:59 2010 -0700
@@ -956,7 +956,7 @@
   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
     by (auto simp add: abs_if not_less)
     (auto simp del: minus_add_distrib simp add: minus_add_distrib [symmetric],
-     auto intro: add_nonneg_nonneg, auto intro!: less_imp_le add_neg_neg)
+     auto intro!: less_imp_le add_neg_neg)
 qed (auto simp add: abs_if)
 
 lemma zero_le_square [simp]: "0 \<le> a * a"