author  wenzelm 
Wed, 29 Oct 2014 11:19:27 +0100  
changeset 58813  625d04d4fd2a 
parent 58148  9764b994a421 
child 63167  0909deb8059b 
permissions  rwrr 
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  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  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  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  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  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  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 