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