# HG changeset patch
# User bulwahn
# Date 1341224610 -7200
# Node ID 18461f745b4ade384a225efcf1d80276c90e3961
# Parent  0192811f0a961ece1b2ef8cbc05764716d33b88b
adding some minimal documentation and an example of quickcheck's interfaces

diff -r 0192811f0a96 -r 18461f745b4a src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Jul 02 11:45:19 2012 +0200
+++ b/src/HOL/IsaMakefile	Mon Jul 02 12:23:30 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 0192811f0a96 -r 18461f745b4a 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	Mon Jul 02 12:23:30 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 0192811f0a96 -r 18461f745b4a src/HOL/Quickcheck_Examples/ROOT.ML
--- a/src/HOL/Quickcheck_Examples/ROOT.ML	Mon Jul 02 11:45:19 2012 +0200
+++ b/src/HOL/Quickcheck_Examples/ROOT.ML	Mon Jul 02 12:23:30 2012 +0200
@@ -2,7 +2,8 @@
   "Find_Unused_Assms_Examples",
   "Quickcheck_Examples",
   "Quickcheck_Lattice_Examples",
-  "Completeness"
+  "Completeness",
+  "Quickcheck_Interfaces"
 ];
 
 if getenv "ISABELLE_GHC" = "" then ()