# HG changeset patch
# User huffman
# Date 1274189322 25200
# Node ID 4ec5131c6f4604737928be82f4186b55e49b5a66
# Parent  71c8973a604b7c65100a98eec0a21b83b0670368# Parent  b0033a307d1fcd410cd5b4515871d8d0fb9638a5
merged

diff -r b0033a307d1f -r 4ec5131c6f46 src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Tue May 18 10:13:33 2010 +0200
+++ b/src/HOL/Big_Operators.thy	Tue May 18 06:28:42 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 b0033a307d1f -r 4ec5131c6f46 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Tue May 18 10:13:33 2010 +0200
+++ b/src/HOL/Groups.thy	Tue May 18 06:28:42 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 b0033a307d1f -r 4ec5131c6f46 src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue May 18 10:13:33 2010 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue May 18 06:28:42 2010 -0700
@@ -214,23 +214,8 @@
     hence "\<exists>z. ?P z n" ..}
   moreover
   {assume o: "odd n"
-    from b have b': "b^2 \<noteq> 0" unfolding power2_eq_square by simp
-    have "Im (inverse b) * (Im (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) +
-    Re (inverse b) * (Re (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) =
-    ((Re (inverse b))^2 + (Im (inverse b))^2) * \<bar>Im b * Im b + Re b * Re b\<bar>" by algebra
-    also have "\<dots> = cmod (inverse b) ^2 * cmod b ^ 2"
-      apply (simp add: cmod_def) using realpow_two_le_add_order[of "Re b" "Im b"]
-      by (simp add: power2_eq_square)
-    finally
-    have th0: "Im (inverse b) * (Im (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) +
-    Re (inverse b) * (Re (inverse b) * \<bar>Im b * Im b + Re b * Re b\<bar>) =
-    1"
-      apply (simp add: power2_eq_square norm_mult[symmetric] norm_inverse[symmetric])
-      using right_inverse[OF b']
-      by (simp add: power2_eq_square[symmetric] power_inverse[symmetric] algebra_simps)
     have th0: "cmod (complex_of_real (cmod b) / b) = 1"
-      apply (simp add: complex_Re_mult cmod_def power2_eq_square Re_complex_of_real Im_complex_of_real divide_inverse algebra_simps )
-      by (simp add: real_sqrt_mult[symmetric] th0)
+      using b by (simp add: norm_divide)
     from o have "\<exists>m. n = Suc (2*m)" by presburger+
     then obtain m where m: "n = Suc (2*m)" by blast
     from unimodular_reduce_norm[OF th0] o
diff -r b0033a307d1f -r 4ec5131c6f46 src/HOL/Library/Lattice_Algebras.thy
--- a/src/HOL/Library/Lattice_Algebras.thy	Tue May 18 10:13:33 2010 +0200
+++ b/src/HOL/Library/Lattice_Algebras.thy	Tue May 18 06:28:42 2010 -0700
@@ -405,21 +405,15 @@
       done
   }
   note b = this[OF refl[of a] refl[of b]]
-  note addm = add_mono[of "0::'a" _ "0::'a", simplified]
-  note addm2 = add_mono[of _ "0::'a" _ "0::'a", simplified]
   have xy: "- ?x <= ?y"
     apply (simp)
-    apply (rule_tac y="0::'a" in order_trans)
-    apply (rule addm2)
-    apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
-    apply (rule addm)
+    apply (rule order_trans [OF add_nonpos_nonpos add_nonneg_nonneg])
     apply (simp_all add: mult_nonneg_nonneg mult_nonpos_nonpos)
     done
   have yx: "?y <= ?x"
     apply (simp add:diff_def)
-    apply (rule_tac y=0 in order_trans)
-    apply (rule addm2, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
-    apply (rule addm, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+)
+    apply (rule order_trans [OF add_nonpos_nonpos add_nonneg_nonneg])
+    apply (simp_all add: mult_nonneg_nonpos mult_nonpos_nonneg)
     done
   have i1: "a*b <= abs a * abs b" by (simp only: a b yx)
   have i2: "- (abs a * abs b) <= a*b" by (simp only: a b xy)
diff -r b0033a307d1f -r 4ec5131c6f46 src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Tue May 18 10:13:33 2010 +0200
+++ b/src/HOL/MacLaurin.thy	Tue May 18 06:28:42 2010 -0700
@@ -383,6 +383,11 @@
 
 text{*It is unclear why so many variant results are needed.*}
 
+lemma sin_expansion_lemma:
+     "sin (x + real (Suc m) * pi / 2) =  
+      cos (x + real (m) * pi / 2)"
+by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
+
 lemma Maclaurin_sin_expansion2:
      "\<exists>t. abs t \<le> abs x &
        sin x =
@@ -394,7 +399,7 @@
         and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
 apply safe
 apply (simp (no_asm))
-apply (simp (no_asm))
+apply (simp (no_asm) add: sin_expansion_lemma)
 apply (case_tac "n", clarify, simp, simp add: lemma_STAR_sin)
 apply (rule ccontr, simp)
 apply (drule_tac x = x in spec, simp)
@@ -414,7 +419,6 @@
 apply (blast intro: elim:); 
 done
 
-
 lemma Maclaurin_sin_expansion3:
      "[| n > 0; 0 < x |] ==>
        \<exists>t. 0 < t & t < x &
@@ -426,7 +430,7 @@
 apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin_objl)
 apply safe
 apply simp
-apply (simp (no_asm))
+apply (simp (no_asm) add: sin_expansion_lemma)
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule setsum_cong[OF refl])
@@ -444,7 +448,7 @@
 apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin2_objl)
 apply safe
 apply simp
