made divide_pos_pos a simp rule
authornipkow
Fri Apr 11 22:53:33 2014 +0200 (2014-04-11)
changeset 565410e3abadbef39
parent 56539 1fd920a86173
child 56542 5dc66c358f7e
made divide_pos_pos a simp rule
src/HOL/Complex.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Deriv.thy
src/HOL/Fields.thy
src/HOL/Library/BigO.thy
src/HOL/Library/Convex.thy
src/HOL/Library/Product_Vector.thy
src/HOL/Limits.thy
src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/NSA/NSA.thy
src/HOL/Probability/Information.thy
src/HOL/Probability/Regularity.thy
src/HOL/Real.thy
src/HOL/Transcendental.thy
src/HOL/ex/Gauge_Integration.thy
     1.1 --- a/src/HOL/Complex.thy	Fri Apr 11 17:53:16 2014 +0200
     1.2 +++ b/src/HOL/Complex.thy	Fri Apr 11 22:53:33 2014 +0200
     1.3 @@ -394,7 +394,7 @@
     1.4    shows "((\<lambda>x. Complex (f x) (g x)) ---> Complex a b) F"
     1.5  proof (rule tendstoI)
     1.6    fix r :: real assume "0 < r"
     1.7 -  hence "0 < r / sqrt 2" by (simp add: divide_pos_pos)
     1.8 +  hence "0 < r / sqrt 2" by simp
     1.9    have "eventually (\<lambda>x. dist (f x) a < r / sqrt 2) F"
    1.10      using `(f ---> a) F` and `0 < r / sqrt 2` by (rule tendstoD)
    1.11    moreover
     2.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Fri Apr 11 17:53:16 2014 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Fri Apr 11 22:53:33 2014 +0200
     2.3 @@ -1635,7 +1635,7 @@
     2.4    have "x \<noteq> 0" using assms by auto
     2.5    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
     2.6    moreover
     2.7 -  have "0 < y / x" using assms divide_pos_pos by auto
     2.8 +  have "0 < y / x" using assms by auto
     2.9    hence "0 < 1 + y / x" by auto
    2.10    ultimately show ?thesis using ln_mult assms by auto
    2.11  qed
     3.1 --- a/src/HOL/Deriv.thy	Fri Apr 11 17:53:16 2014 +0200
     3.2 +++ b/src/HOL/Deriv.thy	Fri Apr 11 22:53:33 2014 +0200
     3.3 @@ -468,10 +468,8 @@
     3.4      fix h show "F h = 0"
     3.5      proof (rule ccontr)
     3.6        assume **: "F h \<noteq> 0"
     3.7 -      then have h: "h \<noteq> 0"
     3.8 -        by (clarsimp simp add: F.zero)
     3.9 -      with ** have "0 < ?r h"
    3.10 -        by (simp add: divide_pos_pos)
    3.11 +      hence h: "h \<noteq> 0" by (clarsimp simp add: F.zero)
    3.12 +      with ** have "0 < ?r h" by simp
    3.13        from LIM_D [OF * this] obtain s where s: "0 < s"
    3.14          and r: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> ?r x < ?r h" by auto
    3.15        from dense [OF s] obtain t where t: "0 < t \<and> t < s" ..
     4.1 --- a/src/HOL/Fields.thy	Fri Apr 11 17:53:16 2014 +0200
     4.2 +++ b/src/HOL/Fields.thy	Fri Apr 11 22:53:33 2014 +0200
     4.3 @@ -801,7 +801,7 @@
     4.4  done
     4.5  *)
     4.6  
     4.7 -lemma divide_pos_pos:
     4.8 +lemma divide_pos_pos[simp]:
     4.9    "0 < x ==> 0 < y ==> 0 < x / y"
    4.10  by(simp add:field_simps)
    4.11  
     5.1 --- a/src/HOL/Library/BigO.thy	Fri Apr 11 17:53:16 2014 +0200
     5.2 +++ b/src/HOL/Library/BigO.thy	Fri Apr 11 22:53:33 2014 +0200
     5.3 @@ -851,8 +851,7 @@
     5.4    apply clarify
     5.5    apply (drule_tac x = "r / c" in spec)
     5.6    apply (drule mp)
     5.7 -  apply (erule divide_pos_pos)
     5.8 -  apply assumption
     5.9 +  apply simp
    5.10    apply clarify
    5.11    apply (rule_tac x = no in exI)
    5.12    apply (rule allI)
     6.1 --- a/src/HOL/Library/Convex.thy	Fri Apr 11 17:53:16 2014 +0200
     6.2 +++ b/src/HOL/Library/Convex.thy	Fri Apr 11 22:53:33 2014 +0200
     6.3 @@ -666,7 +666,7 @@
     6.4    then have f''0: "\<And>z :: real. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)"
     6.5      unfolding inverse_eq_divide by (auto simp add: mult_assoc)
     6.6    have f''_ge0: "\<And>z :: real. z > 0 \<Longrightarrow> 1 / (ln b * z * z) \<ge> 0"
     6.7 -    using `b > 1` by (auto intro!:less_imp_le simp add: divide_pos_pos[of 1] mult_pos_pos)
     6.8 +    using `b > 1` by (auto intro!:less_imp_le simp add: mult_pos_pos)
     6.9    from f''_ge0_imp_convex[OF pos_is_convex,
    6.10      unfolded greaterThan_iff, OF f' f''0 f''_ge0]
    6.11    show ?thesis by auto
     7.1 --- a/src/HOL/Library/Product_Vector.thy	Fri Apr 11 17:53:16 2014 +0200
     7.2 +++ b/src/HOL/Library/Product_Vector.thy	Fri Apr 11 22:53:33 2014 +0200
     7.3 @@ -319,7 +319,7 @@
     7.4          using * by fast
     7.5        def r \<equiv> "e / sqrt 2" and s \<equiv> "e / sqrt 2"
     7.6        from `0 < e` have "0 < r" and "0 < s"
     7.7 -        unfolding r_def s_def by (simp_all add: divide_pos_pos)
     7.8 +        unfolding r_def s_def by simp_all
     7.9        from `0 < e` have "e = sqrt (r\<^sup>2 + s\<^sup>2)"
    7.10          unfolding r_def s_def by (simp add: power_divide)
    7.11        def A \<equiv> "{y. dist (fst x) y < r}" and B \<equiv> "{y. dist (snd x) y < s}"
    7.12 @@ -359,8 +359,7 @@
    7.13    shows "Cauchy (\<lambda>n. (X n, Y n))"
    7.14  proof (rule metric_CauchyI)
    7.15    fix r :: real assume "0 < r"
    7.16 -  then have "0 < r / sqrt 2" (is "0 < ?s")
    7.17 -    by (simp add: divide_pos_pos)
    7.18 +  hence "0 < r / sqrt 2" (is "0 < ?s") by simp
    7.19    obtain M where M: "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < ?s"
    7.20      using metric_CauchyD [OF `Cauchy X` `0 < ?s`] ..
    7.21    obtain N where N: "\<forall>m\<ge>N. \<forall>n\<ge>N. dist (Y m) (Y n) < ?s"
     8.1 --- a/src/HOL/Limits.thy	Fri Apr 11 17:53:16 2014 +0200
     8.2 +++ b/src/HOL/Limits.thy	Fri Apr 11 22:53:33 2014 +0200
     8.3 @@ -283,8 +283,7 @@
     8.4    show ?thesis
     8.5    proof (rule ZfunI)
     8.6      fix r::real assume "0 < r"
     8.7 -    hence "0 < r / K"
     8.8 -      using K by (rule divide_pos_pos)
     8.9 +    hence "0 < r / K" using K by simp
    8.10      then have "eventually (\<lambda>x. norm (f x) < r / K) F"
    8.11        using ZfunD [OF f] by fast
    8.12      with g show "eventually (\<lambda>x. norm (g x) < r) F"
    8.13 @@ -1711,7 +1710,7 @@
    8.14      using pos_bounded by fast
    8.15    show "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
    8.16    proof (rule exI, safe)
    8.17 -    from r K show "0 < r / K" by (rule divide_pos_pos)
    8.18 +    from r K show "0 < r / K" by simp
    8.19    next
    8.20      fix x y :: 'a
    8.21      assume xy: "norm (x - y) < r / K"
     9.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Fri Apr 11 17:53:16 2014 +0200
     9.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Fri Apr 11 22:53:33 2014 +0200
     9.3 @@ -1538,11 +1538,7 @@
     9.4        abs ((f(z) - z)\<bullet>i) < d / (real n)"
     9.5    proof -
     9.6      have d': "d / real n / 8 > 0"
     9.7 -      apply (rule divide_pos_pos)+
     9.8 -      using d(1)
     9.9 -      unfolding n_def
    9.10 -      apply (auto simp:  DIM_positive)
    9.11 -      done
    9.12 +      using d(1) by (simp add: n_def DIM_positive)
    9.13      have *: "uniformly_continuous_on unit_cube f"
    9.14        by (rule compact_uniformly_continuous[OF assms(1) compact_unit_cube])
    9.15      obtain e where e:
    9.16 @@ -1627,12 +1623,7 @@
    9.17    obtain p :: nat where p: "1 + real n / e \<le> real p"
    9.18      using real_arch_simple ..
    9.19    have "1 + real n / e > 0"
    9.20 -    apply (rule add_pos_pos)
    9.21 -    defer
    9.22 -    apply (rule divide_pos_pos)
    9.23 -    using e(1) n
    9.24 -    apply auto
    9.25 -    done
    9.26 +    using e(1) n by (simp add: add_pos_pos)
    9.27    then have "p > 0"
    9.28      using p by auto
    9.29  
    10.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Apr 11 17:53:16 2014 +0200
    10.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Apr 11 22:53:33 2014 +0200
    10.3 @@ -1359,9 +1359,7 @@
    10.4      by (auto simp add: dist_nz[symmetric])
    10.5  
    10.6    then obtain u where "0 < u" "u \<le> 1" and u: "u < e / dist x y"
    10.7 -    using real_lbound_gt_zero[of 1 "e / dist x y"]
    10.8 -    using xy `e>0` and divide_pos_pos[of e "dist x y"]
    10.9 -    by auto
   10.10 +    using real_lbound_gt_zero[of 1 "e / dist x y"] xy `e>0` by auto
   10.11    then have "f ((1-u) *\<^sub>R x + u *\<^sub>R y) \<le> (1-u) * f x + u * f y"
   10.12      using `x\<in>s` `y\<in>s`
   10.13      using assms(2)[unfolded convex_on_def,
   10.14 @@ -4227,7 +4225,7 @@
   10.15      then show "norm (v *\<^sub>R z - y) < norm y"
   10.16        unfolding norm_lt using z and assms
   10.17        by (simp add: field_simps inner_diff inner_commute mult_strict_left_mono[OF _ `0<v`])
   10.18 -  qed (rule divide_pos_pos, auto)
   10.19 +  qed auto
   10.20  qed
   10.21  
   10.22  lemma closer_point_lemma:
   10.23 @@ -5104,7 +5102,7 @@
   10.24      fix e
   10.25      assume "e > 0" and as: "(u + e / 2 / norm x) *\<^sub>R x \<in> s"
   10.26      then have "u + e / 2 / norm x > u"
   10.27 -      using `norm x > 0` by (auto simp del:zero_less_norm_iff intro!: divide_pos_pos)
   10.28 +      using `norm x > 0` by (auto simp del:zero_less_norm_iff)
   10.29      then show False using u_max[OF _ as] by auto
   10.30    qed (insert `y\<in>s`, auto simp add: dist_norm scaleR_left_distrib obt(3))
   10.31    then show ?thesis by(metis that[of u] u_max obt(1))
   10.32 @@ -6148,10 +6146,7 @@
   10.33      using assms(1) unfolding open_contains_cball by auto
   10.34    def d \<equiv> "e / real DIM('a)"
   10.35    have "0 < d"
   10.36 -    unfolding d_def using `e > 0` dimge1
   10.37 -    apply (rule_tac divide_pos_pos)
   10.38 -    apply auto
   10.39 -    done
   10.40 +    unfolding d_def using `e > 0` dimge1 by auto
   10.41    let ?d = "(\<Sum>i\<in>Basis. d *\<^sub>R i)::'a"
   10.42    obtain c
   10.43      where c: "finite c"
   10.44 @@ -6737,10 +6732,7 @@
   10.45      apply auto
   10.46      done
   10.47    moreover have "?d > 0"
   10.48 -    apply (rule divide_pos_pos)
   10.49 -    using as(2)
   10.50 -    apply (auto simp add: Suc_le_eq DIM_positive)
   10.51 -    done
   10.52 +    using as(2) by (auto simp: Suc_le_eq DIM_positive)
   10.53    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"
   10.54      apply (rule_tac x="min (Min ((op \<bullet> x) ` Basis)) ?D" in exI)
   10.55      apply rule
   10.56 @@ -6915,9 +6907,7 @@
   10.57          by (simp add: card_gt_0_iff)
   10.58        have "Min ((op \<bullet> x) ` d) > 0"
   10.59          using as `d \<noteq> {}` `finite d` by (simp add: Min_grI)
   10.60 -      moreover have "?d > 0"
   10.61 -        apply (rule divide_pos_pos)
   10.62 -        using as using `0 < card d` by auto
   10.63 +      moreover have "?d > 0" using as using `0 < card d` by auto
   10.64        ultimately have h3: "min (Min ((op \<bullet> x) ` d)) ?d > 0"
   10.65          by auto
   10.66  
   10.67 @@ -7185,7 +7175,7 @@
   10.68             assume "e > 0"
   10.69             def e1 \<equiv> "min 1 (e/norm (x - a))"
   10.70             then have e1: "e1 > 0" "e1 \<le> 1" "e1 * norm (x - a) \<le> e"
   10.71 -             using `x \<noteq> a` `e > 0` divide_pos_pos[of e] le_divide_eq[of e1 e "norm (x - a)"]
   10.72 +             using `x \<noteq> a` `e > 0` le_divide_eq[of e1 e "norm (x - a)"]
   10.73               by simp_all
   10.74             then have *: "x - e1 *\<^sub>R (x - a) : rel_interior S"
   10.75               using rel_interior_closure_convex_shrink[of S a x e1] assms x a e1_def
   10.76 @@ -7265,12 +7255,9 @@
   10.77      done
   10.78    finally have "z = y - e *\<^sub>R (y-x)"
   10.79      by auto
   10.80 -  moreover have "e > 0"
   10.81 -    using e_def assms divide_pos_pos[of a "a+b"] by auto
   10.82 -  moreover have "e \<le> 1"
   10.83 -    using e_def assms by auto
   10.84 -  ultimately show ?thesis
   10.85 -    using that[of e] by auto
   10.86 +  moreover have "e > 0" using e_def assms by auto
   10.87 +  moreover have "e \<le> 1" using e_def assms by auto
   10.88 +  ultimately show ?thesis using that[of e] by auto
   10.89  qed
   10.90  
   10.91  lemma convex_rel_interior_closure:
   10.92 @@ -7300,8 +7287,7 @@
   10.93        case False
   10.94        obtain e where e: "e > 0" "cball z e \<inter> affine hull closure S \<le> closure S"
   10.95          using z rel_interior_cball[of "closure S"] by auto
   10.96 -      then have *: "0 < e/norm(z-x)"
   10.97 -        using e False divide_pos_pos[of e "norm(z-x)"] by auto
   10.98 +      hence *: "0 < e/norm(z-x)" using e False by auto
   10.99        def y \<equiv> "z + (e/norm(z-x)) *\<^sub>R (z-x)"
  10.100        have yball: "y \<in> cball z e"
  10.101          using mem_cball y_def dist_norm[of z y] e by auto
  10.102 @@ -7459,8 +7445,7 @@
  10.103      {
  10.104        assume "x \<noteq> z"
  10.105        def m \<equiv> "1 + e1/norm(x-z)"
  10.106 -      then have "m > 1"
  10.107 -        using e1 `x \<noteq> z` divide_pos_pos[of e1 "norm (x - z)"] by auto
  10.108 +      hence "m > 1" using e1 `x \<noteq> z` by auto
  10.109        {
  10.110          fix e
  10.111          assume e: "e > 1 \<and> e \<le> m"
  10.112 @@ -7730,7 +7715,7 @@
  10.113          assume e: "e > 0"
  10.114          def e1 \<equiv> "min 1 (e/norm (y - x))"
  10.115          then have e1: "e1 > 0" "e1 \<le> 1" "e1 * norm (y - x) \<le> e"
  10.116 -          using `y \<noteq> x` `e > 0` divide_pos_pos[of e] le_divide_eq[of e1 e "norm (y - x)"]
  10.117 +          using `y \<noteq> x` `e > 0` le_divide_eq[of e1 e "norm (y - x)"]
  10.118            by simp_all
  10.119          def z \<equiv> "y - e1 *\<^sub>R (y - x)"
  10.120          {
    11.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Fri Apr 11 17:53:16 2014 +0200
    11.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Fri Apr 11 22:53:33 2014 +0200
    11.3 @@ -549,8 +549,7 @@
    11.4        by (rule has_derivative_compose, simp add: deriv)
    11.5      then have "DERIV (\<lambda>r. f (x + r *\<^sub>R h)) 0 :> f' h"
    11.6        unfolding has_field_derivative_def by (simp add: f'.scaleR mult_commute_abs)
    11.7 -    moreover have "0 < d / norm h"
    11.8 -      using d1 and `h \<noteq> 0` by (simp add: divide_pos_pos)
    11.9 +    moreover have "0 < d / norm h" using d1 and `h \<noteq> 0` by simp
   11.10      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)"
   11.11        using `h \<noteq> 0` by (auto simp add: d2 dist_norm pos_less_divide_eq)
   11.12      ultimately show "f' h = 0"
   11.13 @@ -926,11 +925,7 @@
   11.14      norm (z - y) < d \<longrightarrow> norm (g z - g y - g'(z - y)) \<le> e * norm (g z - g y)"
   11.15    proof (rule, rule)
   11.16      case goal1
   11.17 -    have *: "e / C > 0"
   11.18 -      apply (rule divide_pos_pos)
   11.19 -      using `e > 0` C(1)
   11.20 -      apply auto
   11.21 -      done
   11.22 +    have *: "e / C > 0" using `e > 0` C(1) by auto
   11.23      obtain d0 where d0:
   11.24          "0 < d0"
   11.25          "\<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)"
   11.26 @@ -1022,8 +1017,7 @@
   11.27      apply rule
   11.28    proof -
   11.29      case goal1
   11.30 -    then have *: "e / B >0"
   11.31 -      by (metis `0 < B` divide_pos_pos)
   11.32 +    hence *: "e / B >0" by (metis `0 < B` divide_pos_pos)
   11.33      obtain d' where d':
   11.34          "0 < d'"
   11.35          "\<forall>z. norm (z - y) < d' \<longrightarrow> norm (g z - g y - g' (z - y)) \<le> e / B * norm (g z - g y)"
   11.36 @@ -1180,8 +1174,7 @@
   11.37      by auto
   11.38    obtain B where B: "0 < B" "\<forall>x. norm (g' x) \<le> norm x * B"
   11.39      using bounded_linear.pos_bounded[OF assms(5)] by blast
   11.40 -  then have *: "1 / (2 * B) > 0"
   11.41 -    by (auto intro!: divide_pos_pos)
   11.42 +  hence *: "1 / (2 * B) > 0" by auto
   11.43    obtain e0 where e0:
   11.44        "0 < e0"
   11.45        "\<forall>y. norm (y - x) < e0 \<longrightarrow> norm (f y - f x - f' (y - x)) \<le> 1 / (2 * B) * norm (y - x)"
   11.46 @@ -1192,11 +1185,7 @@
   11.47      using assms(8)
   11.48      unfolding mem_interior_cball
   11.49      by blast
   11.50 -  have *: "0 < e0 / B" "0 < e1 / B"
   11.51 -    apply (rule_tac[!] divide_pos_pos)
   11.52 -    using e0 e1 B
   11.53 -    apply auto
   11.54 -    done
   11.55 +  have *: "0 < e0 / B" "0 < e1 / B" using e0 e1 B by auto
   11.56    obtain e where e: "0 < e" "e < e0 / B" "e < e1 / B"
   11.57      using real_lbound_gt_zero[OF *] by blast
   11.58    have "\<forall>z\<in>cball (f x) (e / 2). \<exists>y\<in>cball (f x) e. f (x + g' (y - f x)) = z"
   11.59 @@ -1668,8 +1657,7 @@
   11.60        proof (rule, rule)
   11.61          fix e :: real
   11.62          assume "e > 0"
   11.63 -        then have *: "e / 2 > 0" "e / 2 / norm (x - x0) > 0"
   11.64 -          using False by (auto intro!: divide_pos_pos)
   11.65 +        hence *: "e / 2 > 0" "e / 2 / norm (x - x0) > 0" using False by auto
   11.66          obtain M where M: "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x0) (f n x0) < e / 2"
   11.67            using LIMSEQ_imp_Cauchy[OF assms(5)]
   11.68            unfolding Cauchy_def
   11.69 @@ -1757,8 +1745,7 @@
   11.70            using `u = 0` and `0 < e` by (auto elim: eventually_elim1)
   11.71        next
   11.72          case False
   11.73 -        with `0 < e` have "0 < e / norm u"
   11.74 -          by (simp add: divide_pos_pos)
   11.75 +        with `0 < e` have "0 < e / norm u" by simp
   11.76          then have "eventually (\<lambda>n. norm (f' n x u - g' x u) \<le> e / norm u * norm u) sequentially"
   11.77            using assms(3)[folded eventually_sequentially] and `x \<in> s`
   11.78            by (fast elim: eventually_elim1)
    12.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Fri Apr 11 17:53:16 2014 +0200
    12.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Fri Apr 11 22:53:33 2014 +0200
    12.3 @@ -310,7 +310,7 @@
    12.4          using * by fast
    12.5        def r \<equiv> "\<lambda>i::'b. e / sqrt (of_nat CARD('b))"
    12.6        from `0 < e` have r: "\<forall>i. 0 < r i"
    12.7 -        unfolding r_def by (simp_all add: divide_pos_pos)
    12.8 +        unfolding r_def by simp_all
    12.9        from `0 < e` have e: "e = setL2 r UNIV"
   12.10          unfolding r_def by (simp add: setL2_constant)
   12.11        def A \<equiv> "\<lambda>i. {y. dist (x $ i) y < r i}"
   12.12 @@ -336,8 +336,7 @@
   12.13    shows "Cauchy (\<lambda>n. X n)"
   12.14  proof (rule metric_CauchyI)
   12.15    fix r :: real assume "0 < r"
   12.16 -  then have "0 < r / of_nat CARD('n)" (is "0 < ?s")
   12.17 -    by (simp add: divide_pos_pos)
   12.18 +  hence "0 < r / of_nat CARD('n)" (is "0 < ?s") by simp
   12.19    def N \<equiv> "\<lambda>i. LEAST N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m $ i) (X n $ i) < ?s"
   12.20    def M \<equiv> "Max (range N)"
   12.21    have "\<And>i. \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m $ i) (X n $ i) < ?s"
    13.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Apr 11 17:53:16 2014 +0200
    13.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri Apr 11 22:53:33 2014 +0200
    13.3 @@ -2631,11 +2631,7 @@
    13.4      from pos_bounded
    13.5      obtain B where B: "0 < B" "\<And>x. norm (h x) \<le> norm x * B"
    13.6        by blast
    13.7 -    have *: "e / B > 0"
    13.8 -      apply (rule divide_pos_pos)
    13.9 -      using goal1(2) B
   13.10 -      apply auto
   13.11 -      done
   13.12 +    have *: "e / B > 0" using goal1(2) B by simp
   13.13      obtain g where g:
   13.14        "gauge g"
   13.15        "\<And>p. p tagged_division_of (cbox a b) \<Longrightarrow> g fine p \<Longrightarrow>
   13.16 @@ -2684,8 +2680,7 @@
   13.17    proof -
   13.18      fix e :: real
   13.19      assume e: "e > 0"
   13.20 -    have *: "0 < e/B"
   13.21 -      by (rule divide_pos_pos,rule e,rule B(1))
   13.22 +    have *: "0 < e/B" using e B(1) by simp
   13.23      obtain M where M:
   13.24        "M > 0"
   13.25        "\<And>a b. ball 0 M \<subseteq> cbox a b \<Longrightarrow>
   13.26 @@ -8354,12 +8349,7 @@
   13.27    have "\<exists>w>0. \<forall>t. c - w < t \<and> t < c \<longrightarrow> norm (f c) * norm(c - t) < e / 3"
   13.28    proof (cases "f c = 0")
   13.29      case False
   13.30 -    then have "0 < e / 3 / norm (f c)"
   13.31 -      apply -
   13.32 -      apply (rule divide_pos_pos)
   13.33 -      using `e>0`
   13.34 -      apply auto
   13.35 -      done
   13.36 +    hence "0 < e / 3 / norm (f c)" using `e>0` by simp
   13.37      then show ?thesis
   13.38        apply -
   13.39        apply rule
   13.40 @@ -10101,11 +10091,7 @@
   13.41      then have i: "i \<in> q"
   13.42        unfolding r_def by auto
   13.43      from q'(4)[OF this] guess u v by (elim exE) note uv=this
   13.44 -    have *: "k / (real (card r) + 1) > 0"
   13.45 -      apply (rule divide_pos_pos)
   13.46 -      apply (rule k)
   13.47 -      apply auto
   13.48 -      done
   13.49 +    have *: "k / (real (card r) + 1) > 0" using k by simp
   13.50      have "f integrable_on cbox u v"
   13.51        apply (rule integrable_subinterval[OF assms(1)])
   13.52        using q'(2)[OF i]
   13.53 @@ -10359,11 +10345,7 @@
   13.54      and "\<forall>p. p tagged_partial_division_of (cbox a b) \<and> d fine p \<longrightarrow>
   13.55        setsum (\<lambda>(x,k). norm(content k *\<^sub>R f x - integral k f)) p < e"
   13.56  proof -
   13.57 -  have *: "e / (2 * (real DIM('n) + 1)) > 0"
   13.58 -    apply (rule divide_pos_pos)
   13.59 -    using assms(2)
   13.60 -    apply auto
   13.61 -    done
   13.62 +  have *: "e / (2 * (real DIM('n) + 1)) > 0" using assms(2) by simp
   13.63    from integrable_integral[OF assms(1),unfolded has_integral[of f],rule_format,OF this]
   13.64    guess d .. note d = conjunctD2[OF this]
   13.65    show thesis
   13.66 @@ -10533,7 +10515,6 @@
   13.67        apply -
   13.68        apply rule
   13.69        apply (rule assms(1)[unfolded has_integral_integral has_integral,rule_format])
   13.70 -      apply (rule divide_pos_pos)
   13.71        apply auto
   13.72        done
   13.73      from choice[OF this] guess c .. note c=conjunctD2[OF this[rule_format],rule_format]
   13.74 @@ -10561,11 +10542,7 @@
   13.75      proof
   13.76        case goal1
   13.77        have "e / (4 * content (cbox a b)) > 0"
   13.78 -        apply (rule divide_pos_pos)
   13.79 -        apply fact
   13.80 -        using False content_pos_le[of a b]
   13.81 -        apply auto
   13.82 -        done
   13.83 +        using `e>0` False content_pos_le[of a b] by auto
   13.84        from assms(3)[rule_format, OF goal1, THEN LIMSEQ_D, OF this]
   13.85        guess n .. note n=this
   13.86        then show ?case
   13.87 @@ -10669,9 +10646,7 @@
   13.88                defer
   13.89                apply (rule henstock_lemma_part1)
   13.90                apply (rule assms(1)[rule_format])
   13.91 -              apply (rule divide_pos_pos)
   13.92 -              apply (rule e)
   13.93 -              defer
   13.94 +              apply (simp add: e)
   13.95                apply safe
   13.96                apply (rule c)+
   13.97                apply rule
    14.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Apr 11 17:53:16 2014 +0200
    14.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Apr 11 22:53:33 2014 +0200
    14.3 @@ -854,7 +854,7 @@
    14.4  proof -
    14.5    def e' \<equiv> "e / (2 * sqrt (real (DIM ('a))))"
    14.6    then have e: "e' > 0"
    14.7 -    using assms by (auto intro!: divide_pos_pos simp: DIM_positive)
    14.8 +    using assms by (auto simp: DIM_positive)
    14.9    have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" (is "\<forall>i. ?th i")
   14.10    proof
   14.11      fix i
   14.12 @@ -2538,7 +2538,7 @@
   14.13      apply (simp only: dist_norm [symmetric])
   14.14      apply (subgoal_tac "\<bar>1 - k\<bar> * dist x y < 1 * dist x y", simp)
   14.15      apply (rule mult_strict_right_mono)
   14.16 -    apply (simp add: k_def divide_pos_pos zero_less_dist_iff `0 < r` `x \<noteq> y`)
   14.17 +    apply (simp add: k_def zero_less_dist_iff `0 < r` `x \<noteq> y`)
   14.18      apply (simp add: zero_less_dist_iff `x \<noteq> y`)
   14.19      done
   14.20    then have "z \<in> ball x (dist x y)"
   14.21 @@ -2620,9 +2620,8 @@
   14.22        then have *: "y + (d / 2 / dist y x) *\<^sub>R (y - x) \<in> cball x e"
   14.23          using d as(1)[unfolded subset_eq] by blast
   14.24        have "y - x \<noteq> 0" using `x \<noteq> y` by auto
   14.25 -      then have **:"d / (2 * norm (y - x)) > 0"
   14.26 -        unfolding zero_less_norm_iff[symmetric]
   14.27 -        using `d>0` divide_pos_pos[of d "2*norm (y - x)"] by auto
   14.28 +      hence **:"d / (2 * norm (y - x)) > 0"
   14.29 +        unfolding zero_less_norm_iff[symmetric] using `d>0` by auto
   14.30        have "dist (y + (d / 2 / dist y x) *\<^sub>R (y - x)) x =
   14.31          norm (y + (d / (2 * norm (y - x))) *\<^sub>R y - (d / (2 * norm (y - x))) *\<^sub>R x - x)"
   14.32          by (auto simp add: dist_norm algebra_simps)
   14.33 @@ -4012,8 +4011,7 @@
   14.34    {
   14.35      fix e::real
   14.36      assume "e > 0"
   14.37 -    then have "e / real_of_nat DIM('a) > 0"
   14.38 -      by (auto intro!: divide_pos_pos DIM_positive)
   14.39 +    hence "e / real_of_nat DIM('a) > 0" by (simp add: DIM_positive)
   14.40      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"
   14.41        by simp
   14.42      moreover
   14.43 @@ -4142,7 +4140,7 @@
   14.44    have " 1 / real (Suc (nat (ceiling (1/e)))) < 1 / (ceiling (1/e))"
   14.45      by (rule divide_strict_left_mono) (auto intro!: mult_pos_pos simp: `0 < e`)
   14.46    also have "1 / (ceiling (1/e)) \<le> 1 / (1/e)"
   14.47 -    by (rule divide_left_mono) (auto intro!: divide_pos_pos simp: `0 < e`)
   14.48 +    by (rule divide_left_mono) (auto simp: `0 < e`)
   14.49    also have "\<dots> = e" by simp
   14.50    finally show  "\<exists>n. 1 / real (Suc n) < e" ..
   14.51  qed
   14.52 @@ -7141,8 +7139,7 @@
   14.53      using `norm b >0`
   14.54      unfolding zero_less_norm_iff
   14.55      by auto
   14.56 -  ultimately have "0 < norm (f b) / norm b"
   14.57 -    by (simp only: divide_pos_pos)
   14.58 +  ultimately have "0 < norm (f b) / norm b" by simp
   14.59    moreover
   14.60    {
   14.61      fix x
   14.62 @@ -7155,8 +7152,7 @@
   14.63        case False
   14.64        then have *: "0 < norm a / norm x"
   14.65          using `a\<noteq>0`
   14.66 -        unfolding zero_less_norm_iff[symmetric]
   14.67 -        by (simp only: divide_pos_pos)
   14.68 +        unfolding zero_less_norm_iff[symmetric] by simp
   14.69        have "\<forall>c. \<forall>x\<in>s. c *\<^sub>R x \<in> s"
   14.70          using s[unfolded subspace_def] by auto
   14.71        then have "(norm a / norm x) *\<^sub>R x \<in> {x \<in> s. norm x = norm a}"
   14.72 @@ -7403,10 +7399,8 @@
   14.73        case False
   14.74        then have "d>0" unfolding d_def using zero_le_dist[of "z 0" "z 1"]
   14.75          by (metis False d_def less_le)
   14.76 -      then have "0 < e * (1 - c) / d"
   14.77 -        using `e>0` and `1-c>0`
   14.78 -        using divide_pos_pos[of "e * (1 - c)" d] and mult_pos_pos[of e "1 - c"]
   14.79 -        by auto
   14.80 +      hence "0 < e * (1 - c) / d"
   14.81 +        using `e>0` and `1-c>0` mult_pos_pos[of e "1 - c"] by auto
   14.82        then obtain N where N:"c ^ N < e * (1 - c) / d"
   14.83          using real_arch_pow_inv[of "e * (1 - c) / d" c] and c by auto
   14.84        {
   14.85 @@ -7416,11 +7410,8 @@
   14.86            using power_decreasing[OF `n\<ge>N`, of c] by auto
   14.87          have "1 - c ^ (m - n) > 0"
   14.88            using c and power_strict_mono[of c 1 "m - n"] using `m>n` by auto
   14.89 -        then have **: "d * (1 - c ^ (m - n)) / (1 - c) > 0"
   14.90 -          using mult_pos_pos[OF `d>0`, of "1 - c ^ (m - n)"]
   14.91 -          using divide_pos_pos[of "d * (1 - c ^ (m - n))" "1 - c"]
   14.92 -          using `0 < 1 - c`
   14.93 -          by auto
   14.94 +        hence **: "d * (1 - c ^ (m - n)) / (1 - c) > 0"
   14.95 +          using mult_pos_pos[OF `d>0`, of "1 - c ^ (m - n)"] `0 < 1 - c` by auto
   14.96  
   14.97          have "dist (z m) (z n) \<le> c ^ n * d * (1 - c ^ (m - n)) / (1 - c)"
   14.98            using cf_z2[of n "m - n"] and `m>n`
    15.1 --- a/src/HOL/NSA/NSA.thy	Fri Apr 11 17:53:16 2014 +0200
    15.2 +++ b/src/HOL/NSA/NSA.thy	Fri Apr 11 22:53:33 2014 +0200
    15.3 @@ -388,9 +388,9 @@
    15.4  apply (subgoal_tac "hnorm (x * y) < (r / t) * t", simp)
    15.5  apply (subgoal_tac "0 < r / t")
    15.6  apply (rule hnorm_mult_less)
    15.7 -apply (simp add: InfinitesimalD Reals_divide)
    15.8 +apply (simp add: InfinitesimalD)
    15.9  apply assumption
   15.10 -apply (simp only: divide_pos_pos)
   15.11 +apply simp
   15.12  apply (erule order_le_less_trans [OF hnorm_ge_zero])
   15.13  done
   15.14  
   15.15 @@ -404,7 +404,6 @@
   15.16  apply (subgoal_tac "\<bar>x\<bar> * hnorm y < (r / t) * t", simp)
   15.17  apply (subgoal_tac "0 < r / t")
   15.18  apply (rule mult_strict_mono', simp_all)
   15.19 -apply (simp only: divide_pos_pos)
   15.20  apply (erule order_le_less_trans [OF hnorm_ge_zero])
   15.21  done
   15.22  
   15.23 @@ -418,8 +417,8 @@
   15.24  apply (subgoal_tac "0 < r / t")
   15.25  apply (rule hnorm_mult_less)
   15.26  apply assumption
   15.27 -apply (simp add: InfinitesimalD Reals_divide)
   15.28 -apply (simp only: divide_pos_pos)
   15.29 +apply (simp add: InfinitesimalD)
   15.30 +apply simp
   15.31  apply (erule order_le_less_trans [OF hnorm_ge_zero])
   15.32  done
   15.33  
   15.34 @@ -430,7 +429,7 @@
   15.35  apply (drule InfinitesimalD)
   15.36  apply (drule_tac x="r / \<bar>star_of a\<bar>" in bspec)
   15.37  apply (simp add: Reals_eq_Standard)
   15.38 -apply (simp add: divide_pos_pos)
   15.39 +apply simp
   15.40  apply (simp add: hnorm_scaleR pos_less_divide_eq mult_commute)
   15.41  done
   15.42  
    16.1 --- a/src/HOL/Probability/Information.thy	Fri Apr 11 17:53:16 2014 +0200
    16.2 +++ b/src/HOL/Probability/Information.thy	Fri Apr 11 22:53:33 2014 +0200
    16.3 @@ -1174,7 +1174,7 @@
    16.4      show "AE x in ?P. ?f x \<in> {0<..}"
    16.5        unfolding AE_density[OF distributed_borel_measurable[OF Pxyz]]
    16.6        using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
    16.7 -      by eventually_elim (auto simp: divide_pos_pos mult_pos_pos)
    16.8 +      by eventually_elim (auto simp: mult_pos_pos)
    16.9      show "integrable ?P ?f"
   16.10        unfolding integrable_def 
   16.11        using fin neg by (auto simp: split_beta')
   16.12 @@ -1419,9 +1419,9 @@
   16.13      show "AE x in ?P. ?f x \<in> {0<..}"
   16.14        unfolding AE_density[OF distributed_borel_measurable[OF Pxyz]]
   16.15        using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
   16.16 -      by eventually_elim (auto simp: divide_pos_pos mult_pos_pos)
   16.17 +      by eventually_elim (auto simp: mult_pos_pos)
   16.18      show "integrable ?P ?f"
   16.19 -      unfolding integrable_def 
   16.20 +      unfolding integrable_def
   16.21        using fin neg by (auto simp: split_beta')
   16.22      show "integrable ?P (\<lambda>x. - log b (?f x))"
   16.23        apply (subst integral_density)
    17.1 --- a/src/HOL/Probability/Regularity.thy	Fri Apr 11 17:53:16 2014 +0200
    17.2 +++ b/src/HOL/Probability/Regularity.thy	Fri Apr 11 22:53:33 2014 +0200
    17.3 @@ -377,7 +377,7 @@
    17.4        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)"
    17.5        proof
    17.6          fix i
    17.7 -        from `0 < e` have "0 < e/(2*Suc n0)" by (auto intro: divide_pos_pos)
    17.8 +        from `0 < e` have "0 < e/(2*Suc n0)" by simp
    17.9          have "emeasure M (D i) = (SUP K:{K. K \<subseteq> (D i) \<and> compact K}. emeasure M K)"
   17.10            using union by blast
   17.11          from SUP_approx_ereal[OF `0 < e/(2*Suc n0)` this]
   17.12 @@ -418,7 +418,7 @@
   17.13        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)"
   17.14        proof
   17.15          fix i::nat
   17.16 -        from `0 < e` have "0 < e/(2 powr Suc i)" by (auto intro: divide_pos_pos)
   17.17 +        from `0 < e` have "0 < e/(2 powr Suc i)" by simp
   17.18          have "emeasure M (D i) = (INF U:{U. (D i) \<subseteq> U \<and> open U}. emeasure M U)"
   17.19            using union by blast
   17.20          from INF_approx_ereal[OF `0 < e/(2 powr Suc i)` this]
    18.1 --- a/src/HOL/Real.thy	Fri Apr 11 17:53:16 2014 +0200
    18.2 +++ b/src/HOL/Real.thy	Fri Apr 11 22:53:33 2014 +0200
    18.3 @@ -110,7 +110,7 @@
    18.4      using X by fast
    18.5    obtain b where b: "0 < b" "r = a * b"
    18.6    proof
    18.7 -    show "0 < r / a" using r a by (simp add: divide_pos_pos)
    18.8 +    show "0 < r / a" using r a by simp
    18.9      show "r = a * (r / a)" using a by simp
   18.10    qed
   18.11    obtain k where k: "\<forall>n\<ge>k. \<bar>Y n\<bar> < b"
   18.12 @@ -215,8 +215,8 @@
   18.13      using cauchy_imp_bounded [OF Y] by fast
   18.14    obtain s t where s: "0 < s" and t: "0 < t" and r: "r = a * t + s * b"
   18.15    proof
   18.16 -    show "0 < v/b" using v b(1) by (rule divide_pos_pos)
   18.17 -    show "0 < u/a" using u a(1) by (rule divide_pos_pos)
   18.18 +    show "0 < v/b" using v b(1) by simp
   18.19 +    show "0 < u/a" using u a(1) by simp
   18.20      show "r = a * (u/a) + (v/b) * b"
   18.21        using a(1) b(1) `r = u + v` by simp
   18.22    qed
    19.1 --- a/src/HOL/Transcendental.thy	Fri Apr 11 17:53:16 2014 +0200
    19.2 +++ b/src/HOL/Transcendental.thy	Fri Apr 11 22:53:33 2014 +0200
    19.3 @@ -687,9 +687,7 @@
    19.4    let ?diff = "\<lambda>i x. (f (x0 + x) i - f x0 i) / x"
    19.5  
    19.6    let ?r = "r / (3 * real ?N)"
    19.7 -  have "0 < 3 * real ?N" by auto
    19.8 -  from divide_pos_pos[OF `0 < r` this]
    19.9 -  have "0 < ?r" .
   19.10 +  from `0 < r` have "0 < ?r" by simp
   19.11  
   19.12    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)"
   19.13    def S' \<equiv> "Min (?s ` {..< ?N })"
    20.1 --- a/src/HOL/ex/Gauge_Integration.thy	Fri Apr 11 17:53:16 2014 +0200
    20.2 +++ b/src/HOL/ex/Gauge_Integration.thy	Fri Apr 11 22:53:33 2014 +0200
    20.3 @@ -352,7 +352,7 @@
    20.4  apply (auto simp add: order_le_less)
    20.5  apply (cases "c = 0", simp add: Integral_zero_fun)
    20.6  apply (rule IntegralI)
    20.7 -apply (erule_tac e="e / \<bar>c\<bar>" in IntegralE, simp add: divide_pos_pos)
    20.8 +apply (erule_tac e="e / \<bar>c\<bar>" in IntegralE, simp)
    20.9  apply (rule_tac x="\<delta>" in exI, clarify)
   20.10  apply (drule_tac x="D" in spec, clarify)
   20.11  apply (simp add: pos_less_divide_eq abs_mult [symmetric]
   20.12 @@ -581,7 +581,7 @@
   20.13    show ?thesis
   20.14    proof (simp add: Integral_def2, clarify)
   20.15      fix e :: real assume "0 < e"
   20.16 -    with `a < b` have "0 < e / (b - a)" by (simp add: divide_pos_pos)
   20.17 +    with `a < b` have "0 < e / (b - a)" by simp
   20.18  
   20.19      from lemma_straddle [OF f' this]
   20.20      obtain \<delta> where "gauge {a..b} \<delta>"