--- a/src/HOL/Decision_Procs/Ferrack.thy Sat Feb 25 13:17:38 2012 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy Sat Feb 25 15:33:36 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 }
--- a/src/HOL/Decision_Procs/MIR.thy Sat Feb 25 13:17:38 2012 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy Sat Feb 25 15:33:36 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/Library/Float.thy Sat Feb 25 13:17:38 2012 +0100
+++ b/src/HOL/Library/Float.thy Sat Feb 25 15:33:36 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
--- a/src/HOL/List.thy Sat Feb 25 13:17:38 2012 +0100
+++ b/src/HOL/List.thy Sat Feb 25 15:33:36 2012 +0100
@@ -2342,12 +2342,8 @@
by (simp add: list_all2_conv_all_nth)
lemma list_all2_update_cong:
- "\<lbrakk> i<size xs; list_all2 P xs ys; P x y \<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
-by (simp add: list_all2_conv_all_nth nth_list_update)
-
-lemma list_all2_update_cong2:
- "\<lbrakk>list_all2 P xs ys; P x y; i < length ys\<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
-by (simp add: list_all2_lengthD list_all2_update_cong)
+ "\<lbrakk> list_all2 P xs ys; P x y \<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
+by (cases "i < length ys") (auto simp add: list_all2_conv_all_nth nth_list_update)
lemma list_all2_takeI [simp,intro?]:
"list_all2 P xs ys \<Longrightarrow> list_all2 P (take n xs) (take n ys)"
--- a/src/HOL/Probability/Lebesgue_Integration.thy Sat Feb 25 13:17:38 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Sat Feb 25 15:33:36 2012 +0100
@@ -366,7 +366,7 @@
also have "\<dots> \<le> natfloor (real (u x) * 2 ^ i * 2)"
proof cases
assume "0 \<le> u x" then show ?thesis
- by (intro le_mult_natfloor) (cases "u x", auto intro!: mult_nonneg_nonneg)
+ by (intro le_mult_natfloor)
next
assume "\<not> 0 \<le> u x" then show ?thesis
by (cases "u x") (auto simp: natfloor_neg mult_nonpos_nonneg)
--- a/src/HOL/Quickcheck_Examples/Find_Unused_Assms_Examples.thy Sat Feb 25 13:17:38 2012 +0100
+++ b/src/HOL/Quickcheck_Examples/Find_Unused_Assms_Examples.thy Sat Feb 25 15:33:36 2012 +0100
@@ -1,5 +1,5 @@
theory Find_Unused_Assms_Examples
-imports Main
+imports Complex_Main
begin
section {* Arithmetics *}
@@ -8,7 +8,8 @@
find_unused_assms Divides
find_unused_assms GCD
-find_unused_assms MacLaurin
+find_unused_assms RealDef
+find_unused_assms RComplete
section {* Set Theory *}
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Sat Feb 25 13:17:38 2012 +0100
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Sat Feb 25 15:33:36 2012 +0100
@@ -245,6 +245,15 @@
quickcheck[exhaustive, expect = counterexample]
oops
+subsection {* Random Testing beats Exhaustive Testing *}
+
+lemma mult_inj_if_coprime_nat:
+ "inj_on f A \<Longrightarrow> inj_on g B
+ \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
+quickcheck[exhaustive]
+quickcheck[random]
+oops
+
subsection {* Examples with quantifiers *}
text {*
--- a/src/HOL/RComplete.thy Sat Feb 25 13:17:38 2012 +0100
+++ b/src/HOL/RComplete.thy Sat Feb 25 15:33:36 2012 +0100
@@ -415,10 +415,9 @@
lemma natfloor_add_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1"
by (simp add: natfloor_add [symmetric] del: One_nat_def)
-lemma natfloor_subtract [simp]: "real a <= x ==>
- natfloor(x - real a) = natfloor x - a"
- unfolding natfloor_def
- unfolding real_of_int_of_nat_eq [symmetric] floor_subtract
+lemma natfloor_subtract [simp]:
+ "natfloor(x - real a) = natfloor x - a"
+ unfolding natfloor_def real_of_int_of_nat_eq [symmetric] floor_subtract
by simp
lemma natfloor_div_nat:
@@ -441,10 +440,9 @@
qed
lemma le_mult_natfloor:
- assumes "0 \<le> (a :: real)" and "0 \<le> b"
shows "natfloor a * natfloor b \<le> natfloor (a * b)"
- using assms
- by (simp add: le_natfloor_eq mult_nonneg_nonneg mult_mono' real_natfloor_le)
+ by (cases "0 <= a & 0 <= b")
+ (auto simp add: le_natfloor_eq mult_nonneg_nonneg mult_mono' real_natfloor_le natfloor_neg)
lemma natceiling_zero [simp]: "natceiling 0 = 0"
by (unfold natceiling_def, simp)
@@ -505,10 +503,8 @@
lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1"
by (simp add: natceiling_add [symmetric] del: One_nat_def)
-lemma natceiling_subtract [simp]: "real a <= x ==>
- natceiling(x - real a) = natceiling x - a"
- unfolding natceiling_def
- unfolding real_of_int_of_nat_eq [symmetric] ceiling_subtract
+lemma natceiling_subtract [simp]: "natceiling(x - real a) = natceiling x - a"
+ unfolding natceiling_def real_of_int_of_nat_eq [symmetric] ceiling_subtract
by simp
subsection {* Exponentiation with floor *}
--- a/src/HOL/RealDef.thy Sat Feb 25 13:17:38 2012 +0100
+++ b/src/HOL/RealDef.thy Sat Feb 25 15:33:36 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
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Sat Feb 25 13:17:38 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Sat Feb 25 15:33:36 2012 +0100
@@ -187,11 +187,11 @@
let
val _ =
Quickcheck.verbose_message ctxt ("[Quickcheck-" ^ name ^ "] Test " ^
- (if size = 0 then "" else "data size: " ^ string_of_int (size - 1) ^ " and ") ^
+ (if size = 0 then "" else "data size: " ^ string_of_int size ^ " and ") ^
"cardinality: " ^ string_of_int card)
val (ts, timing) =
cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card)
- (fn () => fst (test_fun genuine_only [card, size - 1]))
+ (fn () => fst (test_fun genuine_only [card, size + 1]))
val _ = Quickcheck.add_timing timing current_result
in
Option.map (pair (card, size)) ts