--- a/NEWS Fri Oct 22 13:59:34 2010 +0200
+++ b/NEWS Fri Oct 22 17:15:46 2010 +0200
@@ -276,18 +276,28 @@
meson_disj_FalseD2 ~> Meson.disj_FalseD2
INCOMPATIBILITY.
-* Sledgehammer: Renamed lemmas:
- COMBI_def ~> Meson.COMBI_def
- COMBK_def ~> Meson.COMBK_def
- COMBB_def ~> Meson.COMBB_def
- COMBC_def ~> Meson.COMBC_def
- COMBS_def ~> Meson.COMBS_def
- abs_I ~> Meson.abs_I
- abs_K ~> Meson.abs_K
- abs_B ~> Meson.abs_B
- abs_C ~> Meson.abs_C
- abs_S ~> Meson.abs_S
-INCOMPATIBILITY.
+* Sledgehammer:
+ - Renamed lemmas:
+ COMBI_def ~> Meson.COMBI_def
+ COMBK_def ~> Meson.COMBK_def
+ COMBB_def ~> Meson.COMBB_def
+ COMBC_def ~> Meson.COMBC_def
+ COMBS_def ~> Meson.COMBS_def
+ abs_I ~> Meson.abs_I
+ abs_K ~> Meson.abs_K
+ abs_B ~> Meson.abs_B
+ abs_C ~> Meson.abs_C
+ abs_S ~> Meson.abs_S
+ INCOMPATIBILITY.
+ - Renamed commands:
+ sledgehammer atp_info ~> sledgehammer running_provers
+ sledgehammer atp_kill ~> sledgehammer kill_provers
+ sledgehammer available_atps ~> sledgehammer available_provers
+ INCOMPATIBILITY.
+ - Renamed options:
+ sledgehammer [atps = ...] ~> sledgehammer [provers = ...]
+ sledgehammer [atp = ...] ~> sledgehammer [prover = ...]
+ INCOMPATIBILITY.
*** FOL ***
--- a/doc-src/Sledgehammer/sledgehammer.tex Fri Oct 22 13:59:34 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Fri Oct 22 17:15:46 2010 +0200
@@ -78,24 +78,26 @@
\label{introduction}
Sledgehammer is a tool that applies first-order automatic theorem provers (ATPs)
-on the current goal. The supported ATPs are E \cite{schulz-2002}, SPASS
-\cite{weidenbach-et-al-2009}, and Vampire \cite{riazanov-voronkov-2002}, which
-can be run locally or remotely via the SystemOnTPTP web service
-\cite{sutcliffe-2000}.
+and satisfiability-modulo-theory (SMT) solvers on the current goal. The
+supported ATPs are E \cite{schulz-2002}, SPASS \cite{weidenbach-et-al-2009},
+Vampire \cite{riazanov-voronkov-2002}, SInE-E \cite{sine}, and SNARK
+\cite{snark}. The ATPs are run either locally or remotely via the
+System\-On\-TPTP web service \cite{sutcliffe-2000}. In addition to the ATPs, the
+\textit{smt} proof method (which typically relies on the Z3 SMT solver
+\cite{z3}) is tried as well.
-The problem passed to ATPs consists of your current goal together with a
-heuristic selection of hundreds of facts (theorems) from the current theory
-context, filtered by relevance. Because jobs are run in the background, you can
-continue to work on your proof by other means. Provers can be run in parallel.
-Any reply (which may arrive minutes later) will appear in the Proof General
-response buffer.
+The problem passed to the automatic provers consists of your current goal
+together with a heuristic selection of hundreds of facts (theorems) from the
+current theory context, filtered by relevance. Because jobs are run in the
+background, you can continue to work on your proof by other means. Provers can
+be run in parallel. Any reply (which may arrive half a minute later) will appear
+in the Proof General response buffer.
-The result of a successful ATP proof search is some source text that usually
-(but not always) reconstructs the proof within Isabelle, without requiring the
-ATPs again. The reconstructed proof relies on the general-purpose Metis prover
-\cite{metis}, which is fully integrated into Isabelle/HOL, with explicit
-inferences going through the kernel. Thus its results are correct by
-construction.
+The result of a successful proof search is some source text that usually (but
+not always) reconstructs the proof within Isabelle. For ATPs, the reconstructed
+proof relies on the general-purpose Metis prover \cite{metis}, which is fully
+integrated into Isabelle/HOL, with explicit inferences going through the kernel.
+Thus its results are correct by construction.
In this manual, we will explicitly invoke the \textbf{sledgehammer} command.
Sledgehammer also provides an automatic mode that can be enabled via the
@@ -123,10 +125,10 @@
\label{installation}
Sledgehammer is part of Isabelle, so you don't need to install it. However, it
-relies on third-party automatic theorem provers (ATPs). Currently, E, SPASS, and
-Vampire are supported. All of these are available remotely via SystemOnTPTP
-\cite{sutcliffe-2000}, but if you want better performance you will need to
-install at least E and SPASS locally.
+relies on third-party automatic theorem provers (ATPs) and SAT solvers.
+Currently, E, SPASS, and Vampire can be run locally; in addition, E, Vampire,
+SInE-E, and SNARK are available remotely via SystemOnTPTP \cite{sutcliffe-2000}.
+If you want better performance, you should install E and SPASS locally.
There are three main ways to install ATPs on your machine:
@@ -199,38 +201,47 @@
\prew
\slshape
-Sledgehammer: ATP ``\textit{e}'' for subgoal 1: \\
+Sledgehammer: ``\textit{e}'' for subgoal 1: \\
$([a] = [b]) = (a = b)$ \\
Try this command: \textbf{by} (\textit{metis hd.simps}). \\
To minimize the number of lemmas, try this: \\
-\textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{e}] (\textit{hd.simps}). \\[3\smallskipamount]
+\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{e}] (\textit{hd.simps}). \\[3\smallskipamount]
%
-Sledgehammer: ATP ``\textit{spass}'' for subgoal 1: \\
+Sledgehammer: ``\textit{spass}'' for subgoal 1: \\
$([a] = [b]) = (a = b)$ \\
Try this command: \textbf{by} (\textit{metis insert\_Nil last\_ConsL}). \\
To minimize the number of lemmas, try this: \\
-\textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{spass}] (\textit{insert\_Nil last\_ConsL}). \\[3\smallskipamount]
+\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{spass}] (\textit{insert\_Nil last\_ConsL}). \\[3\smallskipamount]
%
-Sledgehammer: ATP ``\textit{remote\_vampire}'' for subgoal 1: \\
+Sledgehammer: ``\textit{vampire}'' for subgoal 1: \\
+$([a] = [b]) = (a = b)$ \\
+Try this command: \textbf{by} (\textit{metis eq\_commute last\_snoc}) \\
+To minimize the number of lemmas, try this: \\
+\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{vampire}]~(\textit{eq\_commute last\_snoc}). \\[3\smallskipamount]
+%
+Sledgehammer: ``\textit{remote\_sine\_e}'' for subgoal 1: \\
$([a] = [b]) = (a = b)$ \\
-Try this command: \textbf{by} (\textit{metis One\_nat\_def\_raw empty\_replicate} \\
-\phantom{Try this command: \textbf{by} (\textit{metis~}}\textit{insert\_Nil last\_ConsL replicate\_Suc}). \\
+Try this command: \textbf{by} (\textit{metis hd.simps}) \\
To minimize the number of lemmas, try this: \\
-\textbf{sledgehammer} \textit{minimize} [\textit{atp} = \textit{remote\_vampire}] \\
-\phantom{\textbf{sledgehammer}~}(\textit{One\_nat\_def\_raw empty\_replicate insert\_Nil} \\
-\phantom{\textbf{sledgehammer}~(}\textit{last\_ConsL replicate\_Suc}).
+\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{remote\_sine\_e}]~(\textit{hd.simps}). \\[3\smallskipamount]
+%
+Sledgehammer: ``\textit{smt}'' for subgoal 1: \\
+$([a] = [b]) = (a = b)$ \\
+Try this command: \textbf{by} (\textit{smt hd.simps}) \\
+To minimize the number of lemmas, try this: \\
+\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{smt}]~(\textit{hd.simps}).
\postw
-Sledgehammer ran E, SPASS, and the remote version of Vampire in parallel. If E
-is not installed (\S\ref{installation}), you will see references to
-its remote American cousin \textit{remote\_e} instead of
-\textit{e}; and if SPASS is not installed, it will not appear in the output.
+Sledgehammer ran E, SPASS, Vampire, SInE-E, and the \textit{smt} proof method in
+parallel. Depending on which provers are installed and how many processor cores
+are available, some of the provers might be missing or present with a
+\textit{remote\_} prefix.
-Based on each ATP proof, Sledgehammer gives a one-liner proof that uses the
-\textit{metis} method. You can click them and insert them into the theory text.
-You can click the ``\textbf{sledgehammer} \textit{minimize}'' command if you
-want to look for a shorter (and faster) proof. But here the proof found by E
-looks perfect, so click it to finish the proof.
+For each successful prover, Sledgehammer gives a one-liner proof that uses the
+\textit{metis} or \textit{smt} method. You can click the proof to insert it into
+the theory text. You can click the ``\textbf{sledgehammer} \textit{minimize}''
+command if you want to look for a shorter (and probably faster) proof. But here
+the proof found by E looks perfect, so click it to finish the proof.
You can ask Sledgehammer for an Isar text proof by passing the
\textit{isar\_proof} option:
@@ -241,7 +252,7 @@
When Isar proof construction is successful, it can yield proofs that are more
readable and also faster than the \textit{metis} one-liners. This feature is
-experimental.
+experimental and is only available for ATPs.
\section{Hints}
\label{hints}
@@ -291,14 +302,16 @@
to Sledgehammer's asynchronous nature. The \textit{num} argument specifies a
limit on the number of messages to display (5 by default).
-\item[$\bullet$] \textbf{\textit{available\_atps}:} Prints the list of installed ATPs.
+\item[$\bullet$] \textbf{\textit{available\_provers}:} Prints the list of installed provers.
See \S\ref{installation} and \S\ref{mode-of-operation} for more information on
-how to install ATPs.
+how to install automatic provers.
-\item[$\bullet$] \textbf{\textit{running\_atps}:} Prints information about currently
-running ATPs, including elapsed runtime and remaining time until timeout.
+\item[$\bullet$] \textbf{\textit{running\_provers}:} Prints information about
+currently running automatic provers, including elapsed runtime and remaining
+time until timeout.
-\item[$\bullet$] \textbf{\textit{kill\_atps}:} Terminates all running ATPs.
+\item[$\bullet$] \textbf{\textit{kill\_provers}:} Terminates all running
+automatic provers.
\item[$\bullet$] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote
ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}.
@@ -334,12 +347,12 @@
You can instruct Sledgehammer to run automatically on newly entered theorems by
enabling the ``Auto Sledgehammer'' option from the ``Isabelle'' menu in Proof
-General. For automatic runs, only the first ATP set using \textit{atps}
+General. For automatic runs, only the first prover set using \textit{provers}
(\S\ref{mode-of-operation}) is considered, \textit{verbose}
(\S\ref{output-format}) and \textit{debug} (\S\ref{output-format}) are disabled,
-fewer facts are passed to the ATP, and \textit{timeout} (\S\ref{timeouts}) is
-superseded by the ``Auto Tools Time Limit'' in Proof General's ``Isabelle''
-menu. Sledgehammer's output is also more concise.
+fewer facts are passed to the prover, and \textit{timeout}
+(\S\ref{mode-of-operation}) is superseded by the ``Auto Tools Time Limit'' in
+Proof General's ``Isabelle'' menu. Sledgehammer's output is also more concise.
\section{Option Reference}
\label{option-reference}
@@ -382,9 +395,9 @@
\label{mode-of-operation}
\begin{enum}
-\opnodefault{atps}{string}
-Specifies the ATPs (automated theorem provers) to use as a space-separated list
-(e.g., ``\textit{e}~\textit{spass}''). The following ATPs are supported:
+\opnodefault{provers}{string}
+Specifies the automatic provers to use as a space-separated list (e.g.,
+``\textit{e}~\textit{spass}''). The following provers are supported:
\begin{enum}
\item[$\bullet$] \textbf{\textit{e}:} E is an ATP developed by Stephan Schulz
@@ -405,6 +418,9 @@
Vampire, set the environment variable \texttt{VAMPIRE\_HOME} to the directory
that contains the \texttt{vampire} executable.
+\item[$\bullet$] \textbf{\textit{smt}:} The \textit{smt} proof method invokes an
+external SMT prover (usually Z3 \cite{z3}).
+
\item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E runs
on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
@@ -418,27 +434,38 @@
\item[$\bullet$] \textbf{\textit{remote\_snark}:} SNARK is a prover
developed by Stickel et al.\ \cite{snark}. The remote version of
SNARK runs on Geoff Sutcliffe's Miami servers.
+
+\item[$\bullet$] \textbf{\textit{remote\_smt}:} The remote version of the
+\textit{smt} proof method runs the SMT solver on servers at the TU M\"unchen (or
+wherever \texttt{REMOTE\_SMT\_URL} is set to point).
+
\end{enum}
-By default, Sledgehammer will run E, SPASS, Vampire, and SInE-E in parallel.
-For at most two of E, SPASS, and Vampire, it will use any locally installed
-version if available. For historical reasons, the default value of this option
-can be overridden using the option ``Sledgehammer: ATPs'' from the ``Isabelle''
-menu in Proof General.
+By default, Sledgehammer will run E, SPASS, Vampire, SInE-E, and \textit{smt} in
+parallel---either locally or remotely, depending on the number of processor
+cores available. For historical reasons, the default value of this option can be
+overridden using the option ``Sledgehammer: Provers'' from the ``Isabelle'' menu
+in Proof General.
-It is a good idea to run several ATPs in parallel, although it could slow down
-your machine. Running E, SPASS, and Vampire together for 5 seconds yields about
-the same success rate as running the most effective of these (Vampire) for 120
-seconds \cite{boehme-nipkow-2010}.
+It is a good idea to run several provers in parallel, although it could slow
+down your machine. Running E, SPASS, Vampire, and SInE-E together for 5 seconds
+yields a better success rate than running the most effective of these (Vampire)
+for 120 seconds \cite{boehme-nipkow-2010}.
+
+\opnodefault{prover}{string}
+Alias for \textit{provers}.
+
+\opnodefault{atps}{string}
+Legacy alias for \textit{provers}.
\opnodefault{atp}{string}
-Alias for \textit{atps}.
+Legacy alias for \textit{provers}.
\opdefault{timeout}{time}{$\mathbf{30}$ s}
-Specifies the maximum amount of time that the ATPs should spend searching for a
-proof. For historical reasons, the default value of this option can be
-overridden using the option ``Sledgehammer: Time Limit'' from the ``Isabelle''
-menu in Proof General.
+Specifies the maximum amount of time that the automatic provers should spend
+searching for a proof. For historical reasons, the default value of this option
+can be overridden using the option ``Sledgehammer: Time Limit'' from the
+``Isabelle'' menu in Proof General.
\opfalse{blocking}{non\_blocking}
Specifies whether the \textbf{sledgehammer} command should operate
@@ -463,16 +490,17 @@
\begin{enum}
\opfalse{explicit\_apply}{implicit\_apply}
Specifies whether function application should be encoded as an explicit
-``apply'' operator. If the option is set to \textit{false}, each function will
-be directly applied to as many arguments as possible. Enabling this option can
-sometimes help discover higher-order proofs that otherwise would not be found.
+``apply'' operator in ATP problems. If the option is set to \textit{false}, each
+function will be directly applied to as many arguments as possible. Enabling
+this option can sometimes help discover higher-order proofs that otherwise would
+not be found.
\opfalse{full\_types}{partial\_types}
-Specifies whether full-type information is exported. Enabling this option can
-prevent the discovery of type-incorrect proofs, but it also tends to slow down
-the ATPs significantly. For historical reasons, the default value of this option
-can be overridden using the option ``Sledgehammer: ATPs'' from the ``Isabelle''
-menu in Proof General.
+Specifies whether full-type information is encoded in ATP problems. Enabling
+this option can prevent the discovery of type-incorrect proofs, but it also
+tends to slow down the ATPs significantly. For historical reasons, the default
+value of this option can be overridden using the option ``Sledgehammer: Full
+Types'' from the ``Isabelle'' menu in Proof General.
\end{enum}
\subsection{Relevance Filter}
@@ -490,18 +518,8 @@
\opdefault{max\_relevant}{int\_or\_smart}{\textit{smart}}
Specifies the maximum number of facts that may be returned by the relevance
filter. If the option is set to \textit{smart}, it is set to a value that was
-empirically found to be appropriate for the ATP. A typical value would be 300.
-
-%\opsmartx{theory\_relevant}{theory\_irrelevant}
-%Specifies whether the theory from which a fact comes should be taken into
-%consideration by the relevance filter. If the option is set to \textit{smart},
-%it is taken to be \textit{true} for SPASS and \textit{false} for the other ATPs;
-%empirical results suggest that these are the best settings.
-
-%\opfalse{defs\_relevant}{defs\_irrelevant}
-%Specifies whether the definition of constants occurring in the formula to prove
-%should be considered particularly relevant. Enabling this option tends to lead
-%to larger problems and typically slows down the ATPs.
+empirically found to be appropriate for the prover. A typical value would be
+300.
\end{enum}
\subsection{Output Format}
--- a/doc-src/manual.bib Fri Oct 22 13:59:34 2010 +0200
+++ b/doc-src/manual.bib Fri Oct 22 17:15:46 2010 +0200
@@ -1593,6 +1593,11 @@
note = {\url{http://www.cs.kun.nl/~freek/notes/mv.ps.gz}}
}
+@misc{wikipedia-2009-aa-trees,
+ key = "Wikipedia",
+ title = "Wikipedia: {AA} Tree",
+ note = "\url{http://en.wikipedia.org/wiki/AA_tree}"}
+
@book{winskel93,
author = {Glynn Winskel},
title = {The Formal Semantics of Programming Languages},
@@ -1611,6 +1616,11 @@
%Z
+@misc{z3,
+ key = "Z3",
+ title = "Z3: An Efficient {SMT} Solver",
+ note = "\url{http://research.microsoft.com/en-us/um/redmond/projects/z3/}"}
+
% CROSS REFERENCES
@@ -1855,8 +1865,3 @@
title = {{ML} Modules and {Haskell} Type Classes: A Constructive Comparison},
author = {Stefan Wehr et. al.}
}
-
-@misc{wikipedia-2009-aa-trees,
- key = "Wikipedia",
- title = "Wikipedia: {AA} Tree",
- note = "\url{http://en.wikipedia.org/wiki/AA_tree}"}
--- a/src/HOL/IsaMakefile Fri Oct 22 13:59:34 2010 +0200
+++ b/src/HOL/IsaMakefile Fri Oct 22 17:15:46 2010 +0200
@@ -327,8 +327,8 @@
Tools/Sledgehammer/sledgehammer_filter.ML \
Tools/Sledgehammer/sledgehammer_minimize.ML \
Tools/Sledgehammer/sledgehammer_isar.ML \
- Tools/Sledgehammer/sledgehammer_reconstruct.ML \
- Tools/Sledgehammer/sledgehammer_translate.ML \
+ Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML \
+ Tools/Sledgehammer/sledgehammer_atp_translate.ML \
Tools/Sledgehammer/sledgehammer_util.ML \
Tools/SMT/cvc3_solver.ML \
Tools/SMT/smtlib_interface.ML \
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Oct 22 13:59:34 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Oct 22 17:15:46 2010 +0200
@@ -29,8 +29,8 @@
lemmas: int,
max_lems: int,
time_isa: int,
- time_atp: int,
- time_atp_fail: int}
+ time_prover: int,
+ time_prover_fail: int}
datatype me_data = MeData of {
calls: int,
@@ -51,10 +51,11 @@
fun make_sh_data
(calls,success,nontriv_calls,nontriv_success,lemmas,max_lems,time_isa,
- time_atp,time_atp_fail) =
+ time_prover,time_prover_fail) =
ShData{calls=calls, success=success, nontriv_calls=nontriv_calls,
nontriv_success=nontriv_success, lemmas=lemmas, max_lems=max_lems,
- time_isa=time_isa, time_atp=time_atp, time_atp_fail=time_atp_fail}
+ time_isa=time_isa, time_prover=time_prover,
+ time_prover_fail=time_prover_fail}
fun make_min_data (succs, ab_ratios) =
MinData{succs=succs, ab_ratios=ab_ratios}
@@ -71,8 +72,8 @@
fun tuple_of_sh_data (ShData {calls, success, nontriv_calls, nontriv_success,
lemmas, max_lems, time_isa,
- time_atp, time_atp_fail}) = (calls, success, nontriv_calls, nontriv_success,
- lemmas, max_lems, time_isa, time_atp, time_atp_fail)
+ time_prover, time_prover_fail}) = (calls, success, nontriv_calls,
+ nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)
fun tuple_of_min_data (MinData {succs, ab_ratios}) = (succs, ab_ratios)
@@ -127,40 +128,40 @@
fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n));
val inc_sh_calls = map_sh_data
- (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_atp, time_atp_fail)
- => (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_atp, time_atp_fail))
+ (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)
+ => (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail))
val inc_sh_success = map_sh_data
- (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_atp, time_atp_fail)
- => (calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_atp, time_atp_fail))
+ (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)
+ => (calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail))
val inc_sh_nontriv_calls = map_sh_data
- (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_atp, time_atp_fail)
- => (calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_atp, time_atp_fail))
+ (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)
+ => (calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail))
val inc_sh_nontriv_success = map_sh_data
- (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_atp, time_atp_fail)
- => (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_atp, time_atp_fail))
+ (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)
+ => (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_prover, time_prover_fail))
fun inc_sh_lemmas n = map_sh_data
- (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail)
- => (calls,success,nontriv_calls, nontriv_success, lemmas+n,max_lems,time_isa,time_atp,time_atp_fail))
+ (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)
+ => (calls,success,nontriv_calls, nontriv_success, lemmas+n,max_lems,time_isa,time_prover,time_prover_fail))
fun inc_sh_max_lems n = map_sh_data
- (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail)
- => (calls,success,nontriv_calls, nontriv_success, lemmas,Int.max(max_lems,n),time_isa,time_atp,time_atp_fail))
+ (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)
+ => (calls,success,nontriv_calls, nontriv_success, lemmas,Int.max(max_lems,n),time_isa,time_prover,time_prover_fail))
fun inc_sh_time_isa t = map_sh_data
- (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail)
- => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa + t,time_atp,time_atp_fail))
+ (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)
+ => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa + t,time_prover,time_prover_fail))
-fun inc_sh_time_atp t = map_sh_data
- (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail)
- => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp + t,time_atp_fail))
+fun inc_sh_time_prover t = map_sh_data
+ (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)
+ => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover + t,time_prover_fail))
-fun inc_sh_time_atp_fail t = map_sh_data
- (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail)
- => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail + t))
+fun inc_sh_time_prover_fail t = map_sh_data
+ (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)
+ => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail + t))
val inc_min_succs = map_min_data
(fn (succs,ab_ratios) => (succs+1, ab_ratios))
@@ -214,7 +215,7 @@
if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0
fun log_sh_data log
- (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_atp, time_atp_fail) =
+ (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) =
(log ("Total number of sledgehammer calls: " ^ str calls);
log ("Number of successful sledgehammer calls: " ^ str success);
log ("Number of sledgehammer lemmas: " ^ str lemmas);
@@ -223,14 +224,14 @@
log ("Total number of nontrivial sledgehammer calls: " ^ str nontriv_calls);
log ("Number of successful nontrivial sledgehammer calls: " ^ str nontriv_success);
log ("Total time for sledgehammer calls (Isabelle): " ^ str3 (time time_isa));
- log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time time_atp));
- log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time time_atp_fail));
+ log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time time_prover));
+ log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time time_prover_fail));
log ("Average time for sledgehammer calls (Isabelle): " ^
str3 (avg_time time_isa calls));
log ("Average time for successful sledgehammer calls (ATP): " ^
- str3 (avg_time time_atp success));
+ str3 (avg_time time_prover success));
log ("Average time for failed sledgehammer calls (ATP): " ^
- str3 (avg_time time_atp_fail (calls - success)))
+ str3 (avg_time time_prover_fail (calls - success)))
)
@@ -313,16 +314,17 @@
fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ())
-fun get_atp thy args =
+fun get_prover ctxt args =
let
- fun default_atp_name () =
- hd (#atps (Sledgehammer_Isar.default_params thy []))
+ val thy = ProofContext.theory_of ctxt
+ fun default_prover_name () =
+ hd (#provers (Sledgehammer_Isar.default_params ctxt []))
handle Empty => error "No ATP available."
- fun get_prover name = (name, Sledgehammer.get_prover_fun thy name)
+ fun get_prover name = (name, Sledgehammer.get_prover thy false name)
in
(case AList.lookup (op =) args proverK of
SOME name => get_prover name
- | NONE => get_prover (default_atp_name ()))
+ | NONE => get_prover (default_prover_name ()))
end
type locality = Sledgehammer_Filter.locality
@@ -346,31 +348,35 @@
(change_dir dir
#> Config.put Sledgehammer.measure_run_time true)
val params as {full_types, relevance_thresholds, max_relevant, ...} =
- Sledgehammer_Isar.default_params thy
+ Sledgehammer_Isar.default_params ctxt
[("timeout", Int.toString timeout ^ " s")]
+ val default_max_relevant =
+ Sledgehammer.default_max_relevant_for_prover thy prover_name
+ val irrelevant_consts =
+ Sledgehammer.irrelevant_consts_for_prover prover_name
+ val relevance_fudge = Sledgehammer.relevance_fudge_for_prover prover_name
val relevance_override = {add = [], del = [], only = false}
- val {default_max_relevant, ...} = ATP_Systems.get_prover thy prover_name
val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
val axioms =
Sledgehammer_Filter.relevant_facts ctxt full_types relevance_thresholds
- (the_default default_max_relevant max_relevant)
- relevance_override chained_ths hyp_ts concl_t
+ (the_default default_max_relevant max_relevant) irrelevant_consts
+ relevance_fudge relevance_override chained_ths hyp_ts concl_t
val problem =
{state = st', goal = goal, subgoal = i,
- axioms = map (Sledgehammer_Translate.prepare_axiom ctxt) axioms,
- only = true}
+ subgoal_count = Sledgehammer_Util.subgoal_count st,
+ axioms = axioms |> map Sledgehammer.Unprepared, only = true}
val time_limit =
(case hard_timeout of
NONE => I
| SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
- val ({outcome, message, used_thm_names,
- atp_run_time_in_msecs = time_atp, ...} : Sledgehammer.prover_result,
+ val ({outcome, message, used_axioms, run_time_in_msecs = SOME time_prover, ...}
+ : Sledgehammer.prover_result,
time_isa) = time_limit (Mirabelle.cpu_time
(prover params (K ""))) problem
in
case outcome of
- NONE => (message, SH_OK (time_isa, time_atp, used_thm_names))
- | SOME _ => (message, SH_FAIL (time_isa, time_atp))
+ NONE => (message, SH_OK (time_isa, time_prover, used_axioms))
+ | SOME _ => (message, SH_FAIL (time_isa, time_prover))
end
handle ERROR msg => ("error: " ^ msg, SH_ERROR)
| TimeLimit.TimeOut => ("timeout", SH_ERROR)
@@ -395,7 +401,7 @@
val triv_str = if trivial then "[T] " else ""
val _ = change_data id inc_sh_calls
val _ = if trivial then () else change_data id inc_sh_nontriv_calls
- val (prover_name, prover) = get_atp (Proof.theory_of st) args
+ val (prover_name, prover) = get_prover (Proof.context_of st) args
val dir = AList.lookup (op =) args keepK
val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
val hard_timeout = AList.lookup (op =) args prover_hard_timeoutK
@@ -403,7 +409,7 @@
val (msg, result) = run_sh prover_name prover hard_timeout timeout dir st
in
case result of
- SH_OK (time_isa, time_atp, names) =>
+ SH_OK (time_isa, time_prover, names) =>
let
fun get_thms (_, Sledgehammer_Filter.Chained) = NONE
| get_thms (name, loc) =
@@ -414,38 +420,36 @@
change_data id (inc_sh_lemmas (length names));
change_data id (inc_sh_max_lems (length names));
change_data id (inc_sh_time_isa time_isa);
- change_data id (inc_sh_time_atp time_atp);
+ change_data id (inc_sh_time_prover time_prover);
named_thms := SOME (map_filter get_thms names);
log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^
- string_of_int time_atp ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
+ string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
end
- | SH_FAIL (time_isa, time_atp) =>
+ | SH_FAIL (time_isa, time_prover) =>
let
val _ = change_data id (inc_sh_time_isa time_isa)
- val _ = change_data id (inc_sh_time_atp_fail time_atp)
+ val _ = change_data id (inc_sh_time_prover_fail time_prover)
in log (sh_tag id ^ triv_str ^ "failed: " ^ msg) end
| SH_ERROR => log (sh_tag id ^ "failed: " ^ msg)
end
end
-
-val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
-
fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
let
open Metis_Translate
- val thy = Proof.theory_of st
+ val ctxt = Proof.context_of st
val n0 = length (these (!named_thms))
- val (prover_name, _) = get_atp thy args
+ val (prover_name, _) = get_prover ctxt args
val timeout =
AList.lookup (op =) args minimize_timeoutK
|> Option.map (fst o read_int o explode)
|> the_default 5
- val params = Sledgehammer_Isar.default_params thy
- [("atps", prover_name), ("timeout", Int.toString timeout ^ " s")]
+ val params = Sledgehammer_Isar.default_params ctxt
+ [("provers", prover_name), ("timeout", Int.toString timeout ^ " s")]
val minimize =
- Sledgehammer_Minimize.minimize_theorems params 1 (subgoal_count st)
+ Sledgehammer_Minimize.minimize_facts params 1
+ (Sledgehammer_Util.subgoal_count st)
val _ = log separator
in
case minimize st (these (!named_thms)) of
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Oct 22 13:59:34 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Oct 22 17:15:46 2010 +0200
@@ -5,26 +5,37 @@
structure Mirabelle_Sledgehammer_Filter : MIRABELLE_ACTION =
struct
-structure SF = Sledgehammer_Filter
+fun get args name default_value =
+ case AList.lookup (op =) args name of
+ SOME value => the (Real.fromString value)
+ | NONE => default_value
-val relevance_filter_args =
- [("worse_irrel_freq", SF.worse_irrel_freq),
- ("higher_order_irrel_weight", SF.higher_order_irrel_weight),
- ("abs_rel_weight", SF.abs_rel_weight),
- ("abs_irrel_weight", SF.abs_irrel_weight),
- ("skolem_irrel_weight", SF.skolem_irrel_weight),
- ("theory_const_rel_weight", SF.theory_const_rel_weight),
- ("theory_const_irrel_weight", SF.theory_const_irrel_weight),
- ("intro_bonus", SF.intro_bonus),
- ("elim_bonus", SF.elim_bonus),
- ("simp_bonus", SF.simp_bonus),
- ("local_bonus", SF.local_bonus),
- ("assum_bonus", SF.assum_bonus),
- ("chained_bonus", SF.chained_bonus),
- ("max_imperfect", SF.max_imperfect),
- ("max_imperfect_exp", SF.max_imperfect_exp),
- ("threshold_divisor", SF.threshold_divisor),
- ("ridiculous_threshold", SF.ridiculous_threshold)]
+fun extract_relevance_fudge args
+ {worse_irrel_freq, higher_order_irrel_weight, abs_rel_weight,
+ abs_irrel_weight, skolem_irrel_weight, theory_const_rel_weight,
+ theory_const_irrel_weight, intro_bonus, elim_bonus, simp_bonus,
+ local_bonus, assum_bonus, chained_bonus, max_imperfect,
+ max_imperfect_exp, threshold_divisor, ridiculous_threshold} =
+ {worse_irrel_freq = get args "worse_irrel_freq" worse_irrel_freq,
+ higher_order_irrel_weight =
+ get args "higher_order_irrel_weight" higher_order_irrel_weight,
+ abs_rel_weight = get args "abs_rel_weight" abs_rel_weight,
+ abs_irrel_weight = get args "abs_irrel_weight" abs_irrel_weight,
+ skolem_irrel_weight = get args "skolem_irrel_weight" skolem_irrel_weight,
+ theory_const_rel_weight =
+ get args "theory_const_rel_weight" theory_const_rel_weight,
+ theory_const_irrel_weight =
+ get args "theory_const_irrel_weight" theory_const_irrel_weight,
+ intro_bonus = get args "intro_bonus" intro_bonus,
+ elim_bonus = get args "elim_bonus" elim_bonus,
+ simp_bonus = get args "simp_bonus" simp_bonus,
+ local_bonus = get args "local_bonus" local_bonus,
+ assum_bonus = get args "assum_bonus" assum_bonus,
+ chained_bonus = get args "chained_bonus" chained_bonus,
+ max_imperfect = get args "max_imperfect" max_imperfect,
+ max_imperfect_exp = get args "max_imperfect_exp" max_imperfect_exp,
+ threshold_divisor = get args "threshold_divisor" threshold_divisor,
+ ridiculous_threshold = get args "ridiculous_threshold" ridiculous_threshold}
structure Prooftab =
Table(type key = int * int val ord = prod_ord int_ord int_ord);
@@ -85,6 +96,7 @@
()
val default_max_relevant = 300
+val prover_name = ATP_Systems.eN (* arbitrary ATP *)
fun with_index (i, s) = s ^ "@" ^ string_of_int i
@@ -95,23 +107,22 @@
SOME proofs =>
let
val {context = ctxt, facts, goal} = Proof.goal pre
- val thy = ProofContext.theory_of ctxt
- val args =
- args
- |> filter (fn (key, value) =>
- case AList.lookup (op =) relevance_filter_args key of
- SOME rf => (rf := the (Real.fromString value); false)
- | NONE => true)
-
+ val irrelevant_consts =
+ Sledgehammer.irrelevant_consts_for_prover prover_name
+ val relevance_fudge =
+ extract_relevance_fudge args
+ (Sledgehammer.relevance_fudge_for_prover prover_name)
+ val relevance_override = {add = [], del = [], only = false}
val {relevance_thresholds, full_types, max_relevant, ...} =
- Sledgehammer_Isar.default_params thy args
+ Sledgehammer_Isar.default_params ctxt args
val subgoal = 1
val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal
val facts =
- SF.relevant_facts ctxt full_types
+ Sledgehammer_Filter.relevant_facts ctxt full_types
relevance_thresholds
(the_default default_max_relevant max_relevant)
- {add = [], del = [], only = false} facts hyp_ts concl_t
+ irrelevant_consts relevance_fudge relevance_override facts hyp_ts
+ concl_t
|> map (fst o fst)
val (found_facts, lost_facts) =
List.concat proofs |> sort_distinct string_ord
--- a/src/HOL/Sledgehammer.thy Fri Oct 22 13:59:34 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Fri Oct 22 17:15:46 2010 +0200
@@ -10,8 +10,8 @@
imports ATP
uses "Tools/Sledgehammer/sledgehammer_util.ML"
"Tools/Sledgehammer/sledgehammer_filter.ML"
- "Tools/Sledgehammer/sledgehammer_translate.ML"
- "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
+ "Tools/Sledgehammer/sledgehammer_atp_translate.ML"
+ "Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML"
"Tools/Sledgehammer/sledgehammer.ML"
"Tools/Sledgehammer/sledgehammer_minimize.ML"
"Tools/Sledgehammer/sledgehammer_isar.ML"
--- a/src/HOL/Tools/ATP/atp_systems.ML Fri Oct 22 13:59:34 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Oct 22 17:15:46 2010 +0200
@@ -9,7 +9,7 @@
sig
type failure = ATP_Proof.failure
- type prover_config =
+ type atp_config =
{exec: string * string,
required_execs: (string * string) list,
arguments: bool -> Time.time -> string,
@@ -20,11 +20,17 @@
explicit_forall: bool,
use_conjecture_for_hypotheses: bool}
- val add_prover: string * prover_config -> theory -> theory
- val get_prover: theory -> string -> prover_config
- val available_atps: theory -> unit
+ val eN : string
+ val spassN : string
+ val vampireN : string
+ val sine_eN : string
+ val snarkN : string
+ val remote_prefix : string
+ val add_atp : string * atp_config -> theory -> theory
+ val get_atp : theory -> string -> atp_config
+ val available_atps : theory -> string list
+ val is_atp_installed : theory -> string -> bool
val refresh_systems_on_tptp : unit -> unit
- val default_atps_param_value : unit -> string
val setup : theory -> theory
end;
@@ -33,9 +39,9 @@
open ATP_Proof
-(* prover configuration *)
+(* ATP configuration *)
-type prover_config =
+type atp_config =
{exec: string * string,
required_execs: (string * string) list,
arguments: bool -> Time.time -> string,
@@ -51,33 +57,28 @@
(NoPerl, "env: perl"),
(NoLibwwwPerl, "Can't locate HTTP")]
-(* named provers *)
+(* named ATPs *)
+
+val eN = "e"
+val spassN = "spass"
+val vampireN = "vampire"
+val sine_eN = "sine_e"
+val snarkN = "snark"
+val remote_prefix = "remote_"
structure Data = Theory_Data
(
- type T = (prover_config * stamp) Symtab.table
+ type T = (atp_config * stamp) Symtab.table
val empty = Symtab.empty
val extend = I
fun merge data : T = Symtab.merge (eq_snd op =) data
handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
)
-fun add_prover (name, config) thy =
- Data.map (Symtab.update_new (name, (config, stamp ()))) thy
- handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
-
-fun get_prover thy name =
- the (Symtab.lookup (Data.get thy) name) |> fst
- handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
-
-fun available_atps thy =
- priority ("Available ATPs: " ^
- commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
-
fun to_secs bonus time = (Time.toMilliseconds time + bonus + 999) div 1000
-(* E prover *)
+(* E *)
(* Give older versions of E an extra second, because the "eproof" script wrongly
subtracted an entire second to account for the overhead of the script
@@ -92,7 +93,7 @@
val tstp_proof_delims =
("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
-val e_config : prover_config =
+val e_config : atp_config =
{exec = ("E_HOME", "eproof"),
required_execs = [],
arguments = fn _ => fn timeout =>
@@ -113,14 +114,14 @@
explicit_forall = false,
use_conjecture_for_hypotheses = true}
-val e = ("e", e_config)
+val e = (eN, e_config)
(* SPASS *)
(* The "-VarWeight=3" option helps the higher-order problems, probably by
counteracting the presence of "hAPP". *)
-val spass_config : prover_config =
+val spass_config : atp_config =
{exec = ("ISABELLE_ATP", "scripts/spass"),
required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
arguments = fn complete => fn timeout =>
@@ -142,12 +143,12 @@
explicit_forall = true,
use_conjecture_for_hypotheses = true}
-val spass = ("spass", spass_config)
+val spass = (spassN, spass_config)
(* Vampire *)
-val vampire_config : prover_config =
+val vampire_config : atp_config =
{exec = ("VAMPIRE_HOME", "vampire"),
required_execs = [],
arguments = fn complete => fn timeout =>
@@ -172,10 +173,10 @@
explicit_forall = false,
use_conjecture_for_hypotheses = true}
-val vampire = ("vampire", vampire_config)
+val vampire = (vampireN, vampire_config)
-(* Remote prover invocation via SystemOnTPTP *)
+(* Remote ATP invocation via SystemOnTPTP *)
val systems = Synchronized.var "atp_systems" ([] : string list)
@@ -187,9 +188,6 @@
SOME failure => string_for_failure failure
| NONE => perhaps (try (unsuffix "\n")) output ^ ".")
-fun refresh_systems_on_tptp () =
- Synchronized.change systems (fn _ => get_systems ())
-
fun find_system name [] systems = find_first (String.isPrefix name) systems
| find_system name (version :: versions) systems =
case find_first (String.isPrefix (name ^ "---" ^ version)) systems of
@@ -208,7 +206,7 @@
fun remote_config system_name system_versions proof_delims known_failures
default_max_relevant use_conjecture_for_hypotheses
- : prover_config =
+ : atp_config =
{exec = ("ISABELLE_ATP", "scripts/remote_atp"),
required_execs = [],
arguments = fn _ => fn timeout =>
@@ -225,48 +223,49 @@
fun remotify_config system_name system_versions
({proof_delims, known_failures, default_max_relevant,
- use_conjecture_for_hypotheses, ...} : prover_config) : prover_config =
+ use_conjecture_for_hypotheses, ...} : atp_config) : atp_config =
remote_config system_name system_versions proof_delims known_failures
default_max_relevant use_conjecture_for_hypotheses
-val remotify_name = prefix "remote_"
-fun remote_prover name system_name system_versions proof_delims known_failures
- default_max_relevant use_conjecture_for_hypotheses =
- (remotify_name name,
+fun remote_atp name system_name system_versions proof_delims known_failures
+ default_max_relevant use_conjecture_for_hypotheses =
+ (remote_prefix ^ name,
remote_config system_name system_versions proof_delims known_failures
default_max_relevant use_conjecture_for_hypotheses)
-fun remotify_prover (name, config) system_name system_versions =
- (remotify_name name, remotify_config system_name system_versions config)
+fun remotify_atp (name, config) system_name system_versions =
+ (remote_prefix ^ name, remotify_config system_name system_versions config)
-val remote_e = remotify_prover e "EP" ["1.0", "1.1", "1.2"]
-val remote_vampire = remotify_prover vampire "Vampire" ["0.6", "9.0", "1.0"]
+val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"]
+val remote_vampire = remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
val remote_sine_e =
- remote_prover "sine_e" "SInE" [] [] [(IncompleteUnprovable, "says Unknown")]
+ remote_atp sine_eN "SInE" [] [] [(IncompleteUnprovable, "says Unknown")]
800 (* FUDGE *) true
val remote_snark =
- remote_prover "snark" "SNARK---" [] [("refutation.", "end_refutation.")] []
- 250 (* FUDGE *) true
+ remote_atp snarkN "SNARK---" [] [("refutation.", "end_refutation.")] []
+ 250 (* FUDGE *) true
(* Setup *)
-fun is_installed ({exec, required_execs, ...} : prover_config) =
- forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
-fun maybe_remote (name, config) =
- name |> not (is_installed config) ? remotify_name
+fun add_atp (name, config) thy =
+ Data.map (Symtab.update_new (name, (config, stamp ()))) thy
+ handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
+
+fun get_atp thy name =
+ the (Symtab.lookup (Data.get thy) name) |> fst
+ handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
+
+val available_atps = Symtab.keys o Data.get
-(* The first prover of the list is used by Auto Sledgehammer. Because of the low
- timeout, it makes sense to put SPASS first. *)
-fun default_atps_param_value () =
- space_implode " " ((if is_installed (snd spass) then [fst spass] else []) @
- [maybe_remote e] @
- [if forall (is_installed o snd) [e, spass] then
- remotify_name (fst vampire)
- else
- maybe_remote vampire,
- fst remote_sine_e])
+fun is_atp_installed thy name =
+ let val {exec, required_execs, ...} = get_atp thy name in
+ forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
+ end
-val provers = [e, spass, vampire, remote_e, remote_vampire, remote_sine_e,
- remote_snark]
-val setup = fold add_prover provers
+fun refresh_systems_on_tptp () =
+ Synchronized.change systems (fn _ => get_systems ())
+
+val atps = [e, spass, vampire, remote_e, remote_vampire, remote_sine_e,
+ remote_snark]
+val setup = fold add_atp atps
end;
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Oct 22 13:59:34 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Oct 22 17:15:46 2010 +0200
@@ -448,8 +448,7 @@
fun add_notin_mtype_fv sn M ((lits, comps, sexps) : constraint_set) =
(trace_msg (fn () => "*** Add " ^ string_for_mtype M ^ " is " ^
- (case sn of Minus => "concrete" | Plus => "complete") ^
- ".");
+ (case sn of Minus => "concrete" | Plus => "complete"));
case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of
NONE => (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ())
| SOME (lits, sexps) => (lits, comps, sexps))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 22 13:59:34 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 22 17:15:46 2010 +0200
@@ -10,16 +10,17 @@
sig
type failure = ATP_Systems.failure
type locality = Sledgehammer_Filter.locality
+ type relevance_fudge = Sledgehammer_Filter.relevance_fudge
type relevance_override = Sledgehammer_Filter.relevance_override
- type fol_formula = Sledgehammer_Translate.fol_formula
- type minimize_command = Sledgehammer_Reconstruct.minimize_command
+ type prepared_formula = Sledgehammer_ATP_Translate.prepared_formula
+ type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
type params =
{blocking: bool,
debug: bool,
verbose: bool,
overlord: bool,
- atps: string list,
+ provers: string list,
full_types: bool,
explicit_apply: bool,
relevance_thresholds: real * real,
@@ -29,33 +30,40 @@
timeout: Time.time,
expect: string}
- type problem =
+ datatype axiom =
+ Unprepared of (string * locality) * thm |
+ Prepared of term * ((string * locality) * prepared_formula) option
+
+ type prover_problem =
{state: Proof.state,
goal: thm,
subgoal: int,
- axioms: (term * ((string * locality) * fol_formula) option) list,
+ subgoal_count: int,
+ axioms: axiom list,
only: bool}
type prover_result =
{outcome: failure option,
- message: string,
- pool: string Symtab.table,
- used_thm_names: (string * locality) list,
- atp_run_time_in_msecs: int,
- output: string,
- tstplike_proof: string,
- axiom_names: (string * locality) list vector,
- conjecture_shape: int list list}
+ used_axioms: (string * locality) list,
+ run_time_in_msecs: int option,
+ message: string}
+
+ type prover = params -> minimize_command -> prover_problem -> prover_result
- type prover = params -> minimize_command -> problem -> prover_result
-
+ val smtN : string
+ val is_prover_available : theory -> string -> bool
+ val is_prover_installed : Proof.context -> string -> bool
+ val default_max_relevant_for_prover : theory -> string -> int
+ val irrelevant_consts_for_prover : string -> string list
+ val relevance_fudge_for_prover : string -> relevance_fudge
val dest_dir : string Config.T
val problem_prefix : string Config.T
val measure_run_time : bool Config.T
- val kill_atps: unit -> unit
- val running_atps: unit -> unit
- val messages: int option -> unit
- val get_prover_fun : theory -> string -> prover
+ val available_provers : theory -> unit
+ val kill_provers : unit -> unit
+ val running_provers : unit -> unit
+ val messages : int option -> unit
+ val get_prover : theory -> bool -> string -> prover
val run_sledgehammer :
params -> bool -> int -> relevance_override -> (string -> minimize_command)
-> Proof.state -> bool * Proof.state
@@ -71,8 +79,8 @@
open Metis_Translate
open Sledgehammer_Util
open Sledgehammer_Filter
-open Sledgehammer_Translate
-open Sledgehammer_Reconstruct
+open Sledgehammer_ATP_Translate
+open Sledgehammer_ATP_Reconstruct
(** The Sledgehammer **)
@@ -81,18 +89,102 @@
"Async_Manager". *)
val das_Tool = "Sledgehammer"
-fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs"
-fun running_atps () = Async_Manager.running_threads das_Tool "ATPs"
-val messages = Async_Manager.thread_messages das_Tool "ATP"
+val smtN = "smt"
+val smt_prover_names = [smtN, remote_prefix ^ smtN]
+
+val is_smt_prover = member (op =) smt_prover_names
+
+fun is_prover_available thy name =
+ is_smt_prover name orelse member (op =) (available_atps thy) name
+
+fun is_prover_installed ctxt name =
+ let val thy = ProofContext.theory_of ctxt in
+ if is_smt_prover name then true (* FIXME *)
+ else is_atp_installed thy name
+ end
+
+val smt_default_max_relevant = 300 (* FUDGE (FIXME) *)
+val auto_max_relevant_divisor = 2 (* FUDGE *)
+
+fun default_max_relevant_for_prover thy name =
+ if is_smt_prover name then smt_default_max_relevant
+ else #default_max_relevant (get_atp thy name)
+
+(* These are typically simplified away by "Meson.presimplify". Equality is
+ handled specially via "fequal". *)
+val atp_irrelevant_consts =
+ [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let},
+ @{const_name HOL.eq}]
+val smt_irrelevant_consts = atp_irrelevant_consts (* FIXME *)
+
+fun irrelevant_consts_for_prover name =
+ if is_smt_prover name then smt_irrelevant_consts else atp_irrelevant_consts
-(** problems, results, provers, etc. **)
+(* FUDGE *)
+val atp_relevance_fudge =
+ {worse_irrel_freq = 100.0,
+ higher_order_irrel_weight = 1.05,
+ abs_rel_weight = 0.5,
+ abs_irrel_weight = 2.0,
+ skolem_irrel_weight = 0.75,
+ theory_const_rel_weight = 0.5,
+ theory_const_irrel_weight = 0.25,
+ intro_bonus = 0.15,
+ elim_bonus = 0.15,
+ simp_bonus = 0.15,
+ local_bonus = 0.55,
+ assum_bonus = 1.05,
+ chained_bonus = 1.5,
+ max_imperfect = 11.5,
+ max_imperfect_exp = 1.0,
+ threshold_divisor = 2.0,
+ ridiculous_threshold = 0.1}
+
+(* FUDGE (FIXME) *)
+val smt_relevance_fudge =
+ {worse_irrel_freq = #worse_irrel_freq atp_relevance_fudge,
+ higher_order_irrel_weight = #higher_order_irrel_weight atp_relevance_fudge,
+ abs_rel_weight = #abs_rel_weight atp_relevance_fudge,
+ abs_irrel_weight = #abs_irrel_weight atp_relevance_fudge,
+ skolem_irrel_weight = #skolem_irrel_weight atp_relevance_fudge,
+ theory_const_rel_weight = #theory_const_rel_weight atp_relevance_fudge,
+ theory_const_irrel_weight = #theory_const_irrel_weight atp_relevance_fudge,
+ intro_bonus = #intro_bonus atp_relevance_fudge,
+ elim_bonus = #elim_bonus atp_relevance_fudge,
+ simp_bonus = #simp_bonus atp_relevance_fudge,
+ local_bonus = #local_bonus atp_relevance_fudge,
+ assum_bonus = #assum_bonus atp_relevance_fudge,
+ chained_bonus = #chained_bonus atp_relevance_fudge,
+ max_imperfect = #max_imperfect atp_relevance_fudge,
+ max_imperfect_exp = #max_imperfect_exp atp_relevance_fudge,
+ threshold_divisor = #threshold_divisor atp_relevance_fudge,
+ ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge}
+
+fun relevance_fudge_for_prover name =
+ if is_smt_prover name then smt_relevance_fudge else atp_relevance_fudge
+
+fun available_provers thy =
+ let
+ val (remote_provers, local_provers) =
+ sort_strings (available_atps thy) @ smt_prover_names
+ |> List.partition (String.isPrefix remote_prefix)
+ in
+ priority ("Available provers: " ^ commas (local_provers @ remote_provers) ^
+ ".")
+ end
+
+fun kill_provers () = Async_Manager.kill_threads das_Tool "provers"
+fun running_provers () = Async_Manager.running_threads das_Tool "provers"
+val messages = Async_Manager.thread_messages das_Tool "prover"
+
+(** problems, results, ATPs, etc. **)
type params =
{blocking: bool,
debug: bool,
verbose: bool,
overlord: bool,
- atps: string list,
+ provers: string list,
full_types: bool,
explicit_apply: bool,
relevance_thresholds: real * real,
@@ -102,25 +194,25 @@
timeout: Time.time,
expect: string}
-type problem =
+datatype axiom =
+ Unprepared of (string * locality) * thm |
+ Prepared of term * ((string * locality) * prepared_formula) option
+
+type prover_problem =
{state: Proof.state,
goal: thm,
subgoal: int,
- axioms: (term * ((string * locality) * fol_formula) option) list,
+ subgoal_count: int,
+ axioms: axiom list,
only: bool}
type prover_result =
{outcome: failure option,
message: string,
- pool: string Symtab.table,
- used_thm_names: (string * locality) list,
- atp_run_time_in_msecs: int,
- output: string,
- tstplike_proof: string,
- axiom_names: (string * locality) list vector,
- conjecture_shape: int list list}
+ used_axioms: (string * locality) list,
+ run_time_in_msecs: int option}
-type prover = params -> minimize_command -> problem -> prover_result
+type prover = params -> minimize_command -> prover_problem -> prover_result
(* configuration attributes *)
@@ -140,41 +232,67 @@
|> Exn.release
|> tap (after path)
-(* generic TPTP-based provers *)
+fun prover_description ctxt ({blocking, verbose, ...} : params) name num_axioms
+ i n goal =
+ quote name ^
+ (if verbose then
+ " with " ^ string_of_int num_axioms ^ " fact" ^ plural_s num_axioms
+ else
+ "") ^
+ " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^
+ (if blocking then
+ ""
+ else
+ "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
+
+fun proof_banner auto =
+ if auto then "Sledgehammer found a proof" else "Try this command"
+
+(* generic TPTP-based ATPs *)
+
+fun dest_Unprepared (Unprepared p) = p
+ | dest_Unprepared (Prepared _) = raise Fail "dest_Unprepared"
+fun prepared_axiom ctxt (Unprepared p) = prepare_axiom ctxt p
+ | prepared_axiom _ (Prepared p) = p
+
+fun int_option_add (SOME m) (SOME n) = SOME (m + n)
+ | int_option_add _ _ = NONE
(* Important messages are important but not so important that users want to see
them each time. *)
val important_message_keep_factor = 0.1
-fun prover_fun auto atp_name
+fun run_atp auto atp_name
{exec, required_execs, arguments, has_incomplete_mode, proof_delims,
known_failures, default_max_relevant, explicit_forall,
use_conjecture_for_hypotheses}
({debug, verbose, overlord, full_types, explicit_apply,
max_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
- minimize_command ({state, goal, subgoal, axioms, only} : problem) =
+ minimize_command
+ ({state, goal, subgoal, axioms, only, ...} : prover_problem) =
let
val ctxt = Proof.context_of state
val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
- val axioms = axioms |> not only
- ? take (the_default default_max_relevant max_relevant)
- val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
- else Config.get ctxt dest_dir
- val the_problem_prefix = Config.get ctxt problem_prefix
+ val axioms =
+ axioms |> not only ? take (the_default default_max_relevant max_relevant)
+ |> map (prepared_axiom ctxt)
+ val dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
+ else Config.get ctxt dest_dir
+ val problem_prefix = Config.get ctxt problem_prefix
val problem_file_name =
Path.basic ((if overlord then "prob_" ^ atp_name
- else the_problem_prefix ^ serial_string ())
+ else problem_prefix ^ serial_string ())
^ "_" ^ string_of_int subgoal)
val problem_path_name =
- if the_dest_dir = "" then
+ if dest_dir = "" then
File.tmp_path problem_file_name
- else if File.exists (Path.explode the_dest_dir) then
- Path.append (Path.explode the_dest_dir) problem_file_name
+ else if File.exists (Path.explode dest_dir) then
+ Path.append (Path.explode dest_dir) problem_file_name
else
- error ("No such directory: " ^ quote the_dest_dir ^ ".")
+ error ("No such directory: " ^ quote dest_dir ^ ".")
val measure_run_time = verbose orelse Config.get ctxt measure_run_time
val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
- (* write out problem file and call prover *)
+ (* write out problem file and call ATP *)
fun command_line complete timeout probfile =
let
val core = File.shell_path command ^ " " ^ arguments complete timeout ^
@@ -192,7 +310,7 @@
val digit = Scan.one Symbol.is_ascii_digit;
val num3 = as_num (digit ::: digit ::: (digit >> single));
val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
- val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;
+ val as_time = Scan.read Symbol.stopper time o explode
in (output, as_time t) end;
fun run_on probfile =
case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of
@@ -210,17 +328,17 @@
prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
else
I)
- |>> (if measure_run_time then split_time else rpair 0)
+ |>> (if measure_run_time then split_time else rpair NONE)
val (tstplike_proof, outcome) =
extract_tstplike_proof_and_outcome complete res_code
proof_delims known_failures output
in (output, msecs, tstplike_proof, outcome) end
val readable_names = debug andalso overlord
- val (problem, pool, conjecture_offset, axiom_names) =
- prepare_problem ctxt readable_names explicit_forall full_types
- explicit_apply hyp_ts concl_t axioms
+ val (atp_problem, pool, conjecture_offset, axiom_names) =
+ prepare_atp_problem ctxt readable_names explicit_forall full_types
+ explicit_apply hyp_ts concl_t axioms
val ss = tptp_strings_for_atp_problem use_conjecture_for_hypotheses
- problem
+ atp_problem
val _ = File.write_list probfile ss
val conjecture_shape =
conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
@@ -237,7 +355,8 @@
? (fn (_, msecs0, _, SOME _) =>
run true (Time.- (timeout, Timer.checkRealTimer timer))
|> (fn (output, msecs, tstplike_proof, outcome) =>
- (output, msecs0 + msecs, tstplike_proof, outcome))
+ (output, int_option_add msecs0 msecs,
+ tstplike_proof, outcome))
| result => result)
in ((pool, conjecture_shape, axiom_names), result) end
else
@@ -246,9 +365,9 @@
(* If the problem file has not been exported, remove it; otherwise, export
the proof file too. *)
fun cleanup probfile =
- if the_dest_dir = "" then try File.rm probfile else NONE
+ if dest_dir = "" then try File.rm probfile else NONE
fun export probfile (_, (output, _, _, _)) =
- if the_dest_dir = "" then
+ if dest_dir = "" then
()
else
File.write (Path.explode (Path.implode probfile ^ "_proof")) output
@@ -263,19 +382,17 @@
extract_important_message output
else
""
- val banner = if auto then "Sledgehammer found a proof"
- else "Try this command"
- val (message, used_thm_names) =
+ val (message, used_axioms) =
case outcome of
NONE =>
proof_text isar_proof
(pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
- (banner, full_types, minimize_command, tstplike_proof, axiom_names,
- goal, subgoal)
+ (proof_banner auto, full_types, minimize_command, tstplike_proof,
+ axiom_names, goal, subgoal)
|>> (fn message =>
message ^ (if verbose then
- "\nATP real CPU time: " ^ string_of_int msecs ^
- " ms."
+ "\nATP real CPU time: " ^
+ string_of_int (the msecs) ^ " ms."
else
"") ^
(if important_message <> "" then
@@ -285,40 +402,58 @@
""))
| SOME failure => (string_for_failure failure, [])
in
- {outcome = outcome, message = message, pool = pool,
- used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs,
- output = output, tstplike_proof = tstplike_proof,
- axiom_names = axiom_names, conjecture_shape = conjecture_shape}
+ {outcome = outcome, message = message, used_axioms = used_axioms,
+ run_time_in_msecs = msecs}
end
-fun get_prover_fun thy name = prover_fun false name (get_prover thy name)
+(* FIXME: dummy *)
+fun saschas_run_smt_solver remote timeout state axioms i =
+ (OS.Process.sleep (Time.fromMilliseconds 1500);
+ {outcome = NONE, used_axioms = axioms |> take 5 |> map fst,
+ run_time_in_msecs = NONE})
-fun run_prover (params as {blocking, debug, verbose, max_relevant, timeout,
- expect, ...})
- auto i n minimize_command (problem as {state, goal, axioms, ...})
- (prover as {default_max_relevant, ...}, atp_name) =
+fun run_smt_solver remote ({timeout, ...} : params) minimize_command
+ ({state, subgoal, subgoal_count, axioms, ...}
+ : prover_problem) =
let
+ val {outcome, used_axioms, run_time_in_msecs} =
+ saschas_run_smt_solver remote timeout state
+ (map_filter (try dest_Unprepared) axioms) subgoal
+ val message =
+ if outcome = NONE then
+ try_command_line (proof_banner false)
+ (apply_on_subgoal subgoal subgoal_count ^
+ command_call smtN (map fst used_axioms)) ^
+ minimize_line minimize_command (map fst used_axioms)
+ else
+ ""
+ in
+ {outcome = outcome, used_axioms = used_axioms,
+ run_time_in_msecs = run_time_in_msecs, message = message}
+ end
+
+fun get_prover thy auto name =
+ if is_smt_prover name then run_smt_solver (String.isPrefix remote_prefix)
+ else run_atp auto name (get_atp thy name)
+
+fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...})
+ auto minimize_command
+ (problem as {state, goal, subgoal, subgoal_count, axioms, ...})
+ name =
+ let
+ val thy = Proof.theory_of state
val ctxt = Proof.context_of state
val birth_time = Time.now ()
val death_time = Time.+ (birth_time, timeout)
- val max_relevant = the_default default_max_relevant max_relevant
+ val max_relevant =
+ the_default (default_max_relevant_for_prover thy name) max_relevant
val num_axioms = Int.min (length axioms, max_relevant)
val desc =
- "ATP " ^ quote atp_name ^
- (if verbose then
- " with " ^ string_of_int num_axioms ^ " fact" ^ plural_s num_axioms
- else
- "") ^
- " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^
- (if blocking then
- ""
- else
- "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
+ prover_description ctxt params name num_axioms subgoal subgoal_count goal
fun go () =
let
fun really_go () =
- prover_fun auto atp_name prover params (minimize_command atp_name)
- problem
+ get_prover thy auto name params (minimize_command name) problem
|> (fn {outcome, message, ...} =>
(if is_some outcome then "none" else "some", message))
val (outcome_code, message) =
@@ -355,51 +490,68 @@
(false, state))
end
-val auto_max_relevant_divisor = 2
-
-fun run_sledgehammer (params as {blocking, atps, full_types,
+fun run_sledgehammer (params as {blocking, provers, full_types,
relevance_thresholds, max_relevant, ...})
auto i (relevance_override as {only, ...}) minimize_command
state =
- if null atps then
- error "No ATP is set."
+ if null provers then
+ error "No prover is set."
else case subgoal_count state of
0 => (priority "No subgoal!"; (false, state))
| n =>
let
val _ = Proof.assert_backward state
val thy = Proof.theory_of state
- val _ = () |> not blocking ? kill_atps
+ val {context = ctxt, facts = chained_ths, goal} = Proof.goal state
+ val (_, hyp_ts, concl_t) = strip_subgoal goal i
+ val _ = () |> not blocking ? kill_provers
val _ = if auto then () else priority "Sledgehammering..."
- val provers = map (`(get_prover thy)) atps
- fun go () =
- let
- val {context = ctxt, facts = chained_ths, goal} = Proof.goal state
- val (_, hyp_ts, concl_t) = strip_subgoal goal i
- val max_max_relevant =
- case max_relevant of
- SOME n => n
- | NONE =>
- 0 |> fold (Integer.max o #default_max_relevant o fst) provers
- |> auto ? (fn n => n div auto_max_relevant_divisor)
- val axioms =
- relevant_facts ctxt full_types relevance_thresholds
- max_max_relevant relevance_override chained_ths
- hyp_ts concl_t
- val problem =
- {state = state, goal = goal, subgoal = i,
- axioms = map (prepare_axiom ctxt) axioms, only = only}
- val run_prover = run_prover params auto i n minimize_command problem
- in
- if auto then
- fold (fn prover => fn (true, state) => (true, state)
- | (false, _) => run_prover prover)
- provers (false, state)
- else
- (if blocking then Par_List.map else map) run_prover provers
- |> exists fst |> rpair state
- end
- in if blocking then go () else Future.fork (tap go) |> K (false, state) end
+ val (smts, atps) = provers |> List.partition is_smt_prover
+ fun run_provers full_types irrelevant_consts relevance_fudge maybe_prepare
+ provers (res as (success, state)) =
+ if success orelse null provers then
+ res
+ else
+ let
+ val max_max_relevant =
+ case max_relevant of
+ SOME n => n
+ | NONE =>
+ 0 |> fold (Integer.max o default_max_relevant_for_prover thy)
+ provers
+ |> auto ? (fn n => n div auto_max_relevant_divisor)
+ val axioms =
+ relevant_facts ctxt full_types relevance_thresholds
+ max_max_relevant irrelevant_consts relevance_fudge
+ relevance_override chained_ths hyp_ts concl_t
+ |> map maybe_prepare
+ val problem =
+ {state = state, goal = goal, subgoal = i, subgoal_count = n,
+ axioms = axioms, only = only}
+ val run_prover = run_prover params auto minimize_command
+ in
+ if auto then
+ fold (fn prover => fn (true, state) => (true, state)
+ | (false, _) => run_prover problem prover)
+ provers (false, state)
+ else
+ provers |> (if blocking then Par_List.map else map)
+ (run_prover problem)
+ |> exists fst |> rpair state
+ end
+ val run_atps =
+ run_provers full_types atp_irrelevant_consts atp_relevance_fudge
+ (Prepared o prepare_axiom ctxt) atps
+ val run_smts =
+ run_provers true smt_irrelevant_consts smt_relevance_fudge Unprepared
+ smts
+ fun run_atps_and_smt_solvers () =
+ [run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ())
+ in
+ (false, state)
+ |> (if blocking then run_atps #> not auto ? run_smts
+ else (fn p => Future.fork (tap run_atps_and_smt_solvers) |> K p))
+ end
val setup =
dest_dir_setup
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Fri Oct 22 17:15:46 2010 +0200
@@ -0,0 +1,949 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
+ Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
+ Author: Claire Quigley, Cambridge University Computer Laboratory
+ Author: Jasmin Blanchette, TU Muenchen
+
+Proof reconstruction for Sledgehammer.
+*)
+
+signature SLEDGEHAMMER_ATP_RECONSTRUCT =
+sig
+ type locality = Sledgehammer_Filter.locality
+ type minimize_command = string list -> string
+ type metis_params =
+ string * bool * minimize_command * string * (string * locality) list vector
+ * thm * int
+ type isar_params =
+ string Symtab.table * bool * int * Proof.context * int list list
+ type text_result = string * (string * locality) list
+
+ val repair_conjecture_shape_and_axiom_names :
+ string -> int list list -> (string * locality) list vector
+ -> int list list * (string * locality) list vector
+ val apply_on_subgoal : int -> int -> string
+ val command_call : string -> string list -> string
+ val try_command_line : string -> string -> string
+ val minimize_line : ('a list -> string) -> 'a list -> string
+ val metis_proof_text : metis_params -> text_result
+ val isar_proof_text : isar_params -> metis_params -> text_result
+ val proof_text : bool -> isar_params -> metis_params -> text_result
+end;
+
+structure Sledgehammer_ATP_Reconstruct : SLEDGEHAMMER_ATP_RECONSTRUCT =
+struct
+
+open ATP_Problem
+open ATP_Proof
+open Metis_Translate
+open Sledgehammer_Util
+open Sledgehammer_Filter
+open Sledgehammer_ATP_Translate
+
+type minimize_command = string list -> string
+type metis_params =
+ string * bool * minimize_command * string * (string * locality) list vector
+ * thm * int
+type isar_params =
+ string Symtab.table * bool * int * Proof.context * int list list
+type text_result = string * (string * locality) list
+
+fun is_head_digit s = Char.isDigit (String.sub (s, 0))
+val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
+
+fun find_first_in_list_vector vec key =
+ Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
+ | (_, value) => value) NONE vec
+
+
+(** SPASS's Flotter hack **)
+
+(* This is a hack required for keeping track of axioms after they have been
+ clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is also
+ part of this hack. *)
+
+val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
+
+fun extract_clause_sequence output =
+ let
+ val tokens_of = String.tokens (not o Char.isAlphaNum)
+ fun extract_num ("clause" :: (ss as _ :: _)) =
+ Int.fromString (List.last ss)
+ | extract_num _ = NONE
+ in output |> split_lines |> map_filter (extract_num o tokens_of) end
+
+val parse_clause_formula_pair =
+ $$ "(" |-- scan_integer --| $$ ","
+ -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")"
+ --| Scan.option ($$ ",")
+val parse_clause_formula_relation =
+ Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
+ |-- Scan.repeat parse_clause_formula_pair
+val extract_clause_formula_relation =
+ Substring.full #> Substring.position set_ClauseFormulaRelationN
+ #> snd #> Substring.position "." #> fst #> Substring.string
+ #> explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
+ #> fst
+
+fun repair_conjecture_shape_and_axiom_names output conjecture_shape
+ axiom_names =
+ if String.isSubstring set_ClauseFormulaRelationN output then
+ let
+ val j0 = hd (hd conjecture_shape)
+ val seq = extract_clause_sequence output
+ val name_map = extract_clause_formula_relation output
+ fun renumber_conjecture j =
+ conjecture_prefix ^ string_of_int (j - j0)
+ |> AList.find (fn (s, ss) => member (op =) ss s) name_map
+ |> map (fn s => find_index (curry (op =) s) seq + 1)
+ fun names_for_number j =
+ j |> AList.lookup (op =) name_map |> these
+ |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of
+ |> map (fn name =>
+ (name, name |> find_first_in_list_vector axiom_names
+ |> the)
+ handle Option.Option =>
+ error ("No such fact: " ^ quote name ^ "."))
+ in
+ (conjecture_shape |> map (maps renumber_conjecture),
+ seq |> map names_for_number |> Vector.fromList)
+ end
+ else
+ (conjecture_shape, axiom_names)
+
+
+(** Soft-core proof reconstruction: Metis one-liner **)
+
+fun string_for_label (s, num) = s ^ string_of_int num
+
+fun apply_on_subgoal _ 1 = "by "
+ | apply_on_subgoal 1 _ = "apply "
+ | apply_on_subgoal i _ = "prefer " ^ string_of_int i ^ " apply "
+fun command_call name [] = name
+ | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
+fun try_command_line banner command =
+ banner ^ ": " ^ Markup.markup Markup.sendback command ^ "."
+fun using_labels [] = ""
+ | using_labels ls =
+ "using " ^ space_implode " " (map string_for_label ls) ^ " "
+fun metis_name full_types = if full_types then "metisFT" else "metis"
+fun metis_call full_types ss = command_call (metis_name full_types) ss
+fun metis_command full_types i n (ls, ss) =
+ using_labels ls ^ apply_on_subgoal i n ^ metis_call full_types ss
+fun metis_line banner full_types i n ss =
+ try_command_line banner (metis_command full_types i n ([], ss))
+fun minimize_line _ [] = ""
+ | minimize_line minimize_command ss =
+ case minimize_command ss of
+ "" => ""
+ | command =>
+ "\nTo minimize the number of lemmas, try this: " ^
+ Markup.markup Markup.sendback command ^ "."
+
+fun resolve_axiom axiom_names ((_, SOME s)) =
+ (case strip_prefix_and_unascii axiom_prefix s of
+ SOME s' => (case find_first_in_list_vector axiom_names s' of
+ SOME x => [(s', x)]
+ | NONE => [])
+ | NONE => [])
+ | resolve_axiom axiom_names (num, NONE) =
+ case Int.fromString num of
+ SOME j =>
+ if j > 0 andalso j <= Vector.length axiom_names then
+ Vector.sub (axiom_names, j - 1)
+ else
+ []
+ | NONE => []
+
+fun add_fact axiom_names (Inference (name, _, [])) =
+ append (resolve_axiom axiom_names name)
+ | add_fact _ _ = I
+
+fun used_facts_in_tstplike_proof axiom_names =
+ atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact axiom_names)
+
+fun used_facts axiom_names =
+ used_facts_in_tstplike_proof axiom_names
+ #> List.partition (curry (op =) Chained o snd)
+ #> pairself (sort_distinct (string_ord o pairself fst))
+
+fun metis_proof_text (banner, full_types, minimize_command,
+ tstplike_proof, axiom_names, goal, i) =
+ let
+ val (chained_lemmas, other_lemmas) =
+ used_facts axiom_names tstplike_proof
+ val n = Logic.count_prems (prop_of goal)
+ in
+ (metis_line banner full_types i n (map fst other_lemmas) ^
+ minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)),
+ other_lemmas @ chained_lemmas)
+ end
+
+
+(** Hard-core proof reconstruction: structured Isar proofs **)
+
+(* Simple simplifications to ensure that sort annotations don't leave a trail of
+ spurious "True"s. *)
+fun s_not @{const False} = @{const True}
+ | s_not @{const True} = @{const False}
+ | s_not (@{const Not} $ t) = t
+ | s_not t = @{const Not} $ t
+fun s_conj (@{const True}, t2) = t2
+ | s_conj (t1, @{const True}) = t1
+ | s_conj p = HOLogic.mk_conj p
+fun s_disj (@{const False}, t2) = t2
+ | s_disj (t1, @{const False}) = t1
+ | s_disj p = HOLogic.mk_disj p
+fun s_imp (@{const True}, t2) = t2
+ | s_imp (t1, @{const False}) = s_not t1
+ | s_imp p = HOLogic.mk_imp p
+fun s_iff (@{const True}, t2) = t2
+ | s_iff (t1, @{const True}) = t1
+ | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
+
+fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t
+fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t
+
+fun negate_term (Const (@{const_name All}, T) $ Abs (s, T', t')) =
+ Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t')
+ | negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
+ Const (@{const_name All}, T) $ Abs (s, T', negate_term t')
+ | negate_term (@{const HOL.implies} $ t1 $ t2) =
+ @{const HOL.conj} $ t1 $ negate_term t2
+ | negate_term (@{const HOL.conj} $ t1 $ t2) =
+ @{const HOL.disj} $ negate_term t1 $ negate_term t2
+ | negate_term (@{const HOL.disj} $ t1 $ t2) =
+ @{const HOL.conj} $ negate_term t1 $ negate_term t2
+ | negate_term (@{const Not} $ t) = t
+ | negate_term t = @{const Not} $ t
+
+val indent_size = 2
+val no_label = ("", ~1)
+
+val raw_prefix = "X"
+val assum_prefix = "A"
+val fact_prefix = "F"
+
+fun resolve_conjecture conjecture_shape (num, s_opt) =
+ let
+ val k = case try (unprefix conjecture_prefix) (the_default "" s_opt) of
+ SOME s => Int.fromString s |> the_default ~1
+ | NONE => case Int.fromString num of
+ SOME j => find_index (exists (curry (op =) j))
+ conjecture_shape
+ | NONE => ~1
+ in if k >= 0 then [k] else [] end
+
+fun is_axiom conjecture_shape = not o null o resolve_axiom conjecture_shape
+fun is_conjecture conjecture_shape = not o null o resolve_conjecture conjecture_shape
+
+fun raw_label_for_name conjecture_shape name =
+ case resolve_conjecture conjecture_shape name of
+ [j] => (conjecture_prefix, j)
+ | _ => case Int.fromString (fst name) of
+ SOME j => (raw_prefix, j)
+ | NONE => (raw_prefix ^ fst name, 0)
+
+(**** INTERPRETATION OF TSTP SYNTAX TREES ****)
+
+exception FO_TERM of string fo_term list
+exception FORMULA of (string, string fo_term) formula list
+exception SAME of unit
+
+(* Type variables are given the basic sort "HOL.type". Some will later be
+ constrained by information from type literals, or by type inference. *)
+fun type_from_fo_term tfrees (u as ATerm (a, us)) =
+ let val Ts = map (type_from_fo_term tfrees) us in
+ case strip_prefix_and_unascii type_const_prefix a of
+ SOME b => Type (invert_const b, Ts)
+ | NONE =>
+ if not (null us) then
+ raise FO_TERM [u] (* only "tconst"s have type arguments *)
+ else case strip_prefix_and_unascii tfree_prefix a of
+ SOME b =>
+ let val s = "'" ^ b in
+ TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
+ end
+ | NONE =>
+ case strip_prefix_and_unascii tvar_prefix a of
+ SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
+ | NONE =>
+ (* Variable from the ATP, say "X1" *)
+ Type_Infer.param 0 (a, HOLogic.typeS)
+ end
+
+(* Type class literal applied to a type. Returns triple of polarity, class,
+ type. *)
+fun type_constraint_from_term pos tfrees (u as ATerm (a, us)) =
+ case (strip_prefix_and_unascii class_prefix a,
+ map (type_from_fo_term tfrees) us) of
+ (SOME b, [T]) => (pos, b, T)
+ | _ => raise FO_TERM [u]
+
+(** Accumulate type constraints in a formula: negative type literals **)
+fun add_var (key, z) = Vartab.map_default (key, []) (cons z)
+fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl)
+ | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl)
+ | add_type_constraint _ = I
+
+fun repair_atp_variable_name f s =
+ let
+ fun subscript_name s n = s ^ nat_subscript n
+ val s = String.map f s
+ in
+ case space_explode "_" s of
+ [_] => (case take_suffix Char.isDigit (String.explode s) of
+ (cs1 as _ :: _, cs2 as _ :: _) =>
+ subscript_name (String.implode cs1)
+ (the (Int.fromString (String.implode cs2)))
+ | (_, _) => s)
+ | [s1, s2] => (case Int.fromString s2 of
+ SOME n => subscript_name s1 n
+ | NONE => s)
+ | _ => s
+ end
+
+(* First-order translation. No types are known for variables. "HOLogic.typeT"
+ should allow them to be inferred. *)
+fun raw_term_from_pred thy full_types tfrees =
+ let
+ fun aux opt_T extra_us u =
+ case u of
+ ATerm ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1
+ | ATerm ("hAPP", [u1, u2]) => aux opt_T (u2 :: extra_us) u1
+ | ATerm (a, us) =>
+ if a = type_wrapper_name then
+ case us of
+ [typ_u, term_u] =>
+ aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
+ | _ => raise FO_TERM us
+ else case strip_prefix_and_unascii const_prefix a of
+ SOME "equal" =>
+ let val ts = map (aux NONE []) us in
+ if length ts = 2 andalso hd ts aconv List.last ts then
+ (* Vampire is keen on producing these. *)
+ @{const True}
+ else
+ list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
+ end
+ | SOME b =>
+ let
+ val c = invert_const b
+ val num_type_args = num_type_args thy c
+ val (type_us, term_us) =
+ chop (if full_types then 0 else num_type_args) us
+ (* Extra args from "hAPP" come after any arguments given directly to
+ the constant. *)
+ val term_ts = map (aux NONE []) term_us
+ val extra_ts = map (aux NONE []) extra_us
+ val t =
+ Const (c, if full_types then
+ case opt_T of
+ SOME T => map fastype_of term_ts ---> T
+ | NONE =>
+ if num_type_args = 0 then
+ Sign.const_instance thy (c, [])
+ else
+ raise Fail ("no type information for " ^ quote c)
+ else
+ Sign.const_instance thy (c,
+ map (type_from_fo_term tfrees) type_us))
+ in list_comb (t, term_ts @ extra_ts) end
+ | NONE => (* a free or schematic variable *)
+ let
+ val ts = map (aux NONE []) (us @ extra_us)
+ val T = map fastype_of ts ---> HOLogic.typeT
+ val t =
+ case strip_prefix_and_unascii fixed_var_prefix a of
+ SOME b => Free (b, T)
+ | NONE =>
+ case strip_prefix_and_unascii schematic_var_prefix a of
+ SOME b => Var ((b, 0), T)
+ | NONE =>
+ if is_atp_variable a then
+ Var ((repair_atp_variable_name Char.toLower a, 0), T)
+ else
+ (* Skolem constants? *)
+ Var ((repair_atp_variable_name Char.toUpper a, 0), T)
+ in list_comb (t, ts) end
+ in aux (SOME HOLogic.boolT) [] end
+
+fun term_from_pred thy full_types tfrees pos (u as ATerm (s, _)) =
+ if String.isPrefix class_prefix s then
+ add_type_constraint (type_constraint_from_term pos tfrees u)
+ #> pair @{const True}
+ else
+ pair (raw_term_from_pred thy full_types tfrees u)
+
+val combinator_table =
+ [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}),
+ (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def_raw}),
+ (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def_raw}),
+ (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}),
+ (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def_raw})]
+
+fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2))
+ | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t')
+ | uncombine_term (t as Const (x as (s, _))) =
+ (case AList.lookup (op =) combinator_table s of
+ SOME thm => thm |> prop_of |> specialize_type @{theory} x |> Logic.dest_equals |> snd
+ | NONE => t)
+ | uncombine_term t = t
+
+(* Update schematic type variables with detected sort constraints. It's not
+ totally clear when this code is necessary. *)
+fun repair_tvar_sorts (t, tvar_tab) =
+ let
+ fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
+ | do_type (TVar (xi, s)) =
+ TVar (xi, the_default s (Vartab.lookup tvar_tab xi))
+ | do_type (TFree z) = TFree z
+ fun do_term (Const (a, T)) = Const (a, do_type T)
+ | do_term (Free (a, T)) = Free (a, do_type T)
+ | do_term (Var (xi, T)) = Var (xi, do_type T)
+ | do_term (t as Bound _) = t
+ | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t)
+ | do_term (t1 $ t2) = do_term t1 $ do_term t2
+ in t |> not (Vartab.is_empty tvar_tab) ? do_term end
+
+fun quantify_over_var quant_of var_s t =
+ let
+ val vars = [] |> Term.add_vars t |> filter (fn ((s, _), _) => s = var_s)
+ |> map Var
+ in fold_rev quant_of vars t end
+
+(* Interpret an ATP formula as a HOL term, extracting sort constraints as they
+ appear in the formula. *)
+fun prop_from_formula thy full_types tfrees phi =
+ let
+ fun do_formula pos phi =
+ case phi of
+ AQuant (_, [], phi) => do_formula pos phi
+ | AQuant (q, x :: xs, phi') =>
+ do_formula pos (AQuant (q, xs, phi'))
+ #>> quantify_over_var (case q of
+ AForall => forall_of
+ | AExists => exists_of)
+ (repair_atp_variable_name Char.toLower x)
+ | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
+ | AConn (c, [phi1, phi2]) =>
+ do_formula (pos |> c = AImplies ? not) phi1
+ ##>> do_formula pos phi2
+ #>> (case c of
+ AAnd => s_conj
+ | AOr => s_disj
+ | AImplies => s_imp
+ | AIf => s_imp o swap
+ | AIff => s_iff
+ | ANotIff => s_not o s_iff
+ | _ => raise Fail "unexpected connective")
+ | AAtom tm => term_from_pred thy full_types tfrees pos tm
+ | _ => raise FORMULA [phi]
+ in repair_tvar_sorts (do_formula true phi Vartab.empty) end
+
+fun check_formula ctxt =
+ Type.constraint HOLogic.boolT
+ #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
+
+
+(**** Translation of TSTP files to Isar Proofs ****)
+
+fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
+ | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
+
+fun decode_line full_types tfrees (Definition (name, phi1, phi2)) ctxt =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val t1 = prop_from_formula thy full_types tfrees phi1
+ val vars = snd (strip_comb t1)
+ val frees = map unvarify_term vars
+ val unvarify_args = subst_atomic (vars ~~ frees)
+ val t2 = prop_from_formula thy full_types tfrees phi2
+ val (t1, t2) =
+ HOLogic.eq_const HOLogic.typeT $ t1 $ t2
+ |> unvarify_args |> uncombine_term |> check_formula ctxt
+ |> HOLogic.dest_eq
+ in
+ (Definition (name, t1, t2),
+ fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
+ end
+ | decode_line full_types tfrees (Inference (name, u, deps)) ctxt =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val t = u |> prop_from_formula thy full_types tfrees
+ |> uncombine_term |> check_formula ctxt
+ in
+ (Inference (name, t, deps),
+ fold Variable.declare_term (OldTerm.term_frees t) ctxt)
+ end
+fun decode_lines ctxt full_types tfrees lines =
+ fst (fold_map (decode_line full_types tfrees) lines ctxt)
+
+fun is_same_inference _ (Definition _) = false
+ | is_same_inference t (Inference (_, t', _)) = t aconv t'
+
+(* No "real" literals means only type information (tfree_tcs, clsrel, or
+ clsarity). *)
+val is_only_type_information = curry (op aconv) HOLogic.true_const
+
+fun replace_one_dependency (old, new) dep =
+ if is_same_step (dep, old) then new else [dep]
+fun replace_dependencies_in_line _ (line as Definition _) = line
+ | replace_dependencies_in_line p (Inference (name, t, deps)) =
+ Inference (name, t, fold (union (op =) o replace_one_dependency p) deps [])
+
+(* Discard axioms; consolidate adjacent lines that prove the same formula, since
+ they differ only in type information.*)
+fun add_line _ _ (line as Definition _) lines = line :: lines
+ | add_line conjecture_shape axiom_names (Inference (name, t, [])) lines =
+ (* No dependencies: axiom, conjecture, or (for Vampire) internal axioms or
+ definitions. *)
+ if is_axiom axiom_names name then
+ (* Axioms are not proof lines. *)
+ if is_only_type_information t then
+ map (replace_dependencies_in_line (name, [])) lines
+ (* Is there a repetition? If so, replace later line by earlier one. *)
+ else case take_prefix (not o is_same_inference t) lines of
+ (_, []) => lines (* no repetition of proof line *)
+ | (pre, Inference (name', _, _) :: post) =>
+ pre @ map (replace_dependencies_in_line (name', [name])) post
+ | _ => raise Fail "unexpected inference"
+ else if is_conjecture conjecture_shape name then
+ Inference (name, negate_term t, []) :: lines
+ else
+ map (replace_dependencies_in_line (name, [])) lines
+ | add_line _ _ (Inference (name, t, deps)) lines =
+ (* Type information will be deleted later; skip repetition test. *)
+ if is_only_type_information t then
+ Inference (name, t, deps) :: lines
+ (* Is there a repetition? If so, replace later line by earlier one. *)
+ else case take_prefix (not o is_same_inference t) lines of
+ (* FIXME: Doesn't this code risk conflating proofs involving different
+ types? *)
+ (_, []) => Inference (name, t, deps) :: lines
+ | (pre, Inference (name', t', _) :: post) =>
+ Inference (name, t', deps) ::
+ pre @ map (replace_dependencies_in_line (name', [name])) post
+ | _ => raise Fail "unexpected inference"
+
+(* Recursively delete empty lines (type information) from the proof. *)
+fun add_nontrivial_line (Inference (name, t, [])) lines =
+ if is_only_type_information t then delete_dependency name lines
+ else Inference (name, t, []) :: lines
+ | add_nontrivial_line line lines = line :: lines
+and delete_dependency name lines =
+ fold_rev add_nontrivial_line
+ (map (replace_dependencies_in_line (name, [])) lines) []
+
+(* ATPs sometimes reuse free variable names in the strangest ways. Removing
+ offending lines often does the trick. *)
+fun is_bad_free frees (Free x) = not (member (op =) frees x)
+ | is_bad_free _ _ = false
+
+fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) =
+ (j, line :: map (replace_dependencies_in_line (name, [])) lines)
+ | add_desired_line isar_shrink_factor conjecture_shape axiom_names frees
+ (Inference (name, t, deps)) (j, lines) =
+ (j + 1,
+ if is_axiom axiom_names name orelse
+ is_conjecture conjecture_shape name orelse
+ (* the last line must be kept *)
+ j = 0 orelse
+ (not (is_only_type_information t) andalso
+ null (Term.add_tvars t []) andalso
+ not (exists_subterm (is_bad_free frees) t) andalso
+ length deps >= 2 andalso j mod isar_shrink_factor = 0 andalso
+ (* kill next to last line, which usually results in a trivial step *)
+ j <> 1) then
+ Inference (name, t, deps) :: lines (* keep line *)
+ else
+ map (replace_dependencies_in_line (name, deps)) lines) (* drop line *)
+
+(** Isar proof construction and manipulation **)
+
+fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
+ (union (op =) ls1 ls2, union (op =) ss1 ss2)
+
+type label = string * int
+type facts = label list * string list
+
+datatype isar_qualifier = Show | Then | Moreover | Ultimately
+
+datatype isar_step =
+ Fix of (string * typ) list |
+ Let of term * term |
+ Assume of label * term |
+ Have of isar_qualifier list * label * term * byline
+and byline =
+ ByMetis of facts |
+ CaseSplit of isar_step list list * facts
+
+fun smart_case_split [] facts = ByMetis facts
+ | smart_case_split proofs facts = CaseSplit (proofs, facts)
+
+fun add_fact_from_dependency conjecture_shape axiom_names name =
+ if is_axiom axiom_names name then
+ apsnd (union (op =) (map fst (resolve_axiom axiom_names name)))
+ else
+ apfst (insert (op =) (raw_label_for_name conjecture_shape name))
+
+fun step_for_line _ _ _ (Definition (_, t1, t2)) = Let (t1, t2)
+ | step_for_line conjecture_shape _ _ (Inference (name, t, [])) =
+ Assume (raw_label_for_name conjecture_shape name, t)
+ | step_for_line conjecture_shape axiom_names j (Inference (name, t, deps)) =
+ Have (if j = 1 then [Show] else [],
+ raw_label_for_name conjecture_shape name,
+ fold_rev forall_of (map Var (Term.add_vars t [])) t,
+ ByMetis (fold (add_fact_from_dependency conjecture_shape axiom_names)
+ deps ([], [])))
+
+fun repair_name "$true" = "c_True"
+ | repair_name "$false" = "c_False"
+ | repair_name "$$e" = "c_equal" (* seen in Vampire proofs *)
+ | repair_name "equal" = "c_equal" (* needed by SPASS? *)
+ | repair_name s =
+ if String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s then
+ "c_equal" (* seen in Vampire proofs *)
+ else
+ s
+
+fun isar_proof_from_tstplike_proof pool ctxt full_types tfrees isar_shrink_factor
+ tstplike_proof conjecture_shape axiom_names params frees =
+ let
+ val lines =
+ tstplike_proof
+ |> atp_proof_from_tstplike_string
+ |> nasty_atp_proof pool
+ |> map_term_names_in_atp_proof repair_name
+ |> decode_lines ctxt full_types tfrees
+ |> rpair [] |-> fold_rev (add_line conjecture_shape axiom_names)
+ |> rpair [] |-> fold_rev add_nontrivial_line
+ |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor
+ conjecture_shape axiom_names frees)
+ |> snd
+ in
+ (if null params then [] else [Fix params]) @
+ map2 (step_for_line conjecture_shape axiom_names) (length lines downto 1)
+ lines
+ end
+
+(* When redirecting proofs, we keep information about the labels seen so far in
+ the "backpatches" data structure. The first component indicates which facts
+ should be associated with forthcoming proof steps. The second component is a
+ pair ("assum_ls", "drop_ls"), where "assum_ls" are the labels that should
+ become assumptions and "drop_ls" are the labels that should be dropped in a
+ case split. *)
+type backpatches = (label * facts) list * (label list * label list)
+
+fun used_labels_of_step (Have (_, _, _, by)) =
+ (case by of
+ ByMetis (ls, _) => ls
+ | CaseSplit (proofs, (ls, _)) =>
+ fold (union (op =) o used_labels_of) proofs ls)
+ | used_labels_of_step _ = []
+and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []
+
+fun new_labels_of_step (Fix _) = []
+ | new_labels_of_step (Let _) = []
+ | new_labels_of_step (Assume (l, _)) = [l]
+ | new_labels_of_step (Have (_, l, _, _)) = [l]
+val new_labels_of = maps new_labels_of_step
+
+val join_proofs =
+ let
+ fun aux _ [] = NONE
+ | aux proof_tail (proofs as (proof1 :: _)) =
+ if exists null proofs then
+ NONE
+ else if forall (curry (op =) (hd proof1) o hd) (tl proofs) then
+ aux (hd proof1 :: proof_tail) (map tl proofs)
+ else case hd proof1 of
+ Have ([], l, t, _) => (* FIXME: should we really ignore the "by"? *)
+ if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t')
+ | _ => false) (tl proofs) andalso
+ not (exists (member (op =) (maps new_labels_of proofs))
+ (used_labels_of proof_tail)) then
+ SOME (l, t, map rev proofs, proof_tail)
+ else
+ NONE
+ | _ => NONE
+ in aux [] o map rev end
+
+fun case_split_qualifiers proofs =
+ case length proofs of
+ 0 => []
+ | 1 => [Then]
+ | _ => [Ultimately]
+
+fun redirect_proof hyp_ts concl_t proof =
+ let
+ (* The first pass outputs those steps that are independent of the negated
+ conjecture. The second pass flips the proof by contradiction to obtain a
+ direct proof, introducing case splits when an inference depends on
+ several facts that depend on the negated conjecture. *)
+ val concl_l = (conjecture_prefix, length hyp_ts)
+ fun first_pass ([], contra) = ([], contra)
+ | first_pass ((step as Fix _) :: proof, contra) =
+ first_pass (proof, contra) |>> cons step
+ | first_pass ((step as Let _) :: proof, contra) =
+ first_pass (proof, contra) |>> cons step
+ | first_pass ((step as Assume (l as (_, j), _)) :: proof, contra) =
+ if l = concl_l then first_pass (proof, contra ||> cons step)
+ else first_pass (proof, contra) |>> cons (Assume (l, nth hyp_ts j))
+ | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
+ let val step = Have (qs, l, t, ByMetis (ls, ss)) in
+ if exists (member (op =) (fst contra)) ls then
+ first_pass (proof, contra |>> cons l ||> cons step)
+ else
+ first_pass (proof, contra) |>> cons step
+ end
+ | first_pass _ = raise Fail "malformed proof"
+ val (proof_top, (contra_ls, contra_proof)) =
+ first_pass (proof, ([concl_l], []))
+ val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst
+ fun backpatch_labels patches ls =
+ fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
+ fun second_pass end_qs ([], assums, patches) =
+ ([Have (end_qs, no_label, concl_t,
+ ByMetis (backpatch_labels patches (map snd assums)))], patches)
+ | second_pass end_qs (Assume (l, t) :: proof, assums, patches) =
+ second_pass end_qs (proof, (t, l) :: assums, patches)
+ | second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums,
+ patches) =
+ (if member (op =) (snd (snd patches)) l andalso
+ not (member (op =) (fst (snd patches)) l) andalso
+ not (AList.defined (op =) (fst patches) l) then
+ second_pass end_qs (proof, assums, patches ||> apsnd (append ls))
+ else case List.partition (member (op =) contra_ls) ls of
+ ([contra_l], co_ls) =>
+ if member (op =) qs Show then
+ second_pass end_qs (proof, assums,
+ patches |>> cons (contra_l, (co_ls, ss)))
+ else
+ second_pass end_qs
+ (proof, assums,
+ patches |>> cons (contra_l, (l :: co_ls, ss)))
+ |>> cons (if member (op =) (fst (snd patches)) l then
+ Assume (l, negate_term t)
+ else
+ Have (qs, l, negate_term t,
+ ByMetis (backpatch_label patches l)))
+ | (contra_ls as _ :: _, co_ls) =>
+ let
+ val proofs =
+ map_filter
+ (fn l =>
+ if l = concl_l then
+ NONE
+ else
+ let
+ val drop_ls = filter (curry (op <>) l) contra_ls
+ in
+ second_pass []
+ (proof, assums,
+ patches ||> apfst (insert (op =) l)
+ ||> apsnd (union (op =) drop_ls))
+ |> fst |> SOME
+ end) contra_ls
+ val (assumes, facts) =
+ if member (op =) (fst (snd patches)) l then
+ ([Assume (l, negate_term t)], (l :: co_ls, ss))
+ else
+ ([], (co_ls, ss))
+ in
+ (case join_proofs proofs of
+ SOME (l, t, proofs, proof_tail) =>
+ Have (case_split_qualifiers proofs @
+ (if null proof_tail then end_qs else []), l, t,
+ smart_case_split proofs facts) :: proof_tail
+ | NONE =>
+ [Have (case_split_qualifiers proofs @ end_qs, no_label,
+ concl_t, smart_case_split proofs facts)],
+ patches)
+ |>> append assumes
+ end
+ | _ => raise Fail "malformed proof")
+ | second_pass _ _ = raise Fail "malformed proof"
+ val proof_bottom =
+ second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst
+ in proof_top @ proof_bottom end
+
+(* FIXME: Still needed? Probably not. *)
+val kill_duplicate_assumptions_in_proof =
+ let
+ fun relabel_facts subst =
+ apfst (map (fn l => AList.lookup (op =) subst l |> the_default l))
+ fun do_step (step as Assume (l, t)) (proof, subst, assums) =
+ (case AList.lookup (op aconv) assums t of
+ SOME l' => (proof, (l, l') :: subst, assums)
+ | NONE => (step :: proof, subst, (t, l) :: assums))
+ | do_step (Have (qs, l, t, by)) (proof, subst, assums) =
+ (Have (qs, l, t,
+ case by of
+ ByMetis facts => ByMetis (relabel_facts subst facts)
+ | CaseSplit (proofs, facts) =>
+ CaseSplit (map do_proof proofs, relabel_facts subst facts)) ::
+ proof, subst, assums)
+ | do_step step (proof, subst, assums) = (step :: proof, subst, assums)
+ and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
+ in do_proof end
+
+val then_chain_proof =
+ let
+ fun aux _ [] = []
+ | aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof
+ | aux l' (Have (qs, l, t, by) :: proof) =
+ (case by of
+ ByMetis (ls, ss) =>
+ Have (if member (op =) ls l' then
+ (Then :: qs, l, t,
+ ByMetis (filter_out (curry (op =) l') ls, ss))
+ else
+ (qs, l, t, ByMetis (ls, ss)))
+ | CaseSplit (proofs, facts) =>
+ Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) ::
+ aux l proof
+ | aux _ (step :: proof) = step :: aux no_label proof
+ in aux no_label end
+
+fun kill_useless_labels_in_proof proof =
+ let
+ val used_ls = used_labels_of proof
+ fun do_label l = if member (op =) used_ls l then l else no_label
+ fun do_step (Assume (l, t)) = Assume (do_label l, t)
+ | do_step (Have (qs, l, t, by)) =
+ Have (qs, do_label l, t,
+ case by of
+ CaseSplit (proofs, facts) =>
+ CaseSplit (map (map do_step) proofs, facts)
+ | _ => by)
+ | do_step step = step
+ in map do_step proof end
+
+fun prefix_for_depth n = replicate_string (n + 1)
+
+val relabel_proof =
+ let
+ fun aux _ _ _ [] = []
+ | aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) =
+ if l = no_label then
+ Assume (l, t) :: aux subst depth (next_assum, next_fact) proof
+ else
+ let val l' = (prefix_for_depth depth assum_prefix, next_assum) in
+ Assume (l', t) ::
+ aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof
+ end
+ | aux subst depth (next_assum, next_fact) (Have (qs, l, t, by) :: proof) =
+ let
+ val (l', subst, next_fact) =
+ if l = no_label then
+ (l, subst, next_fact)
+ else
+ let
+ val l' = (prefix_for_depth depth fact_prefix, next_fact)
+ in (l', (l, l') :: subst, next_fact + 1) end
+ val relabel_facts =
+ apfst (maps (the_list o AList.lookup (op =) subst))
+ val by =
+ case by of
+ ByMetis facts => ByMetis (relabel_facts facts)
+ | CaseSplit (proofs, facts) =>
+ CaseSplit (map (aux subst (depth + 1) (1, 1)) proofs,
+ relabel_facts facts)
+ in
+ Have (qs, l', t, by) ::
+ aux subst depth (next_assum, next_fact) proof
+ end
+ | aux subst depth nextp (step :: proof) =
+ step :: aux subst depth nextp proof
+ in aux [] 0 (1, 1) end
+
+fun string_for_proof ctxt0 full_types i n =
+ let
+ val ctxt = ctxt0
+ |> Config.put show_free_types false
+ |> Config.put show_types true
+ fun fix_print_mode f x =
+ Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
+ (print_mode_value ())) f x
+ fun do_indent ind = replicate_string (ind * indent_size) " "
+ fun do_free (s, T) =
+ maybe_quote s ^ " :: " ^
+ maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
+ fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
+ fun do_have qs =
+ (if member (op =) qs Moreover then "moreover " else "") ^
+ (if member (op =) qs Ultimately then "ultimately " else "") ^
+ (if member (op =) qs Then then
+ if member (op =) qs Show then "thus" else "hence"
+ else
+ if member (op =) qs Show then "show" else "have")
+ val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
+ fun do_facts (ls, ss) =
+ metis_command full_types 1 1
+ (ls |> sort_distinct (prod_ord string_ord int_ord),
+ ss |> sort_distinct string_ord)
+ and do_step ind (Fix xs) =
+ do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
+ | do_step ind (Let (t1, t2)) =
+ do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
+ | do_step ind (Assume (l, t)) =
+ do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
+ | do_step ind (Have (qs, l, t, ByMetis facts)) =
+ do_indent ind ^ do_have qs ^ " " ^
+ do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n"
+ | do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) =
+ space_implode (do_indent ind ^ "moreover\n")
+ (map (do_block ind) proofs) ^
+ do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^
+ do_facts facts ^ "\n"
+ and do_steps prefix suffix ind steps =
+ let val s = implode (map (do_step ind) steps) in
+ replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
+ String.extract (s, ind * indent_size,
+ SOME (size s - ind * indent_size - 1)) ^
+ suffix ^ "\n"
+ end
+ and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
+ (* One-step proofs are pointless; better use the Metis one-liner
+ directly. *)
+ and do_proof [Have (_, _, _, ByMetis _)] = ""
+ | do_proof proof =
+ (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
+ do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^
+ (if n <> 1 then "next" else "qed")
+ in do_proof end
+
+fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
+ (other_params as (_, full_types, _, tstplike_proof,
+ axiom_names, goal, i)) =
+ let
+ val (params, hyp_ts, concl_t) = strip_subgoal goal i
+ val frees = fold Term.add_frees (concl_t :: hyp_ts) []
+ val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
+ val n = Logic.count_prems (prop_of goal)
+ val (one_line_proof, lemma_names) = metis_proof_text other_params
+ fun isar_proof_for () =
+ case isar_proof_from_tstplike_proof pool ctxt full_types tfrees
+ isar_shrink_factor tstplike_proof conjecture_shape axiom_names
+ params frees
+ |> redirect_proof hyp_ts concl_t
+ |> kill_duplicate_assumptions_in_proof
+ |> then_chain_proof
+ |> kill_useless_labels_in_proof
+ |> relabel_proof
+ |> string_for_proof ctxt full_types i n of
+ "" => "\nNo structured proof available."
+ | proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
+ val isar_proof =
+ if debug then
+ isar_proof_for ()
+ else
+ try isar_proof_for ()
+ |> the_default "\nWarning: The Isar proof construction failed."
+ in (one_line_proof ^ isar_proof, lemma_names) end
+
+fun proof_text isar_proof isar_params other_params =
+ (if isar_proof then isar_proof_text isar_params else metis_proof_text)
+ other_params
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Fri Oct 22 17:15:46 2010 +0200
@@ -0,0 +1,534 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_translate.ML
+ Author: Fabian Immler, TU Muenchen
+ Author: Makarius
+ Author: Jasmin Blanchette, TU Muenchen
+
+Translation of HOL to FOL for Sledgehammer.
+*)
+
+signature SLEDGEHAMMER_ATP_TRANSLATE =
+sig
+ type 'a problem = 'a ATP_Problem.problem
+ type prepared_formula
+
+ val axiom_prefix : string
+ val conjecture_prefix : string
+ val prepare_axiom :
+ Proof.context -> (string * 'a) * thm
+ -> term * ((string * 'a) * prepared_formula) option
+ val prepare_atp_problem :
+ Proof.context -> bool -> bool -> bool -> bool -> term list -> term
+ -> (term * ((string * 'a) * prepared_formula) option) list
+ -> string problem * string Symtab.table * int * (string * 'a) list vector
+end;
+
+structure Sledgehammer_ATP_Translate : SLEDGEHAMMER_ATP_TRANSLATE =
+struct
+
+open ATP_Problem
+open Metis_Translate
+open Sledgehammer_Util
+
+val axiom_prefix = "ax_"
+val conjecture_prefix = "conj_"
+val helper_prefix = "help_"
+val class_rel_clause_prefix = "clrel_";
+val arity_clause_prefix = "arity_"
+val tfree_prefix = "tfree_"
+
+(* Freshness almost guaranteed! *)
+val sledgehammer_weak_prefix = "Sledgehammer:"
+
+type prepared_formula =
+ {name: string,
+ kind: kind,
+ combformula: (name, combterm) formula,
+ ctypes_sorts: typ list}
+
+fun mk_anot phi = AConn (ANot, [phi])
+fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
+fun mk_ahorn [] phi = phi
+ | mk_ahorn (phi :: phis) psi =
+ AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
+
+fun combformula_for_prop thy =
+ let
+ val do_term = combterm_from_term thy ~1
+ fun do_quant bs q s T t' =
+ let val s = Name.variant (map fst bs) s in
+ do_formula ((s, T) :: bs) t'
+ #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
+ end
+ and do_conn bs c t1 t2 =
+ do_formula bs t1 ##>> do_formula bs t2
+ #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))
+ and do_formula bs t =
+ case t of
+ @{const Not} $ t1 =>
+ do_formula bs t1 #>> (fn phi => AConn (ANot, [phi]))
+ | Const (@{const_name All}, _) $ Abs (s, T, t') =>
+ do_quant bs AForall s T t'
+ | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
+ do_quant bs AExists s T t'
+ | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
+ | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
+ | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
+ | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
+ do_conn bs AIff t1 t2
+ | _ => (fn ts => do_term bs (Envir.eta_contract t)
+ |>> AAtom ||> union (op =) ts)
+ in do_formula [] end
+
+val presimplify_term = prop_of o Meson.presimplify oo Skip_Proof.make_thm
+
+fun concealed_bound_name j = sledgehammer_weak_prefix ^ Int.toString j
+fun conceal_bounds Ts t =
+ subst_bounds (map (Free o apfst concealed_bound_name)
+ (0 upto length Ts - 1 ~~ Ts), t)
+fun reveal_bounds Ts =
+ subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
+ (0 upto length Ts - 1 ~~ Ts))
+
+(* Removes the lambdas from an equation of the form "t = (%x. u)".
+ (Cf. "extensionalize_theorem" in "Meson_Clausify".) *)
+fun extensionalize_term t =
+ let
+ fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t'
+ | aux j (t as Const (s, Type (_, [Type (_, [_, T']),
+ Type (_, [_, res_T])]))
+ $ t2 $ Abs (var_s, var_T, t')) =
+ if s = @{const_name HOL.eq} orelse s = @{const_name "=="} then
+ let val var_t = Var ((var_s, j), var_T) in
+ Const (s, T' --> T' --> res_T)
+ $ betapply (t2, var_t) $ subst_bound (var_t, t')
+ |> aux (j + 1)
+ end
+ else
+ t
+ | aux _ t = t
+ in aux (maxidx_of_term t + 1) t end
+
+fun introduce_combinators_in_term ctxt kind t =
+ let val thy = ProofContext.theory_of ctxt in
+ if Meson.is_fol_term thy t then
+ t
+ else
+ let
+ fun aux Ts t =
+ case t of
+ @{const Not} $ t1 => @{const Not} $ aux Ts t1
+ | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
+ t0 $ Abs (s, T, aux (T :: Ts) t')
+ | (t0 as Const (@{const_name All}, _)) $ t1 =>
+ aux Ts (t0 $ eta_expand Ts t1 1)
+ | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
+ t0 $ Abs (s, T, aux (T :: Ts) t')
+ | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
+ aux Ts (t0 $ eta_expand Ts t1 1)
+ | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
+ | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
+ $ t1 $ t2 =>
+ t0 $ aux Ts t1 $ aux Ts t2
+ | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
+ t
+ else
+ t |> conceal_bounds Ts
+ |> Envir.eta_contract
+ |> cterm_of thy
+ |> Meson_Clausify.introduce_combinators_in_cterm
+ |> prop_of |> Logic.dest_equals |> snd
+ |> reveal_bounds Ts
+ val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
+ in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
+ handle THM _ =>
+ (* A type variable of sort "{}" will make abstraction fail. *)
+ if kind = Conjecture then HOLogic.false_const
+ else HOLogic.true_const
+ end
+
+(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
+ same in Sledgehammer to prevent the discovery of unreplable proofs. *)
+fun freeze_term t =
+ let
+ fun aux (t $ u) = aux t $ aux u
+ | aux (Abs (s, T, t)) = Abs (s, T, aux t)
+ | aux (Var ((s, i), T)) =
+ Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
+ | aux t = t
+ in t |> exists_subterm is_Var t ? aux end
+
+(* "Object_Logic.atomize_term" isn't as powerful as it could be; for example,
+ it leaves metaequalities over "prop"s alone. *)
+val atomize_term =
+ let
+ fun aux (@{const Trueprop} $ t1) = t1
+ | aux (Const (@{const_name all}, _) $ Abs (s, T, t')) =
+ HOLogic.all_const T $ Abs (s, T, aux t')
+ | aux (@{const "==>"} $ t1 $ t2) = HOLogic.mk_imp (pairself aux (t1, t2))
+ | aux (Const (@{const_name "=="}, Type (_, [@{typ prop}, _])) $ t1 $ t2) =
+ HOLogic.eq_const HOLogic.boolT $ aux t1 $ aux t2
+ | aux (Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2) =
+ HOLogic.eq_const T $ t1 $ t2
+ | aux _ = raise Fail "aux"
+ in perhaps (try aux) end
+
+(* making axiom and conjecture formulas *)
+fun make_formula ctxt presimp name kind t =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val t = t |> Envir.beta_eta_contract
+ |> transform_elim_term
+ |> atomize_term
+ val need_trueprop = (fastype_of t = HOLogic.boolT)
+ val t = t |> need_trueprop ? HOLogic.mk_Trueprop
+ |> extensionalize_term
+ |> presimp ? presimplify_term thy
+ |> perhaps (try (HOLogic.dest_Trueprop))
+ |> introduce_combinators_in_term ctxt kind
+ |> kind <> Axiom ? freeze_term
+ val (combformula, ctypes_sorts) = combformula_for_prop thy t []
+ in
+ {name = name, combformula = combformula, kind = kind,
+ ctypes_sorts = ctypes_sorts}
+ end
+
+fun make_axiom ctxt presimp ((name, loc), th) =
+ case make_formula ctxt presimp name Axiom (prop_of th) of
+ {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => NONE
+ | formula => SOME ((name, loc), formula)
+fun make_conjecture ctxt ts =
+ let val last = length ts - 1 in
+ map2 (fn j => make_formula ctxt true (Int.toString j)
+ (if j = last then Conjecture else Hypothesis))
+ (0 upto last) ts
+ end
+
+(** Helper facts **)
+
+fun count_combterm (CombConst ((s, _), _, _)) =
+ Symtab.map_entry s (Integer.add 1)
+ | count_combterm (CombVar _) = I
+ | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2]
+fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
+ | count_combformula (AConn (_, phis)) = fold count_combformula phis
+ | count_combformula (AAtom tm) = count_combterm tm
+fun count_prepared_formula ({combformula, ...} : prepared_formula) =
+ count_combformula combformula
+
+val optional_helpers =
+ [(["c_COMBI"], @{thms Meson.COMBI_def}),
+ (["c_COMBK"], @{thms Meson.COMBK_def}),
+ (["c_COMBB"], @{thms Meson.COMBB_def}),
+ (["c_COMBC"], @{thms Meson.COMBC_def}),
+ (["c_COMBS"], @{thms Meson.COMBS_def})]
+val optional_typed_helpers =
+ [(["c_True", "c_False", "c_If"], @{thms True_or_False}),
+ (["c_If"], @{thms if_True if_False})]
+val mandatory_helpers = @{thms Metis.fequal_def}
+
+val init_counters =
+ [optional_helpers, optional_typed_helpers] |> maps (maps fst)
+ |> sort_distinct string_ord |> map (rpair 0) |> Symtab.make
+
+fun get_helper_facts ctxt is_FO full_types conjectures axioms =
+ let
+ val ct =
+ fold (fold count_prepared_formula) [conjectures, axioms] init_counters
+ fun is_needed c = the (Symtab.lookup ct c) > 0
+ fun baptize th = ((Thm.get_name_hint th, false), th)
+ in
+ (optional_helpers
+ |> full_types ? append optional_typed_helpers
+ |> maps (fn (ss, ths) =>
+ if exists is_needed ss then map baptize ths else [])) @
+ (if is_FO then [] else map baptize mandatory_helpers)
+ |> map_filter (Option.map snd o make_axiom ctxt false)
+ end
+
+fun prepare_axiom ctxt (ax as (_, th)) = (prop_of th, make_axiom ctxt true ax)
+
+fun prepare_formulas ctxt full_types hyp_ts concl_t axioms =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val (axiom_ts, prepared_axioms) = ListPair.unzip axioms
+ (* Remove existing axioms from the conjecture, as this can dramatically
+ boost an ATP's performance (for some reason). *)
+ val hyp_ts = hyp_ts |> filter_out (member (op aconv) axiom_ts)
+ val goal_t = Logic.list_implies (hyp_ts, concl_t)
+ val is_FO = Meson.is_fol_term thy goal_t
+ val subs = tfree_classes_of_terms [goal_t]
+ val supers = tvar_classes_of_terms axiom_ts
+ val tycons = type_consts_of_terms thy (goal_t :: axiom_ts)
+ (* TFrees in the conjecture; TVars in the axioms *)
+ val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t])
+ val (axiom_names, axioms) = ListPair.unzip (map_filter I prepared_axioms)
+ val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
+ val (supers', arity_clauses) = make_arity_clauses thy tycons supers
+ val class_rel_clauses = make_class_rel_clauses thy subs supers'
+ in
+ (axiom_names |> map single |> Vector.fromList,
+ (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses))
+ end
+
+fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
+
+fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])
+ | fo_term_for_combtyp (CombTFree name) = ATerm (name, [])
+ | fo_term_for_combtyp (CombType (name, tys)) =
+ ATerm (name, map fo_term_for_combtyp tys)
+
+fun fo_literal_for_type_literal (TyLitVar (class, name)) =
+ (true, ATerm (class, [ATerm (name, [])]))
+ | fo_literal_for_type_literal (TyLitFree (class, name)) =
+ (true, ATerm (class, [ATerm (name, [])]))
+
+fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
+
+fun fo_term_for_combterm full_types =
+ let
+ fun aux top_level u =
+ let
+ val (head, args) = strip_combterm_comb u
+ val (x, ty_args) =
+ case head of
+ CombConst (name as (s, s'), _, ty_args) =>
+ let val ty_args = if full_types then [] else ty_args in
+ if s = "equal" then
+ if top_level andalso length args = 2 then (name, [])
+ else (("c_fequal", @{const_name Metis.fequal}), ty_args)
+ else if top_level then
+ case s of
+ "c_False" => (("$false", s'), [])
+ | "c_True" => (("$true", s'), [])
+ | _ => (name, ty_args)
+ else
+ (name, ty_args)
+ end
+ | CombVar (name, _) => (name, [])
+ | CombApp _ => raise Fail "impossible \"CombApp\""
+ val t = ATerm (x, map fo_term_for_combtyp ty_args @
+ map (aux false) args)
+ in
+ if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t
+ end
+ in aux true end
+
+fun formula_for_combformula full_types =
+ let
+ fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
+ | aux (AConn (c, phis)) = AConn (c, map aux phis)
+ | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm)
+ in aux end
+
+fun formula_for_axiom full_types
+ ({combformula, ctypes_sorts, ...} : prepared_formula) =
+ mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
+ (type_literals_for_types ctypes_sorts))
+ (formula_for_combformula full_types combformula)
+
+fun problem_line_for_fact prefix full_types (formula as {name, kind, ...}) =
+ Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula)
+
+fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
+ superclass, ...}) =
+ let val ty_arg = ATerm (("T", "T"), []) in
+ Fof (class_rel_clause_prefix ^ ascii_of name, Axiom,
+ AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
+ AAtom (ATerm (superclass, [ty_arg]))]))
+ end
+
+fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
+ (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
+ | fo_literal_for_arity_literal (TVarLit (c, sort)) =
+ (false, ATerm (c, [ATerm (sort, [])]))
+
+fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits,
+ ...}) =
+ Fof (arity_clause_prefix ^ ascii_of name, Axiom,
+ mk_ahorn (map (formula_for_fo_literal o apfst not
+ o fo_literal_for_arity_literal) premLits)
+ (formula_for_fo_literal
+ (fo_literal_for_arity_literal conclLit)))
+
+fun problem_line_for_conjecture full_types
+ ({name, kind, combformula, ...} : prepared_formula) =
+ Fof (conjecture_prefix ^ name, kind,
+ formula_for_combformula full_types combformula)
+
+fun free_type_literals_for_conjecture ({ctypes_sorts, ...} : prepared_formula) =
+ map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
+
+fun problem_line_for_free_type j lit =
+ Fof (tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit)
+fun problem_lines_for_free_types conjectures =
+ let
+ val litss = map free_type_literals_for_conjecture conjectures
+ val lits = fold (union (op =)) litss []
+ in map2 problem_line_for_free_type (0 upto length lits - 1) lits end
+
+(** "hBOOL" and "hAPP" **)
+
+type const_info = {min_arity: int, max_arity: int, sub_level: bool}
+
+fun consider_term top_level (ATerm ((s, _), ts)) =
+ (if is_atp_variable s then
+ I
+ else
+ let val n = length ts in
+ Symtab.map_default
+ (s, {min_arity = n, max_arity = 0, sub_level = false})
+ (fn {min_arity, max_arity, sub_level} =>
+ {min_arity = Int.min (n, min_arity),
+ max_arity = Int.max (n, max_arity),
+ sub_level = sub_level orelse not top_level})
+ end)
+ #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
+fun consider_formula (AQuant (_, _, phi)) = consider_formula phi
+ | consider_formula (AConn (_, phis)) = fold consider_formula phis
+ | consider_formula (AAtom tm) = consider_term true tm
+
+fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi
+fun consider_problem problem = fold (fold consider_problem_line o snd) problem
+
+fun const_table_for_problem explicit_apply problem =
+ if explicit_apply then NONE
+ else SOME (Symtab.empty |> consider_problem problem)
+
+fun min_arity_of thy full_types NONE s =
+ (if s = "equal" orelse s = type_wrapper_name orelse
+ String.isPrefix type_const_prefix s orelse
+ String.isPrefix class_prefix s then
+ 16383 (* large number *)
+ else if full_types then
+ 0
+ else case strip_prefix_and_unascii const_prefix s of
+ SOME s' => num_type_args thy (invert_const s')
+ | NONE => 0)
+ | min_arity_of _ _ (SOME the_const_tab) s =
+ case Symtab.lookup the_const_tab s of
+ SOME ({min_arity, ...} : const_info) => min_arity
+ | NONE => 0
+
+fun full_type_of (ATerm ((s, _), [ty, _])) =
+ if s = type_wrapper_name then ty else raise Fail "expected type wrapper"
+ | full_type_of _ = raise Fail "expected type wrapper"
+
+fun list_hAPP_rev _ t1 [] = t1
+ | list_hAPP_rev NONE t1 (t2 :: ts2) =
+ ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])
+ | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
+ let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
+ [full_type_of t2, ty]) in
+ ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
+ end
+
+fun repair_applications_in_term thy full_types const_tab =
+ let
+ fun aux opt_ty (ATerm (name as (s, _), ts)) =
+ if s = type_wrapper_name then
+ case ts of
+ [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])
+ | _ => raise Fail "malformed type wrapper"
+ else
+ let
+ val ts = map (aux NONE) ts
+ val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts
+ in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
+ in aux NONE end
+
+fun boolify t = ATerm (`I "hBOOL", [t])
+
+(* True if the constant ever appears outside of the top-level position in
+ literals, or if it appears with different arities (e.g., because of different
+ type instantiations). If false, the constant always receives all of its
+ arguments and is used as a predicate. *)
+fun is_predicate NONE s =
+ s = "equal" orelse s = "$false" orelse s = "$true" orelse
+ String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s
+ | is_predicate (SOME the_const_tab) s =
+ case Symtab.lookup the_const_tab s of
+ SOME {min_arity, max_arity, sub_level} =>
+ not sub_level andalso min_arity = max_arity
+ | NONE => false
+
+fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) =
+ if s = type_wrapper_name then
+ case ts of
+ [_, t' as ATerm ((s', _), _)] =>
+ if is_predicate const_tab s' then t' else boolify t
+ | _ => raise Fail "malformed type wrapper"
+ else
+ t |> not (is_predicate const_tab s) ? boolify
+
+fun close_universally phi =
+ let
+ fun term_vars bounds (ATerm (name as (s, _), tms)) =
+ (is_atp_variable s andalso not (member (op =) bounds name))
+ ? insert (op =) name
+ #> fold (term_vars bounds) tms
+ fun formula_vars bounds (AQuant (_, xs, phi)) =
+ formula_vars (xs @ bounds) phi
+ | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
+ | formula_vars bounds (AAtom tm) = term_vars bounds tm
+ in
+ case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)
+ end
+
+fun repair_formula thy explicit_forall full_types const_tab =
+ let
+ fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
+ | aux (AConn (c, phis)) = AConn (c, map aux phis)
+ | aux (AAtom tm) =
+ AAtom (tm |> repair_applications_in_term thy full_types const_tab
+ |> repair_predicates_in_term const_tab)
+ in aux #> explicit_forall ? close_universally end
+
+fun repair_problem_line thy explicit_forall full_types const_tab
+ (Fof (ident, kind, phi)) =
+ Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi)
+fun repair_problem_with_const_table thy =
+ map o apsnd o map ooo repair_problem_line thy
+
+fun repair_problem thy explicit_forall full_types explicit_apply problem =
+ repair_problem_with_const_table thy explicit_forall full_types
+ (const_table_for_problem explicit_apply problem) problem
+
+fun prepare_atp_problem ctxt readable_names explicit_forall full_types
+ explicit_apply hyp_ts concl_t axioms =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val (axiom_names, (conjectures, axioms, helper_facts, class_rel_clauses,
+ arity_clauses)) =
+ prepare_formulas ctxt full_types hyp_ts concl_t axioms
+ val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms
+ val helper_lines =
+ map (problem_line_for_fact helper_prefix full_types) helper_facts
+ val conjecture_lines =
+ map (problem_line_for_conjecture full_types) conjectures
+ val tfree_lines = problem_lines_for_free_types conjectures
+ val class_rel_lines =
+ map problem_line_for_class_rel_clause class_rel_clauses
+ val arity_lines = map problem_line_for_arity_clause arity_clauses
+ (* Reordering these might or might not confuse the proof reconstruction
+ code or the SPASS Flotter hack. *)
+ val problem =
+ [("Relevant facts", axiom_lines),
+ ("Class relationships", class_rel_lines),
+ ("Arity declarations", arity_lines),
+ ("Helper facts", helper_lines),
+ ("Conjectures", conjecture_lines),
+ ("Type variables", tfree_lines)]
+ |> repair_problem thy explicit_forall full_types explicit_apply
+ val (problem, pool) = nice_atp_problem readable_names problem
+ val conjecture_offset =
+ length axiom_lines + length class_rel_lines + length arity_lines
+ + length helper_lines
+ in
+ (problem,
+ case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
+ conjecture_offset, axiom_names)
+ end
+
+end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Fri Oct 22 13:59:34 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Fri Oct 22 17:15:46 2010 +0200
@@ -9,35 +9,38 @@
sig
datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
+ type relevance_fudge =
+ {worse_irrel_freq : real,
+ higher_order_irrel_weight : real,
+ abs_rel_weight : real,
+ abs_irrel_weight : real,
+ skolem_irrel_weight : real,
+ theory_const_rel_weight : real,
+ theory_const_irrel_weight : real,
+ intro_bonus : real,
+ elim_bonus : real,
+ simp_bonus : real,
+ local_bonus : real,
+ assum_bonus : real,
+ chained_bonus : real,
+ max_imperfect : real,
+ max_imperfect_exp : real,
+ threshold_divisor : real,
+ ridiculous_threshold : real}
+
type relevance_override =
- {add: (Facts.ref * Attrib.src list) list,
- del: (Facts.ref * Attrib.src list) list,
- only: bool}
+ {add : (Facts.ref * Attrib.src list) list,
+ del : (Facts.ref * Attrib.src list) list,
+ only : bool}
val trace : bool Unsynchronized.ref
- val worse_irrel_freq : real Unsynchronized.ref
- val higher_order_irrel_weight : real Unsynchronized.ref
- val abs_rel_weight : real Unsynchronized.ref
- val abs_irrel_weight : real Unsynchronized.ref
- val skolem_irrel_weight : real Unsynchronized.ref
- val theory_const_rel_weight : real Unsynchronized.ref
- val theory_const_irrel_weight : real Unsynchronized.ref
- val intro_bonus : real Unsynchronized.ref
- val elim_bonus : real Unsynchronized.ref
- val simp_bonus : real Unsynchronized.ref
- val local_bonus : real Unsynchronized.ref
- val assum_bonus : real Unsynchronized.ref
- val chained_bonus : real Unsynchronized.ref
- val max_imperfect : real Unsynchronized.ref
- val max_imperfect_exp : real Unsynchronized.ref
- val threshold_divisor : real Unsynchronized.ref
- val ridiculous_threshold : real Unsynchronized.ref
val name_thm_pairs_from_ref :
Proof.context -> unit Symtab.table -> thm list
-> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
val relevant_facts :
- Proof.context -> bool -> real * real -> int -> relevance_override
- -> thm list -> term list -> term -> ((string * locality) * thm) list
+ Proof.context -> bool -> real * real -> int -> string list
+ -> relevance_fudge -> relevance_override -> thm list -> term list -> term
+ -> ((string * locality) * thm) list
end;
structure Sledgehammer_Filter : SLEDGEHAMMER_FILTER =
@@ -52,31 +55,31 @@
val term_patterns = false
val respect_no_atp = true
-(* FUDGE *)
-val worse_irrel_freq = Unsynchronized.ref 100.0
-val higher_order_irrel_weight = Unsynchronized.ref 1.05
-val abs_rel_weight = Unsynchronized.ref 0.5
-val abs_irrel_weight = Unsynchronized.ref 2.0
-val skolem_irrel_weight = Unsynchronized.ref 0.75
-val theory_const_rel_weight = Unsynchronized.ref 0.5
-val theory_const_irrel_weight = Unsynchronized.ref 0.25
-val intro_bonus = Unsynchronized.ref 0.15
-val elim_bonus = Unsynchronized.ref 0.15
-val simp_bonus = Unsynchronized.ref 0.15
-val local_bonus = Unsynchronized.ref 0.55
-val assum_bonus = Unsynchronized.ref 1.05
-val chained_bonus = Unsynchronized.ref 1.5
-val max_imperfect = Unsynchronized.ref 11.5
-val max_imperfect_exp = Unsynchronized.ref 1.0
-val threshold_divisor = Unsynchronized.ref 2.0
-val ridiculous_threshold = Unsynchronized.ref 0.1
-
datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
+type relevance_fudge =
+ {worse_irrel_freq : real,
+ higher_order_irrel_weight : real,
+ abs_rel_weight : real,
+ abs_irrel_weight : real,
+ skolem_irrel_weight : real,
+ theory_const_rel_weight : real,
+ theory_const_irrel_weight : real,
+ intro_bonus : real,
+ elim_bonus : real,
+ simp_bonus : real,
+ local_bonus : real,
+ assum_bonus : real,
+ chained_bonus : real,
+ max_imperfect : real,
+ max_imperfect_exp : real,
+ threshold_divisor : real,
+ ridiculous_threshold : real}
+
type relevance_override =
- {add: (Facts.ref * Attrib.src list) list,
- del: (Facts.ref * Attrib.src list) list,
- only: bool}
+ {add : (Facts.ref * Attrib.src list) list,
+ del : (Facts.ref * Attrib.src list) list,
+ only : bool}
val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
val abs_name = sledgehammer_prefix ^ "abs"
@@ -172,16 +175,10 @@
fun string_for_hyper_pconst (s, ps) =
s ^ "{" ^ commas (map string_for_ptype ps) ^ "}"
-(* These are typically simplified away by "Meson.presimplify". Equality is
- handled specially via "fequal". *)
-val boring_consts =
- [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let},
- @{const_name HOL.eq}]
-
(* Add a pconstant to the table, but a [] entry means a standard
connective, which we ignore.*)
-fun add_pconst_to_table also_skolem (c, p) =
- if member (op =) boring_consts c orelse
+fun add_pconst_to_table irrelevant_consts also_skolem (c, p) =
+ if member (op =) irrelevant_consts c orelse
(not also_skolem andalso String.isPrefix skolem_prefix c) then
I
else
@@ -189,14 +186,15 @@
fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
-fun pconsts_in_terms thy also_skolems pos ts =
+fun pconsts_in_terms thy irrelevant_consts also_skolems pos ts =
let
val flip = Option.map not
(* We include free variables, as well as constants, to handle locales. For
each quantifiers that must necessarily be skolemized by the ATP, we
introduce a fresh constant to simulate the effect of Skolemization. *)
fun do_const const (s, T) ts =
- add_pconst_to_table also_skolems (rich_pconst thy const (s, T) ts)
+ add_pconst_to_table irrelevant_consts also_skolems
+ (rich_pconst thy const (s, T) ts)
#> fold do_term ts
and do_term t =
case strip_comb t of
@@ -204,13 +202,14 @@
| (Free x, ts) => do_const false x ts
| (Abs (_, T, t'), ts) =>
(null ts
- ? add_pconst_to_table true (abs_name, PType (order_of_type T + 1, [])))
+ ? add_pconst_to_table irrelevant_consts true
+ (abs_name, PType (order_of_type T + 1, [])))
#> fold do_term (t' :: ts)
| (_, ts) => fold do_term ts
fun do_quantifier will_surely_be_skolemized abs_T body_t =
do_formula pos body_t
#> (if also_skolems andalso will_surely_be_skolemized then
- add_pconst_to_table true
+ add_pconst_to_table irrelevant_consts true
(gensym skolem_prefix, PType (order_of_type abs_T, []))
else
I)
@@ -254,9 +253,11 @@
(*Inserts a dummy "constant" referring to the theory name, so that relevance
takes the given theory into account.*)
-fun theory_const_prop_of th =
- if exists (curry (op <) 0.0) [!theory_const_rel_weight,
- !theory_const_irrel_weight] then
+fun theory_const_prop_of ({theory_const_rel_weight,
+ theory_const_irrel_weight, ...} : relevance_fudge)
+ th =
+ if exists (curry (op <) 0.0) [theory_const_rel_weight,
+ theory_const_irrel_weight] then
let
val name = Context.theory_name (theory_of_thm th)
val t = Const (name ^ theory_const_suffix, @{typ bool})
@@ -282,7 +283,7 @@
structure PType_Tab = Table(type key = ptype val ord = ptype_ord)
-fun count_axiom_consts thy =
+fun count_axiom_consts thy fudge =
let
fun do_const const (s, T) ts =
(* Two-dimensional table update. Constant maps to types maps to count. *)
@@ -295,7 +296,7 @@
| (Free x, ts) => do_const false x ts
| (Abs (_, _, t'), ts) => fold do_term (t' :: ts)
| (_, ts) => fold do_term ts
- in do_term o theory_const_prop_of o snd end
+ in do_term o theory_const_prop_of fudge o snd end
(**** Actual Filtering Code ****)
@@ -322,11 +323,12 @@
very rare constants and very common ones -- the former because they can't
lead to the inclusion of too many new facts, and the latter because they are
so common as to be of little interest. *)
-fun irrel_weight_for order freq =
- let val (k, x) = !worse_irrel_freq |> `Real.ceil in
+fun irrel_weight_for ({worse_irrel_freq, higher_order_irrel_weight, ...}
+ : relevance_fudge) order freq =
+ let val (k, x) = worse_irrel_freq |> `Real.ceil in
(if freq < k then Math.ln (Real.fromInt (freq + 1)) / Math.ln x
else rel_weight_for order freq / rel_weight_for order k)
- * pow_int (!higher_order_irrel_weight) (order - 1)
+ * pow_int higher_order_irrel_weight (order - 1)
end
(* Computes a constant's weight, as determined by its frequency. *)
@@ -337,22 +339,25 @@
else if String.isSuffix theory_const_suffix s then theory_const_weight
else weight_for m (pconst_freq (match_ptype o f) const_tab c)
-fun rel_pconst_weight const_tab =
- generic_pconst_weight (!abs_rel_weight) 0.0 (!theory_const_rel_weight)
+fun rel_pconst_weight ({abs_rel_weight, theory_const_rel_weight, ...}
+ : relevance_fudge) const_tab =
+ generic_pconst_weight abs_rel_weight 0.0 theory_const_rel_weight
rel_weight_for I const_tab
-fun irrel_pconst_weight const_tab =
- generic_pconst_weight (!abs_irrel_weight) (!skolem_irrel_weight)
- (!theory_const_irrel_weight) irrel_weight_for swap const_tab
+fun irrel_pconst_weight (fudge as {abs_irrel_weight, skolem_irrel_weight,
+ theory_const_irrel_weight, ...}) const_tab =
+ generic_pconst_weight abs_irrel_weight skolem_irrel_weight
+ theory_const_irrel_weight (irrel_weight_for fudge) swap
+ const_tab
-fun locality_bonus General = 0.0
- | locality_bonus Intro = !intro_bonus
- | locality_bonus Elim = !elim_bonus
- | locality_bonus Simp = !simp_bonus
- | locality_bonus Local = !local_bonus
- | locality_bonus Assum = !assum_bonus
- | locality_bonus Chained = !chained_bonus
+fun locality_bonus (_ : relevance_fudge) General = 0.0
+ | locality_bonus {intro_bonus, ...} Intro = intro_bonus
+ | locality_bonus {elim_bonus, ...} Elim = elim_bonus
+ | locality_bonus {simp_bonus, ...} Simp = simp_bonus
+ | locality_bonus {local_bonus, ...} Local = local_bonus
+ | locality_bonus {assum_bonus, ...} Assum = assum_bonus
+ | locality_bonus {chained_bonus, ...} Chained = chained_bonus
-fun axiom_weight loc const_tab relevant_consts axiom_consts =
+fun axiom_weight fudge loc const_tab relevant_consts axiom_consts =
case axiom_consts |> List.partition (pconst_hyper_mem I relevant_consts)
||> filter_out (pconst_hyper_mem swap relevant_consts) of
([], _) => 0.0
@@ -360,15 +365,15 @@
let
val irrel = irrel |> filter_out (pconst_mem swap rel)
val rel_weight =
- 0.0 |> fold (curry (op +) o rel_pconst_weight const_tab) rel
+ 0.0 |> fold (curry (op +) o rel_pconst_weight fudge const_tab) rel
val irrel_weight =
- ~ (locality_bonus loc)
- |> fold (curry (op +) o irrel_pconst_weight const_tab) irrel
+ ~ (locality_bonus fudge loc)
+ |> fold (curry (op +) o irrel_pconst_weight fudge const_tab) irrel
val res = rel_weight / (rel_weight + irrel_weight)
in if Real.isFinite res then res else 0.0 end
(* FIXME: experiment
-fun debug_axiom_weight loc const_tab relevant_consts axiom_consts =
+fun debug_axiom_weight fudge loc const_tab relevant_consts axiom_consts =
case axiom_consts |> List.partition (pconst_hyper_mem I relevant_consts)
||> filter_out (pconst_hyper_mem swap relevant_consts) of
([], _) => 0.0
@@ -378,19 +383,20 @@
val rels_weight =
0.0 |> fold (curry (op +) o rel_pconst_weight const_tab) rel
val irrels_weight =
- ~ (locality_bonus loc)
- |> fold (curry (op +) o irrel_pconst_weight const_tab) irrel
+ ~ (locality_bonus fudge loc)
+ |> fold (curry (op +) o irrel_pconst_weight fudge const_tab) irrel
val _ = tracing (PolyML.makestring ("REL: ", map (`(rel_pconst_weight const_tab)) rel))
-val _ = tracing (PolyML.makestring ("IRREL: ", map (`(irrel_pconst_weight const_tab)) irrel))
+val _ = tracing (PolyML.makestring ("IRREL: ", map (`(irrel_pconst_weight fudge const_tab)) irrel))
val res = rels_weight / (rels_weight + irrels_weight)
in if Real.isFinite res then res else 0.0 end
*)
-fun pconsts_in_axiom thy t =
+fun pconsts_in_axiom thy irrelevant_consts t =
Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
- (pconsts_in_terms thy true (SOME true) [t]) []
-fun pair_consts_axiom thy axiom =
- case axiom |> snd |> theory_const_prop_of |> pconsts_in_axiom thy of
+ (pconsts_in_terms thy irrelevant_consts true (SOME true) [t]) []
+fun pair_consts_axiom thy irrelevant_consts fudge axiom =
+ case axiom |> snd |> theory_const_prop_of fudge
+ |> pconsts_in_axiom thy irrelevant_consts of
[] => NONE
| consts => SOME ((axiom, consts), NONE)
@@ -398,12 +404,13 @@
(((unit -> string) * locality) * thm) * (string * ptype) list
fun take_most_relevant max_relevant remaining_max
- (candidates : (annotated_thm * real) list) =
+ ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge)
+ (candidates : (annotated_thm * real) list) =
let
val max_imperfect =
- Real.ceil (Math.pow (!max_imperfect,
+ Real.ceil (Math.pow (max_imperfect,
Math.pow (Real.fromInt remaining_max
- / Real.fromInt max_relevant, !max_imperfect_exp)))
+ / Real.fromInt max_relevant, max_imperfect_exp)))
val (perfect, imperfect) =
candidates |> sort (Real.compare o swap o pairself snd)
|> take_prefix (fn (_, w) => w > 0.99999)
@@ -419,22 +426,23 @@
(accepts, more_rejects @ rejects)
end
-fun if_empty_replace_with_locality thy axioms loc tab =
+fun if_empty_replace_with_locality thy irrelevant_consts axioms loc tab =
if Symtab.is_empty tab then
- pconsts_in_terms thy false (SOME false)
+ pconsts_in_terms thy irrelevant_consts false (SOME false)
(map_filter (fn ((_, loc'), th) =>
if loc' = loc then SOME (prop_of th) else NONE) axioms)
else
tab
-fun relevance_filter ctxt threshold0 decay max_relevant
- ({add, del, ...} : relevance_override) axioms goal_ts =
+fun relevance_filter ctxt threshold0 decay max_relevant irrelevant_consts
+ (fudge as {threshold_divisor, ridiculous_threshold, ...})
+ ({add, del, ...} : relevance_override) axioms goal_ts =
let
val thy = ProofContext.theory_of ctxt
- val const_tab = fold (count_axiom_consts thy) axioms Symtab.empty
+ val const_tab = fold (count_axiom_consts thy fudge) axioms Symtab.empty
val goal_const_tab =
- pconsts_in_terms thy false (SOME false) goal_ts
- |> fold (if_empty_replace_with_locality thy axioms)
+ pconsts_in_terms thy irrelevant_consts false (SOME false) goal_ts
+ |> fold (if_empty_replace_with_locality thy irrelevant_consts axioms)
[Chained, Assum, Local]
val add_ths = Attrib.eval_thms ctxt add
val del_ths = Attrib.eval_thms ctxt del
@@ -450,19 +458,20 @@
else NONE) rejects
fun relevant [] rejects [] =
(* Nothing has been added this iteration. *)
- if j = 0 andalso threshold >= !ridiculous_threshold then
+ if j = 0 andalso threshold >= ridiculous_threshold then
(* First iteration? Try again. *)
- iter 0 max_relevant (threshold / !threshold_divisor) rel_const_tab
+ iter 0 max_relevant (threshold / threshold_divisor) rel_const_tab
hopeless hopeful
else
game_over (rejects @ hopeless)
| relevant candidates rejects [] =
let
val (accepts, more_rejects) =
- take_most_relevant max_relevant remaining_max candidates
+ take_most_relevant max_relevant remaining_max fudge candidates
val rel_const_tab' =
rel_const_tab
- |> fold (add_pconst_to_table false) (maps (snd o fst) accepts)
+ |> fold (add_pconst_to_table irrelevant_consts false)
+ (maps (snd o fst) accepts)
fun is_dirty (c, _) =
Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c
val (hopeful_rejects, hopeless_rejects) =
@@ -499,11 +508,12 @@
val weight =
case cached_weight of
SOME w => w
- | NONE => axiom_weight loc const_tab rel_const_tab axiom_consts
+ | NONE => axiom_weight fudge loc const_tab rel_const_tab
+ axiom_consts
(* FIXME: experiment
val name = fst (fst (fst ax)) ()
val _ = if String.isSubstring "positive_minus" name orelse String.isSubstring "not_exp_le_zero" name then
-tracing ("*** " ^ name ^ PolyML.makestring (debug_axiom_weight loc const_tab rel_const_tab axiom_consts))
+tracing ("*** " ^ name ^ PolyML.makestring (debug_axiom_weight fudge loc const_tab rel_const_tab axiom_consts))
else
()
*)
@@ -524,7 +534,7 @@
end
in
axioms |> filter_out (member Thm.eq_thm del_ths o snd)
- |> map_filter (pair_consts_axiom thy)
+ |> map_filter (pair_consts_axiom thy irrelevant_consts fudge)
|> iter 0 max_relevant threshold0 goal_const_tab []
|> tap (fn res => trace_msg (fn () =>
"Total relevant: " ^ Int.toString (length res)))
@@ -708,7 +718,9 @@
(Term.add_vars t [] |> sort_wrt (fst o fst))
|> fst
-fun all_name_thms_pairs ctxt reserved full_types add_ths chained_ths =
+fun all_name_thms_pairs ctxt reserved full_types
+ ({intro_bonus, elim_bonus, simp_bonus, ...} : relevance_fudge) add_ths
+ chained_ths =
let
val thy = ProofContext.theory_of ctxt
val global_facts = Global_Theory.facts_of thy
@@ -718,7 +730,7 @@
fun is_assum th = exists (fn ct => prop_of th aconv term_of ct) assms
val is_chained = member Thm.eq_thm chained_ths
val (intros, elims, simps) =
- if exists (curry (op <) 0.0) [!intro_bonus, !elim_bonus, !simp_bonus] then
+ if exists (curry (op <) 0.0) [intro_bonus, elim_bonus, simp_bonus] then
clasimpset_rules_of ctxt
else
(Termtab.empty, Termtab.empty, Termtab.empty)
@@ -773,7 +785,8 @@
| NONE => ""
end),
let val t = prop_of th in
- if is_chained th then Chained
+ if is_chained th then
+ Chained
else if global then
if Termtab.defined intros t then Intro
else if Termtab.defined elims t then Elim
@@ -801,8 +814,8 @@
(***************************************************************)
fun relevant_facts ctxt full_types (threshold0, threshold1) max_relevant
- (relevance_override as {add, only, ...}) chained_ths hyp_ts
- concl_t =
+ irrelevant_consts fudge (override as {add, only, ...})
+ chained_ths hyp_ts concl_t =
let
val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
1.0 / Real.fromInt (max_relevant + 1))
@@ -813,7 +826,7 @@
maps (map (fn ((name, loc), th) => ((K name, loc), (true, th)))
o name_thm_pairs_from_ref ctxt reserved chained_ths) add
else
- all_name_thms_pairs ctxt reserved full_types add_ths chained_ths)
+ all_name_thms_pairs ctxt reserved full_types fudge add_ths chained_ths)
|> name_thm_pairs ctxt (respect_no_atp andalso not only)
|> uniquify
in
@@ -825,8 +838,8 @@
max_relevant = 0 then
[]
else
- relevance_filter ctxt threshold0 decay max_relevant relevance_override
- axioms (concl_t :: hyp_ts))
+ relevance_filter ctxt threshold0 decay max_relevant irrelevant_consts
+ fudge override axioms (concl_t :: hyp_ts))
|> map (apfst (apfst (fn f => f ())))
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Oct 22 13:59:34 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Oct 22 17:15:46 2010 +0200
@@ -9,10 +9,10 @@
type params = Sledgehammer.params
val auto : bool Unsynchronized.ref
- val atps : string Unsynchronized.ref
+ val provers : string Unsynchronized.ref
val timeout : int Unsynchronized.ref
val full_types : bool Unsynchronized.ref
- val default_params : theory -> (string * string) list -> params
+ val default_params : Proof.context -> (string * string) list -> params
val setup : theory -> theory
end;
@@ -49,14 +49,14 @@
(*** parameters ***)
-val atps = Unsynchronized.ref ""
+val provers = Unsynchronized.ref ""
val timeout = Unsynchronized.ref 30
val full_types = Unsynchronized.ref false
val _ =
ProofGeneralPgip.add_preference Preferences.category_proof
- (Preferences.string_pref atps
- "Sledgehammer: ATPs"
+ (Preferences.string_pref provers
+ "Sledgehammer: Provers"
"Default automatic provers (separated by whitespace)")
val _ =
@@ -84,7 +84,9 @@
("isar_shrink_factor", "1")]
val alias_params =
- [("atp", "atps")]
+ [("prover", "provers"),
+ ("atps", "provers"), (* FIXME: legacy *)
+ ("atp", "provers")] (* FIXME: legacy *)
val negated_alias_params =
[("non_blocking", "blocking"),
("no_debug", "debug"),
@@ -98,7 +100,7 @@
["debug", "verbose", "overlord", "full_types", "isar_proof",
"isar_shrink_factor", "timeout"]
-val property_dependent_params = ["atps", "full_types", "timeout"]
+val property_dependent_params = ["provers", "full_types", "timeout"]
fun is_known_raw_param s =
AList.defined (op =) default_default_params s orelse
@@ -128,16 +130,57 @@
val extend = I
fun merge p : T = AList.merge (op =) (K true) p)
+(* FIXME: dummy *)
+fun is_smt_solver_installed ctxt = true
+
+fun remotify_prover_if_available_and_not_already_remote thy name =
+ if String.isPrefix remote_prefix name then
+ SOME name
+ else
+ let val remote_name = remote_prefix ^ name in
+ if is_prover_available thy remote_name then SOME remote_name else NONE
+ end
+
+fun remotify_prover_if_not_installed ctxt name =
+ let val thy = ProofContext.theory_of ctxt in
+ if is_prover_available thy name andalso is_prover_installed ctxt name then
+ SOME name
+ else
+ remotify_prover_if_available_and_not_already_remote thy name
+ end
+
+fun avoid_too_many_local_threads _ _ [] = []
+ | avoid_too_many_local_threads thy 0 provers =
+ map_filter (remotify_prover_if_available_and_not_already_remote thy) provers
+ | avoid_too_many_local_threads thy n (prover :: provers) =
+ let val n = if String.isPrefix remote_prefix prover then n else n - 1 in
+ prover :: avoid_too_many_local_threads thy n provers
+ end
+
+(* The first ATP of the list is used by Auto Sledgehammer. Because of the low
+ timeout, it makes sense to put SPASS first. *)
+fun default_provers_param_value ctxt =
+ let val thy = ProofContext.theory_of ctxt in
+ [spassN, eN, vampireN, sine_eN (* FIXME: , smtN *)]
+ |> map_filter (remotify_prover_if_not_installed ctxt)
+ |> avoid_too_many_local_threads thy (Thread.numProcessors ())
+ |> space_implode " "
+ end
+
val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param
-fun default_raw_params thy =
- Data.get thy
- |> fold (AList.default (op =))
- [("atps", [case !atps of "" => default_atps_param_value () | s => s]),
- ("full_types", [if !full_types then "true" else "false"]),
- ("timeout", let val timeout = !timeout in
- [if timeout <= 0 then "none"
- else string_of_int timeout ^ " s"]
- end)]
+fun default_raw_params ctxt =
+ let val thy = ProofContext.theory_of ctxt in
+ Data.get thy
+ |> fold (AList.default (op =))
+ [("provers", [case !provers of
+ "" => default_provers_param_value ctxt
+ | s => s]),
+ ("full_types", [if !full_types then "true" else "false"]),
+ ("timeout", let val timeout = !timeout in
+ [if timeout <= 0 then "none"
+ else string_of_int timeout ^ " s"]
+ end)]
+ end
val infinity_time_in_secs = 60 * 60 * 24 * 365
val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
@@ -180,7 +223,8 @@
val debug = not auto andalso lookup_bool "debug"
val verbose = debug orelse (not auto andalso lookup_bool "verbose")
val overlord = lookup_bool "overlord"
- val atps = lookup_string "atps" |> space_explode " " |> auto ? single o hd
+ val provers = lookup_string "provers" |> space_explode " "
+ |> auto ? single o hd
val full_types = lookup_bool "full_types"
val explicit_apply = lookup_bool "explicit_apply"
val relevance_thresholds =
@@ -193,13 +237,14 @@
val expect = lookup_string "expect"
in
{blocking = blocking, debug = debug, verbose = verbose, overlord = overlord,
- atps = atps, full_types = full_types, explicit_apply = explicit_apply,
+ provers = provers, full_types = full_types,
+ explicit_apply = explicit_apply,
relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
timeout = timeout, expect = expect}
end
-fun get_params auto thy = extract_params auto (default_raw_params thy)
+fun get_params auto ctxt = extract_params auto (default_raw_params ctxt)
fun default_params thy = get_params false thy o map (apsnd single)
(* Sledgehammer the given subgoal *)
@@ -210,9 +255,9 @@
val runN = "run"
val minimizeN = "minimize"
val messagesN = "messages"
-val available_atpsN = "available_atps"
-val running_atpsN = "running_atps"
-val kill_atpsN = "kill_atps"
+val available_proversN = "available_provers"
+val running_proversN = "running_provers"
+val kill_proversN = "kill_provers"
val refresh_tptpN = "refresh_tptp"
val is_raw_param_relevant_for_minimize =
@@ -220,8 +265,8 @@
fun string_for_raw_param (key, values) =
key ^ (case space_implode " " values of "" => "" | value => " = " ^ value)
-fun minimize_command override_params i atp_name fact_names =
- sledgehammerN ^ " " ^ minimizeN ^ " [atp = " ^ atp_name ^
+fun minimize_command override_params i prover_name fact_names =
+ sledgehammerN ^ " " ^ minimizeN ^ " [prover = " ^ prover_name ^
(override_params |> filter is_raw_param_relevant_for_minimize
|> implode o map (prefix ", " o string_for_raw_param)) ^
"] (" ^ space_implode " " fact_names ^ ")" ^
@@ -229,27 +274,28 @@
fun hammer_away override_params subcommand opt_i relevance_override state =
let
+ val ctxt = Proof.context_of state
val thy = Proof.theory_of state
val _ = app check_raw_param override_params
in
if subcommand = runN then
let val i = the_default 1 opt_i in
- run_sledgehammer (get_params false thy override_params) false i
+ run_sledgehammer (get_params false ctxt override_params) false i
relevance_override (minimize_command override_params i)
state
|> K ()
end
else if subcommand = minimizeN then
- run_minimize (get_params false thy override_params) (the_default 1 opt_i)
+ run_minimize (get_params false ctxt override_params) (the_default 1 opt_i)
(#add relevance_override) state
else if subcommand = messagesN then
messages opt_i
- else if subcommand = available_atpsN then
- available_atps thy
- else if subcommand = running_atpsN then
- running_atps ()
- else if subcommand = kill_atpsN then
- kill_atps ()
+ else if subcommand = available_proversN then
+ available_provers thy
+ else if subcommand = running_proversN then
+ running_provers ()
+ else if subcommand = kill_proversN then
+ kill_provers ()
else if subcommand = refresh_tptpN then
refresh_systems_on_tptp ()
else
@@ -266,13 +312,15 @@
Toplevel.theory
(fold set_default_raw_param params
#> tap (fn thy =>
- writeln ("Default parameters for Sledgehammer:\n" ^
- (case rev (default_raw_params thy) of
- [] => "none"
- | params =>
- (map check_raw_param params;
- params |> map string_for_raw_param
- |> sort_strings |> cat_lines)))))
+ let val ctxt = ProofContext.init_global thy in
+ writeln ("Default parameters for Sledgehammer:\n" ^
+ (case default_raw_params ctxt |> rev of
+ [] => "none"
+ | params =>
+ (map check_raw_param params;
+ params |> map string_for_raw_param
+ |> sort_strings |> cat_lines)))
+ end))
val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
val parse_value = Scan.repeat1 Parse.xname
@@ -307,8 +355,8 @@
if not (!auto) then
(false, state)
else
- let val thy = Proof.theory_of state in
- run_sledgehammer (get_params true thy []) true 1 no_relevance_override
+ let val ctxt = Proof.context_of state in
+ run_sledgehammer (get_params true ctxt []) true 1 no_relevance_override
(minimize_command [] 1) state
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Oct 22 13:59:34 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Oct 22 17:15:46 2010 +0200
@@ -2,7 +2,7 @@
Author: Philipp Meyer, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
-Minimization of theorem list for Metis using automatic theorem provers.
+Minimization of fact list for Metis using ATPs.
*)
signature SLEDGEHAMMER_MINIMIZE =
@@ -10,7 +10,7 @@
type locality = Sledgehammer_Filter.locality
type params = Sledgehammer.params
- val minimize_theorems :
+ val minimize_facts :
params -> int -> int -> Proof.state -> ((string * locality) * thm list) list
-> ((string * locality) * thm list) list option * string
val run_minimize :
@@ -23,8 +23,6 @@
open ATP_Proof
open Sledgehammer_Util
open Sledgehammer_Filter
-open Sledgehammer_Translate
-open Sledgehammer_Reconstruct
open Sledgehammer
(* wrapper for calling external prover *)
@@ -34,9 +32,9 @@
| string_for_failure Interrupted = "Interrupted."
| string_for_failure _ = "Unknown error."
-fun n_theorems names =
+fun n_facts names =
let val n = length names in
- string_of_int n ^ " theorem" ^ plural_s n ^
+ string_of_int n ^ " fact" ^ plural_s n ^
(if n > 0 then
": " ^ (names |> map fst
|> sort_distinct string_ord |> space_implode " ")
@@ -44,46 +42,44 @@
"")
end
-fun test_theorems ({debug, verbose, overlord, atps, full_types, isar_proof,
- isar_shrink_factor, ...} : params)
- (prover : prover) explicit_apply timeout subgoal state
- axioms =
+fun test_facts ({debug, verbose, overlord, provers, full_types, isar_proof,
+ isar_shrink_factor, ...} : params) (prover : prover)
+ explicit_apply timeout i n state axioms =
let
val _ =
- priority ("Testing " ^ n_theorems (map fst axioms) ^ "...")
+ priority ("Testing " ^ n_facts (map fst axioms) ^ "...")
val params =
{blocking = true, debug = debug, verbose = verbose, overlord = overlord,
- atps = atps, full_types = full_types, explicit_apply = explicit_apply,
- relevance_thresholds = (1.01, 1.01),
- max_relevant = SOME 65536 (* a large number *), isar_proof = isar_proof,
+ provers = provers, full_types = full_types,
+ explicit_apply = explicit_apply, relevance_thresholds = (1.01, 1.01),
+ max_relevant = NONE, isar_proof = isar_proof,
isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""}
- val axioms = maps (fn (n, ths) => map (pair n) ths) axioms
- val {context = ctxt, goal, ...} = Proof.goal state
+ val axioms =
+ axioms |> maps (fn (n, ths) => ths |> map (Unprepared o pair n))
+ val {goal, ...} = Proof.goal state
val problem =
- {state = state, goal = goal, subgoal = subgoal,
- axioms = map (prepare_axiom ctxt) axioms, only = true}
- val result as {outcome, used_thm_names, ...} = prover params (K "") problem
+ {state = state, goal = goal, subgoal = i, subgoal_count = n,
+ axioms = axioms, only = true}
+ val result as {outcome, used_axioms, ...} = prover params (K "") problem
in
priority (case outcome of
- NONE =>
- if length used_thm_names = length axioms then
- "Found proof."
- else
- "Found proof with " ^ n_theorems used_thm_names ^ "."
- | SOME failure => string_for_failure failure);
+ SOME failure => string_for_failure failure
+ | NONE =>
+ if length used_axioms = length axioms then "Found proof."
+ else "Found proof with " ^ n_facts used_axioms ^ ".");
result
end
(* minimalization of thms *)
-fun filter_used_facts used = filter (member (op =) used o fst)
+fun filter_used_axioms used = filter (member (op =) used o fst)
fun sublinear_minimize _ [] p = p
| sublinear_minimize test (x :: xs) (seen, result) =
case test (xs @ seen) of
- result as {outcome = NONE, used_thm_names, ...} : prover_result =>
- sublinear_minimize test (filter_used_facts used_thm_names xs)
- (filter_used_facts used_thm_names seen, result)
+ result as {outcome = NONE, used_axioms, ...} : prover_result =>
+ sublinear_minimize test (filter_used_axioms used_axioms xs)
+ (filter_used_axioms used_axioms seen, result)
| _ => sublinear_minimize test xs (x :: seen, result)
(* Give the ATP some slack. The ATP gets further slack because the Sledgehammer
@@ -91,48 +87,40 @@
timeout. *)
val fudge_msecs = 1000
-fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set."
- | minimize_theorems (params as {debug, atps = atp :: _, full_types,
- isar_proof, isar_shrink_factor, timeout, ...})
- i (_ : int) state axioms =
+fun minimize_facts {provers = [], ...} _ _ _ _ = error "No prover is set."
+ | minimize_facts (params as {provers = prover_name :: _, timeout, ...}) i n
+ state axioms =
let
val thy = Proof.theory_of state
- val prover = get_prover_fun thy atp
+ val prover = get_prover thy false prover_name
val msecs = Time.toMilliseconds timeout
- val _ = priority ("Sledgehammer minimize: ATP " ^ quote atp ^ ".")
- val {context = ctxt, goal, ...} = Proof.goal state
+ val _ = priority ("Sledgehammer minimize: " ^ quote prover_name ^ ".")
+ val {goal, ...} = Proof.goal state
val (_, hyp_ts, concl_t) = strip_subgoal goal i
val explicit_apply =
not (forall (Meson.is_fol_term thy)
(concl_t :: hyp_ts @ maps (map prop_of o snd) axioms))
fun do_test timeout =
- test_theorems params prover explicit_apply timeout i state
+ test_facts params prover explicit_apply timeout i n state
val timer = Timer.startRealTimer ()
in
(case do_test timeout axioms of
- result as {outcome = NONE, pool, used_thm_names,
- conjecture_shape, ...} =>
+ result as {outcome = NONE, used_axioms, ...} =>
let
val time = Timer.checkRealTimer timer
val new_timeout =
Int.min (msecs, Time.toMilliseconds time + fudge_msecs)
|> Time.fromMilliseconds
- val (min_thms, {tstplike_proof, axiom_names, ...}) =
+ val (min_thms, {message, ...}) =
sublinear_minimize (do_test new_timeout)
- (filter_used_facts used_thm_names axioms) ([], result)
+ (filter_used_axioms used_axioms axioms) ([], result)
val n = length min_thms
val _ = priority (cat_lines
- ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^
+ ["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^
(case length (filter (curry (op =) Chained o snd o fst) min_thms) of
0 => ""
| n => " (including " ^ Int.toString n ^ " chained)") ^ ".")
- in
- (SOME min_thms,
- proof_text isar_proof
- (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
- ("Minimized command", full_types, K "", tstplike_proof,
- axiom_names, goal, i) |> fst)
- end
+ in (SOME min_thms, message) end
| {outcome = SOME TimedOut, ...} =>
(NONE, "Timeout: You can increase the time limit using the \"timeout\" \
\option (e.g., \"timeout = " ^
@@ -159,7 +147,8 @@
case subgoal_count state of
0 => priority "No subgoal!"
| n =>
- (kill_atps (); priority (#2 (minimize_theorems params i n state axioms)))
+ (kill_provers ();
+ priority (#2 (minimize_facts params i n state axioms)))
end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Oct 22 13:59:34 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,941 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
- Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
- Author: Claire Quigley, Cambridge University Computer Laboratory
- Author: Jasmin Blanchette, TU Muenchen
-
-Proof reconstruction for Sledgehammer.
-*)
-
-signature SLEDGEHAMMER_RECONSTRUCT =
-sig
- type locality = Sledgehammer_Filter.locality
- type minimize_command = string list -> string
- type metis_params =
- string * bool * minimize_command * string * (string * locality) list vector
- * thm * int
- type isar_params =
- string Symtab.table * bool * int * Proof.context * int list list
- type text_result = string * (string * locality) list
-
- val repair_conjecture_shape_and_axiom_names :
- string -> int list list -> (string * locality) list vector
- -> int list list * (string * locality) list vector
- val metis_proof_text : metis_params -> text_result
- val isar_proof_text : isar_params -> metis_params -> text_result
- val proof_text : bool -> isar_params -> metis_params -> text_result
-end;
-
-structure Sledgehammer_Reconstruct : SLEDGEHAMMER_RECONSTRUCT =
-struct
-
-open ATP_Problem
-open ATP_Proof
-open Metis_Translate
-open Sledgehammer_Util
-open Sledgehammer_Filter
-open Sledgehammer_Translate
-
-type minimize_command = string list -> string
-type metis_params =
- string * bool * minimize_command * string * (string * locality) list vector
- * thm * int
-type isar_params =
- string Symtab.table * bool * int * Proof.context * int list list
-type text_result = string * (string * locality) list
-
-fun is_head_digit s = Char.isDigit (String.sub (s, 0))
-val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
-
-fun find_first_in_list_vector vec key =
- Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
- | (_, value) => value) NONE vec
-
-
-(** SPASS's Flotter hack **)
-
-(* This is a hack required for keeping track of axioms after they have been
- clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is also
- part of this hack. *)
-
-val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
-
-fun extract_clause_sequence output =
- let
- val tokens_of = String.tokens (not o Char.isAlphaNum)
- fun extract_num ("clause" :: (ss as _ :: _)) =
- Int.fromString (List.last ss)
- | extract_num _ = NONE
- in output |> split_lines |> map_filter (extract_num o tokens_of) end
-
-val parse_clause_formula_pair =
- $$ "(" |-- scan_integer --| $$ ","
- -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")"
- --| Scan.option ($$ ",")
-val parse_clause_formula_relation =
- Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
- |-- Scan.repeat parse_clause_formula_pair
-val extract_clause_formula_relation =
- Substring.full #> Substring.position set_ClauseFormulaRelationN
- #> snd #> Substring.position "." #> fst #> Substring.string
- #> explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
- #> fst
-
-fun repair_conjecture_shape_and_axiom_names output conjecture_shape
- axiom_names =
- if String.isSubstring set_ClauseFormulaRelationN output then
- let
- val j0 = hd (hd conjecture_shape)
- val seq = extract_clause_sequence output
- val name_map = extract_clause_formula_relation output
- fun renumber_conjecture j =
- conjecture_prefix ^ string_of_int (j - j0)
- |> AList.find (fn (s, ss) => member (op =) ss s) name_map
- |> map (fn s => find_index (curry (op =) s) seq + 1)
- fun names_for_number j =
- j |> AList.lookup (op =) name_map |> these
- |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of
- |> map (fn name =>
- (name, name |> find_first_in_list_vector axiom_names
- |> the)
- handle Option.Option =>
- error ("No such fact: " ^ quote name ^ "."))
- in
- (conjecture_shape |> map (maps renumber_conjecture),
- seq |> map names_for_number |> Vector.fromList)
- end
- else
- (conjecture_shape, axiom_names)
-
-
-(** Soft-core proof reconstruction: Metis one-liner **)
-
-fun string_for_label (s, num) = s ^ string_of_int num
-
-fun metis_using [] = ""
- | metis_using ls =
- "using " ^ space_implode " " (map string_for_label ls) ^ " "
-fun metis_apply _ 1 = "by "
- | metis_apply 1 _ = "apply "
- | metis_apply i _ = "prefer " ^ string_of_int i ^ " apply "
-fun metis_name full_types = if full_types then "metisFT" else "metis"
-fun metis_call full_types [] = metis_name full_types
- | metis_call full_types ss =
- "(" ^ metis_name full_types ^ " " ^ space_implode " " ss ^ ")"
-fun metis_command full_types i n (ls, ss) =
- metis_using ls ^ metis_apply i n ^ metis_call full_types ss
-fun metis_line banner full_types i n ss =
- banner ^ ": " ^
- Markup.markup Markup.sendback (metis_command full_types i n ([], ss)) ^ "."
-fun minimize_line _ [] = ""
- | minimize_line minimize_command ss =
- case minimize_command ss of
- "" => ""
- | command =>
- "\nTo minimize the number of lemmas, try this: " ^
- Markup.markup Markup.sendback command ^ "."
-
-fun resolve_axiom axiom_names ((_, SOME s)) =
- (case strip_prefix_and_unascii axiom_prefix s of
- SOME s' => (case find_first_in_list_vector axiom_names s' of
- SOME x => [(s', x)]
- | NONE => [])
- | NONE => [])
- | resolve_axiom axiom_names (num, NONE) =
- case Int.fromString num of
- SOME j =>
- if j > 0 andalso j <= Vector.length axiom_names then
- Vector.sub (axiom_names, j - 1)
- else
- []
- | NONE => []
-
-fun add_fact axiom_names (Inference (name, _, [])) =
- append (resolve_axiom axiom_names name)
- | add_fact _ _ = I
-
-fun used_facts_in_tstplike_proof axiom_names =
- atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact axiom_names)
-
-fun used_facts axiom_names =
- used_facts_in_tstplike_proof axiom_names
- #> List.partition (curry (op =) Chained o snd)
- #> pairself (sort_distinct (string_ord o pairself fst))
-
-fun metis_proof_text (banner, full_types, minimize_command,
- tstplike_proof, axiom_names, goal, i) =
- let
- val (chained_lemmas, other_lemmas) =
- used_facts axiom_names tstplike_proof
- val n = Logic.count_prems (prop_of goal)
- in
- (metis_line banner full_types i n (map fst other_lemmas) ^
- minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)),
- other_lemmas @ chained_lemmas)
- end
-
-
-(** Hard-core proof reconstruction: structured Isar proofs **)
-
-(* Simple simplifications to ensure that sort annotations don't leave a trail of
- spurious "True"s. *)
-fun s_not @{const False} = @{const True}
- | s_not @{const True} = @{const False}
- | s_not (@{const Not} $ t) = t
- | s_not t = @{const Not} $ t
-fun s_conj (@{const True}, t2) = t2
- | s_conj (t1, @{const True}) = t1
- | s_conj p = HOLogic.mk_conj p
-fun s_disj (@{const False}, t2) = t2
- | s_disj (t1, @{const False}) = t1
- | s_disj p = HOLogic.mk_disj p
-fun s_imp (@{const True}, t2) = t2
- | s_imp (t1, @{const False}) = s_not t1
- | s_imp p = HOLogic.mk_imp p
-fun s_iff (@{const True}, t2) = t2
- | s_iff (t1, @{const True}) = t1
- | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
-
-fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t
-fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t
-
-fun negate_term (Const (@{const_name All}, T) $ Abs (s, T', t')) =
- Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t')
- | negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
- Const (@{const_name All}, T) $ Abs (s, T', negate_term t')
- | negate_term (@{const HOL.implies} $ t1 $ t2) =
- @{const HOL.conj} $ t1 $ negate_term t2
- | negate_term (@{const HOL.conj} $ t1 $ t2) =
- @{const HOL.disj} $ negate_term t1 $ negate_term t2
- | negate_term (@{const HOL.disj} $ t1 $ t2) =
- @{const HOL.conj} $ negate_term t1 $ negate_term t2
- | negate_term (@{const Not} $ t) = t
- | negate_term t = @{const Not} $ t
-
-val indent_size = 2
-val no_label = ("", ~1)
-
-val raw_prefix = "X"
-val assum_prefix = "A"
-val fact_prefix = "F"
-
-fun resolve_conjecture conjecture_shape (num, s_opt) =
- let
- val k = case try (unprefix conjecture_prefix) (the_default "" s_opt) of
- SOME s => Int.fromString s |> the_default ~1
- | NONE => case Int.fromString num of
- SOME j => find_index (exists (curry (op =) j))
- conjecture_shape
- | NONE => ~1
- in if k >= 0 then [k] else [] end
-
-fun is_axiom conjecture_shape = not o null o resolve_axiom conjecture_shape
-fun is_conjecture conjecture_shape = not o null o resolve_conjecture conjecture_shape
-
-fun raw_label_for_name conjecture_shape name =
- case resolve_conjecture conjecture_shape name of
- [j] => (conjecture_prefix, j)
- | _ => case Int.fromString (fst name) of
- SOME j => (raw_prefix, j)
- | NONE => (raw_prefix ^ fst name, 0)
-
-(**** INTERPRETATION OF TSTP SYNTAX TREES ****)
-
-exception FO_TERM of string fo_term list
-exception FORMULA of (string, string fo_term) formula list
-exception SAME of unit
-
-(* Type variables are given the basic sort "HOL.type". Some will later be
- constrained by information from type literals, or by type inference. *)
-fun type_from_fo_term tfrees (u as ATerm (a, us)) =
- let val Ts = map (type_from_fo_term tfrees) us in
- case strip_prefix_and_unascii type_const_prefix a of
- SOME b => Type (invert_const b, Ts)
- | NONE =>
- if not (null us) then
- raise FO_TERM [u] (* only "tconst"s have type arguments *)
- else case strip_prefix_and_unascii tfree_prefix a of
- SOME b =>
- let val s = "'" ^ b in
- TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
- end
- | NONE =>
- case strip_prefix_and_unascii tvar_prefix a of
- SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
- | NONE =>
- (* Variable from the ATP, say "X1" *)
- Type_Infer.param 0 (a, HOLogic.typeS)
- end
-
-(* Type class literal applied to a type. Returns triple of polarity, class,
- type. *)
-fun type_constraint_from_term pos tfrees (u as ATerm (a, us)) =
- case (strip_prefix_and_unascii class_prefix a,
- map (type_from_fo_term tfrees) us) of
- (SOME b, [T]) => (pos, b, T)
- | _ => raise FO_TERM [u]
-
-(** Accumulate type constraints in a formula: negative type literals **)
-fun add_var (key, z) = Vartab.map_default (key, []) (cons z)
-fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl)
- | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl)
- | add_type_constraint _ = I
-
-fun repair_atp_variable_name f s =
- let
- fun subscript_name s n = s ^ nat_subscript n
- val s = String.map f s
- in
- case space_explode "_" s of
- [_] => (case take_suffix Char.isDigit (String.explode s) of
- (cs1 as _ :: _, cs2 as _ :: _) =>
- subscript_name (String.implode cs1)
- (the (Int.fromString (String.implode cs2)))
- | (_, _) => s)
- | [s1, s2] => (case Int.fromString s2 of
- SOME n => subscript_name s1 n
- | NONE => s)
- | _ => s
- end
-
-(* First-order translation. No types are known for variables. "HOLogic.typeT"
- should allow them to be inferred. *)
-fun raw_term_from_pred thy full_types tfrees =
- let
- fun aux opt_T extra_us u =
- case u of
- ATerm ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1
- | ATerm ("hAPP", [u1, u2]) => aux opt_T (u2 :: extra_us) u1
- | ATerm (a, us) =>
- if a = type_wrapper_name then
- case us of
- [typ_u, term_u] =>
- aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
- | _ => raise FO_TERM us
- else case strip_prefix_and_unascii const_prefix a of
- SOME "equal" =>
- let val ts = map (aux NONE []) us in
- if length ts = 2 andalso hd ts aconv List.last ts then
- (* Vampire is keen on producing these. *)
- @{const True}
- else
- list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
- end
- | SOME b =>
- let
- val c = invert_const b
- val num_type_args = num_type_args thy c
- val (type_us, term_us) =
- chop (if full_types then 0 else num_type_args) us
- (* Extra args from "hAPP" come after any arguments given directly to
- the constant. *)
- val term_ts = map (aux NONE []) term_us
- val extra_ts = map (aux NONE []) extra_us
- val t =
- Const (c, if full_types then
- case opt_T of
- SOME T => map fastype_of term_ts ---> T
- | NONE =>
- if num_type_args = 0 then
- Sign.const_instance thy (c, [])
- else
- raise Fail ("no type information for " ^ quote c)
- else
- Sign.const_instance thy (c,
- map (type_from_fo_term tfrees) type_us))
- in list_comb (t, term_ts @ extra_ts) end
- | NONE => (* a free or schematic variable *)
- let
- val ts = map (aux NONE []) (us @ extra_us)
- val T = map fastype_of ts ---> HOLogic.typeT
- val t =
- case strip_prefix_and_unascii fixed_var_prefix a of
- SOME b => Free (b, T)
- | NONE =>
- case strip_prefix_and_unascii schematic_var_prefix a of
- SOME b => Var ((b, 0), T)
- | NONE =>
- if is_atp_variable a then
- Var ((repair_atp_variable_name Char.toLower a, 0), T)
- else
- (* Skolem constants? *)
- Var ((repair_atp_variable_name Char.toUpper a, 0), T)
- in list_comb (t, ts) end
- in aux (SOME HOLogic.boolT) [] end
-
-fun term_from_pred thy full_types tfrees pos (u as ATerm (s, _)) =
- if String.isPrefix class_prefix s then
- add_type_constraint (type_constraint_from_term pos tfrees u)
- #> pair @{const True}
- else
- pair (raw_term_from_pred thy full_types tfrees u)
-
-val combinator_table =
- [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}),
- (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def_raw}),
- (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def_raw}),
- (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}),
- (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def_raw})]
-
-fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2))
- | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t')
- | uncombine_term (t as Const (x as (s, _))) =
- (case AList.lookup (op =) combinator_table s of
- SOME thm => thm |> prop_of |> specialize_type @{theory} x |> Logic.dest_equals |> snd
- | NONE => t)
- | uncombine_term t = t
-
-(* Update schematic type variables with detected sort constraints. It's not
- totally clear when this code is necessary. *)
-fun repair_tvar_sorts (t, tvar_tab) =
- let
- fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
- | do_type (TVar (xi, s)) =
- TVar (xi, the_default s (Vartab.lookup tvar_tab xi))
- | do_type (TFree z) = TFree z
- fun do_term (Const (a, T)) = Const (a, do_type T)
- | do_term (Free (a, T)) = Free (a, do_type T)
- | do_term (Var (xi, T)) = Var (xi, do_type T)
- | do_term (t as Bound _) = t
- | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t)
- | do_term (t1 $ t2) = do_term t1 $ do_term t2
- in t |> not (Vartab.is_empty tvar_tab) ? do_term end
-
-fun quantify_over_var quant_of var_s t =
- let
- val vars = [] |> Term.add_vars t |> filter (fn ((s, _), _) => s = var_s)
- |> map Var
- in fold_rev quant_of vars t end
-
-(* Interpret an ATP formula as a HOL term, extracting sort constraints as they
- appear in the formula. *)
-fun prop_from_formula thy full_types tfrees phi =
- let
- fun do_formula pos phi =
- case phi of
- AQuant (_, [], phi) => do_formula pos phi
- | AQuant (q, x :: xs, phi') =>
- do_formula pos (AQuant (q, xs, phi'))
- #>> quantify_over_var (case q of
- AForall => forall_of
- | AExists => exists_of)
- (repair_atp_variable_name Char.toLower x)
- | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
- | AConn (c, [phi1, phi2]) =>
- do_formula (pos |> c = AImplies ? not) phi1
- ##>> do_formula pos phi2
- #>> (case c of
- AAnd => s_conj
- | AOr => s_disj
- | AImplies => s_imp
- | AIf => s_imp o swap
- | AIff => s_iff
- | ANotIff => s_not o s_iff)
- | AAtom tm => term_from_pred thy full_types tfrees pos tm
- | _ => raise FORMULA [phi]
- in repair_tvar_sorts (do_formula true phi Vartab.empty) end
-
-fun check_formula ctxt =
- Type.constraint HOLogic.boolT
- #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
-
-
-(**** Translation of TSTP files to Isar Proofs ****)
-
-fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
- | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
-
-fun decode_line full_types tfrees (Definition (name, phi1, phi2)) ctxt =
- let
- val thy = ProofContext.theory_of ctxt
- val t1 = prop_from_formula thy full_types tfrees phi1
- val vars = snd (strip_comb t1)
- val frees = map unvarify_term vars
- val unvarify_args = subst_atomic (vars ~~ frees)
- val t2 = prop_from_formula thy full_types tfrees phi2
- val (t1, t2) =
- HOLogic.eq_const HOLogic.typeT $ t1 $ t2
- |> unvarify_args |> uncombine_term |> check_formula ctxt
- |> HOLogic.dest_eq
- in
- (Definition (name, t1, t2),
- fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
- end
- | decode_line full_types tfrees (Inference (name, u, deps)) ctxt =
- let
- val thy = ProofContext.theory_of ctxt
- val t = u |> prop_from_formula thy full_types tfrees
- |> uncombine_term |> check_formula ctxt
- in
- (Inference (name, t, deps),
- fold Variable.declare_term (OldTerm.term_frees t) ctxt)
- end
-fun decode_lines ctxt full_types tfrees lines =
- fst (fold_map (decode_line full_types tfrees) lines ctxt)
-
-fun is_same_inference _ (Definition _) = false
- | is_same_inference t (Inference (_, t', _)) = t aconv t'
-
-(* No "real" literals means only type information (tfree_tcs, clsrel, or
- clsarity). *)
-val is_only_type_information = curry (op aconv) HOLogic.true_const
-
-fun replace_one_dependency (old, new) dep =
- if is_same_step (dep, old) then new else [dep]
-fun replace_dependencies_in_line _ (line as Definition _) = line
- | replace_dependencies_in_line p (Inference (name, t, deps)) =
- Inference (name, t, fold (union (op =) o replace_one_dependency p) deps [])
-
-(* Discard axioms; consolidate adjacent lines that prove the same formula, since
- they differ only in type information.*)
-fun add_line _ _ (line as Definition _) lines = line :: lines
- | add_line conjecture_shape axiom_names (Inference (name, t, [])) lines =
- (* No dependencies: axiom, conjecture, or (for Vampire) internal axioms or
- definitions. *)
- if is_axiom axiom_names name then
- (* Axioms are not proof lines. *)
- if is_only_type_information t then
- map (replace_dependencies_in_line (name, [])) lines
- (* Is there a repetition? If so, replace later line by earlier one. *)
- else case take_prefix (not o is_same_inference t) lines of
- (_, []) => lines (* no repetition of proof line *)
- | (pre, Inference (name', _, _) :: post) =>
- pre @ map (replace_dependencies_in_line (name', [name])) post
- else if is_conjecture conjecture_shape name then
- Inference (name, negate_term t, []) :: lines
- else
- map (replace_dependencies_in_line (name, [])) lines
- | add_line _ _ (Inference (name, t, deps)) lines =
- (* Type information will be deleted later; skip repetition test. *)
- if is_only_type_information t then
- Inference (name, t, deps) :: lines
- (* Is there a repetition? If so, replace later line by earlier one. *)
- else case take_prefix (not o is_same_inference t) lines of
- (* FIXME: Doesn't this code risk conflating proofs involving different
- types? *)
- (_, []) => Inference (name, t, deps) :: lines
- | (pre, Inference (name', t', _) :: post) =>
- Inference (name, t', deps) ::
- pre @ map (replace_dependencies_in_line (name', [name])) post
-
-(* Recursively delete empty lines (type information) from the proof. *)
-fun add_nontrivial_line (Inference (name, t, [])) lines =
- if is_only_type_information t then delete_dependency name lines
- else Inference (name, t, []) :: lines
- | add_nontrivial_line line lines = line :: lines
-and delete_dependency name lines =
- fold_rev add_nontrivial_line
- (map (replace_dependencies_in_line (name, [])) lines) []
-
-(* ATPs sometimes reuse free variable names in the strangest ways. Removing
- offending lines often does the trick. *)
-fun is_bad_free frees (Free x) = not (member (op =) frees x)
- | is_bad_free _ _ = false
-
-fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) =
- (j, line :: map (replace_dependencies_in_line (name, [])) lines)
- | add_desired_line isar_shrink_factor conjecture_shape axiom_names frees
- (Inference (name, t, deps)) (j, lines) =
- (j + 1,
- if is_axiom axiom_names name orelse
- is_conjecture conjecture_shape name orelse
- (* the last line must be kept *)
- j = 0 orelse
- (not (is_only_type_information t) andalso
- null (Term.add_tvars t []) andalso
- not (exists_subterm (is_bad_free frees) t) andalso
- length deps >= 2 andalso j mod isar_shrink_factor = 0 andalso
- (* kill next to last line, which usually results in a trivial step *)
- j <> 1) then
- Inference (name, t, deps) :: lines (* keep line *)
- else
- map (replace_dependencies_in_line (name, deps)) lines) (* drop line *)
-
-(** Isar proof construction and manipulation **)
-
-fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
- (union (op =) ls1 ls2, union (op =) ss1 ss2)
-
-type label = string * int
-type facts = label list * string list
-
-datatype isar_qualifier = Show | Then | Moreover | Ultimately
-
-datatype isar_step =
- Fix of (string * typ) list |
- Let of term * term |
- Assume of label * term |
- Have of isar_qualifier list * label * term * byline
-and byline =
- ByMetis of facts |
- CaseSplit of isar_step list list * facts
-
-fun smart_case_split [] facts = ByMetis facts
- | smart_case_split proofs facts = CaseSplit (proofs, facts)
-
-fun add_fact_from_dependency conjecture_shape axiom_names name =
- if is_axiom axiom_names name then
- apsnd (union (op =) (map fst (resolve_axiom axiom_names name)))
- else
- apfst (insert (op =) (raw_label_for_name conjecture_shape name))
-
-fun step_for_line _ _ _ (Definition (_, t1, t2)) = Let (t1, t2)
- | step_for_line conjecture_shape _ _ (Inference (name, t, [])) =
- Assume (raw_label_for_name conjecture_shape name, t)
- | step_for_line conjecture_shape axiom_names j (Inference (name, t, deps)) =
- Have (if j = 1 then [Show] else [],
- raw_label_for_name conjecture_shape name,
- fold_rev forall_of (map Var (Term.add_vars t [])) t,
- ByMetis (fold (add_fact_from_dependency conjecture_shape axiom_names)
- deps ([], [])))
-
-fun repair_name "$true" = "c_True"
- | repair_name "$false" = "c_False"
- | repair_name "$$e" = "c_equal" (* seen in Vampire proofs *)
- | repair_name "equal" = "c_equal" (* needed by SPASS? *)
- | repair_name s =
- if String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s then
- "c_equal" (* seen in Vampire proofs *)
- else
- s
-
-fun isar_proof_from_tstplike_proof pool ctxt full_types tfrees isar_shrink_factor
- tstplike_proof conjecture_shape axiom_names params frees =
- let
- val lines =
- tstplike_proof
- |> atp_proof_from_tstplike_string
- |> nasty_atp_proof pool
- |> map_term_names_in_atp_proof repair_name
- |> decode_lines ctxt full_types tfrees
- |> rpair [] |-> fold_rev (add_line conjecture_shape axiom_names)
- |> rpair [] |-> fold_rev add_nontrivial_line
- |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor
- conjecture_shape axiom_names frees)
- |> snd
- in
- (if null params then [] else [Fix params]) @
- map2 (step_for_line conjecture_shape axiom_names) (length lines downto 1)
- lines
- end
-
-(* When redirecting proofs, we keep information about the labels seen so far in
- the "backpatches" data structure. The first component indicates which facts
- should be associated with forthcoming proof steps. The second component is a
- pair ("assum_ls", "drop_ls"), where "assum_ls" are the labels that should
- become assumptions and "drop_ls" are the labels that should be dropped in a
- case split. *)
-type backpatches = (label * facts) list * (label list * label list)
-
-fun used_labels_of_step (Have (_, _, _, by)) =
- (case by of
- ByMetis (ls, _) => ls
- | CaseSplit (proofs, (ls, _)) =>
- fold (union (op =) o used_labels_of) proofs ls)
- | used_labels_of_step _ = []
-and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []
-
-fun new_labels_of_step (Fix _) = []
- | new_labels_of_step (Let _) = []
- | new_labels_of_step (Assume (l, _)) = [l]
- | new_labels_of_step (Have (_, l, _, _)) = [l]
-val new_labels_of = maps new_labels_of_step
-
-val join_proofs =
- let
- fun aux _ [] = NONE
- | aux proof_tail (proofs as (proof1 :: _)) =
- if exists null proofs then
- NONE
- else if forall (curry (op =) (hd proof1) o hd) (tl proofs) then
- aux (hd proof1 :: proof_tail) (map tl proofs)
- else case hd proof1 of
- Have ([], l, t, _) => (* FIXME: should we really ignore the "by"? *)
- if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t')
- | _ => false) (tl proofs) andalso
- not (exists (member (op =) (maps new_labels_of proofs))
- (used_labels_of proof_tail)) then
- SOME (l, t, map rev proofs, proof_tail)
- else
- NONE
- | _ => NONE
- in aux [] o map rev end
-
-fun case_split_qualifiers proofs =
- case length proofs of
- 0 => []
- | 1 => [Then]
- | _ => [Ultimately]
-
-fun redirect_proof hyp_ts concl_t proof =
- let
- (* The first pass outputs those steps that are independent of the negated
- conjecture. The second pass flips the proof by contradiction to obtain a
- direct proof, introducing case splits when an inference depends on
- several facts that depend on the negated conjecture. *)
- val concl_l = (conjecture_prefix, length hyp_ts)
- fun first_pass ([], contra) = ([], contra)
- | first_pass ((step as Fix _) :: proof, contra) =
- first_pass (proof, contra) |>> cons step
- | first_pass ((step as Let _) :: proof, contra) =
- first_pass (proof, contra) |>> cons step
- | first_pass ((step as Assume (l as (_, j), _)) :: proof, contra) =
- if l = concl_l then first_pass (proof, contra ||> cons step)
- else first_pass (proof, contra) |>> cons (Assume (l, nth hyp_ts j))
- | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
- let val step = Have (qs, l, t, ByMetis (ls, ss)) in
- if exists (member (op =) (fst contra)) ls then
- first_pass (proof, contra |>> cons l ||> cons step)
- else
- first_pass (proof, contra) |>> cons step
- end
- | first_pass _ = raise Fail "malformed proof"
- val (proof_top, (contra_ls, contra_proof)) =
- first_pass (proof, ([concl_l], []))
- val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst
- fun backpatch_labels patches ls =
- fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
- fun second_pass end_qs ([], assums, patches) =
- ([Have (end_qs, no_label, concl_t,
- ByMetis (backpatch_labels patches (map snd assums)))], patches)
- | second_pass end_qs (Assume (l, t) :: proof, assums, patches) =
- second_pass end_qs (proof, (t, l) :: assums, patches)
- | second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums,
- patches) =
- (if member (op =) (snd (snd patches)) l andalso
- not (member (op =) (fst (snd patches)) l) andalso
- not (AList.defined (op =) (fst patches) l) then
- second_pass end_qs (proof, assums, patches ||> apsnd (append ls))
- else case List.partition (member (op =) contra_ls) ls of
- ([contra_l], co_ls) =>
- if member (op =) qs Show then
- second_pass end_qs (proof, assums,
- patches |>> cons (contra_l, (co_ls, ss)))
- else
- second_pass end_qs
- (proof, assums,
- patches |>> cons (contra_l, (l :: co_ls, ss)))
- |>> cons (if member (op =) (fst (snd patches)) l then
- Assume (l, negate_term t)
- else
- Have (qs, l, negate_term t,
- ByMetis (backpatch_label patches l)))
- | (contra_ls as _ :: _, co_ls) =>
- let
- val proofs =
- map_filter
- (fn l =>
- if l = concl_l then
- NONE
- else
- let
- val drop_ls = filter (curry (op <>) l) contra_ls
- in
- second_pass []
- (proof, assums,
- patches ||> apfst (insert (op =) l)
- ||> apsnd (union (op =) drop_ls))
- |> fst |> SOME
- end) contra_ls
- val (assumes, facts) =
- if member (op =) (fst (snd patches)) l then
- ([Assume (l, negate_term t)], (l :: co_ls, ss))
- else
- ([], (co_ls, ss))
- in
- (case join_proofs proofs of
- SOME (l, t, proofs, proof_tail) =>
- Have (case_split_qualifiers proofs @
- (if null proof_tail then end_qs else []), l, t,
- smart_case_split proofs facts) :: proof_tail
- | NONE =>
- [Have (case_split_qualifiers proofs @ end_qs, no_label,
- concl_t, smart_case_split proofs facts)],
- patches)
- |>> append assumes
- end
- | _ => raise Fail "malformed proof")
- | second_pass _ _ = raise Fail "malformed proof"
- val proof_bottom =
- second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst
- in proof_top @ proof_bottom end
-
-(* FIXME: Still needed? Probably not. *)
-val kill_duplicate_assumptions_in_proof =
- let
- fun relabel_facts subst =
- apfst (map (fn l => AList.lookup (op =) subst l |> the_default l))
- fun do_step (step as Assume (l, t)) (proof, subst, assums) =
- (case AList.lookup (op aconv) assums t of
- SOME l' => (proof, (l, l') :: subst, assums)
- | NONE => (step :: proof, subst, (t, l) :: assums))
- | do_step (Have (qs, l, t, by)) (proof, subst, assums) =
- (Have (qs, l, t,
- case by of
- ByMetis facts => ByMetis (relabel_facts subst facts)
- | CaseSplit (proofs, facts) =>
- CaseSplit (map do_proof proofs, relabel_facts subst facts)) ::
- proof, subst, assums)
- | do_step step (proof, subst, assums) = (step :: proof, subst, assums)
- and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
- in do_proof end
-
-val then_chain_proof =
- let
- fun aux _ [] = []
- | aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof
- | aux l' (Have (qs, l, t, by) :: proof) =
- (case by of
- ByMetis (ls, ss) =>
- Have (if member (op =) ls l' then
- (Then :: qs, l, t,
- ByMetis (filter_out (curry (op =) l') ls, ss))
- else
- (qs, l, t, ByMetis (ls, ss)))
- | CaseSplit (proofs, facts) =>
- Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) ::
- aux l proof
- | aux _ (step :: proof) = step :: aux no_label proof
- in aux no_label end
-
-fun kill_useless_labels_in_proof proof =
- let
- val used_ls = used_labels_of proof
- fun do_label l = if member (op =) used_ls l then l else no_label
- fun do_step (Assume (l, t)) = Assume (do_label l, t)
- | do_step (Have (qs, l, t, by)) =
- Have (qs, do_label l, t,
- case by of
- CaseSplit (proofs, facts) =>
- CaseSplit (map (map do_step) proofs, facts)
- | _ => by)
- | do_step step = step
- in map do_step proof end
-
-fun prefix_for_depth n = replicate_string (n + 1)
-
-val relabel_proof =
- let
- fun aux _ _ _ [] = []
- | aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) =
- if l = no_label then
- Assume (l, t) :: aux subst depth (next_assum, next_fact) proof
- else
- let val l' = (prefix_for_depth depth assum_prefix, next_assum) in
- Assume (l', t) ::
- aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof
- end
- | aux subst depth (next_assum, next_fact) (Have (qs, l, t, by) :: proof) =
- let
- val (l', subst, next_fact) =
- if l = no_label then
- (l, subst, next_fact)
- else
- let
- val l' = (prefix_for_depth depth fact_prefix, next_fact)
- in (l', (l, l') :: subst, next_fact + 1) end
- val relabel_facts =
- apfst (maps (the_list o AList.lookup (op =) subst))
- val by =
- case by of
- ByMetis facts => ByMetis (relabel_facts facts)
- | CaseSplit (proofs, facts) =>
- CaseSplit (map (aux subst (depth + 1) (1, 1)) proofs,
- relabel_facts facts)
- in
- Have (qs, l', t, by) ::
- aux subst depth (next_assum, next_fact) proof
- end
- | aux subst depth nextp (step :: proof) =
- step :: aux subst depth nextp proof
- in aux [] 0 (1, 1) end
-
-fun string_for_proof ctxt0 full_types i n =
- let
- val ctxt = ctxt0
- |> Config.put show_free_types false
- |> Config.put show_types true
- fun fix_print_mode f x =
- Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
- (print_mode_value ())) f x
- fun do_indent ind = replicate_string (ind * indent_size) " "
- fun do_free (s, T) =
- maybe_quote s ^ " :: " ^
- maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
- fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
- fun do_have qs =
- (if member (op =) qs Moreover then "moreover " else "") ^
- (if member (op =) qs Ultimately then "ultimately " else "") ^
- (if member (op =) qs Then then
- if member (op =) qs Show then "thus" else "hence"
- else
- if member (op =) qs Show then "show" else "have")
- val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
- fun do_facts (ls, ss) =
- metis_command full_types 1 1
- (ls |> sort_distinct (prod_ord string_ord int_ord),
- ss |> sort_distinct string_ord)
- and do_step ind (Fix xs) =
- do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
- | do_step ind (Let (t1, t2)) =
- do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
- | do_step ind (Assume (l, t)) =
- do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
- | do_step ind (Have (qs, l, t, ByMetis facts)) =
- do_indent ind ^ do_have qs ^ " " ^
- do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n"
- | do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) =
- space_implode (do_indent ind ^ "moreover\n")
- (map (do_block ind) proofs) ^
- do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^
- do_facts facts ^ "\n"
- and do_steps prefix suffix ind steps =
- let val s = implode (map (do_step ind) steps) in
- replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
- String.extract (s, ind * indent_size,
- SOME (size s - ind * indent_size - 1)) ^
- suffix ^ "\n"
- end
- and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
- (* One-step proofs are pointless; better use the Metis one-liner
- directly. *)
- and do_proof [Have (_, _, _, ByMetis _)] = ""
- | do_proof proof =
- (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
- do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^
- (if n <> 1 then "next" else "qed")
- in do_proof end
-
-fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
- (other_params as (_, full_types, _, tstplike_proof,
- axiom_names, goal, i)) =
- let
- val (params, hyp_ts, concl_t) = strip_subgoal goal i
- val frees = fold Term.add_frees (concl_t :: hyp_ts) []
- val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
- val n = Logic.count_prems (prop_of goal)
- val (one_line_proof, lemma_names) = metis_proof_text other_params
- fun isar_proof_for () =
- case isar_proof_from_tstplike_proof pool ctxt full_types tfrees
- isar_shrink_factor tstplike_proof conjecture_shape axiom_names
- params frees
- |> redirect_proof hyp_ts concl_t
- |> kill_duplicate_assumptions_in_proof
- |> then_chain_proof
- |> kill_useless_labels_in_proof
- |> relabel_proof
- |> string_for_proof ctxt full_types i n of
- "" => "\nNo structured proof available."
- | proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
- val isar_proof =
- if debug then
- isar_proof_for ()
- else
- try isar_proof_for ()
- |> the_default "\nWarning: The Isar proof construction failed."
- in (one_line_proof ^ isar_proof, lemma_names) end
-
-fun proof_text isar_proof isar_params other_params =
- (if isar_proof then isar_proof_text isar_params else metis_proof_text)
- other_params
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Fri Oct 22 13:59:34 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,533 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_translate.ML
- Author: Fabian Immler, TU Muenchen
- Author: Makarius
- Author: Jasmin Blanchette, TU Muenchen
-
-Translation of HOL to FOL for Sledgehammer.
-*)
-
-signature SLEDGEHAMMER_TRANSLATE =
-sig
- type 'a problem = 'a ATP_Problem.problem
- type fol_formula
-
- val axiom_prefix : string
- val conjecture_prefix : string
- val prepare_axiom :
- Proof.context -> (string * 'a) * thm
- -> term * ((string * 'a) * fol_formula) option
- val prepare_problem :
- Proof.context -> bool -> bool -> bool -> bool -> term list -> term
- -> (term * ((string * 'a) * fol_formula) option) list
- -> string problem * string Symtab.table * int * (string * 'a) list vector
-end;
-
-structure Sledgehammer_Translate : SLEDGEHAMMER_TRANSLATE =
-struct
-
-open ATP_Problem
-open Metis_Translate
-open Sledgehammer_Util
-
-val axiom_prefix = "ax_"
-val conjecture_prefix = "conj_"
-val helper_prefix = "help_"
-val class_rel_clause_prefix = "clrel_";
-val arity_clause_prefix = "arity_"
-val tfree_prefix = "tfree_"
-
-(* Freshness almost guaranteed! *)
-val sledgehammer_weak_prefix = "Sledgehammer:"
-
-type fol_formula =
- {name: string,
- kind: kind,
- combformula: (name, combterm) formula,
- ctypes_sorts: typ list}
-
-fun mk_anot phi = AConn (ANot, [phi])
-fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
-fun mk_ahorn [] phi = phi
- | mk_ahorn (phi :: phis) psi =
- AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
-
-fun combformula_for_prop thy =
- let
- val do_term = combterm_from_term thy ~1
- fun do_quant bs q s T t' =
- let val s = Name.variant (map fst bs) s in
- do_formula ((s, T) :: bs) t'
- #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
- end
- and do_conn bs c t1 t2 =
- do_formula bs t1 ##>> do_formula bs t2
- #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))
- and do_formula bs t =
- case t of
- @{const Not} $ t1 =>
- do_formula bs t1 #>> (fn phi => AConn (ANot, [phi]))
- | Const (@{const_name All}, _) $ Abs (s, T, t') =>
- do_quant bs AForall s T t'
- | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
- do_quant bs AExists s T t'
- | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2
- | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2
- | @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2
- | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
- do_conn bs AIff t1 t2
- | _ => (fn ts => do_term bs (Envir.eta_contract t)
- |>> AAtom ||> union (op =) ts)
- in do_formula [] end
-
-val presimplify_term = prop_of o Meson.presimplify oo Skip_Proof.make_thm
-
-fun concealed_bound_name j = sledgehammer_weak_prefix ^ Int.toString j
-fun conceal_bounds Ts t =
- subst_bounds (map (Free o apfst concealed_bound_name)
- (0 upto length Ts - 1 ~~ Ts), t)
-fun reveal_bounds Ts =
- subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
- (0 upto length Ts - 1 ~~ Ts))
-
-(* Removes the lambdas from an equation of the form "t = (%x. u)".
- (Cf. "extensionalize_theorem" in "Meson_Clausify".) *)
-fun extensionalize_term t =
- let
- fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t'
- | aux j (t as Const (s, Type (_, [Type (_, [_, T']),
- Type (_, [_, res_T])]))
- $ t2 $ Abs (var_s, var_T, t')) =
- if s = @{const_name HOL.eq} orelse s = @{const_name "=="} then
- let val var_t = Var ((var_s, j), var_T) in
- Const (s, T' --> T' --> res_T)
- $ betapply (t2, var_t) $ subst_bound (var_t, t')
- |> aux (j + 1)
- end
- else
- t
- | aux _ t = t
- in aux (maxidx_of_term t + 1) t end
-
-fun introduce_combinators_in_term ctxt kind t =
- let val thy = ProofContext.theory_of ctxt in
- if Meson.is_fol_term thy t then
- t
- else
- let
- fun aux Ts t =
- case t of
- @{const Not} $ t1 => @{const Not} $ aux Ts t1
- | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
- t0 $ Abs (s, T, aux (T :: Ts) t')
- | (t0 as Const (@{const_name All}, _)) $ t1 =>
- aux Ts (t0 $ eta_expand Ts t1 1)
- | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
- t0 $ Abs (s, T, aux (T :: Ts) t')
- | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
- aux Ts (t0 $ eta_expand Ts t1 1)
- | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
- | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
- $ t1 $ t2 =>
- t0 $ aux Ts t1 $ aux Ts t2
- | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
- t
- else
- t |> conceal_bounds Ts
- |> Envir.eta_contract
- |> cterm_of thy
- |> Meson_Clausify.introduce_combinators_in_cterm
- |> prop_of |> Logic.dest_equals |> snd
- |> reveal_bounds Ts
- val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
- in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
- handle THM _ =>
- (* A type variable of sort "{}" will make abstraction fail. *)
- if kind = Conjecture then HOLogic.false_const
- else HOLogic.true_const
- end
-
-(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
- same in Sledgehammer to prevent the discovery of unreplable proofs. *)
-fun freeze_term t =
- let
- fun aux (t $ u) = aux t $ aux u
- | aux (Abs (s, T, t)) = Abs (s, T, aux t)
- | aux (Var ((s, i), T)) =
- Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
- | aux t = t
- in t |> exists_subterm is_Var t ? aux end
-
-(* "Object_Logic.atomize_term" isn't as powerful as it could be; for example,
- it leaves metaequalities over "prop"s alone. *)
-val atomize_term =
- let
- fun aux (@{const Trueprop} $ t1) = t1
- | aux (Const (@{const_name all}, _) $ Abs (s, T, t')) =
- HOLogic.all_const T $ Abs (s, T, aux t')
- | aux (@{const "==>"} $ t1 $ t2) = HOLogic.mk_imp (pairself aux (t1, t2))
- | aux (Const (@{const_name "=="}, Type (_, [@{typ prop}, _])) $ t1 $ t2) =
- HOLogic.eq_const HOLogic.boolT $ aux t1 $ aux t2
- | aux (Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2) =
- HOLogic.eq_const T $ t1 $ t2
- | aux _ = raise Fail "aux"
- in perhaps (try aux) end
-
-(* making axiom and conjecture formulas *)
-fun make_formula ctxt presimp name kind t =
- let
- val thy = ProofContext.theory_of ctxt
- val t = t |> Envir.beta_eta_contract
- |> transform_elim_term
- |> atomize_term
- val need_trueprop = (fastype_of t = HOLogic.boolT)
- val t = t |> need_trueprop ? HOLogic.mk_Trueprop
- |> extensionalize_term
- |> presimp ? presimplify_term thy
- |> perhaps (try (HOLogic.dest_Trueprop))
- |> introduce_combinators_in_term ctxt kind
- |> kind <> Axiom ? freeze_term
- val (combformula, ctypes_sorts) = combformula_for_prop thy t []
- in
- {name = name, combformula = combformula, kind = kind,
- ctypes_sorts = ctypes_sorts}
- end
-
-fun make_axiom ctxt presimp ((name, loc), th) =
- case make_formula ctxt presimp name Axiom (prop_of th) of
- {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => NONE
- | formula => SOME ((name, loc), formula)
-fun make_conjecture ctxt ts =
- let val last = length ts - 1 in
- map2 (fn j => make_formula ctxt true (Int.toString j)
- (if j = last then Conjecture else Hypothesis))
- (0 upto last) ts
- end
-
-(** Helper facts **)
-
-fun count_combterm (CombConst ((s, _), _, _)) =
- Symtab.map_entry s (Integer.add 1)
- | count_combterm (CombVar _) = I
- | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2]
-fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
- | count_combformula (AConn (_, phis)) = fold count_combformula phis
- | count_combformula (AAtom tm) = count_combterm tm
-fun count_fol_formula ({combformula, ...} : fol_formula) =
- count_combformula combformula
-
-val optional_helpers =
- [(["c_COMBI"], @{thms Meson.COMBI_def}),
- (["c_COMBK"], @{thms Meson.COMBK_def}),
- (["c_COMBB"], @{thms Meson.COMBB_def}),
- (["c_COMBC"], @{thms Meson.COMBC_def}),
- (["c_COMBS"], @{thms Meson.COMBS_def})]
-val optional_typed_helpers =
- [(["c_True", "c_False", "c_If"], @{thms True_or_False}),
- (["c_If"], @{thms if_True if_False})]
-val mandatory_helpers = @{thms Metis.fequal_def}
-
-val init_counters =
- [optional_helpers, optional_typed_helpers] |> maps (maps fst)
- |> sort_distinct string_ord |> map (rpair 0) |> Symtab.make
-
-fun get_helper_facts ctxt is_FO full_types conjectures axioms =
- let
- val ct = fold (fold count_fol_formula) [conjectures, axioms] init_counters
- fun is_needed c = the (Symtab.lookup ct c) > 0
- fun baptize th = ((Thm.get_name_hint th, false), th)
- in
- (optional_helpers
- |> full_types ? append optional_typed_helpers
- |> maps (fn (ss, ths) =>
- if exists is_needed ss then map baptize ths else [])) @
- (if is_FO then [] else map baptize mandatory_helpers)
- |> map_filter (Option.map snd o make_axiom ctxt false)
- end
-
-fun prepare_axiom ctxt (ax as (_, th)) = (prop_of th, make_axiom ctxt true ax)
-
-fun prepare_formulas ctxt full_types hyp_ts concl_t axioms =
- let
- val thy = ProofContext.theory_of ctxt
- val (axiom_ts, prepared_axioms) = ListPair.unzip axioms
- (* Remove existing axioms from the conjecture, as this can dramatically
- boost an ATP's performance (for some reason). *)
- val hyp_ts = hyp_ts |> filter_out (member (op aconv) axiom_ts)
- val goal_t = Logic.list_implies (hyp_ts, concl_t)
- val is_FO = Meson.is_fol_term thy goal_t
- val subs = tfree_classes_of_terms [goal_t]
- val supers = tvar_classes_of_terms axiom_ts
- val tycons = type_consts_of_terms thy (goal_t :: axiom_ts)
- (* TFrees in the conjecture; TVars in the axioms *)
- val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t])
- val (axiom_names, axioms) = ListPair.unzip (map_filter I prepared_axioms)
- val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
- val (supers', arity_clauses) = make_arity_clauses thy tycons supers
- val class_rel_clauses = make_class_rel_clauses thy subs supers'
- in
- (axiom_names |> map single |> Vector.fromList,
- (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses))
- end
-
-fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
-
-fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])
- | fo_term_for_combtyp (CombTFree name) = ATerm (name, [])
- | fo_term_for_combtyp (CombType (name, tys)) =
- ATerm (name, map fo_term_for_combtyp tys)
-
-fun fo_literal_for_type_literal (TyLitVar (class, name)) =
- (true, ATerm (class, [ATerm (name, [])]))
- | fo_literal_for_type_literal (TyLitFree (class, name)) =
- (true, ATerm (class, [ATerm (name, [])]))
-
-fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
-
-fun fo_term_for_combterm full_types =
- let
- fun aux top_level u =
- let
- val (head, args) = strip_combterm_comb u
- val (x, ty_args) =
- case head of
- CombConst (name as (s, s'), _, ty_args) =>
- let val ty_args = if full_types then [] else ty_args in
- if s = "equal" then
- if top_level andalso length args = 2 then (name, [])
- else (("c_fequal", @{const_name Metis.fequal}), ty_args)
- else if top_level then
- case s of
- "c_False" => (("$false", s'), [])
- | "c_True" => (("$true", s'), [])
- | _ => (name, ty_args)
- else
- (name, ty_args)
- end
- | CombVar (name, _) => (name, [])
- | CombApp _ => raise Fail "impossible \"CombApp\""
- val t = ATerm (x, map fo_term_for_combtyp ty_args @
- map (aux false) args)
- in
- if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t
- end
- in aux true end
-
-fun formula_for_combformula full_types =
- let
- fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
- | aux (AConn (c, phis)) = AConn (c, map aux phis)
- | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm)
- in aux end
-
-fun formula_for_axiom full_types
- ({combformula, ctypes_sorts, ...} : fol_formula) =
- mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
- (type_literals_for_types ctypes_sorts))
- (formula_for_combformula full_types combformula)
-
-fun problem_line_for_fact prefix full_types (formula as {name, kind, ...}) =
- Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula)
-
-fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
- superclass, ...}) =
- let val ty_arg = ATerm (("T", "T"), []) in
- Fof (class_rel_clause_prefix ^ ascii_of name, Axiom,
- AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
- AAtom (ATerm (superclass, [ty_arg]))]))
- end
-
-fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
- (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
- | fo_literal_for_arity_literal (TVarLit (c, sort)) =
- (false, ATerm (c, [ATerm (sort, [])]))
-
-fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits,
- ...}) =
- Fof (arity_clause_prefix ^ ascii_of name, Axiom,
- mk_ahorn (map (formula_for_fo_literal o apfst not
- o fo_literal_for_arity_literal) premLits)
- (formula_for_fo_literal
- (fo_literal_for_arity_literal conclLit)))
-
-fun problem_line_for_conjecture full_types
- ({name, kind, combformula, ...} : fol_formula) =
- Fof (conjecture_prefix ^ name, kind,
- formula_for_combformula full_types combformula)
-
-fun free_type_literals_for_conjecture ({ctypes_sorts, ...} : fol_formula) =
- map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
-
-fun problem_line_for_free_type j lit =
- Fof (tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit)
-fun problem_lines_for_free_types conjectures =
- let
- val litss = map free_type_literals_for_conjecture conjectures
- val lits = fold (union (op =)) litss []
- in map2 problem_line_for_free_type (0 upto length lits - 1) lits end
-
-(** "hBOOL" and "hAPP" **)
-
-type const_info = {min_arity: int, max_arity: int, sub_level: bool}
-
-fun consider_term top_level (ATerm ((s, _), ts)) =
- (if is_atp_variable s then
- I
- else
- let val n = length ts in
- Symtab.map_default
- (s, {min_arity = n, max_arity = 0, sub_level = false})
- (fn {min_arity, max_arity, sub_level} =>
- {min_arity = Int.min (n, min_arity),
- max_arity = Int.max (n, max_arity),
- sub_level = sub_level orelse not top_level})
- end)
- #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
-fun consider_formula (AQuant (_, _, phi)) = consider_formula phi
- | consider_formula (AConn (_, phis)) = fold consider_formula phis
- | consider_formula (AAtom tm) = consider_term true tm
-
-fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi
-fun consider_problem problem = fold (fold consider_problem_line o snd) problem
-
-fun const_table_for_problem explicit_apply problem =
- if explicit_apply then NONE
- else SOME (Symtab.empty |> consider_problem problem)
-
-fun min_arity_of thy full_types NONE s =
- (if s = "equal" orelse s = type_wrapper_name orelse
- String.isPrefix type_const_prefix s orelse
- String.isPrefix class_prefix s then
- 16383 (* large number *)
- else if full_types then
- 0
- else case strip_prefix_and_unascii const_prefix s of
- SOME s' => num_type_args thy (invert_const s')
- | NONE => 0)
- | min_arity_of _ _ (SOME the_const_tab) s =
- case Symtab.lookup the_const_tab s of
- SOME ({min_arity, ...} : const_info) => min_arity
- | NONE => 0
-
-fun full_type_of (ATerm ((s, _), [ty, _])) =
- if s = type_wrapper_name then ty else raise Fail "expected type wrapper"
- | full_type_of _ = raise Fail "expected type wrapper"
-
-fun list_hAPP_rev _ t1 [] = t1
- | list_hAPP_rev NONE t1 (t2 :: ts2) =
- ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])
- | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
- let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
- [full_type_of t2, ty]) in
- ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
- end
-
-fun repair_applications_in_term thy full_types const_tab =
- let
- fun aux opt_ty (ATerm (name as (s, _), ts)) =
- if s = type_wrapper_name then
- case ts of
- [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])
- | _ => raise Fail "malformed type wrapper"
- else
- let
- val ts = map (aux NONE) ts
- val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts
- in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
- in aux NONE end
-
-fun boolify t = ATerm (`I "hBOOL", [t])
-
-(* True if the constant ever appears outside of the top-level position in
- literals, or if it appears with different arities (e.g., because of different
- type instantiations). If false, the constant always receives all of its
- arguments and is used as a predicate. *)
-fun is_predicate NONE s =
- s = "equal" orelse s = "$false" orelse s = "$true" orelse
- String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s
- | is_predicate (SOME the_const_tab) s =
- case Symtab.lookup the_const_tab s of
- SOME {min_arity, max_arity, sub_level} =>
- not sub_level andalso min_arity = max_arity
- | NONE => false
-
-fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) =
- if s = type_wrapper_name then
- case ts of
- [_, t' as ATerm ((s', _), _)] =>
- if is_predicate const_tab s' then t' else boolify t
- | _ => raise Fail "malformed type wrapper"
- else
- t |> not (is_predicate const_tab s) ? boolify
-
-fun close_universally phi =
- let
- fun term_vars bounds (ATerm (name as (s, _), tms)) =
- (is_atp_variable s andalso not (member (op =) bounds name))
- ? insert (op =) name
- #> fold (term_vars bounds) tms
- fun formula_vars bounds (AQuant (_, xs, phi)) =
- formula_vars (xs @ bounds) phi
- | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
- | formula_vars bounds (AAtom tm) = term_vars bounds tm
- in
- case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)
- end
-
-fun repair_formula thy explicit_forall full_types const_tab =
- let
- fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
- | aux (AConn (c, phis)) = AConn (c, map aux phis)
- | aux (AAtom tm) =
- AAtom (tm |> repair_applications_in_term thy full_types const_tab
- |> repair_predicates_in_term const_tab)
- in aux #> explicit_forall ? close_universally end
-
-fun repair_problem_line thy explicit_forall full_types const_tab
- (Fof (ident, kind, phi)) =
- Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi)
-fun repair_problem_with_const_table thy =
- map o apsnd o map ooo repair_problem_line thy
-
-fun repair_problem thy explicit_forall full_types explicit_apply problem =
- repair_problem_with_const_table thy explicit_forall full_types
- (const_table_for_problem explicit_apply problem) problem
-
-fun prepare_problem ctxt readable_names explicit_forall full_types
- explicit_apply hyp_ts concl_t axioms =
- let
- val thy = ProofContext.theory_of ctxt
- val (axiom_names, (conjectures, axioms, helper_facts, class_rel_clauses,
- arity_clauses)) =
- prepare_formulas ctxt full_types hyp_ts concl_t axioms
- val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms
- val helper_lines =
- map (problem_line_for_fact helper_prefix full_types) helper_facts
- val conjecture_lines =
- map (problem_line_for_conjecture full_types) conjectures
- val tfree_lines = problem_lines_for_free_types conjectures
- val class_rel_lines =
- map problem_line_for_class_rel_clause class_rel_clauses
- val arity_lines = map problem_line_for_arity_clause arity_clauses
- (* Reordering these might or might not confuse the proof reconstruction
- code or the SPASS Flotter hack. *)
- val problem =
- [("Relevant facts", axiom_lines),
- ("Class relationships", class_rel_lines),
- ("Arity declarations", arity_lines),
- ("Helper facts", helper_lines),
- ("Conjectures", conjecture_lines),
- ("Type variables", tfree_lines)]
- |> repair_problem thy explicit_forall full_types explicit_apply
- val (problem, pool) = nice_atp_problem readable_names problem
- val conjecture_offset =
- length axiom_lines + length class_rel_lines + length arity_lines
- + length helper_lines
- in
- (problem,
- case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
- conjecture_offset, axiom_names)
- end
-
-end;