document "lam_trans" option
authorblanchet
Wed, 16 Nov 2011 10:34:08 +0100
changeset 45516 b2c8422833da
parent 45515 9fa58cacf95d
child 45517 e1d9f0fa80d3
document "lam_trans" option
NEWS
doc-src/Sledgehammer/sledgehammer.tex
src/HOL/Tools/ATP/atp_translate.ML
--- a/NEWS	Wed Nov 16 10:09:44 2011 +0100
+++ b/NEWS	Wed Nov 16 10:34:08 2011 +0100
@@ -85,10 +85,16 @@
 produces a rule which can be used to perform case distinction on both
 a list and a nat.
 
-
 * Nitpick:
-  - Fixed infinite loop caused by the 'peephole_optim' option and affecting
-    'rat' and 'real'.
+  - Fixed infinite loop caused by the 'peephole_optim' option and
+    affecting 'rat' and 'real'.
+
+* Sledgehammer:
+  - Added "lam_trans" option.
+
+* Metis:
+  - Added possibility to specify lambda translations scheme as a
+    parenthesized argument (e.g., "by (metis (lam_lifting) ...)").
 
 
 *** FOL ***
--- a/doc-src/Sledgehammer/sledgehammer.tex	Wed Nov 16 10:09:44 2011 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Wed Nov 16 10:34:08 2011 +0100
@@ -15,6 +15,8 @@
 \def\qty#1{\ensuremath{\left<\mathit{#1\/}\right>}}
 \def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1\/}}\right>}$}
 
