divide_minus_left divide_minus_right are in field_simps but are not default simprules
authorpaulson <lp15@cam.ac.uk>
Fri Apr 04 17:58:25 2014 +0100 (2014-04-04)
changeset 56410a14831ac3023
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
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/Rat_Pair.thy
src/HOL/Fields.thy
src/HOL/Library/Float.thy
src/HOL/Library/Formal_Power_Series.thy
     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.281 -        by (simp add: add_divide_distrib diff_divide_distrib mult_minus2_left mult_commute)
   4.282 +        by (simp add: divide_minus_left divide_minus_right add_divide_distrib diff_divide_distrib mult_minus2_left mult_commute)
   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.290 -        by (simp add: diff_divide_distrib add_divide_distrib mult_minus2_left mult_commute)
   4.291 +        by (simp add: divide_minus_left divide_minus_right diff_divide_distrib add_divide_distrib mult_minus2_left mult_commute)
   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})"
    5.27    by (simp add: Ndiv_def)
     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.9    by (simp add: divide_inverse)
    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.14    by (simp add: divide_inverse)
    6.15  
    6.16 -lemma divide_minus_right:
    6.17 +lemma divide_minus_right [field_simps]:
    6.18    "a / - b = - (a / b)"
    6.19    by (simp add: divide_inverse)
    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)