--- 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]
--- 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
--- 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)
--- 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)"
--- 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
--- 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)"
--- 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
--- 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;
--- 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 .
--- 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
--- 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
--- 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
--- 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
--- 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"
--- 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"
--- 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
--- 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"
--- 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:
--- 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))))"
--- 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
--- 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)
--- 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)
--- 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])
--- 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