+\newcommand\const[1]{\textsf{#1}}
+
 %\oddsidemargin=4.6mm
 %\evensidemargin=4.6mm
 %\textwidth=150mm
@@ -40,6 +42,10 @@
 
 \begin{document}
 
+%%% TYPESETTING
+%\renewcommand\labelitemi{$\bullet$}
+\renewcommand\labelitemi{\raise.065ex\hbox{\small\textbullet}}
+
 \selectlanguage{english}
 
 \title{\includegraphics[scale=0.5]{isabelle_sledgehammer} \\[4ex]
@@ -149,13 +155,13 @@
 There are three main ways to install ATPs on your machine:
 
 \begin{enum}
-\item[$\bullet$] If you installed an official Isabelle package with everything
+\item[\labelitemi] If you installed an official Isabelle package with everything
 inside, it should already include properly setup executables for E and SPASS,
 ready to use.%
 \footnote{Vampire's license prevents us from doing the same for this otherwise
 wonderful tool.}
 
-\item[$\bullet$] Alternatively, you can download the Isabelle-aware E and SPASS
+\item[\labelitemi] Alternatively, you can download the Isabelle-aware E and SPASS
 binary packages from Isabelle's download page. Extract the archives, then add a
 line to your \texttt{\$ISABELLE\_HOME\_USER/etc/components}%
 \footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at
@@ -172,7 +178,7 @@
 
 in it.
 
-\item[$\bullet$] If you prefer to build E or SPASS yourself, or obtained a
+\item[\labelitemi] If you prefer to build E or SPASS yourself, or obtained a
 Vampire executable from somewhere (e.g., \url{http://www.vprover.org/}),
 set the environment variable \texttt{E\_HOME}, \texttt{SPASS\_HOME}, or
 \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
@@ -215,7 +221,7 @@
 There are two main ways of installing SMT solvers locally.
 
 \begin{enum}
-\item[$\bullet$] If you installed an official Isabelle package with everything
+\item[\labelitemi] If you installed an official Isabelle package with everything
 inside, it should already include properly setup executables for CVC3 and Z3,
 ready to use.%
 \footnote{Yices's license prevents us from doing the same for this otherwise
@@ -224,7 +230,7 @@
 \texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a noncommercial
 user.
 
-\item[$\bullet$] Otherwise, follow the instructions documented in the \emph{SMT}
+\item[\labelitemi] Otherwise, follow the instructions documented in the \emph{SMT}
 theory (\texttt{\$ISABELLE\_HOME/src/HOL/SMT.thy}).
 \end{enum}
 
@@ -330,25 +336,25 @@
 familiarize themselves with the following options:
 
 \begin{enum}
-\item[$\bullet$] \textbf{\textit{provers}} (\S\ref{mode-of-operation}) specifies
+\item[\labelitemi] \textbf{\textit{provers}} (\S\ref{mode-of-operation}) specifies
 the automatic provers (ATPs and SMT solvers) that should be run whenever
 Sledgehammer is invoked (e.g., ``\textit{provers}~= \textit{e spass
 remote\_vampire}''). For convenience, you can omit ``\textit{provers}~=''
 and simply write the prover names as a space-separated list (e.g., ``\textit{e
 spass remote\_vampire}'').
 
-\item[$\bullet$] \textbf{\textit{max\_relevant}} (\S\ref{relevance-filter})
+\item[\labelitemi] \textbf{\textit{max\_relevant}} (\S\ref{relevance-filter})
 specifies the maximum number of facts that should be passed to the provers. By
 default, the value is prover-dependent but varies between about 150 and 1000. If
 the provers time out, you can try lowering this value to, say, 100 or 50 and see
 if that helps.
 
-\item[$\bullet$] \textbf{\textit{isar\_proof}} (\S\ref{output-format}) specifies
+\item[\labelitemi] \textbf{\textit{isar\_proof}} (\S\ref{output-format}) specifies
 that Isar proofs should be generated, instead of one-liner \textit{metis} or
 \textit{smt} proofs. The length of the Isar proofs can be controlled by setting
 \textit{isar\_shrink\_factor} (\S\ref{output-format}).
 
-\item[$\bullet$] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the
+\item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the
 provers' time limit. It is set to 30 seconds, but since Sledgehammer runs
 asynchronously you should not hesitate to raise this limit to 60 or 120 seconds
 if you are the kind of user who can think clearly while ATPs are active.
@@ -377,17 +383,17 @@
 solutions:
 
 \begin{enum}
-\item[$\bullet$] Try the \textit{isar\_proof} option (\S\ref{output-format}) to
+\item[\labelitemi] Try the \textit{isar\_proof} option (\S\ref{output-format}) to
 obtain a step-by-step Isar proof where each step is justified by \textit{metis}.
 Since the steps are fairly small, \textit{metis} is more likely to be able to
 replay them.
 
-\item[$\bullet$] Try the \textit{smt} proof method instead of \textit{metis}. It
+\item[\labelitemi] Try the \textit{smt} proof method instead of \textit{metis}. It
 is usually stronger, but you need to either have Z3 available to replay the
 proofs, trust the SMT solver, or use certificates. See the documentation in the
 \emph{SMT} theory (\texttt{\$ISABELLE\_HOME/src/HOL/SMT.thy}) for details.
 
-\item[$\bullet$] Try the \textit{blast} or \textit{auto} proof methods, passing
+\item[\labelitemi] Try the \textit{blast} or \textit{auto} proof methods, passing
 the necessary facts via \textbf{unfolding}, \textbf{using}, \textit{intro}{:},
 \textit{elim}{:}, \textit{dest}{:}, or \textit{simp}{:}, as appropriate.
 \end{enum}
@@ -487,7 +493,7 @@
 The \textit{metis}~(\textit{full\_types}) proof method is the fully-typed
 version of Metis. It is somewhat slower than \textit{metis}, but the proof
 search is fully typed, and it also includes more powerful rules such as the
-axiom ``$x = \mathit{True} \mathrel{\lor} x = \mathit{False}$'' for reasoning in
+axiom ``$x = \const{True} \mathrel{\lor} x = \const{False}$'' for reasoning in
 higher-order places (e.g., in set comprehensions). The method kicks in
 automatically as a fallback when \textit{metis} fails, and it is sometimes
 generated by Sledgehammer instead of \textit{metis} if the proof obviously
@@ -580,31 +586,31 @@
 In the general syntax, the \qty{subcommand} may be any of the following:
 
 \begin{enum}
-\item[$\bullet$] \textbf{\textit{run} (the default):} Runs Sledgehammer on
+\item[\labelitemi] \textbf{\textit{run} (the default):} Runs Sledgehammer on
 subgoal number \qty{num} (1 by default), with the given options and facts.
 
-\item[$\bullet$] \textbf{\textit{min}:} Attempts to minimize the facts
+\item[\labelitemi] \textbf{\textit{min}:} Attempts to minimize the facts
 specified in the \qty{facts\_override} argument to obtain a simpler proof
 involving fewer facts. The options and goal number are as for \textit{run}.
 
-\item[$\bullet$] \textbf{\textit{messages}:} Redisplays recent messages issued
+\item[\labelitemi] \textbf{\textit{messages}:} Redisplays recent messages issued
 by Sledgehammer. This allows you to examine results that might have been lost
 due to Sledgehammer's asynchronous nature. The \qty{num} argument specifies a
 limit on the number of messages to display (5 by default).
 
-\item[$\bullet$] \textbf{\textit{supported\_provers}:} Prints the list of
+\item[\labelitemi] \textbf{\textit{supported\_provers}:} Prints the list of
 automatic provers supported by Sledgehammer. See \S\ref{installation} and
 \S\ref{mode-of-operation} for more information on how to install automatic
 provers.
 
-\item[$\bullet$] \textbf{\textit{running\_provers}:} Prints information about
+\item[\labelitemi] \textbf{\textit{running\_provers}:} Prints information about
 currently running automatic provers, including elapsed runtime and remaining
 time until timeout.
 
-\item[$\bullet$] \textbf{\textit{kill\_provers}:} Terminates all running
+\item[\labelitemi] \textbf{\textit{kill\_provers}:} Terminates all running
 automatic provers.
 
-\item[$\bullet$] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote
+\item[\labelitemi] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote
 ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}.
 \end{enum}
 
@@ -686,16 +692,16 @@
 The descriptions below refer to the following syntactic quantities:
 
 \begin{enum}
-\item[$\bullet$] \qtybf{string}: A string.
-\item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}.
-\item[$\bullet$] \qtybf{smart\_bool\/}: \textit{true}, \textit{false}, or
+\item[\labelitemi] \qtybf{string}: A string.
+\item[\labelitemi] \qtybf{bool\/}: \textit{true} or \textit{false}.
+\item[\labelitemi] \qtybf{smart\_bool\/}: \textit{true}, \textit{false}, or
 \textit{smart}.
-\item[$\bullet$] \qtybf{int\/}: An integer.
-%\item[$\bullet$] \qtybf{float\/}: A floating-point number (e.g., 2.5).
-\item[$\bullet$] \qtybf{float\_pair\/}: A pair of floating-point numbers
+\item[\labelitemi] \qtybf{int\/}: An integer.
+%\item[\labelitemi] \qtybf{float\/}: A floating-point number (e.g., 2.5).
+\item[\labelitemi] \qtybf{float\_pair\/}: A pair of floating-point numbers
 (e.g., 0.6 0.95).
-\item[$\bullet$] \qtybf{smart\_int\/}: An integer or \textit{smart}.
-\item[$\bullet$] \qtybf{float\_or\_none\/}: A floating-point number (e.g., 60 or
+\item[\labelitemi] \qtybf{smart\_int\/}: An integer or \textit{smart}.
+\item[\labelitemi] \qtybf{float\_or\_none\/}: A floating-point number (e.g., 60 or
 0.5) expressing a number of seconds, or the keyword \textit{none} ($\infty$
 seconds).
 \end{enum}
@@ -714,68 +720,68 @@
 provers are supported:
 
 \begin{enum}
-\item[$\bullet$] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by
+\item[\labelitemi] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by
 Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3,
 set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the
 executable, including the file name. Sledgehammer has been tested with version
 2.2.
 
-\item[$\bullet$] \textbf{\textit{e}:} E is a first-order resolution prover
+\item[\labelitemi] \textbf{\textit{e}:} E is a first-order resolution prover
 developed by Stephan Schulz \cite{schulz-2002}. To use E, set the environment
 variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof}
 executable, or install the prebuilt E package from Isabelle's download page. See
 \S\ref{installation} for details.
 
-\item[$\bullet$] \textbf{\textit{leo2}:} LEO-II is an automatic
+\item[\labelitemi] \textbf{\textit{leo2}:} LEO-II is an automatic
 higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
-with support for the TPTP many-typed higher-order syntax (THF0). Sledgehammer
+with support for the TPTP typed higher-order syntax (THF0). Sledgehammer
 requires version 1.2.9 or above.
 
-\item[$\bullet$] \textbf{\textit{metis}:} Although it is much less powerful than
+\item[\labelitemi] \textbf{\textit{metis}:} Although it is much less powerful than
 the external provers, Metis itself can be used for proof search.
 
-\item[$\bullet$] \textbf{\textit{metis\_full\_types}:} Fully typed version of
+\item[\labelitemi] \textbf{\textit{metis\_full\_types}:} Fully typed version of
 Metis, corresponding to \textit{metis} (\textit{full\_types}).
 
-\item[$\bullet$] \textbf{\textit{metis\_no\_types}:} Untyped version of Metis,
+\item[\labelitemi] \textbf{\textit{metis\_no\_types}:} Untyped version of Metis,
 corresponding to \textit{metis} (\textit{no\_types}).
 
-\item[$\bullet$] \textbf{\textit{satallax}:} Satallax is an automatic
+\item[\labelitemi] \textbf{\textit{satallax}:} Satallax is an automatic
 higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with
-support for the TPTP many-typed higher-order syntax (THF0). Sledgehammer
+support for the TPTP typed higher-order syntax (THF0). Sledgehammer
 requires version 2.2 or above.
 
-\item[$\bullet$] \textbf{\textit{smt}:} The \textit{smt} proof method with the
+\item[\labelitemi] \textbf{\textit{smt}:} The \textit{smt} proof method with the
 current settings (typically, Z3 with proof reconstruction).
 
-\item[$\bullet$] \textbf{\textit{spass}:} SPASS is a first-order resolution
+\item[\labelitemi] \textbf{\textit{spass}:} SPASS is a first-order resolution
 prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}.
 To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory
 that contains the \texttt{SPASS} executable, or install the prebuilt SPASS
 package from Isabelle's download page. Sledgehammer requires version 3.5 or
 above. See \S\ref{installation} for details.
 
-\item[$\bullet$] \textbf{\textit{vampire}:} Vampire is a first-order resolution
+\item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a first-order resolution
 prover developed by Andrei Voronkov and his colleagues
 \cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable
 \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire}
 executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g., ``1.8'').
 Sledgehammer has been tested with versions 0.6, 1.0, and 1.8. Vampire 1.8
-supports the TPTP many-typed first-order format (TFF0).
+supports the TPTP typed first-order format (TFF0).
 
-\item[$\bullet$] \textbf{\textit{yices}:} Yices is an SMT solver developed at
+\item[\labelitemi] \textbf{\textit{yices}:} Yices is an SMT solver developed at
 SRI \cite{yices}. To use Yices, set the environment variable
 \texttt{YICES\_SOLVER} to the complete path of the executable, including the
 file name. Sledgehammer has been tested with version 1.0.
 
-\item[$\bullet$] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
+\item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
 Microsoft Research \cite{z3}. To use Z3, set the environment variable
 \texttt{Z3\_SOLVER} to the complete path of the executable, including the file
 name, and set \texttt{Z3\_NON\_COMMERCIAL} to ``yes'' to confirm that you are a
 noncommercial user. Sledgehammer has been tested with versions 2.7 to 2.18.
 
-\item[$\bullet$] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be
-an ATP, exploiting Z3's support for the TPTP untyped and many-typed first-order
+\item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to be
+an ATP, exploiting Z3's support for the TPTP untyped and typed first-order
 formats (FOF and TFF0). It is included for experimental purposes. It requires
 version 3.0 or above.
 \end{enum}
@@ -783,28 +789,28 @@
 In addition, the following remote provers are supported:
 
 \begin{enum}
-\item[$\bullet$] \textbf{\textit{remote\_cvc3}:} The remote version of CVC3 runs
+\item[\labelitemi] \textbf{\textit{remote\_cvc3}:} The remote version of CVC3 runs
 on servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
 point).
 
