# HG changeset patch
# User nipkow
# Date 1397316387 -7200
# Node ID b60d5d11948917a9a85ee35538a8449b2ac7dd43
# Parent  9bd56f2e4c10faa0ccff9d315ff8d6043ad267a1
made mult_pos_pos a simp rule

diff -r 9bd56f2e4c10 -r b60d5d119489 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -734,8 +734,7 @@
 proof (cases "real x = 0")
   case False hence "real x \<noteq> 0" by auto
   hence "0 < x" and "0 < real x" using `0 \<le> real x` by auto
-  have "0 < x * x" using `0 < x`
-    using mult_pos_pos[where a="real x" and b="real x"] by auto
+  have "0 < x * x" using `0 < x` by simp
 
   { fix x n have "(\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i))) * x ^ (2 * i))
     = (\<Sum> i = 0 ..< 2 * n. (if even(i) then (-1 ^ (i div 2))/(real (fact i)) else 0) * x ^ i)" (is "?sum = ?ifsum")
@@ -851,8 +850,7 @@
 proof (cases "real x = 0")
   case False hence "real x \<noteq> 0" by auto
   hence "0 < x" and "0 < real x" using `0 \<le> real x` by auto
-  have "0 < x * x" using `0 < x`
-    using mult_pos_pos[where a="real x" and b="real x"] by auto
+  have "0 < x * x" using `0 < x` by simp
 
   { fix x n have "(\<Sum> j = 0 ..< n. -1 ^ (((2 * j + 1) - Suc 0) div 2) / (real (fact (2 * j + 1))) * x ^(2 * j + 1))
     = (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else (-1 ^ ((i - Suc 0) div 2))/(real (fact i))) * x ^ i)" (is "?SUM = _")
diff -r 9bd56f2e4c10 -r b60d5d119489 src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -1674,8 +1674,7 @@
       with uset_l[OF lp] have tnb: "numbound0 t" and np:"real n > 0" and snb: "numbound0 s" and mp:"real m > 0"
         by auto
       let ?st = "Add (Mul m t) (Mul n s)"
-      from mult_pos_pos[OF np mp] have mnp: "real (2*n*m) > 0" 
-        by (simp add: mult_commute)
+      from np mp have mnp: "real (2*n*m) > 0" by (simp add: mult_commute)
       from tnb snb have st_nb: "numbound0 ?st" by simp
       have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)"
         using mnp mp np by (simp add: algebra_simps add_divide_distrib)
@@ -1691,8 +1690,7 @@
     and px:"?I x (usubst p (Add (Mul l t) (Mul k s), 2*k*l))"
     with uset_l[OF lp] have tnb: "numbound0 t" and np:"real k > 0" and snb: "numbound0 s" and mp:"real l > 0" by auto
     let ?st = "Add (Mul l t) (Mul k s)"
-    from mult_pos_pos[OF np mp] have mnp: "real (2*k*l) > 0" 
-      by (simp add: mult_commute)
+    from np mp have mnp: "real (2*k*l) > 0" by (simp add: mult_commute)
     from tnb snb have st_nb: "numbound0 ?st" by simp
     from usubst_I[OF lp mnp st_nb, where bs="bs"] px have "?E" by auto}
   ultimately show "?E" by blast
@@ -1779,7 +1777,7 @@
   from tnU smU U have tnb: "numbound0 t" and np: "n > 0" 
     and snb: "numbound0 s" and mp:"m > 0"  by auto
   let ?st= "Add (Mul m t) (Mul n s)"
-  from mult_pos_pos[OF np mp] have mnp: "real (2*n*m) > 0" 
+  from np mp have mnp: "real (2*n*m) > 0" 
       by (simp add: mult_commute real_of_int_mult[symmetric] del: real_of_int_mult)
     from tnb snb have stnb: "numbound0 ?st" by simp
   have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)"
@@ -1807,7 +1805,7 @@
   from tnU smU U have tnb: "numbound0 t" and np: "n > 0" 
     and snb: "numbound0 s" and mp:"m > 0"  by auto
   let ?st= "Add (Mul m t) (Mul n s)"
-  from mult_pos_pos[OF np mp] have mnp: "real (2*n*m) > 0" 
+  from np mp have mnp: "real (2*n*m) > 0" 
       by (simp add: mult_commute real_of_int_mult[symmetric] del: real_of_int_mult)
     from tnb snb have stnb: "numbound0 ?st" by simp
   have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)"
@@ -1842,8 +1840,7 @@
   from uset_l[OF lq] have U_l: "\<forall> (t,n) \<in> set ?U. numbound0 t \<and> n > 0" .
   from U_l UpU 
   have "\<forall> ((t,n),(s,m)) \<in> set ?Up. numbound0 t \<and> n> 0 \<and> numbound0 s \<and> m > 0" by auto
