--- a/src/HOL/Complex.thy Fri Apr 11 22:19:37 2014 +0200
+++ b/src/HOL/Complex.thy Fri Apr 11 22:53:47 2014 +0200
@@ -394,7 +394,7 @@
shows "((\<lambda>x. Complex (f x) (g x)) ---> Complex a b) F"
proof (rule tendstoI)
fix r :: real assume "0 < r"
- hence "0 < r / sqrt 2" by (simp add: divide_pos_pos)
+ hence "0 < r / sqrt 2" by simp
have "eventually (\<lambda>x. dist (f x) a < r / sqrt 2) F"
using `(f ---> a) F` and `0 < r / sqrt 2` by (rule tendstoD)
moreover
--- a/src/HOL/Decision_Procs/Approximation.thy Fri Apr 11 22:19:37 2014 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Fri Apr 11 22:53:47 2014 +0200
@@ -1635,7 +1635,7 @@
have "x \<noteq> 0" using assms by auto
have "x + y = x * (1 + y / x)" unfolding distrib_left times_divide_eq_right nonzero_mult_divide_cancel_left[OF `x \<noteq> 0`] by auto
moreover
- have "0 < y / x" using assms divide_pos_pos by auto
+ have "0 < y / x" using assms by auto
hence "0 < 1 + y / x" by auto
ultimately show ?thesis using ln_mult assms by auto
qed
--- a/src/HOL/Deriv.thy Fri Apr 11 22:19:37 2014 +0200
+++ b/src/HOL/Deriv.thy Fri Apr 11 22:53:47 2014 +0200
@@ -468,10 +468,8 @@
fix h show "F h = 0"
proof (rule ccontr)
assume **: "F h \<noteq> 0"
- then have h: "h \<noteq> 0"
- by (clarsimp simp add: F.zero)
- with ** have "0 < ?r h"
- by (simp add: divide_pos_pos)
+ hence h: "h \<noteq> 0" by (clarsimp simp add: F.zero)
+ with ** have "0 < ?r h" by simp
from LIM_D [OF * this] obtain s where s: "0 < s"
and r: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> ?r x < ?r h" by auto
from dense [OF s] obtain t where t: "0 < t \<and> t < s" ..
--- a/src/HOL/Fields.thy Fri Apr 11 22:19:37 2014 +0200
+++ b/src/HOL/Fields.thy Fri Apr 11 22:53:47 2014 +0200
@@ -801,7 +801,7 @@
done
*)
-lemma divide_pos_pos:
+lemma divide_pos_pos[simp]:
"0 < x ==> 0 < y ==> 0 < x / y"
by(simp add:field_simps)
--- a/src/HOL/Library/BigO.thy Fri Apr 11 22:19:37 2014 +0200
+++ b/src/HOL/Library/BigO.thy Fri Apr 11 22:53:47 2014 +0200
@@ -851,8 +851,7 @@
apply clarify
apply (drule_tac x = "r / c" in spec)
apply (drule mp)
- apply (erule divide_pos_pos)
- apply assumption
+ apply simp
apply clarify
apply (rule_tac x = no in exI)
apply (rule allI)
--- a/src/HOL/Library/Convex.thy Fri Apr 11 22:19:37 2014 +0200
+++ b/src/HOL/Library/Convex.thy Fri Apr 11 22:53:47 2014 +0200
@@ -666,7 +666,7 @@
then have f''0: "\<And>z :: real. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)"
unfolding inverse_eq_divide by (auto simp add: mult_assoc)
have f''_ge0: "\<And>z :: real. z > 0 \<Longrightarrow> 1 / (ln b * z * z) \<ge> 0"
- using `b > 1` by (auto intro!:less_imp_le simp add: divide_pos_pos[of 1] mult_pos_pos)
+ using `b > 1` by (auto intro!:less_imp_le simp add: mult_pos_pos)
from f''_ge0_imp_convex[OF pos_is_convex,
unfolded greaterThan_iff, OF f' f''0 f''_ge0]
show ?thesis by auto
--- a/src/HOL/Library/Product_Vector.thy Fri Apr 11 22:19:37 2014 +0200
+++ b/src/HOL/Library/Product_Vector.thy Fri Apr 11 22:53:47 2014 +0200
@@ -319,7 +319,7 @@
using * by fast
def r \<equiv> "e / sqrt 2" and s \<equiv> "e / sqrt 2"
from `0 < e` have "0 < r" and "0 < s"
- unfolding r_def s_def by (simp_all add: divide_pos_pos)
+ unfolding r_def s_def by simp_all
from `0 < e` have "e = sqrt (r\<^sup>2 + s\<^sup>2)"
unfolding r_def s_def by (simp add: power_divide)
def A \<equiv> "{y. dist (fst x) y < r}" and B \<equiv> "{y. dist (snd x) y < s}"
@@ -359,8 +359,7 @@
shows "Cauchy (\<lambda>n. (X n, Y n))"
proof (rule metric_CauchyI)
fix r :: real assume "0 < r"
- then have "0 < r / sqrt 2" (is "0 < ?s")
- by (simp add: divide_pos_pos)
+ hence "0 < r / sqrt 2" (is "0 < ?s") by simp
obtain M where M: "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < ?s"
using metric_CauchyD [OF `Cauchy X` `0 < ?s`] ..
obtain N where N: "\<forall>m\<ge>N. \<forall>n\<ge>N. dist (Y m) (Y n) < ?s"
--- a/src/HOL/Limits.thy Fri Apr 11 22:19:37 2014 +0200
+++ b/src/HOL/Limits.thy Fri Apr 11 22:53:47 2014 +0200
@@ -283,8 +283,7 @@
show ?thesis
proof (rule ZfunI)
fix r::real assume "0 < r"
- hence "0 < r / K"
- using K by (rule divide_pos_pos)
+ hence "0 < r / K" using K by simp
then have "eventually (\<lambda>x. norm (f x) < r / K) F"
using ZfunD [OF f] by fast
with g show "eventually (\<lambda>x. norm (g x) < r) F"
@@ -1711,7 +1710,7 @@
using pos_bounded by fast
show "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
proof (rule exI, safe)
- from r K show "0 < r / K" by (rule divide_pos_pos)
+ from r K show "0 < r / K" by simp
next
fix x y :: 'a
assume xy: "norm (x - y) < r / K"
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Fri Apr 11 22:19:37 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Fri Apr 11 22:53:47 2014 +0200
@@ -1538,11 +1538,7 @@
abs ((f(z) - z)\<bullet>i) < d / (real n)"
proof -
have d': "d / real n / 8 > 0"
- apply (rule divide_pos_pos)+
- using d(1)
- unfolding n_def
- apply (auto simp: DIM_positive)
- done
+ using d(1) by (simp add: n_def DIM_positive)
have *: "uniformly_continuous_on unit_cube f"
by (rule compact_uniformly_continuous[OF assms(1) compact_unit_cube])
obtain e where e:
@@ -1627,12 +1623,7 @@
obtain p :: nat where p: "1 + real n / e \<le> real p"
using real_arch_simple ..
have "1 + real n / e > 0"
- apply (rule add_pos_pos)
- defer
- apply (rule divide_pos_pos)
- using e(1) n
- apply auto
- done
+ using e(1) n by (simp add: add_pos_pos)
then have "p > 0"
using p by auto
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Apr 11 22:19:37 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Apr 11 22:53:47 2014 +0200
@@ -1359,9 +1359,7 @@
by (auto simp add: dist_nz[symmetric])
then obtain u where "0 < u" "u \<le> 1" and u: "u < e / dist x y"
- using real_lbound_gt_zero[of 1 "e / dist x y"]
- using xy `e>0` and divide_pos_pos[of e "dist x y"]
- by auto
+ using real_lbound_gt_zero[of 1 "e / dist x y"] xy `e>0` by auto
then have "f ((1-u) *\<^sub>R x + u *\<^sub>R y) \<le> (1-u) * f x + u * f y"
using `x\<in>s` `y\<in>s`
using assms(2)[unfolded convex_on_def,
@@ -4227,7 +4225,7 @@
then show "norm (v *\<^sub>R z - y) < norm y"
unfolding norm_lt using z and assms
by (simp add: field_simps inner_diff inner_commute mult_strict_left_mono[OF _ `0<v`])
- qed (rule divide_pos_pos, auto)
+ qed auto
qed
lemma closer_point_lemma:
@@ -5104,7 +5102,7 @@
fix e
assume "e > 0" and as: "(u + e / 2 / norm x) *\<^sub>R x \<in> s"
then have "u + e / 2 / norm x > u"
- using `norm x > 0` by (auto simp del:zero_less_norm_iff intro!: divide_pos_pos)
+ using `norm x > 0` by (auto simp del:zero_less_norm_iff)
then show False using u_max[OF _ as] by auto
qed (insert `y\<in>s`, auto simp add: dist_norm scaleR_left_distrib obt(3))
then show ?thesis by(metis that[of u] u_max obt(1))
@@ -6148,10 +6146,7 @@
using assms(1) unfolding open_contains_cball by auto
def d \<equiv> "e / real DIM('a)"
have "0 < d"
- unfolding d_def using `e > 0` dimge1
- apply (rule_tac divide_pos_pos)
- apply auto
- done
+ unfolding d_def using `e > 0` dimge1 by auto
let ?d = "(\<Sum>i\<in>Basis. d *\<^sub>R i)::'a"
obtain c
where c: "finite c"
@@ -6737,10 +6732,7 @@
apply auto
done
moreover have "?d > 0"
- apply (rule divide_pos_pos)
- using as(2)
- apply (auto simp add: Suc_le_eq DIM_positive)
- done
+ using as(2) by (auto simp: Suc_le_eq DIM_positive)
ultimately show "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> (\<forall>i\<in>Basis. 0 \<le> y \<bullet> i) \<and> setsum (op \<bullet> y) Basis \<le> 1"
apply (rule_tac x="min (Min ((op \<bullet> x) ` Basis)) ?D" in exI)
apply rule
@@ -6915,9 +6907,7 @@
by (simp add: card_gt_0_iff)
have "Min ((op \<bullet> x) ` d) > 0"
using as `d \<noteq> {}` `finite d` by (simp add: Min_grI)
- moreover have "?d > 0"
- apply (rule divide_pos_pos)
- using as using `0 < card d` by auto
+ moreover have "?d > 0" using as using `0 < card d` by auto
ultimately have h3: "min (Min ((op \<bullet> x) ` d)) ?d > 0"
by auto
@@ -7185,7 +7175,7 @@
assume "e > 0"
def e1 \<equiv> "min 1 (e/norm (x - a))"
then have e1: "e1 > 0" "e1 \<le> 1" "e1 * norm (x - a) \<le> e"
- using `x \<noteq> a` `e > 0` divide_pos_pos[of e] le_divide_eq[of e1 e "norm (x - a)"]
+ using `x \<noteq> a` `e > 0` le_divide_eq[of e1 e "norm (x - a)"]
by simp_all
then have *: "x - e1 *\<^sub>R (x - a) : rel_interior S"
using rel_interior_closure_convex_shrink[of S a x e1] assms x a e1_def
@@ -7265,12 +7255,9 @@
done
finally have "z = y - e *\<^sub>R (y-x)"
by auto
- moreover have "e > 0"
- using e_def assms divide_pos_pos[of a "a+b"] by auto
- moreover have "e \<le> 1"
- using e_def assms by auto
- ultimately show ?thesis
- using that[of e] by auto
+ moreover have "e > 0" using e_def assms by auto
+ moreover have "e \<le> 1" using e_def assms by auto
+ ultimately show ?thesis using that[of e] by auto
qed
lemma convex_rel_interior_closure:
@@ -7300,8 +7287,7 @@
case False
obtain e where e: "e > 0" "cball z e \<inter> affine hull closure S \<le> closure S"
using z rel_interior_cball[of "closure S"] by auto
- then have *: "0 < e/norm(z-x)"
- using e False divide_pos_pos[of e "norm(z-x)"] by auto
+ hence *: "0 < e/norm(z-x)" using e False by auto
def y \<equiv> "z + (e/norm(z-x)) *\<^sub>R (z-x)"
have yball: "y \<in> cball z e"
using mem_cball y_def dist_norm[of z y] e by auto
@@ -7459,8 +7445,7 @@
{
assume "x \<noteq> z"
def m \<equiv> "1 + e1/norm(x-z)"
- then have "m > 1"
- using e1 `x \<noteq> z` divide_pos_pos[of e1 "norm (x - z)"] by auto
+ hence "m > 1" using e1 `x \<noteq> z` by auto
{
fix e
assume e: "e > 1 \<and> e \<le> m"
@@ -7730,7 +7715,7 @@
assume e: "e > 0"
def e1 \<equiv> "min 1 (e/norm (y - x))"
then have e1: "e1 > 0" "e1 \<le> 1" "e1 * norm (y - x) \<le> e"
- using `y \<noteq> x` `e > 0` divide_pos_pos[of e] le_divide_eq[of e1 e "norm (y - x)"]
+ using `y \<noteq> x` `e > 0` le_divide_eq[of e1 e "norm (y - x)"]
by simp_all
def z \<equiv> "y - e1 *\<^sub>R (y - x)"
{
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Fri Apr 11 22:19:37 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Fri Apr 11 22:53:47 2014 +0200
@@ -549,8 +549,7 @@
by (rule has_derivative_compose, simp add: deriv)
then have "DERIV (\<lambda>r. f (x + r *\<^sub>R h)) 0 :> f' h"
unfolding has_field_derivative_def by (simp add: f'.scaleR mult_commute_abs)
- moreover have "0 < d / norm h"
- using d1 and `h \<noteq> 0` by (simp add: divide_pos_pos)
+ moreover have "0 < d / norm h" using d1 and `h \<noteq> 0` by simp
moreover have "\<forall>y. \<bar>0 - y\<bar> < d / norm h \<longrightarrow> f (x + 0 *\<^sub>R h) \<le> f (x + y *\<^sub>R h)"
using `h \<noteq> 0` by (auto simp add: d2 dist_norm pos_less_divide_eq)
ultimately show "f' h = 0"
@@ -926,11 +925,7 @@
norm (z - y) < d \<longrightarrow> norm (g z - g y - g'(z - y)) \<le> e * norm (g z - g y)"
proof (rule, rule)
case goal1
- have *: "e / C > 0"
- apply (rule divide_pos_pos)
- using `e > 0` C(1)
- apply auto
- done
+ have *: "e / C > 0" using `e > 0` C(1) by auto
obtain d0 where d0:
"0 < d0"
"\<forall>ya. norm (ya - g y) < d0 \<longrightarrow> norm (f ya - f (g y) - f' (ya - g y)) \<le> e / C * norm (ya - g y)"
@@ -1022,8 +1017,7 @@
apply rule
proof -
case goal1
- then have *: "e / B >0"
- by (metis `0 < B` divide_pos_pos)
+ hence *: "e / B >0" by (metis `0 < B` divide_pos_pos)
obtain d' where d':
"0 < d'"
"\<forall>z. norm (z - y) < d' \<longrightarrow> norm (g z - g y - g' (z - y)) \<le> e / B * norm (g z - g y)"
@@ -1180,8 +1174,7 @@
by auto
obtain B where B: "0 < B" "\<forall>x. norm (g' x) \<le> norm x * B"
using bounded_linear.pos_bounded[OF assms(5)] by blast
- then have *: "1 / (2 * B) > 0"
- by (auto intro!: divide_pos_pos)
+ hence *: "1 / (2 * B) > 0" by auto
obtain e0 where e0:
"0 < e0"
"\<forall>y. norm (y - x) < e0 \<longrightarrow> norm (f y - f x - f' (y - x)) \<le> 1 / (2 * B) * norm (y - x)"
@@ -1192,11 +1185,7 @@
using assms(8)
unfolding mem_interior_cball
by blast
- have *: "0 < e0 / B" "0 < e1 / B"
- apply (rule_tac[!] divide_pos_pos)
- using e0 e1 B
- apply auto
- done
+ have *: "0 < e0 / B" "0 < e1 / B" using e0 e1 B by auto
obtain e where e: "0 < e" "e < e0 / B" "e < e1 / B"
using real_lbound_gt_zero[OF *] by blast
have "\<forall>z\<in>cball (f x) (e / 2). \<exists>y\<in>cball (f x) e. f (x + g' (y - f x)) = z"
@@ -1668,8 +1657,7 @@
proof (rule, rule)
fix e :: real
assume "e > 0"
- then have *: "e / 2 > 0" "e / 2 / norm (x - x0) > 0"
- using False by (auto intro!: divide_pos_pos)
+ hence *: "e / 2 > 0" "e / 2 / norm (x - x0) > 0" using False by auto
obtain M where M: "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x0) (f n x0) < e / 2"
using LIMSEQ_imp_Cauchy[OF assms(5)]
unfolding Cauchy_def
@@ -1757,8 +1745,7 @@
using `u = 0` and `0 < e` by (auto elim: eventually_elim1)
next
case False
- with `0 < e` have "0 < e / norm u"
- by (simp add: divide_pos_pos)
+ with `0 < e` have "0 < e / norm u" by simp
then have "eventually (\<lambda>n. norm (f' n x u - g' x u) \<le> e / norm u * norm u) sequentially"
using assms(3)[folded eventually_sequentially] and `x \<in> s`
by (fast elim: eventually_elim1)
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Fri Apr 11 22:19:37 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Fri Apr 11 22:53:47 2014 +0200
@@ -310,7 +310,7 @@
using * by fast
def r \<equiv> "\<lambda>i::'b. e / sqrt (of_nat CARD('b))"
from `0 < e` have r: "\<forall>i. 0 < r i"
- unfolding r_def by (simp_all add: divide_pos_pos)
+ unfolding r_def by simp_all
from `0 < e` have e: "e = setL2 r UNIV"
unfolding r_def by (simp add: setL2_constant)
def A \<equiv> "\<lambda>i. {y. dist (x $ i) y < r i}"
@@ -336,8 +336,7 @@
shows "Cauchy (\<lambda>n. X n)"
proof (rule metric_CauchyI)
fix r :: real assume "0 < r"
- then have "0 < r / of_nat CARD('n)" (is "0 < ?s")
- by (simp add: divide_pos_pos)
+ hence "0 < r / of_nat CARD('n)" (is "0 < ?s") by simp
def N \<equiv> "\<lambda>i. LEAST N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m $ i) (X n $ i) < ?s"
def M \<equiv> "Max (range N)"
have "\<And>i. \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m $ i) (X n $ i) < ?s"
--- a/src/HOL/Multivariate_Analysis/Integration.thy Fri Apr 11 22:19:37 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri Apr 11 22:53:47 2014 +0200
@@ -2631,11 +2631,7 @@
from pos_bounded
obtain B where B: "0 < B" "\<And>x. norm (h x) \<le> norm x * B"
by blast
- have *: "e / B > 0"
- apply (rule divide_pos_pos)
- using goal1(2) B
- apply auto
- done
+ have *: "e / B > 0" using goal1(2) B by simp
obtain g where g:
"gauge g"
"\<And>p. p tagged_division_of (cbox a b) \<Longrightarrow> g fine p \<Longrightarrow>
@@ -2684,8 +2680,7 @@
proof -
fix e :: real
assume e: "e > 0"
- have *: "0 < e/B"
- by (rule divide_pos_pos,rule e,rule B(1))
+ have *: "0 < e/B" using e B(1) by simp
obtain M where M:
"M > 0"
"\<And>a b. ball 0 M \<subseteq> cbox a b \<Longrightarrow>
@@ -8354,12 +8349,7 @@
have "\<exists>w>0. \<forall>t. c - w < t \<and> t < c \<longrightarrow> norm (f c) * norm(c - t) < e / 3"
proof (cases "f c = 0")
case False
- then have "0 < e / 3 / norm (f c)"
- apply -
- apply (rule divide_pos_pos)
- using `e>0`
- apply auto
- done
+ hence "0 < e / 3 / norm (f c)" using `e>0` by simp
then show ?thesis
apply -
apply rule
@@ -10101,11 +10091,7 @@
then have i: "i \<in> q"
unfolding r_def by auto
from q'(4)[OF this] guess u v by (elim exE) note uv=this
- have *: "k / (real (card r) + 1) > 0"
- apply (rule divide_pos_pos)
- apply (rule k)
- apply auto
- done
+ have *: "k / (real (card r) + 1) > 0" using k by simp
have "f integrable_on cbox u v"
apply (rule integrable_subinterval[OF assms(1)])
using q'(2)[OF i]
@@ -10359,11 +10345,7 @@
and "\<forall>p. p tagged_partial_division_of (cbox a b) \<and> d fine p \<longrightarrow>
setsum (\<lambda>(x,k). norm(content k *\<^sub>R f x - integral k f)) p < e"
proof -
- have *: "e / (2 * (real DIM('n) + 1)) > 0"
- apply (rule divide_pos_pos)
- using assms(2)
- apply auto
- done
+ have *: "e / (2 * (real DIM('n) + 1)) > 0" using assms(2) by simp
from integrable_integral[OF assms(1),unfolded has_integral[of f],rule_format,OF this]
guess d .. note d = conjunctD2[OF this]
show thesis
@@ -10533,7 +10515,6 @@
apply -
apply rule
apply (rule assms(1)[unfolded has_integral_integral has_integral,rule_format])
- apply (rule divide_pos_pos)
apply auto
done
from choice[OF this] guess c .. note c=conjunctD2[OF this[rule_format],rule_format]
@@ -10561,11 +10542,7 @@
proof
case goal1
have "e / (4 * content (cbox a b)) > 0"
- apply (rule divide_pos_pos)
- apply fact
- using False content_pos_le[of a b]
- apply auto
- done
+ using `e>0` False content_pos_le[of a b] by auto
from assms(3)[rule_format, OF goal1, THEN LIMSEQ_D, OF this]
guess n .. note n=this
then show ?case
@@ -10669,9 +10646,7 @@
defer
apply (rule henstock_lemma_part1)
apply (rule assms(1)[rule_format])
- apply (rule divide_pos_pos)
- apply (rule e)
- defer
+ apply (simp add: e)
apply safe
apply (rule c)+
apply rule
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Apr 11 22:19:37 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Apr 11 22:53:47 2014 +0200
@@ -854,7 +854,7 @@
proof -
def e' \<equiv> "e / (2 * sqrt (real (DIM ('a))))"
then have e: "e' > 0"
- using assms by (auto intro!: divide_pos_pos simp: DIM_positive)
+ using assms by (auto simp: DIM_positive)
have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" (is "\<forall>i. ?th i")
proof
fix i
@@ -2538,7 +2538,7 @@
apply (simp only: dist_norm [symmetric])
apply (subgoal_tac "\<bar>1 - k\<bar> * dist x y < 1 * dist x y", simp)
apply (rule mult_strict_right_mono)
- apply (simp add: k_def divide_pos_pos zero_less_dist_iff `0 < r` `x \<noteq> y`)
+ apply (simp add: k_def zero_less_dist_iff `0 < r` `x \<noteq> y`)
apply (simp add: zero_less_dist_iff `x \<noteq> y`)
done
then have "z \<in> ball x (dist x y)"
@@ -2620,9 +2620,8 @@
then have *: "y + (d / 2 / dist y x) *\<^sub>R (y - x) \<in> cball x e"
using d as(1)[unfolded subset_eq] by blast
have "y - x \<noteq> 0" using `x \<noteq> y` by auto
- then have **:"d / (2 * norm (y - x)) > 0"
- unfolding zero_less_norm_iff[symmetric]
- using `d>0` divide_pos_pos[of d "2*norm (y - x)"] by auto
+ hence **:"d / (2 * norm (y - x)) > 0"
+ unfolding zero_less_norm_iff[symmetric] using `d>0` by auto
have "dist (y + (d / 2 / dist y x) *\<^sub>R (y - x)) x =
norm (y + (d / (2 * norm (y - x))) *\<^sub>R y - (d / (2 * norm (y - x))) *\<^sub>R x - x)"
by (auto simp add: dist_norm algebra_simps)
@@ -4012,8 +4011,7 @@
{
fix e::real
assume "e > 0"
- then have "e / real_of_nat DIM('a) > 0"
- by (auto intro!: divide_pos_pos DIM_positive)
+ hence "e / real_of_nat DIM('a) > 0" by (simp add: DIM_positive)
with l have "eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))) sequentially"
by simp
moreover
@@ -4142,7 +4140,7 @@
have " 1 / real (Suc (nat (ceiling (1/e)))) < 1 / (ceiling (1/e))"
by (rule divide_strict_left_mono) (auto intro!: mult_pos_pos simp: `0 < e`)
also have "1 / (ceiling (1/e)) \<le> 1 / (1/e)"
- by (rule divide_left_mono) (auto intro!: divide_pos_pos simp: `0 < e`)
+ by (rule divide_left_mono) (auto simp: `0 < e`)
also have "\<dots> = e" by simp
finally show "\<exists>n. 1 / real (Suc n) < e" ..
qed
@@ -7141,8 +7139,7 @@
using `norm b >0`
unfolding zero_less_norm_iff
by auto
- ultimately have "0 < norm (f b) / norm b"
- by (simp only: divide_pos_pos)
+ ultimately have "0 < norm (f b) / norm b" by simp
moreover
{
fix x
@@ -7155,8 +7152,7 @@
case False
then have *: "0 < norm a / norm x"
using `a\<noteq>0`
- unfolding zero_less_norm_iff[symmetric]
- by (simp only: divide_pos_pos)
+ unfolding zero_less_norm_iff[symmetric] by simp
have "\<forall>c. \<forall>x\<in>s. c *\<^sub>R x \<in> s"
using s[unfolded subspace_def] by auto
then have "(norm a / norm x) *\<^sub>R x \<in> {x \<in> s. norm x = norm a}"
@@ -7403,10 +7399,8 @@
case False
then have "d>0" unfolding d_def using zero_le_dist[of "z 0" "z 1"]
by (metis False d_def less_le)
- then have "0 < e * (1 - c) / d"
- using `e>0` and `1-c>0`
- using divide_pos_pos[of "e * (1 - c)" d] and mult_pos_pos[of e "1 - c"]
- by auto
+ hence "0 < e * (1 - c) / d"
+ using `e>0` and `1-c>0` mult_pos_pos[of e "1 - c"] by auto
then obtain N where N:"c ^ N < e * (1 - c) / d"
using real_arch_pow_inv[of "e * (1 - c) / d" c] and c by auto
{
@@ -7416,11 +7410,8 @@
using power_decreasing[OF `n\<ge>N`, of c] by auto
have "1 - c ^ (m - n) > 0"
using c and power_strict_mono[of c 1 "m - n"] using `m>n` by auto
- then have **: "d * (1 - c ^ (m - n)) / (1 - c) > 0"
- using mult_pos_pos[OF `d>0`, of "1 - c ^ (m - n)"]
- using divide_pos_pos[of "d * (1 - c ^ (m - n))" "1 - c"]
- using `0 < 1 - c`
- by auto
+ hence **: "d * (1 - c ^ (m - n)) / (1 - c) > 0"
+ using mult_pos_pos[OF `d>0`, of "1 - c ^ (m - n)"] `0 < 1 - c` by auto
have "dist (z m) (z n) \<le> c ^ n * d * (1 - c ^ (m - n)) / (1 - c)"
using cf_z2[of n "m - n"] and `m>n`
--- a/src/HOL/NSA/NSA.thy Fri Apr 11 22:19:37 2014 +0200
+++ b/src/HOL/NSA/NSA.thy Fri Apr 11 22:53:47 2014 +0200
@@ -388,9 +388,9 @@
apply (subgoal_tac "hnorm (x * y) < (r / t) * t", simp)
apply (subgoal_tac "0 < r / t")
apply (rule hnorm_mult_less)
-apply (simp add: InfinitesimalD Reals_divide)
+apply (simp add: InfinitesimalD)
apply assumption
-apply (simp only: divide_pos_pos)
+apply simp
apply (erule order_le_less_trans [OF hnorm_ge_zero])
done
@@ -404,7 +404,6 @@
apply (subgoal_tac "\<bar>x\<bar> * hnorm y < (r / t) * t", simp)
apply (subgoal_tac "0 < r / t")
apply (rule mult_strict_mono', simp_all)
-apply (simp only: divide_pos_pos)
apply (erule order_le_less_trans [OF hnorm_ge_zero])
done
@@ -418,8 +417,8 @@
apply (subgoal_tac "0 < r / t")
apply (rule hnorm_mult_less)
apply assumption
-apply (simp add: InfinitesimalD Reals_divide)
-apply (simp only: divide_pos_pos)
+apply (simp add: InfinitesimalD)
+apply simp
apply (erule order_le_less_trans [OF hnorm_ge_zero])
done
@@ -430,7 +429,7 @@
apply (drule InfinitesimalD)
apply (drule_tac x="r / \<bar>star_of a\<bar>" in bspec)
apply (simp add: Reals_eq_Standard)
-apply (simp add: divide_pos_pos)
+apply simp
apply (simp add: hnorm_scaleR pos_less_divide_eq mult_commute)
done
--- a/src/HOL/Probability/Information.thy Fri Apr 11 22:19:37 2014 +0200
+++ b/src/HOL/Probability/Information.thy Fri Apr 11 22:53:47 2014 +0200
@@ -1174,7 +1174,7 @@
show "AE x in ?P. ?f x \<in> {0<..}"
unfolding AE_density[OF distributed_borel_measurable[OF Pxyz]]
using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
- by eventually_elim (auto simp: divide_pos_pos mult_pos_pos)
+ by eventually_elim (auto simp: mult_pos_pos)
show "integrable ?P ?f"
unfolding integrable_def
using fin neg by (auto simp: split_beta')
@@ -1419,9 +1419,9 @@
show "AE x in ?P. ?f x \<in> {0<..}"
unfolding AE_density[OF distributed_borel_measurable[OF Pxyz]]
using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
- by eventually_elim (auto simp: divide_pos_pos mult_pos_pos)
+ by eventually_elim (auto simp: mult_pos_pos)
show "integrable ?P ?f"
- unfolding integrable_def
+ unfolding integrable_def
using fin neg by (auto simp: split_beta')
show "integrable ?P (\<lambda>x. - log b (?f x))"
apply (subst integral_density)
--- a/src/HOL/Probability/Regularity.thy Fri Apr 11 22:19:37 2014 +0200
+++ b/src/HOL/Probability/Regularity.thy Fri Apr 11 22:53:47 2014 +0200
@@ -377,7 +377,7 @@
have "\<forall>i. \<exists>K. K \<subseteq> D i \<and> compact K \<and> emeasure M (D i) \<le> emeasure M K + e/(2*Suc n0)"
proof
fix i
- from `0 < e` have "0 < e/(2*Suc n0)" by (auto intro: divide_pos_pos)
+ from `0 < e` have "0 < e/(2*Suc n0)" by simp
have "emeasure M (D i) = (SUP K:{K. K \<subseteq> (D i) \<and> compact K}. emeasure M K)"
using union by blast
from SUP_approx_ereal[OF `0 < e/(2*Suc n0)` this]
@@ -418,7 +418,7 @@
have "\<forall>i::nat. \<exists>U. D i \<subseteq> U \<and> open U \<and> e/(2 powr Suc i) > emeasure M U - emeasure M (D i)"
proof
fix i::nat
- from `0 < e` have "0 < e/(2 powr Suc i)" by (auto intro: divide_pos_pos)
+ from `0 < e` have "0 < e/(2 powr Suc i)" by simp
have "emeasure M (D i) = (INF U:{U. (D i) \<subseteq> U \<and> open U}. emeasure M U)"
using union by blast
from INF_approx_ereal[OF `0 < e/(2 powr Suc i)` this]
--- a/src/HOL/Real.thy Fri Apr 11 22:19:37 2014 +0200
+++ b/src/HOL/Real.thy Fri Apr 11 22:53:47 2014 +0200
@@ -110,7 +110,7 @@
using X by fast
obtain b where b: "0 < b" "r = a * b"
proof
- show "0 < r / a" using r a by (simp add: divide_pos_pos)
+ show "0 < r / a" using r a by simp
show "r = a * (r / a)" using a by simp
qed
obtain k where k: "\<forall>n\<ge>k. \<bar>Y n\<bar> < b"
@@ -215,8 +215,8 @@
using cauchy_imp_bounded [OF Y] by fast
obtain s t where s: "0 < s" and t: "0 < t" and r: "r = a * t + s * b"
proof
- show "0 < v/b" using v b(1) by (rule divide_pos_pos)
- show "0 < u/a" using u a(1) by (rule divide_pos_pos)
+ show "0 < v/b" using v b(1) by simp
+ show "0 < u/a" using u a(1) by simp
show "r = a * (u/a) + (v/b) * b"
using a(1) b(1) `r = u + v` by simp
qed
--- a/src/HOL/Transcendental.thy Fri Apr 11 22:19:37 2014 +0200
+++ b/src/HOL/Transcendental.thy Fri Apr 11 22:53:47 2014 +0200
@@ -687,9 +687,7 @@
let ?diff = "\<lambda>i x. (f (x0 + x) i - f x0 i) / x"
let ?r = "r / (3 * real ?N)"
- have "0 < 3 * real ?N" by auto
- from divide_pos_pos[OF `0 < r` this]
- have "0 < ?r" .
+ from `0 < r` have "0 < ?r" by simp
let ?s = "\<lambda>n. SOME s. 0 < s \<and> (\<forall> x. x \<noteq> 0 \<and> \<bar> x \<bar> < s \<longrightarrow> \<bar> ?diff n x - f' x0 n \<bar> < ?r)"
def S' \<equiv> "Min (?s ` {..< ?N })"
--- a/src/HOL/ex/Gauge_Integration.thy Fri Apr 11 22:19:37 2014 +0200
+++ b/src/HOL/ex/Gauge_Integration.thy Fri Apr 11 22:53:47 2014 +0200
@@ -352,7 +352,7 @@
apply (auto simp add: order_le_less)
apply (cases "c = 0", simp add: Integral_zero_fun)
apply (rule IntegralI)
-apply (erule_tac e="e / \<bar>c\<bar>" in IntegralE, simp add: divide_pos_pos)
+apply (erule_tac e="e / \<bar>c\<bar>" in IntegralE, simp)
apply (rule_tac x="\<delta>" in exI, clarify)
apply (drule_tac x="D" in spec, clarify)
apply (simp add: pos_less_divide_eq abs_mult [symmetric]
@@ -581,7 +581,7 @@
show ?thesis
proof (simp add: Integral_def2, clarify)
fix e :: real assume "0 < e"
- with `a < b` have "0 < e / (b - a)" by (simp add: divide_pos_pos)
+ with `a < b` have "0 < e / (b - a)" by simp
from lemma_straddle [OF f' this]
obtain \<delta> where "gauge {a..b} \<delta>"