# HG changeset patch
# User bulwahn
# Date 1330157259 -3600
# Node ID e9aa6d151329977df09a49b2e01cc71aa476afd4
# Parent  c1d2ab32174abb6ed05e8aba587fce2d564cbe96
removing unnecessary assumptions in RealDef;
simplifying proofs in Float, MIR, and Ferrack

diff -r c1d2ab32174a -r e9aa6d151329 src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Sat Feb 25 09:07:37 2012 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Sat Feb 25 09:07:39 2012 +0100
@@ -461,13 +461,11 @@
 proof (induct t rule: reducecoeffh.induct) 
   case (1 i)
   hence gd: "g dvd i" by simp
-  from gp have gnz: "g \<noteq> 0" by simp
-  with assms show ?case by (simp add: real_of_int_div[OF gnz gd])
+  with assms show ?case by (simp add: real_of_int_div[OF gd])
 next
   case (2 n c t)
   hence gd: "g dvd c" by simp
-  from gp have gnz: "g \<noteq> 0" by simp
-  from assms 2 show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps)
+  from assms 2 show ?case by (simp add: real_of_int_div[OF gd] algebra_simps)
 qed (auto simp add: numgcd_def gp)
 
 fun ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool" where
@@ -695,7 +693,7 @@
         from g1 g'1 have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_def Let_def)
         also have "\<dots> = (real ?g' * ?t) / (real ?g' * (real (n div ?g')))" by simp
         also have "\<dots> = (Inum bs ?t' / real n)"
-          using real_of_int_div[OF gp0 gpdd] th2 gp0 by simp
+          using real_of_int_div[OF gpdd] th2 gp0 by simp
         finally have "?lhs = Inum bs t / real n" by simp
         then have ?thesis by (simp add: simp_num_pair_def) }
       ultimately have ?thesis by blast }
diff -r c1d2ab32174a -r e9aa6d151329 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Sat Feb 25 09:07:37 2012 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy	Sat Feb 25 09:07:39 2012 +0100
@@ -602,16 +602,13 @@
   using gt
 proof(induct t rule: reducecoeffh.induct) 
   case (1 i) hence gd: "g dvd i" by simp
-  from gp have gnz: "g \<noteq> 0" by simp
-  from assms 1 show ?case by (simp add: real_of_int_div[OF gnz gd])
+  from assms 1 show ?case by (simp add: real_of_int_div[OF gd])
 next
   case (2 n c t)  hence gd: "g dvd c" by simp
-  from gp have gnz: "g \<noteq> 0" by simp
-  from assms 2 show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps)
+  from assms 2 show ?case by (simp add: real_of_int_div[OF gd] algebra_simps)
 next
   case (3 c s t)  hence gd: "g dvd c" by simp
-  from gp have gnz: "g \<noteq> 0" by simp
-  from assms 3 show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps) 
+  from assms 3 show ?case by (simp add: real_of_int_div[OF gd] algebra_simps) 
 qed (auto simp add: numgcd_def gp)
 
 fun ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool" where
@@ -972,7 +969,7 @@
         from nnz g1 g'1 have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_def Let_def)
         also have "\<dots> = (real ?g' * ?t) / (real ?g' * (real (n div ?g')))" by simp
         also have "\<dots> = (Inum bs ?t' / real n)"
-          using real_of_int_div[OF gp0 gpdd] th2 gp0 by simp
+          using real_of_int_div[OF gpdd] th2 gp0 by simp
         finally have "?lhs = Inum bs t / real n" by simp
         then have ?thesis using nnz g1 g'1 by (simp add: simp_num_pair_def) }
       ultimately have ?thesis by blast }
@@ -1105,7 +1102,7 @@
 next
   assume d: "real (d div g) rdvd real (c div g) * t"
   from gp have gnz: "g \<noteq> 0" by simp
-  thus "real d rdvd real c * t" using d rdvd_mult[OF gnz, where n="d div g" and x="real (c div g) * t"] real_of_int_div[OF gnz gd] real_of_int_div[OF gnz gc] by simp
+  thus "real d rdvd real c * t" using d rdvd_mult[OF gnz, where n="d div g" and x="real (c div g) * t"] real_of_int_div[OF gd] real_of_int_div[OF gc] by simp
 qed
 
 definition simpdvd :: "int \<Rightarrow> num \<Rightarrow> (int \<times> num)" where
