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