-  hence Snb: "\<forall> (t,n) \<in> set ?S. numbound0 t \<and> n > 0 "
-    by (auto simp add: mult_pos_pos)
+  hence Snb: "\<forall> (t,n) \<in> set ?S. numbound0 t \<and> n > 0 " by auto
   have Y_l: "\<forall> (t,n) \<in> set ?Y. numbound0 t \<and> n > 0" 
   proof-
     { fix t n assume tnY: "(t,n) \<in> set ?Y" 
diff -r 9bd56f2e4c10 -r b60d5d119489 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -3096,15 +3096,15 @@
   from 5 mult_strict_left_mono[OF dp cp, simplified real_of_int_less_iff[symmetric] 
     real_of_int_mult]
   show ?case using 5 dp 
-    by (simp add: add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"] 
-      algebra_simps)
+    by (simp add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"] 
+      algebra_simps del: mult_pos_pos)
 next
   case (6 c e) hence cp: "c > 0" by simp
   from 6 mult_strict_left_mono[OF dp cp, simplified real_of_int_less_iff[symmetric] 
     real_of_int_mult]
   show ?case using 6 dp 
-    by (simp add: add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"] 
-      algebra_simps)
+    by (simp add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"] 
+      algebra_simps del: mult_pos_pos)
 next
   case (7 c e) hence cp: "c >0" and nb: "numbound0 e" and ei: "isint e (real i#bs)"
     and nob: "\<forall> j\<in> {1 .. c*d}. real (c*i) \<noteq> - ?N i e + real j"
@@ -4747,8 +4747,7 @@
       with \<Upsilon>_l[OF lp] have tnb: "numbound0 t" and np:"real n > 0" and snb: "numbound0 s" and mp:"real m > 0"
         by auto
       let ?st = "Add (Mul m t) (Mul n s)"
-      from mult_pos_pos[OF np mp] have mnp: "real (2*n*m) > 0" 
-        by (simp add: mult_commute)
+      from np mp have mnp: "real (2*n*m) > 0" by (simp add: mult_commute)
       from tnb snb have st_nb: "numbound0 ?st" by simp
       have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)"
         using mnp mp np by (simp add: algebra_simps add_divide_distrib)
@@ -4764,8 +4763,7 @@
     and px:"?I x (\<upsilon> p (Add (Mul l t) (Mul k s), 2*k*l))"
     with \<Upsilon>_l[OF lp] have tnb: "numbound0 t" and np:"real k > 0" and snb: "numbound0 s" and mp:"real l > 0" by auto
     let ?st = "Add (Mul l t) (Mul k s)"
-    from mult_pos_pos[OF np mp] have mnp: "real (2*k*l) > 0" 
-      by (simp add: mult_commute)
+    from np mp have mnp: "real (2*k*l) > 0" by (simp add: mult_commute)
     from tnb snb have st_nb: "numbound0 ?st" by simp
     from \<upsilon>_I[OF lp mnp st_nb, where bs="bs"] px have "?E" by auto}
   ultimately show "?E" by blast
@@ -4885,8 +4883,7 @@
     from aU bU \<Upsilon>_l[OF lrq] have tnb: "numbound0 t" and np:"real n > 0" and snb: "numbound0 s" and mp:"real m > 0" by (auto simp add: split_def)
     let ?st = "Add (Mul m t) (Mul n s)"
     from tnb snb have stnb: "numbound0 ?st" by simp
-    from mult_pos_pos[OF np mp] have mnp: "real (2*n*m) > 0" 
-      by (simp add: mult_commute)
+    from np mp have mnp: "real (2*n*m) > 0" by (simp add: mult_commute)
     from conjunct1[OF \<upsilon>_I[OF lrq mnp stnb, where bs="bs" and x="x"], symmetric] rqx
     have "\<exists> x. ?I x ?rq" by auto
     thus "?E" 
@@ -4966,7 +4963,7 @@
   from tnU smU U have tnb: "numbound0 t" and np: "n > 0" 
     and snb: "numbound0 s" and mp:"m > 0"  by auto
   let ?st= "Add (Mul m t) (Mul n s)"
-  from mult_pos_pos[OF np mp] have mnp: "real (2*n*m) > 0" 
+  from np mp have mnp: "real (2*n*m) > 0" 
       by (simp add: mult_commute real_of_int_mult[symmetric] del: real_of_int_mult)
     from tnb snb have stnb: "numbound0 ?st" by simp
   have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)"
@@ -4994,7 +4991,7 @@
   from tnU smU U have tnb: "numbound0 t" and np: "n > 0" 
     and snb: "numbound0 s" and mp:"m > 0"  by auto
   let ?st= "Add (Mul m t) (Mul n s)"
-  from mult_pos_pos[OF np mp] have mnp: "real (2*n*m) > 0" 
+  from np mp have mnp: "real (2*n*m) > 0" 
       by (simp add: mult_commute real_of_int_mult[symmetric] del: real_of_int_mult)
     from tnb snb have stnb: "numbound0 ?st" by simp
   have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)"