-\item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E runs
+\item[\labelitemi] \textbf{\textit{remote\_e}:} The remote version of E runs
 on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
 
-\item[$\bullet$] \textbf{\textit{remote\_e\_sine}:} E-SInE is a metaprover
+\item[\labelitemi] \textbf{\textit{remote\_e\_sine}:} E-SInE is a metaprover
 developed by Kry\v stof Hoder \cite{sine} based on E. The remote version of
 SInE runs on Geoff Sutcliffe's Miami servers.
 
-\item[$\bullet$] \textbf{\textit{remote\_e\_tofof}:} E-ToFoF is a metaprover
+\item[\labelitemi] \textbf{\textit{remote\_e\_tofof}:} E-ToFoF is a metaprover
 developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
-servers. This ATP supports the TPTP many-typed first-order format (TFF0). The
+servers. This ATP supports the TPTP typed first-order format (TFF0). The
 remote version of E-ToFoF runs on Geoff Sutcliffe's Miami servers.
 
-\item[$\bullet$] \textbf{\textit{remote\_iprover}:} iProver is a pure
+\item[\labelitemi] \textbf{\textit{remote\_iprover}:} iProver is a pure
 instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}. The
 remote version of iProver runs on Geoff Sutcliffe's Miami servers
 \cite{sutcliffe-2000}.
 
