removing unnecessary assumptions in RealDef;
authorbulwahn
Sat Feb 25 09:07:39 2012 +0100 (2012-02-25)
changeset 46670e9aa6d151329
parent 46669 c1d2ab32174a
child 46671 3a40ea076230
removing unnecessary assumptions in RealDef;
simplifying proofs in Float, MIR, and Ferrack
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Library/Float.thy
src/HOL/RealDef.thy
     1.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Sat Feb 25 09:07:37 2012 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Sat Feb 25 09:07:39 2012 +0100
     1.3 @@ -461,13 +461,11 @@
     1.4  proof (induct t rule: reducecoeffh.induct) 
     1.5    case (1 i)
     1.6    hence gd: "g dvd i" by simp
     1.7 -  from gp have gnz: "g \<noteq> 0" by simp
     1.8 -  with assms show ?case by (simp add: real_of_int_div[OF gnz gd])
     1.9 +  with assms show ?case by (simp add: real_of_int_div[OF gd])
    1.10  next
    1.11    case (2 n c t)
    1.12    hence gd: "g dvd c" by simp
    1.13 -  from gp have gnz: "g \<noteq> 0" by simp
    1.14 -  from assms 2 show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps)
    1.15 +  from assms 2 show ?case by (simp add: real_of_int_div[OF gd] algebra_simps)
    1.16  qed (auto simp add: numgcd_def gp)
    1.17  
    1.18  fun ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool" where
    1.19 @@ -695,7 +693,7 @@
    1.20          from g1 g'1 have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_def Let_def)
    1.21          also have "\<dots> = (real ?g' * ?t) / (real ?g' * (real (n div ?g')))" by simp
    1.22          also have "\<dots> = (Inum bs ?t' / real n)"
    1.23 -          using real_of_int_div[OF gp0 gpdd] th2 gp0 by simp
    1.24 +          using real_of_int_div[OF gpdd] th2 gp0 by simp
    1.25          finally have "?lhs = Inum bs t / real n" by simp
    1.26          then have ?thesis by (simp add: simp_num_pair_def) }
    1.27        ultimately have ?thesis by blast }
     2.1 --- a/src/HOL/Decision_Procs/MIR.thy	Sat Feb 25 09:07:37 2012 +0100
     2.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Sat Feb 25 09:07:39 2012 +0100
     2.3 @@ -602,16 +602,13 @@
     2.4    using gt
     2.5  proof(induct t rule: reducecoeffh.induct) 
     2.6    case (1 i) hence gd: "g dvd i" by simp
     2.7 -  from gp have gnz: "g \<noteq> 0" by simp
     2.8 -  from assms 1 show ?case by (simp add: real_of_int_div[OF gnz gd])
     2.9 +  from assms 1 show ?case by (simp add: real_of_int_div[OF gd])
    2.10  next
    2.11    case (2 n c t)  hence gd: "g dvd c" by simp
    2.12 -  from gp have gnz: "g \<noteq> 0" by simp
    2.13 -  from assms 2 show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps)
    2.14 +  from assms 2 show ?case by (simp add: real_of_int_div[OF gd] algebra_simps)
    2.15  next
    2.16    case (3 c s t)  hence gd: "g dvd c" by simp
    2.17 -  from gp have gnz: "g \<noteq> 0" by simp
    2.18 -  from assms 3 show ?case by (simp add: real_of_int_div[OF gnz gd] algebra_simps) 
    2.19 +  from assms 3 show ?case by (simp add: real_of_int_div[OF gd] algebra_simps) 
    2.20  qed (auto simp add: numgcd_def gp)
    2.21  
    2.22  fun ismaxcoeff:: "num \<Rightarrow> int \<Rightarrow> bool" where
    2.23 @@ -972,7 +969,7 @@
    2.24          from nnz g1 g'1 have "?lhs = ?t / real (n div ?g')" by (simp add: simp_num_pair_def Let_def)
    2.25          also have "\<dots> = (real ?g' * ?t) / (real ?g' * (real (n div ?g')))" by simp
    2.26          also have "\<dots> = (Inum bs ?t' / real n)"
    2.27 -          using real_of_int_div[OF gp0 gpdd] th2 gp0 by simp
    2.28 +          using real_of_int_div[OF gpdd] th2 gp0 by simp
    2.29          finally have "?lhs = Inum bs t / real n" by simp
    2.30          then have ?thesis using nnz g1 g'1 by (simp add: simp_num_pair_def) }
    2.31        ultimately have ?thesis by blast }
    2.32 @@ -1105,7 +1102,7 @@
    2.33  next
    2.34    assume d: "real (d div g) rdvd real (c div g) * t"
    2.35    from gp have gnz: "g \<noteq> 0" by simp
    2.36 -  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
    2.37 +  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
    2.38  qed
    2.39  
    2.40  definition simpdvd :: "int \<Rightarrow> num \<Rightarrow> (int \<times> num)" where
    2.41 @@ -2842,25 +2839,24 @@
    2.42    case (3 c e) 
    2.43    from 3 have cp: "c > 0" and nb: "numbound0 e" by auto
    2.44    { assume kdc: "k dvd c" 
    2.45 -    from kpos have knz: "k\<noteq>0" by simp
    2.46      from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
    2.47 -    from kdc have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt]
    2.48 +    from kdc have ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
    2.49        numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
    2.50        numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
    2.51    moreover 
    2.52    { assume *: "\<not> k dvd c"
    2.53 -    from kpos have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
    2.54 +    from kpos have knz': "real k \<noteq> 0" by simp
    2.55      from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t"
    2.56        using isint_def by simp
    2.57      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)"
    2.58 -      using real_of_int_div[OF knz kdt]
    2.59 +      using real_of_int_div[OF kdt]
    2.60          numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
    2.61          numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
    2.62        by (simp add: ti algebra_simps)
    2.63        also have "\<dots> = (?I ?tk (Eq (CN 0 c e)))"
    2.64          using nonzero_eq_divide_eq[OF knz',
    2.65              where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric]
    2.66 -          real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
    2.67 +          real_of_int_div[OF kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
    2.68            numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
    2.69          by (simp add: ti)
    2.70        finally have ?case . }
    2.71 @@ -2869,24 +2865,23 @@
    2.72    case (4 c e)  
    2.73    then have cp: "c > 0" and nb: "numbound0 e" by auto
    2.74    { assume kdc: "k dvd c" 
    2.75 -    from kpos have knz: "k\<noteq>0" by simp
    2.76      from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
    2.77 -    from kdc have  ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt]
    2.78 +    from kdc have  ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
    2.79        numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
    2.80        numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
    2.81    moreover 
    2.82    { assume *: "\<not> k dvd c"
    2.83 -    from kpos have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
    2.84 +    from kpos have knz': "real k \<noteq> 0" by simp
    2.85      from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
    2.86      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)"
    2.87 -      using real_of_int_div[OF knz kdt]
    2.88 +      using real_of_int_div[OF kdt]
    2.89          numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
    2.90          numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
    2.91        by (simp add: ti algebra_simps)
    2.92      also have "\<dots> = (?I ?tk (NEq (CN 0 c e)))"
    2.93        using nonzero_eq_divide_eq[OF knz',
    2.94            where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric]
    2.95 -        real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
    2.96 +        real_of_int_div[OF kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
    2.97          numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
    2.98        by (simp add: ti)
    2.99      finally have ?case . }
   2.100 @@ -2895,50 +2890,46 @@
   2.101    case (5 c e) 
   2.102    then have cp: "c > 0" and nb: "numbound0 e" by auto
   2.103    { assume kdc: "k dvd c" 
   2.104 -    from kpos have knz: "k\<noteq>0" by simp
   2.105      from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
   2.106 -    from kdc have  ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt]
   2.107 +    from kdc have  ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
   2.108        numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   2.109        numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
   2.110    moreover 
   2.111    { assume *: "\<not> k dvd c"
   2.112 -    from kpos have knz: "k\<noteq>0" by simp
   2.113      from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
   2.114      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)"
   2.115 -      using real_of_int_div[OF knz kdt]
   2.116 +      using real_of_int_div[OF kdt]
   2.117          numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   2.118          numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
   2.119        by (simp add: ti algebra_simps)
   2.120      also have "\<dots> = (?I ?tk (Lt (CN 0 c e)))"
   2.121        using pos_less_divide_eq[OF kpos,
   2.122            where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric]
   2.123 -        real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   2.124 +        real_of_int_div[OF kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   2.125          numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
   2.126        by (simp add: ti)
   2.127      finally have ?case . }
   2.128    ultimately show ?case by blast 
   2.129  next
   2.130 -  case (6 c e)  
   2.131 +  case (6 c e)
   2.132    then have cp: "c > 0" and nb: "numbound0 e" by auto
   2.133    { assume kdc: "k dvd c" 
   2.134 -    from kpos have knz: "k\<noteq>0" by simp
   2.135      from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
   2.136 -    from kdc have  ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt]
   2.137 +    from kdc have  ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
   2.138        numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   2.139        numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
   2.140    moreover 
   2.141    { assume *: "\<not> k dvd c"
   2.142 -    from kpos have knz: "k\<noteq>0" by simp
   2.143      from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
   2.144      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)"
   2.145 -      using real_of_int_div[OF knz kdt]
   2.146 +      using real_of_int_div[OF kdt]
   2.147          numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   2.148          numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
   2.149        by (simp add: ti algebra_simps)
   2.150      also have "\<dots> = (?I ?tk (Le (CN 0 c e)))"
   2.151        using pos_le_divide_eq[OF kpos,
   2.152            where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric]
   2.153 -        real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   2.154 +        real_of_int_div[OF kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   2.155          numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
   2.156        by (simp add: ti)
   2.157      finally have ?case . }
   2.158 @@ -2947,24 +2938,22 @@
   2.159    case (7 c e) 
   2.160    then have cp: "c > 0" and nb: "numbound0 e" by auto
   2.161    { assume kdc: "k dvd c" 
   2.162 -    from kpos have knz: "k\<noteq>0" by simp
   2.163      from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
   2.164 -    from kdc have  ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt]
   2.165 +    from kdc have  ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
   2.166        numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   2.167        numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
   2.168    moreover 
   2.169    { assume *: "\<not> k dvd c"
   2.170 -    from kpos have knz: "k\<noteq>0" by simp
   2.171      from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
   2.172      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)"
   2.173 -      using real_of_int_div[OF knz kdt]
   2.174 +      using real_of_int_div[OF kdt]
   2.175          numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   2.176          numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
   2.177        by (simp add: ti algebra_simps)
   2.178      also have "\<dots> = (?I ?tk (Gt (CN 0 c e)))"
   2.179        using pos_divide_less_eq[OF kpos,
   2.180            where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric]
   2.181 -        real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   2.182 +        real_of_int_div[OF kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   2.183          numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
   2.184        by (simp add: ti)
   2.185      finally have ?case . }
   2.186 @@ -2973,24 +2962,22 @@
   2.187    case (8 c e)  
   2.188    then have cp: "c > 0" and nb: "numbound0 e" by auto
   2.189    { assume kdc: "k dvd c" 
   2.190 -    from kpos have knz: "k\<noteq>0" by simp
   2.191      from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
   2.192 -    from kdc have  ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt]
   2.193 +    from kdc have  ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
   2.194        numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   2.195        numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
   2.196    moreover 
   2.197    { assume *: "\<not> k dvd c"
   2.198 -    from kpos have knz: "k\<noteq>0" by simp
   2.199      from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
   2.200      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)"
   2.201 -      using real_of_int_div[OF knz kdt]
   2.202 +      using real_of_int_div[OF kdt]
   2.203          numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   2.204          numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
   2.205        by (simp add: ti algebra_simps)
   2.206      also have "\<dots> = (?I ?tk (Ge (CN 0 c e)))"
   2.207        using pos_divide_le_eq[OF kpos,
   2.208            where a="real c * (?N (real x) t / real k) + ?N (real x) e" and b="0", symmetric]
   2.209 -        real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   2.210 +        real_of_int_div[OF kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   2.211          numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
   2.212        by (simp add: ti)
   2.213      finally have ?case . }
   2.214 @@ -2999,9 +2986,8 @@
   2.215    case (9 i c e)
   2.216    then have cp: "c > 0" and nb: "numbound0 e" by auto
   2.217    { assume kdc: "k dvd c" 
   2.218 -    from kpos have knz: "k\<noteq>0" by simp
   2.219      from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
   2.220 -    from kdc have ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt]
   2.221 +    from kdc have ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
   2.222        numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   2.223        numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
   2.224    moreover 
   2.225 @@ -3009,13 +2995,13 @@
   2.226      from kpos have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
   2.227      from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
   2.228      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)"
   2.229 -      using real_of_int_div[OF knz kdt]
   2.230 +      using real_of_int_div[OF kdt]
   2.231          numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   2.232          numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
   2.233        by (simp add: ti algebra_simps)
   2.234      also have "\<dots> = (?I ?tk (Dvd i (CN 0 c e)))"
   2.235        using rdvd_mult[OF knz, where n="i"]
   2.236 -        real_of_int_div[OF knz kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   2.237 +        real_of_int_div[OF kdt] numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   2.238          numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
   2.239        by (simp add: ti)
   2.240      finally have ?case . }
   2.241 @@ -3024,9 +3010,8 @@
   2.242    case (10 i c e)
   2.243    then have cp: "c > 0" and nb: "numbound0 e" by auto
   2.244    { assume kdc: "k dvd c" 
   2.245 -    from kpos have knz: "k\<noteq>0" by simp
   2.246      from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
   2.247 -    from kdc have  ?case using real_of_int_div[OF knz kdc] real_of_int_div[OF knz kdt]
   2.248 +    from kdc have  ?case using real_of_int_div[OF kdc] real_of_int_div[OF kdt]
   2.249        numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   2.250        numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"] by (simp add: ti) } 
   2.251    moreover 
   2.252 @@ -3034,12 +3019,12 @@
   2.253      from kpos have knz: "k\<noteq>0" by simp hence knz': "real k \<noteq> 0" by simp
   2.254      from tint have ti: "real (floor (?N (real x) t)) = ?N (real x) t" using isint_def by simp
   2.255      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))"
   2.256 -      using real_of_int_div[OF knz kdt]
   2.257 +      using real_of_int_div[OF kdt]
   2.258          numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   2.259          numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
   2.260        by (simp add: ti algebra_simps)
   2.261      also have "\<dots> = (?I ?tk (NDvd i (CN 0 c e)))"
   2.262 -      using rdvd_mult[OF knz, where n="i"] real_of_int_div[OF knz kdt]
   2.263 +      using rdvd_mult[OF knz, where n="i"] real_of_int_div[OF kdt]
   2.264          numbound0_I[OF tnb, where bs="bs" and b="b'" and b'="real x"]
   2.265          numbound0_I[OF nb, where bs="bs" and b="?tk" and b'="real x"]
   2.266        by (simp add: ti)
     3.1 --- a/src/HOL/Library/Float.thy	Sat Feb 25 09:07:37 2012 +0100
     3.2 +++ b/src/HOL/Library/Float.thy	Sat Feb 25 09:07:39 2012 +0100
     3.3 @@ -670,7 +670,7 @@
     3.4    let ?l = "nat (int prec + bitlen y - bitlen x)" let ?X = "x * 2^?l"
     3.5    show ?thesis 
     3.6    proof (cases "?X mod y = 0")
     3.7 -    case True hence "y \<noteq> 0" and "y dvd ?X" using `0 < y` by auto
     3.8 +    case True hence "y dvd ?X" using `0 < y` by auto
     3.9      from real_of_int_div[OF this]
    3.10      have "real (?X div y) * inverse (2 ^ ?l) = real ?X / real y * inverse (2 ^ ?l)" by auto
    3.11      also have "\<dots> = real x / real y * (2^?l * inverse (2^?l))" by auto
    3.12 @@ -702,7 +702,7 @@
    3.13    let ?l = "nat (int n + bitlen y - bitlen x)" let ?X = "x * 2^?l"
    3.14    show ?thesis
    3.15    proof (cases "?X mod y = 0")
    3.16 -    case True hence "y \<noteq> 0" and "y dvd ?X" using `0 < y` by auto
    3.17 +    case True hence "y dvd ?X" using `0 < y` by auto
    3.18      from real_of_int_div[OF this]
    3.19      have "real (?X div y) * inverse (2 ^ ?l) = real ?X / real y * inverse (2 ^ ?l)" by auto
    3.20      also have "\<dots> = real x / real y * (2^?l * inverse (2^?l))" by auto
    3.21 @@ -757,7 +757,7 @@
    3.22    let ?l = "nat (int n + bitlen y - bitlen x)" let ?X = "x * 2^?l"
    3.23    show ?thesis
    3.24    proof (cases "?X mod y = 0")
    3.25 -    case True hence "y \<noteq> 0" and "y dvd ?X" using `0 < y` by auto
    3.26 +    case True hence "y dvd ?X" using `0 < y` by auto
    3.27      from real_of_int_div[OF this]
    3.28      have "real (?X div y) * inverse (2 ^ ?l) = real ?X / real y * inverse (2 ^ ?l)" by auto
    3.29      also have "\<dots> = real x / real y * (2^?l * inverse (2^?l))" by auto
     4.1 --- a/src/HOL/RealDef.thy	Sat Feb 25 09:07:37 2012 +0100
     4.2 +++ b/src/HOL/RealDef.thy	Sat Feb 25 09:07:39 2012 +0100
     4.3 @@ -1184,10 +1184,9 @@
     4.4    apply simp
     4.5  done
     4.6  
     4.7 -lemma real_of_int_div_aux: "d ~= 0 ==> (real (x::int)) / (real d) = 
     4.8 +lemma real_of_int_div_aux: "(real (x::int)) / (real d) = 
     4.9      real (x div d) + (real (x mod d)) / (real d)"
    4.10  proof -
    4.11 -  assume d: "d ~= 0"
    4.12    have "x = (x div d) * d + x mod d"
    4.13      by auto
    4.14    then have "real x = real (x div d) * real d + real(x mod d)"
    4.15 @@ -1195,12 +1194,12 @@
    4.16    then have "real x / real d = ... / real d"
    4.17      by simp
    4.18    then show ?thesis
    4.19 -    by (auto simp add: add_divide_distrib algebra_simps d)
    4.20 +    by (auto simp add: add_divide_distrib algebra_simps)
    4.21  qed
    4.22  
    4.23 -lemma real_of_int_div: "(d::int) ~= 0 ==> d dvd n ==>
    4.24 +lemma real_of_int_div: "(d :: int) dvd n ==>
    4.25      real(n div d) = real n / real d"
    4.26 -  apply (frule real_of_int_div_aux [of d n])
    4.27 +  apply (subst real_of_int_div_aux)
    4.28    apply simp
    4.29    apply (simp add: dvd_eq_mod_eq_0)
    4.30  done
    4.31 @@ -1213,34 +1212,20 @@
    4.32    apply (simp add: algebra_simps)
    4.33    apply (subst real_of_int_div_aux)
    4.34    apply simp
    4.35 -  apply simp
    4.36    apply (subst zero_le_divide_iff)
    4.37    apply auto
    4.38    apply (simp add: algebra_simps)
    4.39    apply (subst real_of_int_div_aux)
    4.40    apply simp
    4.41 -  apply simp
    4.42    apply (subst zero_le_divide_iff)
    4.43    apply auto
    4.44  done
    4.45  
    4.46  lemma real_of_int_div3:
    4.47    "real (n::int) / real (x) - real (n div x) <= 1"
    4.48 -  apply(case_tac "x = 0")
    4.49 -  apply simp
    4.50    apply (simp add: algebra_simps)
    4.51    apply (subst real_of_int_div_aux)
    4.52 -  apply assumption
    4.53 -  apply simp
    4.54 -  apply (subst divide_le_eq)
    4.55 -  apply clarsimp
    4.56 -  apply (rule conjI)
    4.57 -  apply (rule impI)
    4.58 -  apply (rule order_less_imp_le)
    4.59 -  apply simp
    4.60 -  apply (rule impI)
    4.61 -  apply (rule order_less_imp_le)
    4.62 -  apply simp
    4.63 +  apply (auto simp add: divide_le_eq intro: order_less_imp_le)
    4.64  done
    4.65  
    4.66  lemma real_of_int_div4: "real (n div x) <= real (n::int) / real x" 
    4.67 @@ -1337,10 +1322,9 @@
    4.68    apply (simp add: real_of_nat_Suc)
    4.69  done
    4.70  
    4.71 -lemma real_of_nat_div_aux: "0 < d ==> (real (x::nat)) / (real d) = 
    4.72 +lemma real_of_nat_div_aux: "(real (x::nat)) / (real d) = 
    4.73      real (x div d) + (real (x mod d)) / (real d)"
    4.74  proof -
    4.75 -  assume d: "0 < d"
    4.76    have "x = (x div d) * d + x mod d"
    4.77      by auto
    4.78    then have "real x = real (x div d) * real d + real(x mod d)"
    4.79 @@ -1348,24 +1332,18 @@
    4.80    then have "real x / real d = \<dots> / real d"
    4.81      by simp
    4.82    then show ?thesis
    4.83 -    by (auto simp add: add_divide_distrib algebra_simps d)
    4.84 +    by (auto simp add: add_divide_distrib algebra_simps)
    4.85  qed
    4.86  
    4.87 -lemma real_of_nat_div: "0 < (d::nat) ==> d dvd n ==>
    4.88 +lemma real_of_nat_div: "(d :: nat) dvd n ==>
    4.89      real(n div d) = real n / real d"
    4.90 -  apply (frule real_of_nat_div_aux [of d n])
    4.91 -  apply simp
    4.92 -  apply (subst dvd_eq_mod_eq_0 [THEN sym])
    4.93 -  apply assumption
    4.94 -done
    4.95 +  by (subst real_of_nat_div_aux)
    4.96 +    (auto simp add: dvd_eq_mod_eq_0 [symmetric])
    4.97  
    4.98  lemma real_of_nat_div2:
    4.99    "0 <= real (n::nat) / real (x) - real (n div x)"
   4.100 -apply(case_tac "x = 0")
   4.101 - apply (simp)
   4.102  apply (simp add: algebra_simps)
   4.103  apply (subst real_of_nat_div_aux)
   4.104 - apply simp
   4.105  apply simp
   4.106  apply (subst zero_le_divide_iff)
   4.107  apply simp
   4.108 @@ -1377,7 +1355,6 @@
   4.109  apply (simp)
   4.110  apply (simp add: algebra_simps)
   4.111  apply (subst real_of_nat_div_aux)
   4.112 - apply simp
   4.113  apply simp
   4.114  done
   4.115