# HG changeset patch
# User bulwahn
# Date 1341316572 -7200
# Node ID 54fd394248aaf4420575074d445c29dd9b3297da
# Parent  18461f745b4ade384a225efcf1d80276c90e3961# Parent  5016a36205fac50cfcdecb011c3354d4b5a6b489
merged

diff -r 5016a36205fa -r 54fd394248aa src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Jul 03 09:31:41 2012 +0200
+++ b/src/HOL/IsaMakefile	Tue Jul 03 13:56:12 2012 +0200
@@ -1499,9 +1499,10 @@
 HOL-Quickcheck_Examples: HOL $(LOG)/HOL-Quickcheck_Examples.gz
 
 $(LOG)/HOL-Quickcheck_Examples.gz: $(OUT)/HOL				\
-  Quickcheck_Examples/Completeness.thy			\
+  Quickcheck_Examples/Completeness.thy					\
   Quickcheck_Examples/Find_Unused_Assms_Examples.thy			\
   Quickcheck_Examples/Quickcheck_Examples.thy				\
+  Quickcheck_Examples/Quickcheck_Interfaces.thy				\
   Quickcheck_Examples/Quickcheck_Lattice_Examples.thy			\
   Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quickcheck_Examples
diff -r 5016a36205fa -r 54fd394248aa src/HOL/Quickcheck_Examples/Quickcheck_Interfaces.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Interfaces.thy	Tue Jul 03 13:56:12 2012 +0200
@@ -0,0 +1,52 @@
+theory Quickcheck_Interfaces
+imports Main
+begin
+
+subsection {* Checking a single proposition (TODO) *}
+
+subsection {* Checking multiple propositions in one batch *}
+
+text {*
+
+First, this requires to setup special generators for all datatypes via the following command.
+*}
+
+setup {* Exhaustive_Generators.setup_bounded_forall_datatype_interpretation *}
+
+text {*
+Now, the function Quickcheck.mk_batch_validator : Proof.context -> term list -> (int -> bool) list option
+takes formulas of type bool with free variables, and returns a list of testing functions.
+*}
+
+ML {*
+val SOME testers = Quickcheck.mk_batch_validator @{context}
+  [@{term "x = (1 :: nat)"}, @{term "x = (0 :: nat)"}, @{term "x <= (5 :: nat)"}, @{term "0 \<le> (x :: nat)"}]
+*}
+
+text {*
+It is upto the user with which strategy the conjectures should be tested.
+For example, one could check all conjectures up to a given size, and check the different conjectures in sequence.
+This is implemented by:
+*}
+
+ML {*
+fun check_upto f i j = if i > j then true else f i andalso check_upto f (i + 1) j
+*}
+
+ML {* 
+  map (fn test => check_upto test 0 1) testers
+*}
+ML {* 
+  map (fn test => check_upto test 0 2) testers
+*}
+ML {* 
+  map (fn test => check_upto test 0 3) testers
+*}
+ML {* 
+  map (fn test => check_upto test 0 7) testers
+*}
+
+text {* Note that all conjectures must be executable to obtain the testers with the function above. *}
+
+
+end
diff -r 5016a36205fa -r 54fd394248aa src/HOL/Quickcheck_Examples/ROOT.ML
--- a/src/HOL/Quickcheck_Examples/ROOT.ML	Tue Jul 03 09:31:41 2012 +0200
+++ b/src/HOL/Quickcheck_Examples/ROOT.ML	Tue Jul 03 13:56:12 2012 +0200
@@ -2,7 +2,8 @@
   "Find_Unused_Assms_Examples",
   "Quickcheck_Examples",
   "Quickcheck_Lattice_Examples",
-  "Completeness"
+  "Completeness",
+  "Quickcheck_Interfaces"
 ];
 
 if getenv "ISABELLE_GHC" = "" then ()
diff -r 5016a36205fa -r 54fd394248aa src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue Jul 03 09:31:41 2012 +0200
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue Jul 03 13:56:12 2012 +0200
@@ -20,6 +20,7 @@
   val optimise_equality : bool Config.T
   val quickcheck_pretty : bool Config.T
   val setup_exhaustive_datatype_interpretation : theory -> theory
+  val setup_bounded_forall_datatype_interpretation : theory -> theory
   val setup: theory -> theory
   
   val instantiate_full_exhaustive_datatype : Datatype_Aux.config -> Datatype_Aux.descr ->
@@ -564,6 +565,11 @@
 val setup_exhaustive_datatype_interpretation =
   Quickcheck_Common.datatype_interpretation (@{sort exhaustive}, instantiate_exhaustive_datatype)
 
+val setup_bounded_forall_datatype_interpretation =
+  Datatype.interpretation (Quickcheck_Common.ensure_sort
+    (((@{sort type}, @{sort type}), @{sort bounded_forall}),
+    (Datatype.the_descr, instantiate_bounded_forall_datatype)))
+
 val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true);
 
 val setup =