-\item[$\bullet$] \textbf{\textit{remote\_iprover\_eq}:} iProver-Eq is an
+\item[\labelitemi] \textbf{\textit{remote\_iprover\_eq}:} iProver-Eq is an
 instantiation-based prover with native support for equality developed by
 Konstantin Korovin and Christoph Sticksel \cite{korovin-sticksel-2010}. The
 remote version of iProver-Eq runs on Geoff Sutcliffe's Miami servers
@@ -813,31 +819,31 @@
 The remote version of LEO-II
 runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
 
-\item[$\bullet$] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II
+\item[\labelitemi] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II
 runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
 
-\item[$\bullet$] \textbf{\textit{remote\_satallax}:} The remote version of
+\item[\labelitemi] \textbf{\textit{remote\_satallax}:} The remote version of
 Satallax runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
 
-\item[$\bullet$] \textbf{\textit{remote\_snark}:} SNARK is a first-order
+\item[\labelitemi] \textbf{\textit{remote\_snark}:} SNARK is a first-order
 resolution prover developed by Stickel et al.\ \cite{snark}. It supports the
-TPTP many-typed first-order format (TFF0). The remote version of SNARK runs on
+TPTP typed first-order format (TFF0). The remote version of SNARK runs on
 Geoff Sutcliffe's Miami servers.
 
