# HG changeset patch
# User nipkow
# Date 1397249627 -7200
# Node ID 5dc66c358f7e68b9cccbd9455c078d2f9ff88855
# Parent  8267d1ff646fc744556bc5184258064f7796fe53# Parent  0e3abadbef39fed2b505c8ffa0c579f690f08a59
merged

diff -r 8267d1ff646f -r 5dc66c358f7e src/HOL/Complex.thy
--- 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
diff -r 8267d1ff646f -r 5dc66c358f7e src/HOL/Decision_Procs/Approximation.thy
--- 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
diff -r 8267d1ff646f -r 5dc66c358f7e src/HOL/Deriv.thy
--- 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" ..
diff -r 8267d1ff646f -r 5dc66c358f7e src/HOL/Fields.thy
--- 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)
 
diff -r 8267d1ff646f -r 5dc66c358f7e src/HOL/Library/BigO.thy
--- 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)
diff -r 8267d1ff646f -r 5dc66c358f7e src/HOL/Library/Convex.thy
--- 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
diff -r 8267d1ff646f -r 5dc66c358f7e src/HOL/Library/Product_Vector.thy
--- 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"
diff -r 8267d1ff646f -r 5dc66c358f7e src/HOL/Limits.thy
--- 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"
diff -r 8267d1ff646f -r 5dc66c358f7e src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- 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
 
diff -r 8267d1ff646f -r 5dc66c358f7e src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- 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)"
         {
diff -r 8267d1ff646f -r 5dc66c358f7e src/HOL/Multivariate_Analysis/Derivative.thy
--- 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)
diff -r 8267d1ff646f -r 5dc66c358f7e src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- 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"
diff -r 8267d1ff646f -r 5dc66c358f7e src/HOL/Multivariate_Analysis/Integration.thy
--- 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
diff -r 8267d1ff646f -r 5dc66c358f7e src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- 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`
diff -r 8267d1ff646f -r 5dc66c358f7e src/HOL/NSA/NSA.thy
--- 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
 
diff -r 8267d1ff646f -r 5dc66c358f7e src/HOL/Probability/Information.thy
--- 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)
diff -r 8267d1ff646f -r 5dc66c358f7e src/HOL/Probability/Regularity.thy
--- 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]
diff -r 8267d1ff646f -r 5dc66c358f7e src/HOL/Real.thy
--- 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
diff -r 8267d1ff646f -r 5dc66c358f7e src/HOL/Transcendental.thy
--- 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 })"
diff -r 8267d1ff646f -r 5dc66c358f7e src/HOL/ex/Gauge_Integration.thy
--- 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>"