# HG changeset patch
# User bulwahn
# Date 1290422100 -3600
# Node ID a716071ec30664c365f2f0ba9e2b1d1e9db9513c
# Parent  d921c97bdbd8e0a942ca6fffd4791d56cc7a1be9
adapting the quickcheck examples

diff -r d921c97bdbd8 -r a716071ec306 src/HOL/Library/Quickcheck_Types.thy
--- 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
 
diff -r d921c97bdbd8 -r a716071ec306 src/HOL/ex/Quickcheck_Examples.thy
--- 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