@@ -5030,7 +5027,7 @@
   from U_l UpU 
   have "\<forall> ((t,n),(s,m)) \<in> set ?Up. numbound0 t \<and> n> 0 \<and> numbound0 s \<and> m > 0" by auto
   hence Snb: "\<forall> (t,n) \<in> set ?S. numbound0 t \<and> n > 0 "
-    by (auto simp add: mult_pos_pos)
+    by (auto)
   have Y_l: "\<forall> (t,n) \<in> set ?Y. numbound0 t \<and> n > 0" 
   proof-
     { fix t n assume tnY: "(t,n) \<in> set ?Y" 
diff -r 9bd56f2e4c10 -r b60d5d119489 src/HOL/Decision_Procs/Rat_Pair.thy
--- a/src/HOL/Decision_Procs/Rat_Pair.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Decision_Procs/Rat_Pair.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -114,7 +114,7 @@
   moreover
   { assume a: "a \<noteq>0" and a': "a'\<noteq>0"
     hence bp: "b > 0" "b' > 0" using xn yn x y by (simp_all add: isnormNum_def)
-    from mult_pos_pos[OF bp] have "x *\<^sub>N y = normNum (a * a', b * b')"
+    from bp have "x *\<^sub>N y = normNum (a * a', b * b')"
       using x y a a' bp by (simp add: Nmul_def Let_def split_def normNum_def)
     hence ?thesis by simp }
   ultimately show ?thesis by blast
diff -r 9bd56f2e4c10 -r b60d5d119489 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Groups_Big.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -1244,7 +1244,7 @@
 
 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::linordered_semidom) < f x)
   --> 0 < setprod f A"
-by (cases "finite A", induct set: finite, simp_all add: mult_pos_pos)
+by (cases "finite A", induct set: finite, simp_all)
 
 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
   (setprod f (A - {a}) :: 'a :: {field}) =
diff -r 9bd56f2e4c10 -r b60d5d119489 src/HOL/Library/BigO.thy
--- a/src/HOL/Library/BigO.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Library/BigO.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -62,8 +62,7 @@
   apply (auto simp add: bigo_alt_def)
   apply (rule_tac x = "ca * c" in exI)
   apply (rule conjI)
-  apply (rule mult_pos_pos)
-  apply assumption+
+  apply simp
   apply (rule allI)
   apply (drule_tac x = "xa" in spec)+
   apply (subgoal_tac "ca * abs (f xa) \<le> ca * (c * abs (g xa))")
diff -r 9bd56f2e4c10 -r b60d5d119489 src/HOL/Library/Convex.thy
--- a/src/HOL/Library/Convex.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Library/Convex.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -391,7 +391,7 @@
   { assume "\<mu> \<noteq> 1" "\<mu> \<noteq> 0"
     then have "\<mu> > 0" "(1 - \<mu>) > 0" using asms by auto
     then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0" using asms
-      by (auto simp add: add_pos_pos mult_pos_pos) }
+      by (auto simp add: add_pos_pos) }
   ultimately show "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x > 0" using assms by fastforce
 qed
 
