src/HOL/Quickcheck_Examples/Quickcheck_Interfaces.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 63167 0909deb8059b
child 69597 ff784d5a5bfb
permissions -rw-r--r--
executable domain membership checks
bulwahn@48179
     1
theory Quickcheck_Interfaces
bulwahn@48179
     2
imports Main
bulwahn@48179
     3
begin
bulwahn@48179
     4
wenzelm@63167
     5
subsection \<open>Checking a single proposition (TODO)\<close>
bulwahn@48179
     6
wenzelm@63167
     7
subsection \<open>Checking multiple propositions in one batch\<close>
bulwahn@48179
     8
wenzelm@63167
     9
text \<open>
bulwahn@48179
    10
bulwahn@48179
    11
First, this requires to setup special generators for all datatypes via the following command.
wenzelm@63167
    12
\<close>
bulwahn@48179
    13
wenzelm@58813
    14
setup Exhaustive_Generators.setup_bounded_forall_datatype_interpretation
bulwahn@48179
    15
wenzelm@63167
    16
text \<open>
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.
wenzelm@63167
    19
\<close>
bulwahn@48179
    20
wenzelm@63167
    21
ML \<open>
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)"}]
wenzelm@63167
    24
\<close>
bulwahn@48179
    25
wenzelm@63167
    26
text \<open>
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:
wenzelm@63167
    30
\<close>
bulwahn@48179
    31
wenzelm@63167
    32
ML \<open>
bulwahn@48179
    33
fun check_upto f i j = if i > j then true else f i andalso check_upto f (i + 1) j
wenzelm@63167
    34
\<close>
bulwahn@48179
    35
wenzelm@63167
    36
ML_val \<open>
bulwahn@48179
    37
  map (fn test => check_upto test 0 1) testers
wenzelm@63167
    38
\<close>
wenzelm@63167
    39
ML_val \<open>
bulwahn@48179
    40
  map (fn test => check_upto test 0 2) testers
wenzelm@63167
    41
\<close>
wenzelm@63167
    42
ML_val \<open>
bulwahn@48179
    43
  map (fn test => check_upto test 0 3) testers
wenzelm@63167
    44
\<close>
wenzelm@63167
    45
ML_val \<open>
bulwahn@48179
    46
  map (fn test => check_upto test 0 7) testers
wenzelm@63167
    47
\<close>
bulwahn@48179
    48
wenzelm@63167
    49
text \<open>Note that all conjectures must be executable to obtain the testers with the function above.\<close>
bulwahn@48179
    50
bulwahn@48179
    51
bulwahn@48179
    52
end