@@ -2842,25 +2839,24 @@
   case (3 c e) 
   from 3 have cp: "c > 0" and nb: "numbound0 e" by auto
   { assume kdc: "k dvd c" 
-    from kpos have knz: "k\<noteq>0" by simp
     from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
-    from kdc have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt]
+    from kdc have ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
       numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
       numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
   moreover 
   { assume *: "\<not> k dvd c"
-    from kpos have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
+    from kpos have knz': "real k \<noteq> 0" by simp
     from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t"
       using isint_def by simp
     from assms * have "?I (real x) (?s (Eq (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k = 0)"
-      using real_of_int_div[OF knz kdt]
+      using real_of_int_div[OF kdt]
         numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
         numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
       by (simp add: ti algebra_simps)
       also have "\<dots> = (?I ?tk (Eq (CN 0 c e)))"
         using nonzero_eq_divide_eq[OF knz',
             where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric]
-          real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
+          real_of_int_div[OF kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
           numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
         by (simp add: ti)
       finally have ?case . }
@@ -2869,24 +2865,23 @@
   case (4 c e)  
   then have cp: "c > 0" and nb: "numbound0 e" by auto
   { assume kdc: "k dvd c" 
-    from kpos have knz: "k\<noteq>0" by simp
     from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
-    from kdc have  ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt]
+    from kdc have  ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
       numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
       numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
   moreover 
   { assume *: "\<not> k dvd c"
-    from kpos have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
+    from kpos have knz': "real k \<noteq> 0" by simp
     from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
     from assms * have "?I (real x) (?s (NEq (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k \<noteq> 0)"
-      using real_of_int_div[OF knz kdt]
+      using real_of_int_div[OF kdt]
         numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
         numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
       by (simp add: ti algebra_simps)
     also have "\<dots> = (?I ?tk (NEq (CN 0 c e)))"
       using nonzero_eq_divide_eq[OF knz',
           where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric]
-        real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
+        real_of_int_div[OF kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
         numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
       by (simp add: ti)
     finally have ?case . }
@@ -2895,50 +2890,46 @@
   case (5 c e) 
   then have cp: "c > 0" and nb: "numbound0 e" by auto
   { assume kdc: "k dvd c" 
-    from kpos have knz: "k\<noteq>0" by simp
     from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
-    from kdc have  ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt]
+    from kdc have  ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
       numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
       numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
   moreover 
   { assume *: "\<not> k dvd c"
-    from kpos have knz: "k\<noteq>0" by simp
     from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
     from assms * have "?I (real x) (?s (Lt (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k < 0)"
-      using real_of_int_div[OF knz kdt]
+      using real_of_int_div[OF kdt]
         numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
         numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
       by (simp add: ti algebra_simps)
     also have "\<dots> = (?I ?tk (Lt (CN 0 c e)))"
       using pos_less_divide_eq[OF kpos,
           where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric]
-        real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
+        real_of_int_div[OF kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
         numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
       by (simp add: ti)
     finally have ?case . }
   ultimately show ?case by blast 
 next
-  case (6 c e)  
+  case (6 c e)
   then have cp: "c > 0" and nb: "numbound0 e" by auto
   { assume kdc: "k dvd c" 
-    from kpos have knz: "k\<noteq>0" by simp
     from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
-    from kdc have  ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt]
+    from kdc have  ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
       numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
       numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
   moreover 
   { assume *: "\<not> k dvd c"
-    from kpos have knz: "k\<noteq>0" by simp
     from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
     from assms * have "?I (real x) (?s (Le (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k \<le> 0)"
-      using real_of_int_div[OF knz kdt]
+      using real_of_int_div[OF kdt]
         numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
         numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
       by (simp add: ti algebra_simps)
     also have "\<dots> = (?I ?tk (Le (CN 0 c e)))"
       using pos_le_divide_eq[OF kpos,
           where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric]
-        real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
+        real_of_int_div[OF kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
         numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
       by (simp add: ti)
     finally have ?case . }
@@ -2947,24 +2938,22 @@
   case (7 c e) 
   then have cp: "c > 0" and nb: "numbound0 e" by auto
   { assume kdc: "k dvd c" 
-    from kpos have knz: "k\<noteq>0" by simp
     from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
-    from kdc have  ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt]
+    from kdc have  ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
       numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
       numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
   moreover 
   { assume *: "\<not> k dvd c"
-    from kpos have knz: "k\<noteq>0" by simp
     from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
     from assms * have "?I (real x) (?s (Gt (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k > 0)"
-      using real_of_int_div[OF knz kdt]
+      using real_of_int_div[OF kdt]
         numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
         numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
       by (simp add: ti algebra_simps)
     also have "\<dots> = (?I ?tk (Gt (CN 0 c e)))"
       using pos_divide_less_eq[OF kpos,
           where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric]
-        real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
+        real_of_int_div[OF kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
         numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
       by (simp add: ti)
     finally have ?case . }
@@ -2973,24 +2962,22 @@
   case (8 c e)  
   then have cp: "c > 0" and nb: "numbound0 e" by auto
   { assume kdc: "k dvd c" 
-    from kpos have knz: "k\<noteq>0" by simp
     from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
-    from kdc have  ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt]
+    from kdc have  ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
       numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
       numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
   moreover 
   { assume *: "\<not> k dvd c"
-    from kpos have knz: "k\<noteq>0" by simp
     from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
     from assms * have "?I (real x) (?s (Ge (CN 0 c e))) = ((real c * (?N (real x) t / real k) + ?N (real x) e)* real k \<ge> 0)"
-      using real_of_int_div[OF knz kdt]
+      using real_of_int_div[OF kdt]
         numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
         numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
       by (simp add: ti algebra_simps)
     also have "\<dots> = (?I ?tk (Ge (CN 0 c e)))"
       using pos_divide_le_eq[OF kpos,
           where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric]
-        real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
+        real_of_int_div[OF kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
         numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
       by (simp add: ti)
     finally have ?case . }
@@ -2999,9 +2986,8 @@
   case (9 i c e)
   then have cp: "c > 0" and nb: "numbound0 e" by auto
   { assume kdc: "k dvd c" 
-    from kpos have knz: "k\<noteq>0" by simp
     from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
-    from kdc have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt]
+    from kdc have ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
       numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
       numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
   moreover 
@@ -3009,13 +2995,13 @@
     from kpos have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
     from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
     from assms * have "?I (real x) (?s (Dvd i (CN 0 c e))) = (real i * real k rdvd (real c * (?N (real x) t / real k) + ?N (real x) e)* real k)"
-      using real_of_int_div[OF knz kdt]
+      using real_of_int_div[OF kdt]
         numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
         numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
       by (simp add: ti algebra_simps)
     also have "\<dots> = (?I ?tk (Dvd i (CN 0 c e)))"
       using rdvd_mult[OF knz, where n="i"]
-        real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
+        real_of_int_div[OF kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
         numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
       by (simp add: ti)
     finally have ?case . }
@@ -3024,9 +3010,8 @@
   case (10 i c e)
   then have cp: "c > 0" and nb: "numbound0 e" by auto
   { assume kdc: "k dvd c" 
-    from kpos have knz: "k\<noteq>0" by simp
     from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
-    from kdc have  ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt]
+    from kdc have  ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
       numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
       numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
   moreover 
@@ -3034,12 +3019,12 @@
     from kpos have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
     from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
     from assms * have "?I (real x) (?s (NDvd i (CN 0 c e))) = (\<not> (real i * real k rdvd (real c * (?N (real x) t / real k) + ?N (real x) e)* real k))"
-      using real_of_int_div[OF knz kdt]
+      using real_of_int_div[OF kdt]
         numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
         numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
       by (simp add: ti algebra_simps)
     also have "\<dots> = (?I ?tk (NDvd i (CN 0 c e)))"
-      using rdvd_mult[OF knz, where n="i"] real_of_int_div[OF knz kdt]
+      using rdvd_mult[OF knz, where n="i"] real_of_int_div[OF kdt]
         numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
         numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
       by (simp add: ti)
diff -r c1d2ab32174a -r e9aa6d151329 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Sat Feb 25 09:07:37 2012 +0100
+++ b/src/HOL/Library/Float.thy	Sat Feb 25 09:07:39 2012 +0100
@@ -670,7 +670,7 @@
   let ?l = "nat (int prec + bitlen y - bitlen x)" let ?X = "x * 2^?l"
   show ?thesis 
   proof (cases "?X mod y = 0")
-    case True hence "y \<noteq> 0" and "y dvd ?X" using `0 < y` by auto
+    case True hence "y dvd ?X" using `0 < y` by auto
     from real_of_int_div[OF this]
     have "real (?X div y) * inverse (2 ^ ?l) = real ?X / real y * inverse (2 ^ ?l)" by auto
     also have "\<dots> = real x / real y * (2^?l * inverse (2^?l))" by auto
@@ -702,7 +702,7 @@
   let ?l = "nat (int n + bitlen y - bitlen x)" let ?X = "x * 2^?l"
   show ?thesis
   proof (cases "?X mod y = 0")
-    case True hence "y \<noteq> 0" and "y dvd ?X" using `0 < y` by auto
+    case True hence "y dvd ?X" using `0 < y` by auto
     from real_of_int_div[OF this]
     have "real (?X div y) * inverse (2 ^ ?l) = real ?X / real y * inverse (2 ^ ?l)" by auto
     also have "\<dots> = real x / real y * (2^?l * inverse (2^?l))" by auto
@@ -757,7 +757,7 @@
   let ?l = "nat (int n + bitlen y - bitlen x)" let ?X = "x * 2^?l"
   show ?thesis
   proof (cases "?X mod y = 0")
-    case True hence "y \<noteq> 0" and "y dvd ?X" using `0 < y` by auto
+    case True hence "y dvd ?X" using `0 < y` by auto
     from real_of_int_div[OF this]
     have "real (?X div y) * inverse (2 ^ ?l) = real ?X / real y * inverse (2 ^ ?l)" by auto
     also have "\<dots> = real x / real y * (2^?l * inverse (2^?l))" by auto
diff -r c1d2ab32174a -r e9aa6d151329 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Sat Feb 25 09:07:37 2012 +0100
+++ b/src/HOL/RealDef.thy	Sat Feb 25 09:07:39 2012 +0100
@@ -1184,10 +1184,9 @@
   apply simp
 done
 
-lemma real_of_int_div_aux: "d ~= 0 ==> (real (x::int)) / (real d) = 
+lemma real_of_int_div_aux: "(real (x::int)) / (real d) = 
     real (x div d) + (real (x mod d)) / (real d)"
 proof -
-  assume d: "d ~= 0"
   have "x = (x div d) * d + x mod d"
     by auto
   then have "real x = real (x div d) * real d + real(x mod d)"
@@ -1195,12 +1194,12 @@
   then have "real x / real d = ... / real d"
     by simp
   then show ?thesis
-    by (auto simp add: add_divide_distrib algebra_simps d)
+    by (auto simp add: add_divide_distrib algebra_simps)
 qed
 
-lemma real_of_int_div: "(d::int) ~= 0 ==> d dvd n ==>
+lemma real_of_int_div: "(d :: int) dvd n ==>
     real(n div d) = real n / real d"
-  apply (frule real_of_int_div_aux [of d n])
+  apply (subst real_of_int_div_aux)
   apply simp
   apply (simp add: dvd_eq_mod_eq_0)
 done
@@ -1213,34 +1212,20 @@
   apply (simp add: algebra_simps)
   apply (subst real_of_int_div_aux)
   apply simp
-  apply simp
   apply (subst zero_le_divide_iff)
   apply auto
   apply (simp add: algebra_simps)
   apply (subst real_of_int_div_aux)
   apply simp
-  apply simp
   apply (subst zero_le_divide_iff)
   apply auto
 done
 
 lemma real_of_int_div3:
   "real (n::int) / real (x) - real (n div x) <= 1"
-  apply(case_tac "x = 0")
-  apply simp
   apply (simp add: algebra_simps)
   apply (subst real_of_int_div_aux)
-  apply assumption
-  apply simp
-  apply (subst divide_le_eq)
-  apply clarsimp
-  apply (rule conjI)
-  apply (rule impI)
-  apply (rule order_less_imp_le)
-  apply simp
-  apply (rule impI)
-  apply (rule order_less_imp_le)
-  apply simp
+  apply (auto simp add: divide_le_eq intro: order_less_imp_le)
 done
 
 lemma real_of_int_div4: "real (n div x) <= real (n::int) / real x" 
@@ -1337,10 +1322,9 @@
   apply (simp add: real_of_nat_Suc)
 done
 
-lemma real_of_nat_div_aux: "0 < d ==> (real (x::nat)) / (real d) = 
+lemma real_of_nat_div_aux: "(real (x::nat)) / (real d) = 
     real (x div d) + (real (x mod d)) / (real d)"
 proof -
-  assume d: "0 < d"
   have "x = (x div d) * d + x mod d"
     by auto
   then have "real x = real (x div d) * real d + real(x mod d)"
@@ -1348,24 +1332,18 @@
   then have "real x / real d = \<dots> / real d"
     by simp
   then show ?thesis
-    by (auto simp add: add_divide_distrib algebra_simps d)
+    by (auto simp add: add_divide_distrib algebra_simps)
 qed
 
-lemma real_of_nat_div: "0 < (d::nat) ==> d dvd n ==>
+lemma real_of_nat_div: "(d :: nat) dvd n ==>
     real(n div d) = real n / real d"
-  apply (frule real_of_nat_div_aux [of d n])
-  apply simp
-  apply (subst dvd_eq_mod_eq_0 [THEN sym])
-  apply assumption
-done
+  by (subst real_of_nat_div_aux)
+    (auto simp add: dvd_eq_mod_eq_0 [symmetric])
 
 lemma real_of_nat_div2:
   "0 <= real (n::nat) / real (x) - real (n div x)"
-apply(case_tac "x = 0")
- apply (simp)
 apply (simp add: algebra_simps)
 apply (subst real_of_nat_div_aux)
- apply simp
 apply simp
 apply (subst zero_le_divide_iff)
 apply simp
@@ -1377,7 +1355,6 @@
 apply (simp)
 apply (simp add: algebra_simps)
 apply (subst real_of_nat_div_aux)
- apply simp
 apply simp
 done