made mult_nonneg_nonneg a simp rule
authornipkow
Fri Apr 11 13:36:57 2014 +0200 (2014-04-11)
changeset 56536aefb4a8da31f
parent 56535 34023a586608
child 56537 01caba82e1d2
child 56538 7c3b6b799b94
made mult_nonneg_nonneg a simp rule
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Groups_Big.thy
src/HOL/Library/BigO.thy
src/HOL/Library/Convex.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Float.thy
src/HOL/Library/Product_Vector.thy
src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
src/HOL/Limits.thy
src/HOL/MacLaurin.thy
src/HOL/Metis_Examples/Big_O.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/L2_Norm.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/NthRoot.thy
src/HOL/Power.thy
src/HOL/Probability/Distributions.thy
src/HOL/Probability/Information.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Real.thy
src/HOL/Rings.thy
src/HOL/Series.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Fri Apr 11 12:43:22 2014 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Fri Apr 11 13:36:57 2014 +0200
     1.3 @@ -779,7 +779,7 @@
     1.4        also have "\<dots> \<le> cos x"
     1.5        proof -
     1.6          from even[OF `even n`] `0 < ?fact` `0 < ?pow`
     1.7 -        have "0 \<le> (?rest / ?fact) * ?pow" by (metis mult_nonneg_nonneg divide_nonneg_pos less_imp_le)
     1.8 +        have "0 \<le> (?rest / ?fact) * ?pow" by (simp add: divide_nonneg_pos)
     1.9          thus ?thesis unfolding cos_eq by auto
    1.10        qed
    1.11        finally have "(lb_sin_cos_aux prec n 1 1 (x * x)) \<le> cos x" .
    1.12 @@ -893,7 +893,7 @@
    1.13        also have "\<dots> \<le> sin x"
    1.14        proof -
    1.15          from even[OF `even n`] `0 < ?fact` `0 < ?pow`
    1.16 -        have "0 \<le> (?rest / ?fact) * ?pow" by (metis mult_nonneg_nonneg divide_nonneg_pos less_imp_le)
    1.17 +        have "0 \<le> (?rest / ?fact) * ?pow" by (simp add: divide_nonneg_pos less_imp_le)
    1.18          thus ?thesis unfolding sin_eq by auto
    1.19        qed
    1.20        finally have "(x * lb_sin_cos_aux prec n 2 1 (x * x)) \<le> sin x" .
    1.21 @@ -1346,9 +1346,8 @@
    1.22        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)"
    1.23          using Maclaurin_exp_le unfolding atLeast0LessThan by blast
    1.24        moreover have "0 \<le> exp t / real (fact (get_even n)) * (real x) ^ (get_even n)"
    1.25 -        by (auto intro!: mult_nonneg_nonneg divide_nonneg_pos simp add: zero_le_even_power)
    1.26 -      ultimately show ?thesis
    1.27 -        using get_odd exp_gt_zero by (auto intro!: mult_nonneg_nonneg)
    1.28 +        by (auto simp: divide_nonneg_pos zero_le_even_power)
    1.29 +      ultimately show ?thesis using get_odd exp_gt_zero by auto
    1.30      qed
    1.31      finally have "lb_exp_horner prec (get_even n) 1 1 x \<le> exp x" .
    1.32    } moreover
    1.33 @@ -1368,7 +1367,7 @@
    1.34      moreover have "exp t / real (fact (get_odd n)) * (real x) ^ (get_odd n) \<le> 0"
    1.35        by (auto intro!: mult_nonneg_nonpos divide_nonpos_pos simp add: x_less_zero)
    1.36      ultimately have "exp x \<le> (\<Sum>j = 0..<get_odd n. 1 / real (fact j) * real x ^ j)"
    1.37 -      using get_odd exp_gt_zero by (auto intro!: mult_nonneg_nonneg)
    1.38 +      using get_odd exp_gt_zero by auto
    1.39      also have "\<dots> \<le> ub_exp_horner prec (get_odd n) 1 1 x"
    1.40        using bounds(2) by auto
    1.41      finally have "exp x \<le> ub_exp_horner prec (get_odd n) 1 1 x" .
    1.42 @@ -1594,12 +1593,12 @@
    1.43    have "norm x < 1" using assms by auto
    1.44    have "?a ----> 0" unfolding Suc_eq_plus1[symmetric] inverse_eq_divide[symmetric]
    1.45      using tendsto_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_Suc[OF LIMSEQ_power_zero[OF `norm x < 1`]]] by auto
    1.46 -  { fix n have "0 \<le> ?a n" by (rule mult_nonneg_nonneg, auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`) }
    1.47 +  { fix n have "0 \<le> ?a n" by (rule mult_nonneg_nonneg, auto simp: `0 \<le> x`) }
    1.48    { fix n have "?a (Suc n) \<le> ?a n" unfolding inverse_eq_divide[symmetric]
    1.49      proof (rule mult_mono)
    1.50 -      show "0 \<le> x ^ Suc (Suc n)" by (auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`)
    1.51 +      show "0 \<le> x ^ Suc (Suc n)" by (auto simp add: `0 \<le> x`)
    1.52        have "x ^ Suc (Suc n) \<le> x ^ Suc n * 1" unfolding power_Suc2 mult_assoc[symmetric]
    1.53 -        by (rule mult_left_mono, fact less_imp_le[OF `x < 1`], auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`)
    1.54 +        by (rule mult_left_mono, fact less_imp_le[OF `x < 1`], auto simp: `0 \<le> x`)
    1.55        thus "x ^ Suc (Suc n) \<le> x ^ Suc n" by auto
    1.56      qed auto }
    1.57    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]
     2.1 --- a/src/HOL/Groups_Big.thy	Fri Apr 11 12:43:22 2014 +0200
     2.2 +++ b/src/HOL/Groups_Big.thy	Fri Apr 11 13:36:57 2014 +0200
     2.3 @@ -1240,7 +1240,7 @@
     2.4  
     2.5  lemma setprod_nonneg [rule_format]:
     2.6     "(ALL x: A. (0::'a::linordered_semidom) \<le> f x) --> 0 \<le> setprod f A"
     2.7 -by (cases "finite A", induct set: finite, simp_all add: mult_nonneg_nonneg)
     2.8 +by (cases "finite A", induct set: finite, simp_all)
     2.9  
    2.10  lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::linordered_semidom) < f x)
    2.11    --> 0 < setprod f A"
    2.12 @@ -1318,7 +1318,7 @@
    2.13      thus "setprod f (insert a F) \<le> setprod g (insert a F)" "0 \<le> setprod f (insert a F)"
    2.14        unfolding setprod_insert[OF insert(1,3)]
    2.15        using assms[rule_format,OF insert(2)] insert
    2.16 -      by (auto intro: mult_mono mult_nonneg_nonneg)
    2.17 +      by (auto intro: mult_mono)
    2.18    qed auto
    2.19    thus ?thesis by simp
    2.20  qed auto
     3.1 --- a/src/HOL/Library/BigO.thy	Fri Apr 11 12:43:22 2014 +0200
     3.2 +++ b/src/HOL/Library/BigO.thy	Fri Apr 11 13:36:57 2014 +0200
     3.3 @@ -115,7 +115,6 @@
     3.4    apply (rule conjI)
     3.5    apply (rule_tac x = "c + c" in exI)
     3.6    apply (clarsimp)
     3.7 -  apply (auto)
     3.8    apply (subgoal_tac "c * abs (f xa + g xa) \<le> (c + c) * abs (f xa)")
     3.9    apply (erule_tac x = xa in allE)
    3.10    apply (erule order_trans)
    3.11 @@ -126,8 +125,6 @@
    3.12    apply (rule mult_left_mono)
    3.13    apply (simp add: abs_triangle_ineq)
    3.14    apply (simp add: order_less_le)
    3.15 -  apply (rule mult_nonneg_nonneg)
    3.16 -  apply auto
    3.17    apply (rule_tac x = "\<lambda>n. if (abs (f n)) < abs (g n) then x n else 0" in exI)
    3.18    apply (rule conjI)
    3.19    apply (rule_tac x = "c + c" in exI)
    3.20 @@ -142,9 +139,6 @@
    3.21    apply (rule mult_left_mono)
    3.22    apply (rule abs_triangle_ineq)
    3.23    apply (simp add: order_less_le)
    3.24 -  apply (rule mult_nonneg_nonneg)
    3.25 -  apply (erule order_less_imp_le)
    3.26 -  apply simp
    3.27    done
    3.28  
    3.29  lemma bigo_plus_subset2 [intro]: "A \<subseteq> O(f) \<Longrightarrow> B \<subseteq> O(f) \<Longrightarrow> A + B \<subseteq> O(f)"
    3.30 @@ -293,7 +287,6 @@
    3.31    apply (subst abs_mult)
    3.32    apply (rule mult_mono)
    3.33    apply assumption+
    3.34 -  apply (rule mult_nonneg_nonneg)
    3.35    apply auto
    3.36    apply (simp add: mult_ac abs_mult)
    3.37    done
    3.38 @@ -651,7 +644,6 @@
    3.39    apply (rule ext)
    3.40    apply (rule setsum_cong2)
    3.41    apply (subst abs_of_nonneg)
    3.42 -  apply (rule mult_nonneg_nonneg)
    3.43    apply auto
    3.44    done
    3.45  
    3.46 @@ -705,9 +697,6 @@
    3.47    apply auto
    3.48    apply (case_tac "x = 0")
    3.49    apply simp
    3.50 -  apply (rule mult_nonneg_nonneg)
    3.51 -  apply force
    3.52 -  apply force
    3.53    apply (subgoal_tac "x = Suc (x - 1)")
    3.54    apply (erule ssubst) back
    3.55    apply (erule spec)
     4.1 --- a/src/HOL/Library/Convex.thy	Fri Apr 11 12:43:22 2014 +0200
     4.2 +++ b/src/HOL/Library/Convex.thy	Fri Apr 11 13:36:57 2014 +0200
     4.3 @@ -606,7 +606,7 @@
     4.4      have "z3 \<in> C" using z3 asm atMostAtLeast_subset_convex
     4.5        `convex C` `x \<in> C` `z1 \<in> C` `x < z1` by fastforce
     4.6      then have B': "f'' z3 \<ge> 0" using assms by auto
     4.7 -    from A' B' have "(y - z1) * f'' z3 \<ge> 0" using mult_nonneg_nonneg by auto
     4.8 +    from A' B' have "(y - z1) * f'' z3 \<ge> 0" by auto
     4.9      from cool' this have "f' y - (f x - f y) / (x - y) \<ge> 0" by auto
    4.10      from mult_right_mono_neg[OF this le(2)]
    4.11      have "f' y * (x - y) - (f x - f y) / (x - y) * (x - y) \<le> 0 * (x - y)"
    4.12 @@ -621,7 +621,7 @@
    4.13      have "z2 \<in> C" using z2 z1 asm atMostAtLeast_subset_convex
    4.14        `convex C` `z1 \<in> C` `y \<in> C` `z1 < y` by fastforce
    4.15      then have B: "f'' z2 \<ge> 0" using assms by auto
    4.16 -    from A B have "(z1 - x) * f'' z2 \<ge> 0" using mult_nonneg_nonneg by auto
    4.17 +    from A B have "(z1 - x) * f'' z2 \<ge> 0" by auto
    4.18      from cool this have "(f y - f x) / (y - x) - f' x \<ge> 0" by auto
    4.19      from mult_right_mono[OF this ge(2)]
    4.20      have "(f y - f x) / (y - x) * (y - x) - f' x * (y - x) \<ge> 0 * (y - x)"
     5.1 --- a/src/HOL/Library/Extended_Real.thy	Fri Apr 11 12:43:22 2014 +0200
     5.2 +++ b/src/HOL/Library/Extended_Real.thy	Fri Apr 11 13:36:57 2014 +0200
     5.3 @@ -717,7 +717,7 @@
     5.4    by (simp add: one_ereal_def zero_ereal_def)
     5.5  
     5.6  lemma ereal_0_le_mult[simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * (b :: ereal)"
     5.7 -  by (cases rule: ereal2_cases[of a b]) (auto simp: mult_nonneg_nonneg)
     5.8 +  by (cases rule: ereal2_cases[of a b]) auto
     5.9  
    5.10  lemma ereal_right_distrib:
    5.11    fixes r a b :: ereal
     6.1 --- a/src/HOL/Library/Float.thy	Fri Apr 11 12:43:22 2014 +0200
     6.2 +++ b/src/HOL/Library/Float.thy	Fri Apr 11 13:36:57 2014 +0200
     6.3 @@ -618,7 +618,7 @@
     6.4    using round_up_correct[of e f] by simp
     6.5  
     6.6  lemma round_down_nonneg: "0 \<le> s \<Longrightarrow> 0 \<le> round_down p s"
     6.7 -  by (auto simp: round_down_def intro!: mult_nonneg_nonneg)
     6.8 +  by (auto simp: round_down_def)
     6.9  
    6.10  lemma ceil_divide_floor_conv:
    6.11  assumes "b \<noteq> 0"
    6.12 @@ -1418,20 +1418,20 @@
    6.13      by simp
    6.14    moreover
    6.15    have "0 \<le> \<lfloor>x * 2 powr (- real \<lfloor>log 2 x\<rfloor> - 1)\<rfloor>"
    6.16 -    using `x > 0` by (auto intro: mult_nonneg_nonneg)
    6.17 +    using `x > 0` by auto
    6.18    ultimately have "\<lfloor>x * 2 powr (- real \<lfloor>log 2 x\<rfloor> - 1)\<rfloor> \<in> {0 ..< 1}"
    6.19      by simp
    6.20    also have "\<dots> \<subseteq> {0}" by auto
    6.21    finally have "\<lfloor>x * 2 powr (- real \<lfloor>log 2 x\<rfloor> - 1)\<rfloor> = 0" by simp
    6.22    with assms show ?thesis
    6.23 -    by (auto simp: truncate_down_def round_down_def intro!: mult_nonneg_nonneg)
    6.24 +    by (auto simp: truncate_down_def round_down_def)
    6.25  qed
    6.26  
    6.27  lemma truncate_down_nonneg: "0 \<le> y \<Longrightarrow> 0 \<le> truncate_down prec y"
    6.28 -  by (auto simp: truncate_down_def round_down_def intro!: mult_nonneg_nonneg)
    6.29 +  by (auto simp: truncate_down_def round_down_def)
    6.30  
    6.31  lemma truncate_down_zero: "truncate_down prec 0 = 0"
    6.32 -  by (auto simp: truncate_down_def round_down_def intro!: mult_nonneg_nonneg)
    6.33 +  by (auto simp: truncate_down_def round_down_def)
    6.34  
    6.35  lemma truncate_down_switch_sign_mono:
    6.36    assumes "x \<le> 0" "0 \<le> y"
    6.37 @@ -1485,7 +1485,7 @@
    6.38        by simp
    6.39      also have "\<dots> \<le> y * 2 powr real prec / (2 powr (real \<lfloor>log 2 y\<rfloor> + 1))"
    6.40        using `0 \<le> y` `0 \<le> x` assms(2)
    6.41 -      by (auto intro!: powr_mono mult_nonneg_nonneg mult_pos_pos divide_left_mono
    6.42 +      by (auto intro!: powr_mono mult_pos_pos divide_left_mono
    6.43          simp: real_of_nat_diff powr_add
    6.44          powr_divide2[symmetric])
    6.45      also have "\<dots> = y * 2 powr real prec / (2 powr real \<lfloor>log 2 y\<rfloor> * 2)"
     7.1 --- a/src/HOL/Library/Product_Vector.thy	Fri Apr 11 12:43:22 2014 +0200
     7.2 +++ b/src/HOL/Library/Product_Vector.thy	Fri Apr 11 13:36:57 2014 +0200
     7.3 @@ -446,7 +446,6 @@
     7.4    shows "sqrt (x + y) \<le> sqrt x + sqrt y"
     7.5  apply (rule power2_le_imp_le)
     7.6  apply (simp add: power2_sum x y)
     7.7 -apply (simp add: mult_nonneg_nonneg x y)
     7.8  apply (simp add: x y)
     7.9  done
    7.10  
     8.1 --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Fri Apr 11 12:43:22 2014 +0200
     8.2 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Fri Apr 11 13:36:57 2014 +0200
     8.3 @@ -1047,8 +1047,11 @@
     8.4  fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i);
     8.5  
     8.6  fun sos_tac print_cert prover ctxt =
     8.7 -  Object_Logic.full_atomize_tac ctxt THEN'
     8.8 -  elim_denom_tac ctxt THEN'
     8.9 -  core_sos_tac print_cert prover ctxt;
    8.10 +  (* The SOS prover breaks if mult_nonneg_nonneg is in the simpset *)
    8.11 +  let val ctxt' = ctxt delsimps [@{thm mult_nonneg_nonneg}]
    8.12 +  in Object_Logic.full_atomize_tac ctxt' THEN'
    8.13 +     elim_denom_tac ctxt' THEN'
    8.14 +     core_sos_tac print_cert prover ctxt'
    8.15 +  end;
    8.16  
    8.17  end;
     9.1 --- a/src/HOL/Limits.thy	Fri Apr 11 12:43:22 2014 +0200
     9.2 +++ b/src/HOL/Limits.thy	Fri Apr 11 13:36:57 2014 +0200
     9.3 @@ -1239,7 +1239,7 @@
     9.4  proof (induct n)
     9.5    case (Suc n)
     9.6    have "real (Suc n) * x + 1 \<le> (x + 1) * (real n * x + 1)"
     9.7 -    by (simp add: field_simps real_of_nat_Suc mult_nonneg_nonneg x)
     9.8 +    by (simp add: field_simps real_of_nat_Suc x)
     9.9    also have "\<dots> \<le> (x + 1)^Suc n"
    9.10      using Suc x by (simp add: mult_left_mono)
    9.11    finally show ?case .
    10.1 --- a/src/HOL/MacLaurin.thy	Fri Apr 11 12:43:22 2014 +0200
    10.2 +++ b/src/HOL/MacLaurin.thy	Fri Apr 11 13:36:57 2014 +0200
    10.3 @@ -575,8 +575,7 @@
    10.4      apply (rule setsum_cong[OF refl])
    10.5      apply (subst diff_m_0, simp)
    10.6      apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono
    10.7 -                simp add: est mult_nonneg_nonneg mult_ac divide_inverse
    10.8 -                          power_abs [symmetric] abs_mult)
    10.9 +                simp add: est mult_ac divide_inverse power_abs [symmetric] abs_mult)
   10.10      done
   10.11  qed
   10.12  
    11.1 --- a/src/HOL/Metis_Examples/Big_O.thy	Fri Apr 11 12:43:22 2014 +0200
    11.2 +++ b/src/HOL/Metis_Examples/Big_O.thy	Fri Apr 11 13:36:57 2014 +0200
    11.3 @@ -164,28 +164,24 @@
    11.4  apply (rule conjI)
    11.5   apply (rule_tac x = "c + c" in exI)
    11.6   apply clarsimp
    11.7 - apply auto
    11.8 -  apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (f xa)")
    11.9 -   apply (metis mult_2 order_trans)
   11.10 -  apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
   11.11 -   apply (erule order_trans)
   11.12 -   apply (simp add: ring_distribs)
   11.13 -  apply (rule mult_left_mono)
   11.14 -   apply (simp add: abs_triangle_ineq)
   11.15 -  apply (simp add: order_less_le)
   11.16 - apply (rule mult_nonneg_nonneg)
   11.17 -  apply auto
   11.18 + apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (f xa)")
   11.19 +  apply (metis mult_2 order_trans)
   11.20 + apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
   11.21 +  apply (erule order_trans)
   11.22 +  apply (simp add: ring_distribs)
   11.23 + apply (rule mult_left_mono)
   11.24 +  apply (simp add: abs_triangle_ineq)
   11.25 + apply (simp add: order_less_le)
   11.26  apply (rule_tac x = "\<lambda>n. if (abs (f n)) < abs (g n) then x n else 0" in exI)
   11.27  apply (rule conjI)
   11.28   apply (rule_tac x = "c + c" in exI)
   11.29   apply auto
   11.30 - apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (g xa)")
   11.31 -  apply (metis order_trans mult_2)
   11.32 - apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
   11.33 -  apply (erule order_trans)
   11.34 -  apply (simp add: ring_distribs)
   11.35 - apply (metis abs_triangle_ineq mult_le_cancel_left_pos)
   11.36 -by (metis abs_ge_zero abs_of_pos zero_le_mult_iff)
   11.37 +apply (subgoal_tac "c * abs (f xa + g xa) <= (c + c) * abs (g xa)")
   11.38 + apply (metis order_trans mult_2)
   11.39 +apply (subgoal_tac "c * abs (f xa + g xa) <= c * (abs (f xa) + abs (g xa))")
   11.40 + apply (erule order_trans)
   11.41 + apply (simp add: ring_distribs)
   11.42 +by (metis abs_triangle_ineq mult_le_cancel_left_pos)
   11.43  
   11.44  lemma bigo_plus_subset2 [intro]: "A <= O(f) \<Longrightarrow> B <= O(f) \<Longrightarrow> A + B <= O(f)"
   11.45  by (metis bigo_plus_idemp set_plus_mono2)
   11.46 @@ -713,6 +709,6 @@
   11.47  lemma bigo_lesso5: "f <o g =o O(h) \<Longrightarrow> \<exists>C. \<forall>x. f x <= g x + C * abs (h x)"
   11.48  apply (simp only: lesso_def bigo_alt_def)
   11.49  apply clarsimp
   11.50 -by (metis abs_if abs_mult add_commute diff_le_eq less_not_permute)
   11.51 +by (metis add_commute diff_le_eq)
   11.52  
   11.53  end
    12.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Apr 11 12:43:22 2014 +0200
    12.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Apr 11 13:36:57 2014 +0200
    12.3 @@ -1173,8 +1173,7 @@
    12.4      then have "c *\<^sub>R x = (c * cx) *\<^sub>R xx"
    12.5        using x by (simp add: algebra_simps)
    12.6      moreover
    12.7 -    have "c * cx \<ge> 0"
    12.8 -      using c x using mult_nonneg_nonneg by auto
    12.9 +    have "c * cx \<ge> 0" using c x by auto
   12.10      ultimately
   12.11      have "c *\<^sub>R x \<in> ?rhs" using x by auto
   12.12    }
   12.13 @@ -1603,13 +1602,7 @@
   12.14          by simp
   12.15        finally have **:"1 - (u * u1 + v * u2) = u * v1 + v * v2" by auto
   12.16        have "0 \<le> u * v1 + v * v2" "0 \<le> u * v1" "0 \<le> u * v1 + v * v2" "0 \<le> v * v2"
   12.17 -        apply (rule add_nonneg_nonneg)
   12.18 -        prefer 4
   12.19 -        apply (rule add_nonneg_nonneg)
   12.20 -        apply (rule_tac [!] mult_nonneg_nonneg)
   12.21 -        using as(1,2) obt1(1,2) obt2(1,2)
   12.22 -        apply auto
   12.23 -        done
   12.24 +        using as(1,2) obt1(1,2) obt2(1,2) by auto
   12.25        then show ?thesis
   12.26          unfolding obt1(5) obt2(5)
   12.27          unfolding * and **
   12.28 @@ -1643,7 +1636,7 @@
   12.29        apply (rule_tac x="1 - u * u1 - v * u2" in exI)
   12.30        unfolding Bex_def
   12.31        using as(1,2) obt1(1,2) obt2(1,2) **
   12.32 -      apply (auto intro!: mult_nonneg_nonneg add_nonneg_nonneg simp add: algebra_simps)
   12.33 +      apply (auto simp add: algebra_simps)
   12.34        done
   12.35    qed
   12.36  qed
   12.37 @@ -1728,19 +1721,15 @@
   12.38      proof (cases "i\<in>{1..k1}")
   12.39        case True
   12.40        then show ?thesis
   12.41 -        using mult_nonneg_nonneg[of u "u1 i"] and uv(1) x(1)[THEN bspec[where x=i]]
   12.42 -        by auto
   12.43 +        using uv(1) x(1)[THEN bspec[where x=i]] by auto
   12.44      next
   12.45        case False
   12.46        def j \<equiv> "i - k1"
   12.47        from i False have "j \<in> {1..k2}"
   12.48          unfolding j_def by auto
   12.49        then show ?thesis
   12.50 -        unfolding j_def[symmetric]
   12.51 -        using False
   12.52 -        using mult_nonneg_nonneg[of v "u2 j"] and uv(2) y(1)[THEN bspec[where x=j]]
   12.53 -        apply auto
   12.54 -        done
   12.55 +        using False uv(2) y(1)[THEN bspec[where x=j]]
   12.56 +        by (auto simp: j_def[symmetric])
   12.57      qed
   12.58    qed (auto simp add: not_le x(2,3) y(2,3) uv(3))
   12.59  qed
   12.60 @@ -1770,9 +1759,7 @@
   12.61      assume "x\<in>s"
   12.62      then have "0 \<le> u * ux x + v * uy x"
   12.63        using ux(1)[THEN bspec[where x=x]] uy(1)[THEN bspec[where x=x]] and uv(1,2)
   12.64 -      apply auto
   12.65 -      apply (metis add_nonneg_nonneg mult_nonneg_nonneg uv(1) uv(2))
   12.66 -      done
   12.67 +      by auto
   12.68    }
   12.69    moreover
   12.70    have "(\<Sum>x\<in>s. u * ux x + v * uy x) = 1"
   12.71 @@ -2290,14 +2277,7 @@
   12.72        show "0 \<le> u v + t * w v"
   12.73        proof (cases "w v < 0")
   12.74          case False
   12.75 -        then show ?thesis
   12.76 -          apply (rule_tac add_nonneg_nonneg)
   12.77 -          using v
   12.78 -          apply simp
   12.79 -          apply (rule mult_nonneg_nonneg)
   12.80 -          using `t\<ge>0`
   12.81 -          apply auto
   12.82 -          done
   12.83 +        thus ?thesis using v `t\<ge>0` by auto
   12.84        next
   12.85          case True
   12.86          then have "t \<le> u v / (- w v)"
   12.87 @@ -4585,13 +4565,7 @@
   12.88        apply (rule_tac x = "inverse(norm a) *\<^sub>R a" in exI)
   12.89        using hull_subset[of c convex]
   12.90        unfolding subset_eq and inner_scaleR
   12.91 -      apply -
   12.92 -      apply rule
   12.93 -      defer
   12.94 -      apply rule
   12.95 -      apply (rule mult_nonneg_nonneg)
   12.96 -      apply (auto simp add: inner_commute del: ballE elim!: ballE)
   12.97 -      done
   12.98 +      by (auto simp add: inner_commute del: ballE elim!: ballE)
   12.99      then show "frontier (cball 0 1) \<inter> \<Inter>f \<noteq> {}"
  12.100        unfolding c(1) frontier_cball dist_norm by auto
  12.101    qed (insert closed_halfspace_ge, auto)
  12.102 @@ -5981,8 +5955,7 @@
  12.103        using assms as(1)[unfolded mem_box]
  12.104        apply (erule_tac x=i in ballE)
  12.105        apply rule
  12.106 -      apply (rule mult_nonneg_nonneg)
  12.107 -      prefer 3
  12.108 +      prefer 2
  12.109        apply (rule mult_right_le_one_le)
  12.110        using assms
  12.111        apply auto
  12.112 @@ -8481,7 +8454,7 @@
  12.113        by auto
  12.114      def e \<equiv> "\<lambda>i. u * c i + v * d i"
  12.115      have ge0: "\<forall>i\<in>I. e i \<ge> 0"
  12.116 -      using e_def xc yc uv by (simp add: mult_nonneg_nonneg)
  12.117 +      using e_def xc yc uv by simp
  12.118      have "setsum (\<lambda>i. u * c i) I = u * setsum c I"
  12.119        by (simp add: setsum_right_distrib)
  12.120      moreover have "setsum (\<lambda>i. v * d i) I = v * setsum d I"
  12.121 @@ -8502,7 +8475,7 @@
  12.122            using mem_convex_alt[of "S i" "s i" "t i" "u * (c i)" "v * (d i)"]
  12.123              mult_nonneg_nonneg[of u "c i"] mult_nonneg_nonneg[of v "d i"]
  12.124              assms q_def e_def i False xc yc uv
  12.125 -          by auto
  12.126 +          by (auto simp del: mult_nonneg_nonneg)
  12.127        qed
  12.128      }
  12.129      then have qs: "\<forall>i\<in>I. q i \<in> S i" by auto
  12.130 @@ -8513,7 +8486,7 @@
  12.131        proof (cases "e i = 0")
  12.132          case True
  12.133          have ge: "u * (c i) \<ge> 0 \<and> v * d i \<ge> 0"
  12.134 -          using xc yc uv i by (simp add: mult_nonneg_nonneg)
  12.135 +          using xc yc uv i by simp
  12.136          moreover from ge have "u * c i \<le> 0 \<and> v * d i \<le> 0"
  12.137            using True e_def i by simp
  12.138          ultimately have "u * c i = 0 \<and> v * d i = 0" by auto
    13.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Apr 11 12:43:22 2014 +0200
    13.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri Apr 11 13:36:57 2014 +0200
    13.3 @@ -5986,9 +5986,8 @@
    13.4          apply (rule setsum_nonneg)
    13.5          apply safe
    13.6          unfolding real_scaleR_def
    13.7 -        apply (rule mult_nonneg_nonneg)
    13.8          apply (drule tagged_division_ofD(4)[OF q(1)])
    13.9 -        apply auto
   13.10 +        apply (auto intro: mult_nonneg_nonneg)
   13.11          done
   13.12        have **: "\<And>f g s t. finite s \<Longrightarrow> finite t \<Longrightarrow> (\<forall>(x,y) \<in> t. (0::real) \<le> g(x,y)) \<Longrightarrow>
   13.13          (\<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"
   13.14 @@ -6022,12 +6021,8 @@
   13.15          assume as'': "(a, b) \<in> q i"
   13.16          show "0 \<le> (real i + 1) * (content b *\<^sub>R indicator s a)"
   13.17            unfolding real_scaleR_def
   13.18 -          apply (rule mult_nonneg_nonneg)
   13.19 -          defer
   13.20 -          apply (rule mult_nonneg_nonneg)
   13.21            using tagged_division_ofD(4)[OF q(1) as'']
   13.22 -          apply auto
   13.23 -          done
   13.24 +          by (auto intro!: mult_nonneg_nonneg)
   13.25        next
   13.26          fix i :: nat
   13.27          show "finite (q i)"
   13.28 @@ -7818,11 +7813,7 @@
   13.29      have "\<exists>l. 0 < l \<and> norm(l *\<^sub>R f' a) \<le> (e * (b - a)) / 8"
   13.30      proof (cases "f' a = 0")
   13.31        case True
   13.32 -      then show ?thesis
   13.33 -        apply (rule_tac x=1 in exI)
   13.34 -        using ab e
   13.35 -        apply (auto intro!:mult_nonneg_nonneg)
   13.36 -        done
   13.37 +      thus ?thesis using ab e by auto
   13.38      next
   13.39        case False
   13.40        then show ?thesis
   13.41 @@ -7885,11 +7876,7 @@
   13.42      have "\<exists>l. 0 < l \<and> norm (l *\<^sub>R f' b) \<le> (e * (b - a)) / 8"
   13.43      proof (cases "f' b = 0")
   13.44        case True
   13.45 -      then show ?thesis
   13.46 -        apply (rule_tac x=1 in exI)
   13.47 -        using ab e
   13.48 -        apply (auto intro!: mult_nonneg_nonneg)
   13.49 -        done
   13.50 +      thus ?thesis using ab e by auto
   13.51      next
   13.52        case False
   13.53        then show ?thesis
    14.1 --- a/src/HOL/Multivariate_Analysis/L2_Norm.thy	Fri Apr 11 12:43:22 2014 +0200
    14.2 +++ b/src/HOL/Multivariate_Analysis/L2_Norm.thy	Fri Apr 11 13:36:57 2014 +0200
    14.3 @@ -109,7 +109,7 @@
    14.4  lemma sqrt_sum_squares_le_sum:
    14.5    "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) \<le> x + y"
    14.6    apply (rule power2_le_imp_le)
    14.7 -  apply (simp add: power2_sum mult_nonneg_nonneg)
    14.8 +  apply (simp add: power2_sum)
    14.9    apply simp
   14.10    done
   14.11  
   14.12 @@ -127,7 +127,7 @@
   14.13  
   14.14  lemma sqrt_sum_squares_le_sum_abs: "sqrt (x\<^sup>2 + y\<^sup>2) \<le> \<bar>x\<bar> + \<bar>y\<bar>"
   14.15    apply (rule power2_le_imp_le)
   14.16 -  apply (simp add: power2_sum mult_nonneg_nonneg)
   14.17 +  apply (simp add: power2_sum)
   14.18    apply simp
   14.19    done
   14.20  
   14.21 @@ -162,15 +162,13 @@
   14.22    apply (rule order_trans)
   14.23    apply (rule power_mono)
   14.24    apply (erule add_left_mono)
   14.25 -  apply (simp add: mult_nonneg_nonneg setsum_nonneg)
   14.26 +  apply (simp add: setsum_nonneg)
   14.27    apply (simp add: power2_sum)
   14.28    apply (simp add: power_mult_distrib)
   14.29    apply (simp add: distrib_left distrib_right)
   14.30    apply (rule ord_le_eq_trans)
   14.31    apply (rule setL2_mult_ineq_lemma)
   14.32 -  apply simp
   14.33 -  apply (intro mult_nonneg_nonneg setL2_nonneg)
   14.34 -  apply simp
   14.35 +  apply simp_all
   14.36    done
   14.37  
   14.38  lemma member_le_setL2: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> setL2 f A"
    15.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Apr 11 12:43:22 2014 +0200
    15.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Apr 11 13:36:57 2014 +0200
    15.3 @@ -487,7 +487,7 @@
    15.4    shows "x \<le> y + z"
    15.5  proof -
    15.6    have "y\<^sup>2 + z\<^sup>2 \<le> y\<^sup>2 + 2 * y * z + z\<^sup>2"
    15.7 -    using z y by (simp add: mult_nonneg_nonneg)
    15.8 +    using z y by simp
    15.9    with xy have th: "x\<^sup>2 \<le> (y + z)\<^sup>2"
   15.10      by (simp add: power2_eq_square field_simps)
   15.11    from y z have yz: "y + z \<ge> 0"
    16.1 --- a/src/HOL/NthRoot.thy	Fri Apr 11 12:43:22 2014 +0200
    16.2 +++ b/src/HOL/NthRoot.thy	Fri Apr 11 13:36:57 2014 +0200
    16.3 @@ -602,7 +602,7 @@
    16.4  apply (rule_tac b="(a * d - b * c)\<^sup>2" in ord_le_eq_trans)
    16.5  apply (rule zero_le_power2)
    16.6  apply (simp add: power2_diff power_mult_distrib)
    16.7 -apply (simp add: mult_nonneg_nonneg)
    16.8 +apply (simp)
    16.9  apply simp
   16.10  apply (simp add: add_increasing)
   16.11  done
    17.1 --- a/src/HOL/Power.thy	Fri Apr 11 12:43:22 2014 +0200
    17.2 +++ b/src/HOL/Power.thy	Fri Apr 11 13:36:57 2014 +0200
    17.3 @@ -301,7 +301,7 @@
    17.4  
    17.5  lemma zero_le_power [simp]:
    17.6    "0 \<le> a \<Longrightarrow> 0 \<le> a ^ n"
    17.7 -  by (induct n) (simp_all add: mult_nonneg_nonneg)
    17.8 +  by (induct n) simp_all
    17.9  
   17.10  lemma power_mono:
   17.11    "a \<le> b \<Longrightarrow> 0 \<le> a \<Longrightarrow> a ^ n \<le> b ^ n"
    18.1 --- a/src/HOL/Probability/Distributions.thy	Fri Apr 11 12:43:22 2014 +0200
    18.2 +++ b/src/HOL/Probability/Distributions.thy	Fri Apr 11 13:36:57 2014 +0200
    18.3 @@ -148,7 +148,7 @@
    18.4    show "emeasure M {x\<in>space M. X x \<le> a} = ereal (if 0 \<le> a then 1 - exp (- a * l) else 0)"
    18.5      using X_distr[of a] eq_0 by (auto simp: one_ereal_def)
    18.6    show "AE x in lborel. 0 \<le> exponential_density l x "
    18.7 -    by (auto simp: exponential_density_def intro!: AE_I2 mult_nonneg_nonneg)
    18.8 +    by (auto simp: exponential_density_def)
    18.9  qed simp_all
   18.10  
   18.11  lemma (in prob_space) exponential_distributed_iff:
    19.1 --- a/src/HOL/Probability/Information.thy	Fri Apr 11 12:43:22 2014 +0200
    19.2 +++ b/src/HOL/Probability/Information.thy	Fri Apr 11 13:36:57 2014 +0200
    19.3 @@ -622,7 +622,7 @@
    19.4        subdensity_real[OF measurable_snd Pxy Py Y]
    19.5        distributed_real_AE[OF Pxy]
    19.6      by eventually_elim
    19.7 -       (auto simp: f_def log_divide_eq log_mult_eq field_simps zero_less_mult_iff mult_nonneg_nonneg)
    19.8 +       (auto simp: f_def log_divide_eq log_mult_eq field_simps zero_less_mult_iff)
    19.9  
   19.10    show "0 \<le> ?M" unfolding M
   19.11    proof (rule ST.KL_density_density_nonneg
   19.12 @@ -1102,7 +1102,7 @@
   19.13      apply (rule positive_integral_mono_AE)
   19.14      using ae5 ae6 ae7 ae8
   19.15      apply eventually_elim
   19.16 -    apply (auto intro!: divide_nonneg_nonneg mult_nonneg_nonneg)
   19.17 +    apply (auto intro!: divide_nonneg_nonneg)
   19.18      done
   19.19    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)"
   19.20      by (subst STP.positive_integral_snd_measurable[symmetric]) (auto simp add: split_beta')
   19.21 @@ -1151,7 +1151,7 @@
   19.22      apply simp
   19.23      using ae5 ae6 ae7 ae8
   19.24      apply eventually_elim
   19.25 -    apply (auto intro!: mult_nonneg_nonneg divide_nonneg_nonneg)
   19.26 +    apply (auto intro!: divide_nonneg_nonneg)
   19.27      done
   19.28  
   19.29    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))))"
   19.30 @@ -1296,7 +1296,7 @@
   19.31      apply (rule integrable_cong_AE_imp)
   19.32      using ae1 ae4 ae5 ae6 ae9
   19.33      by eventually_elim
   19.34 -       (auto simp: log_divide_eq log_mult_eq mult_nonneg_nonneg field_simps zero_less_mult_iff)
   19.35 +       (auto simp: log_divide_eq log_mult_eq field_simps zero_less_mult_iff)
   19.36  
   19.37    have "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P)
   19.38      (\<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))))"
   19.39 @@ -1311,7 +1311,7 @@
   19.40      apply (rule integrable_cong_AE_imp)
   19.41      using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 ae9
   19.42      by eventually_elim
   19.43 -       (auto simp: log_divide_eq log_mult_eq mult_nonneg_nonneg field_simps zero_less_mult_iff)
   19.44 +       (auto simp: log_divide_eq log_mult_eq field_simps zero_less_mult_iff)
   19.45  
   19.46    from ae I1 I2 show ?eq
   19.47      unfolding conditional_mutual_information_def
   19.48 @@ -1347,7 +1347,7 @@
   19.49      apply (rule positive_integral_mono_AE)
   19.50      using ae5 ae6 ae7 ae8
   19.51      apply eventually_elim
   19.52 -    apply (auto intro!: divide_nonneg_nonneg mult_nonneg_nonneg)
   19.53 +    apply (auto intro!: divide_nonneg_nonneg)
   19.54      done
   19.55    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)"
   19.56      by (subst STP.positive_integral_snd_measurable[symmetric])
   19.57 @@ -1396,7 +1396,7 @@
   19.58      apply (auto simp: split_beta') []
   19.59      using ae5 ae6 ae7 ae8
   19.60      apply eventually_elim
   19.61 -    apply (auto intro!: mult_nonneg_nonneg divide_nonneg_nonneg)
   19.62 +    apply (auto intro!: divide_nonneg_nonneg)
   19.63      done
   19.64  
   19.65    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))))"
    20.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Fri Apr 11 12:43:22 2014 +0200
    20.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Fri Apr 11 13:36:57 2014 +0200
    20.3 @@ -236,9 +236,9 @@
    20.4      proof (split split_if, intro conjI impI)
    20.5        assume "\<not> real j \<le> u x"
    20.6        then have "natfloor (real (u x) * 2 ^ j) \<le> natfloor (j * 2 ^ j)"
    20.7 -         by (cases "u x") (auto intro!: natfloor_mono simp: mult_nonneg_nonneg)
    20.8 +         by (cases "u x") (auto intro!: natfloor_mono)
    20.9        moreover have "real (natfloor (j * 2 ^ j)) \<le> j * 2^j"
   20.10 -        by (intro real_natfloor_le) (auto simp: mult_nonneg_nonneg)
   20.11 +        by (intro real_natfloor_le) auto
   20.12        ultimately show "natfloor (real (u x) * 2 ^ j) \<le> j * 2 ^ j"
   20.13          unfolding real_of_nat_le_iff by auto
   20.14      qed auto }
   20.15 @@ -300,7 +300,7 @@
   20.16      proof (rule SUP_eqI)
   20.17        fix i show "?g i x \<le> max 0 (u x)" unfolding max_def f_def
   20.18          by (cases "u x") (auto simp: field_simps real_natfloor_le natfloor_neg
   20.19 -                                     mult_nonpos_nonneg mult_nonneg_nonneg)
   20.20 +                                     mult_nonpos_nonneg)
   20.21      next
   20.22        fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> ?g i x \<le> y"
   20.23        have "\<And>i. 0 \<le> ?g i x" by (auto simp: divide_nonneg_pos)
   20.24 @@ -317,12 +317,12 @@
   20.25          proof (rule ccontr)
   20.26            assume "\<not> p \<le> r"
   20.27            with LIMSEQ_inverse_realpow_zero[unfolded LIMSEQ_iff, rule_format, of 2 "p - r"]
   20.28 -          obtain N where "\<forall>n\<ge>N. r * 2^n < p * 2^n - 1" by (auto simp: inverse_eq_divide field_simps)
   20.29 +          obtain N where "\<forall>n\<ge>N. r * 2^n < p * 2^n - 1" by (auto simp: field_simps)
   20.30            then have "r * 2^max N m < p * 2^max N m - 1" by simp
   20.31            moreover
   20.32            have "real (natfloor (p * 2 ^ max N m)) \<le> r * 2 ^ max N m"
   20.33              using *[of "max N m"] m unfolding real_f using ux
   20.34 -            by (cases "0 \<le> u x") (simp_all add: max_def mult_nonneg_nonneg split: split_if_asm)
   20.35 +            by (cases "0 \<le> u x") (simp_all add: max_def split: split_if_asm)
   20.36            then have "p * 2 ^ max N m - 1 < r * 2 ^ max N m"
   20.37              by (metis real_natfloor_gt_diff_one less_le_trans)
   20.38            ultimately show False by auto
    21.1 --- a/src/HOL/Real.thy	Fri Apr 11 12:43:22 2014 +0200
    21.2 +++ b/src/HOL/Real.thy	Fri Apr 11 13:36:57 2014 +0200
    21.3 @@ -333,7 +333,7 @@
    21.4        by (simp add: inverse_diff_inverse abs_mult)
    21.5      also have "\<dots> < inverse a * s * inverse b"
    21.6        apply (intro mult_strict_mono' less_imp_inverse_less)
    21.7 -      apply (simp_all add: a b i j k n mult_nonneg_nonneg)
    21.8 +      apply (simp_all add: a b i j k n)
    21.9        done
   21.10      also note `inverse a * s * inverse b = r`
   21.11      finally show "\<bar>inverse (X n) - inverse (Y n)\<bar> < r" .
   21.12 @@ -1927,7 +1927,7 @@
   21.13  lemma le_mult_natfloor:
   21.14    shows "natfloor a * natfloor b \<le> natfloor (a * b)"
   21.15    by (cases "0 <= a & 0 <= b")
   21.16 -    (auto simp add: le_natfloor_eq mult_nonneg_nonneg mult_mono' real_natfloor_le natfloor_neg)
   21.17 +    (auto simp add: le_natfloor_eq mult_mono' real_natfloor_le natfloor_neg)
   21.18  
   21.19  lemma natceiling_zero [simp]: "natceiling 0 = 0"
   21.20    by (unfold natceiling_def, simp)
    22.1 --- a/src/HOL/Rings.thy	Fri Apr 11 12:43:22 2014 +0200
    22.2 +++ b/src/HOL/Rings.thy	Fri Apr 11 13:36:57 2014 +0200
    22.3 @@ -492,7 +492,7 @@
    22.4  
    22.5  subclass semiring_0_cancel ..
    22.6  
    22.7 -lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
    22.8 +lemma mult_nonneg_nonneg[simp]: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
    22.9  using mult_left_mono [of 0 b a] by simp
   22.10  
   22.11  lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"
   22.12 @@ -759,7 +759,7 @@
   22.13  
   22.14  lemma split_mult_pos_le:
   22.15    "(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b"
   22.16 -by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
   22.17 +by (auto simp add: mult_nonpos_nonpos)
   22.18  
   22.19  end
   22.20  
   22.21 @@ -777,7 +777,7 @@
   22.22  
   22.23  lemma zero_le_square [simp]: "0 \<le> a * a"
   22.24    using linear [of 0 a]
   22.25 -  by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
   22.26 +  by (auto simp add: mult_nonpos_nonpos)
   22.27  
   22.28  lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
   22.29    by (simp add: not_less)
    23.1 --- a/src/HOL/Series.thy	Fri Apr 11 12:43:22 2014 +0200
    23.2 +++ b/src/HOL/Series.thy	Fri Apr 11 13:36:57 2014 +0200
    23.3 @@ -575,8 +575,7 @@
    23.4  
    23.5    let ?g = "\<lambda>(i,j). a i * b j"
    23.6    let ?f = "\<lambda>(i,j). norm (a i) * norm (b j)"
    23.7 -  have f_nonneg: "\<And>x. 0 \<le> ?f x"
    23.8 -    by (auto simp add: mult_nonneg_nonneg)
    23.9 +  have f_nonneg: "\<And>x. 0 \<le> ?f x" by (auto)
   23.10    hence norm_setsum_f: "\<And>A. norm (setsum ?f A) = setsum ?f A"
   23.11      unfolding real_norm_def
   23.12      by (simp only: abs_of_nonneg setsum_nonneg [rule_format])
    24.1 --- a/src/HOL/Transcendental.thy	Fri Apr 11 12:43:22 2014 +0200
    24.2 +++ b/src/HOL/Transcendental.thy	Fri Apr 11 13:36:57 2014 +0200
    24.3 @@ -1395,7 +1395,7 @@
    24.4        by (simp add: power_inverse)
    24.5      hence "inverse (fact (n + 2)) * (x^n * x\<^sup>2) \<le> 1/2 * (1/2)^n * (1 * x\<^sup>2)"
    24.6        by (rule mult_mono)
    24.7 -        (rule mult_mono, simp_all add: power_le_one a b mult_nonneg_nonneg)
    24.8 +        (rule mult_mono, simp_all add: power_le_one a b)
    24.9      hence "inverse (fact (n + 2)) * x ^ (n + 2) \<le> (x\<^sup>2/2) * ((1/2)^n)"
   24.10        unfolding power_add by (simp add: mult_ac del: fact_Suc) }
   24.11    note aux1 = this