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
```