# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1396630705 -3600
# Node ID a14831ac3023790f61bc66cdf9dc71eda2e8ce33
# Parent  36489d77c4840735a168eb43cd049e33819101b1
divide_minus_left divide_minus_right are in field_simps but are not default simprules

diff -r 36489d77c484 -r a14831ac3023 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Thu Apr 03 23:51:52 2014 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Fri Apr 04 17:58:25 2014 +0100
@@ -1466,7 +1466,8 @@
         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
+      have "exp x = exp (?num * (x / ?num))" using `real ?num \<noteq> 0`
+        by (auto simp: divide_minus_left divide_minus_right)
       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
@@ -1486,15 +1487,16 @@
         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 intro!: order_trans[OF float_divl] divide_nonpos_neg)
-
+          using `real (floor_fl x) < 0` `real x \<le> 0` 
+            by (auto simp: field_simps intro!: order_trans[OF float_divl])
         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
+        also have "\<dots> = exp x" using `real ?num \<noteq> 0` 
+          by (auto simp: field_simps)
         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
@@ -1506,7 +1508,8 @@
         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
+        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)
         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
diff -r 36489d77c484 -r a14831ac3023 src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Thu Apr 03 23:51:52 2014 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Fri Apr 04 17:58:25 2014 +0100
@@ -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: mult_ac)
+    have "(real c * x > - ?e)" by (simp add: divide_minus_left 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: mult_ac)
+    have "(real c * x > - ?e)" by (simp add: divide_minus_left 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: mult_ac)
+    have "(real c * x > - ?e)" by (simp add: divide_minus_left 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: mult_ac)
+    have "(real c * x > - ?e)" by (simp add: divide_minus_left 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: mult_ac)
+    have "(real c * x > - ?e)" by (simp add: divide_minus_left 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: mult_ac)
+    have "(real c * x > - ?e)" by (simp add: divide_minus_left 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 }
diff -r 36489d77c484 -r a14831ac3023 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Thu Apr 03 23:51:52 2014 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy	Fri Apr 04 17:58:25 2014 +0100
@@ -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: less_floor_eq , rule allI, rule impI) 
+  proof (simp add: divide_minus_left 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: less_floor_eq , rule allI, rule impI) 
+  proof (simp add: divide_minus_left 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: less_floor_eq , rule allI, rule impI) 
+  proof (simp add: divide_minus_left 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: less_floor_eq , rule allI, rule impI) 
+  proof (simp add: divide_minus_left 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: less_floor_eq , rule allI, rule impI) 
+  proof (simp add: divide_minus_left 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: less_floor_eq , rule allI, rule impI) 
+  proof (simp add: divide_minus_left 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: mult_ac)
+    have "(real c * x > - ?e)" by (simp add: divide_minus_left 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: mult_ac)
+    have "(real c * x > - ?e)" by (simp add: divide_minus_left 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: mult_ac)
+    have "(real c * x > - ?e)" by (simp add: divide_minus_left 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: mult_ac)
+    have "(real c * x > - ?e)" by (simp add: divide_minus_left 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: mult_ac)
+    have "(real c * x > - ?e)" by (simp add: divide_minus_left 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: mult_ac)
+    have "(real c * x > - ?e)" by (simp add: divide_minus_left 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 }
diff -r 36489d77c484 -r a14831ac3023 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Apr 03 23:51:52 2014 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Apr 04 17:58:25 2014 +0100
@@ -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: r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"])
+      by (simp add: field_simps 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: r[of "- (?t/ (2 * ?c))"])
+      by (simp add: field_simps 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
+    also have "\<dots> \<longleftrightarrow> - (?a * ?t) + 2 * ?c * ?r = 0" using c by (simp add: field_simps)
     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: algebra_simps diff_divide_distrib del: distrib_right)
+      by (simp add: divide_minus_left 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: r[of "- (Itm vs (x # bs) s / (2 * \<lparr>d\<rparr>\<^sub>p\<^bsup>vs\<^esup>))"])
+      by (simp add: field_simps 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: r[of "- (?t/ (2 * ?c))"])
+      by (simp add: field_simps 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
+      using c by (simp add: field_simps)
     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: algebra_simps diff_divide_distrib del: distrib_right)
