src/HOL/Quickcheck_Examples/Quickcheck_Interfaces.thy
author wenzelm
Fri Mar 07 22:30:58 2014 +0100 (2014-03-07)
changeset 55990 41c6b99c5fb7
parent 51272 9c8d63b4b6be
child 58148 9764b994a421
permissions -rw-r--r--
more antiquotations;
     1 theory Quickcheck_Interfaces
     2 imports Main
     3 begin
     4 
     5 subsection {* Checking a single proposition (TODO) *}
     6 
     7 subsection {* Checking multiple propositions in one batch *}
     8 
     9 text {*
    10 
    11 First, this requires to setup special generators for all datatypes via the following command.
    12 *}
    13 
    14 setup {* Exhaustive_Generators.setup_bounded_forall_datatype_interpretation *}
    15 
    16 text {*
    17 Now, the function Quickcheck.mk_batch_validator : Proof.context -> term list -> (int -> bool) list option
    18 takes formulas of type bool with free variables, and returns a list of testing functions.
    19 *}
    20 
    21 ML {*
    22 val SOME testers = Quickcheck.mk_batch_validator @{context}
    23   [@{term "x = (1 :: nat)"}, @{term "x = (0 :: nat)"}, @{term "x <= (5 :: nat)"}, @{term "0 \<le> (x :: nat)"}]
    24 *}
    25 
    26 text {*
    27 It is upto the user with which strategy the conjectures should be tested.
    28 For example, one could check all conjectures up to a given size, and check the different conjectures in sequence.
    29 This is implemented by:
    30 *}
    31 
    32 ML {*
    33 fun check_upto f i j = if i > j then true else f i andalso check_upto f (i + 1) j
    34 *}
    35 
    36 ML_val {* 
    37   map (fn test => check_upto test 0 1) testers
    38 *}
    39 ML_val {* 
    40   map (fn test => check_upto test 0 2) testers
    41 *}
    42 ML_val {* 
    43   map (fn test => check_upto test 0 3) testers
    44 *}
    45 ML_val {* 
    46   map (fn test => check_upto test 0 7) testers
    47 *}
    48 
    49 text {* Note that all conjectures must be executable to obtain the testers with the function above. *}
    50 
    51 
    52 end