--- a/NEWS Wed Nov 16 15:20:27 2011 +0100
+++ b/NEWS Thu Nov 17 05:27:45 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/Nitpick/nitpick.tex Wed Nov 16 15:20:27 2011 +0100
+++ b/doc-src/Nitpick/nitpick.tex Thu Nov 17 05:27:45 2011 +0100
@@ -41,6 +41,10 @@
\begin{document}
+%%% TYPESETTING
+%\renewcommand\labelitemi{$\bullet$}
+\renewcommand\labelitemi{\raise.065ex\hbox{\small\textbullet}}
+
\selectlanguage{english}
\title{\includegraphics[scale=0.5]{isabelle_nitpick} \\[4ex]
@@ -1530,7 +1534,7 @@
\end{tabular}
\postw
-The intuition behind the grammar is that $A$ generates all string with one more
+The intuition behind the grammar is that $A$ generates all strings with one more
$a$ than $b$'s and $B$ generates all strings with one more $b$ than $a$'s.
The alphabet consists exclusively of $a$'s and $b$'s:
@@ -1885,24 +1889,24 @@
The descriptions below refer to the following syntactic quantities:
\begin{enum}
-\item[$\bullet$] \qtybf{string}: A string.
-\item[$\bullet$] \qtybf{string\_list\/}: A space-separated list of strings
+\item[\labelitemi] \qtybf{string}: A string.
+\item[\labelitemi] \qtybf{string\_list\/}: A space-separated list of strings
(e.g., ``\textit{ichi ni san}'').
-\item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}.
-\item[$\bullet$] \qtybf{smart\_bool\/}: \textit{true}, \textit{false}, or \textit{smart}.
-\item[$\bullet$] \qtybf{int\/}: An integer. Negative integers are prefixed with a hyphen.
-\item[$\bullet$] \qtybf{smart\_int\/}: An integer or \textit{smart}.
-\item[$\bullet$] \qtybf{int\_range}: An integer (e.g., 3) or a range
+\item[\labelitemi] \qtybf{bool\/}: \textit{true} or \textit{false}.
+\item[\labelitemi] \qtybf{smart\_bool\/}: \textit{true}, \textit{false}, or \textit{smart}.
+\item[\labelitemi] \qtybf{int\/}: An integer. Negative integers are prefixed with a hyphen.
+\item[\labelitemi] \qtybf{smart\_int\/}: An integer or \textit{smart}.
+\item[\labelitemi] \qtybf{int\_range}: An integer (e.g., 3) or a range
of nonnegative integers (e.g., $1$--$4$). The range symbol `--' can be entered as \texttt{-} (hyphen) or \texttt{\char`\\\char`\<emdash\char`\>}.
-\item[$\bullet$] \qtybf{int\_seq}: A comma-separated sequence of ranges of integers (e.g.,~1{,}3{,}\allowbreak6--8).
-\item[$\bullet$] \qtybf{float\_or\_none}: An integer (e.g., 60) or floating-point number
+\item[\labelitemi] \qtybf{int\_seq}: A comma-separated sequence of ranges of integers (e.g.,~1{,}3{,}\allowbreak6--8).
+\item[\labelitemi] \qtybf{float\_or\_none}: An integer (e.g., 60) or floating-point number
(e.g., 0.5) expressing a number of seconds, or the keyword \textit{none}
($\infty$ seconds).
-\item[$\bullet$] \qtybf{const\/}: The name of a HOL constant.
-\item[$\bullet$] \qtybf{term}: A HOL term (e.g., ``$f~x$'').
-\item[$\bullet$] \qtybf{term\_list\/}: A space-separated list of HOL terms (e.g.,
+\item[\labelitemi] \qtybf{const\/}: The name of a HOL constant.
+\item[\labelitemi] \qtybf{term}: A HOL term (e.g., ``$f~x$'').
+\item[\labelitemi] \qtybf{term\_list\/}: A space-separated list of HOL terms (e.g.,
``$f~x$''~``$g~y$'').
-\item[$\bullet$] \qtybf{type}: A HOL type.
+\item[\labelitemi] \qtybf{type}: A HOL type.
\end{enum}
Default values are indicated in curly brackets (\textrm{\{\}}). Boolean options
@@ -2032,17 +2036,17 @@
well-founded. The option can take the following values:
\begin{enum}
-\item[$\bullet$] \textbf{\textit{true}:} Tentatively treat the (co)in\-duc\-tive
+\item[\labelitemi] \textbf{\textit{true}:} Tentatively treat the (co)in\-duc\-tive
predicate as if it were well-founded. Since this is generally not sound when the
predicate is not well-founded, the counterexamples are tagged as ``quasi
genuine.''
-\item[$\bullet$] \textbf{\textit{false}:} Treat the (co)in\-duc\-tive predicate
+\item[\labelitemi] \textbf{\textit{false}:} Treat the (co)in\-duc\-tive predicate
as if it were not well-founded. The predicate is then unrolled as prescribed by
the \textit{star\_linear\_preds}, \textit{iter}~\qty{const}, and \textit{iter}
options.
-\item[$\bullet$] \textbf{\textit{smart}:} Try to prove that the inductive
+\item[\labelitemi] \textbf{\textit{smart}:} Try to prove that the inductive
predicate is well-founded using Isabelle's \textit{lexicographic\_order} and
\textit{size\_change} tactics. If this succeeds (or the predicate occurs with an
appropriate polarity in the formula to falsify), use an efficient fixed-point
@@ -2095,10 +2099,10 @@
counterexamples. The option can take the following values:
\begin{enum}
-\item[$\bullet$] \textbf{\textit{true}:} Box the specified type whenever
+\item[\labelitemi] \textbf{\textit{true}:} Box the specified type whenever
practicable.
-\item[$\bullet$] \textbf{\textit{false}:} Never box the type.
-\item[$\bullet$] \textbf{\textit{smart}:} Box the type only in contexts where it
+\item[\labelitemi] \textbf{\textit{false}:} Never box the type.
+\item[\labelitemi] \textbf{\textit{smart}:} Box the type only in contexts where it
is likely to help. For example, $n$-tuples where $n > 2$ and arguments to
higher-order functions are good candidates for boxing.
\end{enum}
@@ -2116,11 +2120,11 @@
option can then take the following values:
\begin{enum}
-\item[$\bullet$] \textbf{\textit{true}:} Finitize the datatype. Since this is
+\item[\labelitemi] \textbf{\textit{true}:} Finitize the datatype. Since this is
unsound, counterexamples generated under these conditions are tagged as ``quasi
genuine.''
-\item[$\bullet$] \textbf{\textit{false}:} Don't attempt to finitize the datatype.
-\item[$\bullet$] \textbf{\textit{smart}:}
+\item[\labelitemi] \textbf{\textit{false}:} Don't attempt to finitize the datatype.
+\item[\labelitemi] \textbf{\textit{smart}:}
If the datatype's constructors don't appear in the problem, perform a
monotonicity analysis to detect whether the datatype can be soundly finitized;
otherwise, don't finitize it.
@@ -2302,14 +2306,14 @@
Specifies the expected outcome, which must be one of the following:
\begin{enum}
-\item[$\bullet$] \textbf{\textit{genuine}:} Nitpick found a genuine counterexample.
-\item[$\bullet$] \textbf{\textit{quasi\_genuine}:} Nitpick found a ``quasi
+\item[\labelitemi] \textbf{\textit{genuine}:} Nitpick found a genuine counterexample.
+\item[\labelitemi] \textbf{\textit{quasi\_genuine}:} Nitpick found a ``quasi
genuine'' counterexample (i.e., a counterexample that is genuine unless
it contradicts a missing axiom or a dangerous option was used inappropriately).
-\item[$\bullet$] \textbf{\textit{potential}:} Nitpick found a potentially
+\item[\labelitemi] \textbf{\textit{potential}:} Nitpick found a potentially
spurious counterexample.
-\item[$\bullet$] \textbf{\textit{none}:} Nitpick found no counterexample.
-\item[$\bullet$] \textbf{\textit{unknown}:} Nitpick encountered some problem (e.g.,
+\item[\labelitemi] \textbf{\textit{none}:} Nitpick found no counterexample.
+\item[\labelitemi] \textbf{\textit{unknown}:} Nitpick encountered some problem (e.g.,
Kodkod ran out of memory).
\end{enum}
@@ -2337,7 +2341,7 @@
\begin{enum}
-\item[$\bullet$] \textbf{\textit{CryptoMiniSat}:} CryptoMiniSat is the winner of
+\item[\labelitemi] \textbf{\textit{CryptoMiniSat}:} CryptoMiniSat is the winner of
the 2010 SAT Race. To use CryptoMiniSat, set the environment variable
\texttt{CRYPTO\-MINISAT\_}\discretionary{}{}{}\texttt{HOME} to the directory that contains the \texttt{crypto\-minisat}
executable.%
@@ -2348,17 +2352,17 @@
\url{http://planete.inrialpes.fr/~soos/}\allowbreak\url{CryptoMiniSat2/index.php}.
Nitpick has been tested with version 2.51.
-\item[$\bullet$] \textbf{\textit{CryptoMiniSat\_JNI}:} The JNI (Java Native
+\item[\labelitemi] \textbf{\textit{CryptoMiniSat\_JNI}:} The JNI (Java Native
Interface) version of CryptoMiniSat is bundled with Kodkodi and is precompiled
for Linux and Mac~OS~X. It is also available from the Kodkod web site
\cite{kodkod-2009}.
-\item[$\bullet$] \textbf{\textit{Lingeling\_JNI}:}
+\item[\labelitemi] \textbf{\textit{Lingeling\_JNI}:}
Lingeling is an efficient solver written in C. The JNI (Java Native Interface)
version of Lingeling is bundled with Kodkodi and is precompiled for Linux and
Mac~OS~X. It is also available from the Kodkod web site \cite{kodkod-2009}.
-\item[$\bullet$] \textbf{\textit{MiniSat}:} MiniSat is an efficient solver
+\item[\labelitemi] \textbf{\textit{MiniSat}:} MiniSat is an efficient solver
written in \cpp{}. To use MiniSat, set the environment variable
\texttt{MINISAT\_HOME} to the directory that contains the \texttt{minisat}
executable.%
@@ -2367,13 +2371,13 @@
\url{http://minisat.se/MiniSat.html}. Nitpick has been tested with versions 1.14
and 2.2.
-\item[$\bullet$] \textbf{\textit{MiniSat\_JNI}:} The JNI
+\item[\labelitemi] \textbf{\textit{MiniSat\_JNI}:} The JNI
version of MiniSat is bundled with Kodkodi and is precompiled for Linux,
Mac~OS~X, and Windows (Cygwin). It is also available from the Kodkod web site
\cite{kodkod-2009}. Unlike the standard version of MiniSat, the JNI version can
be used incrementally.
-\item[$\bullet$] \textbf{\textit{zChaff}:} zChaff is an older solver written
+\item[\labelitemi] \textbf{\textit{zChaff}:} zChaff is an older solver written
in \cpp{}. To use zChaff, set the environment variable \texttt{ZCHAFF\_HOME} to
the directory that contains the \texttt{zchaff} executable.%
\footref{cygwin-paths}
@@ -2381,7 +2385,7 @@
\url{http://www.princeton.edu/~chaff/zchaff.html}. Nitpick has been tested with
versions 2004-05-13, 2004-11-15, and 2007-03-12.
-\item[$\bullet$] \textbf{\textit{RSat}:} RSat is an efficient solver written in
+\item[\labelitemi] \textbf{\textit{RSat}:} RSat is an efficient solver written in
\cpp{}. To use RSat, set the environment variable \texttt{RSAT\_HOME} to the
directory that contains the \texttt{rsat} executable.%
\footref{cygwin-paths}
@@ -2389,30 +2393,30 @@
\url{http://reasoning.cs.ucla.edu/rsat/}. Nitpick has been tested with version
2.01.
-\item[$\bullet$] \textbf{\textit{BerkMin}:} BerkMin561 is an efficient solver
+\item[\labelitemi] \textbf{\textit{BerkMin}:} BerkMin561 is an efficient solver
written in C. To use BerkMin, set the environment variable
\texttt{BERKMIN\_HOME} to the directory that contains the \texttt{BerkMin561}
executable.\footref{cygwin-paths}
The BerkMin executables are available at
\url{http://eigold.tripod.com/BerkMin.html}.
-\item[$\bullet$] \textbf{\textit{BerkMin\_Alloy}:} Variant of BerkMin that is
+\item[\labelitemi] \textbf{\textit{BerkMin\_Alloy}:} Variant of BerkMin that is
included with Alloy 4 and calls itself ``sat56'' in its banner text. To use this
version of BerkMin, set the environment variable
\texttt{BERKMINALLOY\_HOME} to the directory that contains the \texttt{berkmin}
executable.%
\footref{cygwin-paths}
-\item[$\bullet$] \textbf{\textit{SAT4J}:} SAT4J is a reasonably efficient solver
+\item[\labelitemi] \textbf{\textit{SAT4J}:} SAT4J is a reasonably efficient solver
written in Java that can be used incrementally. It is bundled with Kodkodi and
requires no further installation or configuration steps. Do not attempt to
install the official SAT4J packages, because their API is incompatible with
Kodkod.
-\item[$\bullet$] \textbf{\textit{SAT4J\_Light}:} Variant of SAT4J that is
+\item[\labelitemi] \textbf{\textit{SAT4J\_Light}:} Variant of SAT4J that is
optimized for small problems. It can also be used incrementally.
-\item[$\bullet$] \textbf{\textit{smart}:} If \textit{sat\_solver} is set to
+\item[\labelitemi] \textbf{\textit{smart}:} If \textit{sat\_solver} is set to
\textit{smart}, Nitpick selects the first solver among the above that is
recognized by Isabelle. If \textit{verbose} (\S\ref{output-format}) is enabled,
Nitpick displays which SAT solver was chosen.
@@ -2837,7 +2841,7 @@
Here are the known bugs and limitations in Nitpick at the time of writing:
\begin{enum}
-\item[$\bullet$] Underspecified functions defined using the \textbf{primrec},
+\item[\labelitemi] Underspecified functions defined using the \textbf{primrec},
\textbf{function}, or \textbf{nominal\_\allowbreak primrec} packages can lead
Nitpick to generate spurious counterexamples for theorems that refer to values
for which the function is not defined. For example:
@@ -2858,33 +2862,33 @@
internal representation of functions synthesized by Isabelle, an implementation
detail.
-\item[$\bullet$] Similarly, Nitpick might find spurious counterexamples for
+\item[\labelitemi] Similarly, Nitpick might find spurious counterexamples for
theorems that rely on the use of the indefinite description operator internally
by \textbf{specification} and \textbf{quot\_type}.
-\item[$\bullet$] Axioms or definitions that restrict the possible values of the
+\item[\labelitemi] Axioms or definitions that restrict the possible values of the
\textit{undefined} constant or other partially specified built-in Isabelle
constants (e.g., \textit{Abs\_} and \textit{Rep\_} constants) are in general
ignored. Again, such nonconservative extensions are generally considered bad
style.
-\item[$\bullet$] Nitpick maintains a global cache of wellfoundedness conditions,
+\item[\labelitemi] Nitpick maintains a global cache of wellfoundedness conditions,
which can become invalid if you change the definition of an inductive predicate
that is registered in the cache. To clear the cache,
run Nitpick with the \textit{tac\_timeout} option set to a new value (e.g.,
$0.51$).
-\item[$\bullet$] Nitpick produces spurious counterexamples when invoked after a
+\item[\labelitemi] Nitpick produces spurious counterexamples when invoked after a
\textbf{guess} command in a structured proof.
-\item[$\bullet$] The \textit{nitpick\_xxx} attributes and the
+\item[\labelitemi] The \textit{nitpick\_xxx} attributes and the
\textit{Nitpick\_xxx.register\_yyy} functions can cause havoc if used
improperly.
-\item[$\bullet$] Although this has never been observed, arbitrary theorem
+\item[\labelitemi] Although this has never been observed, arbitrary theorem
morphisms could possibly confuse Nitpick, resulting in spurious counterexamples.
-\item[$\bullet$] All constants, types, free variables, and schematic variables
+\item[\labelitemi] All constants, types, free variables, and schematic variables
whose names start with \textit{Nitpick}{.} are reserved for internal use.
\end{enum}
--- a/doc-src/Sledgehammer/sledgehammer.tex Wed Nov 16 15:20:27 2011 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex Thu Nov 17 05:27:45 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}
@@ -649,16 +655,26 @@
The \textit{metis} proof method has the syntax
\prew
-\textbf{\textit{metis}}~(\qty{type\_enc})${}^?$~\qty{facts}${}^?$
+\textbf{\textit{metis}}~(\qty{options})${}^?$~\qty{facts}${}^?$
\postw
-where \qty{type\_enc} is a type encoding specification with the same semantics
-as Sledgehammer's \textit{type\_enc} option (\S\ref{problem-encoding}) and
-\qty{facts} is a list of arbitrary facts. In addition to the values listed in
-\S\ref{problem-encoding}, \qty{type\_enc} may also be \textit{full\_types}, in
-which case an appropriate type-sound encoding is chosen, \textit{partial\_types}
-(the default type-unsound encoding), or \textit{no\_types}, a synonym for
-\textit{erased}.
+where \qty{facts} is a list of arbitrary facts and \qty{options} is a
+comma-separated list consisting of at most one $\lambda$ translation scheme
+specification with the same semantics as Sledgehammer's \textit{lam\_trans}
+option (\S\ref{problem-encoding}) and at most one type encoding specification
+with the same semantics as Sledgehammer's \textit{type\_enc} option
+(\S\ref{problem-encoding}).
+%
+The supported $\lambda$ translation schemes are \textit{hide\_lams},
+\textit{lam\_lifting}, and \textit{combinators} (the default).
+%
+All the untyped type encodings listed in \S\ref{problem-encoding} are supported.
+For convenience, the following aliases are provided:
+\begin{enum}
+\item[\labelitemi] \textbf{\textit{full\_types}:} An appropriate type-sound encoding.
+\item[\labelitemi] \textbf{\textit{partial\_types}:} Synonym for \textit{poly\_args}.
+\item[\labelitemi] \textbf{\textit{no\_types}:} Synonym for \textit{erased}.
+\end{enum}
\section{Option Reference}
\label{option-reference}
@@ -686,16 +702,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 +730,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 +799,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 +829,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 +917,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 +962,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 +988,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 +996,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 +1025,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 +1034,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 +1042,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 +1058,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 +1067,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 +1075,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 +1169,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/ATP.thy Wed Nov 16 15:20:27 2011 +0100
+++ b/src/HOL/ATP.thy Thu Nov 17 05:27:45 2011 +0100
@@ -12,9 +12,9 @@
"Tools/ATP/atp_util.ML"
"Tools/ATP/atp_problem.ML"
"Tools/ATP/atp_proof.ML"
- "Tools/ATP/atp_systems.ML"
("Tools/ATP/atp_translate.ML")
("Tools/ATP/atp_reconstruct.ML")
+ ("Tools/ATP/atp_systems.ML")
begin
subsection {* Higher-order reasoning helpers *}
@@ -50,6 +50,7 @@
use "Tools/ATP/atp_translate.ML"
use "Tools/ATP/atp_reconstruct.ML"
+use "Tools/ATP/atp_systems.ML"
setup ATP_Systems.setup
--- a/src/HOL/Metis.thy Wed Nov 16 15:20:27 2011 +0100
+++ b/src/HOL/Metis.thy Thu Nov 17 05:27:45 2011 +0100
@@ -15,7 +15,7 @@
("Tools/try_methods.ML")
begin
-subsection {* Literal selection helpers *}
+subsection {* Literal selection and lambda-lifting helpers *}
definition select :: "'a \<Rightarrow> 'a" where
[no_atp]: "select = (\<lambda>x. x)"
@@ -31,6 +31,12 @@
lemma select_FalseI: "False \<Longrightarrow> select False" by simp
+definition lambda :: "'a \<Rightarrow> 'a" where
+[no_atp]: "lambda = (\<lambda>x. x)"
+
+lemma eq_lambdaI: "x \<equiv> y \<Longrightarrow> x \<equiv> lambda y"
+unfolding lambda_def by assumption
+
subsection {* Metis package *}
@@ -40,10 +46,11 @@
setup {* Metis_Tactic.setup *}
-hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal select
+hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal select lambda
hide_fact (open) fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def
fequal_def select_def not_atomize atomize_not_select not_atomize_select
- select_FalseI
+ select_FalseI lambda_def eq_lambdaI
+
subsection {* Try Methods *}
--- a/src/HOL/Metis_Examples/Type_Encodings.thy Wed Nov 16 15:20:27 2011 +0100
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy Thu Nov 17 05:27:45 2011 +0100
@@ -72,7 +72,7 @@
| tac (type_enc :: type_encs) st =
st (* |> tap (fn _ => tracing (PolyML.makestring type_enc)) *)
|> ((if null type_encs then all_tac else rtac @{thm fork} 1)
- THEN Metis_Tactic.metis_tac [type_enc] ctxt ths 1
+ THEN Metis_Tactic.metis_tac [type_enc] "combinators" ctxt ths 1
THEN COND (has_fewer_prems 2) all_tac no_tac
THEN tac type_encs)
in tac end
--- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Wed Nov 16 15:20:27 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Thu Nov 17 05:27:45 2011 +0100
@@ -18,7 +18,8 @@
val facts = Facts.props (Proof_Context.facts_of (Proof.context_of pre))
- fun metis ctxt = Metis_Tactic.metis_tac [] ctxt (thms @ facts)
+ fun metis ctxt =
+ Metis_Tactic.metis_tac [] ATP_Translate.lam_liftingN ctxt (thms @ facts)
in
(if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
|> prefix (metis_tag id)
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Nov 16 15:20:27 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Nov 17 05:27:45 2011 +0100
@@ -11,7 +11,7 @@
val type_encK = "type_enc"
val soundK = "sound"
val slicingK = "slicing"
-val lambda_translationK = "lambda_translation"
+val lam_transK = "lam_trans"
val e_weight_methodK = "e_weight_method"
val force_sosK = "force_sos"
val max_relevantK = "max_relevant"
@@ -343,10 +343,16 @@
(case AList.lookup (op =) args reconstructorK of
SOME name => name
| NONE =>
- if String.isSubstring "metis (full_types)" msg then "metis (full_types)"
- else if String.isSubstring "metis (no_types)" msg then "metis (no_types)"
- else if String.isSubstring "metis" msg then "metis"
- else "smt")
+ if String.isSubstring "metis (" msg then
+ msg |> Substring.full
+ |> Substring.position "metis ("
+ |> snd |> Substring.position ")"
+ |> fst |> Substring.string
+ |> suffix ")"
+ else if String.isSubstring "metis" msg then
+ "metis"
+ else
+ "smt")
local
@@ -355,9 +361,8 @@
SH_FAIL of int * int |
SH_ERROR
-fun run_sh prover_name prover type_enc sound max_relevant slicing
- lambda_translation e_weight_method force_sos hard_timeout timeout dir
- pos st =
+fun run_sh prover_name prover type_enc sound max_relevant slicing lam_trans
+ e_weight_method force_sos hard_timeout timeout dir pos st =
let
val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
val i = 1
@@ -372,9 +377,6 @@
val st' =
st |> Proof.map_context
(set_file_name dir
- #> (Option.map (Config.put
- Sledgehammer_Provers.atp_lambda_translation)
- lambda_translation |> the_default I)
#> (Option.map (Config.put ATP_Systems.e_weight_method)
e_weight_method |> the_default I)
#> (Option.map (Config.put ATP_Systems.force_sos)
@@ -384,6 +386,7 @@
[("verbose", "true"),
("type_enc", type_enc),
("sound", sound),
+ ("lam_trans", lam_trans |> the_default "smart"),
("preplay_timeout", preplay_timeout),
("max_relevant", max_relevant),
("slicing", slicing),
@@ -406,7 +409,8 @@
| SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
fun failed failure =
({outcome = SOME failure, used_facts = [], run_time = Time.zeroTime,
- preplay = K (ATP_Reconstruct.Failed_to_Play ATP_Reconstruct.Metis),
+ preplay =
+ K (ATP_Reconstruct.Failed_to_Play Sledgehammer_Provers.plain_metis),
message = K "", message_tail = ""}, ~1)
val ({outcome, used_facts, run_time, preplay, message, message_tail}
: Sledgehammer_Provers.prover_result,
@@ -428,7 +432,7 @@
subgoal_count = Sledgehammer_Util.subgoal_count st,
facts = facts |> map Sledgehammer_Provers.Untranslated_Fact,
smt_filter = NONE}
- in prover params (K (K "")) problem end)) ()
+ in prover params (K (K (K ""))) problem end)) ()
handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut
| Fail "inappropriate" => failed ATP_Proof.Inappropriate
val time_prover = run_time |> Time.toMilliseconds
@@ -466,7 +470,7 @@
val sound = AList.lookup (op =) args soundK |> the_default "false"
val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"
val slicing = AList.lookup (op =) args slicingK |> the_default "true"
- val lambda_translation = AList.lookup (op =) args lambda_translationK
+ val lam_trans = AList.lookup (op =) args lam_transK
val e_weight_method = AList.lookup (op =) args e_weight_methodK
val force_sos = AList.lookup (op =) args force_sosK
|> Option.map (curry (op <>) "false")
@@ -476,9 +480,8 @@
minimizer has a chance to do its magic *)
val hard_timeout = SOME (2 * timeout)
val (msg, result) =
- run_sh prover_name prover type_enc sound max_relevant slicing
- lambda_translation e_weight_method force_sos hard_timeout timeout dir
- pos st
+ run_sh prover_name prover type_enc sound max_relevant slicing lam_trans
+ e_weight_method force_sos hard_timeout timeout dir pos st
in
case result of
SH_OK (time_isa, time_prover, names) =>
@@ -578,15 +581,25 @@
ORELSE' sledge_tac 0.2 ATP_Systems.eN "mono_guards??"
ORELSE' sledge_tac 0.2 ATP_Systems.vampireN "mono_guards??"
ORELSE' sledge_tac 0.2 ATP_Systems.spassN "poly_tags"
- ORELSE' Metis_Tactic.metis_tac [] ctxt thms
+ ORELSE' Metis_Tactic.metis_tac [] ATP_Translate.combinatorsN ctxt thms
else if !reconstructor = "smt" then
SMT_Solver.smt_tac ctxt thms
- else if full orelse !reconstructor = "metis (full_types)" then
- Metis_Tactic.metis_tac [Metis_Tactic.full_type_enc] ctxt thms
- else if !reconstructor = "metis (no_types)" then
- Metis_Tactic.metis_tac [Metis_Tactic.no_type_enc] ctxt thms
+ else if full then
+ Metis_Tactic.metis_tac [ATP_Reconstruct.full_typesN]
+ ATP_Reconstruct.metis_default_lam_trans ctxt thms
+ else if String.isPrefix "metis (" (!reconstructor) then
+ let
+ val (type_encs, lam_trans) =
+ !reconstructor
+ |> Outer_Syntax.scan Position.start
+ |> filter Token.is_proper |> tl
+ |> Metis_Tactic.parse_metis_options |> fst
+ |>> the_default [ATP_Reconstruct.partial_typesN]
+ ||> the_default ATP_Reconstruct.metis_default_lam_trans
+ in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end
else if !reconstructor = "metis" then
- Metis_Tactic.metis_tac [] ctxt thms
+ Metis_Tactic.metis_tac [] ATP_Reconstruct.metis_default_lam_trans ctxt
+ thms
else
K all_tac
end
--- a/src/HOL/Rat.thy Wed Nov 16 15:20:27 2011 +0100
+++ b/src/HOL/Rat.thy Thu Nov 17 05:27:45 2011 +0100
@@ -1154,7 +1154,7 @@
begin
definition
- "exhaustive f d = exhaustive (%k. exhaustive (%l. f (Fract (Code_Numeral.int_of k) (Code_Numeral.int_of l))) d) d"
+ "exhaustive f d = exhaustive (%l. exhaustive (%k. f (Fract k (Code_Numeral.int_of l + 1))) d) d"
instance ..
@@ -1164,8 +1164,9 @@
begin
definition
- "full_exhaustive f d = full_exhaustive (%(k, kt). full_exhaustive (%(l, lt).
- f (valterm_fract (Code_Numeral.int_of k, %_. Code_Evaluation.term_of (Code_Numeral.int_of k)) (Code_Numeral.int_of l, %_. Code_Evaluation.term_of (Code_Numeral.int_of l)))) d) d"
+ "full_exhaustive f d = full_exhaustive (%(l, _). full_exhaustive (%k.
+ f (let j = Code_Numeral.int_of l + 1
+ in valterm_fract k (j, %_. Code_Evaluation.term_of j))) d) d"
instance ..
@@ -1181,16 +1182,17 @@
lemma [code]:
"partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Var p tt) == Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Rat.rat'') [])"
"partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Ctr 0 [l, k]) ==
- Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.Const (STR ''Rat.Fract'')
- (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Int.int'') [],
- Typerep.Typerep (STR ''Rat.rat'') []]])) (partial_term_of (TYPE(int)) l)) (partial_term_of (TYPE(int)) k)"
+ Code_Evaluation.App (Code_Evaluation.Const (STR ''Rat.Frct'')
+ (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Product_Type.prod'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Int.int'') []],
+ Typerep.Typerep (STR ''Rat.rat'') []])) (Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.Const (STR ''Product_Type.Pair'') (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Product_Type.prod'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Int.int'') []]]])) (partial_term_of (TYPE(int)) l)) (partial_term_of (TYPE(int)) k))"
by (rule partial_term_of_anything)+
instantiation rat :: narrowing
begin
definition
- "narrowing = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.apply (Quickcheck_Narrowing.cons Fract) narrowing) narrowing"
+ "narrowing = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.apply
+ (Quickcheck_Narrowing.cons (%nom denom. Fract nom denom)) narrowing) narrowing"
instance ..
--- a/src/HOL/TPTP/CASC_Setup.thy Wed Nov 16 15:20:27 2011 +0100
+++ b/src/HOL/TPTP/CASC_Setup.thy Thu Nov 17 05:27:45 2011 +0100
@@ -131,7 +131,7 @@
Sledgehammer_Filter.no_relevance_override))
ORELSE
SOLVE_TIMEOUT (max_secs div 10) "metis"
- (ALLGOALS (Metis_Tactic.metis_tac [] ctxt []))
+ (ALLGOALS (Metis_Tactic.metis_tac [] ATP_Translate.lam_liftingN ctxt []))
ORELSE
SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt))
ORELSE
--- a/src/HOL/TPTP/atp_export.ML Wed Nov 16 15:20:27 2011 +0100
+++ b/src/HOL/TPTP/atp_export.ML Thu Nov 17 05:27:45 2011 +0100
@@ -175,7 +175,7 @@
val path = file_name |> Path.explode
val _ = File.write path ""
val facts = facts_of thy
- val (atp_problem, _, _, _, _, _, _) =
+ val (atp_problem, _, _, _, _, _, _, _) =
facts
|> map (fn ((_, loc), th) =>
((Thm.get_name_hint th, loc),
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Nov 16 15:20:27 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Thu Nov 17 05:27:45 2011 +0100
@@ -14,9 +14,7 @@
type locality = ATP_Translate.locality
datatype reconstructor =
- Metis |
- Metis_Full_Types |
- Metis_No_Types |
+ Metis of string * string |
SMT
datatype play =
@@ -30,6 +28,18 @@
type isar_params =
bool * bool * int * string Symtab.table * int list list * int
* (string * locality) list vector * int Symtab.table * string proof * thm
+
+ val metisN : string
+ val smtN : string
+ val full_typesN : string
+ val partial_typesN : string
+ val no_typesN : string
+ val really_full_type_enc : string
+ val full_type_enc : string
+ val partial_type_enc : string
+ val no_type_enc : string
+ val full_type_encs : string list
+ val partial_type_encs : string list
val used_facts_in_atp_proof :
Proof.context -> int -> (string * locality) list vector -> string proof
-> (string * locality) list
@@ -37,6 +47,9 @@
Proof.context -> int list list -> int -> (string * locality) list vector
-> 'a proof -> string list option
val uses_typed_helpers : int list -> 'a proof -> bool
+ val unalias_type_enc : string -> string list
+ val metis_default_lam_trans : string
+ val metis_call : string -> string -> string
val name_of_reconstructor : reconstructor -> string
val one_line_proof_text : one_line_params -> string
val make_tvar : string -> typ
@@ -62,9 +75,7 @@
open ATP_Translate
datatype reconstructor =
- Metis |
- Metis_Full_Types |
- Metis_No_Types |
+ Metis of string * string |
SMT
datatype play =
@@ -188,13 +199,48 @@
| _ => false)
-(** Soft-core proof reconstruction: Metis one-liner **)
+(** Soft-core proof reconstruction: one-liners **)
+
+val metisN = "metis"
+val smtN = "smt"
+
+val full_typesN = "full_types"
+val partial_typesN = "partial_types"
+val no_typesN = "no_types"
+
+val really_full_type_enc = "mono_tags"
+val full_type_enc = "poly_guards_query"
+val partial_type_enc = "poly_args"
+val no_type_enc = "erased"
+
+val full_type_encs = [full_type_enc, really_full_type_enc]
+val partial_type_encs = partial_type_enc :: full_type_encs
+
+val type_enc_aliases =
+ [(full_typesN, full_type_encs),
+ (partial_typesN, partial_type_encs),
+ (no_typesN, [no_type_enc])]
+
+fun unalias_type_enc s =
+ AList.lookup (op =) type_enc_aliases s |> the_default [s]
+
+val metis_default_lam_trans = combinatorsN
+
+fun metis_call type_enc lam_trans =
+ let
+ val type_enc =
+ case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases
+ type_enc of
+ [alias] => alias
+ | _ => type_enc
+ val opts = [] |> type_enc <> partial_typesN ? cons type_enc
+ |> lam_trans <> metis_default_lam_trans ? cons lam_trans
+ in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end
(* unfortunate leaking abstraction *)
-fun name_of_reconstructor Metis = "metis"
- | name_of_reconstructor Metis_Full_Types = "metis (full_types)"
- | name_of_reconstructor Metis_No_Types = "metis (no_types)"
- | name_of_reconstructor SMT = "smt"
+fun name_of_reconstructor (Metis (type_enc, lam_trans)) =
+ metis_call type_enc lam_trans
+ | name_of_reconstructor SMT = smtN
fun string_for_label (s, num) = s ^ string_of_int num
@@ -213,9 +259,9 @@
fun using_labels [] = ""
| using_labels ls =
"using " ^ space_implode " " (map string_for_label ls) ^ " "
-fun reconstructor_command reconstructor i n (ls, ss) =
+fun reconstructor_command reconstr i n (ls, ss) =
using_labels ls ^ apply_on_subgoal i n ^
- command_call (name_of_reconstructor reconstructor) ss
+ command_call (name_of_reconstructor reconstr) ss
fun minimize_line _ [] = ""
| minimize_line minimize_command ss =
case minimize_command ss of
@@ -230,20 +276,19 @@
subgoal, subgoal_count) =
let
val (chained, extra) = split_used_facts used_facts
- val (failed, reconstructor, ext_time) =
+ val (failed, reconstr, ext_time) =
case preplay of
- Played (reconstructor, time) =>
- (false, reconstructor, (SOME (false, time)))
- | Trust_Playable (reconstructor, time) =>
- (false, reconstructor,
+ Played (reconstr, time) => (false, reconstr, (SOME (false, time)))
+ | Trust_Playable (reconstr, time) =>
+ (false, reconstr,
case time of
NONE => NONE
| SOME time =>
if time = Time.zeroTime then NONE else SOME (true, time))
- | Failed_to_Play reconstructor => (true, reconstructor, NONE)
+ | Failed_to_Play reconstr => (true, reconstr, NONE)
val try_line =
([], map fst extra)
- |> reconstructor_command reconstructor subgoal subgoal_count
+ |> reconstructor_command reconstr subgoal subgoal_count
|> (if failed then enclose "One-line proof reconstruction failed: " "."
else try_command_line banner ext_time)
in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end
@@ -283,26 +328,26 @@
constrained by information from type literals, or by type inference. *)
fun typ_from_atp ctxt (u as ATerm (a, us)) =
let val Ts = map (typ_from_atp ctxt) us in
- case strip_prefix_and_unascii type_const_prefix a of
+ case unprefix_and_unascii type_const_prefix a of
SOME b => Type (invert_const b, Ts)
| NONE =>
if not (null us) then
raise HO_TERM [u] (* only "tconst"s have type arguments *)
- else case strip_prefix_and_unascii tfree_prefix a of
+ else case unprefix_and_unascii tfree_prefix a of
SOME b => make_tfree ctxt b
| NONE =>
(* Could be an Isabelle variable or a variable from the ATP, say "X1"
or "_5018". Sometimes variables from the ATP are indistinguishable
from Isabelle variables, which forces us to use a type parameter in
all cases. *)
- (a |> perhaps (strip_prefix_and_unascii tvar_prefix), HOLogic.typeS)
+ (a |> perhaps (unprefix_and_unascii tvar_prefix), HOLogic.typeS)
|> Type_Infer.param 0
end
(* Type class literal applied to a type. Returns triple of polarity, class,
type. *)
fun type_constraint_from_term ctxt (u as ATerm (a, us)) =
- case (strip_prefix_and_unascii class_prefix a, map (typ_from_atp ctxt) us) of
+ case (unprefix_and_unascii class_prefix a, map (typ_from_atp ctxt) us) of
(SOME b, [T]) => (b, T)
| _ => raise HO_TERM [u]
@@ -335,6 +380,8 @@
fun num_type_args thy s =
if String.isPrefix skolem_const_prefix s then
s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
+ else if String.isPrefix lambda_lifted_prefix s then
+ if String.isPrefix lambda_lifted_poly_prefix s then 2 else 0
else
(s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
@@ -364,7 +411,7 @@
else
list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
end
- else case strip_prefix_and_unascii const_prefix s of
+ else case unprefix_and_unascii const_prefix s of
SOME s' =>
let
val ((s', s''), mangled_us) =
@@ -429,12 +476,10 @@
SOME T => map slack_fastype_of term_ts ---> T
| NONE => map slack_fastype_of ts ---> HOLogic.typeT
val t =
- case strip_prefix_and_unascii fixed_var_prefix s of
- SOME s =>
- (* FIXME: reconstruction of lambda-lifting *)
- Free (s, T)
+ case unprefix_and_unascii fixed_var_prefix s of
+ SOME s => Free (s, T)
| NONE =>
- case strip_prefix_and_unascii schematic_var_prefix s of
+ case unprefix_and_unascii schematic_var_prefix s of
SOME s => Var ((s, var_index), T)
| NONE =>
Var ((s |> textual ? repair_variable_name Char.toLower,
@@ -964,9 +1009,10 @@
else
if member (op =) qs Show then "show" else "have")
val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
- val reconstructor = if full_types then Metis_Full_Types else Metis
+ val reconstr =
+ Metis (if full_types then full_typesN else partial_typesN, combinatorsN)
fun do_facts (ls, ss) =
- reconstructor_command reconstructor 1 1
+ reconstructor_command reconstr 1 1
(ls |> sort_distinct (prod_ord string_ord int_ord),
ss |> sort_distinct string_ord)
and do_step ind (Fix xs) =
--- a/src/HOL/Tools/ATP/atp_systems.ML Wed Nov 16 15:20:27 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Nov 17 05:27:45 2011 +0100
@@ -23,7 +23,7 @@
prem_kind : formula_kind,
best_slices :
Proof.context
- -> (real * (bool * (int * atp_format * string * string))) list}
+ -> (real * (bool * (int * atp_format * string * string * string))) list}
val force_sos : bool Config.T
val e_smartN : string
@@ -56,7 +56,8 @@
val remote_atp :
string -> string -> string list -> (string * string) list
-> (failure * string) list -> formula_kind -> formula_kind
- -> (Proof.context -> int * atp_format * string) -> string * atp_config
+ -> (Proof.context -> int * atp_format * string * string)
+ -> string * atp_config
val add_atp : string * atp_config -> theory -> theory
val get_atp : theory -> string -> atp_config
val supported_atps : theory -> string list
@@ -70,6 +71,7 @@
open ATP_Problem
open ATP_Proof
+open ATP_Translate
(* ATP configuration *)
@@ -85,15 +87,16 @@
prem_kind : formula_kind,
best_slices :
Proof.context
- -> (real * (bool * (int * atp_format * string * string))) list}
+ -> (real * (bool * (int * atp_format * string * string * string))) list}
(* "best_slices" must be found empirically, taking a wholistic approach since
the ATPs are run in parallel. The "real" components give the faction of the
time available given to the slice and should add up to 1.0. The "bool"
component indicates whether the slice's strategy is complete; the "int", the
preferred number of facts to pass; the first "string", the preferred type
- system (which should be sound or quasi-sound); the second "string", extra
- information to the prover (e.g., SOS or no SOS).
+ system (which should be sound or quasi-sound); the second "string", the
+ preferred lambda translation scheme; the third "string", extra information to
+ the prover (e.g., SOS or no SOS).
The last slice should be the most "normal" one, because it will get all the
time available if the other slices fail early and also because it is used if
@@ -242,11 +245,14 @@
let val method = effective_e_weight_method ctxt in
(* FUDGE *)
if method = e_smartN then
- [(0.333, (true, (500, FOF, "mono_tags??", e_fun_weightN))),
- (0.334, (true, (50, FOF, "mono_guards??", e_fun_weightN))),
- (0.333, (true, (1000, FOF, "mono_tags??", e_sym_offset_weightN)))]
+ [(0.333, (true, (500, FOF, "mono_tags??", combinatorsN,
+ e_fun_weightN))),
+ (0.334, (true, (50, FOF, "mono_guards??", combinatorsN,
+ e_fun_weightN))),
+ (0.333, (true, (1000, FOF, "mono_tags??", combinatorsN,
+ e_sym_offset_weightN)))]
else
- [(1.0, (true, (500, FOF, "mono_tags??", method)))]
+ [(1.0, (true, (500, FOF, "mono_tags??", combinatorsN, method)))]
end}
val e = (eN, e_config)
@@ -271,8 +277,10 @@
prem_kind = Hypothesis,
best_slices = fn ctxt =>
(* FUDGE *)
- [(0.667, (false, (150, leo2_thf0, "mono_simple_higher", sosN))),
- (0.333, (true, (50, leo2_thf0, "mono_simple_higher", no_sosN)))]
+ [(0.667, (false, (150, leo2_thf0, "mono_simple_higher", lam_liftingN,
+ sosN))),
+ (0.333, (true, (50, leo2_thf0, "mono_simple_higher", lam_liftingN,
+ no_sosN)))]
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
@@ -296,7 +304,8 @@
prem_kind = Hypothesis,
best_slices =
(* FUDGE *)
- K [(1.0, (true, (100, satallax_thf0, "mono_simple_higher", "")))]}
+ K [(1.0, (true, (100, satallax_thf0, "mono_simple_higher", keep_lamsN,
+ "")))]}
val satallax = (satallaxN, satallax_config)
@@ -326,9 +335,12 @@
prem_kind = Conjecture,
best_slices = fn ctxt =>
(* FUDGE *)
- [(0.333, (false, (150, DFG DFG_Unsorted, "mono_tags??", sosN))),
- (0.333, (false, (300, DFG DFG_Unsorted, "poly_tags??", sosN))),
- (0.334, (true, (50, DFG DFG_Unsorted, "mono_tags??", no_sosN)))]
+ [(0.333, (false, (150, DFG DFG_Unsorted, "mono_tags??", lam_liftingN,
+ sosN))),
+ (0.333, (false, (300, DFG DFG_Unsorted, "poly_tags??", lam_liftingN,
+ sosN))),
+ (0.334, (true, (50, DFG DFG_Unsorted, "mono_tags??", lam_liftingN,
+ no_sosN)))]
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
@@ -345,9 +357,12 @@
prem_kind = #prem_kind spass_config,
best_slices = fn ctxt =>
(* FUDGE *)
- [(0.333, (false, (150, DFG DFG_Sorted, "mono_simple", sosN))) (*,
- (0.333, (false, (300, DFG DFG_Sorted, "poly_tags??", sosN))),
- (0.334, (true, (50, DFG DFG_Sorted, "mono_simple", no_sosN)))*)]
+ [(0.333, (false, (150, DFG DFG_Sorted, "mono_simple", lam_liftingN,
+ sosN))) (*,
+ (0.333, (false, (300, DFG DFG_Sorted, "poly_tags??", lam_liftingN,
+ sosN))),
+ (0.334, (true, (50, DFG DFG_Sorted, "mono_simple", lam_liftingN,
+ no_sosN)))*)]
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
@@ -389,13 +404,16 @@
best_slices = fn ctxt =>
(* FUDGE *)
(if is_old_vampire_version () then
- [(0.333, (false, (150, FOF, "poly_guards??", sosN))),
- (0.333, (false, (500, FOF, "mono_tags??", sosN))),
- (0.334, (true, (50, FOF, "mono_guards??", no_sosN)))]
+ [(0.333, (false, (150, FOF, "poly_guards??", hybrid_lamsN, sosN))),
+ (0.333, (false, (500, FOF, "mono_tags??", hybrid_lamsN, sosN))),
+ (0.334, (true, (50, FOF, "mono_guards??", hybrid_lamsN, no_sosN)))]
else
- [(0.333, (false, (150, vampire_tff0, "poly_guards??", sosN))),
- (0.333, (false, (500, vampire_tff0, "mono_simple", sosN))),
- (0.334, (true, (50, vampire_tff0, "mono_simple", no_sosN)))])
+ [(0.333, (false, (150, vampire_tff0, "poly_guards??", hybrid_lamsN,
+ sosN))),
+ (0.333, (false, (500, vampire_tff0, "mono_simple", hybrid_lamsN,
+ sosN))),
+ (0.334, (true, (50, vampire_tff0, "mono_simple", hybrid_lamsN,
+ no_sosN)))])
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
@@ -417,10 +435,10 @@
prem_kind = Hypothesis,
best_slices =
(* FUDGE *)
- K [(0.5, (false, (250, z3_tff0, "mono_simple", ""))),
- (0.25, (false, (125, z3_tff0, "mono_simple", ""))),
- (0.125, (false, (62, z3_tff0, "mono_simple", ""))),
- (0.125, (false, (31, z3_tff0, "mono_simple", "")))]}
+ K [(0.5, (false, (250, z3_tff0, "mono_simple", combinatorsN, ""))),
+ (0.25, (false, (125, z3_tff0, "mono_simple", combinatorsN, ""))),
+ (0.125, (false, (62, z3_tff0, "mono_simple", combinatorsN, ""))),
+ (0.125, (false, (31, z3_tff0, "mono_simple", combinatorsN, "")))]}
val z3_tptp = (z3_tptpN, z3_tptp_config)
@@ -435,7 +453,10 @@
known_failures = known_szs_status_failures,
conj_sym_kind = Hypothesis,
prem_kind = Hypothesis,
- best_slices = K [(1.0, (false, (200, format, type_enc, "")))]}
+ best_slices =
+ K [(1.0, (false, (200, format, type_enc,
+ if is_format_higher_order format then keep_lamsN
+ else combinatorsN, "")))]}
val dummy_tff1_format = TFF (TPTP_Polymorphic, TPTP_Explicit)
val dummy_tff1_config = dummy_config dummy_tff1_format "poly_simple"
@@ -493,8 +514,8 @@
conj_sym_kind = conj_sym_kind,
prem_kind = prem_kind,
best_slices = fn ctxt =>
- let val (max_relevant, format, type_enc) = best_slice ctxt in
- [(1.0, (false, (max_relevant, format, type_enc, "")))]
+ let val (max_relevant, format, type_enc, lam_trans) = best_slice ctxt in
+ [(1.0, (false, (max_relevant, format, type_enc, lam_trans, "")))]
end}
fun remotify_config system_name system_versions best_slice
@@ -516,42 +537,43 @@
val remote_e =
remotify_atp e "EP" ["1.0", "1.1", "1.2"]
- (K (750, FOF, "mono_tags??") (* FUDGE *))
+ (K (750, FOF, "mono_tags??", combinatorsN) (* FUDGE *))
val remote_leo2 =
remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
- (K (100, leo2_thf0, "mono_simple_higher") (* FUDGE *))
+ (K (100, leo2_thf0, "mono_simple_higher", lam_liftingN) (* FUDGE *))
val remote_satallax =
remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
- (K (100, satallax_thf0, "mono_simple_higher") (* FUDGE *))
+ (K (100, satallax_thf0, "mono_simple_higher", keep_lamsN) (* FUDGE *))
val remote_vampire =
remotify_atp vampire "Vampire" ["1.8"]
- (K (250, FOF, "mono_guards??") (* FUDGE *))
+ (K (250, FOF, "mono_guards??", hybrid_lamsN) (* FUDGE *))
val remote_z3_tptp =
remotify_atp z3_tptp "Z3" ["3.0"]
- (K (250, z3_tff0, "mono_simple") (* FUDGE *))
+ (K (250, z3_tff0, "mono_simple", combinatorsN) (* FUDGE *))
val remote_e_sine =
remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
- Conjecture (K (500, FOF, "mono_guards??") (* FUDGE *))
+ Conjecture (K (500, FOF, "mono_guards??", combinatorsN) (* FUDGE *))
val remote_iprover =
remote_atp iproverN "iProver" [] [] [] Axiom Conjecture
- (K (150, FOF, "mono_guards??") (* FUDGE *))
+ (K (150, FOF, "mono_guards??", lam_liftingN) (* FUDGE *))
val remote_iprover_eq =
remote_atp iprover_eqN "iProver-Eq" [] [] [] Axiom Conjecture
- (K (150, FOF, "mono_guards??") (* FUDGE *))
+ (K (150, FOF, "mono_guards??", lam_liftingN) (* FUDGE *))
val remote_snark =
remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
- [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
- (K (100, explicit_tff0, "mono_simple") (* FUDGE *))
+ [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
+ (K (100, explicit_tff0, "mono_simple", lam_liftingN) (* FUDGE *))
val remote_e_tofof =
remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
- Hypothesis (K (150, explicit_tff0, "mono_simple") (* FUDGE *))
+ Hypothesis
+ (K (150, explicit_tff0, "mono_simple", lam_liftingN) (* FUDGE *))
val remote_waldmeister =
remote_atp waldmeisterN "Waldmeister" ["710"]
- [("#START OF PROOF", "Proved Goals:")]
- [(OutOfResources, "Too many function symbols"),
- (Crashed, "Unrecoverable Segmentation Fault")]
- Hypothesis Hypothesis
- (K (50, CNF_UEQ, "mono_tags??") (* FUDGE *))
+ [("#START OF PROOF", "Proved Goals:")]
+ [(OutOfResources, "Too many function symbols"),
+ (Crashed, "Unrecoverable Segmentation Fault")]
+ Hypothesis Hypothesis
+ (K (50, CNF_UEQ, "mono_tags??", combinatorsN) (* FUDGE *))
(* Setup *)
--- a/src/HOL/Tools/ATP/atp_translate.ML Wed Nov 16 15:20:27 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML Thu Nov 17 05:27:45 2011 +0100
@@ -31,13 +31,12 @@
val type_tag_idempotence : bool Config.T
val type_tag_arguments : bool Config.T
- val no_lambdasN : string
- val concealedN : string
- val liftingN : string
+ val no_lamsN : string
+ val hide_lamsN : string
+ val lam_liftingN : string
val combinatorsN : string
- val hybridN : string
- val lambdasN : string
- val smartN : string
+ val hybrid_lamsN : string
+ val keep_lamsN : string
val schematic_var_prefix : string
val fixed_var_prefix : string
val tvar_prefix : string
@@ -45,7 +44,9 @@
val const_prefix : string
val type_const_prefix : string
val class_prefix : string
- val polymorphic_free_prefix : string
+ val lambda_lifted_prefix : string
+ val lambda_lifted_mono_prefix : string
+ val lambda_lifted_poly_prefix : string
val skolem_const_prefix : string
val old_skolem_const_prefix : string
val new_skolem_const_prefix : string
@@ -59,6 +60,7 @@
val class_rel_clause_prefix : string
val arity_clause_prefix : string
val tfree_clause_prefix : string
+ val lambda_fact_prefix : string
val typed_helper_suffix : string
val untyped_helper_suffix : string
val type_tag_idempotence_helper_name : string
@@ -72,7 +74,7 @@
val prefixed_type_tag_name : string
val ascii_of : string -> string
val unascii_of : string -> string
- val strip_prefix_and_unascii : string -> string -> string option
+ val unprefix_and_unascii : string -> string -> string option
val proxy_table : (string * (string * (thm * (string * string)))) list
val proxify_const : string -> (string * string) option
val invert_const : string -> string
@@ -92,13 +94,16 @@
val unmangled_const : string -> string * (string, 'b) ho_term list
val unmangled_const_name : string -> string
val helper_table : ((string * bool) * thm list) list
+ val trans_lams_from_string :
+ Proof.context -> type_enc -> string -> term list -> term list * term list
val factsN : string
val prepare_atp_problem :
Proof.context -> atp_format -> formula_kind -> formula_kind -> type_enc
-> bool -> string -> bool -> bool -> term list -> term
-> ((string * locality) * term) list
-> string problem * string Symtab.table * int * int
- * (string * locality) list vector * int list * int Symtab.table
+ * (string * locality) list vector * int list * (string * term) list
+ * int Symtab.table
val atp_problem_weights : string problem -> (string * real) list
end;
@@ -115,13 +120,12 @@
val type_tag_arguments =
Attrib.setup_config_bool @{binding atp_type_tag_arguments} (K false)
-val no_lambdasN = "no_lambdas"
-val concealedN = "concealed"
-val liftingN = "lifting"
+val no_lamsN = "no_lams" (* used internally; undocumented *)
+val hide_lamsN = "hide_lams"
+val lam_liftingN = "lam_lifting"
val combinatorsN = "combinators"
-val hybridN = "hybrid"
-val lambdasN = "lambdas"
-val smartN = "smart"
+val hybrid_lamsN = "hybrid_lams"
+val keep_lamsN = "keep_lams"
(* TFF1 is still in development, and it is still unclear whether symbols will be
allowed to have types like "$tType > $o" (i.e., "![A : $tType] : $o"), with
@@ -140,7 +144,12 @@
val simple_type_prefix = "s_"
val class_prefix = "cl_"
-val polymorphic_free_prefix = "poly_free"
+(* Freshness almost guaranteed! *)
+val atp_weak_prefix = "ATP:"
+
+val lambda_lifted_prefix = atp_weak_prefix ^ "Lam"
+val lambda_lifted_mono_prefix = lambda_lifted_prefix ^ "m"
+val lambda_lifted_poly_prefix = lambda_lifted_prefix ^ "p"
val skolem_const_prefix = "ATP" ^ Long_Name.separator ^ "Sko"
val old_skolem_const_prefix = skolem_const_prefix ^ "o"
@@ -171,9 +180,6 @@
val prefixed_app_op_name = const_prefix ^ app_op_name
val prefixed_type_tag_name = const_prefix ^ type_tag_name
-(* Freshness almost guaranteed! *)
-val atp_weak_prefix = "ATP:"
-
(*Escaping of special characters.
Alphanumeric characters are left unchanged.
The character _ goes to __
@@ -223,7 +229,7 @@
(* If string s has the prefix s1, return the result of deleting it,
un-ASCII'd. *)
-fun strip_prefix_and_unascii s1 s =
+fun unprefix_and_unascii s1 s =
if String.isPrefix s1 s then
SOME (unascii_of (String.extract (s, size s1, NONE)))
else
@@ -468,18 +474,40 @@
fun atomic_types_of T = fold_atyps (insert (op =)) T []
+val tvar_a_str = "'a"
+val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
+val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str)
+val itself_name = `make_fixed_type_const @{type_name itself}
+val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
+val tvar_a_atype = AType (tvar_a_name, [])
+val a_itself_atype = AType (itself_name, [tvar_a_atype])
+
fun new_skolem_const_name s num_T_args =
[new_skolem_const_prefix, s, string_of_int num_T_args]
|> space_implode Long_Name.separator
fun robust_const_type thy s =
- if s = app_op_name then Logic.varifyT_global @{typ "('a => 'b) => 'a => 'b"}
- else s |> Sign.the_const_type thy
+ if s = app_op_name then
+ Logic.varifyT_global @{typ "('a => 'b) => 'a => 'b"}
+ else if String.isPrefix lambda_lifted_prefix s then
+ Logic.varifyT_global @{typ "'a => 'b"}
+ else
+ (* Old Skolems throw a "TYPE" exception here, which will be caught. *)
+ s |> Sign.the_const_type thy
(* This function only makes sense if "T" is as general as possible. *)
fun robust_const_typargs thy (s, T) =
- (s, T) |> Sign.const_typargs thy
- handle TYPE _ => [] |> Term.add_tvarsT T |> rev |> map TVar
+ if s = app_op_name then
+ let val (T1, T2) = T |> domain_type |> dest_funT in [T1, T2] end
+ else if String.isPrefix old_skolem_const_prefix s then
+ [] |> Term.add_tvarsT T |> rev |> map TVar
+ else if String.isPrefix lambda_lifted_prefix s then
+ if String.isPrefix lambda_lifted_poly_prefix s then
+ let val (T1, T2) = T |> dest_funT in [T1, T2] end
+ else
+ []
+ else
+ (s, T) |> Sign.const_typargs thy
(* Converts an Isabelle/HOL term (with combinators) into an intermediate term.
Also accumulates sort infomation. *)
@@ -493,9 +521,7 @@
robust_const_typargs thy (c, T)),
atomic_types_of T)
| iterm_from_term _ _ _ (Free (s, T)) =
- (IConst (`make_fixed_var s, T,
- if String.isPrefix polymorphic_free_prefix s then [T] else []),
- atomic_types_of T)
+ (IConst (`make_fixed_var s, T, []), atomic_types_of T)
| iterm_from_term _ format _ (Var (v as (s, _), T)) =
(if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
let
@@ -650,15 +676,27 @@
(if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff
| adjust_type_enc _ type_enc = type_enc
-fun lift_lambdas ctxt type_enc =
- map (close_form o Envir.eta_contract) #> rpair ctxt
+fun constify_lifted (t $ u) = constify_lifted t $ constify_lifted u
+ | constify_lifted (Abs (s, T, t)) = Abs (s, T, constify_lifted t)
+ | constify_lifted (Free (x as (s, _))) =
+ (if String.isPrefix lambda_lifted_prefix s then Const else Free) x
+ | constify_lifted t = t
+
+(* Requires bound variables to have distinct names and not to clash with any
+ schematic variables (as should be the case right after lambda-lifting). *)
+fun open_form (Const (@{const_name All}, _) $ Abs (s, T, t)) =
+ open_form (subst_bound (Var ((s, 0), T), t))
+ | open_form t = t
+
+fun lift_lams ctxt type_enc =
+ map (Envir.eta_contract #> close_form) #> rpair ctxt
#-> Lambda_Lifting.lift_lambdas
- (if polymorphism_of_type_enc type_enc = Polymorphic then
- SOME polymorphic_free_prefix
- else
- NONE)
+ (SOME (if polymorphism_of_type_enc type_enc = Polymorphic then
+ lambda_lifted_poly_prefix
+ else
+ lambda_lifted_mono_prefix))
Lambda_Lifting.is_quantifier
- #> fst
+ #> fst #> pairself (map (open_form o constify_lifted))
fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
intentionalize_def t
@@ -737,14 +775,6 @@
fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
| add_sorts_on_tvar _ = I
-val tvar_a_str = "'a"
-val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
-val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str)
-val itself_name = `make_fixed_type_const @{type_name itself}
-val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
-val tvar_a_atype = AType (tvar_a_name, [])
-val a_itself_atype = AType (itself_name, [tvar_a_atype])
-
fun type_class_formula type_enc class arg =
AAtom (ATerm (class, arg ::
(case type_enc of
@@ -947,7 +977,7 @@
fun mangle (IApp (tm1, tm2)) = IApp (mangle tm1, mangle tm2)
| mangle (tm as IConst (_, _, [])) = tm
| mangle (tm as IConst (name as (s, _), T, T_args)) =
- (case strip_prefix_and_unascii const_prefix s of
+ (case unprefix_and_unascii const_prefix s of
NONE => tm
| SOME s'' =>
case type_arg_policy type_enc (invert_const s'') of
@@ -983,7 +1013,7 @@
fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2)
| filt _ (tm as IConst (_, _, [])) = tm
| filt ary (IConst (name as (s, _), T, T_args)) =
- (case strip_prefix_and_unascii const_prefix s of
+ (case unprefix_and_unascii const_prefix s of
NONE =>
(name,
if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then
@@ -1117,8 +1147,8 @@
do_cheaply_conceal_lambdas Ts t1
$ do_cheaply_conceal_lambdas Ts t2
| do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) =
- Free (polymorphic_free_prefix ^ serial_string (),
- T --> fastype_of1 (T :: Ts, t))
+ Const (lambda_lifted_poly_prefix ^ serial_string (),
+ T --> fastype_of1 (T :: Ts, t))
| do_cheaply_conceal_lambdas _ t = t
fun do_introduce_combinators ctxt Ts t =
@@ -1133,10 +1163,10 @@
handle THM _ => t |> do_cheaply_conceal_lambdas Ts
val introduce_combinators = simple_translate_lambdas do_introduce_combinators
-fun preprocess_abstractions_in_terms trans_lambdas facts =
+fun preprocess_abstractions_in_terms trans_lams facts =
let
val (facts, lambda_ts) =
- facts |> map (snd o snd) |> trans_lambdas
+ facts |> map (snd o snd) |> trans_lams
|>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
val lambda_facts =
map2 (fn t => fn j =>
@@ -1202,7 +1232,7 @@
(** Finite and infinite type inference **)
fun tvar_footprint thy s ary =
- (case strip_prefix_and_unascii const_prefix s of
+ (case unprefix_and_unascii const_prefix s of
SOME s =>
s |> invert_const |> robust_const_type thy |> chop_fun ary |> fst
|> map (fn T => Term.add_tvarsT T [] |> map fst)
@@ -1425,7 +1455,7 @@
case Symtab.lookup sym_tab s of
SOME ({min_ary, ...} : sym_info) => min_ary
| NONE =>
- case strip_prefix_and_unascii const_prefix s of
+ case unprefix_and_unascii const_prefix s of
SOME s =>
let val s = s |> unmangled_const_name |> invert_const in
if s = predicator_name then 1
@@ -1560,7 +1590,7 @@
not (null (Term.hidden_polymorphism t))
fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
- case strip_prefix_and_unascii const_prefix s of
+ case unprefix_and_unascii const_prefix s of
SOME mangled_s =>
let
val thy = Proof_Context.theory_of ctxt
@@ -1629,11 +1659,6 @@
| add (t $ u) = add t #> add u
| add (Const x) =
x |> robust_const_typargs thy |> fold (fold_type_constrs set_insert)
- | add (Free (s, T)) =
- if String.isPrefix polymorphic_free_prefix s then
- T |> fold_type_constrs set_insert
- else
- I
| add (Abs (_, _, u)) = add u
| add _ = I
in add end
@@ -1641,10 +1666,37 @@
fun type_constrs_of_terms thy ts =
Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
-fun translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
- hyp_ts concl_t facts =
+fun extract_lambda_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
+ let val (head, args) = strip_comb t in
+ (head |> dest_Const |> fst,
+ fold_rev (fn t as Var ((s, _), T) =>
+ (fn u => Abs (s, T, abstract_over (t, u)))
+ | _ => raise Fail "expected Var") args u)
+ end
+ | extract_lambda_def _ = raise Fail "malformed lifted lambda"
+
+fun trans_lams_from_string ctxt type_enc lam_trans =
+ if lam_trans = no_lamsN then
+ rpair []
+ else if lam_trans = hide_lamsN then
+ lift_lams ctxt type_enc ##> K []
+ else if lam_trans = lam_liftingN then
+ lift_lams ctxt type_enc
+ else if lam_trans = combinatorsN then
+ map (introduce_combinators ctxt) #> rpair []
+ else if lam_trans = hybrid_lamsN then
+ lift_lams ctxt type_enc
+ ##> maps (fn t => [t, introduce_combinators ctxt (intentionalize_def t)])
+ else if lam_trans = keep_lamsN then
+ map (Envir.eta_contract) #> rpair []
+ else
+ error ("Unknown lambda translation scheme: " ^ quote lam_trans ^ ".")
+
+fun translate_formulas ctxt format prem_kind type_enc lam_trans presimp hyp_ts
+ concl_t facts =
let
val thy = Proof_Context.theory_of ctxt
+ val trans_lams = trans_lams_from_string ctxt type_enc lam_trans
val presimp_consts = Meson.presimplified_consts ctxt
val fact_ts = facts |> map snd
(* Remove existing facts from the conjecture, as this can dramatically
@@ -1657,14 +1709,16 @@
map (pair prem_kind) hyp_ts @ [(Conjecture, s_not_trueprop concl_t)]
|> map (apsnd freeze_term)
|> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts)
- val ((conjs, facts), lambdas) =
- if preproc then
- conjs @ facts
- |> map (apsnd (uncurry (presimp_prop ctxt presimp_consts)))
- |> preprocess_abstractions_in_terms trans_lambdas
- |>> chop (length conjs)
- else
- ((conjs, facts), [])
+ val ((conjs, facts), lambda_facts) =
+ (conjs, facts)
+ |> presimp
+ ? pairself (map (apsnd (uncurry (presimp_prop ctxt presimp_consts))))
+ |> (if lam_trans = no_lamsN then
+ rpair []
+ else
+ op @
+ #> preprocess_abstractions_in_terms trans_lams
+ #>> chop (length conjs))
val conjs = conjs |> make_conjecture ctxt format type_enc
val (fact_names, facts) =
facts
@@ -1672,8 +1726,10 @@
make_fact ctxt format type_enc true (name, t)
|> Option.map (pair name))
|> ListPair.unzip
- val lambdas =
- lambdas |> map_filter (make_fact ctxt format type_enc true o apsnd snd)
+ val lifted = lambda_facts |> map (extract_lambda_def o snd o snd)
+ val lambda_facts =
+ lambda_facts
+ |> map_filter (make_fact ctxt format type_enc true o apsnd snd)
val all_ts = concl_t :: hyp_ts @ fact_ts
val subs = tfree_classes_of_terms all_ts
val supers = tvar_classes_of_terms all_ts
@@ -1683,8 +1739,8 @@
else make_arity_clauses thy tycons supers
val class_rel_clauses = make_class_rel_clauses thy subs supers
in
- (fact_names |> map single, union (op =) subs supers, conjs, facts @ lambdas,
- class_rel_clauses, arity_clauses)
+ (fact_names |> map single, union (op =) subs supers, conjs,
+ facts @ lambda_facts, class_rel_clauses, arity_clauses, lifted)
end
val type_guard = `(make_fixed_const NONE) type_guard_name
@@ -2086,18 +2142,13 @@
val (T, T_args) =
if null T_args then
(T, [])
- else case strip_prefix_and_unascii const_prefix s of
+ else case unprefix_and_unascii const_prefix s of
SOME s' =>
let
val s' = s' |> invert_const
val T = s' |> robust_const_type thy
in (T, robust_const_typargs thy (s', T)) end
- | NONE =>
- case strip_prefix_and_unascii fixed_var_prefix s of
- SOME s' =>
- if String.isPrefix polymorphic_free_prefix s' then (tvar_a, [tvar_a])
- else raise Fail "unexpected type arguments to free variable"
- | NONE => raise Fail "unexpected type arguments"
+ | NONE => raise Fail "unexpected type arguments"
in
Decl (sym_decl_prefix ^ s, (s, s'),
T |> fused_type ctxt mono (level_of_type_enc type_enc) ary
@@ -2277,7 +2328,7 @@
val explicit_apply_threshold = 50
fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
- lambda_trans readable_names preproc hyp_ts concl_t facts =
+ lam_trans readable_names preproc hyp_ts concl_t facts =
let
val thy = Proof_Context.theory_of ctxt
val type_enc = type_enc |> adjust_type_enc format
@@ -2290,36 +2341,17 @@
NONE
else
SOME false
- val lambda_trans =
- if lambda_trans = smartN then
- if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
- else if lambda_trans = lambdasN andalso
- not (is_type_enc_higher_order type_enc) then
- error ("Lambda translation method incompatible with first-order \
+ val lam_trans =
+ if lam_trans = keep_lamsN andalso
+ not (is_type_enc_higher_order type_enc) then
+ error ("Lambda translation scheme incompatible with first-order \
\encoding.")
else
- lambda_trans
- val trans_lambdas =
- if lambda_trans = no_lambdasN then
- rpair []
- else if lambda_trans = concealedN then
- lift_lambdas ctxt type_enc ##> K []
- else if lambda_trans = liftingN then
- lift_lambdas ctxt type_enc
- else if lambda_trans = combinatorsN then
- map (introduce_combinators ctxt) #> rpair []
- else if lambda_trans = hybridN then
- lift_lambdas ctxt type_enc
- ##> maps (fn t => [t, introduce_combinators ctxt
- (intentionalize_def t)])
- else if lambda_trans = lambdasN then
- map (Envir.eta_contract) #> rpair []
- else
- error ("Unknown lambda translation method: " ^
- quote lambda_trans ^ ".")
- val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses) =
- translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
- hyp_ts concl_t facts
+ lam_trans
+ val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses,
+ lifted) =
+ translate_formulas ctxt format prem_kind type_enc lam_trans preproc hyp_ts
+ concl_t facts
val sym_tab =
sym_table_for_facts ctxt type_enc explicit_apply conjs facts
val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
@@ -2390,6 +2422,7 @@
offset_of_heading_in_problem factsN problem 0,
fact_names |> Vector.fromList,
typed_helpers,
+ lifted,
Symtab.empty |> Symtab.fold add_sym_ary sym_tab)
end
--- a/src/HOL/Tools/ATP/atp_util.ML Wed Nov 16 15:20:27 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML Thu Nov 17 05:27:45 2011 +0100
@@ -268,7 +268,8 @@
fun close_form t =
fold (fn ((x, i), T) => fn t' =>
- HOLogic.all_const T $ Abs (x, T, abstract_over (Var ((x, i), T), t')))
+ HOLogic.all_const T
+ $ Abs (x, T, abstract_over (Var ((x, i), T), t')))
(Term.add_vars t []) t
fun monomorphic_term subst =
--- a/src/HOL/Tools/Meson/meson_clausify.ML Wed Nov 16 15:20:27 2011 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Thu Nov 17 05:27:45 2011 +0100
@@ -10,12 +10,14 @@
val new_skolem_var_prefix : string
val new_nonskolem_var_prefix : string
val is_zapped_var_name : string -> bool
+ val is_quasi_lambda_free : term -> bool
val introduce_combinators_in_cterm : cterm -> thm
val introduce_combinators_in_theorem : thm -> thm
val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool
val ss_only : thm list -> simpset
val cnf_axiom :
- Proof.context -> bool -> int -> thm -> (thm * term) option * thm list
+ Proof.context -> bool -> bool -> int -> thm
+ -> (thm * term) option * thm list
end;
structure Meson_Clausify : MESON_CLAUSIFY =
@@ -173,7 +175,7 @@
(warning ("Error in the combinator translation of " ^
Display.string_of_thm_without_context th ^
"\nException message: " ^ msg ^ ".");
- (* A type variable of sort "{}" will make abstraction fail. *)
+ (* A type variable of sort "{}" will make "abstraction" fail. *)
TrueI)
(*cterms are used throughout for efficiency*)
@@ -364,7 +366,7 @@
end
(* Convert a theorem to CNF, with additional premises due to skolemization. *)
-fun cnf_axiom ctxt0 new_skolemizer ax_no th =
+fun cnf_axiom ctxt0 new_skolemizer combinators ax_no th =
let
val thy = Proof_Context.theory_of ctxt0
val choice_ths = choice_theorems thy
@@ -385,7 +387,7 @@
(opt |> Option.map (I #>> singleton (Variable.export ctxt ctxt0)
##> (term_of #> HOLogic.dest_Trueprop
#> singleton (Variable.export_terms ctxt ctxt0))),
- cnf_ths |> map (introduce_combinators_in_theorem
+ cnf_ths |> map (combinators ? introduce_combinators_in_theorem
#> (case opt of SOME (_, ct) => intr_imp ct | NONE => I))
|> Variable.export ctxt ctxt0
|> finish_cnf
--- a/src/HOL/Tools/Meson/meson_tactic.ML Wed Nov 16 15:20:27 2011 +0100
+++ b/src/HOL/Tools/Meson/meson_tactic.ML Thu Nov 17 05:27:45 2011 +0100
@@ -18,7 +18,7 @@
fun meson_general_tac ctxt ths =
let val ctxt' = put_claset HOL_cs ctxt
- in Meson.meson_tac ctxt' (maps (snd o cnf_axiom ctxt' false 0) ths) end
+ in Meson.meson_tac ctxt' (maps (snd o cnf_axiom ctxt' false true 0) ths) end
val setup =
Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Nov 16 15:20:27 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Thu Nov 17 05:27:45 2011 +0100
@@ -14,11 +14,12 @@
exception METIS of string * string
val hol_clause_from_metis :
- Proof.context -> type_enc -> int Symtab.table -> (string * term) list
- -> Metis_Thm.thm -> term
+ Proof.context -> type_enc -> int Symtab.table
+ -> (string * term) list * (string * term) list -> Metis_Thm.thm -> term
val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
val replay_one_inference :
- Proof.context -> type_enc -> (string * term) list -> int Symtab.table
+ Proof.context -> type_enc
+ -> (string * term) list * (string * term) list -> int Symtab.table
-> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
-> (Metis_Thm.thm * thm) list
val discharge_skolem_premises :
@@ -55,24 +56,23 @@
| atp_clause_from_metis type_enc lits =
lits |> map (atp_literal_from_metis type_enc) |> mk_aconns AOr
-fun reveal_old_skolems_and_infer_types ctxt old_skolems =
- map (reveal_old_skolem_terms old_skolems)
+fun polish_hol_terms ctxt (lifted, old_skolems) =
+ map (reveal_lambda_lifted lifted #> reveal_old_skolem_terms old_skolems)
#> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
-fun hol_clause_from_metis ctxt type_enc sym_tab old_skolems =
+fun hol_clause_from_metis ctxt type_enc sym_tab concealed =
Metis_Thm.clause
#> Metis_LiteralSet.toList
#> atp_clause_from_metis type_enc
#> prop_from_atp ctxt false sym_tab
- #> singleton (reveal_old_skolems_and_infer_types ctxt old_skolems)
+ #> singleton (polish_hol_terms ctxt concealed)
-fun hol_terms_from_metis ctxt type_enc old_skolems sym_tab fol_tms =
+fun hol_terms_from_metis ctxt type_enc concealed sym_tab fol_tms =
let val ts = map (hol_term_from_metis ctxt type_enc sym_tab) fol_tms
val _ = trace_msg ctxt (fn () => " calling type inference:")
val _ = app (fn t => trace_msg ctxt
(fn () => Syntax.string_of_term ctxt t)) ts
- val ts' =
- ts |> reveal_old_skolems_and_infer_types ctxt old_skolems
+ val ts' = ts |> polish_hol_terms ctxt concealed
val _ = app (fn t => trace_msg ctxt
(fn () => " final term: " ^ Syntax.string_of_term ctxt t ^
" of type " ^ Syntax.string_of_typ ctxt (type_of t)))
@@ -114,10 +114,10 @@
val substs = [(cterm_of thy (Var vx), cterm_of thy i_atom)]
in cterm_instantiate substs th end;
-fun assume_inference ctxt type_enc old_skolems sym_tab atom =
+fun assume_inference ctxt type_enc concealed sym_tab atom =
inst_excluded_middle
(Proof_Context.theory_of ctxt)
- (singleton (hol_terms_from_metis ctxt type_enc old_skolems sym_tab)
+ (singleton (hol_terms_from_metis ctxt type_enc concealed sym_tab)
(Metis_Term.Fn atom))
(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
@@ -125,14 +125,14 @@
sorts. Instead we try to arrange that new TVars are distinct and that types
can be inferred from terms. *)
-fun inst_inference ctxt type_enc old_skolems sym_tab th_pairs fsubst th =
+fun inst_inference ctxt type_enc concealed sym_tab th_pairs fsubst th =
let val thy = Proof_Context.theory_of ctxt
val i_th = lookth th_pairs th
val i_th_vars = Term.add_vars (prop_of i_th) []
fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
fun subst_translation (x,y) =
let val v = find_var x
- (* We call "reveal_old_skolems_and_infer_types" below. *)
+ (* We call "polish_hol_terms" below. *)
val t = hol_term_from_metis ctxt type_enc sym_tab y
in SOME (cterm_of thy (Var v), t) end
handle Option.Option =>
@@ -145,10 +145,10 @@
NONE)
fun remove_typeinst (a, t) =
let val a = Metis_Name.toString a in
- case strip_prefix_and_unascii schematic_var_prefix a of
+ case unprefix_and_unascii schematic_var_prefix a of
SOME b => SOME (b, t)
| NONE =>
- case strip_prefix_and_unascii tvar_prefix a of
+ case unprefix_and_unascii tvar_prefix a of
SOME _ => NONE (* type instantiations are forbidden *)
| NONE => SOME (a, t) (* internal Metis var? *)
end
@@ -156,7 +156,7 @@
val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
val (vars, tms) =
ListPair.unzip (map_filter subst_translation substs)
- ||> reveal_old_skolems_and_infer_types ctxt old_skolems
+ ||> polish_hol_terms ctxt concealed
val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
val substs' = ListPair.zip (vars, map ctm_of tms)
val _ = trace_msg ctxt (fn () =>
@@ -258,7 +258,7 @@
(* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
val select_literal = negate_head oo make_last
-fun resolve_inference ctxt type_enc old_skolems sym_tab th_pairs atom th1 th2 =
+fun resolve_inference ctxt type_enc concealed sym_tab th_pairs atom th1 th2 =
let
val (i_th1, i_th2) = pairself (lookth th_pairs) (th1, th2)
val _ = trace_msg ctxt (fn () =>
@@ -274,7 +274,7 @@
let
val thy = Proof_Context.theory_of ctxt
val i_atom =
- singleton (hol_terms_from_metis ctxt type_enc old_skolems sym_tab)
+ singleton (hol_terms_from_metis ctxt type_enc concealed sym_tab)
(Metis_Term.Fn atom)
val _ = trace_msg ctxt (fn () =>
" atom: " ^ Syntax.string_of_term ctxt i_atom)
@@ -303,11 +303,11 @@
val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
val refl_idx = 1 + Thm.maxidx_of REFL_THM;
-fun refl_inference ctxt type_enc old_skolems sym_tab t =
+fun refl_inference ctxt type_enc concealed sym_tab t =
let
val thy = Proof_Context.theory_of ctxt
val i_t =
- singleton (hol_terms_from_metis ctxt type_enc old_skolems sym_tab) t
+ singleton (hol_terms_from_metis ctxt type_enc concealed sym_tab) t
val _ = trace_msg ctxt (fn () => " term: " ^ Syntax.string_of_term ctxt i_t)
val c_t = cterm_incr_types thy refl_idx i_t
in cterm_instantiate [(refl_x, c_t)] REFL_THM end
@@ -317,11 +317,11 @@
val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
-fun equality_inference ctxt type_enc old_skolems sym_tab (pos, atom) fp fr =
+fun equality_inference ctxt type_enc concealed sym_tab (pos, atom) fp fr =
let val thy = Proof_Context.theory_of ctxt
val m_tm = Metis_Term.Fn atom
val [i_atom, i_tm] =
- hol_terms_from_metis ctxt type_enc old_skolems sym_tab [m_tm, fr]
+ hol_terms_from_metis ctxt type_enc concealed sym_tab [m_tm, fr]
val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
fun replace_item_list lx 0 (_::ls) = lx::ls
| replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
@@ -336,7 +336,7 @@
| path_finder tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
let
val s = s |> Metis_Name.toString
- |> perhaps (try (strip_prefix_and_unascii const_prefix
+ |> perhaps (try (unprefix_and_unascii const_prefix
#> the #> unmangled_const_name))
in
if s = metis_predicator orelse s = predicator_name orelse
@@ -382,22 +382,22 @@
val factor = Seq.hd o distinct_subgoals_tac
-fun one_step ctxt type_enc old_skolems sym_tab th_pairs p =
+fun one_step ctxt type_enc concealed sym_tab th_pairs p =
case p of
(fol_th, Metis_Proof.Axiom _) => axiom_inference th_pairs fol_th |> factor
| (_, Metis_Proof.Assume f_atom) =>
- assume_inference ctxt type_enc old_skolems sym_tab f_atom
+ assume_inference ctxt type_enc concealed sym_tab f_atom
| (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
- inst_inference ctxt type_enc old_skolems sym_tab th_pairs f_subst f_th1
+ inst_inference ctxt type_enc concealed sym_tab th_pairs f_subst f_th1
|> factor
| (_, Metis_Proof.Resolve(f_atom, f_th1, f_th2)) =>
- resolve_inference ctxt type_enc old_skolems sym_tab th_pairs f_atom f_th1
+ resolve_inference ctxt type_enc concealed sym_tab th_pairs f_atom f_th1
f_th2
|> factor
| (_, Metis_Proof.Refl f_tm) =>
- refl_inference ctxt type_enc old_skolems sym_tab f_tm
+ refl_inference ctxt type_enc concealed sym_tab f_tm
| (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
- equality_inference ctxt type_enc old_skolems sym_tab f_lit f_p f_r
+ equality_inference ctxt type_enc concealed sym_tab f_lit f_p f_r
fun flexflex_first_order th =
case Thm.tpairs_of th of
@@ -449,7 +449,7 @@
end
end
-fun replay_one_inference ctxt type_enc old_skolems sym_tab (fol_th, inf)
+fun replay_one_inference ctxt type_enc concealed sym_tab (fol_th, inf)
th_pairs =
if not (null th_pairs) andalso
prop_of (snd (hd th_pairs)) aconv @{prop False} then
@@ -465,7 +465,7 @@
(fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
val _ = trace_msg ctxt
(fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
- val th = one_step ctxt type_enc old_skolems sym_tab th_pairs (fol_th, inf)
+ val th = one_step ctxt type_enc concealed sym_tab th_pairs (fol_th, inf)
|> flexflex_first_order
|> resynchronize ctxt fol_th
val _ = trace_msg ctxt
--- a/src/HOL/Tools/Metis/metis_tactic.ML Wed Nov 16 15:20:27 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Thu Nov 17 05:27:45 2011 +0100
@@ -9,21 +9,14 @@
signature METIS_TACTIC =
sig
- val metisN : string
- val full_typesN : string
- val partial_typesN : string
- val no_typesN : string
- val really_full_type_enc : string
- val full_type_enc : string
- val partial_type_enc : string
- val no_type_enc : string
- val full_type_syss : string list
- val partial_type_syss : string list
val trace : bool Config.T
val verbose : bool Config.T
val new_skolemizer : bool Config.T
val type_has_top_sort : typ -> bool
- val metis_tac : string list -> Proof.context -> thm list -> int -> tactic
+ val metis_tac :
+ string list -> string -> Proof.context -> thm list -> int -> tactic
+ val metis_lam_transs : string list
+ val parse_metis_options : (string list option * string option) parser
val setup : theory -> theory
end
@@ -31,34 +24,10 @@
struct
open ATP_Translate
+open ATP_Reconstruct
open Metis_Translate
open Metis_Reconstruct
-val metisN = "metis"
-
-val full_typesN = "full_types"
-val partial_typesN = "partial_types"
-val no_typesN = "no_types"
-
-val really_full_type_enc = "mono_tags"
-val full_type_enc = "poly_guards_query"
-val partial_type_enc = "poly_args"
-val no_type_enc = "erased"
-
-val full_type_syss = [full_type_enc, really_full_type_enc]
-val partial_type_syss = partial_type_enc :: full_type_syss
-
-val type_enc_aliases =
- [(full_typesN, full_type_syss),
- (partial_typesN, partial_type_syss),
- (no_typesN, [no_type_enc])]
-
-fun method_call_for_type_enc type_syss =
- metisN ^ " (" ^
- (case AList.find (op =) type_enc_aliases type_syss of
- [alias] => alias
- | _ => hd type_syss) ^ ")"
-
val new_skolemizer =
Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
@@ -75,9 +44,9 @@
"t => t'", where "t" and "t'" are the same term modulo type tags.
In Isabelle, type tags are stripped away, so we are left with "t = t" or
"t => t". Type tag idempotence is also handled this way. *)
-fun reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth =
+fun reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth =
let val thy = Proof_Context.theory_of ctxt in
- case hol_clause_from_metis ctxt type_enc sym_tab old_skolems mth of
+ case hol_clause_from_metis ctxt type_enc sym_tab concealed mth of
Const (@{const_name HOL.eq}, _) $ _ $ t =>
let
val ct = cterm_of thy t
@@ -86,10 +55,34 @@
| Const (@{const_name disj}, _) $ t1 $ t2 =>
(if can HOLogic.dest_not t1 then t2 else t1)
|> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial
- | _ => raise Fail "unexpected tags sym clause"
+ | _ => raise Fail "expected reflexive or trivial clause"
end
|> Meson.make_meta_clause
+fun lambda_lifted_from_metis ctxt type_enc sym_tab concealed mth =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val tac = rewrite_goals_tac @{thms lambda_def_raw} THEN rtac refl 1
+ val t = hol_clause_from_metis ctxt type_enc sym_tab concealed mth
+ val ct = cterm_of thy (HOLogic.mk_Trueprop t)
+ in Goal.prove_internal [] ct (K tac) |> Meson.make_meta_clause end
+
+fun introduce_lambda_wrappers_in_theorem ctxt th =
+ if Meson_Clausify.is_quasi_lambda_free (prop_of th) then
+ th
+ else
+ let
+ fun conv wrap ctxt ct =
+ if Meson_Clausify.is_quasi_lambda_free (term_of ct) then
+ Thm.reflexive ct
+ else case term_of ct of
+ Abs _ =>
+ Conv.abs_conv (conv false o snd) ctxt ct
+ |> wrap ? (fn th => th RS @{thm Metis.eq_lambdaI})
+ | _ => Conv.comb_conv (conv true ctxt) ct
+ val eqth = conv true ctxt (cprop_of th)
+ in Thm.equal_elim eqth th end
+
val clause_params =
{ordering = Metis_KnuthBendixOrder.default,
orderLiterals = Metis_Clause.UnsignedLiteralOrder,
@@ -106,14 +99,15 @@
val resolution_params = {active = active_params, waiting = waiting_params}
(* Main function to start Metis proof and reconstruction *)
-fun FOL_SOLVE (type_enc :: fallback_type_syss) ctxt cls ths0 =
+fun FOL_SOLVE (type_enc :: fallback_type_encs) lam_trans ctxt cls ths0 =
let val thy = Proof_Context.theory_of ctxt
val new_skolemizer =
Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
val th_cls_pairs =
map2 (fn j => fn th =>
(Thm.get_name_hint th,
- Meson_Clausify.cnf_axiom ctxt new_skolemizer j th))
+ Meson_Clausify.cnf_axiom ctxt new_skolemizer
+ (lam_trans = combinatorsN) j th))
(0 upto length ths0 - 1) ths0
val ths = maps (snd o snd) th_cls_pairs
val dischargers = map (fst o snd) th_cls_pairs
@@ -121,11 +115,15 @@
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
val type_enc = type_enc_from_string Sound type_enc
- val (sym_tab, axioms, old_skolems) =
- prepare_metis_problem ctxt type_enc cls ths
+ val (sym_tab, axioms, concealed) =
+ prepare_metis_problem ctxt type_enc lam_trans cls ths
fun get_isa_thm mth Isa_Reflexive_or_Trivial =
- reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth
- | get_isa_thm _ (Isa_Raw ith) = ith
+ reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth
+ | get_isa_thm mth Isa_Lambda_Lifted =
+ lambda_lifted_from_metis ctxt type_enc sym_tab concealed mth
+ | get_isa_thm _ (Isa_Raw ith) =
+ ith |> lam_trans = lam_liftingN
+ ? introduce_lambda_wrappers_in_theorem ctxt
val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
val _ = app (fn (_, th) => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) axioms
@@ -148,7 +146,7 @@
val proof = Metis_Proof.proof mth
val result =
axioms
- |> fold (replay_one_inference ctxt' type_enc old_skolems sym_tab) proof
+ |> fold (replay_one_inference ctxt' type_enc concealed sym_tab) proof
val used = map_filter (used_axioms axioms) proof
val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:")
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
@@ -177,7 +175,7 @@
end
| Metis_Resolution.Satisfiable _ =>
(trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied");
- if null fallback_type_syss then
+ if null fallback_type_encs then
()
else
raise METIS ("FOL_SOLVE",
@@ -185,20 +183,20 @@
[])
end
handle METIS (loc, msg) =>
- case fallback_type_syss of
+ case fallback_type_encs of
[] => error ("Failed to replay Metis proof in Isabelle." ^
(if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg
else ""))
- | _ =>
+ | first_fallback :: _ =>
(verbose_warning ctxt
("Falling back on " ^
- quote (method_call_for_type_enc fallback_type_syss) ^ "...");
- FOL_SOLVE fallback_type_syss ctxt cls ths0)
+ quote (metis_call first_fallback lam_trans) ^ "...");
+ FOL_SOLVE fallback_type_encs lam_trans ctxt cls ths0)
-fun neg_clausify ctxt =
+fun neg_clausify ctxt combinators =
single
#> Meson.make_clauses_unsorted ctxt
- #> map Meson_Clausify.introduce_combinators_in_theorem
+ #> combinators ? map Meson_Clausify.introduce_combinators_in_theorem
#> Meson.finish_cnf
fun preskolem_tac ctxt st0 =
@@ -212,22 +210,25 @@
val type_has_top_sort =
exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
-fun generic_metis_tac type_syss ctxt ths i st0 =
+fun generic_metis_tac type_encs lam_trans ctxt ths i st0 =
let
val _ = trace_msg ctxt (fn () =>
"Metis called with theorems\n" ^
cat_lines (map (Display.string_of_thm ctxt) ths))
- fun tac clause = resolve_tac (FOL_SOLVE type_syss ctxt clause ths) 1
+ val type_encs = type_encs |> maps unalias_type_enc
+ fun tac clause =
+ resolve_tac (FOL_SOLVE type_encs lam_trans ctxt clause ths) 1
in
if exists_type type_has_top_sort (prop_of st0) then
verbose_warning ctxt "Proof state contains the universal sort {}"
else
();
- Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt)) tac ctxt i st0
+ Meson.MESON (preskolem_tac ctxt)
+ (maps (neg_clausify ctxt (lam_trans = combinatorsN))) tac ctxt i st0
end
-fun metis_tac [] = generic_metis_tac partial_type_syss
- | metis_tac type_syss = generic_metis_tac type_syss
+fun metis_tac [] = generic_metis_tac partial_type_encs
+ | metis_tac type_encs = generic_metis_tac type_encs
(* Whenever "X" has schematic type variables, we treat "using X by metis" as
"by (metis X)" to prevent "Subgoal.FOCUS" from freezing the type variables.
@@ -237,32 +238,45 @@
val has_tvar =
exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
-fun method default_type_syss (override_type_syss, ths) ctxt facts =
+fun method default_type_encs ((override_type_encs, lam_trans), ths) ctxt facts =
let
val _ =
- if default_type_syss = full_type_syss then
+ if default_type_encs = full_type_encs then
legacy_feature "Old \"metisFT\" method -- use \"metis (full_types)\" instead"
else
()
val (schem_facts, nonschem_facts) = List.partition has_tvar facts
- val type_syss = override_type_syss |> the_default default_type_syss
+ val type_encs = override_type_encs |> the_default default_type_encs
+ val lam_trans = lam_trans |> the_default metis_default_lam_trans
in
HEADGOAL (Method.insert_tac nonschem_facts THEN'
- CHANGED_PROP
- o generic_metis_tac type_syss ctxt (schem_facts @ ths))
+ CHANGED_PROP o generic_metis_tac type_encs lam_trans ctxt
+ (schem_facts @ ths))
end
-fun setup_method (binding, type_syss) =
- ((Args.parens (Scan.repeat Parse.short_ident)
- >> maps (fn s => AList.lookup (op =) type_enc_aliases s |> the_default [s]))
- |> Scan.option |> Scan.lift)
- -- Attrib.thms >> (METHOD oo method type_syss)
+val metis_lam_transs = [hide_lamsN, lam_liftingN, combinatorsN]
+
+fun consider_opt s =
+ if member (op =) metis_lam_transs s then apsnd (K (SOME s))
+ else apfst (K (SOME [s]))
+
+val parse_metis_options =
+ Scan.optional
+ (Args.parens (Parse.short_ident
+ -- Scan.option (Parse.$$$ "," |-- Parse.short_ident))
+ >> (fn (s, s') =>
+ (NONE, NONE) |> consider_opt s
+ |> (case s' of SOME s' => consider_opt s' | _ => I)))
+ (NONE, NONE)
+
+fun setup_method (binding, type_encs) =
+ Scan.lift parse_metis_options -- Attrib.thms >> (METHOD oo method type_encs)
|> Method.setup binding
val setup =
- [((@{binding metis}, partial_type_syss),
+ [((@{binding metis}, partial_type_encs),
"Metis for FOL and HOL problems"),
- ((@{binding metisFT}, full_type_syss),
+ ((@{binding metisFT}, full_type_encs),
"Metis for FOL/HOL problems with fully-typed translation")]
|> fold (uncurry setup_method)
--- a/src/HOL/Tools/Metis/metis_translate.ML Wed Nov 16 15:20:27 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_translate.ML Thu Nov 17 05:27:45 2011 +0100
@@ -13,6 +13,7 @@
datatype isa_thm =
Isa_Reflexive_or_Trivial |
+ Isa_Lambda_Lifted |
Isa_Raw of thm
val metis_equal : string
@@ -27,9 +28,11 @@
val verbose_warning : Proof.context -> string -> unit
val metis_name_table : ((string * int) * ((type_enc -> string) * bool)) list
val reveal_old_skolem_terms : (string * term) list -> term -> term
+ val reveal_lambda_lifted : (string * term) list -> term -> term
val prepare_metis_problem :
- Proof.context -> type_enc -> thm list -> thm list
- -> int Symtab.table * (Metis_Thm.thm * isa_thm) list * (string * term) list
+ Proof.context -> type_enc -> string -> thm list -> thm list
+ -> int Symtab.table * (Metis_Thm.thm * isa_thm) list
+ * ((string * term) list * (string * term) list)
end
structure Metis_Translate : METIS_TRANSLATE =
@@ -107,6 +110,18 @@
t
| t => t)
+fun reveal_lambda_lifted lambdas =
+ map_aterms (fn t as Const (s, _) =>
+ if String.isPrefix lambda_lifted_prefix s then
+ case AList.lookup (op =) lambdas s of
+ SOME t =>
+ Const (@{const_name Metis.lambda}, dummyT)
+ $ map_types (map_type_tvar (K dummyT)) t
+ | NONE => t
+ else
+ t
+ | t => t)
+
(* ------------------------------------------------------------------------- *)
(* Logic maps manage the interface between HOL and first-order logic. *)
@@ -114,6 +129,7 @@
datatype isa_thm =
Isa_Reflexive_or_Trivial |
+ Isa_Lambda_Lifted |
Isa_Raw of thm
val proxy_defs = map (fst o snd o snd) proxy_table
@@ -167,15 +183,23 @@
| _ => raise Fail ("malformed helper identifier " ^ quote ident)
else case try (unprefix fact_prefix) ident of
SOME s =>
- let
- val j = s |> space_explode "_" |> List.last |> Int.fromString |> the
- in Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some end
+ let val s = s |> space_explode "_" |> tl |> space_implode "_"
+ in
+ case Int.fromString s of
+ SOME j =>
+ Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some
+ | NONE =>
+ if String.isPrefix lambda_fact_prefix (unascii_of s) then
+ Isa_Lambda_Lifted |> some
+ else
+ raise Fail ("malformed fact identifier " ^ quote ident)
+ end
| NONE => TrueI |> Isa_Raw |> some
end
| metis_axiom_from_atp _ _ _ = raise Fail "not CNF -- expected formula"
(* Function to generate metis clauses, including comb and type clauses *)
-fun prepare_metis_problem ctxt type_enc conj_clauses fact_clauses =
+fun prepare_metis_problem ctxt type_enc lam_trans conj_clauses fact_clauses =
let
val (conj_clauses, fact_clauses) =
if polymorphism_of_type_enc type_enc = Polymorphic then
@@ -205,17 +229,18 @@
tracing ("PROPS:\n" ^
cat_lines (map (Syntax.string_of_term ctxt o snd) props))
*)
- val (atp_problem, _, _, _, _, _, sym_tab) =
- prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false no_lambdasN
+ val lam_trans = if lam_trans = combinatorsN then no_lamsN else lam_trans
+ val (atp_problem, _, _, _, _, _, lifted, sym_tab) =
+ prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lam_trans
false false [] @{prop False} props
(*
val _ = tracing ("ATP PROBLEM: " ^
- cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
+ cat_lines (lines_for_atp_problem CNF atp_problem))
*)
- (* "rev" is for compatibility. *)
+ (* "rev" is for compatibility with existing proof scripts. *)
val axioms =
atp_problem
|> maps (map_filter (metis_axiom_from_atp type_enc clauses) o snd) |> rev
- in (sym_tab, axioms, old_skolems) end
+ in (sym_tab, axioms, (lifted, old_skolems)) end
end;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Nov 16 15:20:27 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Nov 17 05:27:45 2011 +0100
@@ -982,7 +982,6 @@
| is_param_type T = is_some (try (dest_monadT compfuns) T)
val (inpTs, outTs) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode
(binder_types T)
- val predT = mk_monadT compfuns (HOLogic.mk_tupleT outTs)
val funT = Comp_Mod.funT_of compilation_modifiers mode T
val (in_ts, _) = fold_map (fold_map_aterms_prodT (curry HOLogic.mk_prod)
(fn T => fn (param_vs, names) =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Nov 16 15:20:27 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Nov 17 05:27:45 2011 +0100
@@ -22,6 +22,7 @@
open ATP_Util
open ATP_Systems
open ATP_Translate
+open ATP_Reconstruct
open Sledgehammer_Util
open Sledgehammer_Filter
open Sledgehammer_Provers
@@ -87,6 +88,7 @@
("blocking", "false"),
("type_enc", "smart"),
("sound", "false"),
+ ("lam_trans", "smart"),
("relevance_thresholds", "0.45 0.85"),
("max_relevant", "smart"),
("max_mono_iters", "3"),
@@ -108,9 +110,9 @@
("no_slicing", "slicing")]
val params_for_minimize =
- ["debug", "verbose", "overlord", "type_enc", "sound", "max_mono_iters",
- "max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout",
- "preplay_timeout"]
+ ["debug", "verbose", "overlord", "type_enc", "sound", "lam_trans",
+ "max_mono_iters", "max_new_mono_instances", "isar_proof",
+ "isar_shrink_factor", "timeout", "preplay_timeout"]
val property_dependent_params = ["provers", "timeout"]
@@ -137,8 +139,10 @@
| _ => value)
| NONE => (name, value)
-(* "provers =" and "type_enc =" can be left out. The latter is a secret
- feature. *)
+val any_type_enc = type_enc_from_string Sound "erased"
+
+(* "provers =", "type_enc =", and "lam_trans" can be omitted. For the last two,
+ this is a secret feature. *)
fun normalize_raw_param ctxt =
unalias_raw_param
#> (fn (name, value) =>
@@ -148,6 +152,9 @@
("provers", [name])
else if can (type_enc_from_string Sound) name andalso null value then
("type_enc", [name])
+ else if can (trans_lams_from_string ctxt any_type_enc) name andalso
+ null value then
+ ("lam_trans", [name])
else
error ("Unknown parameter: " ^ quote name ^ "."))
@@ -275,6 +282,7 @@
"smart" => NONE
| s => (type_enc_from_string Sound s; SOME s)
val sound = mode = Auto_Try orelse lookup_bool "sound"
+ val lam_trans = lookup_option lookup_string "lam_trans"
val relevance_thresholds = lookup_real_pair "relevance_thresholds"
val max_relevant = lookup_option lookup_int "max_relevant"
val max_mono_iters = lookup_int "max_mono_iters"
@@ -290,10 +298,10 @@
val expect = lookup_string "expect"
in
{debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
- provers = provers, relevance_thresholds = relevance_thresholds,
+ provers = provers, type_enc = type_enc, sound = sound,
+ lam_trans = lam_trans, relevance_thresholds = relevance_thresholds,
max_relevant = max_relevant, max_mono_iters = max_mono_iters,
- max_new_mono_instances = max_new_mono_instances, type_enc = type_enc,
- sound = sound, isar_proof = isar_proof,
+ max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
isar_shrink_factor = isar_shrink_factor, slicing = slicing,
timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
end
@@ -303,17 +311,20 @@
(* Sledgehammer the given subgoal *)
-val default_minimize_prover = Metis_Tactic.metisN
+val default_minimize_prover = metisN
fun is_raw_param_relevant_for_minimize (name, _) =
member (op =) params_for_minimize name
fun string_for_raw_param (key, values) =
key ^ (case implode_param values of "" => "" | value => " = " ^ value)
-fun minimize_command override_params i prover_name fact_names =
+fun minimize_command override_params i more_override_params prover_name
+ fact_names =
let
val params =
- override_params
+ (override_params
+ |> filter_out (AList.defined (op =) more_override_params o fst)) @
+ more_override_params
|> filter is_raw_param_relevant_for_minimize
|> map string_for_raw_param
|> (if prover_name = default_minimize_prover then I else cons prover_name)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Nov 16 15:20:27 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Nov 17 05:27:45 2011 +0100
@@ -47,7 +47,7 @@
fun print silent f = if silent then () else Output.urgent_message (f ())
fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
- max_new_mono_instances, type_enc, isar_proof,
+ max_new_mono_instances, type_enc, lam_trans, isar_proof,
isar_shrink_factor, preplay_timeout, ...} : params)
silent (prover : prover) timeout i n state facts =
let
@@ -62,8 +62,8 @@
val params =
{debug = debug, verbose = verbose, overlord = overlord, blocking = true,
provers = provers, type_enc = type_enc, sound = true,
- relevance_thresholds = (1.01, 1.01), max_relevant = SOME (length facts),
- max_mono_iters = max_mono_iters,
+ lam_trans = lam_trans, relevance_thresholds = (1.01, 1.01),
+ max_relevant = SOME (length facts), max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
isar_shrink_factor = isar_shrink_factor, slicing = false,
timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
@@ -71,7 +71,7 @@
{state = state, goal = goal, subgoal = i, subgoal_count = n,
facts = facts, smt_filter = NONE}
val result as {outcome, used_facts, run_time, ...} =
- prover params (K (K "")) problem
+ prover params (K (K (K ""))) problem
in
print silent
(fn () =>
@@ -205,7 +205,7 @@
| {preplay, message, ...} =>
(NONE, (preplay, prefix "Prover error: " o message, "")))
handle ERROR msg =>
- (NONE, (K (Failed_to_Play Metis), fn _ => "Error: " ^ msg, ""))
+ (NONE, (K (Failed_to_Play plain_metis), fn _ => "Error: " ^ msg, ""))
end
fun run_minimize (params as {provers, ...}) i refs state =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Nov 16 15:20:27 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Nov 17 05:27:45 2011 +0100
@@ -26,6 +26,7 @@
provers: string list,
type_enc: string option,
sound: bool,
+ lam_trans: string option,
relevance_thresholds: real * real,
max_relevant: int option,
max_mono_iters: int,
@@ -58,11 +59,11 @@
message_tail: string}
type prover =
- params -> (string -> minimize_command) -> prover_problem -> prover_result
+ params -> ((string * string list) list -> string -> minimize_command)
+ -> prover_problem -> prover_result
val dest_dir : string Config.T
val problem_prefix : string Config.T
- val atp_lambda_translation : string Config.T
val atp_full_names : bool Config.T
val smt_triggers : bool Config.T
val smt_weights : bool Config.T
@@ -76,8 +77,10 @@
val smt_slice_time_frac : real Config.T
val smt_slice_min_secs : int Config.T
val das_tool : string
+ val plain_metis : reconstructor
val select_smt_solver : string -> Proof.context -> Proof.context
- val prover_name_for_reconstructor : reconstructor -> string
+ val extract_reconstructor :
+ reconstructor -> string * (string * string list) list
val is_reconstructor : string -> bool
val is_atp : theory -> string -> bool
val is_smt_prover : Proof.context -> string -> bool
@@ -117,6 +120,7 @@
open ATP_Systems
open ATP_Translate
open ATP_Reconstruct
+open Metis_Tactic
open Sledgehammer_Util
open Sledgehammer_Filter
@@ -128,22 +132,26 @@
"Async_Manager". *)
val das_tool = "Sledgehammer"
-val metisN = Metis_Tactic.metisN
-val metis_full_typesN = metisN ^ "_" ^ Metis_Tactic.full_typesN
-val metis_no_typesN = metisN ^ "_" ^ Metis_Tactic.no_typesN
-val smtN = name_of_reconstructor SMT
+fun extract_reconstructor (Metis (type_enc, lam_trans)) =
+ let
+ val override_params =
+ (if type_enc = hd partial_type_encs then []
+ else [("type_enc", [type_enc])]) @
+ (if lam_trans = metis_default_lam_trans then []
+ else [("lam_trans", [lam_trans])])
+ in (metisN, override_params) end
+ | extract_reconstructor SMT = (smtN, [])
-val reconstructor_infos =
- [(metisN, Metis),
- (metis_full_typesN, Metis_Full_Types),
- (metis_no_typesN, Metis_No_Types),
- (smtN, SMT)]
+val reconstructor_names = [metisN, smtN]
+val plain_metis = Metis (hd partial_type_encs, combinatorsN)
-val prover_name_for_reconstructor = AList.find (op =) reconstructor_infos #> hd
+fun standard_reconstructors lam_trans =
+ [Metis (hd partial_type_encs, lam_trans),
+ Metis (hd full_type_encs, lam_trans),
+ Metis (no_type_enc, lam_trans),
+ SMT]
-val all_reconstructors = map snd reconstructor_infos
-
-val is_reconstructor = AList.defined (op =) reconstructor_infos
+val is_reconstructor = member (op =) reconstructor_names
val is_atp = member (op =) o supported_atps
val select_smt_solver = Context.proof_map o SMT_Config.select_solver
@@ -154,7 +162,7 @@
let val thy = Proof_Context.theory_of ctxt in
case try (get_atp thy) name of
SOME {best_slices, ...} =>
- exists (fn (_, (_, (_, format, _, _))) => is_format format)
+ exists (fn (_, (_, (_, format, _, _, _))) => is_format format)
(best_slices ctxt)
| NONE => false
end
@@ -274,7 +282,7 @@
let
val thy = Proof_Context.theory_of ctxt
val (remote_provers, local_provers) =
- map fst reconstructor_infos @
+ reconstructor_names @
sort_strings (supported_atps thy) @
sort_strings (SMT_Solver.available_solvers_of ctxt)
|> List.partition (String.isPrefix remote_prefix)
@@ -297,6 +305,7 @@
provers: string list,
type_enc: string option,
sound: bool,
+ lam_trans: string option,
relevance_thresholds: real * real,
max_relevant: int option,
max_mono_iters: int,
@@ -329,7 +338,8 @@
message_tail: string}
type prover =
- params -> (string -> minimize_command) -> prover_problem -> prover_result
+ params -> ((string * string list) list -> string -> minimize_command)
+ -> prover_problem -> prover_result
(* configuration attributes *)
@@ -339,9 +349,6 @@
val problem_prefix =
Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
-val atp_lambda_translation =
- Attrib.setup_config_string @{binding sledgehammer_atp_lambda_translation}
- (K smartN)
(* In addition to being easier to read, readable names are often much shorter,
especially if types are mangled in names. This makes a difference for some
provers (e.g., E). For these reason, short names are enabled by default. *)
@@ -412,57 +419,52 @@
val full_tac = Method.insert_tac facts i THEN tac ctxt i
in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end
-fun tac_for_reconstructor Metis =
- Metis_Tactic.metis_tac [Metis_Tactic.partial_type_enc]
- | tac_for_reconstructor Metis_Full_Types =
- Metis_Tactic.metis_tac Metis_Tactic.full_type_syss
- | tac_for_reconstructor Metis_No_Types =
- Metis_Tactic.metis_tac [Metis_Tactic.no_type_enc]
+fun tac_for_reconstructor (Metis (type_enc, lam_trans)) =
+ metis_tac [type_enc] lam_trans
| tac_for_reconstructor SMT = SMT_Solver.smt_tac
-fun timed_reconstructor reconstructor debug timeout ths =
+fun timed_reconstructor reconstr debug timeout ths =
(Config.put Metis_Tactic.verbose debug
- #> (fn ctxt => tac_for_reconstructor reconstructor ctxt ths))
+ #> (fn ctxt => tac_for_reconstructor reconstr ctxt ths))
|> timed_apply timeout
fun filter_used_facts used = filter (member (op =) used o fst)
fun play_one_line_proof mode debug verbose timeout ths state i preferred
- reconstructors =
+ reconstrs =
let
val _ =
if mode = Minimize andalso Time.> (timeout, Time.zeroTime) then
Output.urgent_message "Preplaying proof..."
else
()
- fun get_preferred reconstructors =
- if member (op =) reconstructors preferred then preferred
- else List.last reconstructors
- fun play [] [] = Failed_to_Play (get_preferred reconstructors)
+ fun get_preferred reconstrs =
+ if member (op =) reconstrs preferred then preferred
+ else List.last reconstrs
+ fun play [] [] = Failed_to_Play (get_preferred reconstrs)
| play timed_outs [] =
Trust_Playable (get_preferred timed_outs, SOME timeout)
- | play timed_out (reconstructor :: reconstructors) =
+ | play timed_out (reconstr :: reconstrs) =
let
val _ =
if verbose then
- "Trying \"" ^ name_of_reconstructor reconstructor ^ "\" for " ^
+ "Trying \"" ^ name_of_reconstructor reconstr ^ "\" for " ^
string_from_time timeout ^ "..."
|> Output.urgent_message
else
()
val timer = Timer.startRealTimer ()
in
- case timed_reconstructor reconstructor debug timeout ths state i of
- SOME (SOME _) => Played (reconstructor, Timer.checkRealTimer timer)
- | _ => play timed_out reconstructors
+ case timed_reconstructor reconstr debug timeout ths state i of
+ SOME (SOME _) => Played (reconstr, Timer.checkRealTimer timer)
+ | _ => play timed_out reconstrs
end
- handle TimeLimit.TimeOut =>
- play (reconstructor :: timed_out) reconstructors
+ handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs
in
if timeout = Time.zeroTime then
- Trust_Playable (get_preferred reconstructors, NONE)
+ Trust_Playable (get_preferred reconstrs, NONE)
else
- play [] reconstructors
+ play [] reconstrs
end
@@ -536,14 +538,16 @@
val metis_minimize_max_time = seconds 2.0
fun choose_minimize_command minimize_command name preplay =
- (case preplay of
- Played (reconstructor, time) =>
- if Time.<= (time, metis_minimize_max_time) then
- prover_name_for_reconstructor reconstructor
- else
- name
- | _ => name)
- |> minimize_command
+ let
+ val (name, override_params) =
+ case preplay of
+ Played (reconstr, time) =>
+ if Time.<= (time, metis_minimize_max_time) then
+ extract_reconstructor reconstr
+ else
+ (name, [])
+ | _ => (name, [])
+ in minimize_command override_params name end
fun repair_monomorph_context max_iters max_new_instances =
Config.put Monomorph.max_rounds max_iters
@@ -562,7 +566,7 @@
fun run_atp mode name
({exec, required_execs, arguments, proof_delims, known_failures,
conj_sym_kind, prem_kind, best_slices, ...} : atp_config)
- ({debug, verbose, overlord, type_enc, sound, max_relevant,
+ ({debug, verbose, overlord, type_enc, sound, lam_trans, max_relevant,
max_mono_iters, max_new_mono_instances, isar_proof,
isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params)
minimize_command
@@ -634,7 +638,7 @@
end
fun run_slice (slice, (time_frac, (complete,
(best_max_relevant, format, best_type_enc,
- extra))))
+ best_lam_trans, extra))))
time_left =
let
val num_facts =
@@ -671,12 +675,16 @@
|> Output.urgent_message
else
()
+ val readable_names = not (Config.get ctxt atp_full_names)
+ val lam_trans =
+ case lam_trans of
+ SOME s => s
+ | NONE => best_lam_trans
val (atp_problem, pool, conjecture_offset, facts_offset,
- fact_names, typed_helpers, sym_tab) =
+ fact_names, typed_helpers, _, sym_tab) =
prepare_atp_problem ctxt format conj_sym_kind prem_kind
- type_enc false (Config.get ctxt atp_lambda_translation)
- (not (Config.get ctxt atp_full_names)) true hyp_ts concl_t
- facts
+ type_enc false lam_trans readable_names true hyp_ts
+ concl_t facts
fun weights () = atp_problem_weights atp_problem
val full_proof = debug orelse isar_proof
val core =
@@ -729,7 +737,7 @@
| _ => outcome
in
((pool, conjecture_shape, facts_offset, fact_names,
- typed_helpers, sym_tab),
+ typed_helpers, sym_tab, lam_trans),
(output, run_time, atp_proof, outcome))
end
val timer = Timer.startRealTimer ()
@@ -748,8 +756,8 @@
end
| maybe_run_slice _ result = result
in
- ((Symtab.empty, [], 0, Vector.fromList [], [], Symtab.empty),
- ("", Time.zeroTime, [], SOME InternalError))
+ ((Symtab.empty, [], 0, Vector.fromList [], [], Symtab.empty,
+ no_lamsN), ("", Time.zeroTime, [], SOME InternalError))
|> fold maybe_run_slice actual_slices
end
else
@@ -765,7 +773,7 @@
else
File.write (Path.explode (Path.implode prob_file ^ "_proof")) output
val ((pool, conjecture_shape, facts_offset, fact_names, typed_helpers,
- sym_tab),
+ sym_tab, lam_trans),
(output, run_time, atp_proof, outcome)) =
with_path cleanup export run_on problem_path_name
val important_message =
@@ -780,6 +788,10 @@
let
val used_facts =
used_facts_in_atp_proof ctxt facts_offset fact_names atp_proof
+ val reconstrs =
+ standard_reconstructors
+ (if member (op =) metis_lam_transs lam_trans then lam_trans
+ else combinatorsN)
in
(used_facts,
fn () =>
@@ -789,7 +801,7 @@
|> map snd
in
play_one_line_proof mode debug verbose preplay_timeout used_ths
- state subgoal Metis all_reconstructors
+ state subgoal (hd reconstrs) reconstrs
end,
fn preplay =>
let
@@ -814,7 +826,8 @@
""))
end
| SOME failure =>
- ([], K (Failed_to_Play Metis), fn _ => string_for_failure failure, "")
+ ([], K (Failed_to_Play plain_metis),
+ fn _ => string_for_failure failure, "")
in
{outcome = outcome, used_facts = used_facts, run_time = run_time,
preplay = preplay, message = message, message_tail = message_tail}
@@ -969,7 +982,8 @@
NONE =>
(fn () =>
play_one_line_proof mode debug verbose preplay_timeout used_ths
- state subgoal SMT all_reconstructors,
+ state subgoal SMT
+ (standard_reconstructors lam_liftingN),
fn preplay =>
let
val one_line_params =
@@ -982,34 +996,41 @@
else
"")
| SOME failure =>
- (K (Failed_to_Play Metis), fn _ => string_for_failure failure, "")
+ (K (Failed_to_Play plain_metis), fn _ => string_for_failure failure, "")
in
{outcome = outcome, used_facts = used_facts, run_time = run_time,
preplay = preplay, message = message, message_tail = message_tail}
end
-fun run_reconstructor mode name ({debug, verbose, timeout, ...} : params)
+fun run_reconstructor mode name
+ ({debug, verbose, timeout, type_enc, lam_trans, ...} : params)
minimize_command
({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
let
- val reconstructor =
- case AList.lookup (op =) reconstructor_infos name of
- SOME r => r
- | NONE => raise Fail ("unknown Metis version: " ^ quote name)
+ val reconstr =
+ if name = metisN then
+ Metis (type_enc |> the_default (hd partial_type_encs),
+ lam_trans |> the_default metis_default_lam_trans)
+ else if name = smtN then
+ SMT
+ else
+ raise Fail ("unknown reconstructor: " ^ quote name)
val (used_facts, used_ths) =
facts |> map untranslated_fact |> ListPair.unzip
in
case play_one_line_proof (if mode = Minimize then Normal else mode) debug
- verbose timeout used_ths state subgoal
- reconstructor [reconstructor] of
+ verbose timeout used_ths state subgoal reconstr
+ [reconstr] of
play as Played (_, time) =>
{outcome = NONE, used_facts = used_facts, run_time = time,
preplay = K play,
message = fn play =>
let
+ val (_, override_params) = extract_reconstructor reconstr
val one_line_params =
- (play, proof_banner mode name, used_facts,
- minimize_command name, subgoal, subgoal_count)
+ (play, proof_banner mode name, used_facts,
+ minimize_command override_params name, subgoal,
+ subgoal_count)
in one_line_proof_text one_line_params end,
message_tail = ""}
| play =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Nov 16 15:20:27 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Nov 17 05:27:45 2011 +0100
@@ -22,7 +22,8 @@
val auto_minimize_max_time : real Config.T
val get_minimizing_prover : Proof.context -> mode -> string -> prover
val run_sledgehammer :
- params -> mode -> int -> relevance_override -> (string -> minimize_command)
+ params -> mode -> int -> relevance_override
+ -> ((string * string list) list -> string -> minimize_command)
-> Proof.state -> bool * (string * Proof.state)
end;
@@ -71,6 +72,31 @@
Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time}
(K 5.0)
+fun adjust_reconstructor_params override_params
+ ({debug, verbose, overlord, blocking, provers, type_enc, sound,
+ lam_trans, relevance_thresholds, max_relevant, max_mono_iters,
+ max_new_mono_instances, isar_proof, isar_shrink_factor, slicing,
+ timeout, preplay_timeout, expect} : params) =
+ let
+ fun lookup_override name default_value =
+ case AList.lookup (op =) override_params name of
+ SOME [s] => SOME s
+ | _ => default_value
+ (* Only those options that reconstructors are interested in are considered
+ here. *)
+ val type_enc = lookup_override "type_enc" type_enc
+ val lam_trans = lookup_override "lam_trans" lam_trans
+ in
+ {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
+ provers = provers, type_enc = type_enc, sound = sound,
+ lam_trans = lam_trans, max_relevant = max_relevant,
+ relevance_thresholds = relevance_thresholds,
+ max_mono_iters = max_mono_iters,
+ max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
+ isar_shrink_factor = isar_shrink_factor, slicing = slicing,
+ timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
+ end
+
fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...})
({state, subgoal, subgoal_count, facts, ...} : prover_problem)
(result as {outcome, used_facts, run_time, preplay, message,
@@ -80,10 +106,10 @@
else
let
val num_facts = length used_facts
- val ((minimize, minimize_name), preplay) =
+ val ((minimize, (minimize_name, params)), preplay) =
if mode = Normal then
if num_facts >= Config.get ctxt auto_minimize_min_facts then
- ((true, name), preplay)
+ ((true, (name, params)), preplay)
else
let
fun can_min_fast_enough time =
@@ -93,21 +119,24 @@
val prover_fast_enough = can_min_fast_enough run_time
in
if isar_proof then
- ((prover_fast_enough, name), preplay)
+ ((prover_fast_enough, (name, params)), preplay)
else
let val preplay = preplay () in
(case preplay of
- Played (reconstructor, timeout) =>
+ Played (reconstr, timeout) =>
if can_min_fast_enough timeout then
- (true, prover_name_for_reconstructor reconstructor)
+ (true, extract_reconstructor reconstr
+ ||> (fn override_params =>
+ adjust_reconstructor_params
+ override_params params))
else
- (prover_fast_enough, name)
- | _ => (prover_fast_enough, name),
+ (prover_fast_enough, (name, params))
+ | _ => (prover_fast_enough, (name, params)),
K preplay)
end
end
else
- ((false, name), preplay)
+ ((false, (name, params)), preplay)
val (used_facts, (preplay, message, _)) =
if minimize then
minimize_facts minimize_name params (not verbose) subgoal
--- a/src/HOL/Tools/cnf_funcs.ML Wed Nov 16 15:20:27 2011 +0100
+++ b/src/HOL/Tools/cnf_funcs.ML Thu Nov 17 05:27:45 2011 +0100
@@ -261,8 +261,7 @@
val thy = Proof_Context.theory_of ctxt
fun conv ctxt ct =
case term_of ct of
- (t1 as Const _) $ (t2 as Abs _) =>
- Conv.comb_conv (conv ctxt) ct
+ Const _ $ Abs _ => Conv.comb_conv (conv ctxt) ct
| Abs _ => Conv.abs_conv (conv o snd) ctxt ct
| Const _ => Conv.all_conv ct
| t => make t RS eq_reflection
--- a/src/HOL/ex/Quickcheck_Examples.thy Wed Nov 16 15:20:27 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy Thu Nov 17 05:27:45 2011 +0100
@@ -304,12 +304,22 @@
quickcheck[random, size = 10]
oops
+lemma "(x :: rat) >= 0"
+quickcheck[random, expect = counterexample]
+quickcheck[exhaustive, expect = counterexample]
+oops
+
lemma
"(x :: real) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
quickcheck[exhaustive, size = 10, expect = counterexample]
quickcheck[random, size = 10]
oops
+lemma "(x :: real) >= 0"
+quickcheck[random, expect = counterexample]
+quickcheck[exhaustive, expect = counterexample]
+oops
+
subsubsection {* floor and ceiling functions *}
lemma
--- a/src/HOL/ex/sledgehammer_tactics.ML Wed Nov 16 15:20:27 2011 +0100
+++ b/src/HOL/ex/sledgehammer_tactics.ML Thu Nov 17 05:27:45 2011 +0100
@@ -49,7 +49,7 @@
facts = map Sledgehammer_Provers.Untranslated_Fact facts,
smt_filter = NONE}
in
- (case prover params (K (K "")) problem of
+ (case prover params (K (K (K ""))) problem of
{outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
| _ => NONE)
handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
@@ -71,7 +71,8 @@
fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th =
case run_atp override_params relevance_override i i ctxt th of
SOME facts =>
- Metis_Tactic.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
+ Metis_Tactic.metis_tac [] ATP_Translate.combinatorsN ctxt
+ (maps (thms_of_name ctxt) facts) i th
| NONE => Seq.empty
fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th =
--- a/src/Pure/Isar/attrib.ML Wed Nov 16 15:20:27 2011 +0100
+++ b/src/Pure/Isar/attrib.ML Thu Nov 17 05:27:45 2011 +0100
@@ -219,26 +219,43 @@
(** partial evaluation **)
local
-(* FIXME assignable, closure (!?) *)
+
+val strict_thm_eq = op = o pairself Thm.rep_thm;
fun apply_att src (context, th) =
- attribute_i (Context.theory_of context) src (context, th);
+ let
+ val src1 = Args.assignable src;
+ val result = attribute_i (Context.theory_of context) src1 (context, th);
+ val src2 = Args.closure src1;
+ in (src2, result) end;
+
+fun err msg src =
+ let val ((name, _), pos) = Args.dest_src src
+ in error (msg ^ " " ^ quote name ^ Position.str_of pos) end;
-fun eval src (th, (decls, context)) =
- (case apply_att src (context, th) of
- (NONE, SOME th') => (th', (decls, context))
- | (opt_context', opt_th') =>
+fun eval src ((th, dyn), (decls, context)) =
+ (case (apply_att src (context, th), dyn) of
+ ((_, (NONE, SOME th')), NONE) => ((th', NONE), (decls, context))
+ | ((_, (NONE, SOME _)), SOME _) => err "Mixed dynamic attribute followed by static rule" src
+ | ((src', (SOME context', NONE)), NONE) =>
+ let
+ val decls' =
+ (case decls of
+ [] => [(th, [src'])]
+ | (th2, srcs2) :: rest =>
+ if strict_thm_eq (th, th2)
+ then ((th2, src' :: srcs2) :: rest)
+ else (th, [src']) :: (th2, srcs2) :: rest);
+ in ((th, NONE), (decls', context')) end
+ | ((src', (opt_context', opt_th')), _) =>
let
val context' = the_default context opt_context';
val th' = the_default th opt_th';
- val decls' =
- (case decls of
- [] => [(th, [src])]
- | (th2, srcs2) :: rest =>
- if op = (pairself Thm.rep_thm (th, th2)) (* FIXME derivation!? *)
- then ((th2, src :: srcs2) :: rest)
- else (th, [src]) :: (th2, srcs2) :: rest);
- in (th', (decls', context')) end);
+ val dyn' =
+ (case dyn of
+ NONE => SOME (th, [src'])
+ | SOME (dyn_th, srcs) => SOME (dyn_th, src' :: srcs));
+ in ((th', dyn'), (decls, context')) end);
in
@@ -247,10 +264,18 @@
val (facts', (decls, _)) =
(facts, ([], Context.Proof ctxt)) |-> fold_map (fn ((b, more_atts), fact) => fn res =>
let
- val (thss', res') =
- (fact, res) |-> fold_map (fn (ths, atts) =>
- fold_map (curry (fold eval (atts @ more_atts))) ths);
- in (((b, []), [(flat thss', [])]), res') end);
+ val (fact', res') =
+ (fact, res) |-> fold_map (fn (ths, atts) => fn res1 =>
+ (ths, res1) |-> fold_map (fn th => fn res2 =>
+ let
+ val ((th', dyn'), res3) = fold eval (atts @ more_atts) ((th, NONE), res2);
+ val th_atts' =
+ (case dyn' of
+ NONE => ([th'], [])
+ | SOME (dyn_th', atts') => ([dyn_th'], rev atts'));
+ in (th_atts', res3) end))
+ |>> flat;
+ in (((b, []), fact'), res') end);
val decl_fact = (empty_binding, rev (map (fn (th, atts) => ([th], rev atts)) decls));
in decl_fact :: facts' end;
--- a/src/Pure/Isar/rule_cases.ML Wed Nov 16 15:20:27 2011 +0100
+++ b/src/Pure/Isar/rule_cases.ML Thu Nov 17 05:27:45 2011 +0100
@@ -247,7 +247,7 @@
val save_consumes = put_consumes o lookup_consumes;
-fun consumes n = Thm.rule_attribute (K (put_consumes (SOME n)));
+fun consumes n = Thm.mixed_attribute (apsnd (put_consumes (SOME n)));
@@ -271,7 +271,7 @@
val save_constraints = put_constraints o lookup_constraints;
-fun constraints n = Thm.rule_attribute (K (put_constraints (SOME n)));
+fun constraints n = Thm.mixed_attribute (apsnd (put_constraints (SOME n)));
@@ -293,7 +293,7 @@
val save_case_names = add_case_names o lookup_case_names;
val name = add_case_names o SOME;
-fun case_names cs = Thm.rule_attribute (K (name cs));
+fun case_names cs = Thm.mixed_attribute (apsnd (name cs));
@@ -315,7 +315,7 @@
val save_cases_hyp_names = add_cases_hyp_names o lookup_cases_hyp_names;
fun cases_hyp_names cs hs =
- Thm.rule_attribute (K (name cs #> add_cases_hyp_names (SOME hs)));
+ Thm.mixed_attribute (apsnd (name cs #> add_cases_hyp_names (SOME hs)));
@@ -342,7 +342,7 @@
else NONE)
in fold add_case_concl concls end;
-fun case_conclusion concl = Thm.rule_attribute (K (add_case_concl concl));
+fun case_conclusion concl = Thm.mixed_attribute (apsnd (add_case_concl concl));
@@ -359,7 +359,7 @@
val save_inner_rule = put_inner_rule o is_inner_rule;
-val inner_rule = Thm.rule_attribute (K (put_inner_rule true));
+val inner_rule = Thm.mixed_attribute (apsnd (put_inner_rule true));