--- 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
--- /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
--- 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 ()
--- 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 =