author | huffman |
Fri, 30 Mar 2012 15:43:30 +0200 | |
changeset 47225 | 650318981557 |
parent 46950 | d0181abdbdac |
child 48891 | c0eafbd55de3 |
permissions | -rw-r--r-- |
33265 | 1 |
(* Title: HOL/Predicate_Compile.thy |
2 |
Author: Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen |
|
3 |
*) |
|
33250
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 |
header {* A compiler for predicates defined by introduction rules *} |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
6 |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
7 |
theory Predicate_Compile |
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
8 |
imports Predicate New_Random_Sequence Quickcheck_Exhaustive |
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
46664
diff
changeset
|
9 |
keywords "code_pred" :: thy_goal and "values" :: diag |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
10 |
uses |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
11 |
"Tools/Predicate_Compile/predicate_compile_aux.ML" |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
36032
diff
changeset
|
12 |
"Tools/Predicate_Compile/predicate_compile_compilations.ML" |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
36046
diff
changeset
|
13 |
"Tools/Predicate_Compile/core_data.ML" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
36046
diff
changeset
|
14 |
"Tools/Predicate_Compile/mode_inference.ML" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
36046
diff
changeset
|
15 |
"Tools/Predicate_Compile/predicate_compile_proof.ML" |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
16 |
"Tools/Predicate_Compile/predicate_compile_core.ML" |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
17 |
"Tools/Predicate_Compile/predicate_compile_data.ML" |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
18 |
"Tools/Predicate_Compile/predicate_compile_fun.ML" |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
19 |
"Tools/Predicate_Compile/predicate_compile_pred.ML" |
36032
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
36021
diff
changeset
|
20 |
"Tools/Predicate_Compile/predicate_compile_specialisation.ML" |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
21 |
"Tools/Predicate_Compile/predicate_compile.ML" |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
22 |
begin |
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
23 |
|
33265 | 24 |
setup Predicate_Compile.setup |
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff
changeset
|
25 |
|
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
33265
diff
changeset
|
26 |
end |