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 huffman
Wed, 18 Apr 2012 15:48:32 +0200
changeset 47544 e455cdaac479
parent 46950 d0181abdbdac
child 48891 c0eafbd55de3
permissions -rw-r--r--
move constant 'Respects' into Lifting.thy; add quantifier transfer rules for quotients
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








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






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