revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
--- a/src/HOL/Complex.thy Tue Apr 08 23:16:00 2014 +0200
+++ b/src/HOL/Complex.thy Wed Apr 09 09:37:47 2014 +0200
@@ -145,7 +145,7 @@
by (simp add: complex_inverse_def)
instance
- by intro_classes (simp_all add: complex_mult_def divide_minus_left
+ by intro_classes (simp_all add: complex_mult_def
distrib_left distrib_right right_diff_distrib left_diff_distrib
complex_inverse_def complex_divide_def
power2_eq_square add_divide_distrib [symmetric]
@@ -656,7 +656,7 @@
moreover have "!!u v. u / (x\<^sup>2 + y\<^sup>2) + v / (x\<^sup>2 + y\<^sup>2) = (u + v) / (x\<^sup>2 + y\<^sup>2)"
by (metis add_divide_distrib)
ultimately show ?thesis using Complex False `0 < x\<^sup>2 + y\<^sup>2`
- apply (simp add: complex_divide_def divide_minus_left zero_less_divide_iff less_divide_eq)
+ apply (simp add: complex_divide_def zero_less_divide_iff less_divide_eq)
apply (metis less_divide_eq mult_zero_left diff_conv_add_uminus minus_divide_left)
done
qed
@@ -844,7 +844,7 @@
real (fact n) *\<^sub>R Complex (cos_coeff n * b ^ n) (sin_coeff n * b ^ n)"
apply (induct n)
apply (simp add: cos_coeff_def sin_coeff_def)
- apply (simp add: sin_coeff_Suc cos_coeff_Suc divide_minus_left del: mult_Suc)
+ apply (simp add: sin_coeff_Suc cos_coeff_Suc del: mult_Suc)
done } note * = this
show "Re (cis b) = Re (exp (Complex 0 b))"
unfolding exp_def cis_def cos_def
--- a/src/HOL/Decision_Procs/Approximation.thy Tue Apr 08 23:16:00 2014 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Wed Apr 09 09:37:47 2014 +0200
@@ -1466,8 +1466,7 @@
using float_divr_nonpos_pos_upper_bound[OF `real x \<le> 0` `0 < real (- floor_fl x)`]
unfolding less_eq_float_def zero_float.rep_eq .
- have "exp x = exp (?num * (x / ?num))" using `real ?num \<noteq> 0`
- by (auto simp: divide_minus_left divide_minus_right)
+ have "exp x = exp (?num * (x / ?num))" using `real ?num \<noteq> 0` by auto
also have "\<dots> = exp (x / ?num) ^ ?num" unfolding exp_real_of_nat_mult ..
also have "\<dots> \<le> exp (float_divr prec x (- floor_fl x)) ^ ?num" unfolding num_eq fl_eq
by (rule power_mono, rule exp_le_cancel_iff[THEN iffD2], rule float_divr) auto
@@ -1487,16 +1486,15 @@
case False hence "0 \<le> real ?horner" by auto
have div_less_zero: "real (float_divl prec x (- floor_fl x)) \<le> 0"
- using `real (floor_fl x) < 0` `real x \<le> 0`
- by (auto simp: field_simps intro!: order_trans[OF float_divl])
+ using `real (floor_fl x) < 0` `real x \<le> 0` by (auto intro!: order_trans[OF float_divl] divide_nonpos_neg)
+
have "(?lb_exp_horner (float_divl prec x (- floor_fl x))) ^ ?num \<le>
exp (float_divl prec x (- floor_fl x)) ^ ?num"
using `0 \<le> real ?horner`[unfolded floor_fl_def[symmetric]] bnds_exp_horner[OF div_less_zero, unfolded atLeastAtMost_iff, THEN conjunct1] by (auto intro!: power_mono)
also have "\<dots> \<le> exp (x / ?num) ^ ?num" unfolding num_eq fl_eq
using float_divl by (auto intro!: power_mono simp del: uminus_float.rep_eq)
also have "\<dots> = exp (?num * (x / ?num))" unfolding exp_real_of_nat_mult ..
- also have "\<dots> = exp x" using `real ?num \<noteq> 0`
- by (auto simp: field_simps)
+ also have "\<dots> = exp x" using `real ?num \<noteq> 0` by auto
finally show ?thesis
unfolding lb_exp.simps if_not_P[OF `\<not> 0 < x`] if_P[OF `x < - 1`] int_floor_fl_def Let_def if_not_P[OF False] by auto
next
@@ -1508,8 +1506,7 @@
have "Float 1 -2 \<le> exp (x / (- floor_fl x))" unfolding Float_num .
hence "real (Float 1 -2) ^ ?num \<le> exp (x / (- floor_fl x)) ^ ?num"
by (auto intro!: power_mono)
- also have "\<dots> = exp x" unfolding num_eq fl_eq exp_real_of_nat_mult[symmetric]
- using `real (floor_fl x) \<noteq> 0` by (auto simp: field_simps)
+ also have "\<dots> = exp x" unfolding num_eq fl_eq exp_real_of_nat_mult[symmetric] using `real (floor_fl x) \<noteq> 0` by auto
finally show ?thesis
unfolding lb_exp.simps if_not_P[OF `\<not> 0 < x`] if_P[OF `x < - 1`] int_floor_fl_def Let_def if_P[OF True] real_of_float_power .
qed
--- a/src/HOL/Decision_Procs/Ferrack.thy Tue Apr 08 23:16:00 2014 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy Wed Apr 09 09:37:47 2014 +0200
@@ -1167,7 +1167,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
+ have "(real c * x > - ?e)" by (simp add: mult_ac)
hence "real c * x + ?e > 0" by arith
hence "real c * x + ?e \<noteq> 0" by simp
with xz have "?P ?z x (Eq (CN 0 c e))"
@@ -1184,7 +1184,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
+ have "(real c * x > - ?e)" by (simp add: mult_ac)
hence "real c * x + ?e > 0" by arith
hence "real c * x + ?e \<noteq> 0" by simp
with xz have "?P ?z x (NEq (CN 0 c e))"
@@ -1201,7 +1201,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
+ have "(real c * x > - ?e)" by (simp add: mult_ac)
hence "real c * x + ?e > 0" by arith
with xz have "?P ?z x (Lt (CN 0 c e))"
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -1217,7 +1217,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
+ have "(real c * x > - ?e)" by (simp add: mult_ac)
hence "real c * x + ?e > 0" by arith
with xz have "?P ?z x (Le (CN 0 c e))"
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -1233,7 +1233,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
+ have "(real c * x > - ?e)" by (simp add: mult_ac)
hence "real c * x + ?e > 0" by arith
with xz have "?P ?z x (Gt (CN 0 c e))"
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -1249,7 +1249,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
+ have "(real c * x > - ?e)" by (simp add: mult_ac)
hence "real c * x + ?e > 0" by arith
with xz have "?P ?z x (Ge (CN 0 c e))"
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
--- a/src/HOL/Decision_Procs/MIR.thy Tue Apr 08 23:16:00 2014 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Wed Apr 09 09:37:47 2014 +0200
@@ -2068,7 +2068,7 @@
from 3 have nbe: "numbound0 e" by simp
fix y
have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Eq (CN 0 c e))) = ?I x (Eq (CN 0 c e))"
- proof (simp add: divide_minus_left less_floor_eq , rule allI, rule impI)
+ proof (simp add: less_floor_eq , rule allI, rule impI)
fix x :: int
assume A: "real x + 1 \<le> - (Inum (y # bs) e / real c)"
hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
@@ -2085,7 +2085,7 @@
from 4 have nbe: "numbound0 e" by simp
fix y
have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (NEq (CN 0 c e))) = ?I x (NEq (CN 0 c e))"
- proof (simp add: divide_minus_left less_floor_eq , rule allI, rule impI)
+ proof (simp add: less_floor_eq , rule allI, rule impI)
fix x :: int
assume A: "real x + 1 \<le> - (Inum (y # bs) e / real c)"
hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
@@ -2102,7 +2102,7 @@
from 5 have nbe: "numbound0 e" by simp
fix y
have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Lt (CN 0 c e))) = ?I x (Lt (CN 0 c e))"
- proof (simp add: divide_minus_left less_floor_eq , rule allI, rule impI)
+ proof (simp add: less_floor_eq , rule allI, rule impI)
fix x :: int
assume A: "real x + 1 \<le> - (Inum (y # bs) e / real c)"
hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
@@ -2118,7 +2118,7 @@
from 6 have nbe: "numbound0 e" by simp
fix y
have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Le (CN 0 c e))) = ?I x (Le (CN 0 c e))"
- proof (simp add: divide_minus_left less_floor_eq , rule allI, rule impI)
+ proof (simp add: less_floor_eq , rule allI, rule impI)
fix x :: int
assume A: "real x + 1 \<le> - (Inum (y # bs) e / real c)"
hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
@@ -2134,7 +2134,7 @@
from 7 have nbe: "numbound0 e" by simp
fix y
have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Gt (CN 0 c e))) = ?I x (Gt (CN 0 c e))"
- proof (simp add: divide_minus_left less_floor_eq , rule allI, rule impI)
+ proof (simp add: less_floor_eq , rule allI, rule impI)
fix x :: int
assume A: "real x + 1 \<le> - (Inum (y # bs) e / real c)"
hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
@@ -2150,7 +2150,7 @@
from 8 have nbe: "numbound0 e" by simp
fix y
have "\<forall> x < (floor (- (Inum (y#bs) e) / (real c))). ?I x (?M (Ge (CN 0 c e))) = ?I x (Ge (CN 0 c e))"
- proof (simp add: divide_minus_left less_floor_eq , rule allI, rule impI)
+ proof (simp add: less_floor_eq , rule allI, rule impI)
fix x :: int
assume A: "real x + 1 \<le> - (Inum (y # bs) e / real c)"
hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
@@ -4267,7 +4267,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
+ have "(real c * x > - ?e)" by (simp add: mult_ac)
hence "real c * x + ?e > 0" by arith
hence "real c * x + ?e \<noteq> 0" by simp
with xz have "?P ?z x (Eq (CN 0 c e))"
@@ -4284,7 +4284,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
+ have "(real c * x > - ?e)" by (simp add: mult_ac)
hence "real c * x + ?e > 0" by arith
hence "real c * x + ?e \<noteq> 0" by simp
with xz have "?P ?z x (NEq (CN 0 c e))"
@@ -4301,7 +4301,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
+ have "(real c * x > - ?e)" by (simp add: mult_ac)
hence "real c * x + ?e > 0" by arith
with xz have "?P ?z x (Lt (CN 0 c e))"
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -4317,7 +4317,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
+ have "(real c * x > - ?e)" by (simp add: mult_ac)
hence "real c * x + ?e > 0" by arith
with xz have "?P ?z x (Le (CN 0 c e))"
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -4333,7 +4333,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
+ have "(real c * x > - ?e)" by (simp add: mult_ac)
hence "real c * x + ?e > 0" by arith
with xz have "?P ?z x (Gt (CN 0 c e))"
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
@@ -4349,7 +4349,7 @@
{fix x
assume xz: "x > ?z"
with mult_strict_right_mono [OF xz cp] cp
- have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
+ have "(real c * x > - ?e)" by (simp add: mult_ac)
hence "real c * x + ?e > 0" by arith
with xz have "?P ?z x (Ge (CN 0 c e))"
using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Tue Apr 08 23:16:00 2014 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Wed Apr 09 09:37:47 2014 +0200
@@ -2708,7 +2708,7 @@
have "?rhs = Ifm vs (-?s / (2*?d) # bs) (Eq (CNP 0 a r))"
by (simp only: th)
also have "\<dots> \<longleftrightarrow> ?a * (-?s / (2*?d)) + ?r = 0"
- by (simp add: field_simps r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"])
+ by (simp add: r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"])
also have "\<dots> \<longleftrightarrow> 2 * ?d * (?a * (-?s / (2*?d)) + ?r) = 0"
using d mult_cancel_left[of "2*?d" "(?a * (-?s / (2*?d)) + ?r)" 0] by simp
also have "\<dots> \<longleftrightarrow> (- ?a * ?s) * (2*?d / (2*?d)) + 2 * ?d * ?r= 0"
@@ -2728,12 +2728,12 @@
have "?rhs = Ifm vs (-?t / (2*?c) # bs) (Eq (CNP 0 a r))"
by (simp only: th)
also have "\<dots> \<longleftrightarrow> ?a * (-?t / (2*?c)) + ?r = 0"
- by (simp add: field_simps r[of "- (?t/ (2 * ?c))"])
+ by (simp add: r[of "- (?t/ (2 * ?c))"])
also have "\<dots> \<longleftrightarrow> 2 * ?c * (?a * (-?t / (2 * ?c)) + ?r) = 0"
using c mult_cancel_left[of "2 * ?c" "(?a * (-?t / (2 * ?c)) + ?r)" 0] by simp
also have "\<dots> \<longleftrightarrow> (?a * -?t)* (2 * ?c) / (2 * ?c) + 2 * ?c * ?r= 0"
by (simp add: field_simps distrib_left[of "2 * ?c"] del: distrib_left)
- also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2 * ?c * ?r = 0" using c by (simp add: field_simps)
+ also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2 * ?c * ?r = 0" using c by simp
finally have ?thesis using c d
by (simp add: r[of "- (?t/ (2 * ?c))"] msubsteq_def Let_def evaldjf_ex)
}
@@ -2755,7 +2755,7 @@
by simp
also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2 * ?c * ?d * ?r = 0"
using nonzero_mult_divide_cancel_left [OF dc] c d
- by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
+ by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally have ?thesis using c d
by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"]
msubsteq_def Let_def evaldjf_ex field_simps)
@@ -2825,7 +2825,7 @@
have "?rhs = Ifm vs (-?s / (2*?d) # bs) (NEq (CNP 0 a r))"
by (simp only: th)
also have "\<dots> \<longleftrightarrow> ?a * (-?s / (2*?d)) + ?r \<noteq> 0"
- by (simp add: field_simps r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"])
+ by (simp add: r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"])
also have "\<dots> \<longleftrightarrow> 2*?d * (?a * (-?s / (2*?d)) + ?r) \<noteq> 0"
using d mult_cancel_left[of "2*?d" "(?a * (-?s / (2*?d)) + ?r)" 0] by simp
also have "\<dots> \<longleftrightarrow> (- ?a * ?s) * (2*?d / (2*?d)) + 2*?d*?r\<noteq> 0"
@@ -2845,13 +2845,13 @@
have "?rhs = Ifm vs (-?t / (2*?c) # bs) (NEq (CNP 0 a r))"
by (simp only: th)
also have "\<dots> \<longleftrightarrow> ?a * (-?t / (2*?c)) + ?r \<noteq> 0"
- by (simp add: field_simps r[of "- (?t/ (2 * ?c))"])
+ by (simp add: r[of "- (?t/ (2 * ?c))"])
also have "\<dots> \<longleftrightarrow> 2*?c * (?a * (-?t / (2*?c)) + ?r) \<noteq> 0"
using c mult_cancel_left[of "2*?c" "(?a * (-?t / (2*?c)) + ?r)" 0] by simp
also have "\<dots> \<longleftrightarrow> (?a * -?t)* (2*?c) / (2*?c) + 2*?c*?r \<noteq> 0"
by (simp add: field_simps distrib_left[of "2*?c"] del: distrib_left)
also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2*?c*?r \<noteq> 0"
- using c by (simp add: field_simps)
+ using c by simp
finally have ?thesis
using c d by (simp add: r[of "- (?t/ (2*?c))"] msubstneq_def Let_def evaldjf_ex)
}
@@ -2873,7 +2873,7 @@
by simp
also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r \<noteq> 0"
using nonzero_mult_divide_cancel_left[OF dc] c d
- by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
+ by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally have ?thesis
using c d
by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"]
@@ -2963,7 +2963,7 @@
by simp
also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r < 0"
using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
- by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
+ by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally have ?thesis using dc c d nc nd dc'
by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"]
msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
@@ -2988,7 +2988,7 @@
by simp
also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - 2 * ?c * ?d * ?r < 0"
using nonzero_mult_divide_cancel_left[of "2 * ?c * ?d"] c d
- by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
+ by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally have ?thesis using dc c d nc nd
by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"]
msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
@@ -3005,14 +3005,14 @@
have "?rhs \<longleftrightarrow> Ifm vs (- ?t / (2 * ?c) # bs) (Lt (CNP 0 a r))"
by (simp only: th)
also have "\<dots> \<longleftrightarrow> ?a * (- ?t / (2 * ?c))+ ?r < 0"
- by (simp add: field_simps r[of "- (?t / (2 * ?c))"])
+ by (simp add: r[of "- (?t / (2 * ?c))"])
also have "\<dots> \<longleftrightarrow> 2 * ?c * (?a * (- ?t / (2 * ?c))+ ?r) < 0"
using c mult_less_cancel_left_disj[of "2 * ?c" "?a* (- ?t / (2*?c))+ ?r" 0] c' c''
order_less_not_sym[OF c'']
by simp
also have "\<dots> \<longleftrightarrow> - ?a * ?t + 2 * ?c * ?r < 0"
using nonzero_mult_divide_cancel_left[OF c'] c
- by (simp add: divide_minus_left algebra_simps diff_divide_distrib less_le del: distrib_right)
+ by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
finally have ?thesis using c d nc nd
by (simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps
lt polyneg_norm polymul_norm)
@@ -3029,7 +3029,7 @@
have "?rhs \<longleftrightarrow> Ifm vs (- ?t / (2*?c) # bs) (Lt (CNP 0 a r))"
by (simp only: th)
also have "\<dots> \<longleftrightarrow> ?a * (- ?t / (2*?c))+ ?r < 0"
- by (simp add: field_simps r[of "- (?t / (2*?c))"])
+ by (simp add: r[of "- (?t / (2*?c))"])
also have "\<dots> \<longleftrightarrow> 2 * ?c * (?a * (- ?t / (2 * ?c))+ ?r) > 0"
using c order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
mult_less_cancel_left_disj[of "2 * ?c" 0 "?a* (- ?t / (2*?c))+ ?r"]
@@ -3037,7 +3037,7 @@
also have "\<dots> \<longleftrightarrow> ?a*?t - 2*?c *?r < 0"
using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c'']
less_imp_neq[OF c''] c''
- by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
+ by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally have ?thesis using c d nc nd
by (simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps
lt polyneg_norm polymul_norm)
@@ -3054,14 +3054,14 @@
have "?rhs \<longleftrightarrow> Ifm vs (- ?s / (2 * ?d) # bs) (Lt (CNP 0 a r))"
by (simp only: th)
also have "\<dots> \<longleftrightarrow> ?a * (- ?s / (2 * ?d))+ ?r < 0"
- by (simp add: field_simps r[of "- (?s / (2 * ?d))"])
+ by (simp add: r[of "- (?s / (2 * ?d))"])
also have "\<dots> \<longleftrightarrow> 2 * ?d * (?a * (- ?s / (2 * ?d))+ ?r) < 0"
using d mult_less_cancel_left_disj[of "2 * ?d" "?a * (- ?s / (2 * ?d))+ ?r" 0] d' d''
order_less_not_sym[OF d'']
by simp
also have "\<dots> \<longleftrightarrow> - ?a * ?s+ 2 * ?d * ?r < 0"
using nonzero_mult_divide_cancel_left[OF d'] d
- by (simp add: divide_minus_left algebra_simps diff_divide_distrib less_le del: distrib_right)
+ by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
finally have ?thesis using c d nc nd
by (simp add: r[of "- (?s / (2*?d))"] msubstlt_def Let_def evaldjf_ex field_simps
lt polyneg_norm polymul_norm)
@@ -3078,7 +3078,7 @@
have "?rhs \<longleftrightarrow> Ifm vs (- ?s / (2 * ?d) # bs) (Lt (CNP 0 a r))"
by (simp only: th)
also have "\<dots> \<longleftrightarrow> ?a * (- ?s / (2 * ?d)) + ?r < 0"
- by (simp add: field_simps r[of "- (?s / (2 * ?d))"])
+ by (simp add: r[of "- (?s / (2 * ?d))"])
also have "\<dots> \<longleftrightarrow> 2 * ?d * (?a * (- ?s / (2 * ?d)) + ?r) > 0"
using d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
mult_less_cancel_left_disj[of "2 * ?d" 0 "?a* (- ?s / (2*?d))+ ?r"]
@@ -3086,7 +3086,7 @@
also have "\<dots> \<longleftrightarrow> ?a * ?s - 2 * ?d * ?r < 0"
using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d'']
less_imp_neq[OF d''] d''
- by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
+ by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally have ?thesis using c d nc nd
by (simp add: r[of "- (?s / (2*?d))"] msubstlt_def Let_def evaldjf_ex field_simps
lt polyneg_norm polymul_norm)
@@ -3177,7 +3177,7 @@
by simp
also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r \<le> 0"
using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
- by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
+ by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally have ?thesis using dc c d nc nd dc'
by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstle_def
Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
@@ -3202,7 +3202,7 @@
by simp
also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - 2 * ?c * ?d * ?r \<le> 0"
using nonzero_mult_divide_cancel_left[of "2 * ?c * ?d"] c d
- by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
+ by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally have ?thesis using dc c d nc nd
by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstle_def
Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
@@ -3219,14 +3219,14 @@
have "?rhs \<longleftrightarrow> Ifm vs (- ?t / (2 * ?c) # bs) (Le (CNP 0 a r))"
by (simp only: th)
also have "\<dots> \<longleftrightarrow> ?a * (- ?t / (2 * ?c))+ ?r \<le> 0"
- by (simp add: field_simps r[of "- (?t / (2 * ?c))"])
+ by (simp add: r[of "- (?t / (2 * ?c))"])
also have "\<dots> \<longleftrightarrow> 2 * ?c * (?a * (- ?t / (2 * ?c))+ ?r) \<le> 0"
using c mult_le_cancel_left[of "2 * ?c" "?a* (- ?t / (2*?c))+ ?r" 0] c' c''
order_less_not_sym[OF c'']
by simp
also have "\<dots> \<longleftrightarrow> - ?a*?t+ 2*?c *?r \<le> 0"
using nonzero_mult_divide_cancel_left[OF c'] c
- by (simp add: divide_minus_left algebra_simps diff_divide_distrib less_le del: distrib_right)
+ by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
finally have ?thesis using c d nc nd
by (simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def
evaldjf_ex field_simps lt polyneg_norm polymul_norm)
@@ -3243,7 +3243,7 @@
have "?rhs \<longleftrightarrow> Ifm vs (- ?t / (2 * ?c) # bs) (Le (CNP 0 a r))"
by (simp only: th)
also have "\<dots> \<longleftrightarrow> ?a * (- ?t / (2*?c))+ ?r \<le> 0"
- by (simp add: field_simps r[of "- (?t / (2*?c))"])
+ by (simp add: r[of "- (?t / (2*?c))"])
also have "\<dots> \<longleftrightarrow> 2 * ?c * (?a * (- ?t / (2 * ?c))+ ?r) \<ge> 0"
using c order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
mult_le_cancel_left[of "2 * ?c" 0 "?a* (- ?t / (2*?c))+ ?r"]
@@ -3251,7 +3251,7 @@
also have "\<dots> \<longleftrightarrow> ?a * ?t - 2 * ?c * ?r \<le> 0"
using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c'']
less_imp_neq[OF c''] c''
- by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
+ by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally have ?thesis using c d nc nd
by (simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def
evaldjf_ex field_simps lt polyneg_norm polymul_norm)
@@ -3268,14 +3268,14 @@
have "?rhs \<longleftrightarrow> Ifm vs (- ?s / (2 * ?d) # bs) (Le (CNP 0 a r))"
by (simp only: th)
also have "\<dots> \<longleftrightarrow> ?a * (- ?s / (2 * ?d))+ ?r \<le> 0"
- by (simp add: field_simps r[of "- (?s / (2*?d))"])
+ by (simp add: r[of "- (?s / (2*?d))"])
also have "\<dots> \<longleftrightarrow> 2 * ?d * (?a * (- ?s / (2 * ?d)) + ?r) \<le> 0"
using d mult_le_cancel_left[of "2 * ?d" "?a* (- ?s / (2*?d))+ ?r" 0] d' d''
order_less_not_sym[OF d'']
by simp
also have "\<dots> \<longleftrightarrow> - ?a * ?s + 2 * ?d * ?r \<le> 0"
using nonzero_mult_divide_cancel_left[OF d'] d
- by (simp add: divide_minus_left algebra_simps diff_divide_distrib less_le del: distrib_right)
+ by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
finally have ?thesis using c d nc nd
by (simp add: r[of "- (?s / (2*?d))"] msubstle_def Let_def
evaldjf_ex field_simps lt polyneg_norm polymul_norm)
@@ -3292,7 +3292,7 @@
have "?rhs \<longleftrightarrow> Ifm vs (- ?s / (2*?d) # bs) (Le (CNP 0 a r))"
by (simp only: th)
also have "\<dots> \<longleftrightarrow> ?a* (- ?s / (2*?d))+ ?r \<le> 0"
- by (simp add: field_simps r[of "- (?s / (2*?d))"])
+ by (simp add: r[of "- (?s / (2*?d))"])
also have "\<dots> \<longleftrightarrow> 2*?d * (?a* (- ?s / (2*?d))+ ?r) \<ge> 0"
using d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
mult_le_cancel_left[of "2 * ?d" 0 "?a* (- ?s / (2*?d))+ ?r"]
@@ -3300,7 +3300,7 @@
also have "\<dots> \<longleftrightarrow> ?a * ?s - 2 * ?d * ?r \<le> 0"
using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d'']
less_imp_neq[OF d''] d''
- by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
+ by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
finally have ?thesis using c d nc nd
by (simp add: r[of "- (?s / (2*?d))"] msubstle_def Let_def
evaldjf_ex field_simps lt polyneg_norm polymul_norm)
@@ -3326,10 +3326,10 @@
Ifm vs (((- Itm vs (x#bs) t / Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) /2)#bs) p"
using lp
by (induct p rule: islin.induct)
- (auto simp add: tmbound0_I
+ (auto simp add: tmbound0_I
[where b = "(- (Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup>) - (Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>)) / 2"
and b' = x and bs = bs and vs = vs]
- msubsteq msubstneq msubstlt [OF nc nd] msubstle [OF nc nd] divide_minus_left)
+ msubsteq msubstneq msubstlt [OF nc nd] msubstle [OF nc nd])
lemma msubst_nb:
assumes lp: "islin p"
@@ -3767,7 +3767,7 @@
by (auto simp add: msubst2_def lt zero_less_mult_iff mult_less_0_iff)
from msubst2[OF lp nn nn2(1), of x bs t]
have "\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> Ifm vs (- Itm vs (x # bs) t / (\<lparr>n\<rparr>\<^sub>p\<^bsup>vs\<^esup> * 2) # bs) p"
- using H(2) nn2 by (simp add: divide_minus_left divide_minus_right mult_minus2_right)
+ using H(2) nn2 by (simp add: mult_minus2_right)
}
moreover
{
@@ -3780,7 +3780,7 @@
then have nn: "isnpoly (n *\<^sub>p (C (-2,1)))" "\<lparr>n *\<^sub>p(C (-2,1)) \<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0"
using H(2) by (simp_all add: polymul_norm n2)
from msubst2[OF lp nn, of x bs t] have "?I (msubst2 p (n *\<^sub>p (C (-2,1))) t)"
- using H(2,3) by (simp add: divide_minus_left divide_minus_right mult_minus2_right)
+ using H(2,3) by (simp add: mult_minus2_right)
}
ultimately show ?thesis by blast
qed
@@ -3811,7 +3811,7 @@
from msubst2[OF lp nn nn'(1), of x bs ] H(3) nn'
have "\<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and>
Ifm vs ((- Itm vs (x # bs) t / \<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> + - Itm vs (x # bs) s / \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>) / 2 # bs) p"
- by (simp add: divide_minus_left divide_minus_right add_divide_distrib diff_divide_distrib mult_minus2_left mult_commute)
+ by (simp add: add_divide_distrib diff_divide_distrib mult_minus2_left mult_commute)
}
moreover
{
@@ -3828,7 +3828,7 @@
using H(3,4) by (simp_all add: polymul_norm n2)
from msubst2[OF lp nn, of x bs ] H(3,4,5)
have "Ifm vs (x#bs) (msubst2 p (C (-2, 1) *\<^sub>p c*\<^sub>p d) (Add (Mul d t) (Mul c s)))"
- by (simp add: divide_minus_left divide_minus_right diff_divide_distrib add_divide_distrib mult_minus2_left mult_commute)
+ by (simp add: diff_divide_distrib add_divide_distrib mult_minus2_left mult_commute)
}
ultimately show ?thesis by blast
qed
--- a/src/HOL/Decision_Procs/Rat_Pair.thy Tue Apr 08 23:16:00 2014 +0200
+++ b/src/HOL/Decision_Procs/Rat_Pair.thy Wed Apr 09 09:37:47 2014 +0200
@@ -227,7 +227,7 @@
let ?g = "gcd a b"
from a b have g: "?g \<noteq> 0"by simp
from of_int_div[OF g, where ?'a = 'a]
- have ?thesis by (auto simp: divide_minus_left divide_minus_right x INum_def normNum_def split_def Let_def) }
+ have ?thesis by (auto simp add: x INum_def normNum_def split_def Let_def) }
ultimately show ?thesis by blast
qed
@@ -300,13 +300,13 @@
qed
lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x ::'a:: field)"
- by (simp add: divide_minus_left Nneg_def split_def INum_def)
+ by (simp add: Nneg_def split_def INum_def)
lemma Nsub[simp]: "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {field_char_0, field_inverse_zero})"
by (simp add: Nsub_def split_def)
lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: field_inverse_zero) / (INum x)"
- by (simp add: divide_minus_left divide_minus_right Ninv_def INum_def split_def)
+ by (simp add: Ninv_def INum_def split_def)
lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0, field_inverse_zero})"
by (simp add: Ndiv_def)
--- a/src/HOL/Deriv.thy Tue Apr 08 23:16:00 2014 +0200
+++ b/src/HOL/Deriv.thy Wed Apr 09 09:37:47 2014 +0200
@@ -825,7 +825,7 @@
lemma DERIV_mirror:
"(DERIV f (- x) :> y) \<longleftrightarrow> (DERIV (\<lambda>x. f (- x::real) :: real) x :> - y)"
- by (simp add: DERIV_def filterlim_at_split filterlim_at_left_to_right divide_minus_right
+ by (simp add: DERIV_def filterlim_at_split filterlim_at_left_to_right
tendsto_minus_cancel_left field_simps conj_commute)
text {* Caratheodory formulation of derivative at a point *}
@@ -908,8 +908,8 @@
fix h::real
assume "0 < h" "h < s"
with all [of "-h"] show "f x < f (x-h)"
- proof (simp add: abs_if pos_less_divide_eq divide_minus_right split add: split_if_asm)
- assume "- ((f (x-h) - f x) / h) < l" and h: "0 < h"
+ proof (simp add: abs_if pos_less_divide_eq split add: split_if_asm)
+ assume " - ((f (x-h) - f x) / h) < l" and h: "0 < h"
with l
have "0 < (f (x-h) - f x) / h" by arith
thus "f x < f (x-h)"
@@ -1628,8 +1628,7 @@
((\<lambda> x. (f' x / g' x)) ---> y) (at_left x) \<Longrightarrow>
((\<lambda> x. f x / g x) ---> y) (at_left x)"
unfolding eventually_at_left_to_right filterlim_at_left_to_right DERIV_mirror
- by (rule lhopital_right[where f'="\<lambda>x. - f' (- x)"])
- (auto simp: DERIV_mirror divide_minus_left divide_minus_right)
+ by (rule lhopital_right[where f'="\<lambda>x. - f' (- x)"]) (auto simp: DERIV_mirror)
lemma lhopital:
"((f::real \<Rightarrow> real) ---> 0) (at x) \<Longrightarrow> (g ---> 0) (at x) \<Longrightarrow>
@@ -1740,8 +1739,7 @@
((\<lambda> x. (f' x / g' x)) ---> y) (at_left x) \<Longrightarrow>
((\<lambda> x. f x / g x) ---> y) (at_left x)"
unfolding eventually_at_left_to_right filterlim_at_left_to_right DERIV_mirror
- by (rule lhopital_right_at_top[where f'="\<lambda>x. - f' (- x)"])
- (auto simp: divide_minus_left divide_minus_right DERIV_mirror)
+ by (rule lhopital_right_at_top[where f'="\<lambda>x. - f' (- x)"]) (auto simp: DERIV_mirror)
lemma lhopital_at_top:
"LIM x at x. (g::real \<Rightarrow> real) x :> at_top \<Longrightarrow>
@@ -1798,7 +1796,7 @@
unfolding filterlim_at_right_to_top
apply (intro filterlim_cong[THEN iffD2, OF refl refl _ lim])
using eventually_ge_at_top[where c="1::real"]
- by eventually_elim (simp add: divide_minus_left divide_minus_right)
+ by eventually_elim simp
qed
end
--- a/src/HOL/Fields.thy Tue Apr 08 23:16:00 2014 +0200
+++ b/src/HOL/Fields.thy Wed Apr 09 09:37:47 2014 +0200
@@ -152,11 +152,11 @@
lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"
by (simp add: divide_inverse nonzero_inverse_minus_eq)
-lemma divide_minus_left [field_simps]: "(-a) / b = - (a / b)"
+lemma divide_minus_left [simp]: "(-a) / b = - (a / b)"
by (simp add: divide_inverse)
lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
- using add_divide_distrib [of a "- b" c] by (simp add: divide_inverse)
+ using add_divide_distrib [of a "- b" c] by simp
lemma nonzero_eq_divide_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"
proof -
@@ -416,11 +416,11 @@
"- (a / b) = a / - b"
by (simp add: divide_inverse)
-lemma divide_minus_right [field_simps]:
+lemma divide_minus_right [simp]:
"a / - b = - (a / b)"
by (simp add: divide_inverse)
-lemma minus_divide_divide [simp]:
+lemma minus_divide_divide:
"(- a) / (- b) = a / b"
apply (cases "b=0", simp)
apply (simp add: nonzero_minus_divide_divide)
@@ -1053,13 +1053,13 @@
lemma divide_right_mono_neg: "a <= b
==> c <= 0 ==> b / c <= a / c"
apply (drule divide_right_mono [of _ _ "- c"])
-apply (auto simp: divide_minus_right)
+apply auto
done
lemma divide_left_mono_neg: "a <= b
==> c <= 0 ==> 0 < a * b ==> c / a <= c / b"
apply (drule divide_left_mono [of _ _ "- c"])
- apply (auto simp add: divide_minus_left mult_commute)
+ apply (auto simp add: mult_commute)
done
lemma inverse_le_iff:
--- a/src/HOL/Library/Convex.thy Tue Apr 08 23:16:00 2014 +0200
+++ b/src/HOL/Library/Convex.thy Wed Apr 09 09:37:47 2014 +0200
@@ -656,7 +656,7 @@
proof -
have "\<And>z. z > 0 \<Longrightarrow> DERIV (log b) z :> 1 / (ln b * z)" using DERIV_log by auto
then have f': "\<And>z. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - log b z) z :> - 1 / (ln b * z)"
- by (auto simp: divide_minus_left DERIV_minus)
+ by (auto simp: DERIV_minus)
have "\<And>z :: real. z > 0 \<Longrightarrow> DERIV inverse z :> - (inverse z ^ Suc (Suc 0))"
using less_imp_neq[THEN not_sym, THEN DERIV_inverse] by auto
from this[THEN DERIV_cmult, of _ "- 1 / ln b"]
@@ -664,7 +664,7 @@
DERIV (\<lambda> z. (- 1 / ln b) * inverse z) z :> (- 1 / ln b) * (- (inverse z ^ Suc (Suc 0)))"
by auto
then have f''0: "\<And>z :: real. z > 0 \<Longrightarrow> DERIV (\<lambda> z. - 1 / (ln b * z)) z :> 1 / (ln b * z * z)"
- by (auto simp add: inverse_eq_divide divide_minus_left mult_assoc)
+ unfolding inverse_eq_divide by (auto simp add: mult_assoc)
have f''_ge0: "\<And>z :: real. z > 0 \<Longrightarrow> 1 / (ln b * z * z) \<ge> 0"
using `b > 1` by (auto intro!:less_imp_le simp add: divide_pos_pos[of 1] mult_pos_pos)
from f''_ge0_imp_convex[OF pos_is_convex,
--- a/src/HOL/Library/Float.thy Tue Apr 08 23:16:00 2014 +0200
+++ b/src/HOL/Library/Float.thy Wed Apr 09 09:37:47 2014 +0200
@@ -637,7 +637,7 @@
qed
thus ?thesis using `\<not> b dvd a` by simp
qed (simp add: ceiling_def real_of_int_minus[symmetric] divide_minus_left[symmetric]
- floor_divide_eq_div dvd_neg_div del: real_of_int_minus)
+ floor_divide_eq_div dvd_neg_div del: divide_minus_left real_of_int_minus)
lemma compute_float_up[code]:
"float_up p (Float m e) =
@@ -1004,7 +1004,7 @@
else (if 0 < y
then - (rapprox_posrat prec (nat (-x)) (nat y))
else lapprox_posrat prec (nat (-x)) (nat (-y))))"
- by transfer (auto simp: round_up_def divide_minus_left divide_minus_right round_down_def ceiling_def ac_simps)
+ by transfer (auto simp: round_up_def round_down_def ceiling_def ac_simps)
hide_fact (open) compute_lapprox_rat
lift_definition rapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" is
@@ -1019,7 +1019,7 @@
else (if 0 < y
then - (lapprox_posrat prec (nat (-x)) (nat y))
else rapprox_posrat prec (nat (-x)) (nat (-y))))"
- by transfer (auto simp: round_up_def round_down_def divide_minus_left divide_minus_right ceiling_def ac_simps)
+ by transfer (auto simp: round_up_def round_down_def ceiling_def ac_simps)
hide_fact (open) compute_rapprox_rat
subsection {* Division *}
--- a/src/HOL/Library/Formal_Power_Series.thy Tue Apr 08 23:16:00 2014 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Wed Apr 09 09:37:47 2014 +0200
@@ -3635,7 +3635,7 @@
done
lemma fps_sin_even: "fps_sin (- c) = - fps_sin c"
- by (auto simp add: divide_minus_left fps_eq_iff fps_sin_def)
+ by (auto simp add: fps_eq_iff fps_sin_def)
lemma fps_cos_odd: "fps_cos (- c) = fps_cos c"
by (auto simp add: fps_eq_iff fps_cos_def)
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Tue Apr 08 23:16:00 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Wed Apr 09 09:37:47 2014 +0200
@@ -998,7 +998,7 @@
f (Suc n) u * (z-u) ^ n / of_nat (fact n) +
f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n) / of_nat (fact (Suc n)) -
f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n) / of_nat (fact (Suc n))"
- using Suc by (simp add: divide_minus_left)
+ using Suc by simp
also have "... = f (Suc (Suc n)) u * (z-u) ^ Suc n / of_nat (fact (Suc n))"
proof -
have "of_nat(fact(Suc n)) *
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Apr 08 23:16:00 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed Apr 09 09:37:47 2014 +0200
@@ -2277,7 +2277,9 @@
using Min_ge_iff[of i 0 ] and obt(1)
unfolding t_def i_def
using obt(4)[unfolded le_less]
- apply (auto simp: divide_le_0_iff divide_minus_right)
+ apply auto
+ unfolding divide_le_0_iff
+ apply auto
done
have t: "\<forall>v\<in>s. u v + t * w v \<ge> 0"
proof
@@ -2314,7 +2316,7 @@
obtain a where "a \<in> s" and "t = (\<lambda>v. (u v) / (- w v)) a" and "w a < 0"
using Min_in[OF _ `i\<noteq>{}`] and obt(1) unfolding i_def t_def by auto
- then have a: "a \<in> s" "u a + t * w a = 0" by (auto simp: divide_minus_right)
+ then have a: "a \<in> s" "u a + t * w a = 0" by auto
have *: "\<And>f. setsum f (s - {a}) = setsum f s - ((f a)::'b::ab_group_add)"
unfolding setsum_diff1'[OF obt(1) `a\<in>s`] by auto
have "(\<Sum>v\<in>s. u v + t * w v) = 1"
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Tue Apr 08 23:16:00 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Apr 09 09:37:47 2014 +0200
@@ -1149,7 +1149,7 @@
setsum (\<lambda>v. (- (inverse (u ?a))) *\<^sub>R (u v *\<^sub>R v)) S - ?u v *\<^sub>R v"
using fS vS uv by (simp add: setsum_diff1 divide_inverse field_simps)
also have "\<dots> = ?a"
- unfolding scaleR_right.setsum [symmetric] u using uv by (simp add: divide_minus_left)
+ unfolding scaleR_right.setsum [symmetric] u using uv by simp
finally have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S = ?a" .
with th0 have ?lhs
unfolding dependent_def span_explicit
@@ -2143,7 +2143,7 @@
case False
with span_mul[OF th, of "- 1/ k"]
have th1: "f a \<in> span (f ` b)"
- by (auto simp: divide_minus_left)
+ by auto
from inj_on_image_set_diff[OF "2.prems"(3), of "insert a b " "{a}", symmetric]
have tha: "f ` insert a b - f ` {a} = f ` (insert a b - {a})" by blast
from "2.prems"(2) [unfolded dependent_def bex_simps(8), rule_format, of "f a"]
--- a/src/HOL/NSA/HDeriv.thy Tue Apr 08 23:16:00 2014 +0200
+++ b/src/HOL/NSA/HDeriv.thy Wed Apr 09 09:37:47 2014 +0200
@@ -359,7 +359,7 @@
have "inverse (- (h * star_of x) + - (star_of x * star_of x)) =
(inverse (star_of x + h) - inverse (star_of x)) / h"
apply (simp add: division_ring_inverse_diff nonzero_inverse_mult_distrib [symmetric]
- nonzero_inverse_minus_eq [symmetric] ac_simps ring_distribs divide_minus_left)
+ nonzero_inverse_minus_eq [symmetric] ac_simps ring_distribs)
apply (subst nonzero_inverse_minus_eq [symmetric])
using distrib_right [symmetric, of h "star_of x" "star_of x"] apply simp
apply (simp add: field_simps)
--- a/src/HOL/Probability/Information.thy Tue Apr 08 23:16:00 2014 +0200
+++ b/src/HOL/Probability/Information.thy Wed Apr 09 09:37:47 2014 +0200
@@ -945,7 +945,7 @@
show "- (\<integral> x. indicator A x / measure MX A * log b (indicator A x / measure MX A) \<partial>MX) =
log b (measure MX A)"
unfolding eq using uniform_distributed_params[OF X]
- by (subst lebesgue_integral_cmult) (auto simp: divide_minus_left measure_def)
+ by (subst lebesgue_integral_cmult) (auto simp: measure_def)
qed
lemma (in information_space) entropy_simple_distributed:
--- a/src/HOL/Probability/Radon_Nikodym.thy Tue Apr 08 23:16:00 2014 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy Wed Apr 09 09:37:47 2014 +0200
@@ -241,7 +241,7 @@
by (auto simp: finite_measure_restricted N.finite_measure_restricted sets_eq)
from finite_measure.Radon_Nikodym_aux_epsilon[OF this] guess X .. note X = this
with S have "?P (S \<inter> X) S n"
- by (simp add: divide_minus_left measure_restricted sets_eq sets.Int) (metis inf_absorb2)
+ by (simp add: measure_restricted sets_eq sets.Int) (metis inf_absorb2)
hence "\<exists>A. ?P A S n" .. }
note Ex_P = this
def A \<equiv> "rec_nat (space M) (\<lambda>n A. SOME B. ?P B A n)"
@@ -280,7 +280,7 @@
hence "0 < - ?d B" by auto
from ex_inverse_of_nat_Suc_less[OF this]
obtain n where *: "?d B < - 1 / real (Suc n)"
- by (auto simp: divide_minus_left real_eq_of_nat inverse_eq_divide field_simps)
+ by (auto simp: real_eq_of_nat inverse_eq_divide field_simps)
have "B \<subseteq> A (Suc n)" using B by (auto simp del: nat.rec(2))
from epsilon[OF B(1) this] *
show False by auto
--- a/src/HOL/Rat.thy Tue Apr 08 23:16:00 2014 +0200
+++ b/src/HOL/Rat.thy Wed Apr 09 09:37:47 2014 +0200
@@ -665,7 +665,7 @@
by transfer (simp add: add_frac_eq)
lemma of_rat_minus: "of_rat (- a) = - of_rat a"
- by transfer (simp add: divide_minus_left)
+ by transfer simp
lemma of_rat_neg_one [simp]:
"of_rat (- 1) = - 1"
--- a/src/HOL/Real_Vector_Spaces.thy Tue Apr 08 23:16:00 2014 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Wed Apr 09 09:37:47 2014 +0200
@@ -1116,10 +1116,10 @@
by (simp add: sgn_div_norm divide_inverse)
lemma real_sgn_pos: "0 < (x::real) \<Longrightarrow> sgn x = 1"
- by (rule sgn_pos)
+unfolding real_sgn_eq by simp
lemma real_sgn_neg: "(x::real) < 0 \<Longrightarrow> sgn x = -1"
- by (rule sgn_neg)
+unfolding real_sgn_eq by simp
lemma norm_conv_dist: "norm x = dist x 0"
unfolding dist_norm by simp
--- a/src/HOL/Transcendental.thy Tue Apr 08 23:16:00 2014 +0200
+++ b/src/HOL/Transcendental.thy Wed Apr 09 09:37:47 2014 +0200
@@ -2145,7 +2145,7 @@
lemma cos_coeff_Suc: "cos_coeff (Suc n) = - sin_coeff n / real (Suc n)"
unfolding cos_coeff_def sin_coeff_def
- by (simp del: mult_Suc, auto simp add: divide_minus_left odd_Suc_mult_two_ex)
+ by (simp del: mult_Suc, auto simp add: odd_Suc_mult_two_ex)
lemma summable_sin: "summable (\<lambda>n. sin_coeff n * x ^ n)"
unfolding sin_coeff_def
@@ -2169,7 +2169,7 @@
by (simp add: diffs_def sin_coeff_Suc real_of_nat_def del: of_nat_Suc)
lemma diffs_cos_coeff: "diffs cos_coeff = (\<lambda>n. - sin_coeff n)"
- by (simp add: divide_minus_left diffs_def cos_coeff_Suc real_of_nat_def del: of_nat_Suc)
+ by (simp add: diffs_def cos_coeff_Suc real_of_nat_def del: of_nat_Suc)
text{*Now at last we can get the derivatives of exp, sin and cos*}
@@ -3239,7 +3239,7 @@
assume "x \<in> {-1..1}"
then show "x \<in> sin ` {- pi / 2..pi / 2}"
using arcsin_lbound arcsin_ubound
- by (intro image_eqI[where x="arcsin x"]) (auto simp: divide_minus_left)
+ by (intro image_eqI[where x="arcsin x"]) auto
qed simp
finally show ?thesis .
qed
@@ -3338,14 +3338,12 @@
lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- pi/2))"
by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
- (auto simp: le_less eventually_at dist_real_def divide_minus_left
- simp del: less_divide_eq_numeral1
+ (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
intro!: tan_monotone exI[of _ "pi/2"])
lemma filterlim_tan_at_left: "filterlim tan at_top (at_left (pi/2))"
by (rule filterlim_at_top_at_left[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
- (auto simp: le_less eventually_at dist_real_def divide_minus_left
- simp del: less_divide_eq_numeral1
+ (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
intro!: tan_monotone exI[of _ "pi/2"])
lemma tendsto_arctan_at_top: "(arctan ---> (pi/2)) at_top"
@@ -3967,7 +3965,7 @@
show "tan (sgn x * pi / 2 - arctan x) = 1 / x"
unfolding tan_inverse [of "arctan x", unfolded tan_arctan]
unfolding sgn_real_def
- by (simp add: divide_minus_left tan_def cos_arctan sin_arctan sin_diff cos_diff)
+ by (simp add: tan_def cos_arctan sin_arctan sin_diff cos_diff)
qed
theorem pi_series: "pi / 4 = (\<Sum> k. (-1)^k * 1 / real (k*2+1))" (is "_ = ?SUM")