-\item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of
+\item[\labelitemi] \textbf{\textit{remote\_vampire}:} The remote version of
 Vampire runs on Geoff Sutcliffe's Miami servers. Version 1.8 is used.
 
-\item[$\bullet$] \textbf{\textit{remote\_waldmeister}:} Waldmeister is a unit
+\item[\labelitemi] \textbf{\textit{remote\_waldmeister}:} Waldmeister is a unit
 equality prover developed by Hillenbrand et al.\ \cite{waldmeister}. It can be
 used to prove universally quantified equations using unconditional equations,
 corresponding to the TPTP CNF UEQ division. The remote version of Waldmeister
 runs on Geoff Sutcliffe's Miami servers.
 
-\item[$\bullet$] \textbf{\textit{remote\_z3}:} The remote version of Z3 runs on
+\item[\labelitemi] \textbf{\textit{remote\_z3}:} The remote version of Z3 runs on
 servers at the TU M\"unchen (or wherever \texttt{REMOTE\_SMT\_URL} is set to
 point).
 
-\item[$\bullet$] \textbf{\textit{remote\_z3\_tptp}:} The remote version of ``Z3
+\item[\labelitemi] \textbf{\textit{remote\_z3\_tptp}:} The remote version of ``Z3
 with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers.
 \end{enum}
 
@@ -901,7 +907,44 @@
 \subsection{Problem Encoding}
 \label{problem-encoding}
 
