author | bulwahn |
Tue, 02 Mar 2010 22:13:33 +0100 | |
changeset 35537 | 59dd6be5834c |
parent 35324 | c9f428269b38 |
child 35951 | 5ad0af66b3c6 |
permissions | -rw-r--r-- |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
1 |
(* Author: Lukas Bulwahn, TU Muenchen *) |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
2 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
3 |
header {* A Prototype of Quickcheck based on the Predicate Compiler *} |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
4 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
5 |
theory Predicate_Compile_Quickcheck |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
6 |
imports "../Predicate_Compile" Quickcheck Predicate_Compile_Alternative_Defs |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
7 |
uses "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML" |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
8 |
begin |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
9 |
|
35537
59dd6be5834c
adding depth to predicate compile quickcheck for mutabelle tests; removing obsolete references in predicate compile quickcheck
bulwahn
parents:
35324
diff
changeset
|
10 |
setup {* Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term false true 8) *} |
59dd6be5834c
adding depth to predicate compile quickcheck for mutabelle tests; removing obsolete references in predicate compile quickcheck
bulwahn
parents:
35324
diff
changeset
|
11 |
setup {* Quickcheck.add_generator ("predicate_compile_ff_fs", Predicate_Compile_Quickcheck.quickcheck_compile_term true true 8) *} |
59dd6be5834c
adding depth to predicate compile quickcheck for mutabelle tests; removing obsolete references in predicate compile quickcheck
bulwahn
parents:
35324
diff
changeset
|
12 |
setup {* Quickcheck.add_generator ("predicate_compile_ff_nofs", Predicate_Compile_Quickcheck.quickcheck_compile_term true false 8) *} |
35324
c9f428269b38
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents:
34948
diff
changeset
|
13 |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33250
diff
changeset
|
14 |
(* |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33250
diff
changeset
|
15 |
datatype alphabet = a | b |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
16 |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33250
diff
changeset
|
17 |
inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33250
diff
changeset
|
18 |
"[] \<in> S\<^isub>1" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33250
diff
changeset
|
19 |
| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33250
diff
changeset
|
20 |
| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33250
diff
changeset
|
21 |
| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33250
diff
changeset
|
22 |
| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33250
diff
changeset
|
23 |
| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33250
diff
changeset
|
24 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33250
diff
changeset
|
25 |
ML {* set Toplevel.debug *} |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33250
diff
changeset
|
26 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33250
diff
changeset
|
27 |
declare mem_def[code_pred_inline] Collect_def[code_pred_inline] |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33250
diff
changeset
|
28 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33250
diff
changeset
|
29 |
lemma |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33250
diff
changeset
|
30 |
"w \<in> S\<^isub>1p \<Longrightarrow> w = []" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33250
diff
changeset
|
31 |
quickcheck[generator = predicate_compile, iterations=1] |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33250
diff
changeset
|
32 |
oops |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33250
diff
changeset
|
33 |
|
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33250
diff
changeset
|
34 |
theorem S\<^isub>1_sound: |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33250
diff
changeset
|
35 |
"w \<in> S\<^isub>1p \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]" |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33250
diff
changeset
|
36 |
quickcheck[generator=predicate_compile, size=15] |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33250
diff
changeset
|
37 |
oops |
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33250
diff
changeset
|
38 |
*) |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
39 |
end |