src/HOL/Decision_Procs/MIR.thy

   then have "c > 0" by simp
   hence rcpos: "real c > 0" by simp
   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
     with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
       by (simp only: mult_strict_left_mono [OF th1 rcpos])

   case (4 c e) 
   then have "c > 0" by simp hence rcpos: "real c > 0" by simp
   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
     with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
       by (simp only: mult_strict_left_mono [OF th1 rcpos])

   case (5 c e) 
   then have "c > 0" by simp hence rcpos: "real c > 0" by simp
   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
     with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
       by (simp only: mult_strict_left_mono [OF th1 rcpos])

   case (6 c e) 
   then have "c > 0" by simp hence rcpos: "real c > 0" by simp
   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
     with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
       by (simp only: mult_strict_left_mono [OF th1 rcpos])

   case (7 c e) 
   then have "c > 0" by simp hence rcpos: "real c > 0" by simp
   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
     with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
       by (simp only: mult_strict_left_mono [OF th1 rcpos])

   case (8 c e) 
   then have "c > 0" by simp hence rcpos: "real c > 0" by simp
   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
     with rcpos  have "(real c)*(real  x) < (real c)*(- (Inum (y # bs) e / real c))"
       by (simp only: mult_strict_left_mono [OF th1 rcpos])

   let ?e="Inum (a#bs) e"
   let ?z = "(- ?e) / real c"
   {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))"
       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
   hence "\<forall> x > ?z. ?P ?z x (Eq (CN 0 c e))" by simp

   let ?e="Inum (a#bs) e"
   let ?z = "(- ?e) / real c"
   {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))"
       using numbound0_I[OF nb, where b="x" and bs="bs" and b'="a"] by simp }
   hence "\<forall> x > ?z. ?P ?z x (NEq (CN 0 c e))" by simp

   let ?e="Inum (a#bs) e"
   let ?z = "(- ?e) / real c"
   {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 }
   hence "\<forall> x > ?z. ?P ?z x (Lt (CN 0 c e))" by simp
   thus ?case by blast

   let ?e="Inum (a#bs) e"
   let ?z = "(- ?e) / real c"
   {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 }
   hence "\<forall> x > ?z. ?P ?z x (Le (CN 0 c e))" by simp
   thus ?case by blast

   let ?e="Inum (a#bs) e"
   let ?z = "(- ?e) / real c"
   {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 }
   hence "\<forall> x > ?z. ?P ?z x (Gt (CN 0 c e))" by simp
   thus ?case by blast

   let ?e="Inum (a#bs) e"
   let ?z = "(- ?e) / real c"
   {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 }
   hence "\<forall> x > ?z. ?P ?z x (Ge (CN 0 c e))" by simp
   thus ?case by blast