--- a/src/HOL/Decision_Procs/Approximation.thy Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Mon Apr 14 13:08:17 2014 +0200
@@ -778,7 +778,7 @@
also have "\<dots> \<le> cos x"
proof -
from even[OF `even n`] `0 < ?fact` `0 < ?pow`
- have "0 \<le> (?rest / ?fact) * ?pow" by (simp add: divide_nonneg_pos)
+ have "0 \<le> (?rest / ?fact) * ?pow" by simp
thus ?thesis unfolding cos_eq by auto
qed
finally have "(lb_sin_cos_aux prec n 1 1 (x * x)) \<le> cos x" .
@@ -891,7 +891,7 @@
also have "\<dots> \<le> sin x"
proof -
from even[OF `even n`] `0 < ?fact` `0 < ?pow`
- have "0 \<le> (?rest / ?fact) * ?pow" by (simp add: divide_nonneg_pos less_imp_le)
+ have "0 \<le> (?rest / ?fact) * ?pow" by simp
thus ?thesis unfolding sin_eq by auto
qed
finally have "(x * lb_sin_cos_aux prec n 2 1 (x * x)) \<le> sin x" .
@@ -1344,7 +1344,7 @@
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 simp: divide_nonneg_pos zero_le_even_power)
+ by (auto simp: 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" .
--- a/src/HOL/Fields.thy Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Fields.thy Mon Apr 14 13:08:17 2014 +0200
@@ -1083,6 +1083,21 @@
"(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
by (auto simp add: divide_less_eq)
+lemma divide_nonneg_nonneg [simp]:
+ "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x / y"
+ by (auto simp add: divide_simps)
+
+lemma divide_nonpos_nonpos:
+ "x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> 0 \<le> x / y"
+ by (auto simp add: divide_simps)
+
+lemma divide_nonneg_nonpos:
+ "0 \<le> x \<Longrightarrow> y \<le> 0 \<Longrightarrow> x / y \<le> 0"
+ by (auto simp add: divide_simps)
+
+lemma divide_nonpos_nonneg:
+ "x \<le> 0 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x / y \<le> 0"
+ by (auto simp add: divide_simps)
text {*Conditional Simplification Rules: No Case Splits*}
--- a/src/HOL/Library/Convex.thy Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Library/Convex.thy Mon Apr 14 13:08:17 2014 +0200
@@ -138,7 +138,7 @@
with `0 \<le> setsum a s` have "0 < setsum a s" by simp
then have "(\<Sum>j\<in>s. (a j / setsum a s) *\<^sub>R y j) \<in> C"
using `\<forall>j\<in>s. 0 \<le> a j` and `\<forall>j\<in>s. y j \<in> C`
- by (simp add: IH divide_nonneg_pos setsum_divide_distrib [symmetric])
+ by (simp add: IH setsum_divide_distrib [symmetric])
from `convex C` and `y i \<in> C` and this and `0 \<le> a i`
and `0 \<le> setsum a s` and `a i + setsum a s = 1`
have "a i *\<^sub>R y i + setsum a s *\<^sub>R (\<Sum>j\<in>s. (a j / setsum a s) *\<^sub>R y j) \<in> C"
@@ -432,9 +432,7 @@
then have "a i < 1" using asm by auto
then have i0: "1 - a i > 0" by auto
let ?a = "\<lambda>j. a j / (1 - a i)"
- { fix j assume "j \<in> s"
- then have "?a j \<ge> 0"
- using i0 asms divide_nonneg_pos
+ { fix j assume "j \<in> s" with i0 asms have "?a j \<ge> 0"
by fastforce }
note a_nonneg = this
have "(\<Sum> j \<in> insert i s. a j) = 1" using asms by auto
--- a/src/HOL/Library/Float.thy Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Library/Float.thy Mon Apr 14 13:08:17 2014 +0200
@@ -1108,7 +1108,7 @@
shows "0 \<le> real (lapprox_rat n x y)"
using assms unfolding lapprox_rat_def p_def[symmetric] round_down_def real_of_int_minus[symmetric]
powr_int[of 2, simplified]
- by (auto simp add: inverse_eq_divide intro!: mult_nonneg_nonneg divide_nonneg_pos)
+ by auto
lemma rapprox_rat: "real x / real y \<le> real (rapprox_rat prec x y)"
using round_up by (simp add: rapprox_rat_def)
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Mon Apr 14 13:08:17 2014 +0200
@@ -64,11 +64,6 @@
apply auto
done
-lemma divide_nonneg_nonneg:
- fixes a b :: "'a :: {linordered_field, field_inverse_zero}"
- shows "a \<ge> 0 \<Longrightarrow> b \<ge> 0 \<Longrightarrow> 0 \<le> a / b"
- by (cases "b = 0") (auto intro!: divide_nonneg_pos)
-
lemma setsum_Un_disjoint':
assumes "finite A"
and "finite B"
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Apr 14 13:08:17 2014 +0200
@@ -2262,10 +2262,7 @@
using Min_ge_iff[of i 0 ] and obt(1)
unfolding t_def i_def
using obt(4)[unfolded le_less]
- apply auto
- unfolding divide_le_0_iff
- apply auto
- done
+ by (auto simp: divide_le_0_iff)
have t: "\<forall>v\<in>s. u v + t * w v \<ge> 0"
proof
fix v
@@ -5056,7 +5053,7 @@
apply(rule *[OF _ assms(2)])
unfolding mem_Collect_eq
using `b > 0` assms(3)
- apply (auto intro!: divide_nonneg_pos)
+ apply auto
done
ultimately obtain u y where obt: "u\<ge>0" "u \<le> b / norm x" "y = u *\<^sub>R x"
"y \<in> ?A" "y \<in> s" "\<forall>z\<in>?A \<inter> s. dist 0 z \<le> dist 0 y"
@@ -5218,8 +5215,6 @@
from nor have y: "y = norm y *\<^sub>R ((inverse (norm x)) *\<^sub>R x)"
unfolding as(3)[unfolded pi_def] by auto
have "0 \<le> norm y * inverse (norm x)" and "0 \<le> norm x * inverse (norm y)"
- unfolding divide_inverse[symmetric]
- apply (rule_tac[!] divide_nonneg_pos)
using nor
apply auto
done
@@ -5230,7 +5225,7 @@
using x y and front_smul[THEN bspec, OF as(1), THEN spec[where x="norm y * (inverse (norm x))"]]
using front_smul[THEN bspec, OF as(2), THEN spec[where x="norm x * (inverse (norm y))"]]
using xys nor
- apply (auto simp add:field_simps divide_le_eq_1 divide_inverse[symmetric])
+ apply (auto simp add: field_simps)
done
then show "x = y"
apply (subst injpi[symmetric])
@@ -6412,9 +6407,7 @@
next
assume as: "dist a b = dist a x + dist x b"
have "norm (a - x) / norm (a - b) \<le> 1"
- unfolding divide_le_eq_1_pos[OF Fal2]
- unfolding as[unfolded dist_norm] norm_ge_zero
- by auto
+ using Fal2 unfolding as[unfolded dist_norm] norm_ge_zero by auto
then show "\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1"
apply (rule_tac x="dist a x / dist a b" in exI)
unfolding dist_norm
@@ -6422,8 +6415,7 @@
apply rule
defer
apply rule
- apply (rule divide_nonneg_pos)
- prefer 4
+ prefer 3
apply rule
proof -
fix i :: 'a
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy Mon Apr 14 13:08:17 2014 +0200
@@ -16,11 +16,6 @@
lemma axis_in_Basis: "a \<in> Basis \<Longrightarrow> axis i a \<in> Basis"
by (auto simp add: Basis_vec_def axis_eq_axis)
-lemma divide_nonneg_nonneg:
- fixes a b :: "'a :: {linordered_field, field_inverse_zero}"
- shows "a \<ge> 0 \<Longrightarrow> b \<ge> 0 \<Longrightarrow> 0 \<le> a / b"
- by (cases "b = 0") (auto intro!: divide_nonneg_pos)
-
subsection {*Bijections between intervals. *}
definition interval_bij :: "'a \<times> 'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<Rightarrow> 'a::euclidean_space"
@@ -60,7 +55,7 @@
have x: "a\<bullet>i\<le>x\<bullet>i" "x\<bullet>i\<le>b\<bullet>i"
using assms(1)[unfolded mem_box] using i by auto
have "0 \<le> (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
- using * x by (auto intro!: mult_nonneg_nonneg divide_nonneg_nonneg)
+ using * x by auto
then show "u \<bullet> i \<le> u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
using * by auto
have "((x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (v \<bullet> i - u \<bullet> i) \<le> 1 * (v \<bullet> i - u \<bullet> i)"
--- a/src/HOL/Probability/Distributions.thy Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Probability/Distributions.thy Mon Apr 14 13:08:17 2014 +0200
@@ -277,7 +277,7 @@
unfolding emeasure_eq_ereal_measure[OF fin] using A by (simp add: measure_def)
finally show "(\<integral>\<^sup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \<partial>lborel) =
ereal (measure lborel (A \<inter> {..a}) / r)" .
-qed (auto intro!: divide_nonneg_nonneg measure_nonneg)
+qed (auto simp: measure_nonneg)
lemma (in prob_space) uniform_distrI_borel_atLeastAtMost:
fixes a b :: real
--- a/src/HOL/Probability/Information.thy Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Probability/Information.thy Mon Apr 14 13:08:17 2014 +0200
@@ -130,7 +130,7 @@
KL_divergence b (density M f) (density (density M f) (\<lambda>x. g x / f x))"
using f g ac by (subst density_density_divide) simp_all
also have "\<dots> = (\<integral>x. (g x / f x) * log b (g x / f x) \<partial>density M f)"
- using f g `1 < b` by (intro Mf.KL_density) (auto simp: AE_density divide_nonneg_nonneg)
+ using f g `1 < b` by (intro Mf.KL_density) (auto simp: AE_density)
also have "\<dots> = (\<integral>x. g x * log b (g x / f x) \<partial>M)"
using ac f g `1 < b` by (subst integral_density) (auto intro!: integral_cong_AE)
finally show ?thesis .
@@ -332,7 +332,7 @@
from f g show "(\<lambda>x. g x / f x) \<in> borel_measurable (density M f)"
by auto
show "AE x in density M f. 0 \<le> g x / f x"
- using f g by (auto simp: AE_density divide_nonneg_nonneg)
+ using f g by (auto simp: AE_density)
show "integrable (density M f) (\<lambda>x. g x / f x * log b (g x / f x))"
using `1 < b` f g ac
by (subst integral_density)
@@ -804,8 +804,7 @@
using D
apply (subst eq_commute)
apply (intro RN_deriv_unique_sigma_finite)
- apply (auto intro: divide_nonneg_nonneg measure_nonneg
- simp: distributed_distr_eq_density[symmetric, OF X] sf)
+ apply (auto simp: distributed_distr_eq_density[symmetric, OF X] sf measure_nonneg)
done
qed
@@ -1102,7 +1101,7 @@
apply (rule positive_integral_mono_AE)
using ae5 ae6 ae7 ae8
apply eventually_elim
- apply (auto intro!: divide_nonneg_nonneg)
+ apply auto
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')
@@ -1115,7 +1114,7 @@
"(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) \<partial>S) = ereal (Pz b)" "0 \<le> Pyz (a, b)"
then show "(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) * ereal (Pyz (a, b) / Pz b) \<partial>S) = ereal (Pyz (a, b))"
by (subst positive_integral_multc)
- (auto intro!: divide_nonneg_nonneg split: prod.split)
+ (auto split: prod.split)
qed
also have "\<dots> = 1"
using Q.emeasure_space_1 distributed_AE[OF Pyz] distributed_distr_eq_density[OF Pyz]
@@ -1151,7 +1150,7 @@
apply simp
using ae5 ae6 ae7 ae8
apply eventually_elim
- apply (auto intro!: divide_nonneg_nonneg)
+ apply auto
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))))"
@@ -1347,7 +1346,7 @@
apply (rule positive_integral_mono_AE)
using ae5 ae6 ae7 ae8
apply eventually_elim
- apply (auto intro!: divide_nonneg_nonneg)
+ apply auto
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])
@@ -1360,7 +1359,7 @@
fix a b assume "Pz b = 0 \<longrightarrow> Pyz (a, b) = 0" "0 \<le> Pz b" "a \<in> space T \<and> b \<in> space P"
"(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) \<partial>S) = ereal (Pz b)" "0 \<le> Pyz (a, b)"
then show "(\<integral>\<^sup>+ x. ereal (Pxz (x, b)) * ereal (Pyz (a, b) / Pz b) \<partial>S) = ereal (Pyz (a, b))"
- by (subst positive_integral_multc) (auto intro!: divide_nonneg_nonneg)
+ by (subst positive_integral_multc) auto
qed
also have "\<dots> = 1"
using Q.emeasure_space_1 distributed_AE[OF Pyz] distributed_distr_eq_density[OF Pyz]
@@ -1396,7 +1395,7 @@
apply (auto simp: split_beta') []
using ae5 ae6 ae7 ae8
apply eventually_elim
- apply (auto intro!: divide_nonneg_nonneg)
+ apply auto
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 Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Mon Apr 14 13:08:17 2014 +0200
@@ -303,7 +303,7 @@
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)
+ have "\<And>i. 0 \<le> ?g i x" by auto
from order_trans[OF this *] have "0 \<le> y" by simp
show "max 0 (u x) \<le> y"
proof (cases y)
@@ -330,7 +330,7 @@
then show "max 0 (u x) \<le> y" using real ux by simp
qed (insert `0 \<le> y`, auto)
qed
- qed (auto simp: divide_nonneg_pos)
+ qed auto
qed
lemma borel_measurable_implies_simple_function_sequence':
--- a/src/HOL/Rat.thy Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Rat.thy Mon Apr 14 13:08:17 2014 +0200
@@ -578,7 +578,7 @@
by (cases "b = 0", simp, simp add: of_int_rat)
moreover have "0 \<le> Fract (a mod b) b \<and> Fract (a mod b) b < 1"
unfolding Fract_of_int_quotient
- by (rule linorder_cases [of b 0]) (simp add: divide_nonpos_neg, simp, simp add: divide_nonneg_pos)
+ by (rule linorder_cases [of b 0]) (simp_all add: divide_nonpos_neg)
ultimately show ?thesis by simp
qed
--- a/src/HOL/Real.thy Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Real.thy Mon Apr 14 13:08:17 2014 +0200
@@ -1136,8 +1136,6 @@
apply (simp add: algebra_simps)
apply (subst real_of_int_div_aux)
apply simp
- apply (subst zero_le_divide_iff)
- apply auto
apply (simp add: algebra_simps)
apply (subst real_of_int_div_aux)
apply simp
@@ -1269,8 +1267,6 @@
apply (simp add: algebra_simps)
apply (subst real_of_nat_div_aux)
apply simp
-apply (subst zero_le_divide_iff)
-apply simp
done
lemma real_of_nat_div3:
--- a/src/HOL/Transcendental.thy Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Transcendental.thy Mon Apr 14 13:08:17 2014 +0200
@@ -1494,10 +1494,7 @@
also have "- (x / (1 - x)) <= ..."
proof -
have "ln (1 + x / (1 - x)) <= x / (1 - x)"
- apply (rule ln_add_one_self_le_self)
- apply (rule divide_nonneg_pos)
- using a c apply auto
- done
+ using a c by (intro ln_add_one_self_le_self) auto
thus ?thesis
by auto
qed
@@ -1586,11 +1583,8 @@
also have "... = 1 + (y - x) / x"
using x a by (simp add: field_simps)
also have "x * ln(1 + (y - x) / x) <= x * ((y - x) / x)"
- apply (rule mult_left_mono)
- apply (rule ln_add_one_self_le_self)
- apply (rule divide_nonneg_pos)
- using x a apply simp_all
- done
+ using x a
+ by (intro mult_left_mono ln_add_one_self_le_self) simp_all
also have "... = y - x" using a by simp
also have "... = (y - x) * ln (exp 1)" by simp
also have "... <= (y - x) * ln x"
@@ -3906,9 +3900,6 @@
hence low2: "- (pi / 2) < y / 2" and high2: "y / 2 < pi / 2"
by auto
- have divide_nonzero_divide: "\<And>A B C :: real. C \<noteq> 0 \<Longrightarrow> A / B = (A / C) / (B / C)"
- by auto
-
have "0 < cos y" using cos_gt_zero_pi[OF low high] .
hence "cos y \<noteq> 0" and cos_sqrt: "sqrt ((cos y)\<^sup>2) = cos y"
by auto
@@ -3922,7 +3913,7 @@
finally have "1 + (tan y)\<^sup>2 = 1 / (cos y)\<^sup>2" .
have "sin y / (cos y + 1) = tan y / ((cos y + 1) / cos y)"
- unfolding tan_def divide_nonzero_divide[OF `cos y \<noteq> 0`, symmetric] ..
+ unfolding tan_def using `cos y \<noteq> 0` by (simp add: field_simps)
also have "\<dots> = tan y / (1 + 1 / cos y)"
using `cos y \<noteq> 0` unfolding add_divide_distrib by auto
also have "\<dots> = tan y / (1 + 1 / sqrt ((cos y)\<^sup>2))"