made mult_pos_pos a simp rule
authornipkow
Sat Apr 12 17:26:27 2014 +0200 (2014-04-12)
changeset 56544b60d5d119489
parent 56543 9bd56f2e4c10
child 56545 8f1e7596deb7
made mult_pos_pos a simp rule
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Decision_Procs/Rat_Pair.thy
src/HOL/Groups_Big.thy
src/HOL/Library/BigO.thy
src/HOL/Library/Convex.thy
src/HOL/Library/Float.thy
src/HOL/Library/Function_Growth.thy
src/HOL/Library/Fundamental_Theorem_Algebra.thy
src/HOL/Library/Polynomial.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/NSA/NSA.thy
src/HOL/Number_Theory/Gauss.thy
src/HOL/Old_Number_Theory/Chinese.thy
src/HOL/Old_Number_Theory/Gauss.thy
src/HOL/Power.thy
src/HOL/Probability/Information.thy
src/HOL/Probability/Regularity.thy
src/HOL/Rat.thy
src/HOL/Real.thy
src/HOL/Rings.thy
src/HOL/Transcendental.thy
src/HOL/ex/Dedekind_Real.thy
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Fri Apr 11 23:22:00 2014 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Sat Apr 12 17:26:27 2014 +0200
     1.3 @@ -734,8 +734,7 @@
     1.4  proof (cases "real x = 0")
     1.5    case False hence "real x \<noteq> 0" by auto
     1.6    hence "0 < x" and "0 < real x" using `0 \<le> real x` by auto
     1.7 -  have "0 < x * x" using `0 < x`
     1.8 -    using mult_pos_pos[where a="real x" and b="real x"] by auto
     1.9 +  have "0 < x * x" using `0 < x` by simp
    1.10  
    1.11    { fix x n have "(\<Sum> i=0..<n. -1^i * (1/real (fact (2 * i))) * x ^ (2 * i))
    1.12      = (\<Sum> i = 0 ..< 2 * n. (if even(i) then (-1 ^ (i div 2))/(real (fact i)) else 0) * x ^ i)" (is "?sum = ?ifsum")
    1.13 @@ -851,8 +850,7 @@
    1.14  proof (cases "real x = 0")
    1.15    case False hence "real x \<noteq> 0" by auto
    1.16    hence "0 < x" and "0 < real x" using `0 \<le> real x` by auto
    1.17 -  have "0 < x * x" using `0 < x`
    1.18 -    using mult_pos_pos[where a="real x" and b="real x"] by auto
    1.19 +  have "0 < x * x" using `0 < x` by simp
    1.20  
    1.21    { 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))
    1.22      = (\<Sum> i = 0 ..< 2 * n. (if even(i) then 0 else (-1 ^ ((i - Suc 0) div 2))/(real (fact i))) * x ^ i)" (is "?SUM = _")
     2.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Fri Apr 11 23:22:00 2014 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Sat Apr 12 17:26:27 2014 +0200
     2.3 @@ -1674,8 +1674,7 @@
     2.4        with uset_l[OF lp] have tnb: "numbound0 t" and np:"real n > 0" and snb: "numbound0 s" and mp:"real m > 0"
     2.5          by auto
     2.6        let ?st = "Add (Mul m t) (Mul n s)"
     2.7 -      from mult_pos_pos[OF np mp] have mnp: "real (2*n*m) > 0" 
     2.8 -        by (simp add: mult_commute)
     2.9 +      from np mp have mnp: "real (2*n*m) > 0" by (simp add: mult_commute)
    2.10        from tnb snb have st_nb: "numbound0 ?st" by simp
    2.11        have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)"
    2.12          using mnp mp np by (simp add: algebra_simps add_divide_distrib)
    2.13 @@ -1691,8 +1690,7 @@
    2.14      and px:"?I x (usubst p (Add (Mul l t) (Mul k s), 2*k*l))"
    2.15      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
    2.16      let ?st = "Add (Mul l t) (Mul k s)"
    2.17 -    from mult_pos_pos[OF np mp] have mnp: "real (2*k*l) > 0" 
    2.18 -      by (simp add: mult_commute)
    2.19 +    from np mp have mnp: "real (2*k*l) > 0" by (simp add: mult_commute)
    2.20      from tnb snb have st_nb: "numbound0 ?st" by simp
    2.21      from usubst_I[OF lp mnp st_nb, where bs="bs"] px have "?E" by auto}
    2.22    ultimately show "?E" by blast
    2.23 @@ -1779,7 +1777,7 @@
    2.24    from tnU smU U have tnb: "numbound0 t" and np: "n > 0" 
    2.25      and snb: "numbound0 s" and mp:"m > 0"  by auto
    2.26    let ?st= "Add (Mul m t) (Mul n s)"
    2.27 -  from mult_pos_pos[OF np mp] have mnp: "real (2*n*m) > 0" 
    2.28 +  from np mp have mnp: "real (2*n*m) > 0" 
    2.29        by (simp add: mult_commute real_of_int_mult[symmetric] del: real_of_int_mult)
    2.30      from tnb snb have stnb: "numbound0 ?st" by simp
    2.31    have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)"
    2.32 @@ -1807,7 +1805,7 @@
    2.33    from tnU smU U have tnb: "numbound0 t" and np: "n > 0" 
    2.34      and snb: "numbound0 s" and mp:"m > 0"  by auto
    2.35    let ?st= "Add (Mul m t) (Mul n s)"
    2.36 -  from mult_pos_pos[OF np mp] have mnp: "real (2*n*m) > 0" 
    2.37 +  from np mp have mnp: "real (2*n*m) > 0" 
    2.38        by (simp add: mult_commute real_of_int_mult[symmetric] del: real_of_int_mult)
    2.39      from tnb snb have stnb: "numbound0 ?st" by simp
    2.40    have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)"
    2.41 @@ -1842,8 +1840,7 @@
    2.42    from uset_l[OF lq] have U_l: "\<forall> (t,n) \<in> set ?U. numbound0 t \<and> n > 0" .
    2.43    from U_l UpU 
    2.44    have "\<forall> ((t,n),(s,m)) \<in> set ?Up. numbound0 t \<and> n> 0 \<and> numbound0 s \<and> m > 0" by auto
    2.45 -  hence Snb: "\<forall> (t,n) \<in> set ?S. numbound0 t \<and> n > 0 "
    2.46 -    by (auto simp add: mult_pos_pos)
    2.47 +  hence Snb: "\<forall> (t,n) \<in> set ?S. numbound0 t \<and> n > 0 " by auto
    2.48    have Y_l: "\<forall> (t,n) \<in> set ?Y. numbound0 t \<and> n > 0" 
    2.49    proof-
    2.50      { fix t n assume tnY: "(t,n) \<in> set ?Y" 
     3.1 --- a/src/HOL/Decision_Procs/MIR.thy	Fri Apr 11 23:22:00 2014 +0200
     3.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Sat Apr 12 17:26:27 2014 +0200
     3.3 @@ -3096,15 +3096,15 @@
     3.4    from 5 mult_strict_left_mono[OF dp cp, simplified real_of_int_less_iff[symmetric] 
     3.5      real_of_int_mult]
     3.6    show ?case using 5 dp 
     3.7 -    by (simp add: add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"] 
     3.8 -      algebra_simps)
     3.9 +    by (simp add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"] 
    3.10 +      algebra_simps del: mult_pos_pos)
    3.11  next
    3.12    case (6 c e) hence cp: "c > 0" by simp
    3.13    from 6 mult_strict_left_mono[OF dp cp, simplified real_of_int_less_iff[symmetric] 
    3.14      real_of_int_mult]
    3.15    show ?case using 6 dp 
    3.16 -    by (simp add: add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"] 
    3.17 -      algebra_simps)
    3.18 +    by (simp add: numbound0_I[where bs="bs" and b="real i - real d" and b'="real i"] 
    3.19 +      algebra_simps del: mult_pos_pos)
    3.20  next
    3.21    case (7 c e) hence cp: "c >0" and nb: "numbound0 e" and ei: "isint e (real i#bs)"
    3.22      and nob: "\<forall> j\<in> {1 .. c*d}. real (c*i) \<noteq> - ?N i e + real j"
    3.23 @@ -4747,8 +4747,7 @@
    3.24        with \<Upsilon>_l[OF lp] have tnb: "numbound0 t" and np:"real n > 0" and snb: "numbound0 s" and mp:"real m > 0"
    3.25          by auto
    3.26        let ?st = "Add (Mul m t) (Mul n s)"
    3.27 -      from mult_pos_pos[OF np mp] have mnp: "real (2*n*m) > 0" 
    3.28 -        by (simp add: mult_commute)
    3.29 +      from np mp have mnp: "real (2*n*m) > 0" by (simp add: mult_commute)
    3.30        from tnb snb have st_nb: "numbound0 ?st" by simp
    3.31        have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)"
    3.32          using mnp mp np by (simp add: algebra_simps add_divide_distrib)
    3.33 @@ -4764,8 +4763,7 @@
    3.34      and px:"?I x (\<upsilon> p (Add (Mul l t) (Mul k s), 2*k*l))"
    3.35      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
    3.36      let ?st = "Add (Mul l t) (Mul k s)"
    3.37 -    from mult_pos_pos[OF np mp] have mnp: "real (2*k*l) > 0" 
    3.38 -      by (simp add: mult_commute)
    3.39 +    from np mp have mnp: "real (2*k*l) > 0" by (simp add: mult_commute)
    3.40      from tnb snb have st_nb: "numbound0 ?st" by simp
    3.41      from \<upsilon>_I[OF lp mnp st_nb, where bs="bs"] px have "?E" by auto}
    3.42    ultimately show "?E" by blast
    3.43 @@ -4885,8 +4883,7 @@
    3.44      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)
    3.45      let ?st = "Add (Mul m t) (Mul n s)"
    3.46      from tnb snb have stnb: "numbound0 ?st" by simp
    3.47 -    from mult_pos_pos[OF np mp] have mnp: "real (2*n*m) > 0" 
    3.48 -      by (simp add: mult_commute)
    3.49 +    from np mp have mnp: "real (2*n*m) > 0" by (simp add: mult_commute)
    3.50      from conjunct1[OF \<upsilon>_I[OF lrq mnp stnb, where bs="bs" and x="x"], symmetric] rqx
    3.51      have "\<exists> x. ?I x ?rq" by auto
    3.52      thus "?E" 
    3.53 @@ -4966,7 +4963,7 @@
    3.54    from tnU smU U have tnb: "numbound0 t" and np: "n > 0" 
    3.55      and snb: "numbound0 s" and mp:"m > 0"  by auto
    3.56    let ?st= "Add (Mul m t) (Mul n s)"
    3.57 -  from mult_pos_pos[OF np mp] have mnp: "real (2*n*m) > 0" 
    3.58 +  from np mp have mnp: "real (2*n*m) > 0" 
    3.59        by (simp add: mult_commute real_of_int_mult[symmetric] del: real_of_int_mult)
    3.60      from tnb snb have stnb: "numbound0 ?st" by simp
    3.61    have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)"
    3.62 @@ -4994,7 +4991,7 @@
    3.63    from tnU smU U have tnb: "numbound0 t" and np: "n > 0" 
    3.64      and snb: "numbound0 s" and mp:"m > 0"  by auto
    3.65    let ?st= "Add (Mul m t) (Mul n s)"
    3.66 -  from mult_pos_pos[OF np mp] have mnp: "real (2*n*m) > 0" 
    3.67 +  from np mp have mnp: "real (2*n*m) > 0" 
    3.68        by (simp add: mult_commute real_of_int_mult[symmetric] del: real_of_int_mult)
    3.69      from tnb snb have stnb: "numbound0 ?st" by simp
    3.70    have st: "(?N t / real n + ?N s / real m)/2 = ?N ?st / real (2*n*m)"
    3.71 @@ -5030,7 +5027,7 @@
    3.72    from U_l UpU 
    3.73    have "\<forall> ((t,n),(s,m)) \<in> set ?Up. numbound0 t \<and> n> 0 \<and> numbound0 s \<and> m > 0" by auto
    3.74    hence Snb: "\<forall> (t,n) \<in> set ?S. numbound0 t \<and> n > 0 "
    3.75 -    by (auto simp add: mult_pos_pos)
    3.76 +    by (auto)
    3.77    have Y_l: "\<forall> (t,n) \<in> set ?Y. numbound0 t \<and> n > 0" 
    3.78    proof-
    3.79      { fix t n assume tnY: "(t,n) \<in> set ?Y" 
     4.1 --- a/src/HOL/Decision_Procs/Rat_Pair.thy	Fri Apr 11 23:22:00 2014 +0200
     4.2 +++ b/src/HOL/Decision_Procs/Rat_Pair.thy	Sat Apr 12 17:26:27 2014 +0200
     4.3 @@ -114,7 +114,7 @@
     4.4    moreover
     4.5    { assume a: "a \<noteq>0" and a': "a'\<noteq>0"
     4.6      hence bp: "b > 0" "b' > 0" using xn yn x y by (simp_all add: isnormNum_def)
     4.7 -    from mult_pos_pos[OF bp] have "x *\<^sub>N y = normNum (a * a', b * b')"
     4.8 +    from bp have "x *\<^sub>N y = normNum (a * a', b * b')"
     4.9        using x y a a' bp by (simp add: Nmul_def Let_def split_def normNum_def)
    4.10      hence ?thesis by simp }
    4.11    ultimately show ?thesis by blast
     5.1 --- a/src/HOL/Groups_Big.thy	Fri Apr 11 23:22:00 2014 +0200
     5.2 +++ b/src/HOL/Groups_Big.thy	Sat Apr 12 17:26:27 2014 +0200
     5.3 @@ -1244,7 +1244,7 @@
     5.4  
     5.5  lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::linordered_semidom) < f x)
     5.6    --> 0 < setprod f A"
     5.7 -by (cases "finite A", induct set: finite, simp_all add: mult_pos_pos)
     5.8 +by (cases "finite A", induct set: finite, simp_all)
     5.9  
    5.10  lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
    5.11    (setprod f (A - {a}) :: 'a :: {field}) =
     6.1 --- a/src/HOL/Library/BigO.thy	Fri Apr 11 23:22:00 2014 +0200
     6.2 +++ b/src/HOL/Library/BigO.thy	Sat Apr 12 17:26:27 2014 +0200
     6.3 @@ -62,8 +62,7 @@
     6.4    apply (auto simp add: bigo_alt_def)
     6.5    apply (rule_tac x = "ca * c" in exI)
     6.6    apply (rule conjI)
     6.7 -  apply (rule mult_pos_pos)
     6.8 -  apply assumption+
     6.9 +  apply simp
    6.10    apply (rule allI)
    6.11    apply (drule_tac x = "xa" in spec)+
    6.12    apply (subgoal_tac "ca * abs (f xa) \<le> ca * (c * abs (g xa))")
     7.1 --- a/src/HOL/Library/Convex.thy	Fri Apr 11 23:22:00 2014 +0200
     7.2 +++ b/src/HOL/Library/Convex.thy	Sat Apr 12 17:26:27 2014 +0200
     7.3 @@ -391,7 +391,7 @@
     7.4    { assume "\<mu> \<noteq> 1" "\<mu> \<noteq> 0"
     7.5      then have "\<mu> > 0" "(1 - \<mu>) > 0" using asms by auto
     7.6      then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0" using asms
     7.7 -      by (auto simp add: add_pos_pos mult_pos_pos) }
     7.8 +      by (auto simp add: add_pos_pos) }
     7.9    ultimately show "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x > 0" using assms by fastforce
    7.10  qed
    7.11  
    7.12 @@ -666,7 +666,7 @@
    7.13    then have f''0: "\<And>z :: real. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)"
    7.14      unfolding inverse_eq_divide by (auto simp add: mult_assoc)
    7.15    have f''_ge0: "\<And>z :: real. z > 0 \<Longrightarrow> 1 / (ln b * z * z) \<ge> 0"
    7.16 -    using `b > 1` by (auto intro!:less_imp_le simp add: mult_pos_pos)
    7.17 +    using `b > 1` by (auto intro!:less_imp_le)
    7.18    from f''_ge0_imp_convex[OF pos_is_convex,
    7.19      unfolded greaterThan_iff, OF f' f''0 f''_ge0]
    7.20    show ?thesis by auto
     8.1 --- a/src/HOL/Library/Float.thy	Fri Apr 11 23:22:00 2014 +0200
     8.2 +++ b/src/HOL/Library/Float.thy	Sat Apr 12 17:26:27 2014 +0200
     8.3 @@ -751,7 +751,7 @@
     8.4    assumes "b > 0"
     8.5    shows "bitlen (b * 2 ^ c) = bitlen b + c"
     8.6  proof -
     8.7 -  from assms have "b * 2 ^ c > 0" by (auto intro: mult_pos_pos)
     8.8 +  from assms have "b * 2 ^ c > 0" by auto
     8.9    thus ?thesis
    8.10      using floor_add[of "log 2 b" c] assms
    8.11      by (auto simp add: log_mult log_nat_power bitlen_def)
    8.12 @@ -1108,7 +1108,7 @@
    8.13    shows "0 \<le> real (lapprox_rat n x y)"
    8.14  using assms unfolding lapprox_rat_def p_def[symmetric] round_down_def real_of_int_minus[symmetric]
    8.15     powr_int[of 2, simplified]
    8.16 -  by (auto simp add: inverse_eq_divide intro!: mult_nonneg_nonneg divide_nonneg_pos mult_pos_pos)
    8.17 +  by (auto simp add: inverse_eq_divide intro!: mult_nonneg_nonneg divide_nonneg_pos)
    8.18  
    8.19  lemma rapprox_rat: "real x / real y \<le> real (rapprox_rat prec x y)"
    8.20    using round_up by (simp add: rapprox_rat_def)
    8.21 @@ -1230,10 +1230,10 @@
    8.22        by (intro powr_mono) auto
    8.23      also have "\<dots> \<le> \<lfloor>2 powr 0\<rfloor>" by simp
    8.24      also have "\<dots> \<le> \<lfloor>2 powr real p / x\<rfloor>" unfolding real_of_int_le_iff
    8.25 -      using x x_le by (intro floor_mono) (simp add:  pos_le_divide_eq mult_pos_pos)
    8.26 +      using x x_le by (intro floor_mono) (simp add:  pos_le_divide_eq)
    8.27      finally show ?thesis
    8.28        using prec x unfolding p_def[symmetric]
    8.29 -      by (simp add: round_down_def powr_minus_divide pos_le_divide_eq mult_pos_pos)
    8.30 +      by (simp add: round_down_def powr_minus_divide pos_le_divide_eq)
    8.31    qed
    8.32  qed
    8.33  
    8.34 @@ -1485,7 +1485,7 @@
    8.35        by simp
    8.36      also have "\<dots> \<le> y * 2 powr real prec / (2 powr (real \<lfloor>log 2 y\<rfloor> + 1))"
    8.37        using `0 \<le> y` `0 \<le> x` assms(2)
    8.38 -      by (auto intro!: powr_mono mult_pos_pos divide_left_mono
    8.39 +      by (auto intro!: powr_mono divide_left_mono
    8.40          simp: real_of_nat_diff powr_add
    8.41          powr_divide2[symmetric])
    8.42      also have "\<dots> = y * 2 powr real prec / (2 powr real \<lfloor>log 2 y\<rfloor> * 2)"
     9.1 --- a/src/HOL/Library/Function_Growth.thy	Fri Apr 11 23:22:00 2014 +0200
     9.2 +++ b/src/HOL/Library/Function_Growth.thy	Sat Apr 12 17:26:27 2014 +0200
     9.3 @@ -223,7 +223,7 @@
     9.4          with * show "f m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by (rule order_trans)
     9.5        qed
     9.6        then have "\<exists>n. \<forall>m>n. f m \<le> (c\<^sub>1 * c\<^sub>2) * h m" by rule
     9.7 -      moreover from `c\<^sub>1 > 0` `c\<^sub>2 > 0` have "c\<^sub>1 * c\<^sub>2 > 0" by (rule mult_pos_pos)
     9.8 +      moreover from `c\<^sub>1 > 0` `c\<^sub>2 > 0` have "c\<^sub>1 * c\<^sub>2 > 0" by simp
     9.9        ultimately show "\<exists>c>0. \<exists>n. \<forall>m>n. f m \<le> c * h m" by blast
    9.10      qed
    9.11    qed
    10.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Fri Apr 11 23:22:00 2014 +0200
    10.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Sat Apr 12 17:26:27 2014 +0200
    10.3 @@ -361,7 +361,7 @@
    10.4      from real_lbound_gt_zero[OF one0 em0]
    10.5      obtain d where d: "d >0" "d < 1" "d < e / m" by blast
    10.6      from d(1,3) m(1) have dm: "d*m > 0" "d*m < e"
    10.7 -      by (simp_all add: field_simps mult_pos_pos)
    10.8 +      by (simp_all add: field_simps)
    10.9      show ?case
   10.10        proof(rule ex_forward[OF real_lbound_gt_zero[OF one0 em0]], clarsimp simp add: norm_mult)
   10.11          fix d w
    11.1 --- a/src/HOL/Library/Polynomial.thy	Fri Apr 11 23:22:00 2014 +0200
    11.2 +++ b/src/HOL/Library/Polynomial.thy	Sat Apr 12 17:26:27 2014 +0200
    11.3 @@ -1109,7 +1109,7 @@
    11.4  lemma pos_poly_mult: "\<lbrakk>pos_poly p; pos_poly q\<rbrakk> \<Longrightarrow> pos_poly (p * q)"
    11.5    unfolding pos_poly_def
    11.6    apply (subgoal_tac "p \<noteq> 0 \<and> q \<noteq> 0")
    11.7 -  apply (simp add: degree_mult_eq coeff_mult_degree_sum mult_pos_pos)
    11.8 +  apply (simp add: degree_mult_eq coeff_mult_degree_sum)
    11.9    apply auto
   11.10    done
   11.11  
    12.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Apr 11 23:22:00 2014 +0200
    12.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sat Apr 12 17:26:27 2014 +0200
    12.3 @@ -3299,7 +3299,7 @@
    12.4    then have "ball (x - e *\<^sub>R (x - c)) (e*d) \<inter> affine hull S \<subseteq> S"
    12.5      by auto
    12.6    moreover have "e * d > 0"
    12.7 -    using `e > 0` `d > 0` by (rule mult_pos_pos)
    12.8 +    using `e > 0` `d > 0` by simp
    12.9    moreover have c: "c \<in> S"
   12.10      using assms rel_interior_subset by auto
   12.11    moreover from c have "x - e *\<^sub>R (x - c) \<in> S"
   12.12 @@ -3453,7 +3453,7 @@
   12.13      case True
   12.14      then show ?thesis using `e > 0` `d > 0`
   12.15        apply (rule_tac bexI[where x=x])
   12.16 -      apply (auto intro!: mult_pos_pos)
   12.17 +      apply (auto)
   12.18        done
   12.19    next
   12.20      case False
   12.21 @@ -3473,8 +3473,7 @@
   12.22      next
   12.23        case False
   12.24        then have "0 < e * d / (1 - e)" and *: "1 - e > 0"
   12.25 -        using `e \<le> 1` `e > 0` `d > 0`
   12.26 -        by (auto intro!:mult_pos_pos divide_pos_pos)
   12.27 +        using `e \<le> 1` `e > 0` `d > 0` by (auto)
   12.28        then obtain y where "y \<in> S" "y \<noteq> x" "dist y x < e * d / (1 - e)"
   12.29          using x[unfolded islimpt_approachable,THEN spec[where x="e*d / (1 - e)"]] by auto
   12.30        then show ?thesis
   12.31 @@ -3602,7 +3601,7 @@
   12.32      then have e1: "e1 > 0" "\<And>x. e1 * norm (f x) \<le> norm x"
   12.33        using K pos_le_divide_eq[of e1] by auto
   12.34      def e \<equiv> "e1 * e2"
   12.35 -    then have "e > 0" using e1 e2 mult_pos_pos by auto
   12.36 +    then have "e > 0" using e1 e2 by auto
   12.37      {
   12.38        fix y
   12.39        assume y: "y \<in> cball x e \<inter> affine hull S"
   12.40 @@ -3645,8 +3644,7 @@
   12.41          subspace_span[of S] closed_subspace[of "span S"]
   12.42        by auto
   12.43      def e \<equiv> "e1 * e2"
   12.44 -    then have "e > 0"
   12.45 -      using e1 e2 mult_pos_pos by auto
   12.46 +    hence "e > 0" using e1 e2 by auto
   12.47      {
   12.48        fix y
   12.49        assume y: "y \<in> cball (f x) e \<inter> affine hull (f ` S)"
   12.50 @@ -6091,7 +6089,7 @@
   12.51        }
   12.52        ultimately show ?thesis by auto
   12.53      qed (insert `0<e`, auto)
   12.54 -  qed (insert `0<e` `0<k` `0<B`, auto simp add:field_simps intro!:mult_pos_pos)
   12.55 +  qed (insert `0<e` `0<k` `0<B`, auto simp: field_simps)
   12.56  qed
   12.57  
   12.58  
   12.59 @@ -6513,7 +6511,7 @@
   12.60        using assms(3-5)
   12.61        apply auto
   12.62        done
   12.63 -  qed (rule mult_pos_pos, insert `e>0` `d>0`, auto)
   12.64 +  qed (insert `e>0` `d>0`, auto)
   12.65  qed
   12.66  
   12.67  lemma mem_interior_closure_convex_shrink:
   12.68 @@ -6533,7 +6531,7 @@
   12.69      then show ?thesis
   12.70        using `e > 0` `d > 0`
   12.71        apply (rule_tac bexI[where x=x])
   12.72 -      apply (auto intro!: mult_pos_pos)
   12.73 +      apply (auto)
   12.74        done
   12.75    next
   12.76      case False
   12.77 @@ -6553,8 +6551,7 @@
   12.78      next
   12.79        case False
   12.80        then have "0 < e * d / (1 - e)" and *: "1 - e > 0"
   12.81 -        using `e \<le> 1` `e > 0` `d > 0`
   12.82 -        by (auto intro!:mult_pos_pos divide_pos_pos)
   12.83 +        using `e \<le> 1` `e > 0` `d > 0` by auto
   12.84        then obtain y where "y \<in> s" "y \<noteq> x" "dist y x < e * d / (1 - e)"
   12.85          using x[unfolded islimpt_approachable,THEN spec[where x="e*d / (1 - e)"]] by auto
   12.86        then show ?thesis
    13.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Apr 11 23:22:00 2014 +0200
    13.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Sat Apr 12 17:26:27 2014 +0200
    13.3 @@ -6738,7 +6738,7 @@
    13.4          defer
    13.5          apply (erule exE,rule_tac x=d in exI)
    13.6          using F e
    13.7 -        apply (auto simp add:field_simps intro:mult_pos_pos)
    13.8 +        apply (auto simp add:field_simps)
    13.9          done
   13.10      }
   13.11      {
   13.12 @@ -6749,7 +6749,7 @@
   13.13          defer
   13.14          apply (erule exE,rule_tac x=d in exI)
   13.15          using F e
   13.16 -        apply (auto simp add: field_simps intro: mult_pos_pos)
   13.17 +        apply (auto simp add: field_simps)
   13.18          done
   13.19      }
   13.20    qed
   13.21 @@ -7342,8 +7342,7 @@
   13.22    proof safe
   13.23      fix e :: real
   13.24      assume e: "e > 0"
   13.25 -    then have "e * r > 0"
   13.26 -      using assms(1) by (rule mult_pos_pos)
   13.27 +    with assms(1) have "e * r > 0" by simp
   13.28      from assms(8)[unfolded has_integral,rule_format,OF this] guess d by (elim exE conjE) note d=this[rule_format]
   13.29      def d' \<equiv> "\<lambda>x. {y. g y \<in> d (g x)}"
   13.30      have d': "\<And>x. d' x = {y. g y \<in> (d (g x))}"
    14.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Apr 11 23:22:00 2014 +0200
    14.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Apr 12 17:26:27 2014 +0200
    14.3 @@ -2832,9 +2832,7 @@
    14.4    then show ?thesis
    14.5      unfolding bounded_pos
    14.6      apply (rule_tac x="b*B" in exI)
    14.7 -    using b B mult_pos_pos [of b B]
    14.8 -    apply (auto simp add: mult_commute)
    14.9 -    done
   14.10 +    using b B by (auto simp add: mult_commute)
   14.11  qed
   14.12  
   14.13  lemma bounded_scaling:
   14.14 @@ -4138,7 +4136,7 @@
   14.15    obtains n :: nat where "1 / (Suc n) < e"
   14.16  proof atomize_elim
   14.17    have " 1 / real (Suc (nat (ceiling (1/e)))) < 1 / (ceiling (1/e))"
   14.18 -    by (rule divide_strict_left_mono) (auto intro!: mult_pos_pos simp: `0 < e`)
   14.19 +    by (rule divide_strict_left_mono) (auto simp: `0 < e`)
   14.20    also have "1 / (ceiling (1/e)) \<le> 1 / (1/e)"
   14.21      by (rule divide_left_mono) (auto simp: `0 < e`)
   14.22    also have "\<dots> = e" by simp
   14.23 @@ -5321,9 +5319,7 @@
   14.24        and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> s" using assms(2)[unfolded open_dist, THEN bspec[where x=x]]
   14.25        by auto
   14.26      have "e * abs c > 0"
   14.27 -      using assms(1)[unfolded zero_less_abs_iff[symmetric]]
   14.28 -      using mult_pos_pos[OF `e>0`]
   14.29 -      by auto
   14.30 +      using assms(1)[unfolded zero_less_abs_iff[symmetric]] `e>0` by auto
   14.31      moreover
   14.32      {
   14.33        fix y
   14.34 @@ -7036,8 +7032,7 @@
   14.35      fix d :: real
   14.36      assume "d > 0"
   14.37      then obtain N where N:"\<forall>n\<ge>N. norm (f (x n) - f (x N)) < e * d"
   14.38 -      using cf[unfolded cauchy o_def dist_norm, THEN spec[where x="e*d"]]
   14.39 -        and e and mult_pos_pos[of e d]
   14.40 +      using cf[unfolded cauchy o_def dist_norm, THEN spec[where x="e*d"]] e
   14.41        by auto
   14.42      {
   14.43        fix n
   14.44 @@ -7400,7 +7395,7 @@
   14.45        then have "d>0" unfolding d_def using zero_le_dist[of "z 0" "z 1"]
   14.46          by (metis False d_def less_le)
   14.47        hence "0 < e * (1 - c) / d"
   14.48 -        using `e>0` and `1-c>0` mult_pos_pos[of e "1 - c"] by auto
   14.49 +        using `e>0` and `1-c>0` by auto
   14.50        then obtain N where N:"c ^ N < e * (1 - c) / d"
   14.51          using real_arch_pow_inv[of "e * (1 - c) / d" c] and c by auto
   14.52        {
   14.53 @@ -7411,7 +7406,7 @@
   14.54          have "1 - c ^ (m - n) > 0"
   14.55            using c and power_strict_mono[of c 1 "m - n"] using `m>n` by auto
   14.56          hence **: "d * (1 - c ^ (m - n)) / (1 - c) > 0"
   14.57 -          using mult_pos_pos[OF `d>0`, of "1 - c ^ (m - n)"] `0 < 1 - c` by auto
   14.58 +          using `d>0` `0 < 1 - c` by auto
   14.59  
   14.60          have "dist (z m) (z n) \<le> c ^ n * d * (1 - c ^ (m - n)) / (1 - c)"
   14.61            using cf_z2[of n "m - n"] and `m>n`
    15.1 --- a/src/HOL/NSA/NSA.thy	Fri Apr 11 23:22:00 2014 +0200
    15.2 +++ b/src/HOL/NSA/NSA.thy	Sat Apr 12 17:26:27 2014 +0200
    15.3 @@ -570,7 +570,7 @@
    15.4  apply (simp only: linorder_not_less hnorm_mult)
    15.5  apply (drule_tac x = "r * s" in bspec)
    15.6  apply (fast intro: Reals_mult)
    15.7 -apply (drule mp, blast intro: mult_pos_pos)
    15.8 +apply (simp)
    15.9  apply (drule_tac c = s and d = "hnorm y" and a = r and b = "hnorm x" in mult_mono)
   15.10  apply (simp_all (no_asm_simp))
   15.11  done
    16.1 --- a/src/HOL/Number_Theory/Gauss.thy	Fri Apr 11 23:22:00 2014 +0200
    16.2 +++ b/src/HOL/Number_Theory/Gauss.thy	Sat Apr 12 17:26:27 2014 +0200
    16.3 @@ -174,7 +174,7 @@
    16.4    by (auto simp add: B_def) (metis cong_prime_prod_zero_int A_ncong_p p_a_relprime p_prime)
    16.5  
    16.6  lemma B_greater_zero: "x \<in> B \<Longrightarrow> 0 < x"
    16.7 -  using a_nonzero by (auto simp add: B_def mult_pos_pos A_greater_zero)
    16.8 +  using a_nonzero by (auto simp add: B_def A_greater_zero)
    16.9  
   16.10  lemma C_greater_zero: "y \<in> C \<Longrightarrow> 0 < y"
   16.11  proof (auto simp add: C_def)
    17.1 --- a/src/HOL/Old_Number_Theory/Chinese.thy	Fri Apr 11 23:22:00 2014 +0200
    17.2 +++ b/src/HOL/Old_Number_Theory/Chinese.thy	Sat Apr 12 17:26:27 2014 +0200
    17.3 @@ -68,10 +68,7 @@
    17.4  text {* \medskip @{term funprod} and @{term funsum} *}
    17.5  
    17.6  lemma funprod_pos: "(\<forall>i. i \<le> n --> 0 < mf i) ==> 0 < funprod mf 0 n"
    17.7 -  apply (induct n)
    17.8 -   apply auto
    17.9 -  apply (simp add: zero_less_mult_iff)
   17.10 -  done
   17.11 +by (induct n) auto
   17.12  
   17.13  lemma funprod_zgcd [rule_format (no_asm)]:
   17.14    "(\<forall>i. k \<le> i \<and> i \<le> k + l --> zgcd (mf i) (mf m) = 1) -->
    18.1 --- a/src/HOL/Old_Number_Theory/Gauss.thy	Fri Apr 11 23:22:00 2014 +0200
    18.2 +++ b/src/HOL/Old_Number_Theory/Gauss.thy	Sat Apr 12 17:26:27 2014 +0200
    18.3 @@ -175,7 +175,7 @@
    18.4    done
    18.5  
    18.6  lemma B_greater_zero: "x \<in> B ==> 0 < x"
    18.7 -  using a_nonzero by (auto simp add: B_def mult_pos_pos A_greater_zero)
    18.8 +  using a_nonzero by (auto simp add: B_def A_greater_zero)
    18.9  
   18.10  lemma C_ncong_p: "x \<in> C ==>  ~[x = 0](mod p)"
   18.11    apply (auto simp add: C_def)
    19.1 --- a/src/HOL/Power.thy	Fri Apr 11 23:22:00 2014 +0200
    19.2 +++ b/src/HOL/Power.thy	Sat Apr 12 17:26:27 2014 +0200
    19.3 @@ -297,7 +297,7 @@
    19.4  
    19.5  lemma zero_less_power [simp]:
    19.6    "0 < a \<Longrightarrow> 0 < a ^ n"
    19.7 -  by (induct n) (simp_all add: mult_pos_pos)
    19.8 +  by (induct n) simp_all
    19.9  
   19.10  lemma zero_le_power [simp]:
   19.11    "0 \<le> a \<Longrightarrow> 0 \<le> a ^ n"
    20.1 --- a/src/HOL/Probability/Information.thy	Fri Apr 11 23:22:00 2014 +0200
    20.2 +++ b/src/HOL/Probability/Information.thy	Sat Apr 12 17:26:27 2014 +0200
    20.3 @@ -1062,7 +1062,7 @@
    20.4        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"
    20.5          by auto
    20.6        then show ?thesis
    20.7 -        using b_gt_1 by (simp add: log_simps mult_pos_pos less_imp_le field_simps)
    20.8 +        using b_gt_1 by (simp add: log_simps less_imp_le field_simps)
    20.9      qed simp
   20.10    qed
   20.11    with I1 I2 show ?eq
   20.12 @@ -1174,7 +1174,7 @@
   20.13      show "AE x in ?P. ?f x \<in> {0<..}"
   20.14        unfolding AE_density[OF distributed_borel_measurable[OF Pxyz]]
   20.15        using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
   20.16 -      by eventually_elim (auto simp: mult_pos_pos)
   20.17 +      by eventually_elim (auto)
   20.18      show "integrable ?P ?f"
   20.19        unfolding integrable_def 
   20.20        using fin neg by (auto simp: split_beta')
   20.21 @@ -1280,7 +1280,7 @@
   20.22        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"
   20.23          by auto
   20.24        then show ?thesis
   20.25 -        using b_gt_1 by (simp add: log_simps mult_pos_pos less_imp_le field_simps)
   20.26 +        using b_gt_1 by (simp add: log_simps less_imp_le field_simps)
   20.27      qed simp
   20.28    qed
   20.29  
   20.30 @@ -1419,7 +1419,7 @@
   20.31      show "AE x in ?P. ?f x \<in> {0<..}"
   20.32        unfolding AE_density[OF distributed_borel_measurable[OF Pxyz]]
   20.33        using ae1 ae2 ae3 ae4 ae5 ae6 ae7 ae8 Pxyz[THEN distributed_real_AE]
   20.34 -      by eventually_elim (auto simp: mult_pos_pos)
   20.35 +      by eventually_elim (auto)
   20.36      show "integrable ?P ?f"
   20.37        unfolding integrable_def
   20.38        using fin neg by (auto simp: split_beta')
   20.39 @@ -1601,7 +1601,7 @@
   20.40      by eventually_elim auto
   20.41    then have ae: "AE x in S \<Otimes>\<^sub>M T.
   20.42       Pxy x * log b (Pxy x) - Pxy x * log b (Py (snd x)) = Pxy x * log b (Pxy x / Py (snd x))"
   20.43 -    by eventually_elim (auto simp: log_simps mult_pos_pos field_simps b_gt_1)
   20.44 +    by eventually_elim (auto simp: log_simps field_simps b_gt_1)
   20.45    have "conditional_entropy b S T X Y = 
   20.46      - (\<integral>x. Pxy x * log b (Pxy x) - Pxy x * log b (Py (snd x)) \<partial>(S \<Otimes>\<^sub>M T))"
   20.47      unfolding conditional_entropy_generic_eq[OF S T Py Pxy] neg_equal_iff_equal
   20.48 @@ -1752,7 +1752,7 @@
   20.49        with goal1 have "0 < Px (fst x)" "0 < Py (snd x)" "0 < Pxy x"
   20.50          by auto
   20.51        then show ?thesis
   20.52 -        using b_gt_1 by (simp add: log_simps mult_pos_pos less_imp_le field_simps)
   20.53 +        using b_gt_1 by (simp add: log_simps less_imp_le field_simps)
   20.54      qed simp
   20.55    qed
   20.56  
    21.1 --- a/src/HOL/Probability/Regularity.thy	Fri Apr 11 23:22:00 2014 +0200
    21.2 +++ b/src/HOL/Probability/Regularity.thy	Sat Apr 12 17:26:27 2014 +0200
    21.3 @@ -144,7 +144,7 @@
    21.4    } note M_space = this
    21.5    {
    21.6      fix e ::real and n :: nat assume "e > 0" "n > 0"
    21.7 -    hence "1/n > 0" "e * 2 powr - n > 0" by (auto intro: mult_pos_pos)
    21.8 +    hence "1/n > 0" "e * 2 powr - n > 0" by (auto)
    21.9      from M_space[OF `1/n>0`]
   21.10      have "(\<lambda>k. measure M (\<Union>i\<in>{0..k}. cball (from_nat_into X i) (1/real n))) ----> measure M (space M)"
   21.11        unfolding emeasure_eq_measure by simp
   21.12 @@ -271,7 +271,7 @@
   21.13          show "?G (1 / real (Suc i)) \<in> sets M" by (simp add: sb borel_open)
   21.14        next
   21.15          show "decseq (\<lambda>i. {x. infdist x A < 1 / real (Suc i)})"
   21.16 -          by (auto intro: less_trans intro!: divide_strict_left_mono mult_pos_pos
   21.17 +          by (auto intro: less_trans intro!: divide_strict_left_mono
   21.18              simp: decseq_def le_eq_less_or_eq)
   21.19        qed simp
   21.20        finally
    22.1 --- a/src/HOL/Rat.thy	Fri Apr 11 23:22:00 2014 +0200
    22.2 +++ b/src/HOL/Rat.thy	Sat Apr 12 17:26:27 2014 +0200
    22.3 @@ -429,7 +429,7 @@
    22.4  apply transfer
    22.5  apply (simp add: zero_less_mult_iff)
    22.6  apply (elim disjE, simp_all add: add_pos_pos add_neg_neg
    22.7 -  mult_pos_pos mult_pos_neg mult_neg_pos mult_neg_neg)
    22.8 +  mult_pos_neg mult_neg_pos mult_neg_neg)
    22.9  done
   22.10  
   22.11  lemma positive_mult:
   22.12 @@ -726,7 +726,7 @@
   22.13  proof (induct r, induct s)
   22.14    fix a b c d :: int
   22.15    assume not_zero: "b > 0" "d > 0"
   22.16 -  then have "b * d > 0" by (rule mult_pos_pos)
   22.17 +  then have "b * d > 0" by simp
   22.18    have of_int_divide_less_eq:
   22.19      "(of_int a :: 'a) / of_int b < of_int c / of_int d
   22.20        \<longleftrightarrow> (of_int a :: 'a) * of_int d < of_int c * of_int b"
    23.1 --- a/src/HOL/Real.thy	Fri Apr 11 23:22:00 2014 +0200
    23.2 +++ b/src/HOL/Real.thy	Sat Apr 12 17:26:27 2014 +0200
    23.3 @@ -282,8 +282,7 @@
    23.4    from b i have nz: "\<forall>n\<ge>i. X n \<noteq> 0" by auto
    23.5    obtain s where s: "0 < s" and r: "r = inverse b * s * inverse b"
    23.6    proof
    23.7 -    show "0 < b * r * b"
    23.8 -      by (simp add: `0 < r` b mult_pos_pos)
    23.9 +    show "0 < b * r * b" by (simp add: `0 < r` b)
   23.10      show "r = inverse b * (b * r * b) * inverse b"
   23.11        using b by simp
   23.12    qed
   23.13 @@ -297,7 +296,7 @@
   23.14        by (simp add: inverse_diff_inverse nz * abs_mult)
   23.15      also have "\<dots> < inverse b * s * inverse b"
   23.16        by (simp add: mult_strict_mono less_imp_inverse_less
   23.17 -                    mult_pos_pos i j b * s)
   23.18 +                    i j b * s)
   23.19      finally show "\<bar>inverse (X m) - inverse (X n)\<bar> < r" unfolding r .
   23.20    qed
   23.21    thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>inverse (X m) - inverse (X n)\<bar> < r" ..
   23.22 @@ -317,7 +316,7 @@
   23.23    obtain s where s: "0 < s" and "inverse a * s * inverse b = r"
   23.24    proof
   23.25      show "0 < a * r * b"
   23.26 -      using a r b by (simp add: mult_pos_pos)
   23.27 +      using a r b by simp
   23.28      show "inverse a * (a * r * b) * inverse b = r"
   23.29        using a r b by simp
   23.30    qed
   23.31 @@ -564,7 +563,7 @@
   23.32    "positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x * y)"
   23.33  apply transfer
   23.34  apply (clarify, rename_tac a b i j)
   23.35 -apply (rule_tac x="a * b" in exI, simp add: mult_pos_pos)
   23.36 +apply (rule_tac x="a * b" in exI, simp)
   23.37  apply (rule_tac x="max i j" in exI, clarsimp)
   23.38  apply (rule mult_strict_mono, auto)
   23.39  done
   23.40 @@ -907,7 +906,7 @@
   23.41        have "\<bar>(b - a) / 2 ^ n\<bar> = \<bar>b - a\<bar> / 2 ^ n"
   23.42          by simp
   23.43        also have "\<dots> \<le> \<bar>b - a\<bar> / 2 ^ k"
   23.44 -        using n by (simp add: divide_left_mono mult_pos_pos)
   23.45 +        using n by (simp add: divide_left_mono)
   23.46        also note k
   23.47        finally show "\<bar>(b - a) / 2 ^ n\<bar> < r" .
   23.48      qed
    24.1 --- a/src/HOL/Rings.thy	Fri Apr 11 23:22:00 2014 +0200
    24.2 +++ b/src/HOL/Rings.thy	Sat Apr 12 17:26:27 2014 +0200
    24.3 @@ -568,7 +568,7 @@
    24.4    "a * c \<le> b * c \<Longrightarrow> 0 < c \<Longrightarrow> a \<le> b"
    24.5  by (force simp add: mult_strict_right_mono not_less [symmetric])
    24.6  
    24.7 -lemma mult_pos_pos: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
    24.8 +lemma mult_pos_pos[simp]: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
    24.9  using mult_strict_left_mono [of 0 b a] by simp
   24.10  
   24.11  lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
   24.12 @@ -602,7 +602,7 @@
   24.13    assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c"
   24.14    shows "a * c < b * d"
   24.15    using assms apply (cases "c=0")
   24.16 -  apply (simp add: mult_pos_pos)
   24.17 +  apply (simp)
   24.18    apply (erule mult_strict_right_mono [THEN less_trans])
   24.19    apply (force simp add: le_less)
   24.20    apply (erule mult_strict_left_mono, assumption)
   24.21 @@ -824,7 +824,7 @@
   24.22        show ?thesis by (auto dest: mult_strict_right_mono_neg)
   24.23      next
   24.24        case False with B have "0 < b" by auto
   24.25 -      with A' show ?thesis by (auto dest: mult_pos_pos)
   24.26 +      with A' show ?thesis by auto
   24.27      qed
   24.28    qed
   24.29    then show "a * b \<noteq> 0" by (simp add: neq_iff)
   24.30 @@ -832,7 +832,7 @@
   24.31  
   24.32  lemma zero_less_mult_iff: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
   24.33    by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
   24.34 -     (auto simp add: mult_pos_pos mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2)
   24.35 +     (auto simp add: mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2)
   24.36  
   24.37  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"
   24.38    by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
    25.1 --- a/src/HOL/Transcendental.thy	Fri Apr 11 23:22:00 2014 +0200
    25.2 +++ b/src/HOL/Transcendental.thy	Sat Apr 12 17:26:27 2014 +0200
    25.3 @@ -1465,7 +1465,7 @@
    25.4    also have "... <= (1 + x + x\<^sup>2) / exp (x \<^sup>2)"
    25.5      by (metis a b divide_right_mono exp_bound exp_ge_zero)
    25.6    also have "... <= (1 + x + x\<^sup>2) / (1 + x\<^sup>2)"
    25.7 -    by (simp add: a divide_left_mono mult_pos_pos add_pos_nonneg)
    25.8 +    by (simp add: a divide_left_mono add_pos_nonneg)
    25.9    also from a have "... <= 1 + x"
   25.10      by (simp add: field_simps add_strict_increasing zero_le_mult_iff)
   25.11    finally have "exp (x - x\<^sup>2) <= 1 + x" .
   25.12 @@ -2378,7 +2378,7 @@
   25.13        by (intro mult_strict_right_mono zero_less_power `0 < x`)
   25.14      thus "0 < ?f n"
   25.15        by (simp del: mult_Suc,
   25.16 -        simp add: less_divide_eq mult_pos_pos field_simps del: mult_Suc)
   25.17 +        simp add: less_divide_eq field_simps del: mult_Suc)
   25.18    qed
   25.19    have sums: "?f sums sin x"
   25.20      by (rule sin_paired [THEN sums_group], simp)
   25.21 @@ -2962,8 +2962,7 @@
   25.22    hence "0 < cos z" using cos_gt_zero_pi by auto
   25.23    hence inv_pos: "0 < inverse ((cos z)\<^sup>2)" by auto
   25.24    have "0 < x - y" using `y < x` by auto
   25.25 -  from mult_pos_pos [OF this inv_pos]
   25.26 -  have "0 < tan x - tan y" unfolding tan_diff by auto
   25.27 +  with inv_pos have "0 < tan x - tan y" unfolding tan_diff by auto
   25.28    thus ?thesis by auto
   25.29  qed
   25.30  
    26.1 --- a/src/HOL/ex/Dedekind_Real.thy	Fri Apr 11 23:22:00 2014 +0200
    26.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Sat Apr 12 17:26:27 2014 +0200
    26.3 @@ -368,7 +368,7 @@
    26.4    from preal_exists_bound [OF B] obtain y where 2 [simp]: "0 < y" "y \<notin> B" by blast
    26.5    show ?thesis
    26.6    proof (intro exI conjI)
    26.7 -    show "0 < x*y" by (simp add: mult_pos_pos)
    26.8 +    show "0 < x*y" by simp
    26.9      show "x * y \<notin> mult_set A B"
   26.10      proof -
   26.11        {