author | wenzelm |
Sat, 13 Mar 2010 14:44:47 +0100 | |
changeset 35743 | c506c029a082 |
parent 34120 | f9920a3ddf50 |
child 39048 | 4006f5c3f421 |
permissions | -rw-r--r-- |
14350 | 1 |
(* Title: HOL/Refute.thy |
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 |
33593 | 11 |
imports Hilbert_Choice List |
26521 | 12 |
uses |
13 |
"Tools/refute.ML" |
|
14 |
"Tools/refute_isar.ML" |
|
15131 | 15 |
begin |
14589 | 16 |
|
17 |
setup Refute.setup |
|
18 |
||
19 |
text {* |
|
20 |
\small |
|
21 |
\begin{verbatim} |
|
14350 | 22 |
(* ------------------------------------------------------------------------- *) |
23 |
(* REFUTE *) |
|
24 |
(* *) |
|
25 |
(* We use a SAT solver to search for a (finite) model that refutes a given *) |
|
26 |
(* HOL formula. *) |
|
27 |
(* ------------------------------------------------------------------------- *) |
|
28 |
||
29 |
(* ------------------------------------------------------------------------- *) |
|
14457 | 30 |
(* NOTE *) |
14350 | 31 |
(* *) |
14457 | 32 |
(* I strongly recommend that you install a stand-alone SAT solver if you *) |
14463 | 33 |
(* 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
|
34 |
(* have installed (a supported version of) zChaff, simply set 'ZCHAFF_HOME' *) |
7797a04cc188
removed explicit mentioning of zChaffs version number
webertj
parents:
15140
diff
changeset
|
35 |
(* in 'etc/settings'. *) |
14350 | 36 |
(* ------------------------------------------------------------------------- *) |
37 |
||
38 |
(* ------------------------------------------------------------------------- *) |
|
39 |
(* USAGE *) |
|
40 |
(* *) |
|
41 |
(* See the file 'HOL/ex/Refute_Examples.thy' for examples. The supported *) |
|
42 |
(* parameters are explained below. *) |
|
43 |
(* ------------------------------------------------------------------------- *) |
|
44 |
||
45 |
(* ------------------------------------------------------------------------- *) |
|
46 |
(* CURRENT LIMITATIONS *) |
|
47 |
(* *) |
|
48 |
(* 'refute' currently accepts formulas of higher-order predicate logic (with *) |
|
49 |
(* equality), including free/bound/schematic variables, lambda abstractions, *) |
|
16870 | 50 |
(* sets and set membership, "arbitrary", "The", "Eps", records and *) |
22058
49faa8c7a5d9
updated to mention the automatic unfolding of constants
webertj
parents:
21332
diff
changeset
|
51 |
(* inductively defined sets. Constants are unfolded automatically, and sort *) |
49faa8c7a5d9
updated to mention the automatic unfolding of constants
webertj
parents:
21332
diff
changeset
|
52 |
(* 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
|
53 |
(* ignored. Inductive datatypes and recursive functions are supported, but *) |
49faa8c7a5d9
updated to mention the automatic unfolding of constants
webertj
parents:
21332
diff
changeset
|
54 |
(* may lead to spurious countermodels. *) |
14463 | 55 |
(* *) |
14808 | 56 |
(* The (space) complexity of the algorithm is non-elementary. *) |
14350 | 57 |
(* *) |
16870 | 58 |
(* Schematic type variables are not supported. *) |
14350 | 59 |
(* ------------------------------------------------------------------------- *) |
60 |
||
61 |
(* ------------------------------------------------------------------------- *) |
|
62 |
(* PARAMETERS *) |
|
63 |
(* *) |
|
34120
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34018
diff
changeset
|
64 |
(* 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
|
65 |
(* except for "expect"): *) |
14350 | 66 |
(* *) |
67 |
(* Name Type Description *) |
|
68 |
(* *) |
|
69 |
(* "minsize" int Only search for models with size at least *) |
|
70 |
(* 'minsize'. *) |
|
71 |
(* "maxsize" int If >0, only search for models with size at most *) |
|
72 |
(* 'maxsize'. *) |
|
73 |
(* "maxvars" int If >0, use at most 'maxvars' boolean variables *) |
|
74 |
(* when transforming the term into a propositional *) |
|
75 |
(* formula. *) |
|
14808 | 76 |
(* "maxtime" int If >0, terminate after at most 'maxtime' seconds. *) |
77 |
(* This value is ignored under some ML compilers. *) |
|
14457 | 78 |
(* "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
|
79 |
(* "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
|
80 |
(* not considered. *) |
f9920a3ddf50
added "no_assms" option to Refute, and include structured proof assumptions by default;
blanchet
parents:
34018
diff
changeset
|
81 |
(* "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
|
82 |
(* "unknown"). *) |
14457 | 83 |
(* *) |
17721 | 84 |
(* See 'HOL/SAT.thy' for default values. *) |
14808 | 85 |
(* *) |
86 |
(* The size of particular types can be specified in the form type=size *) |
|
87 |
(* (where 'type' is a string, and 'size' is an int). Examples: *) |
|
88 |
(* "'a"=1 *) |
|
89 |
(* "List.list"=2 *) |
|
14350 | 90 |
(* ------------------------------------------------------------------------- *) |
91 |
||
92 |
(* ------------------------------------------------------------------------- *) |
|
93 |
(* FILES *) |
|
94 |
(* *) |
|
14457 | 95 |
(* HOL/Tools/prop_logic.ML Propositional logic *) |
96 |
(* HOL/Tools/sat_solver.ML SAT solvers *) |
|
97 |
(* HOL/Tools/refute.ML Translation HOL -> propositional logic and *) |
|
14808 | 98 |
(* Boolean assignment -> HOL model *) |
14350 | 99 |
(* HOL/Tools/refute_isar.ML Adds 'refute'/'refute_params' to Isabelle's *) |
14457 | 100 |
(* syntax *) |
101 |
(* HOL/Refute.thy This file: loads the ML files, basic setup, *) |
|
102 |
(* documentation *) |
|
17721 | 103 |
(* HOL/SAT.thy Sets default parameters *) |
14457 | 104 |
(* HOL/ex/RefuteExamples.thy Examples *) |
14350 | 105 |
(* ------------------------------------------------------------------------- *) |
14589 | 106 |
\end{verbatim} |
107 |
*} |
|
14350 | 108 |
|
109 |
end |