author paulson Fri Apr 04 17:58:25 2014 +0100 (2014-04-04) changeset 56410 a14831ac3023 parent 56409 36489d77c484 child 56411 913dc982ef55
divide_minus_left divide_minus_right are in field_simps but are not default simprules
 src/HOL/Decision_Procs/Approximation.thy file | annotate | diff | revisions src/HOL/Decision_Procs/Ferrack.thy file | annotate | diff | revisions src/HOL/Decision_Procs/MIR.thy file | annotate | diff | revisions src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy file | annotate | diff | revisions src/HOL/Decision_Procs/Rat_Pair.thy file | annotate | diff | revisions src/HOL/Fields.thy file | annotate | diff | revisions src/HOL/Library/Float.thy file | annotate | diff | revisions src/HOL/Library/Formal_Power_Series.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Thu Apr 03 23:51:52 2014 +0100
1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Fri Apr 04 17:58:25 2014 +0100
1.3 @@ -1466,7 +1466,8 @@
1.4          using float_divr_nonpos_pos_upper_bound[OF `real x \<le> 0` `0 < real (- floor_fl x)`]
1.5          unfolding less_eq_float_def zero_float.rep_eq .
1.6
1.7 -      have "exp x = exp (?num * (x / ?num))" using `real ?num \<noteq> 0` by auto
1.8 +      have "exp x = exp (?num * (x / ?num))" using `real ?num \<noteq> 0`
1.9 +        by (auto simp: divide_minus_left divide_minus_right)
1.10        also have "\<dots> = exp (x / ?num) ^ ?num" unfolding exp_real_of_nat_mult ..
1.11        also have "\<dots> \<le> exp (float_divr prec x (- floor_fl x)) ^ ?num" unfolding num_eq fl_eq
1.12          by (rule power_mono, rule exp_le_cancel_iff[THEN iffD2], rule float_divr) auto
1.13 @@ -1486,15 +1487,16 @@
1.14          case False hence "0 \<le> real ?horner" by auto
1.15
1.16          have div_less_zero: "real (float_divl prec x (- floor_fl x)) \<le> 0"
1.17 -          using `real (floor_fl x) < 0` `real x \<le> 0` by (auto intro!: order_trans[OF float_divl] divide_nonpos_neg)
1.18 -
1.19 +          using `real (floor_fl x) < 0` `real x \<le> 0`
1.20 +            by (auto simp: field_simps intro!: order_trans[OF float_divl])
1.21          have "(?lb_exp_horner (float_divl prec x (- floor_fl x))) ^ ?num \<le>
1.22            exp (float_divl prec x (- floor_fl x)) ^ ?num"
1.23            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)
1.24          also have "\<dots> \<le> exp (x / ?num) ^ ?num" unfolding num_eq fl_eq
1.25            using float_divl by (auto intro!: power_mono simp del: uminus_float.rep_eq)
1.26          also have "\<dots> = exp (?num * (x / ?num))" unfolding exp_real_of_nat_mult ..
1.27 -        also have "\<dots> = exp x" using `real ?num \<noteq> 0` by auto
1.28 +        also have "\<dots> = exp x" using `real ?num \<noteq> 0`
1.29 +          by (auto simp: field_simps)
1.30          finally show ?thesis
1.31            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
1.32        next
1.33 @@ -1506,7 +1508,8 @@
1.34          have "Float 1 -2 \<le> exp (x / (- floor_fl x))" unfolding Float_num .
1.35          hence "real (Float 1 -2) ^ ?num \<le> exp (x / (- floor_fl x)) ^ ?num"
1.36            by (auto intro!: power_mono)
1.37 -        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
1.38 +        also have "\<dots> = exp x" unfolding num_eq fl_eq exp_real_of_nat_mult[symmetric]
1.39 +          using `real (floor_fl x) \<noteq> 0` by (auto simp: field_simps)
1.40          finally show ?thesis
1.41            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 .
1.42        qed
```
```     2.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Thu Apr 03 23:51:52 2014 +0100
2.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Fri Apr 04 17:58:25 2014 +0100
2.3 @@ -1167,7 +1167,7 @@
2.4    {fix x
2.5      assume xz: "x > ?z"
2.6      with mult_strict_right_mono [OF xz cp] cp
2.7 -    have "(real c * x > - ?e)" by (simp add: mult_ac)
2.8 +    have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
2.9      hence "real c * x + ?e > 0" by arith
2.10      hence "real c * x + ?e \<noteq> 0" by simp
2.11      with xz have "?P ?z x (Eq (CN 0 c e))"
2.12 @@ -1184,7 +1184,7 @@
2.13    {fix x
2.14      assume xz: "x > ?z"
2.15      with mult_strict_right_mono [OF xz cp] cp
2.16 -    have "(real c * x > - ?e)" by (simp add: mult_ac)
2.17 +    have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
2.18      hence "real c * x + ?e > 0" by arith
2.19      hence "real c * x + ?e \<noteq> 0" by simp
2.20      with xz have "?P ?z x (NEq (CN 0 c e))"
2.21 @@ -1201,7 +1201,7 @@
2.22    {fix x
2.23      assume xz: "x > ?z"
2.24      with mult_strict_right_mono [OF xz cp] cp
2.25 -    have "(real c * x > - ?e)" by (simp add: mult_ac)
2.26 +    have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
2.27      hence "real c * x + ?e > 0" by arith
2.28      with xz have "?P ?z x (Lt (CN 0 c e))"
2.29        using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
2.30 @@ -1217,7 +1217,7 @@
2.31    {fix x
2.32      assume xz: "x > ?z"
2.33      with mult_strict_right_mono [OF xz cp] cp
2.34 -    have "(real c * x > - ?e)" by (simp add: mult_ac)
2.35 +    have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
2.36      hence "real c * x + ?e > 0" by arith
2.37      with xz have "?P ?z x (Le (CN 0 c e))"
2.38        using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
2.39 @@ -1233,7 +1233,7 @@
2.40    {fix x
2.41      assume xz: "x > ?z"
2.42      with mult_strict_right_mono [OF xz cp] cp
2.43 -    have "(real c * x > - ?e)" by (simp add: mult_ac)
2.44 +    have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
2.45      hence "real c * x + ?e > 0" by arith
2.46      with xz have "?P ?z x (Gt (CN 0 c e))"
2.47        using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
2.48 @@ -1249,7 +1249,7 @@
2.49    {fix x
2.50      assume xz: "x > ?z"
2.51      with mult_strict_right_mono [OF xz cp] cp
2.52 -    have "(real c * x > - ?e)" by (simp add: mult_ac)
2.53 +    have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
2.54      hence "real c * x + ?e > 0" by arith
2.55      with xz have "?P ?z x (Ge (CN 0 c e))"
2.56        using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"]   by simp }
```
```     3.1 --- a/src/HOL/Decision_Procs/MIR.thy	Thu Apr 03 23:51:52 2014 +0100
3.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Fri Apr 04 17:58:25 2014 +0100
3.3 @@ -2068,7 +2068,7 @@
3.4    from 3 have nbe: "numbound0 e" by simp
3.5    fix y
3.6    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))"
3.7 -  proof (simp add: less_floor_eq , rule allI, rule impI)
3.8 +  proof (simp add: divide_minus_left less_floor_eq , rule allI, rule impI)
3.9      fix x :: int
3.10      assume A: "real x + 1 \<le> - (Inum (y # bs) e / real c)"
3.11      hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
3.12 @@ -2085,7 +2085,7 @@
3.13    from 4 have nbe: "numbound0 e" by simp
3.14    fix y
3.15    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))"
3.16 -  proof (simp add: less_floor_eq , rule allI, rule impI)
3.17 +  proof (simp add: divide_minus_left less_floor_eq , rule allI, rule impI)
3.18      fix x :: int
3.19      assume A: "real x + 1 \<le> - (Inum (y # bs) e / real c)"
3.20      hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
3.21 @@ -2102,7 +2102,7 @@
3.22    from 5 have nbe: "numbound0 e" by simp
3.23    fix y
3.24    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))"
3.25 -  proof (simp add: less_floor_eq , rule allI, rule impI)
3.26 +  proof (simp add: divide_minus_left less_floor_eq , rule allI, rule impI)
3.27      fix x :: int
3.28      assume A: "real x + 1 \<le> - (Inum (y # bs) e / real c)"
3.29      hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
3.30 @@ -2118,7 +2118,7 @@
3.31    from 6 have nbe: "numbound0 e" by simp
3.32    fix y
3.33    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))"
3.34 -  proof (simp add: less_floor_eq , rule allI, rule impI)
3.35 +  proof (simp add: divide_minus_left less_floor_eq , rule allI, rule impI)
3.36      fix x :: int
3.37      assume A: "real x + 1 \<le> - (Inum (y # bs) e / real c)"
3.38      hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
3.39 @@ -2134,7 +2134,7 @@
3.40    from 7 have nbe: "numbound0 e" by simp
3.41    fix y
3.42    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))"
3.43 -  proof (simp add: less_floor_eq , rule allI, rule impI)
3.44 +  proof (simp add: divide_minus_left less_floor_eq , rule allI, rule impI)
3.45      fix x :: int
3.46      assume A: "real x + 1 \<le> - (Inum (y # bs) e / real c)"
3.47      hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
3.48 @@ -2150,7 +2150,7 @@
3.49    from 8 have nbe: "numbound0 e" by simp
3.50    fix y
3.51    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))"
3.52 -  proof (simp add: less_floor_eq , rule allI, rule impI)
3.53 +  proof (simp add: divide_minus_left less_floor_eq , rule allI, rule impI)
3.54      fix x :: int
3.55      assume A: "real x + 1 \<le> - (Inum (y # bs) e / real c)"
3.56      hence th1:"real x < - (Inum (y # bs) e / real c)" by simp
3.57 @@ -4267,7 +4267,7 @@
3.58    {fix x
3.59      assume xz: "x > ?z"
3.60      with mult_strict_right_mono [OF xz cp] cp
3.61 -    have "(real c * x > - ?e)" by (simp add: mult_ac)
3.62 +    have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
3.63      hence "real c * x + ?e > 0" by arith
3.64      hence "real c * x + ?e \<noteq> 0" by simp
3.65      with xz have "?P ?z x (Eq (CN 0 c e))"
3.66 @@ -4284,7 +4284,7 @@
3.67    {fix x
3.68      assume xz: "x > ?z"
3.69      with mult_strict_right_mono [OF xz cp] cp
3.70 -    have "(real c * x > - ?e)" by (simp add: mult_ac)
3.71 +    have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
3.72      hence "real c * x + ?e > 0" by arith
3.73      hence "real c * x + ?e \<noteq> 0" by simp
3.74      with xz have "?P ?z x (NEq (CN 0 c e))"
3.75 @@ -4301,7 +4301,7 @@
3.76    {fix x
3.77      assume xz: "x > ?z"
3.78      with mult_strict_right_mono [OF xz cp] cp
3.79 -    have "(real c * x > - ?e)" by (simp add: mult_ac)
3.80 +    have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
3.81      hence "real c * x + ?e > 0" by arith
3.82      with xz have "?P ?z x (Lt (CN 0 c e))"
3.83        using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
3.84 @@ -4317,7 +4317,7 @@
3.85    {fix x
3.86      assume xz: "x > ?z"
3.87      with mult_strict_right_mono [OF xz cp] cp
3.88 -    have "(real c * x > - ?e)" by (simp add: mult_ac)
3.89 +    have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
3.90      hence "real c * x + ?e > 0" by arith
3.91      with xz have "?P ?z x (Le (CN 0 c e))"
3.92        using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
3.93 @@ -4333,7 +4333,7 @@
3.94    {fix x
3.95      assume xz: "x > ?z"
3.96      with mult_strict_right_mono [OF xz cp] cp
3.97 -    have "(real c * x > - ?e)" by (simp add: mult_ac)
3.98 +    have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
3.99      hence "real c * x + ?e > 0" by arith
3.100      with xz have "?P ?z x (Gt (CN 0 c e))"
3.101        using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
3.102 @@ -4349,7 +4349,7 @@
3.103    {fix x
3.104      assume xz: "x > ?z"
3.105      with mult_strict_right_mono [OF xz cp] cp
3.106 -    have "(real c * x > - ?e)" by (simp add: mult_ac)
3.107 +    have "(real c * x > - ?e)" by (simp add: divide_minus_left mult_ac)
3.108      hence "real c * x + ?e > 0" by arith
3.109      with xz have "?P ?z x (Ge (CN 0 c e))"
3.110        using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"]   by simp }
```
```     4.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Apr 03 23:51:52 2014 +0100
4.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Apr 04 17:58:25 2014 +0100
4.3 @@ -2708,7 +2708,7 @@
4.4      have "?rhs = Ifm vs (-?s / (2*?d) # bs) (Eq (CNP 0 a r))"
4.5        by (simp only: th)
4.6      also have "\<dots> \<longleftrightarrow> ?a * (-?s / (2*?d)) + ?r = 0"
4.7 -      by (simp add: r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"])
4.8 +      by (simp add: field_simps r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"])
4.9      also have "\<dots> \<longleftrightarrow> 2 * ?d * (?a * (-?s / (2*?d)) + ?r) = 0"
4.10        using d mult_cancel_left[of "2*?d" "(?a * (-?s / (2*?d)) + ?r)" 0] by simp
4.11      also have "\<dots> \<longleftrightarrow> (- ?a * ?s) * (2*?d / (2*?d)) + 2 * ?d * ?r= 0"
4.12 @@ -2728,12 +2728,12 @@
4.13      have "?rhs = Ifm vs (-?t / (2*?c) # bs) (Eq (CNP 0 a r))"
4.14        by (simp only: th)
4.15      also have "\<dots> \<longleftrightarrow> ?a * (-?t / (2*?c)) + ?r = 0"
4.16 -      by (simp add: r[of "- (?t/ (2 * ?c))"])
4.17 +      by (simp add: field_simps r[of "- (?t/ (2 * ?c))"])
4.18      also have "\<dots> \<longleftrightarrow> 2 * ?c * (?a * (-?t / (2 * ?c)) + ?r) = 0"
4.19        using c mult_cancel_left[of "2 * ?c" "(?a * (-?t / (2 * ?c)) + ?r)" 0] by simp
4.20      also have "\<dots> \<longleftrightarrow> (?a * -?t)* (2 * ?c) / (2 * ?c) + 2 * ?c * ?r= 0"
4.21        by (simp add: field_simps distrib_left[of "2 * ?c"] del: distrib_left)
4.22 -    also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2 * ?c * ?r = 0" using c by simp
4.23 +    also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2 * ?c * ?r = 0" using c by (simp add: field_simps)
4.24      finally have ?thesis using c d
4.25        by (simp add: r[of "- (?t/ (2 * ?c))"] msubsteq_def Let_def evaldjf_ex)
4.26    }
4.27 @@ -2755,7 +2755,7 @@
4.28        by simp
4.29      also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2 * ?c * ?d * ?r = 0"
4.30        using nonzero_mult_divide_cancel_left [OF dc] c d
4.31 -      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
4.32 +      by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
4.33      finally  have ?thesis using c d
4.34        by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"]
4.35            msubsteq_def Let_def evaldjf_ex field_simps)
4.36 @@ -2825,7 +2825,7 @@
4.37      have "?rhs = Ifm vs (-?s / (2*?d) # bs) (NEq (CNP 0 a r))"
4.38        by (simp only: th)
4.39      also have "\<dots> \<longleftrightarrow> ?a * (-?s / (2*?d)) + ?r \<noteq> 0"
4.40 -      by (simp add: r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"])
4.41 +      by (simp add: field_simps r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"])
4.42      also have "\<dots> \<longleftrightarrow> 2*?d * (?a * (-?s / (2*?d)) + ?r) \<noteq> 0"
4.43        using d mult_cancel_left[of "2*?d" "(?a * (-?s / (2*?d)) + ?r)" 0] by simp
4.44      also have "\<dots> \<longleftrightarrow> (- ?a * ?s) * (2*?d / (2*?d)) + 2*?d*?r\<noteq> 0"
4.45 @@ -2845,13 +2845,13 @@
4.46      have "?rhs = Ifm vs (-?t / (2*?c) # bs) (NEq (CNP 0 a r))"
4.47        by (simp only: th)
4.48      also have "\<dots> \<longleftrightarrow> ?a * (-?t / (2*?c)) + ?r \<noteq> 0"
4.49 -      by (simp add: r[of "- (?t/ (2 * ?c))"])
4.50 +      by (simp add: field_simps r[of "- (?t/ (2 * ?c))"])
4.51      also have "\<dots> \<longleftrightarrow> 2*?c * (?a * (-?t / (2*?c)) + ?r) \<noteq> 0"
4.52        using c mult_cancel_left[of "2*?c" "(?a * (-?t / (2*?c)) + ?r)" 0] by simp
4.53      also have "\<dots> \<longleftrightarrow> (?a * -?t)* (2*?c) / (2*?c) + 2*?c*?r \<noteq> 0"
4.54        by (simp add: field_simps distrib_left[of "2*?c"] del: distrib_left)
4.55      also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2*?c*?r \<noteq> 0"
4.56 -      using c by simp
4.57 +      using c by (simp add: field_simps)
4.58      finally have ?thesis
4.59        using c d by (simp add: r[of "- (?t/ (2*?c))"] msubstneq_def Let_def evaldjf_ex)
4.60    }
4.61 @@ -2873,7 +2873,7 @@
4.62        by simp
4.63      also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r \<noteq> 0"
4.64        using nonzero_mult_divide_cancel_left[OF dc] c d
4.65 -      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
4.66 +      by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
4.67      finally have ?thesis
4.68        using c d
4.69        by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"]
4.70 @@ -2963,7 +2963,7 @@
4.71        by simp
4.72      also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r < 0"
4.73        using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
4.74 -      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
4.75 +      by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
4.76      finally  have ?thesis using dc c d  nc nd dc'
4.77        by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"]
4.78            msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
4.79 @@ -2988,7 +2988,7 @@
4.80        by simp
4.81      also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - 2 * ?c * ?d * ?r < 0"
4.82        using nonzero_mult_divide_cancel_left[of "2 * ?c * ?d"] c d
4.83 -      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
4.84 +      by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
4.85      finally have ?thesis using dc c d nc nd
4.86        by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"]
4.87            msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
4.88 @@ -3005,14 +3005,14 @@
4.89      have "?rhs \<longleftrightarrow> Ifm vs (- ?t / (2 * ?c) # bs) (Lt (CNP 0 a r))"
4.90        by (simp only: th)
4.91      also have "\<dots> \<longleftrightarrow> ?a * (- ?t / (2 * ?c))+ ?r < 0"
4.92 -      by (simp add: r[of "- (?t / (2 * ?c))"])
4.93 +      by (simp add: field_simps r[of "- (?t / (2 * ?c))"])
4.94      also have "\<dots> \<longleftrightarrow> 2 * ?c * (?a * (- ?t / (2 * ?c))+ ?r) < 0"
4.95        using c mult_less_cancel_left_disj[of "2 * ?c" "?a* (- ?t / (2*?c))+ ?r" 0] c' c''
4.96          order_less_not_sym[OF c'']
4.97        by simp
4.98      also have "\<dots> \<longleftrightarrow> - ?a * ?t + 2 * ?c * ?r < 0"
4.99        using nonzero_mult_divide_cancel_left[OF c'] c
4.100 -      by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
4.101 +      by (simp add: divide_minus_left algebra_simps diff_divide_distrib less_le del: distrib_right)
4.102      finally have ?thesis using c d nc nd
4.103        by (simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps
4.104            lt polyneg_norm polymul_norm)
4.105 @@ -3029,7 +3029,7 @@
4.106      have "?rhs \<longleftrightarrow> Ifm vs (- ?t / (2*?c) # bs) (Lt (CNP 0 a r))"
4.107        by (simp only: th)
4.108      also have "\<dots> \<longleftrightarrow> ?a * (- ?t / (2*?c))+ ?r < 0"
4.109 -      by (simp add: r[of "- (?t / (2*?c))"])
4.110 +      by (simp add: field_simps r[of "- (?t / (2*?c))"])
4.111      also have "\<dots> \<longleftrightarrow> 2 * ?c * (?a * (- ?t / (2 * ?c))+ ?r) > 0"
4.112        using c order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
4.113          mult_less_cancel_left_disj[of "2 * ?c" 0 "?a* (- ?t / (2*?c))+ ?r"]
4.114 @@ -3037,7 +3037,7 @@
4.115      also have "\<dots> \<longleftrightarrow> ?a*?t -  2*?c *?r < 0"
4.116        using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c'']
4.117            less_imp_neq[OF c''] c''
4.118 -        by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
4.119 +        by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
4.120      finally have ?thesis using c d nc nd
4.121        by (simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps
4.122            lt polyneg_norm polymul_norm)
4.123 @@ -3054,14 +3054,14 @@
4.124      have "?rhs \<longleftrightarrow> Ifm vs (- ?s / (2 * ?d) # bs) (Lt (CNP 0 a r))"
4.125        by (simp only: th)
4.126      also have "\<dots> \<longleftrightarrow> ?a * (- ?s / (2 * ?d))+ ?r < 0"
4.127 -      by (simp add: r[of "- (?s / (2 * ?d))"])
4.128 +      by (simp add: field_simps r[of "- (?s / (2 * ?d))"])
4.129      also have "\<dots> \<longleftrightarrow> 2 * ?d * (?a * (- ?s / (2 * ?d))+ ?r) < 0"
4.130        using d mult_less_cancel_left_disj[of "2 * ?d" "?a * (- ?s / (2 * ?d))+ ?r" 0] d' d''
4.131          order_less_not_sym[OF d'']
4.132        by simp
4.133      also have "\<dots> \<longleftrightarrow> - ?a * ?s+  2 * ?d * ?r < 0"
4.134        using nonzero_mult_divide_cancel_left[OF d'] d
4.135 -      by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
4.136 +      by (simp add: divide_minus_left algebra_simps diff_divide_distrib less_le del: distrib_right)
4.137      finally have ?thesis using c d nc nd
4.138        by (simp add: r[of "- (?s / (2*?d))"] msubstlt_def Let_def evaldjf_ex field_simps
4.139            lt polyneg_norm polymul_norm)
4.140 @@ -3078,7 +3078,7 @@
4.141      have "?rhs \<longleftrightarrow> Ifm vs (- ?s / (2 * ?d) # bs) (Lt (CNP 0 a r))"
4.142        by (simp only: th)
4.143      also have "\<dots> \<longleftrightarrow> ?a * (- ?s / (2 * ?d)) + ?r < 0"
4.144 -      by (simp add: r[of "- (?s / (2 * ?d))"])
4.145 +      by (simp add: field_simps r[of "- (?s / (2 * ?d))"])
4.146      also have "\<dots> \<longleftrightarrow> 2 * ?d * (?a * (- ?s / (2 * ?d)) + ?r) > 0"
4.147        using d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
4.148          mult_less_cancel_left_disj[of "2 * ?d" 0 "?a* (- ?s / (2*?d))+ ?r"]
4.149 @@ -3086,7 +3086,7 @@
4.150      also have "\<dots> \<longleftrightarrow> ?a * ?s -  2 * ?d * ?r < 0"
4.151        using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d'']
4.152            less_imp_neq[OF d''] d''
4.153 -        by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
4.154 +        by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
4.155      finally have ?thesis using c d nc nd
4.156        by (simp add: r[of "- (?s / (2*?d))"] msubstlt_def Let_def evaldjf_ex field_simps
4.157            lt polyneg_norm polymul_norm)
4.158 @@ -3177,7 +3177,7 @@
4.159        by simp
4.160      also have "\<dots> \<longleftrightarrow> ?a * (- (?d * ?t + ?c* ?s )) + 2*?c*?d*?r \<le> 0"
4.161        using nonzero_mult_divide_cancel_left[of "2*?c*?d"] c d
4.162 -      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
4.163 +      by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
4.164      finally  have ?thesis using dc c d  nc nd dc'
4.165        by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstle_def
4.166            Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
4.167 @@ -3202,7 +3202,7 @@
4.168        by simp
4.169      also have "\<dots> \<longleftrightarrow> ?a * ((?d * ?t + ?c* ?s )) - 2 * ?c * ?d * ?r \<le> 0"
4.170        using nonzero_mult_divide_cancel_left[of "2 * ?c * ?d"] c d
4.171 -      by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
4.172 +      by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
4.173      finally  have ?thesis using dc c d  nc nd
4.174        by (simp add: r[of "(- (?d * ?t) + - (?c *?s)) / (2 * ?c * ?d)"] msubstle_def
4.175            Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
4.176 @@ -3219,14 +3219,14 @@
4.177      have "?rhs \<longleftrightarrow> Ifm vs (- ?t / (2 * ?c) # bs) (Le (CNP 0 a r))"
4.178        by (simp only: th)
4.179      also have "\<dots> \<longleftrightarrow> ?a * (- ?t / (2 * ?c))+ ?r \<le> 0"
4.180 -      by (simp add: r[of "- (?t / (2 * ?c))"])
4.181 +      by (simp add: field_simps r[of "- (?t / (2 * ?c))"])
4.182      also have "\<dots> \<longleftrightarrow> 2 * ?c * (?a * (- ?t / (2 * ?c))+ ?r) \<le> 0"
4.183        using c mult_le_cancel_left[of "2 * ?c" "?a* (- ?t / (2*?c))+ ?r" 0] c' c''
4.184          order_less_not_sym[OF c'']
4.185        by simp
4.186      also have "\<dots> \<longleftrightarrow> - ?a*?t+  2*?c *?r \<le> 0"
4.187        using nonzero_mult_divide_cancel_left[OF c'] c
4.188 -      by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
4.189 +      by (simp add: divide_minus_left algebra_simps diff_divide_distrib less_le del: distrib_right)
4.190      finally have ?thesis using c d nc nd
4.191        by (simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def
4.192            evaldjf_ex field_simps lt polyneg_norm polymul_norm)
4.193 @@ -3243,7 +3243,7 @@
4.194      have "?rhs \<longleftrightarrow> Ifm vs (- ?t / (2 * ?c) # bs) (Le (CNP 0 a r))"
4.195        by (simp only: th)
4.196      also have "\<dots> \<longleftrightarrow> ?a * (- ?t / (2*?c))+ ?r \<le> 0"
4.197 -      by (simp add: r[of "- (?t / (2*?c))"])
4.198 +      by (simp add: field_simps r[of "- (?t / (2*?c))"])
4.199      also have "\<dots> \<longleftrightarrow> 2 * ?c * (?a * (- ?t / (2 * ?c))+ ?r) \<ge> 0"
4.200        using c order_less_not_sym[OF c''] less_imp_neq[OF c''] c''
4.201          mult_le_cancel_left[of "2 * ?c" 0 "?a* (- ?t / (2*?c))+ ?r"]
4.202 @@ -3251,7 +3251,7 @@
4.203      also have "\<dots> \<longleftrightarrow> ?a * ?t - 2 * ?c * ?r \<le> 0"
4.204        using nonzero_mult_divide_cancel_left[OF c'] c order_less_not_sym[OF c'']
4.205            less_imp_neq[OF c''] c''
4.206 -        by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
4.207 +        by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
4.208      finally have ?thesis using c d nc nd
4.209        by (simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def
4.210            evaldjf_ex field_simps lt polyneg_norm polymul_norm)
4.211 @@ -3268,14 +3268,14 @@
4.212      have "?rhs \<longleftrightarrow> Ifm vs (- ?s / (2 * ?d) # bs) (Le (CNP 0 a r))"
4.213        by (simp only: th)
4.214      also have "\<dots> \<longleftrightarrow> ?a * (- ?s / (2 * ?d))+ ?r \<le> 0"
4.215 -      by (simp add: r[of "- (?s / (2*?d))"])
4.216 +      by (simp add: field_simps r[of "- (?s / (2*?d))"])
4.217      also have "\<dots> \<longleftrightarrow> 2 * ?d * (?a * (- ?s / (2 * ?d)) + ?r) \<le> 0"
4.218        using d mult_le_cancel_left[of "2 * ?d" "?a* (- ?s / (2*?d))+ ?r" 0] d' d''
4.219          order_less_not_sym[OF d'']
4.220        by simp
4.221      also have "\<dots> \<longleftrightarrow> - ?a * ?s + 2 * ?d * ?r \<le> 0"
4.222        using nonzero_mult_divide_cancel_left[OF d'] d
4.223 -      by (simp add: algebra_simps diff_divide_distrib less_le del: distrib_right)
4.224 +      by (simp add: divide_minus_left algebra_simps diff_divide_distrib less_le del: distrib_right)
4.225      finally have ?thesis using c d nc nd
4.226        by (simp add: r[of "- (?s / (2*?d))"] msubstle_def Let_def
4.227            evaldjf_ex field_simps lt polyneg_norm polymul_norm)
4.228 @@ -3292,7 +3292,7 @@
4.229      have "?rhs \<longleftrightarrow> Ifm vs (- ?s / (2*?d) # bs) (Le (CNP 0 a r))"
4.230        by (simp only: th)
4.231      also have "\<dots> \<longleftrightarrow> ?a* (- ?s / (2*?d))+ ?r \<le> 0"
4.232 -      by (simp add: r[of "- (?s / (2*?d))"])
4.233 +      by (simp add: field_simps r[of "- (?s / (2*?d))"])
4.234      also have "\<dots> \<longleftrightarrow> 2*?d * (?a* (- ?s / (2*?d))+ ?r) \<ge> 0"
4.235        using d order_less_not_sym[OF d''] less_imp_neq[OF d''] d''
4.236          mult_le_cancel_left[of "2 * ?d" 0 "?a* (- ?s / (2*?d))+ ?r"]
4.237 @@ -3300,7 +3300,7 @@
4.238      also have "\<dots> \<longleftrightarrow> ?a * ?s -  2 * ?d * ?r \<le> 0"
4.239        using nonzero_mult_divide_cancel_left[OF d'] d order_less_not_sym[OF d'']
4.240            less_imp_neq[OF d''] d''
4.241 -        by (simp add: algebra_simps diff_divide_distrib del: distrib_right)
4.242 +        by (simp add: divide_minus_left algebra_simps diff_divide_distrib del: distrib_right)
4.243      finally have ?thesis using c d nc nd
4.244        by (simp add: r[of "- (?s / (2*?d))"] msubstle_def Let_def
4.245            evaldjf_ex field_simps lt polyneg_norm polymul_norm)
4.246 @@ -3326,10 +3326,10 @@
4.247      Ifm vs (((- Itm vs (x#bs) t /  Ipoly vs c + - Itm vs (x#bs) s / Ipoly vs d) /2)#bs) p"
4.248    using lp
4.249    by (induct p rule: islin.induct)
4.250 -    (auto simp add: tmbound0_I
4.251 +    (auto simp add: tmbound0_I
4.252        [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"
4.253          and b' = x and bs = bs and vs = vs]
4.254 -      msubsteq msubstneq msubstlt [OF nc nd] msubstle [OF nc nd])
4.255 +      msubsteq msubstneq msubstlt [OF nc nd] msubstle [OF nc nd] divide_minus_left)
4.256
4.257  lemma msubst_nb:
4.258    assumes lp: "islin p"
4.259 @@ -3767,7 +3767,7 @@
4.260          by (auto simp add: msubst2_def lt zero_less_mult_iff mult_less_0_iff)
4.261        from msubst2[OF lp nn nn2(1), of x bs t]
4.262        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"
4.263 -        using H(2) nn2 by (simp add: mult_minus2_right)
4.264 +        using H(2) nn2 by (simp add: divide_minus_left divide_minus_right mult_minus2_right)
4.265      }
4.266      moreover
4.267      {
4.268 @@ -3780,7 +3780,7 @@
4.269        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"
4.270          using H(2) by (simp_all add: polymul_norm n2)
4.271        from msubst2[OF lp nn, of x bs t] have "?I (msubst2 p (n *\<^sub>p (C (-2,1))) t)"
4.272 -        using H(2,3) by (simp add: mult_minus2_right)
4.273 +        using H(2,3) by (simp add: divide_minus_left divide_minus_right mult_minus2_right)
4.274      }
4.275      ultimately show ?thesis by blast
4.276    qed
4.277 @@ -3811,7 +3811,7 @@
4.278        from msubst2[OF lp nn nn'(1), of x bs ] H(3) nn'
4.279        have "\<lparr>c\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and> \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup> \<noteq> 0 \<and>
4.280            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"
4.283      }
4.284      moreover
4.285      {
4.286 @@ -3828,7 +3828,7 @@
4.287          using H(3,4) by (simp_all add: polymul_norm n2)
4.288        from msubst2[OF lp nn, of x bs ] H(3,4,5)
4.289        have "Ifm vs (x#bs) (msubst2 p (C (-2, 1) *\<^sub>p c*\<^sub>p d) (Add (Mul d t) (Mul c s)))"
4.292      }
4.293      ultimately show ?thesis by blast
4.294    qed
```
```     5.1 --- a/src/HOL/Decision_Procs/Rat_Pair.thy	Thu Apr 03 23:51:52 2014 +0100
5.2 +++ b/src/HOL/Decision_Procs/Rat_Pair.thy	Fri Apr 04 17:58:25 2014 +0100
5.3 @@ -227,7 +227,7 @@
5.4      let ?g = "gcd a b"
5.5      from a b have g: "?g \<noteq> 0"by simp
5.6      from of_int_div[OF g, where ?'a = 'a]
5.7 -    have ?thesis by (auto simp add: x INum_def normNum_def split_def Let_def) }
5.8 +    have ?thesis by (auto simp: divide_minus_left divide_minus_right x INum_def normNum_def split_def Let_def) }
5.9    ultimately show ?thesis by blast
5.10  qed
5.11
5.12 @@ -300,13 +300,13 @@
5.13  qed
5.14
5.15  lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x ::'a:: field)"
5.16 -  by (simp add: Nneg_def split_def INum_def)
5.17 +  by (simp add: divide_minus_left Nneg_def split_def INum_def)
5.18
5.19  lemma Nsub[simp]: "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {field_char_0, field_inverse_zero})"
5.20    by (simp add: Nsub_def split_def)
5.21
5.22  lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: field_inverse_zero) / (INum x)"
5.23 -  by (simp add: Ninv_def INum_def split_def)
5.24 +  by (simp add: divide_minus_left divide_minus_right Ninv_def INum_def split_def)
5.25
5.26  lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0, field_inverse_zero})"
```
```     6.1 --- a/src/HOL/Fields.thy	Thu Apr 03 23:51:52 2014 +0100
6.2 +++ b/src/HOL/Fields.thy	Fri Apr 04 17:58:25 2014 +0100
6.3 @@ -152,7 +152,7 @@
6.4  lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"
6.5    by (simp add: divide_inverse nonzero_inverse_minus_eq)
6.6
6.7 -lemma divide_minus_left: "(-a) / b = - (a / b)"
6.8 +lemma divide_minus_left [field_simps]: "(-a) / b = - (a / b)"
6.10
6.11  lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
6.12 @@ -408,7 +408,7 @@
6.13    "- (a / b) = a / - b"
6.15
6.16 -lemma divide_minus_right:
6.17 +lemma divide_minus_right [field_simps]:
6.18    "a / - b = - (a / b)"
6.20
```
```     7.1 --- a/src/HOL/Library/Float.thy	Thu Apr 03 23:51:52 2014 +0100
7.2 +++ b/src/HOL/Library/Float.thy	Fri Apr 04 17:58:25 2014 +0100
7.3 @@ -637,7 +637,7 @@
7.4    qed
7.5    thus ?thesis using `\<not> b dvd a` by simp
7.6  qed (simp add: ceiling_def real_of_int_minus[symmetric] divide_minus_left[symmetric]
7.7 -  floor_divide_eq_div dvd_neg_div del: divide_minus_left real_of_int_minus)
7.8 +               floor_divide_eq_div dvd_neg_div del: real_of_int_minus)
7.9
7.10  lemma compute_float_up[code]:
7.11    "float_up p (Float m e) =
7.12 @@ -1004,7 +1004,7 @@
7.13        else (if 0 < y
7.14          then - (rapprox_posrat prec (nat (-x)) (nat y))
7.15          else lapprox_posrat prec (nat (-x)) (nat (-y))))"
7.16 -  by transfer (auto simp: round_up_def round_down_def ceiling_def ac_simps)
7.17 +  by transfer (auto simp: round_up_def divide_minus_left divide_minus_right round_down_def ceiling_def ac_simps)
7.18  hide_fact (open) compute_lapprox_rat
7.19
7.20  lift_definition rapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" is
7.21 @@ -1019,7 +1019,7 @@
7.22        else (if 0 < y
7.23          then - (lapprox_posrat prec (nat (-x)) (nat y))
7.24          else rapprox_posrat prec (nat (-x)) (nat (-y))))"
7.25 -  by transfer (auto simp: round_up_def round_down_def ceiling_def ac_simps)
7.26 +  by transfer (auto simp: round_up_def round_down_def divide_minus_left divide_minus_right ceiling_def ac_simps)
7.27  hide_fact (open) compute_rapprox_rat
7.28
7.29  subsection {* Division *}
```
```     8.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Thu Apr 03 23:51:52 2014 +0100
8.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Apr 04 17:58:25 2014 +0100
8.3 @@ -3635,7 +3635,7 @@
8.4    done
8.5
8.6  lemma fps_sin_even: "fps_sin (- c) = - fps_sin c"
8.7 -  by (auto simp add: fps_eq_iff fps_sin_def)
8.8 +  by (auto simp add: divide_minus_left fps_eq_iff fps_sin_def)
8.9
8.10  lemma fps_cos_odd: "fps_cos (- c) = fps_cos c"
8.11    by (auto simp add: fps_eq_iff fps_cos_def)
```