|
1 (* Title: HOL/Refute.thy |
|
2 Author: Tjark Weber |
|
3 Copyright 2003-2007 |
|
4 |
|
5 Basic setup and documentation for the 'refute' (and 'refute_params') command. |
|
6 *) |
|
7 |
|
8 header {* Refute *} |
|
9 |
|
10 theory Refute |
|
11 imports Hilbert_Choice List Sledgehammer |
|
12 keywords "refute" :: diag and "refute_params" :: thy_decl |
|
13 begin |
|
14 |
|
15 ML_file "refute.ML" |
|
16 setup Refute.setup |
|
17 |
|
18 refute_params |
|
19 [itself = 1, |
|
20 minsize = 1, |
|
21 maxsize = 8, |
|
22 maxvars = 10000, |
|
23 maxtime = 60, |
|
24 satsolver = auto, |
|
25 no_assms = false] |
|
26 |
|
27 text {* |
|
28 \small |
|
29 \begin{verbatim} |
|
30 (* ------------------------------------------------------------------------- *) |
|
31 (* REFUTE *) |
|
32 (* *) |
|
33 (* We use a SAT solver to search for a (finite) model that refutes a given *) |
|
34 (* HOL formula. *) |
|
35 (* ------------------------------------------------------------------------- *) |
|
36 |
|
37 (* ------------------------------------------------------------------------- *) |
|
38 (* NOTE *) |
|
39 (* *) |
|
40 (* I strongly recommend that you install a stand-alone SAT solver if you *) |
|
41 (* want to use 'refute'. For details see 'HOL/Tools/sat_solver.ML'. If you *) |
|
42 (* have installed (a supported version of) zChaff, simply set 'ZCHAFF_HOME' *) |
|
43 (* in 'etc/settings'. *) |
|
44 (* ------------------------------------------------------------------------- *) |
|
45 |
|
46 (* ------------------------------------------------------------------------- *) |
|
47 (* USAGE *) |
|
48 (* *) |
|
49 (* See the file 'HOL/ex/Refute_Examples.thy' for examples. The supported *) |
|
50 (* parameters are explained below. *) |
|
51 (* ------------------------------------------------------------------------- *) |
|
52 |
|
53 (* ------------------------------------------------------------------------- *) |
|
54 (* CURRENT LIMITATIONS *) |
|
55 (* *) |
|
56 (* 'refute' currently accepts formulas of higher-order predicate logic (with *) |
|
57 (* equality), including free/bound/schematic variables, lambda abstractions, *) |
|
58 (* sets and set membership, "arbitrary", "The", "Eps", records and *) |
|
59 (* inductively defined sets. Constants are unfolded automatically, and sort *) |
|
60 (* axioms are added as well. Other, user-asserted axioms however are *) |
|
61 (* ignored. Inductive datatypes and recursive functions are supported, but *) |
|
62 (* may lead to spurious countermodels. *) |
|
63 (* *) |
|
64 (* The (space) complexity of the algorithm is non-elementary. *) |
|
65 (* *) |
|
66 (* Schematic type variables are not supported. *) |
|
67 (* ------------------------------------------------------------------------- *) |
|
68 |
|
69 (* ------------------------------------------------------------------------- *) |
|
70 (* PARAMETERS *) |
|
71 (* *) |
|
72 (* The following global parameters are currently supported (and required, *) |
|
73 (* except for "expect"): *) |
|
74 (* *) |
|
75 (* Name Type Description *) |
|
76 (* *) |
|
77 (* "minsize" int Only search for models with size at least *) |
|
78 (* 'minsize'. *) |
|
79 (* "maxsize" int If >0, only search for models with size at most *) |
|
80 (* 'maxsize'. *) |
|
81 (* "maxvars" int If >0, use at most 'maxvars' boolean variables *) |
|
82 (* when transforming the term into a propositional *) |
|
83 (* formula. *) |
|
84 (* "maxtime" int If >0, terminate after at most 'maxtime' seconds. *) |
|
85 (* This value is ignored under some ML compilers. *) |
|
86 (* "satsolver" string Name of the SAT solver to be used. *) |
|
87 (* "no_assms" bool If "true", assumptions in structured proofs are *) |
|
88 (* not considered. *) |
|
89 (* "expect" string Expected result ("genuine", "potential", "none", or *) |
|
90 (* "unknown"). *) |
|
91 (* *) |
|
92 (* The size of particular types can be specified in the form type=size *) |
|
93 (* (where 'type' is a string, and 'size' is an int). Examples: *) |
|
94 (* "'a"=1 *) |
|
95 (* "List.list"=2 *) |
|
96 (* ------------------------------------------------------------------------- *) |
|
97 |
|
98 (* ------------------------------------------------------------------------- *) |
|
99 (* FILES *) |
|
100 (* *) |
|
101 (* HOL/Tools/prop_logic.ML Propositional logic *) |
|
102 (* HOL/Tools/sat_solver.ML SAT solvers *) |
|
103 (* HOL/Tools/refute.ML Translation HOL -> propositional logic and *) |
|
104 (* Boolean assignment -> HOL model *) |
|
105 (* HOL/Refute.thy This file: loads the ML files, basic setup, *) |
|
106 (* documentation *) |
|
107 (* HOL/SAT.thy Sets default parameters *) |
|
108 (* HOL/ex/Refute_Examples.thy Examples *) |
|
109 (* ------------------------------------------------------------------------- *) |
|
110 \end{verbatim} |
|
111 *} |
|
112 |
|
113 end |