Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Predicate_Compile.thy
author haftmann
Thu, 14 Feb 2013 15:27:10 +0100
changeset 51126 df86080de4cb
parent 50055 94041d602ecb
child 52023 b477be38a7bb
permissions -rw-r--r--
reform of predicate compiler / quickcheck theories: implement yieldn operations uniformly on the ML level -- predicate compiler uses negative integers as parameter to yieldn, whereas code_numeral represents natural numbers! avoid odd New_ prefix by joining related theories; avoid overcompact name DSequence; separated predicate inside random monad into separate theory; consolidated name of theory Quickcheck
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33265
01c9c6dbd890 proper headers;
wenzelm
parents: 33250
diff changeset 
     1
 
(*  Title:      HOL/Predicate_Compile.thy
01c9c6dbd890 proper headers;
wenzelm
parents: 33250
diff changeset 
     2
 
    Author:     Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen
01c9c6dbd890 proper headers;
wenzelm
parents: 33250
diff changeset 
     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








51126






df86080de4cb
reform of predicate compiler / quickcheck theories:



haftmann


parents: 
50055

diff
changeset




     8


imports 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


begin













5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck



bulwahn


parents: 

diff
changeset




    11









48891






c0eafbd55de3
prefer ML_file over old uses;



wenzelm


parents: 
46950

diff
changeset




    12


ML_file "Tools/Predicate_Compile/predicate_compile_aux.ML"













c0eafbd55de3
prefer ML_file over old uses;



wenzelm


parents: 
46950

diff
changeset




    13


ML_file "Tools/Predicate_Compile/predicate_compile_compilations.ML"













c0eafbd55de3
prefer ML_file over old uses;



wenzelm


parents: 
46950

diff
changeset




    14


ML_file "Tools/Predicate_Compile/core_data.ML"













c0eafbd55de3
prefer ML_file over old uses;



wenzelm


parents: 
46950

diff
changeset




    15


ML_file "Tools/Predicate_Compile/mode_inference.ML"













c0eafbd55de3
prefer ML_file over old uses;



wenzelm


parents: 
46950

diff
changeset




    16


ML_file "Tools/Predicate_Compile/predicate_compile_proof.ML"













c0eafbd55de3
prefer ML_file over old uses;



wenzelm


parents: 
46950

diff
changeset




    17


ML_file "Tools/Predicate_Compile/predicate_compile_core.ML"













c0eafbd55de3
prefer ML_file over old uses;



wenzelm


parents: 
46950

diff
changeset




    18


ML_file "Tools/Predicate_Compile/predicate_compile_data.ML"













c0eafbd55de3
prefer ML_file over old uses;



wenzelm


parents: 
46950

diff
changeset




    19


ML_file "Tools/Predicate_Compile/predicate_compile_fun.ML"













c0eafbd55de3
prefer ML_file over old uses;



wenzelm


parents: 
46950

diff
changeset




    20


ML_file "Tools/Predicate_Compile/predicate_compile_pred.ML"













c0eafbd55de3
prefer ML_file over old uses;



wenzelm


parents: 
46950

diff
changeset




    21


ML_file "Tools/Predicate_Compile/predicate_compile_specialisation.ML"













c0eafbd55de3
prefer ML_file over old uses;



wenzelm


parents: 
46950

diff
changeset




    22


ML_file "Tools/Predicate_Compile/predicate_compile.ML"













c0eafbd55de3
prefer ML_file over old uses;



wenzelm


parents: 
46950

diff
changeset




    23









33265






01c9c6dbd890
proper headers;



wenzelm


parents: 
33250

diff
changeset




    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















isabelle