# HG changeset patch
# User nipkow
# Date 1397216217 -7200
# Node ID aefb4a8da31fb91b75d80c0ddf5ff6db3a22623b
# Parent  34023a586608dc7fcf21a927cd8c5a62dc79cd37
made mult_nonneg_nonneg a simp rule

diff -r 34023a586608 -r aefb4a8da31f src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -779,7 +779,7 @@
       also have "\<dots> \<le> cos x"
       proof -
         from even[OF `even n`] `0 < ?fact` `0 < ?pow`
-        have "0 \<le> (?rest / ?fact) * ?pow" by (metis mult_nonneg_nonneg divide_nonneg_pos less_imp_le)
+        have "0 \<le> (?rest / ?fact) * ?pow" by (simp add: divide_nonneg_pos)
         thus ?thesis unfolding cos_eq by auto
       qed
       finally have "(lb_sin_cos_aux prec n 1 1 (x * x)) \<le> cos x" .
@@ -893,7 +893,7 @@
       also have "\<dots> \<le> sin x"
       proof -
         from even[OF `even n`] `0 < ?fact` `0 < ?pow`
-        have "0 \<le> (?rest / ?fact) * ?pow" by (metis mult_nonneg_nonneg divide_nonneg_pos less_imp_le)
+        have "0 \<le> (?rest / ?fact) * ?pow" by (simp add: divide_nonneg_pos less_imp_le)
         thus ?thesis unfolding sin_eq by auto
       qed
       finally have "(x * lb_sin_cos_aux prec n 2 1 (x * x)) \<le> sin x" .
@@ -1346,9 +1346,8 @@
       obtain t where "\<bar>t\<bar> \<le> \<bar>real x\<bar>" and "exp x = (\<Sum>m = 0..<get_even n. real x ^ m / real (fact m)) + exp t / real (fact (get_even n)) * (real x) ^ (get_even n)"
         using Maclaurin_exp_le unfolding atLeast0LessThan by blast
       moreover have "0 \<le> exp t / real (fact (get_even n)) * (real x) ^ (get_even n)"
-        by (auto intro!: mult_nonneg_nonneg divide_nonneg_pos simp add: zero_le_even_power)
-      ultimately show ?thesis
-        using get_odd exp_gt_zero by (auto intro!: mult_nonneg_nonneg)
+        by (auto simp: divide_nonneg_pos zero_le_even_power)
+      ultimately show ?thesis using get_odd exp_gt_zero by auto
     qed
     finally have "lb_exp_horner prec (get_even n) 1 1 x \<le> exp x" .
   } moreover
@@ -1368,7 +1367,7 @@
     moreover have "exp t / real (fact (get_odd n)) * (real x) ^ (get_odd n) \<le> 0"
       by (auto intro!: mult_nonneg_nonpos divide_nonpos_pos simp add: x_less_zero)
     ultimately have "exp x \<le> (\<Sum>j = 0..<get_odd n. 1 / real (fact j) * real x ^ j)"
-      using get_odd exp_gt_zero by (auto intro!: mult_nonneg_nonneg)
+      using get_odd exp_gt_zero by auto
     also have "\<dots> \<le> ub_exp_horner prec (get_odd n) 1 1 x"
       using bounds(2) by auto
     finally have "exp x \<le> ub_exp_horner prec (get_odd n) 1 1 x" .
@@ -1594,12 +1593,12 @@
   have "norm x < 1" using assms by auto
   have "?a ----> 0" unfolding Suc_eq_plus1[symmetric] inverse_eq_divide[symmetric]
     using tendsto_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_Suc[OF LIMSEQ_power_zero[OF `norm x < 1`]]] by auto