+      by (simp add: divide_minus_left 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: algebra_simps diff_divide_distrib del: distrib_right)
+      by (simp add: divide_minus_left 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: algebra_simps diff_divide_distrib del: distrib_right)
+      by (simp add: divide_minus_left 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: r[of "- (?t / (2 * ?c))"])
+      by (simp add: field_simps 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: algebra_simps diff_divide_distrib less_le del: distrib_right)
+      by (simp add: divide_minus_left 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: r[of "- (?t / (2*?c))"])
+      by (simp add: field_simps 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: algebra_simps diff_divide_distrib del: distrib_right)
+        by (simp add: divide_minus_left 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: r[of "- (?s / (2 * ?d))"])
+      by (simp add: field_simps 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: algebra_simps diff_divide_distrib less_le del: distrib_right)
+      by (simp add: divide_minus_left 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: r[of "- (?s / (2 * ?d))"])
+      by (simp add: field_simps 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: algebra_simps diff_divide_distrib del: distrib_right)
+        by (simp add: divide_minus_left 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: algebra_simps diff_divide_distrib del: distrib_right)
+      by (simp add: divide_minus_left 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: algebra_simps diff_divide_distrib del: distrib_right)
+      by (simp add: divide_minus_left 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: r[of "- (?t / (2 * ?c))"])
+      by (simp add: field_simps 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: algebra_simps diff_divide_distrib less_le del: distrib_right)
+      by (simp add: divide_minus_left 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: r[of "- (?t / (2*?c))"])
+      by (simp add: field_simps 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: algebra_simps diff_divide_distrib del: distrib_right)
+        by (simp add: divide_minus_left 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: r[of "- (?s / (2*?d))"])
+      by (simp add: field_simps 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: algebra_simps diff_divide_distrib less_le del: distrib_right)
+      by (simp add: divide_minus_left 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: r[of "- (?s / (2*?d))"])
+      by (simp add: field_simps 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: algebra_simps diff_divide_distrib del: distrib_right)
+        by (simp add: divide_minus_left 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])
+      msubsteq msubstneq msubstlt [OF nc nd] msubstle [OF nc nd] divide_minus_left)
 
 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: mult_minus2_right)
+        using H(2) nn2 by (simp add: divide_minus_left divide_minus_right 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: mult_minus2_right)
+        using H(2,3) by (simp add: divide_minus_left divide_minus_right 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: add_divide_distrib diff_divide_distrib mult_minus2_left mult_commute)
+        by (simp add: divide_minus_left divide_minus_right 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: diff_divide_distrib add_divide_distrib mult_minus2_left mult_commute)
+        by (simp add: divide_minus_left divide_minus_right diff_divide_distrib add_divide_distrib mult_minus2_left mult_commute)
     }
     ultimately show ?thesis by blast
   qed
diff -r 36489d77c484 -r a14831ac3023 src/HOL/Decision_Procs/Rat_Pair.thy
--- a/src/HOL/Decision_Procs/Rat_Pair.thy	Thu Apr 03 23:51:52 2014 +0100
+++ b/src/HOL/Decision_Procs/Rat_Pair.thy	Fri Apr 04 17:58:25 2014 +0100
@@ -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 add: x INum_def normNum_def split_def Let_def) }
+    have ?thesis by (auto simp: divide_minus_left divide_minus_right 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: Nneg_def split_def INum_def)
+  by (simp add: divide_minus_left 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: Ninv_def INum_def split_def)
+  by (simp add: divide_minus_left divide_minus_right 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)
diff -r 36489d77c484 -r a14831ac3023 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Thu Apr 03 23:51:52 2014 +0100
+++ b/src/HOL/Fields.thy	Fri Apr 04 17:58:25 2014 +0100
@@ -152,7 +152,7 @@
 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: "(-a) / b = - (a / b)"
+lemma divide_minus_left [field_simps]: "(-a) / b = - (a / b)"
   by (simp add: divide_inverse)
 
 lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
@@ -408,7 +408,7 @@
   "- (a / b) = a / - b"
   by (simp add: divide_inverse)
 
-lemma divide_minus_right:
+lemma divide_minus_right [field_simps]:
   "a / - b = - (a / b)"
   by (simp add: divide_inverse)
 
diff -r 36489d77c484 -r a14831ac3023 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Thu Apr 03 23:51:52 2014 +0100
+++ b/src/HOL/Library/Float.thy	Fri Apr 04 17:58:25 2014 +0100
@@ -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: divide_minus_left real_of_int_minus)
+               floor_divide_eq_div dvd_neg_div del: 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 round_down_def ceiling_def ac_simps)
+  by transfer (auto simp: round_up_def divide_minus_left divide_minus_right 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 ceiling_def ac_simps)
+  by transfer (auto simp: round_up_def round_down_def divide_minus_left divide_minus_right ceiling_def ac_simps)
 hide_fact (open) compute_rapprox_rat
 
 subsection {* Division *}
diff -r 36489d77c484 -r a14831ac3023 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Thu Apr 03 23:51:52 2014 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Apr 04 17:58:25 2014 +0100
@@ -3635,7 +3635,7 @@
   done
 
 lemma fps_sin_even: "fps_sin (- c) = - fps_sin c"
-  by (auto simp add: fps_eq_iff fps_sin_def)
+  by (auto simp add: divide_minus_left 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)