--- 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 = _")
--- 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"
--- 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"
--- 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
--- 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}) =
--- 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))")
--- 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
--- 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)"
--- 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
--- 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
--- 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
--- 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
--- 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))}"
--- 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`
--- 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
--- 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)
--- 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) -->
--- 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)
--- 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"
--- 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
--- 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
--- 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"
--- 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
--- 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)
--- 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
--- 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 -
{