--- a/src/HOL/Library/Quickcheck_Types.thy Mon Nov 22 11:34:59 2010 +0100
+++ b/src/HOL/Library/Quickcheck_Types.thy Mon Nov 22 11:35:00 2010 +0100
@@ -460,7 +460,7 @@
section {* Quickcheck configuration *}
-quickcheck_params[default_type = ["int", "non_distrib_lattice", "int bot", "int top", "int flat_complete_lattice"]]
+quickcheck_params[finite_types = false, default_type = ["int", "non_distrib_lattice", "int bot", "int top", "int flat_complete_lattice"]]
hide_type non_distrib_lattice flat_complete_lattice bot top
--- a/src/HOL/ex/Quickcheck_Examples.thy Mon Nov 22 11:34:59 2010 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy Mon Nov 22 11:35:00 2010 +0100
@@ -11,9 +11,14 @@
text {*
The 'quickcheck' command allows to find counterexamples by evaluating
-formulae under an assignment of free variables to random values.
-In contrast to 'refute', it can deal with inductive datatypes,
-but cannot handle quantifiers.
+formulae.
+Currently, there are two different exploration schemes:
+- random testing: this is incomplete, but explores the search space faster.
+- exhaustive testing: this is complete, but increasing the depth leads to
+ exponentially many assignments.
+
+quickcheck can handle quantifiers on finite universes.
+
*}
subsection {* Lists *}
@@ -229,4 +234,22 @@
quickcheck[generator = small, expect = counterexample]
oops
+section {* Examples with quantifiers *}
+
+text {*
+ These examples show that we can handle quantifiers.
+*}
+
+lemma "(\<exists>x. P x) \<longrightarrow> (\<forall>x. P x)"
+ quickcheck[expect = counterexample]
+oops
+
+lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)"
+ quickcheck[expect = counterexample]
+oops
+
+lemma "(\<exists>x. P x) \<longrightarrow> (EX! x. P x)"
+ quickcheck[expect = counterexample]
+oops
+
end