1.1 --- a/doc-src/Nitpick/nitpick.tex Wed Nov 16 09:42:27 2011 +0100
1.2 +++ b/doc-src/Nitpick/nitpick.tex Wed Nov 16 10:09:44 2011 +0100
1.3 @@ -41,6 +41,10 @@
1.4
1.5 \begin{document}
1.6
1.7 +%%% TYPESETTING
1.8 +%\renewcommand\labelitemi{$\bullet$}
1.9 +\renewcommand\labelitemi{\raise.065ex\hbox{\small\textbullet}}
1.10 +
1.11 \selectlanguage{english}
1.12
1.13 \title{\includegraphics[scale=0.5]{isabelle_nitpick} \\[4ex]
1.14 @@ -1885,24 +1889,24 @@
1.15 The descriptions below refer to the following syntactic quantities:
1.16
1.17 \begin{enum}
1.18 -\item[$\bullet$] \qtybf{string}: A string.
1.19 -\item[$\bullet$] \qtybf{string\_list\/}: A space-separated list of strings
1.20 +\item[\labelitemi] \qtybf{string}: A string.
1.21 +\item[\labelitemi] \qtybf{string\_list\/}: A space-separated list of strings
1.22 (e.g., ``\textit{ichi ni san}'').
1.23 -\item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}.
1.24 -\item[$\bullet$] \qtybf{smart\_bool\/}: \textit{true}, \textit{false}, or \textit{smart}.
1.25 -\item[$\bullet$] \qtybf{int\/}: An integer. Negative integers are prefixed with a hyphen.
1.26 -\item[$\bullet$] \qtybf{smart\_int\/}: An integer or \textit{smart}.
1.27 -\item[$\bullet$] \qtybf{int\_range}: An integer (e.g., 3) or a range
1.28 +\item[\labelitemi] \qtybf{bool\/}: \textit{true} or \textit{false}.
1.29 +\item[\labelitemi] \qtybf{smart\_bool\/}: \textit{true}, \textit{false}, or \textit{smart}.
1.30 +\item[\labelitemi] \qtybf{int\/}: An integer. Negative integers are prefixed with a hyphen.
1.31 +\item[\labelitemi] \qtybf{smart\_int\/}: An integer or \textit{smart}.
1.32 +\item[\labelitemi] \qtybf{int\_range}: An integer (e.g., 3) or a range
1.33 of nonnegative integers (e.g., $1$--$4$). The range symbol `--' can be entered as \texttt{-} (hyphen) or \texttt{\char`\\\char`\<emdash\char`\>}.
1.34 -\item[$\bullet$] \qtybf{int\_seq}: A comma-separated sequence of ranges of integers (e.g.,~1{,}3{,}\allowbreak6--8).
1.35 -\item[$\bullet$] \qtybf{float\_or\_none}: An integer (e.g., 60) or floating-point number
1.36 +\item[\labelitemi] \qtybf{int\_seq}: A comma-separated sequence of ranges of integers (e.g.,~1{,}3{,}\allowbreak6--8).
1.37 +\item[\labelitemi] \qtybf{float\_or\_none}: An integer (e.g., 60) or floating-point number
1.38 (e.g., 0.5) expressing a number of seconds, or the keyword \textit{none}
1.39 ($\infty$ seconds).
1.40 -\item[$\bullet$] \qtybf{const\/}: The name of a HOL constant.
1.41 -\item[$\bullet$] \qtybf{term}: A HOL term (e.g., ``$f~x$'').
1.42 -\item[$\bullet$] \qtybf{term\_list\/}: A space-separated list of HOL terms (e.g.,
1.43 +\item[\labelitemi] \qtybf{const\/}: The name of a HOL constant.
1.44 +\item[\labelitemi] \qtybf{term}: A HOL term (e.g., ``$f~x$'').
1.45 +\item[\labelitemi] \qtybf{term\_list\/}: A space-separated list of HOL terms (e.g.,
1.46 ``$f~x$''~``$g~y$'').
1.47 -\item[$\bullet$] \qtybf{type}: A HOL type.
1.48 +\item[\labelitemi] \qtybf{type}: A HOL type.
1.49 \end{enum}
1.50
1.51 Default values are indicated in curly brackets (\textrm{\{\}}). Boolean options
1.52 @@ -2032,17 +2036,17 @@
1.53 well-founded. The option can take the following values:
1.54
1.55 \begin{enum}
1.56 -\item[$\bullet$] \textbf{\textit{true}:} Tentatively treat the (co)in\-duc\-tive
1.57 +\item[\labelitemi] \textbf{\textit{true}:} Tentatively treat the (co)in\-duc\-tive
1.58 predicate as if it were well-founded. Since this is generally not sound when the
1.59 predicate is not well-founded, the counterexamples are tagged as ``quasi
1.60 genuine.''
1.61
1.62 -\item[$\bullet$] \textbf{\textit{false}:} Treat the (co)in\-duc\-tive predicate
1.63 +\item[\labelitemi] \textbf{\textit{false}:} Treat the (co)in\-duc\-tive predicate
1.64 as if it were not well-founded. The predicate is then unrolled as prescribed by
1.65 the \textit{star\_linear\_preds}, \textit{iter}~\qty{const}, and \textit{iter}
1.66 options.
1.67
1.68 -\item[$\bullet$] \textbf{\textit{smart}:} Try to prove that the inductive
1.69 +\item[\labelitemi] \textbf{\textit{smart}:} Try to prove that the inductive
1.70 predicate is well-founded using Isabelle's \textit{lexicographic\_order} and
1.71 \textit{size\_change} tactics. If this succeeds (or the predicate occurs with an
1.72 appropriate polarity in the formula to falsify), use an efficient fixed-point
1.73 @@ -2095,10 +2099,10 @@
1.74 counterexamples. The option can take the following values:
1.75
1.76 \begin{enum}
1.77 -\item[$\bullet$] \textbf{\textit{true}:} Box the specified type whenever
1.78 +\item[\labelitemi] \textbf{\textit{true}:} Box the specified type whenever
1.79 practicable.
1.80 -\item[$\bullet$] \textbf{\textit{false}:} Never box the type.
1.81 -\item[$\bullet$] \textbf{\textit{smart}:} Box the type only in contexts where it
1.82 +\item[\labelitemi] \textbf{\textit{false}:} Never box the type.
1.83 +\item[\labelitemi] \textbf{\textit{smart}:} Box the type only in contexts where it
1.84 is likely to help. For example, $n$-tuples where $n > 2$ and arguments to
1.85 higher-order functions are good candidates for boxing.
1.86 \end{enum}
1.87 @@ -2116,11 +2120,11 @@
1.88 option can then take the following values:
1.89
1.90 \begin{enum}
1.91 -\item[$\bullet$] \textbf{\textit{true}:} Finitize the datatype. Since this is
1.92 +\item[\labelitemi] \textbf{\textit{true}:} Finitize the datatype. Since this is
1.93 unsound, counterexamples generated under these conditions are tagged as ``quasi
1.94 genuine.''
1.95 -\item[$\bullet$] \textbf{\textit{false}:} Don't attempt to finitize the datatype.
1.96 -\item[$\bullet$] \textbf{\textit{smart}:}
1.97 +\item[\labelitemi] \textbf{\textit{false}:} Don't attempt to finitize the datatype.
1.98 +\item[\labelitemi] \textbf{\textit{smart}:}
1.99 If the datatype's constructors don't appear in the problem, perform a
1.100 monotonicity analysis to detect whether the datatype can be soundly finitized;
1.101 otherwise, don't finitize it.
1.102 @@ -2302,14 +2306,14 @@
1.103 Specifies the expected outcome, which must be one of the following:
1.104
1.105 \begin{enum}
1.106 -\item[$\bullet$] \textbf{\textit{genuine}:} Nitpick found a genuine counterexample.
1.107 -\item[$\bullet$] \textbf{\textit{quasi\_genuine}:} Nitpick found a ``quasi
1.108 +\item[\labelitemi] \textbf{\textit{genuine}:} Nitpick found a genuine counterexample.
1.109 +\item[\labelitemi] \textbf{\textit{quasi\_genuine}:} Nitpick found a ``quasi
1.110 genuine'' counterexample (i.e., a counterexample that is genuine unless
1.111 it contradicts a missing axiom or a dangerous option was used inappropriately).
1.112 -\item[$\bullet$] \textbf{\textit{potential}:} Nitpick found a potentially
1.113 +\item[\labelitemi] \textbf{\textit{potential}:} Nitpick found a potentially
1.114 spurious counterexample.
1.115 -\item[$\bullet$] \textbf{\textit{none}:} Nitpick found no counterexample.
1.116 -\item[$\bullet$] \textbf{\textit{unknown}:} Nitpick encountered some problem (e.g.,
1.117 +\item[\labelitemi] \textbf{\textit{none}:} Nitpick found no counterexample.
1.118 +\item[\labelitemi] \textbf{\textit{unknown}:} Nitpick encountered some problem (e.g.,
1.119 Kodkod ran out of memory).
1.120 \end{enum}
1.121
1.122 @@ -2337,7 +2341,7 @@
1.123
1.124 \begin{enum}
1.125
1.126 -\item[$\bullet$] \textbf{\textit{CryptoMiniSat}:} CryptoMiniSat is the winner of
1.127 +\item[\labelitemi] \textbf{\textit{CryptoMiniSat}:} CryptoMiniSat is the winner of
1.128 the 2010 SAT Race. To use CryptoMiniSat, set the environment variable
1.129 \texttt{CRYPTO\-MINISAT\_}\discretionary{}{}{}\texttt{HOME} to the directory that contains the \texttt{crypto\-minisat}
1.130 executable.%
1.131 @@ -2348,17 +2352,17 @@
1.132 \url{http://planete.inrialpes.fr/~soos/}\allowbreak\url{CryptoMiniSat2/index.php}.
1.133 Nitpick has been tested with version 2.51.
1.134
1.135 -\item[$\bullet$] \textbf{\textit{CryptoMiniSat\_JNI}:} The JNI (Java Native
1.136 +\item[\labelitemi] \textbf{\textit{CryptoMiniSat\_JNI}:} The JNI (Java Native
1.137 Interface) version of CryptoMiniSat is bundled with Kodkodi and is precompiled
1.138 for Linux and Mac~OS~X. It is also available from the Kodkod web site
1.139 \cite{kodkod-2009}.
1.140
1.141 -\item[$\bullet$] \textbf{\textit{Lingeling\_JNI}:}
1.142 +\item[\labelitemi] \textbf{\textit{Lingeling\_JNI}:}
1.143 Lingeling is an efficient solver written in C. The JNI (Java Native Interface)
1.144 version of Lingeling is bundled with Kodkodi and is precompiled for Linux and
1.145 Mac~OS~X. It is also available from the Kodkod web site \cite{kodkod-2009}.
1.146
1.147 -\item[$\bullet$] \textbf{\textit{MiniSat}:} MiniSat is an efficient solver
1.148 +\item[\labelitemi] \textbf{\textit{MiniSat}:} MiniSat is an efficient solver
1.149 written in \cpp{}. To use MiniSat, set the environment variable
1.150 \texttt{MINISAT\_HOME} to the directory that contains the \texttt{minisat}
1.151 executable.%
1.152 @@ -2367,13 +2371,13 @@
1.153 \url{http://minisat.se/MiniSat.html}. Nitpick has been tested with versions 1.14
1.154 and 2.2.
1.155
1.156 -\item[$\bullet$] \textbf{\textit{MiniSat\_JNI}:} The JNI
1.157 +\item[\labelitemi] \textbf{\textit{MiniSat\_JNI}:} The JNI
1.158 version of MiniSat is bundled with Kodkodi and is precompiled for Linux,
1.159 Mac~OS~X, and Windows (Cygwin). It is also available from the Kodkod web site
1.160 \cite{kodkod-2009}. Unlike the standard version of MiniSat, the JNI version can
1.161 be used incrementally.
1.162
1.163 -\item[$\bullet$] \textbf{\textit{zChaff}:} zChaff is an older solver written
1.164 +\item[\labelitemi] \textbf{\textit{zChaff}:} zChaff is an older solver written
1.165 in \cpp{}. To use zChaff, set the environment variable \texttt{ZCHAFF\_HOME} to
1.166 the directory that contains the \texttt{zchaff} executable.%
1.167 \footref{cygwin-paths}
1.168 @@ -2381,7 +2385,7 @@
1.169 \url{http://www.princeton.edu/~chaff/zchaff.html}. Nitpick has been tested with
1.170 versions 2004-05-13, 2004-11-15, and 2007-03-12.
1.171
1.172 -\item[$\bullet$] \textbf{\textit{RSat}:} RSat is an efficient solver written in
1.173 +\item[\labelitemi] \textbf{\textit{RSat}:} RSat is an efficient solver written in
1.174 \cpp{}. To use RSat, set the environment variable \texttt{RSAT\_HOME} to the
1.175 directory that contains the \texttt{rsat} executable.%
1.176 \footref{cygwin-paths}
1.177 @@ -2389,30 +2393,30 @@
1.178 \url{http://reasoning.cs.ucla.edu/rsat/}. Nitpick has been tested with version
1.179 2.01.
1.180
1.181 -\item[$\bullet$] \textbf{\textit{BerkMin}:} BerkMin561 is an efficient solver
1.182 +\item[\labelitemi] \textbf{\textit{BerkMin}:} BerkMin561 is an efficient solver
1.183 written in C. To use BerkMin, set the environment variable
1.184 \texttt{BERKMIN\_HOME} to the directory that contains the \texttt{BerkMin561}
1.185 executable.\footref{cygwin-paths}
1.186 The BerkMin executables are available at
1.187 \url{http://eigold.tripod.com/BerkMin.html}.
1.188
1.189 -\item[$\bullet$] \textbf{\textit{BerkMin\_Alloy}:} Variant of BerkMin that is
1.190 +\item[\labelitemi] \textbf{\textit{BerkMin\_Alloy}:} Variant of BerkMin that is
1.191 included with Alloy 4 and calls itself ``sat56'' in its banner text. To use this
1.192 version of BerkMin, set the environment variable
1.193 \texttt{BERKMINALLOY\_HOME} to the directory that contains the \texttt{berkmin}
1.194 executable.%
1.195 \footref{cygwin-paths}
1.196
1.197 -\item[$\bullet$] \textbf{\textit{SAT4J}:} SAT4J is a reasonably efficient solver
1.198 +\item[\labelitemi] \textbf{\textit{SAT4J}:} SAT4J is a reasonably efficient solver
1.199 written in Java that can be used incrementally. It is bundled with Kodkodi and
1.200 requires no further installation or configuration steps. Do not attempt to
1.201 install the official SAT4J packages, because their API is incompatible with
1.202 Kodkod.
1.203
1.204 -\item[$\bullet$] \textbf{\textit{SAT4J\_Light}:} Variant of SAT4J that is
1.205 +\item[\labelitemi] \textbf{\textit{SAT4J\_Light}:} Variant of SAT4J that is
1.206 optimized for small problems. It can also be used incrementally.
1.207
1.208 -\item[$\bullet$] \textbf{\textit{smart}:} If \textit{sat\_solver} is set to
1.209 +\item[\labelitemi] \textbf{\textit{smart}:} If \textit{sat\_solver} is set to
1.210 \textit{smart}, Nitpick selects the first solver among the above that is
1.211 recognized by Isabelle. If \textit{verbose} (\S\ref{output-format}) is enabled,
1.212 Nitpick displays which SAT solver was chosen.
1.213 @@ -2837,7 +2841,7 @@
1.214 Here are the known bugs and limitations in Nitpick at the time of writing:
1.215
1.216 \begin{enum}
1.217 -\item[$\bullet$] Underspecified functions defined using the \textbf{primrec},
1.218 +\item[\labelitemi] Underspecified functions defined using the \textbf{primrec},
1.219 \textbf{function}, or \textbf{nominal\_\allowbreak primrec} packages can lead
1.220 Nitpick to generate spurious counterexamples for theorems that refer to values
1.221 for which the function is not defined. For example:
1.222 @@ -2858,33 +2862,33 @@
1.223 internal representation of functions synthesized by Isabelle, an implementation
1.224 detail.
1.225
1.226 -\item[$\bullet$] Similarly, Nitpick might find spurious counterexamples for
1.227 +\item[\labelitemi] Similarly, Nitpick might find spurious counterexamples for
1.228 theorems that rely on the use of the indefinite description operator internally
1.229 by \textbf{specification} and \textbf{quot\_type}.
1.230
1.231 -\item[$\bullet$] Axioms or definitions that restrict the possible values of the
1.232 +\item[\labelitemi] Axioms or definitions that restrict the possible values of the
1.233 \textit{undefined} constant or other partially specified built-in Isabelle
1.234 constants (e.g., \textit{Abs\_} and \textit{Rep\_} constants) are in general
1.235 ignored. Again, such nonconservative extensions are generally considered bad
1.236 style.
1.237
1.238 -\item[$\bullet$] Nitpick maintains a global cache of wellfoundedness conditions,
1.239 +\item[\labelitemi] Nitpick maintains a global cache of wellfoundedness conditions,
1.240 which can become invalid if you change the definition of an inductive predicate
1.241 that is registered in the cache. To clear the cache,
1.242 run Nitpick with the \textit{tac\_timeout} option set to a new value (e.g.,
1.243 $0.51$).
1.244
1.245 -\item[$\bullet$] Nitpick produces spurious counterexamples when invoked after a
1.246 +\item[\labelitemi] Nitpick produces spurious counterexamples when invoked after a
1.247 \textbf{guess} command in a structured proof.
1.248
1.249 -\item[$\bullet$] The \textit{nitpick\_xxx} attributes and the
1.250 +\item[\labelitemi] The \textit{nitpick\_xxx} attributes and the
1.251 \textit{Nitpick\_xxx.register\_yyy} functions can cause havoc if used
1.252 improperly.
1.253
1.254 -\item[$\bullet$] Although this has never been observed, arbitrary theorem
1.255 +\item[\labelitemi] Although this has never been observed, arbitrary theorem
1.256 morphisms could possibly confuse Nitpick, resulting in spurious counterexamples.
1.257
1.258 -\item[$\bullet$] All constants, types, free variables, and schematic variables
1.259 +\item[\labelitemi] All constants, types, free variables, and schematic variables
1.260 whose names start with \textit{Nitpick}{.} are reserved for internal use.
1.261 \end{enum}
1.262