+\newcommand\comb[1]{\const{#1}}
+
 \begin{enum}
+\opdefault{lam\_trans}{string}{smart}
+Specifies the $\lambda$ translation scheme to use in ATP problems. The supported
+translation schemes are listed below:
+
+\begin{enum}
+\item[\labelitemi] \textbf{\textit{hide\_lams}:} Hide the $\lambda$-abstractions
+by replacing them by unspecified fresh constants, effectively disabling all
+reasoning under $\lambda$-abstractions.
+
+\item[\labelitemi] \textbf{\textit{lam\_lifting}:} Introduce a new
+supercombinator \const{c} for each cluster of $n$~$\lambda$-abstractions,
+defined using an equation $\const{c}~x_1~\ldots~x_n = t$ ($\lambda$-lifting).
+
+\item[\labelitemi] \textbf{\textit{combinators}:} Rewrite lambdas to the Curry
+combinators (\comb{I}, \comb{K}, \comb{S}, \comb{B}, \comb{C}). Combinators
+enable the ATPs to synthesize $\lambda$-terms but tend to yield bulkier formulas
+than $\lambda$-lifting: The translation is quadratic in the worst case, and the
+equational definitions of the combinators are very prolific in the context of
+resolution.
+
+\item[\labelitemi] \textbf{\textit{hybrid\_lams}:} Introduce a new
+supercombinator \const{c} for each cluster of $\lambda$-abstractions and characterize it both using a
+lifted equation $\const{c}~x_1~\ldots~x_n = t$ and via Curry combinators.
+
+\item[\labelitemi] \textbf{\textit{keep\_lams}:}
+Keep the $\lambda$-abstractions in the generated problems. This is available
+only with provers that support the THF0 syntax.
+
+\item[\labelitemi] \textbf{\textit{smart}:} The actual translation scheme used
+depends on the ATP and should be the most efficient scheme for that ATP.
+\end{enum}
+
+For SMT solvers, the $\lambda$ translation scheme is always
+\textit{lam\_lifting}, irrespective of the value of this option.
+
 \opdefault{type\_enc}{string}{smart}
 Specifies the type encoding to use in ATP problems. Some of the type encodings
 are unsound, meaning that they can give rise to spurious proofs
@@ -909,23 +952,23 @@
 listed below, with an indication of their soundness in parentheses:
 
 \begin{enum}
-\item[$\bullet$] \textbf{\textit{erased} (very unsound):} No type information is
+\item[\labelitemi] \textbf{\textit{erased} (very unsound):} No type information is
 supplied to the ATP. Types are simply erased.
 
-\item[$\bullet$] \textbf{\textit{poly\_guards} (sound):} Types are encoded using
+\item[\labelitemi] \textbf{\textit{poly\_guards} (sound):} Types are encoded using
 a predicate \textit{has\_\allowbreak type\/}$(\tau, t)$ that guards bound
 variables. Constants are annotated with their types, supplied as additional
 arguments, to resolve overloading.
 
-\item[$\bullet$] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is
-tagged with its type using a function $\mathit{type\/}(\tau, t)$.
+\item[\labelitemi] \textbf{\textit{poly\_tags} (sound):} Each term and subterm is
+tagged with its type using a function $\const{type\/}(\tau, t)$.
 
-\item[$\bullet$] \textbf{\textit{poly\_args} (unsound):}
+\item[\labelitemi] \textbf{\textit{poly\_args} (unsound):}
 Like for \textit{poly\_guards} constants are annotated with their types to
 resolve overloading, but otherwise no type information is encoded. This
 coincides with the default encoding used by the \textit{metis} command.
 
-\item[$\bullet$]
+\item[\labelitemi]
 \textbf{%
 \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags} (sound); \\
 \textit{raw\_mono\_args} (unsound):} \\
@@ -935,7 +978,7 @@
 Monomorphization can simplify reasoning but also leads to larger fact bases,
 which can slow down the ATPs.
 
-\item[$\bullet$]
+\item[\labelitemi]
 \textbf{%
 \textit{mono\_guards}, \textit{mono\_tags} (sound);
 \textit{mono\_args} (unsound):} \\
@@ -943,20 +986,20 @@
 \textit{raw\_mono\_guards}, \textit{raw\_mono\_tags}, and
 \textit{raw\_mono\_args}, respectively but types are mangled in constant names
 instead of being supplied as ground term arguments. The binary predicate
-$\mathit{has\_type\/}(\tau, t)$ becomes a unary predicate
-$\mathit{has\_type\_}\tau(t)$, and the binary function
-$\mathit{type\/}(\tau, t)$ becomes a unary function
-$\mathit{type\_}\tau(t)$.
+$\const{has\_type\/}(\tau, t)$ becomes a unary predicate
+$\const{has\_type\_}\tau(t)$, and the binary function
+$\const{type\/}(\tau, t)$ becomes a unary function
+$\const{type\_}\tau(t)$.
 
-\item[$\bullet$] \textbf{\textit{mono\_simple} (sound):} Exploits simple
+\item[\labelitemi] \textbf{\textit{mono\_simple} (sound):} Exploits simple
 first-order types if the prover supports the TFF0 or THF0 syntax; otherwise,
 falls back on \textit{mono\_guards}. The problem is monomorphized.
 
-\item[$\bullet$] \textbf{\textit{mono\_simple\_higher} (sound):} Exploits simple
+\item[\labelitemi] \textbf{\textit{mono\_simple\_higher} (sound):} Exploits simple
 higher-order types if the prover supports the THF0 syntax; otherwise, falls back
 on \textit{mono\_simple} or \textit{mono\_guards}. The problem is monomorphized.
 
-\item[$\bullet$]
+\item[\labelitemi]
 \textbf{%
 \textit{poly\_guards}?, \textit{poly\_tags}?, \textit{raw\_mono\_guards}?, \\
 \textit{raw\_mono\_tags}?, \textit{mono\_guards}?, \textit{mono\_tags}?, \\
@@ -972,7 +1015,7 @@
 mark is replaced by a \hbox{``\textit{\_query}''} suffix. If the \emph{sound}
 option is enabled, these encodings are fully sound.
 
-\item[$\bullet$]
+\item[\labelitemi]
 \textbf{%
 \textit{poly\_guards}??, \textit{poly\_tags}??, \textit{raw\_mono\_guards}??, \\
 \textit{raw\_mono\_tags}??, \textit{mono\_guards}??, \textit{mono\_tags}?? \\
@@ -981,7 +1024,7 @@
 \textit{metis} proof method, the `\hbox{??}' suffix is replaced by
 \hbox{``\textit{\_query\_query}''}.
 
-\item[$\bullet$]
+\item[\labelitemi]
 \textbf{%
 \textit{poly\_guards}@?, \textit{poly\_tags}@?, \textit{raw\_mono\_guards}@?, \\
 \textit{raw\_mono\_tags}@? (quasi-sound):} \\
@@ -989,7 +1032,7 @@
 \textit{metis} proof method, the `\hbox{@?}' suffix is replaced by
 \hbox{``\textit{\_at\_query}''}.
 
-\item[$\bullet$]
+\item[\labelitemi]
 \textbf{%
 \textit{poly\_guards}!, \textit{poly\_tags}!, \textit{raw\_mono\_guards}!, \\
 \textit{raw\_mono\_tags}!, \textit{mono\_guards}!, \textit{mono\_tags}!, \\
@@ -1005,7 +1048,7 @@
 \textit{metis} proof method, the exclamation mark is replaced by the suffix
 \hbox{``\textit{\_bang}''}.
 
-\item[$\bullet$]
+\item[\labelitemi]
 \textbf{%
 \textit{poly\_guards}!!, \textit{poly\_tags}!!, \textit{raw\_mono\_guards}!!, \\
 \textit{raw\_mono\_tags}!!, \textit{mono\_guards}!!, \textit{mono\_tags}!! \\
@@ -1014,7 +1057,7 @@
 \textit{metis} proof method, the `\hbox{!!}' suffix is replaced by
 \hbox{``\textit{\_bang\_bang}''}.
 
-\item[$\bullet$]
+\item[\labelitemi]
 \textbf{%
 \textit{poly\_guards}@!, \textit{poly\_tags}@!, \textit{raw\_mono\_guards}@!, \\
 \textit{raw\_mono\_tags}@! (mildly unsound):} \\
@@ -1022,7 +1065,7 @@
 \textit{metis} proof method, the `\hbox{@!}' suffix is replaced by
 \hbox{``\textit{\_at\_bang}''}.
 
-\item[$\bullet$] \textbf{\textit{smart}:} The actual encoding used depends on
+\item[\labelitemi] \textbf{\textit{smart}:} The actual encoding used depends on
 the ATP and should be the most efficient virtually sound encoding for that ATP.
 \end{enum}
 
@@ -1116,11 +1159,11 @@
 Specifies the expected outcome, which must be one of the following:
 
 \begin{enum}
-\item[$\bullet$] \textbf{\textit{some}:} Sledgehammer found a (potentially
+\item[\labelitemi] \textbf{\textit{some}:} Sledgehammer found a (potentially
 unsound) proof.
-\item[$\bullet$] \textbf{\textit{none}:} Sledgehammer found no proof.
-\item[$\bullet$] \textbf{\textit{timeout}:} Sledgehammer timed out.
-\item[$\bullet$] \textbf{\textit{unknown}:} Sledgehammer encountered some
+\item[\labelitemi] \textbf{\textit{none}:} Sledgehammer found no proof.
+\item[\labelitemi] \textbf{\textit{timeout}:} Sledgehammer timed out.
+\item[\labelitemi] \textbf{\textit{unknown}:} Sledgehammer encountered some
 problem.
 \end{enum}
 
--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Nov 16 10:09:44 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Nov 16 10:34:08 2011 +0100
@@ -121,7 +121,7 @@
 val type_tag_arguments =
   Attrib.setup_config_bool @{binding atp_type_tag_arguments} (K false)
 
-val no_lamsN = "no_lams"
+val no_lamsN = "no_lams" (* used internally; undocumented *)
 val hide_lamsN = "hide_lams"
 val lam_liftingN = "lam_lifting"
 val combinatorsN = "combinators"