--- 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)
--- 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