-apply (simp (no_asm))
+apply (simp (no_asm) add: sin_expansion_lemma)
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule setsum_cong[OF refl])
@@ -459,6 +463,10 @@
      (if even m then -1 ^ (m div 2)/(real  (fact m)) else 0) * 0 ^ m) = 1"
 by (induct "n", auto)
 
+lemma cos_expansion_lemma:
+  "cos (x + real(Suc m) * pi / 2) = -sin (x + real m * pi / 2)"
+by (simp only: cos_add sin_add real_of_nat_Suc left_distrib add_divide_distrib, auto)
+
 lemma Maclaurin_cos_expansion:
      "\<exists>t. abs t \<le> abs x &
        cos x =
@@ -470,7 +478,7 @@
 apply (cut_tac f = cos and n = n and x = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_all_lt_objl)
 apply safe
 apply (simp (no_asm))
-apply (simp (no_asm))
+apply (simp (no_asm) add: cos_expansion_lemma)
 apply (case_tac "n", simp)
 apply (simp del: setsum_op_ivl_Suc)
 apply (rule ccontr, simp)
@@ -493,7 +501,7 @@
 apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_objl)
 apply safe
 apply simp
-apply (simp (no_asm))
+apply (simp (no_asm) add: cos_expansion_lemma)
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule setsum_cong[OF refl])
@@ -512,7 +520,7 @@
 apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_minus_objl)
 apply safe
 apply simp
-apply (simp (no_asm))
+apply (simp (no_asm) add: cos_expansion_lemma)
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule setsum_cong[OF refl])
diff -r b0033a307d1f -r 4ec5131c6f46 src/HOL/NSA/NSCA.thy
--- a/src/HOL/NSA/NSCA.thy	Tue May 18 10:13:33 2010 +0200
+++ b/src/HOL/NSA/NSCA.thy	Tue May 18 06:28:42 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 b0033a307d1f -r 4ec5131c6f46 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue May 18 10:13:33 2010 +0200
+++ b/src/HOL/Nat.thy	Tue May 18 06:28:42 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 b0033a307d1f -r 4ec5131c6f46 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Tue May 18 10:13:33 2010 +0200
+++ b/src/HOL/RealDef.thy	Tue May 18 06:28:42 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 b0033a307d1f -r 4ec5131c6f46 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Tue May 18 10:13:33 2010 +0200
+++ b/src/HOL/Rings.thy	Tue May 18 06:28:42 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"
diff -r b0033a307d1f -r 4ec5131c6f46 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue May 18 10:13:33 2010 +0200
+++ b/src/HOL/Transcendental.thy	Tue May 18 06:28:42 2010 -0700
@@ -2580,18 +2580,6 @@
 lemma tan_60: "tan (pi / 3) = sqrt 3"
 unfolding tan_def by (simp add: sin_60 cos_60)
 
-text{*NEEDED??*}
-lemma [simp]:
-     "sin (x + 1 / 2 * real (Suc m) * pi) =  
-      cos (x + 1 / 2 * real  (m) * pi)"
-by (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib, auto)
-
-text{*NEEDED??*}
-lemma [simp]:
-     "sin (x + real (Suc m) * pi / 2) =  
-      cos (x + real (m) * pi / 2)"
-by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
-
 lemma DERIV_sin_add [simp]: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"
   by (auto intro!: DERIV_intros)
 
@@ -2620,16 +2608,6 @@
 apply (subst sin_add, simp)
 done
 
-(*NEEDED??*)
-lemma [simp]:
-     "cos(x + 1 / 2 * real(Suc m) * pi) = -sin (x + 1 / 2 * real m * pi)"
-apply (simp only: cos_add sin_add real_of_nat_Suc right_distrib left_distrib minus_mult_right, auto)
-done
-
-(*NEEDED??*)
-lemma [simp]: "cos (x + real(Suc m) * pi / 2) = -sin (x + real m * pi / 2)"
-by (simp only: cos_add sin_add real_of_nat_Suc left_distrib add_divide_distrib, auto)
-
 lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
 by (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib add_divide_distrib, auto)