author | wenzelm |
Sat, 12 Jan 2013 14:53:56 +0100 | |
changeset 50843 | 1465521b92a1 |
parent 50530 | 6266e44b3396 |
child 54556 | dd511ddcb203 |
permissions | -rw-r--r-- |
50530 | 1 |
(* Title: HOL/Library/Refute.thy |
14350 | 2 |
Author: Tjark Weber |
22058
49faa8c7a5d9
updated to mention the automatic unfolding of constants
webertj
parents:
21332
diff
changeset
|
3 |
Copyright 2003-2007 |
14350 | 4 |
|
5 |
Basic setup and documentation for the 'refute' (and 'refute_params') command. |
|
6 |
*) |
|
7 |
||
14589 | 8 |
header {* Refute *} |
9 |
||
15131 | 10 |
theory Refute |
40178
00152d17855b
reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
blanchet
parents:
40121
diff
changeset
|
11 |
imports Hilbert_Choice List Sledgehammer |
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
40178
diff
changeset
|
12 |
keywords "refute" :: diag and "refute_params" :: thy_decl |
15131 | 13 |
begin |
14589 | 14 |
|
49985
5b4b0e4e5205
moved Refute to "HOL/Library" to speed up building "Main" even more
blanchet
parents:
48891
diff
changeset
|
15 |
ML_file "refute.ML" |
14589 | 16 |
setup Refute.setup |
17 |
||
46960 | 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 |
||
14589 | 27 |
text {* |
28 |
\small |
|
29 |
\begin{verbatim} |
|
14350 | 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 |
(* ------------------------------------------------------------------------- *) |
|
14457 | 38 |
(* NOTE *) |
14350 | 39 |
(* *) |
14457 | 40 |
(* I strongly recommend that you install a stand-alone SAT solver if you *) |
14463 | 41 |
(* want to use 'refute'. For details see 'HOL/Tools/sat_solver.ML'. If you *) |
15293
7797a04cc188
removed explicit mentioning of zChaffs version number
webertj
parents:
15140
diff
changeset
|
42 |
(* have installed (a supported version of) zChaff, simply set 'ZCHAFF_HOME' *) |
7797a04cc188
removed explicit mentioning of zChaffs version number
webertj
parents:
15140
diff
changeset
|
43 |
(* in 'etc/settings'. *) |
14350 | 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, *) |
|
16870 | 58 |
(* sets and set membership, "arbitrary", "The", "Eps", records and *) |
22058
49faa8c7a5d9
updated to mention the automatic unfolding of constants
webertj
parents:
21332
diff
changeset
|
59 |
(* inductively defined sets. Constants are unfolded automatically, and sort *) |
49faa8c7a5d9
updated to mention the automatic unfolding of constants
webertj
parents:
21332
diff
changeset
|
60 |
(* axioms are added as well. Other, user-asserted axioms however are *) |
49faa8c7a5d9
updated to mention the automatic unfolding of constants
webertj
parents:
21332
diff
changeset
|
61 |
(* ignored. Inductive datatypes and recursive functions are supported, but *) |
49faa8c7a5d9
updated to mention the automatic unfolding of constants
webertj
parents:
21332
diff
changeset
|
62 |
(* may lead to spurious countermodels. *) |
14463 | 63 |
(* *) |
14808 | 64 |
(* The (space) complexity of the algorithm is non-elementary. *) |
14350 | 65 |
(* *) |
16870 | 66 |
(* Schematic type variables are not supported. *) |
14350 | 67 |
(* ------------------------------------------------------------------------- *) |
68 |
||
69 |
(* ------------------------------------------------------------------------- *) |
|
70 |
(* PARAMETERS *) |
|
71 |
(* *) |
|
34120
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34018
diff
changeset
|
72 |
(* The following global parameters are currently supported (and required, *) |
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34018
diff
changeset
|
73 |
(* except for "expect"): *) |
14350 | 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. *) |
|
14808 | 84 |
(* "maxtime" int If >0, terminate after at most 'maxtime' seconds. *) |
85 |
(* This value is ignored under some ML compilers. *) |
|
14457 | 86 |
(* "satsolver" string Name of the SAT solver to be used. *) |
34120
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34018
diff
changeset
|
87 |
(* "no_assms" bool If "true", assumptions in structured proofs are *) |
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34018
diff
changeset
|
88 |
(* not considered. *) |
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34018
diff
changeset
|
89 |
(* "expect" string Expected result ("genuine", "potential", "none", or *) |
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34018
diff
changeset
|
90 |
(* "unknown"). *) |
14457 | 91 |
(* *) |
14808 | 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 *) |
|
14350 | 96 |
(* ------------------------------------------------------------------------- *) |
97 |
||
98 |
(* ------------------------------------------------------------------------- *) |
|
99 |
(* FILES *) |
|
100 |
(* *) |
|
39048 | 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 *) |
|
14350 | 109 |
(* ------------------------------------------------------------------------- *) |
14589 | 110 |
\end{verbatim} |
111 |
*} |
|
14350 | 112 |
|
113 |
end |