-  { fix n have "0 \<le> ?a n" by (rule mult_nonneg_nonneg, auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`) }
+  { fix n have "0 \<le> ?a n" by (rule mult_nonneg_nonneg, auto simp: `0 \<le> x`) }
   { fix n have "?a (Suc n) \<le> ?a n" unfolding inverse_eq_divide[symmetric]
     proof (rule mult_mono)
-      show "0 \<le> x ^ Suc (Suc n)" by (auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`)
+      show "0 \<le> x ^ Suc (Suc n)" by (auto simp add: `0 \<le> x`)
       have "x ^ Suc (Suc n) \<le> x ^ Suc n * 1" unfolding power_Suc2 mult_assoc[symmetric]
-        by (rule mult_left_mono, fact less_imp_le[OF `x < 1`], auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`)
+        by (rule mult_left_mono, fact less_imp_le[OF `x < 1`], auto simp: `0 \<le> x`)
       thus "x ^ Suc (Suc n) \<le> x ^ Suc n" by auto
     qed auto }
   from summable_Leibniz'(2,4)[OF `?a ----> 0` `\<And>n. 0 \<le> ?a n`, OF `\<And>n. ?a (Suc n) \<le> ?a n`, unfolded ln_eq]
diff -r 34023a586608 -r aefb4a8da31f src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/Groups_Big.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -1240,7 +1240,7 @@
 
 lemma setprod_nonneg [rule_format]:
    "(ALL x: A. (0::'a::linordered_semidom) \<le> f x) --> 0 \<le> setprod f A"
-by (cases "finite A", induct set: finite, simp_all add: mult_nonneg_nonneg)
+by (cases "finite A", induct set: finite, simp_all)
 
 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::linordered_semidom) < f x)
   --> 0 < setprod f A"
@@ -1318,7 +1318,7 @@
     thus "setprod f (insert a F) \<le> setprod g (insert a F)" "0 \<le> setprod f (insert a F)"
       unfolding setprod_insert[OF insert(1,3)]
       using assms[rule_format,OF insert(2)] insert
-      by (auto intro: mult_mono mult_nonneg_nonneg)
+      by (auto intro: mult_mono)
   qed auto
   thus ?thesis by simp
 qed auto
diff -r 34023a586608 -r aefb4a8da31f src/HOL/Library/BigO.thy
--- a/src/HOL/Library/BigO.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/Library/BigO.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -115,7 +115,6 @@
   apply (rule conjI)
   apply (rule_tac x = "c + c" in exI)
   apply (clarsimp)
-  apply (auto)
   apply (subgoal_tac "c * abs (f xa + g xa) \<le> (c + c) * abs (f xa)")
   apply (erule_tac x = xa in allE)
   apply (erule order_trans)
@@ -126,8 +125,6 @@
   apply (rule mult_left_mono)
   apply (simp add: abs_triangle_ineq)
   apply (simp add: order_less_le)
-  apply (rule mult_nonneg_nonneg)
-  apply auto
   apply (rule_tac x = "\<lambda>n. if (abs (f n)) < abs (g n) then x n else 0" in exI)
   apply (rule conjI)
   apply (rule_tac x = "c + c" in exI)
@@ -142,9 +139,6 @@
   apply (rule mult_left_mono)
   apply (rule abs_triangle_ineq)
   apply (simp add: order_less_le)
-  apply (rule mult_nonneg_nonneg)
-  apply (erule order_less_imp_le)
-  apply simp
   done
 
 lemma bigo_plus_subset2 [intro]: "A \<subseteq> O(f) \<Longrightarrow> B \<subseteq> O(f) \<Longrightarrow> A + B \<subseteq> O(f)"
@@ -293,7 +287,6 @@
   apply (subst abs_mult)
   apply (rule mult_mono)
   apply assumption+
-  apply (rule mult_nonneg_nonneg)
   apply auto
   apply (simp add: mult_ac abs_mult)
   done
@@ -651,7 +644,6 @@
   apply (rule ext)
   apply (rule setsum_cong2)
   apply (subst abs_of_nonneg)
-  apply (rule mult_nonneg_nonneg)
   apply auto
   done
 
@@ -705,9 +697,6 @@
   apply auto
   apply (case_tac "x = 0")
   apply simp
-  apply (rule mult_nonneg_nonneg)
-  apply force
-  apply force
   apply (subgoal_tac "x = Suc (x - 1)")
   apply (erule ssubst) back
   apply (erule spec)
diff -r 34023a586608 -r aefb4a8da31f src/HOL/Library/Convex.thy
--- a/src/HOL/Library/Convex.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/Library/Convex.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -606,7 +606,7 @@
     have "z3 \<in> C" using z3 asm atMostAtLeast_subset_convex
       `convex C` `x \<in> C` `z1 \<in> C` `x < z1` by fastforce
     then have B': "f'' z3 \<ge> 0" using assms by auto
-    from A' B' have "(y - z1) * f'' z3 \<ge> 0" using mult_nonneg_nonneg by auto
+    from A' B' have "(y - z1) * f'' z3 \<ge> 0" by auto
     from cool' this have "f' y - (f x - f y) / (x - y) \<ge> 0" by auto
     from mult_right_mono_neg[OF this le(2)]
     have "f' y * (x - y) - (f x - f y) / (x - y) * (x - y) \<le> 0 * (x - y)"
@@ -621,7 +621,7 @@
     have "z2 \<in> C" using z2 z1 asm atMostAtLeast_subset_convex
       `convex C` `z1 \<in> C` `y \<in> C` `z1 < y` by fastforce
     then have B: "f'' z2 \<ge> 0" using assms by auto
-    from A B have "(z1 - x) * f'' z2 \<ge> 0" using mult_nonneg_nonneg by auto
+    from A B have "(z1 - x) * f'' z2 \<ge> 0" by auto
     from cool this have "(f y - f x) / (y - x) - f' x \<ge> 0" by auto
     from mult_right_mono[OF this ge(2)]
     have "(f y - f x) / (y - x) * (y - x) - f' x * (y - x) \<ge> 0 * (y - x)"
diff -r 34023a586608 -r aefb4a8da31f src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -717,7 +717,7 @@
   by (simp add: one_ereal_def zero_ereal_def)
 
 lemma ereal_0_le_mult[simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * (b :: ereal)"
-  by (cases rule: ereal2_cases[of a b]) (auto simp: mult_nonneg_nonneg)
+  by (cases rule: ereal2_cases[of a b]) auto
 
 lemma ereal_right_distrib:
   fixes r a b :: ereal
diff -r 34023a586608 -r aefb4a8da31f src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/Library/Float.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -618,7 +618,7 @@
   using round_up_correct[of e f] by simp
 
 lemma round_down_nonneg: "0 \<le> s \<Longrightarrow> 0 \<le> round_down p s"
-  by (auto simp: round_down_def intro!: mult_nonneg_nonneg)
+  by (auto simp: round_down_def)
 
 lemma ceil_divide_floor_conv:
 assumes "b \<noteq> 0"
@@ -1418,20 +1418,20 @@
     by simp
   moreover
   have "0 \<le> \<lfloor>x * 2 powr (- real \<lfloor>log 2 x\<rfloor> - 1)\<rfloor>"
-    using `x > 0` by (auto intro: mult_nonneg_nonneg)
+    using `x > 0` by auto
   ultimately have "\<lfloor>x * 2 powr (- real \<lfloor>log 2 x\<rfloor> - 1)\<rfloor> \<in> {0 ..< 1}"
     by simp
   also have "\<dots> \<subseteq> {0}" by auto
   finally have "\<lfloor>x * 2 powr (- real \<lfloor>log 2 x\<rfloor> - 1)\<rfloor> = 0" by simp
   with assms show ?thesis
-    by (auto simp: truncate_down_def round_down_def intro!: mult_nonneg_nonneg)
+    by (auto simp: truncate_down_def round_down_def)
 qed
 
 lemma truncate_down_nonneg: "0 \<le> y \<Longrightarrow> 0 \<le> truncate_down prec y"
-  by (auto simp: truncate_down_def round_down_def intro!: mult_nonneg_nonneg)
+  by (auto simp: truncate_down_def round_down_def)
 
 lemma truncate_down_zero: "truncate_down prec 0 = 0"
-  by (auto simp: truncate_down_def round_down_def intro!: mult_nonneg_nonneg)
+  by (auto simp: truncate_down_def round_down_def)
 
 lemma truncate_down_switch_sign_mono:
   assumes "x \<le> 0" "0 \<le> y"
@@ -1485,7 +1485,7 @@
       by simp
     also have "\<dots> \<le> y * 2 powr real prec / (2 powr (real \<lfloor>log 2 y\<rfloor> + 1))"
       using `0 \<le> y` `0 \<le> x` assms(2)
-      by (auto intro!: powr_mono mult_nonneg_nonneg mult_pos_pos divide_left_mono
+      by (auto intro!: powr_mono mult_pos_pos divide_left_mono
         simp: real_of_nat_diff powr_add
         powr_divide2[symmetric])
     also have "\<dots> = y * 2 powr real prec / (2 powr real \<lfloor>log 2 y\<rfloor> * 2)"
diff -r 34023a586608 -r aefb4a8da31f src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/Library/Product_Vector.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -446,7 +446,6 @@
   shows "sqrt (x + y) \<le> sqrt x + sqrt y"
 apply (rule power2_le_imp_le)
 apply (simp add: power2_sum x y)
-apply (simp add: mult_nonneg_nonneg x y)
 apply (simp add: x y)
 done
 
diff -r 34023a586608 -r aefb4a8da31f src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Fri Apr 11 13:36:57 2014 +0200
@@ -1047,8 +1047,11 @@
 fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i);
 
 fun sos_tac print_cert prover ctxt =
-  Object_Logic.full_atomize_tac ctxt THEN'
-  elim_denom_tac ctxt THEN'
-  core_sos_tac print_cert prover ctxt;
+  (* The SOS prover breaks if mult_nonneg_nonneg is in the simpset *)
+  let val ctxt' = ctxt delsimps [@{thm mult_nonneg_nonneg}]
+  in Object_Logic.full_atomize_tac ctxt' THEN'
+     elim_denom_tac ctxt' THEN'
+     core_sos_tac print_cert prover ctxt'
+  end;
 
 end;
diff -r 34023a586608 -r aefb4a8da31f src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/Limits.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -1239,7 +1239,7 @@
 proof (induct n)
   case (Suc n)
   have "real (Suc n) * x + 1 \<le> (x + 1) * (real n * x + 1)"
-    by (simp add: field_simps real_of_nat_Suc mult_nonneg_nonneg x)
+    by (simp add: field_simps real_of_nat_Suc x)
   also have "\<dots> \<le> (x + 1)^Suc n"
     using Suc x by (simp add: mult_left_mono)
   finally show ?case .
diff -r 34023a586608 -r aefb4a8da31f src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/MacLaurin.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -575,8 +575,7 @@
     apply (rule setsum_cong[OF refl])
     apply (subst diff_m_0, simp)
     apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono
-                simp add: est mult_nonneg_nonneg mult_ac divide_inverse
-                          power_abs [symmetric] abs_mult)
+                simp add: est mult_ac divide_inverse power_abs [symmetric] abs_mult)
     done
 qed
 
diff -r 34023a586608 -r aefb4a8da31f src/HOL/Metis_Examples/Big_O.thy
--- a/src/HOL/Metis_Examples/Big_O.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/Metis_Examples/Big_O.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -164,28 +164,24 @@
 apply (rule conjI)
  apply (rule_tac x = "c + c" in exI)
  apply clarsimp
- apply auto
-  apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (f xa)")
-   apply (metis mult_2 order_trans)
-  apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
-   apply (erule order_trans)
-   apply (simp add: ring_distribs)
-  apply (rule mult_left_mono)
-   apply (simp add: abs_triangle_ineq)
-  apply (simp add: order_less_le)
- apply (rule mult_nonneg_nonneg)
-  apply auto
+ apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (f xa)")
+  apply (metis mult_2 order_trans)
+ apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
+  apply (erule order_trans)
+  apply (simp add: ring_distribs)
+ apply (rule mult_left_mono)
+  apply (simp add: abs_triangle_ineq)
+ apply (simp add: order_less_le)
 apply (rule_tac x = "\<lambda>n. if (abs (f n)) < abs (g n) then x n else 0" in exI)
 apply (rule conjI)
  apply (rule_tac x = "c + c" in exI)
  apply auto
- apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (g xa)")
-  apply (metis order_trans mult_2)
- apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
-  apply (erule order_trans)
-  apply (simp add: ring_distribs)
- apply (metis abs_triangle_ineq mult_le_cancel_left_pos)
-by (metis abs_ge_zero abs_of_pos zero_le_mult_iff)
+apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (g xa)")
+ apply (metis order_trans mult_2)
+apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
+ apply (erule order_trans)
+ apply (simp add: ring_distribs)
+by (metis abs_triangle_ineq mult_le_cancel_left_pos)
 
 lemma bigo_plus_subset2 [intro]: "A <= O(f) \<Longrightarrow> B <= O(f) \<Longrightarrow> A + B <= O(f)"
 by (metis bigo_plus_idemp set_plus_mono2)
@@ -713,6 +709,6 @@
 lemma bigo_lesso5: "f <o g =o O(h) \<Longrightarrow> \<exists>C. \<forall>x. f x <= g x + C * abs (h x)"
 apply (simp only: lesso_def bigo_alt_def)
 apply clarsimp
-by (metis abs_if abs_mult add_commute diff_le_eq less_not_permute)
+by (metis add_commute diff_le_eq)
 
 end
diff -r 34023a586608 -r aefb4a8da31f src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -1173,8 +1173,7 @@
     then have "c *\<^sub>R x = (c * cx) *\<^sub>R xx"
       using x by (simp add: algebra_simps)
     moreover
-    have "c * cx \<ge> 0"
-      using c x using mult_nonneg_nonneg by auto
+    have "c * cx \<ge> 0" using c x by auto
     ultimately
     have "c *\<^sub>R x \<in> ?rhs" using x by auto
   }
@@ -1603,13 +1602,7 @@
         by simp
       finally have **:"1 - (u * u1 + v * u2) = u * v1 + v * v2" by auto
       have "0 \<le> u * v1 + v * v2" "0 \<le> u * v1" "0 \<le> u * v1 + v * v2" "0 \<le> v * v2"
-        apply (rule add_nonneg_nonneg)
-        prefer 4
-        apply (rule add_nonneg_nonneg)
-        apply (rule_tac [!] mult_nonneg_nonneg)
-        using as(1,2) obt1(1,2) obt2(1,2)
-        apply auto
-        done
+        using as(1,2) obt1(1,2) obt2(1,2) by auto
       then show ?thesis
         unfolding obt1(5) obt2(5)
         unfolding * and **
@@ -1643,7 +1636,7 @@
       apply (rule_tac x="1 - u * u1 - v * u2" in exI)
       unfolding Bex_def
       using as(1,2) obt1(1,2) obt2(1,2) **
-      apply (auto intro!: mult_nonneg_nonneg add_nonneg_nonneg simp add: algebra_simps)
+      apply (auto simp add: algebra_simps)
       done
   qed
 qed
@@ -1728,19 +1721,15 @@
     proof (cases "i\<in>{1..k1}")
       case True
       then show ?thesis
-        using mult_nonneg_nonneg[of u "u1 i"] and uv(1) x(1)[THEN bspec[where x=i]]
-        by auto
+        using uv(1) x(1)[THEN bspec[where x=i]] by auto
     next
       case False
       def j \<equiv> "i - k1"
       from i False have "j \<in> {1..k2}"
         unfolding j_def by auto
       then show ?thesis
-        unfolding j_def[symmetric]
-        using False
-        using mult_nonneg_nonneg[of v "u2 j"] and uv(2) y(1)[THEN bspec[where x=j]]
-        apply auto
-        done
+        using False uv(2) y(1)[THEN bspec[where x=j]]
+        by (auto simp: j_def[symmetric])
     qed
   qed (auto simp add: not_le x(2,3) y(2,3) uv(3))
 qed
@@ -1770,9 +1759,7 @@
     assume "x\<in>s"
     then have "0 \<le> u * ux x + v * uy x"
       using ux(1)[THEN bspec[where x=x]] uy(1)[THEN bspec[where x=x]] and uv(1,2)
-      apply auto
-      apply (metis add_nonneg_nonneg mult_nonneg_nonneg uv(1) uv(2))
-      done
+      by auto
   }
   moreover
   have "(\<Sum>x\<in>s. u * ux x + v * uy x) = 1"
@@ -2290,14 +2277,7 @@
       show "0 \<le> u v + t * w v"
       proof (cases "w v < 0")
         case False
-        then show ?thesis
-          apply (rule_tac add_nonneg_nonneg)
-          using v
-          apply simp
-          apply (rule mult_nonneg_nonneg)
-          using `t\<ge>0`
-          apply auto
-          done
+        thus ?thesis using v `t\<ge>0` by auto
       next
         case True
         then have "t \<le> u v / (- w v)"
@@ -4585,13 +4565,7 @@
       apply (rule_tac x = "inverse(norm a) *\<^sub>R a" in exI)
       using hull_subset[of c convex]
       unfolding subset_eq and inner_scaleR
-      apply -
-      apply rule
-      defer
-      apply rule
-      apply (rule mult_nonneg_nonneg)
-      apply (auto simp add: inner_commute del: ballE elim!: ballE)
-      done
+      by (auto simp add: inner_commute del: ballE elim!: ballE)
     then show "frontier (cball 0 1) \<inter> \<Inter>f \<noteq> {}"
       unfolding c(1) frontier_cball dist_norm by auto
   qed (insert closed_halfspace_ge, auto)
@@ -5981,8 +5955,7 @@
       using assms as(1)[unfolded mem_box]
       apply (erule_tac x=i in ballE)
       apply rule
-      apply (rule mult_nonneg_nonneg)
-      prefer 3
+      prefer 2
       apply (rule mult_right_le_one_le)
       using assms
       apply auto
@@ -8481,7 +8454,7 @@
       by auto
     def e \<equiv> "\<lambda>i. u * c i + v * d i"
     have ge0: "\<forall>i\<in>I. e i \<ge> 0"
-      using e_def xc yc uv by (simp add: mult_nonneg_nonneg)
+      using e_def xc yc uv by simp
     have "setsum (\<lambda>i. u * c i) I = u * setsum c I"
       by (simp add: setsum_right_distrib)
     moreover have "setsum (\<lambda>i. v * d i) I = v * setsum d I"
@@ -8502,7 +8475,7 @@
           using mem_convex_alt[of "S i" "s i" "t i" "u * (c i)" "v * (d i)"]
             mult_nonneg_nonneg[of u "c i"] mult_nonneg_nonneg[of v "d i"]
             assms q_def e_def i False xc yc uv
-          by auto
+          by (auto simp del: mult_nonneg_nonneg)
       qed
     }
     then have qs: "\<forall>i\<in>I. q i \<in> S i" by auto
@@ -8513,7 +8486,7 @@
       proof (cases "e i = 0")
         case True
         have ge: "u * (c i) \<ge> 0 \<and> v * d i \<ge> 0"
-          using xc yc uv i by (simp add: mult_nonneg_nonneg)
+          using xc yc uv i by simp
         moreover from ge have "u * c i \<le> 0 \<and> v * d i \<le> 0"
           using True e_def i by simp
         ultimately have "u * c i = 0 \<and> v * d i = 0" by auto
diff -r 34023a586608 -r aefb4a8da31f src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -5986,9 +5986,8 @@
         apply (rule setsum_nonneg)
         apply safe
         unfolding real_scaleR_def
-        apply (rule mult_nonneg_nonneg)
         apply (drule tagged_division_ofD(4)[OF q(1)])
-        apply auto
+        apply (auto intro: mult_nonneg_nonneg)
         done
       have **: "\<And>f g s t. finite s \<Longrightarrow> finite t \<Longrightarrow> (\<forall>(x,y) \<in> t. (0::real) \<le> g(x,y)) \<Longrightarrow>
         (\<forall>y\<in>s. \<exists>x. (x,y) \<in> t \<and> f(y) \<le> g(x,y)) \<Longrightarrow> setsum f s \<le> setsum g t"
@@ -6022,12 +6021,8 @@
         assume as'': "(a, b) \<in> q i"
         show "0 \<le> (real i + 1) * (content b *\<^sub>R indicator s a)"
           unfolding real_scaleR_def
-          apply (rule mult_nonneg_nonneg)
-          defer
-          apply (rule mult_nonneg_nonneg)
           using tagged_division_ofD(4)[OF q(1) as'']
-          apply auto
-          done
+          by (auto intro!: mult_nonneg_nonneg)
       next
         fix i :: nat
         show "finite (q i)"
@@ -7818,11 +7813,7 @@
     have "\<exists>l. 0 < l \<and> norm(l *\<^sub>R f' a) \<le> (e * (b - a)) / 8"
     proof (cases "f' a = 0")
       case True
-      then show ?thesis
-        apply (rule_tac x=1 in exI)
-        using ab e
-        apply (auto intro!:mult_nonneg_nonneg)
-        done
+      thus ?thesis using ab e by auto
     next
       case False
       then show ?thesis
@@ -7885,11 +7876,7 @@
     have "\<exists>l. 0 < l \<and> norm (l *\<^sub>R f' b) \<le> (e * (b - a)) / 8"
     proof (cases "f' b = 0")
       case True
-      then show ?thesis
-        apply (rule_tac x=1 in exI)
-        using ab e
-        apply (auto intro!: mult_nonneg_nonneg)
-        done
+      thus ?thesis using ab e by auto
     next
       case False
       then show ?thesis
diff -r 34023a586608 -r aefb4a8da31f src/HOL/Multivariate_Analysis/L2_Norm.thy
--- a/src/HOL/Multivariate_Analysis/L2_Norm.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/L2_Norm.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -109,7 +109,7 @@
 lemma sqrt_sum_squares_le_sum:
   "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) \<le> x + y"
   apply (rule power2_le_imp_le)
-  apply (simp add: power2_sum mult_nonneg_nonneg)
+  apply (simp add: power2_sum)
   apply simp
   done
 
@@ -127,7 +127,7 @@
 
 lemma sqrt_sum_squares_le_sum_abs: "sqrt (x\<^sup>2 + y\<^sup>2) \<le> \<bar>x\<bar> + \<bar>y\<bar>"
   apply (rule power2_le_imp_le)
-  apply (simp add: power2_sum mult_nonneg_nonneg)
+  apply (simp add: power2_sum)
   apply simp
   done
 
@@ -162,15 +162,13 @@
   apply (rule order_trans)
   apply (rule power_mono)
   apply (erule add_left_mono)
-  apply (simp add: mult_nonneg_nonneg setsum_nonneg)
+  apply (simp add: setsum_nonneg)
   apply (simp add: power2_sum)
   apply (simp add: power_mult_distrib)
   apply (simp add: distrib_left distrib_right)
   apply (rule ord_le_eq_trans)
   apply (rule setL2_mult_ineq_lemma)
-  apply simp
-  apply (intro mult_nonneg_nonneg setL2_nonneg)
-  apply simp
+  apply simp_all
   done
 
 lemma member_le_setL2: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> setL2 f A"
diff -r 34023a586608 -r aefb4a8da31f src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -487,7 +487,7 @@
   shows "x \<le> y + z"
 proof -
   have "y\<^sup>2 + z\<^sup>2 \<le> y\<^sup>2 + 2 * y * z + z\<^sup>2"
-    using z y by (simp add: mult_nonneg_nonneg)
+    using z y by simp
   with xy have th: "x\<^sup>2 \<le> (y + z)\<^sup>2"
     by (simp add: power2_eq_square field_simps)
   from y z have yz: "y + z \<ge> 0"
diff -r 34023a586608 -r aefb4a8da31f src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/NthRoot.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -602,7 +602,7 @@
 apply (rule_tac b="(a * d - b * c)\<^sup>2" in ord_le_eq_trans)
 apply (rule zero_le_power2)
 apply (simp add: power2_diff power_mult_distrib)
-apply (simp add: mult_nonneg_nonneg)
+apply (simp)
 apply simp
 apply (simp add: add_increasing)
 done
diff -r 34023a586608 -r aefb4a8da31f src/HOL/Power.thy
--- a/src/HOL/Power.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/Power.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -301,7 +301,7 @@
 
 lemma zero_le_power [simp]:
   "0 \<le> a \<Longrightarrow> 0 \<le> a ^ n"
-  by (induct n) (simp_all add: mult_nonneg_nonneg)
+  by (induct n) simp_all
 
 lemma power_mono:
   "a \<le> b \<Longrightarrow> 0 \<le> a \<Longrightarrow> a ^ n \<le> b ^ n"
diff -r 34023a586608 -r aefb4a8da31f src/HOL/Probability/Distributions.thy
--- a/src/HOL/Probability/Distributions.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/Probability/Distributions.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -148,7 +148,7 @@
   show "emeasure M {x\<in>space M. X x \<le> a} = ereal (if 0 \<le> a then 1 - exp (- a * l) else 0)"
     using X_distr[of a] eq_0 by (auto simp: one_ereal_def)
   show "AE x in lborel. 0 \<le> exponential_density l x "
-    by (auto simp: exponential_density_def intro!: AE_I2 mult_nonneg_nonneg)
+    by (auto simp: exponential_density_def)
 qed simp_all
 
 lemma (in prob_space) exponential_distributed_iff:
diff -r 34023a586608 -r aefb4a8da31f src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/Probability/Information.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -622,7 +622,7 @@
       subdensity_real[OF measurable_snd Pxy Py Y]
       distributed_real_AE[OF Pxy]
     by eventually_elim
-       (auto simp: f_def log_divide_eq log_mult_eq field_simps zero_less_mult_iff mult_nonneg_nonneg)
+       (auto simp: f_def log_divide_eq log_mult_eq field_simps zero_less_mult_iff)
 
   show "0 \<le> ?M" unfolding M
   proof (rule ST.KL_density_density_nonneg
@@ -1102,7 +1102,7 @@
     apply (rule positive_integral_mono_AE)
     using ae5 ae6 ae7 ae8
     apply eventually_elim
-    apply (auto intro!: divide_nonneg_nonneg mult_nonneg_nonneg)
+    apply (auto intro!: divide_nonneg_nonneg)
     done
   also have "\<dots> = (\<integral>\<^sup>+(y, z). \<integral>\<^sup>+ x. ereal (Pxz (x, z)) * ereal (Pyz (y, z) / Pz z) \<partial>S \<partial>T \<Otimes>\<^sub>M P)"
     by (subst STP.positive_integral_snd_measurable[symmetric]) (auto simp add: split_beta')
@@ -1151,7 +1151,7 @@
     apply simp
     using ae5 ae6 ae7 ae8
     apply eventually_elim
-    apply (auto intro!: mult_nonneg_nonneg divide_nonneg_nonneg)
+    apply (auto intro!: divide_nonneg_nonneg)
     done
 
   have I3: "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))))"
@@ -1296,7 +1296,7 @@
     apply (rule integrable_cong_AE_imp)
     using ae1 ae4 ae5 ae6 ae9
     by eventually_elim
-       (auto simp: log_divide_eq log_mult_eq mult_nonneg_nonneg field_simps zero_less_mult_iff)
+       (auto simp: log_divide_eq log_mult_eq field_simps zero_less_mult_iff)
 
   have "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P)
     (\<lambda>x. Pxyz x * log b (Pxz (fst x, snd (snd x))) - Pxyz x * log b (Px (fst x)) - Pxyz x * log b (Pz (snd (snd x))))"
@@ -1311,7 +1311,7 @@
     apply (rule integrable_cong_AE_imp)
     using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 ae9
     by eventually_elim
-       (auto simp: log_divide_eq log_mult_eq mult_nonneg_nonneg field_simps zero_less_mult_iff)
+       (auto simp: log_divide_eq log_mult_eq field_simps zero_less_mult_iff)
 
   from ae I1 I2 show ?eq
     unfolding conditional_mutual_information_def
@@ -1347,7 +1347,7 @@
     apply (rule positive_integral_mono_AE)
     using ae5 ae6 ae7 ae8
     apply eventually_elim
-    apply (auto intro!: divide_nonneg_nonneg mult_nonneg_nonneg)
+    apply (auto intro!: divide_nonneg_nonneg)
     done
   also have "\<dots> = (\<integral>\<^sup>+(y, z). \<integral>\<^sup>+ x. ereal (Pxz (x, z)) * ereal (Pyz (y, z) / Pz z) \<partial>S \<partial>T \<Otimes>\<^sub>M P)"
     by (subst STP.positive_integral_snd_measurable[symmetric])
@@ -1396,7 +1396,7 @@
     apply (auto simp: split_beta') []
     using ae5 ae6 ae7 ae8
     apply eventually_elim
-    apply (auto intro!: mult_nonneg_nonneg divide_nonneg_nonneg)
+    apply (auto intro!: divide_nonneg_nonneg)
     done
 
   have I3: "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))))"
diff -r 34023a586608 -r aefb4a8da31f src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -236,9 +236,9 @@
     proof (split split_if, intro conjI impI)
       assume "\<not> real j \<le> u x"
       then have "natfloor (real (u x) * 2 ^ j) \<le> natfloor (j * 2 ^ j)"
-         by (cases "u x") (auto intro!: natfloor_mono simp: mult_nonneg_nonneg)
+         by (cases "u x") (auto intro!: natfloor_mono)
       moreover have "real (natfloor (j * 2 ^ j)) \<le> j * 2^j"
-        by (intro real_natfloor_le) (auto simp: mult_nonneg_nonneg)
+        by (intro real_natfloor_le) auto
       ultimately show "natfloor (real (u x) * 2 ^ j) \<le> j * 2 ^ j"
         unfolding real_of_nat_le_iff by auto
     qed auto }
@@ -300,7 +300,7 @@
     proof (rule SUP_eqI)
       fix i show "?g i x \<le> max 0 (u x)" unfolding max_def f_def
         by (cases "u x") (auto simp: field_simps real_natfloor_le natfloor_neg
-                                     mult_nonpos_nonneg mult_nonneg_nonneg)
+                                     mult_nonpos_nonneg)
     next
       fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> ?g i x \<le> y"
       have "\<And>i. 0 \<le> ?g i x" by (auto simp: divide_nonneg_pos)
@@ -317,12 +317,12 @@
         proof (rule ccontr)
           assume "\<not> p \<le> r"
           with LIMSEQ_inverse_realpow_zero[unfolded LIMSEQ_iff, rule_format, of 2 "p - r"]
-          obtain N where "\<forall>n\<ge>N. r * 2^n < p * 2^n - 1" by (auto simp: inverse_eq_divide field_simps)
+          obtain N where "\<forall>n\<ge>N. r * 2^n < p * 2^n - 1" by (auto simp: field_simps)
           then have "r * 2^max N m < p * 2^max N m - 1" by simp
           moreover
           have "real (natfloor (p * 2 ^ max N m)) \<le> r * 2 ^ max N m"
             using *[of "max N m"] m unfolding real_f using ux
-            by (cases "0 \<le> u x") (simp_all add: max_def mult_nonneg_nonneg split: split_if_asm)
+            by (cases "0 \<le> u x") (simp_all add: max_def split: split_if_asm)
           then have "p * 2 ^ max N m - 1 < r * 2 ^ max N m"
             by (metis real_natfloor_gt_diff_one less_le_trans)
           ultimately show False by auto
diff -r 34023a586608 -r aefb4a8da31f src/HOL/Real.thy
--- a/src/HOL/Real.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/Real.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -333,7 +333,7 @@
       by (simp add: inverse_diff_inverse abs_mult)
     also have "\<dots> < inverse a * s * inverse b"
       apply (intro mult_strict_mono' less_imp_inverse_less)
-      apply (simp_all add: a b i j k n mult_nonneg_nonneg)
+      apply (simp_all add: a b i j k n)
       done
     also note `inverse a * s * inverse b = r`
     finally show "\<bar>inverse (X n) - inverse (Y n)\<bar> < r" .
@@ -1927,7 +1927,7 @@
 lemma le_mult_natfloor:
   shows "natfloor a * natfloor b \<le> natfloor (a * b)"
   by (cases "0 <= a & 0 <= b")
-    (auto simp add: le_natfloor_eq mult_nonneg_nonneg mult_mono' real_natfloor_le natfloor_neg)
+    (auto simp add: le_natfloor_eq mult_mono' real_natfloor_le natfloor_neg)
 
 lemma natceiling_zero [simp]: "natceiling 0 = 0"
   by (unfold natceiling_def, simp)
diff -r 34023a586608 -r aefb4a8da31f src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/Rings.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -492,7 +492,7 @@
 
 subclass semiring_0_cancel ..
 
-lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
+lemma mult_nonneg_nonneg[simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
 using mult_left_mono [of 0 b a] by simp
 
 lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"
@@ -759,7 +759,7 @@
 
 lemma split_mult_pos_le:
   "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b"
-by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
+by (auto simp add: mult_nonpos_nonpos)
 
 end
 
@@ -777,7 +777,7 @@
 
 lemma zero_le_square [simp]: "0 \<le> a * a"
   using linear [of 0 a]
-  by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
+  by (auto simp add: mult_nonpos_nonpos)
 
 lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
   by (simp add: not_less)
diff -r 34023a586608 -r aefb4a8da31f src/HOL/Series.thy
--- a/src/HOL/Series.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/Series.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -575,8 +575,7 @@
 
   let ?g = "\<lambda>(i,j). a i * b j"
   let ?f = "\<lambda>(i,j). norm (a i) * norm (b j)"
-  have f_nonneg: "\<And>x. 0 \<le> ?f x"
-    by (auto simp add: mult_nonneg_nonneg)
+  have f_nonneg: "\<And>x. 0 \<le> ?f x" by (auto)
   hence norm_setsum_f: "\<And>A. norm (setsum ?f A) = setsum ?f A"
     unfolding real_norm_def
     by (simp only: abs_of_nonneg setsum_nonneg [rule_format])
diff -r 34023a586608 -r aefb4a8da31f src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Fri Apr 11 12:43:22 2014 +0200
+++ b/src/HOL/Transcendental.thy	Fri Apr 11 13:36:57 2014 +0200
@@ -1395,7 +1395,7 @@
       by (simp add: power_inverse)
     hence "inverse (fact (n + 2)) * (x^n * x\<^sup>2) \<le> 1/2 * (1/2)^n * (1 * x\<^sup>2)"
       by (rule mult_mono)
-        (rule mult_mono, simp_all add: power_le_one a b mult_nonneg_nonneg)
+        (rule mult_mono, simp_all add: power_le_one a b)
     hence "inverse (fact (n + 2)) * x ^ (n + 2) \<le> (x\<^sup>2/2) * ((1/2)^n)"
       unfolding power_add by (simp add: mult_ac del: fact_Suc) }
   note aux1 = this