equal
deleted
inserted
replaced
1 (* Author: Lukas Bulwahn, TU Muenchen *) |
1 (* Author: Lukas Bulwahn, TU Muenchen *) |
2 |
2 |
3 header {* A Prototype of Quickcheck based on the Predicate Compiler *} |
3 header {* A Prototype of Quickcheck based on the Predicate Compiler *} |
4 |
4 |
5 theory Predicate_Compile_Quickcheck |
5 theory Predicate_Compile_Quickcheck |
6 imports "../Predicate_Compile" |
6 imports "../Predicate_Compile" Quickcheck Predicate_Compile_Alternative_Defs |
7 uses "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML" |
7 uses "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML" |
8 begin |
8 begin |
9 |
9 |
10 setup {* Quickcheck.add_generator ("predicate_compile", Predicate_Compile_Quickcheck.quickcheck) *} |
10 setup {* Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term false true) *} |
|
11 setup {* Quickcheck.add_generator ("predicate_compile_ff_fs", Predicate_Compile_Quickcheck.quickcheck_compile_term true true) *} |
|
12 setup {* Quickcheck.add_generator ("predicate_compile_ff_nofs", Predicate_Compile_Quickcheck.quickcheck_compile_term true false) *} |
|
13 |
11 (* |
14 (* |
12 datatype alphabet = a | b |
15 datatype alphabet = a | b |
13 |
16 |
14 inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where |
17 inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where |
15 "[] \<in> S\<^isub>1" |
18 "[] \<in> S\<^isub>1" |