@@ -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: mult_pos_pos)
+    using `b > 1` by (auto intro!:less_imp_le)
   from f''_ge0_imp_convex[OF pos_is_convex,
     unfolded greaterThan_iff, OF f' f''0 f''_ge0]
   show ?thesis by auto
diff -r 9bd56f2e4c10 -r b60d5d119489 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Library/Float.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -751,7 +751,7 @@
   assumes "b > 0"
   shows "bitlen (b * 2 ^ c) = bitlen b + c"
 proof -
-  from assms have "b * 2 ^ c > 0" by (auto intro: mult_pos_pos)
+  from assms have "b * 2 ^ c > 0" by auto
   thus ?thesis
     using floor_add[of "log 2 b" c] assms
     by (auto simp add: log_mult log_nat_power bitlen_def)
@@ -1108,7 +1108,7 @@
   shows "0 \<le> real (lapprox_rat n x y)"
 using assms unfolding lapprox_rat_def p_def[symmetric] round_down_def real_of_int_minus[symmetric]
    powr_int[of 2, simplified]
-  by (auto simp add: inverse_eq_divide intro!: mult_nonneg_nonneg divide_nonneg_pos mult_pos_pos)
+  by (auto simp add: inverse_eq_divide intro!: mult_nonneg_nonneg divide_nonneg_pos)
 
 lemma rapprox_rat: "real x / real y \<le> real (rapprox_rat prec x y)"
   using round_up by (simp add: rapprox_rat_def)
@@ -1230,10 +1230,10 @@
       by (intro powr_mono) auto
     also have "\<dots> \<le> \<lfloor>2 powr 0\<rfloor>" by simp
     also have "\<dots> \<le> \<lfloor>2 powr real p / x\<rfloor>" unfolding real_of_int_le_iff
-      using x x_le by (intro floor_mono) (simp add:  pos_le_divide_eq mult_pos_pos)
+      using x x_le by (intro floor_mono) (simp add:  pos_le_divide_eq)
     finally show ?thesis
       using prec x unfolding p_def[symmetric]
-      by (simp add: round_down_def powr_minus_divide pos_le_divide_eq mult_pos_pos)
+      by (simp add: round_down_def powr_minus_divide pos_le_divide_eq)
   qed
 qed
 
@@ -1485,7 +1485,7 @@
       by simp
     also have "\<dots> \<le> y * 2 powr real prec / (2 powr (real \<lfloor>log 2 y\<rfloor> + 1))"
       using `0 \<le> y` `0 \<le> x` assms(2)
-      by (auto intro!: powr_mono mult_pos_pos divide_left_mono
+      by (auto intro!: powr_mono divide_left_mono
         simp: real_of_nat_diff powr_add
         powr_divide2[symmetric])
     also have "\<dots> = y * 2 powr real prec / (2 powr real \<lfloor>log 2 y\<rfloor> * 2)"
diff -r 9bd56f2e4c10 -r b60d5d119489 src/HOL/Library/Function_Growth.thy
--- a/src/HOL/Library/Function_Growth.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Library/Function_Growth.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -223,7 +223,7 @@
         with * show "f m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by (rule order_trans)
       qed
       then have "\<exists>n. \<forall>m>n. f m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by rule
-      moreover from `c\<^sub>1 > 0` `c\<^sub>2 > 0` have "c\<^sub>1 * c\<^sub>2 > 0" by (rule mult_pos_pos)
+      moreover from `c\<^sub>1 > 0` `c\<^sub>2 > 0` have "c\<^sub>1 * c\<^sub>2 > 0" by simp
       ultimately show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * h m" by blast
     qed
   qed
diff -r 9bd56f2e4c10 -r b60d5d119489 src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -361,7 +361,7 @@
     from real_lbound_gt_zero[OF one0 em0]
     obtain d where d: "d >0" "d < 1" "d < e / m" by blast
     from d(1,3) m(1) have dm: "d*m > 0" "d*m < e"
-      by (simp_all add: field_simps mult_pos_pos)
+      by (simp_all add: field_simps)
     show ?case
       proof(rule ex_forward[OF real_lbound_gt_zero[OF one0 em0]], clarsimp simp add: norm_mult)
         fix d w
diff -r 9bd56f2e4c10 -r b60d5d119489 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Library/Polynomial.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -1109,7 +1109,7 @@
 lemma pos_poly_mult: "\<lbrakk>pos_poly p; pos_poly q\<rbrakk> \<Longrightarrow> pos_poly (p * q)"
   unfolding pos_poly_def
   apply (subgoal_tac "p \<noteq> 0 \<and> q \<noteq> 0")
-  apply (simp add: degree_mult_eq coeff_mult_degree_sum mult_pos_pos)
+  apply (simp add: degree_mult_eq coeff_mult_degree_sum)
   apply auto
   done
 
diff -r 9bd56f2e4c10 -r b60d5d119489 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -3299,7 +3299,7 @@
   then have "ball (x - e *\<^sub>R (x - c)) (e*d) \<inter> affine hull S \<subseteq> S"
     by auto
   moreover have "e * d > 0"
-    using `e > 0` `d > 0` by (rule mult_pos_pos)
+    using `e > 0` `d > 0` by simp
   moreover have c: "c \<in> S"
     using assms rel_interior_subset by auto
   moreover from c have "x - e *\<^sub>R (x - c) \<in> S"
@@ -3453,7 +3453,7 @@
     case True
     then show ?thesis using `e > 0` `d > 0`
       apply (rule_tac bexI[where x=x])
-      apply (auto intro!: mult_pos_pos)
+      apply (auto)
       done
   next
     case False
@@ -3473,8 +3473,7 @@
     next
       case False
       then have "0 < e * d / (1 - e)" and *: "1 - e > 0"
-        using `e \<le> 1` `e > 0` `d > 0`
-        by (auto intro!:mult_pos_pos divide_pos_pos)
+        using `e \<le> 1` `e > 0` `d > 0` by (auto)
       then obtain y where "y \<in> S" "y \<noteq> x" "dist y x < e * d / (1 - e)"
         using x[unfolded islimpt_approachable,THEN spec[where x="e*d / (1 - e)"]] by auto
       then show ?thesis
@@ -3602,7 +3601,7 @@
     then have e1: "e1 > 0" "\<And>x. e1 * norm (f x) \<le> norm x"
       using K pos_le_divide_eq[of e1] by auto
     def e \<equiv> "e1 * e2"
-    then have "e > 0" using e1 e2 mult_pos_pos by auto
+    then have "e > 0" using e1 e2 by auto
     {
       fix y
       assume y: "y \<in> cball x e \<inter> affine hull S"
@@ -3645,8 +3644,7 @@
         subspace_span[of S] closed_subspace[of "span S"]
       by auto
     def e \<equiv> "e1 * e2"
-    then have "e > 0"
-      using e1 e2 mult_pos_pos by auto
+    hence "e > 0" using e1 e2 by auto
     {
       fix y
       assume y: "y \<in> cball (f x) e \<inter> affine hull (f ` S)"
@@ -6091,7 +6089,7 @@
       }
       ultimately show ?thesis by auto
     qed (insert `0<e`, auto)
-  qed (insert `0<e` `0<k` `0<B`, auto simp add:field_simps intro!:mult_pos_pos)
+  qed (insert `0<e` `0<k` `0<B`, auto simp: field_simps)
 qed
 
 
@@ -6513,7 +6511,7 @@
       using assms(3-5)
       apply auto
       done
-  qed (rule mult_pos_pos, insert `e>0` `d>0`, auto)
+  qed (insert `e>0` `d>0`, auto)
 qed
 
 lemma mem_interior_closure_convex_shrink:
@@ -6533,7 +6531,7 @@
     then show ?thesis
       using `e > 0` `d > 0`
       apply (rule_tac bexI[where x=x])
-      apply (auto intro!: mult_pos_pos)
+      apply (auto)
       done
   next
     case False
@@ -6553,8 +6551,7 @@
     next
       case False
       then have "0 < e * d / (1 - e)" and *: "1 - e > 0"
-        using `e \<le> 1` `e > 0` `d > 0`
-        by (auto intro!:mult_pos_pos divide_pos_pos)
+        using `e \<le> 1` `e > 0` `d > 0` by auto
       then obtain y where "y \<in> s" "y \<noteq> x" "dist y x < e * d / (1 - e)"
         using x[unfolded islimpt_approachable,THEN spec[where x="e*d / (1 - e)"]] by auto
       then show ?thesis
diff -r 9bd56f2e4c10 -r b60d5d119489 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -6738,7 +6738,7 @@
         defer
         apply (erule exE,rule_tac x=d in exI)
         using F e
-        apply (auto simp add:field_simps intro:mult_pos_pos)
+        apply (auto simp add:field_simps)
         done
     }
     {
@@ -6749,7 +6749,7 @@
         defer
         apply (erule exE,rule_tac x=d in exI)
         using F e
-        apply (auto simp add: field_simps intro: mult_pos_pos)
+        apply (auto simp add: field_simps)
         done
     }
   qed
@@ -7342,8 +7342,7 @@
   proof safe
     fix e :: real
     assume e: "e > 0"
-    then have "e * r > 0"
-      using assms(1) by (rule mult_pos_pos)
+    with assms(1) have "e * r > 0" by simp
     from assms(8)[unfolded has_integral,rule_format,OF this] guess d by (elim exE conjE) note d=this[rule_format]
     def d' \<equiv> "\<lambda>x. {y. g y \<in> d (g x)}"
     have d': "\<And>x. d' x = {y. g y \<in> (d (g x))}"
diff -r 9bd56f2e4c10 -r b60d5d119489 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -2832,9 +2832,7 @@
   then show ?thesis
     unfolding bounded_pos
     apply (rule_tac x="b*B" in exI)
-    using b B mult_pos_pos [of b B]
-    apply (auto simp add: mult_commute)
-    done
+    using b B by (auto simp add: mult_commute)
 qed
 
 lemma bounded_scaling:
@@ -4138,7 +4136,7 @@
   obtains n :: nat where "1 / (Suc n) < e"
 proof atomize_elim
   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`)
+    by (rule divide_strict_left_mono) (auto simp: `0 < e`)
   also have "1 / (ceiling (1/e)) \<le> 1 / (1/e)"
     by (rule divide_left_mono) (auto simp: `0 < e`)
   also have "\<dots> = e" by simp
@@ -5321,9 +5319,7 @@
       and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> s" using assms(2)[unfolded open_dist, THEN bspec[where x=x]]
       by auto
     have "e * abs c > 0"
-      using assms(1)[unfolded zero_less_abs_iff[symmetric]]
-      using mult_pos_pos[OF `e>0`]
-      by auto
+      using assms(1)[unfolded zero_less_abs_iff[symmetric]] `e>0` by auto
     moreover
     {
       fix y
@@ -7036,8 +7032,7 @@
     fix d :: real
     assume "d > 0"
     then obtain N where N:"\<forall>n\<ge>N. norm (f (x n) - f (x N)) < e * d"
-      using cf[unfolded cauchy o_def dist_norm, THEN spec[where x="e*d"]]
-        and e and mult_pos_pos[of e d]
+      using cf[unfolded cauchy o_def dist_norm, THEN spec[where x="e*d"]] e
       by auto
     {
       fix n
@@ -7400,7 +7395,7 @@
       then have "d>0" unfolding d_def using zero_le_dist[of "z 0" "z 1"]
         by (metis False d_def less_le)
       hence "0 < e * (1 - c) / d"
-        using `e>0` and `1-c>0` mult_pos_pos[of e "1 - c"] by auto
+        using `e>0` and `1-c>0` 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
       {
@@ -7411,7 +7406,7 @@
         have "1 - c ^ (m - n) > 0"
           using c and power_strict_mono[of c 1 "m - n"] using `m>n` 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
+          using `d>0` `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 9bd56f2e4c10 -r b60d5d119489 src/HOL/NSA/NSA.thy
--- a/src/HOL/NSA/NSA.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/NSA/NSA.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -570,7 +570,7 @@
 apply (simp only: linorder_not_less hnorm_mult)
 apply (drule_tac x = "r * s" in bspec)
 apply (fast intro: Reals_mult)
-apply (drule mp, blast intro: mult_pos_pos)
+apply (simp)
 apply (drule_tac c = s and d = "hnorm y" and a = r and b = "hnorm x" in mult_mono)
 apply (simp_all (no_asm_simp))
 done
diff -r 9bd56f2e4c10 -r b60d5d119489 src/HOL/Number_Theory/Gauss.thy
--- a/src/HOL/Number_Theory/Gauss.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -174,7 +174,7 @@
   by (auto simp add: B_def) (metis cong_prime_prod_zero_int A_ncong_p p_a_relprime p_prime)
 
 lemma B_greater_zero: "x \<in> B \<Longrightarrow> 0 < x"
-  using a_nonzero by (auto simp add: B_def mult_pos_pos A_greater_zero)
+  using a_nonzero by (auto simp add: B_def A_greater_zero)
 
 lemma C_greater_zero: "y \<in> C \<Longrightarrow> 0 < y"
 proof (auto simp add: C_def)
diff -r 9bd56f2e4c10 -r b60d5d119489 src/HOL/Old_Number_Theory/Chinese.thy
--- a/src/HOL/Old_Number_Theory/Chinese.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Chinese.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -68,10 +68,7 @@
 text {* \medskip @{term funprod} and @{term funsum} *}
 
 lemma funprod_pos: "(\<forall>i. i \<le> n --> 0 < mf i) ==> 0 < funprod mf 0 n"
-  apply (induct n)
-   apply auto
-  apply (simp add: zero_less_mult_iff)
-  done
+by (induct n) auto
 
 lemma funprod_zgcd [rule_format (no_asm)]:
   "(\<forall>i. k \<le> i \<and> i \<le> k + l --> zgcd (mf i) (mf m) = 1) -->
diff -r 9bd56f2e4c10 -r b60d5d119489 src/HOL/Old_Number_Theory/Gauss.thy
--- a/src/HOL/Old_Number_Theory/Gauss.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Gauss.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -175,7 +175,7 @@
   done
 
 lemma B_greater_zero: "x \<in> B ==> 0 < x"
-  using a_nonzero by (auto simp add: B_def mult_pos_pos A_greater_zero)
+  using a_nonzero by (auto simp add: B_def A_greater_zero)
 
 lemma C_ncong_p: "x \<in> C ==>  ~[x = 0](mod p)"
   apply (auto simp add: C_def)
diff -r 9bd56f2e4c10 -r b60d5d119489 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Power.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -297,7 +297,7 @@
 
 lemma zero_less_power [simp]:
   "0 < a \<Longrightarrow> 0 < a ^ n"
-  by (induct n) (simp_all add: mult_pos_pos)
+  by (induct n) simp_all
 
 lemma zero_le_power [simp]:
   "0 \<le> a \<Longrightarrow> 0 \<le> a ^ n"
diff -r 9bd56f2e4c10 -r b60d5d119489 src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Probability/Information.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -1062,7 +1062,7 @@
       with goal1 have "0 < Px (fst x)" "0 < Pz (snd (snd x))" "0 < Pxz (fst x, snd (snd x))" "0 < Pyz (snd x)" "0 < Pxyz x"
         by auto
       then show ?thesis
-        using b_gt_1 by (simp add: log_simps mult_pos_pos less_imp_le field_simps)
+        using b_gt_1 by (simp add: log_simps less_imp_le field_simps)
     qed simp
   qed
   with I1 I2 show ?eq
@@ -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: mult_pos_pos)
+      by eventually_elim (auto)
     show "integrable ?P ?f"
       unfolding integrable_def 
       using fin neg by (auto simp: split_beta')
@@ -1280,7 +1280,7 @@
       with goal1 have "0 < Px (fst x)" "0 < Pz (snd (snd x))" "0 < Pxz (fst x, snd (snd x))" "0 < Pyz (snd x)" "0 < Pxyz x"
         by auto
       then show ?thesis
-        using b_gt_1 by (simp add: log_simps mult_pos_pos less_imp_le field_simps)
+        using b_gt_1 by (simp add: log_simps less_imp_le field_simps)
     qed simp
   qed
 
@@ -1419,7 +1419,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: mult_pos_pos)
+      by eventually_elim (auto)
     show "integrable ?P ?f"
       unfolding integrable_def
       using fin neg by (auto simp: split_beta')
@@ -1601,7 +1601,7 @@
     by eventually_elim auto
   then have ae: "AE x in S \<Otimes>\<^sub>M T.
      Pxy x * log b (Pxy x) - Pxy x * log b (Py (snd x)) = Pxy x * log b (Pxy x / Py (snd x))"
-    by eventually_elim (auto simp: log_simps mult_pos_pos field_simps b_gt_1)
+    by eventually_elim (auto simp: log_simps field_simps b_gt_1)
   have "conditional_entropy b S T X Y = 
     - (\<integral>x. Pxy x * log b (Pxy x) - Pxy x * log b (Py (snd x)) \<partial>(S \<Otimes>\<^sub>M T))"
     unfolding conditional_entropy_generic_eq[OF S T Py Pxy] neg_equal_iff_equal
@@ -1752,7 +1752,7 @@
       with goal1 have "0 < Px (fst x)" "0 < Py (snd x)" "0 < Pxy x"
         by auto
       then show ?thesis
-        using b_gt_1 by (simp add: log_simps mult_pos_pos less_imp_le field_simps)
+        using b_gt_1 by (simp add: log_simps less_imp_le field_simps)
     qed simp
   qed
 
diff -r 9bd56f2e4c10 -r b60d5d119489 src/HOL/Probability/Regularity.thy
--- a/src/HOL/Probability/Regularity.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Probability/Regularity.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -144,7 +144,7 @@
   } note M_space = this
   {
     fix e ::real and n :: nat assume "e > 0" "n > 0"
-    hence "1/n > 0" "e * 2 powr - n > 0" by (auto intro: mult_pos_pos)
+    hence "1/n > 0" "e * 2 powr - n > 0" by (auto)
     from M_space[OF `1/n>0`]
     have "(\<lambda>k. measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n))) ----> measure M (space M)"
       unfolding emeasure_eq_measure by simp
@@ -271,7 +271,7 @@
         show "?G (1 / real (Suc i)) \<in> sets M" by (simp add: sb borel_open)
       next
         show "decseq (\<lambda>i. {x. infdist x A < 1 / real (Suc i)})"
-          by (auto intro: less_trans intro!: divide_strict_left_mono mult_pos_pos
+          by (auto intro: less_trans intro!: divide_strict_left_mono
             simp: decseq_def le_eq_less_or_eq)
       qed simp
       finally
diff -r 9bd56f2e4c10 -r b60d5d119489 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Rat.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -429,7 +429,7 @@
 apply transfer
 apply (simp add: zero_less_mult_iff)
 apply (elim disjE, simp_all add: add_pos_pos add_neg_neg
-  mult_pos_pos mult_pos_neg mult_neg_pos mult_neg_neg)
+  mult_pos_neg mult_neg_pos mult_neg_neg)
 done
 
 lemma positive_mult:
@@ -726,7 +726,7 @@
 proof (induct r, induct s)
   fix a b c d :: int
   assume not_zero: "b > 0" "d > 0"
-  then have "b * d > 0" by (rule mult_pos_pos)
+  then have "b * d > 0" by simp
   have of_int_divide_less_eq:
     "(of_int a :: 'a) / of_int b < of_int c / of_int d
       \<longleftrightarrow> (of_int a :: 'a) * of_int d < of_int c * of_int b"
diff -r 9bd56f2e4c10 -r b60d5d119489 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Real.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -282,8 +282,7 @@
   from b i have nz: "\<forall>n\<ge>i. X n \<noteq> 0" by auto
   obtain s where s: "0 < s" and r: "r = inverse b * s * inverse b"
   proof
-    show "0 < b * r * b"
-      by (simp add: `0 < r` b mult_pos_pos)
+    show "0 < b * r * b" by (simp add: `0 < r` b)
     show "r = inverse b * (b * r * b) * inverse b"
       using b by simp
   qed
@@ -297,7 +296,7 @@
       by (simp add: inverse_diff_inverse nz * abs_mult)
     also have "\<dots> < inverse b * s * inverse b"
       by (simp add: mult_strict_mono less_imp_inverse_less
-                    mult_pos_pos i j b * s)
+                    i j b * s)
     finally show "\<bar>inverse (X m) - inverse (X n)\<bar> < r" unfolding r .
   qed
   thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>inverse (X m) - inverse (X n)\<bar> < r" ..
@@ -317,7 +316,7 @@
   obtain s where s: "0 < s" and "inverse a * s * inverse b = r"
   proof
     show "0 < a * r * b"
-      using a r b by (simp add: mult_pos_pos)
+      using a r b by simp
     show "inverse a * (a * r * b) * inverse b = r"
       using a r b by simp
   qed
@@ -564,7 +563,7 @@
   "positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x * y)"
 apply transfer
 apply (clarify, rename_tac a b i j)
-apply (rule_tac x="a * b" in exI, simp add: mult_pos_pos)
+apply (rule_tac x="a * b" in exI, simp)
 apply (rule_tac x="max i j" in exI, clarsimp)
 apply (rule mult_strict_mono, auto)
 done
@@ -907,7 +906,7 @@
       have "\<bar>(b - a) / 2 ^ n\<bar> = \<bar>b - a\<bar> / 2 ^ n"
         by simp
       also have "\<dots> \<le> \<bar>b - a\<bar> / 2 ^ k"
-        using n by (simp add: divide_left_mono mult_pos_pos)
+        using n by (simp add: divide_left_mono)
       also note k
       finally show "\<bar>(b - a) / 2 ^ n\<bar> < r" .
     qed
diff -r 9bd56f2e4c10 -r b60d5d119489 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Rings.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -568,7 +568,7 @@
   "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
 by (force simp add: mult_strict_right_mono not_less [symmetric])
 
-lemma mult_pos_pos: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
+lemma mult_pos_pos[simp]: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
 using mult_strict_left_mono [of 0 b a] by simp
 
 lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
@@ -602,7 +602,7 @@
   assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c"
   shows "a * c < b * d"
   using assms apply (cases "c=0")
-  apply (simp add: mult_pos_pos)
+  apply (simp)
   apply (erule mult_strict_right_mono [THEN less_trans])
   apply (force simp add: le_less)
   apply (erule mult_strict_left_mono, assumption)
@@ -824,7 +824,7 @@
       show ?thesis by (auto dest: mult_strict_right_mono_neg)
     next
       case False with B have "0 < b" by auto
-      with A' show ?thesis by (auto dest: mult_pos_pos)
+      with A' show ?thesis by auto
     qed
   qed
   then show "a * b \<noteq> 0" by (simp add: neq_iff)
@@ -832,7 +832,7 @@
 
 lemma zero_less_mult_iff: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
   by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
-     (auto simp add: mult_pos_pos mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2)
+     (auto simp add: mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2)
 
 lemma zero_le_mult_iff: "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
   by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
diff -r 9bd56f2e4c10 -r b60d5d119489 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Transcendental.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -1465,7 +1465,7 @@
   also have "... <= (1 + x + x\<^sup>2) / exp (x \<^sup>2)"
     by (metis a b divide_right_mono exp_bound exp_ge_zero)
   also have "... <= (1 + x + x\<^sup>2) / (1 + x\<^sup>2)"
-    by (simp add: a divide_left_mono mult_pos_pos add_pos_nonneg)
+    by (simp add: a divide_left_mono add_pos_nonneg)
   also from a have "... <= 1 + x"
     by (simp add: field_simps add_strict_increasing zero_le_mult_iff)
   finally have "exp (x - x\<^sup>2) <= 1 + x" .
@@ -2378,7 +2378,7 @@
       by (intro mult_strict_right_mono zero_less_power `0 < x`)
     thus "0 < ?f n"
       by (simp del: mult_Suc,
-        simp add: less_divide_eq mult_pos_pos field_simps del: mult_Suc)
+        simp add: less_divide_eq field_simps del: mult_Suc)
   qed
   have sums: "?f sums sin x"
     by (rule sin_paired [THEN sums_group], simp)
@@ -2962,8 +2962,7 @@
   hence "0 < cos z" using cos_gt_zero_pi by auto
   hence inv_pos: "0 < inverse ((cos z)\<^sup>2)" by auto
   have "0 < x - y" using `y < x` by auto
-  from mult_pos_pos [OF this inv_pos]
-  have "0 < tan x - tan y" unfolding tan_diff by auto
+  with inv_pos have "0 < tan x - tan y" unfolding tan_diff by auto
   thus ?thesis by auto
 qed
 
diff -r 9bd56f2e4c10 -r b60d5d119489 src/HOL/ex/Dedekind_Real.thy
--- a/src/HOL/ex/Dedekind_Real.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/ex/Dedekind_Real.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -368,7 +368,7 @@
   from preal_exists_bound [OF B] obtain y where 2 [simp]: "0 < y" "y \<notin> B" by blast
   show ?thesis
   proof (intro exI conjI)
-    show "0 < x*y" by (simp add: mult_pos_pos)
+    show "0 < x*y" by simp
     show "x * y \<notin> mult_set A B"
     proof -
       {