--- a/doc-src/IsarRef/Thy/Generic.thy Tue Aug 09 08:07:22 2011 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy Tue Aug 09 18:52:18 2011 +0200
@@ -201,7 +201,7 @@
@{rail "
@@{method subst} ('(' 'asm' ')')? \\ ('(' (@{syntax nat}+) ')')? @{syntax thmref}
;
- @@{method split} ('(' 'asm' ')')? @{syntax thmrefs}
+ @@{method split} @{syntax thmrefs}
"}
These methods provide low-level facilities for equational reasoning
@@ -245,12 +245,13 @@
t"} where @{text x} is a free or bound variable.
\item @{method split}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} performs single-step case
- splitting using the given rules. By default, splitting is performed
- in the conclusion of a goal; the @{text "(asm)"} option indicates to
- operate on assumptions instead.
+ splitting using the given rules. Splitting is performed in the
+ conclusion or some assumption of the subgoal, depending of the
+ structure of the rule.
Note that the @{method simp} method already involves repeated
- application of split rules as declared in the current context.
+ application of split rules as declared in the current context, using
+ @{attribute split}, for example.
\end{description}
*}
--- a/doc-src/IsarRef/Thy/document/Generic.tex Tue Aug 09 08:07:22 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Tue Aug 09 18:52:18 2011 +0200
@@ -336,14 +336,8 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.thmref}{\mbox{\isa{thmref}}}}[]
\rail@end
-\rail@begin{2}{}
+\rail@begin{1}{}
\rail@term{\hyperlink{method.split}{\mbox{\isa{split}}}}[]
-\rail@bar
-\rail@nextbar{1}
-\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
-\rail@term{\isa{asm}}[]
-\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
-\rail@endbar
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
\rail@end
\end{railoutput}
@@ -388,12 +382,13 @@
assumption; this only works for equations of the form \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequote}}} where \isa{x} is a free or bound variable.
\item \hyperlink{method.split}{\mbox{\isa{split}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}} performs single-step case
- splitting using the given rules. By default, splitting is performed
- in the conclusion of a goal; the \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}asm{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} option indicates to
- operate on assumptions instead.
+ splitting using the given rules. Splitting is performed in the
+ conclusion or some assumption of the subgoal, depending of the
+ structure of the rule.
Note that the \hyperlink{method.simp}{\mbox{\isa{simp}}} method already involves repeated
- application of split rules as declared in the current context.
+ application of split rules as declared in the current context, using
+ \hyperlink{attribute.split}{\mbox{\isa{split}}}, for example.
\end{description}%
\end{isamarkuptext}%
--- a/doc-src/Sledgehammer/sledgehammer.tex Tue Aug 09 08:07:22 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Tue Aug 09 18:52:18 2011 +0200
@@ -85,15 +85,14 @@
Sledgehammer is a tool that applies automatic theorem provers (ATPs)
and satisfiability-modulo-theories (SMT) solvers on the current goal. The
-supported ATPs are E \cite{schulz-2002}, LEO-II \cite{leo2}, Satallax
-\cite{satallax}, SInE-E \cite{sine}, SNARK \cite{snark}, SPASS
-\cite{weidenbach-et-al-2009}, ToFoF-E \cite{tofof}, Vampire
-\cite{riazanov-voronkov-2002}, and Waldmeister \cite{waldmeister}. The ATPs are
-run either locally or remotely via the System\-On\-TPTP web service
-\cite{sutcliffe-2000}. In addition to the ATPs, the SMT solvers Z3 \cite{z3} is
-used by default, and you can tell Sledgehammer to try CVC3 \cite{cvc3} and Yices
-\cite{yices} as well; these are run either locally or on a server at the TU
-M\"unchen.
+supported ATPs are E \cite{schulz-2002}, E-SInE \cite{sine}, E-ToFoF
+\cite{tofof}, LEO-II \cite{leo2}, Satallax \cite{satallax}, SNARK \cite{snark},
+SPASS \cite{weidenbach-et-al-2009}, Vampire \cite{riazanov-voronkov-2002}, and
+Waldmeister \cite{waldmeister}. The ATPs are run either locally or remotely via
+the System\-On\-TPTP web service \cite{sutcliffe-2000}. In addition to the ATPs,
+the SMT solvers Z3 \cite{z3} is used by default, and you can tell Sledgehammer
+to try CVC3 \cite{cvc3} and Yices \cite{yices} as well; these are run either
+locally or on a server at the TU M\"unchen.
The problem passed to the automatic provers consists of your current goal
together with a heuristic selection of hundreds of facts (theorems) from the
@@ -141,10 +140,10 @@
\subsection{Installing ATPs}
-Currently, E, SPASS, and Vampire can be run locally; in addition, E, Vampire,
-LEO-II, Satallax, SInE-E, SNARK, ToFoF-E, and Waldmeister are available remotely
-via System\-On\-TPTP \cite{sutcliffe-2000}. If you want better performance, you
-should at least install E and SPASS locally.
+Currently, E, LEO-II, Satallax, SPASS, and Vampire can be run locally; in
+addition, E, E-SInE, E-ToFoF, LEO-II, Satallax, SNARK, Waldmeister, and Vampire
+are available remotely via System\-On\-TPTP \cite{sutcliffe-2000}. If you want
+better performance, you should at least install E and SPASS locally.
There are three main ways to install ATPs on your machine:
@@ -266,7 +265,7 @@
$[a] = [b] \,\Longrightarrow\, a = b$ \\
Try this: \textbf{by} (\textit{metis hd.simps}) (15 ms). \\[3\smallskipamount]
%
-Sledgehammer: ``\textit{remote\_sine\_e}'' on goal \\
+Sledgehammer: ``\textit{remote\_e\_sine}'' on goal \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms). \\[3\smallskipamount]
%
@@ -275,7 +274,7 @@
Try this: \textbf{by} (\textit{metis list.inject}) (20 ms).
\postw
-Sledgehammer ran E, SInE-E, SPASS, Vampire, Waldmeister, and Z3 in parallel.
+Sledgehammer ran E, E-SInE, SPASS, Vampire, Waldmeister, and Z3 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. Waldmeister is run only for unit equational problems,
@@ -525,7 +524,7 @@
it took to find it or replay it).
In addition, some provers (notably CVC3, Satallax, and Yices) do not provide
-proofs or sometimes provide incomplete proofs. The minimizer is then invoked to
+proofs or sometimes produce incomplete proofs. The minimizer is then invoked to
find out which facts are actually needed from the (large) set of facts that was
initinally given to the prover. Finally, if a prover returns a proof with lots
of facts, the minimizer is invoked automatically since Metis would be unlikely
@@ -723,6 +722,23 @@
executable, or install the prebuilt E package from Isabelle's download page. See
\S\ref{installation} for details.
+\item[$\bullet$] \textbf{\textit{leo2}:} LEO-II is an automatic
+higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
+with support for the TPTP higher-order syntax (THF).
+
+\item[$\bullet$] \textbf{\textit{metis}:} Although it is much less powerful than
+the external provers, Metis itself can be used for proof search.
+
+\item[$\bullet$] \textbf{\textit{metis\_full\_types}:} Fully typed version of
+Metis, corresponding to \textit{metis} (\textit{full\_types}).
+
+\item[$\bullet$] \textbf{\textit{metis\_no\_types}:} Untyped version of Metis,
+corresponding to \textit{metis} (\textit{no\_types}).
+
+\item[$\bullet$] \textbf{\textit{satallax}:} Satallax is an automatic
+higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with
+support for the TPTP higher-order syntax (THF).
+
\item[$\bullet$] \textbf{\textit{spass}:} SPASS is a first-order resolution
prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}.
To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory
@@ -730,17 +746,17 @@
package from Isabelle's download page. Sledgehammer requires version 3.5 or
above. See \S\ref{installation} for details.
-\item[$\bullet$] \textbf{\textit{yices}:} Yices is an SMT solver developed at
-SRI \cite{yices}. To use Yices, set the environment variable
-\texttt{YICES\_SOLVER} to the complete path of the executable, including the
-file name. Sledgehammer has been tested with version 1.0.
-
\item[$\bullet$] \textbf{\textit{vampire}:} Vampire is a first-order resolution
prover developed by Andrei Voronkov and his colleagues
\cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire}
executable. Sledgehammer has been tested with versions 11, 0.6, and 1.0.
+\item[$\bullet$] \textbf{\textit{yices}:} Yices is an SMT solver developed at
+SRI \cite{yices}. To use Yices, set the environment variable
+\texttt{YICES\_SOLVER} to the complete path of the executable, including the
+file name. Sledgehammer has been tested with version 1.0.
+
\item[$\bullet$] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
Microsoft Research \cite{z3}. To use Z3, set the environment variable
\texttt{Z3\_SOLVER} to the complete path of the executable, including the file
@@ -750,15 +766,6 @@
\item[$\bullet$] \textbf{\textit{z3\_atp}:} This version of Z3 pretends to be an
ATP, exploiting Z3's undocumented support for the TPTP format. It is included
for experimental purposes. It requires version 2.18 or above.
-
-\item[$\bullet$] \textbf{\textit{metis}:} Although it is much less powerful than
-the external provers, Metis itself can be used for proof search.
-
-\item[$\bullet$] \textbf{\textit{metis\_full\_types}:} Fully typed version of
-Metis, corresponding to \textit{metis} (\textit{full\_types}).
-
-\item[$\bullet$] \textbf{\textit{metis\_no\_types}:} Untyped version of Metis,
-corresponding to \textit{metis} (\textit{no\_types}).
\end{enum}
In addition, the following remote provers are supported:
@@ -771,32 +778,26 @@
\item[$\bullet$] \textbf{\textit{remote\_e}:} The remote version of E runs
on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
-\item[$\bullet$] \textbf{\textit{remote\_leo2}:} LEO-II is an automatic
-higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2},
-with support for the TPTP higher-order syntax (THF). The remote version of
-LEO-II runs on Geoff Sutcliffe's Miami servers. In the current setup, the
-problems given to LEO-II are only mildly higher-order.
-
-\item[$\bullet$] \textbf{\textit{remote\_satallax}:} Satallax is an automatic
-higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with
-support for the TPTP higher-order syntax (THF). The remote version of Satallax
-runs on Geoff Sutcliffe's Miami servers. In the current setup, the problems
-given to Satallax are only mildly higher-order.
-
-\item[$\bullet$] \textbf{\textit{remote\_sine\_e}:} SInE-E is a metaprover
+\item[$\bullet$] \textbf{\textit{remote\_e\_sine}:} E-SInE is a metaprover
developed by Kry\v stof Hoder \cite{sine} based on E. The remote version of
SInE runs on Geoff Sutcliffe's Miami servers.
+\item[$\bullet$] \textbf{\textit{remote\_e\_tofof}:} E-ToFoF is a metaprover
+developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
+servers. This ATP supports the TPTP many-typed first-order format (TFF). The
+remote version of E-ToFoF runs on Geoff Sutcliffe's Miami servers.
+
+\item[$\bullet$] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II
+runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
+
+\item[$\bullet$] \textbf{\textit{remote\_satallax}:} The remote version of
+Satallax runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
+
\item[$\bullet$] \textbf{\textit{remote\_snark}:} SNARK is a first-order
resolution prover developed by Stickel et al.\ \cite{snark}. It supports the
TPTP many-typed first-order format (TFF). The remote version of SNARK runs on
Geoff Sutcliffe's Miami servers.
-\item[$\bullet$] \textbf{\textit{remote\_tofof\_e}:} ToFoF-E is a metaprover
-developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami
-servers. This ATP supports the TPTP many-typed first-order format (TFF). The
-remote version of ToFoF-E runs on Geoff Sutcliffe's Miami servers.
-
\item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of
Vampire runs on Geoff Sutcliffe's Miami servers. Version 9 is used.
@@ -814,12 +815,12 @@
as an ATP'' runs on Geoff Sutcliffe's Miami servers.
\end{enum}
-By default, Sledgehammer will run E, SPASS, Vampire, SInE-E, and Z3 (or whatever
-the SMT module's \textit{smt\_solver} configuration option is set to) 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.
+By default, Sledgehammer will run E, E-SInE, SPASS, Vampire, Z3 (or whatever
+the SMT module's \textit{smt\_solver} configuration option is set to), and (if
+appropriate) Waldmeister 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 provers in parallel, although it could slow
down your machine. Running E, SPASS, and Vampire for 5~seconds yields a similar
--- a/doc-src/manual.bib Tue Aug 09 08:07:22 2011 +0200
+++ b/doc-src/manual.bib Tue Aug 09 18:52:18 2011 +0200
@@ -140,7 +140,7 @@
%B
-@inproceedings{satallax,
+@inproceedings{backes-brown-2010,
title = "Analytic Tableaux for Higher-Order Logic with Choice",
author = "Julian Backes and Chad E. Brown",
booktitle={Automated Reasoning: IJCAR 2010},
@@ -335,6 +335,17 @@
publisher = {Academic Press},
year = 1988}
+@inproceedings{satallax,
+ author = "Chad E. Brown",
+ title = "Reducing Higher-Order Theorem Proving to a Sequence of {SAT} Problems",
+ booktitle = {Automated Deduction --- CADE-23},
+ publisher = Springer,
+ series = LNCS,
+ volume = 6803,
+ pages = "147--161",
+ editor = "Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans",
+ year = 2011}
+
@Article{debruijn72,
author = {N. G. de Bruijn},
title = {Lambda Calculus Notation with Nameless Dummies,
@@ -686,9 +697,10 @@
booktitle = {Automated Deduction --- CADE-23},
publisher = Springer,
series = LNCS,
+ volume = 6803,
+ pages = "299--314",
editor = "Nikolaj Bj{\o}rner and Viorica Sofronie-Stokkermans",
- year = 2011,
- note = "To appear."}
+ year = 2011}
@book{Hudak-Haskell,author={Paul Hudak},
title={The Haskell School of Expression},publisher=CUP,year=2000}
--- a/src/HOL/ATP.thy Tue Aug 09 08:07:22 2011 +0200
+++ b/src/HOL/ATP.thy Tue Aug 09 18:52:18 2011 +0200
@@ -7,7 +7,8 @@
theory ATP
imports Meson
-uses "Tools/monomorph.ML"
+uses "Tools/lambda_lifting.ML"
+ "Tools/monomorph.ML"
"Tools/ATP/atp_util.ML"
"Tools/ATP/atp_problem.ML"
"Tools/ATP/atp_proof.ML"
--- a/src/HOL/IsaMakefile Tue Aug 09 08:07:22 2011 +0200
+++ b/src/HOL/IsaMakefile Tue Aug 09 18:52:18 2011 +0200
@@ -244,7 +244,9 @@
Tools/inductive_codegen.ML \
Tools/inductive_realizer.ML \
Tools/inductive_set.ML \
+ Tools/lambda_lifting.ML \
Tools/lin_arith.ML \
+ Tools/monomorph.ML \
Tools/nat_arith.ML \
Tools/primrec.ML \
Tools/prop_logic.ML \
@@ -309,10 +311,8 @@
Tools/code_evaluation.ML \
Tools/groebner.ML \
Tools/int_arith.ML \
- Tools/lambda_lifting.ML \
Tools/list_code.ML \
Tools/list_to_set_comprehension.ML \
- Tools/monomorph.ML \
Tools/nat_numeral_simprocs.ML \
Tools/Nitpick/kodkod.ML \
Tools/Nitpick/kodkod_sat.ML \
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Aug 09 08:07:22 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Aug 09 18:52:18 2011 +0200
@@ -9,11 +9,11 @@
val prover_timeoutK = "prover_timeout"
val keepK = "keep"
val type_encK = "type_enc"
+val soundK = "sound"
val slicingK = "slicing"
val lambda_translationK = "lambda_translation"
val e_weight_methodK = "e_weight_method"
-val spass_force_sosK = "spass_force_sos"
-val vampire_force_sosK = "vampire_force_sos"
+val force_sosK = "force_sos"
val max_relevantK = "max_relevant"
val minimizeK = "minimize"
val minimize_timeoutK = "minimize_timeout"
@@ -213,6 +213,8 @@
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns)) m
+val str0 = string_of_int o the_default 0
+
local
val str = string_of_int
@@ -242,13 +244,9 @@
str3 (avg_time time_prover_fail (calls - success)))
)
-
fun str_of_pos (pos, triv) =
- let val str0 = string_of_int o the_default 0
- in
- str0 (Position.line_of pos) (* ^ ":" ^ str0 (Position.offset_of pos) *) ^
- (if triv then "[T]" else "")
- end
+ str0 (Position.line_of pos) (* ^ ":" ^ str0 (Position.offset_of pos) *) ^
+ (if triv then "[T]" else "")
fun log_re_data log tag sh_calls (re_calls, re_success, re_nontriv_calls,
re_nontriv_success, re_proofs, re_time, re_timeout,
@@ -354,35 +352,36 @@
SH_FAIL of int * int |
SH_ERROR
-fun run_sh prover_name prover type_enc max_relevant slicing lambda_translation
- e_weight_method spass_force_sos vampire_force_sos hard_timeout timeout dir
- st =
+fun run_sh prover_name prover type_enc sound max_relevant slicing
+ lambda_translation e_weight_method force_sos hard_timeout timeout dir
+ pos st =
let
val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
val i = 1
- fun change_dir (SOME dir) =
+ fun set_file_name (SOME dir) =
Config.put Sledgehammer_Provers.dest_dir dir
+ #> Config.put Sledgehammer_Provers.problem_prefix
+ ("prob_" ^ str0 (Position.line_of pos))
#> Config.put SMT_Config.debug_files
(dir ^ "/" ^ Name.desymbolize false (ATP_Util.timestamp ()) ^ "_"
^ serial_string ())
- | change_dir NONE = I
+ | set_file_name NONE = I
val st' =
st |> Proof.map_context
- (change_dir dir
+ (set_file_name dir
#> (Option.map (Config.put
Sledgehammer_Provers.atp_lambda_translation)
lambda_translation |> the_default I)
#> (Option.map (Config.put ATP_Systems.e_weight_method)
e_weight_method |> the_default I)
- #> (Option.map (Config.put ATP_Systems.spass_force_sos)
- spass_force_sos |> the_default I)
- #> (Option.map (Config.put ATP_Systems.vampire_force_sos)
- vampire_force_sos |> the_default I)
+ #> (Option.map (Config.put ATP_Systems.force_sos)
+ force_sos |> the_default I)
#> Config.put Sledgehammer_Provers.measure_run_time true)
val params as {relevance_thresholds, max_relevant, slicing, ...} =
Sledgehammer_Isar.default_params ctxt
[("verbose", "true"),
("type_enc", type_enc),
+ ("sound", sound),
("max_relevant", max_relevant),
("slicing", slicing),
("timeout", string_of_int timeout)]
@@ -451,20 +450,20 @@
in
-fun run_sledgehammer trivial args reconstructor named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
+fun run_sledgehammer trivial args reconstructor named_thms id
+ ({pre=st, log, pos, ...}: Mirabelle.run_args) =
let
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_prover (Proof.context_of st) args
val type_enc = AList.lookup (op =) args type_encK |> the_default "smart"
+ val sound = AList.lookup (op =) args soundK |> the_default "false"
val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"
val slicing = AList.lookup (op =) args slicingK |> the_default "true"
val lambda_translation = AList.lookup (op =) args lambda_translationK
val e_weight_method = AList.lookup (op =) args e_weight_methodK
- val spass_force_sos = AList.lookup (op =) args spass_force_sosK
- |> Option.map (curry (op <>) "false")
- val vampire_force_sos = AList.lookup (op =) args vampire_force_sosK
+ val force_sos = AList.lookup (op =) args force_sosK
|> Option.map (curry (op <>) "false")
val dir = AList.lookup (op =) args keepK
val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
@@ -472,9 +471,9 @@
minimizer has a chance to do its magic *)
val hard_timeout = SOME (2 * timeout)
val (msg, result) =
- run_sh prover_name prover type_enc max_relevant slicing lambda_translation
- e_weight_method spass_force_sos vampire_force_sos hard_timeout timeout
- dir st
+ run_sh prover_name prover type_enc sound max_relevant slicing
+ lambda_translation e_weight_method force_sos hard_timeout timeout dir
+ pos st
in
case result of
SH_OK (time_isa, time_prover, names) =>
@@ -511,6 +510,7 @@
val n0 = length (these (!named_thms))
val (prover_name, _) = get_prover ctxt args
val type_enc = AList.lookup (op =) args type_encK |> the_default "smart"
+ val sound = AList.lookup (op =) args soundK |> the_default "false"
val timeout =
AList.lookup (op =) args minimize_timeoutK
|> Option.map (fst o read_int o raw_explode) (* FIXME Symbol.explode (?) *)
@@ -519,6 +519,7 @@
[("provers", prover_name),
("verbose", "true"),
("type_enc", type_enc),
+ ("sound", sound),
("timeout", string_of_int timeout)]
val minimize =
Sledgehammer_Minimize.minimize_facts prover_name params
--- a/src/HOL/SMT.thy Tue Aug 09 08:07:22 2011 +0200
+++ b/src/HOL/SMT.thy Tue Aug 09 18:52:18 2011 +0200
@@ -7,7 +7,6 @@
theory SMT
imports Record
uses
- "Tools/lambda_lifting.ML"
"Tools/SMT/smt_utils.ML"
"Tools/SMT/smt_failure.ML"
"Tools/SMT/smt_config.ML"
--- a/src/HOL/TPTP/atp_export.ML Tue Aug 09 08:07:22 2011 +0200
+++ b/src/HOL/TPTP/atp_export.ML Tue Aug 09 18:52:18 2011 +0200
@@ -160,8 +160,7 @@
facts
|> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th))
|> prepare_atp_problem ctxt format Axiom Axiom type_enc true true
- (rpair [] o map (introduce_combinators ctxt))
- false true [] @{prop False}
+ combinatorsN false true [] @{prop False}
val atp_problem =
atp_problem
|> map (apsnd (filter_out (is_problem_line_tautology ctxt)))
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 09 08:07:22 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 09 18:52:18 2011 +0200
@@ -25,6 +25,7 @@
best_slices :
Proof.context -> (real * (bool * (int * string * string))) list}
+ val force_sos : bool Config.T
val e_smartN : string
val e_autoN : string
val e_fun_weightN : string
@@ -36,16 +37,14 @@
val e_default_sym_offs_weight : real Config.T
val e_sym_offs_weight_base : real Config.T
val e_sym_offs_weight_span : real Config.T
- val spass_force_sos : bool Config.T
- val vampire_force_sos : bool Config.T
val eN : string
val spassN : string
val vampireN : string
val leo2N : string
val satallaxN : string
- val sine_eN : string
+ val e_sineN : string
val snarkN : string
- val tofof_eN : string
+ val e_tofofN : string
val waldmeisterN : string
val z3_atpN : string
val remote_prefix : string
@@ -103,14 +102,14 @@
(* named ATPs *)
val eN = "e"
+val leo2N = "leo2"
+val satallaxN = "satallax"
val spassN = "spass"
val vampireN = "vampire"
val z3_atpN = "z3_atp"
-val leo2N = "leo2"
-val satallaxN = "satallax"
-val sine_eN = "sine_e"
+val e_sineN = "e_sine"
val snarkN = "snark"
-val tofof_eN = "tofof_e"
+val e_tofofN = "e_tofof"
val waldmeisterN = "waldmeister"
val remote_prefix = "remote_"
@@ -128,6 +127,8 @@
val sosN = "sos"
val no_sosN = "no_sos"
+val force_sos = Attrib.setup_config_bool @{binding atp_force_sos} (K false)
+
(* E *)
@@ -228,10 +229,49 @@
val e = (eN, e_config)
-(* SPASS *)
+(* LEO-II *)
+
+val leo2_config : atp_config =
+ {exec = ("LEO2_HOME", "leo"),
+ required_execs = [],
+ arguments =
+ fn _ => fn _ => fn sos => fn timeout => fn _ =>
+ "--proofoutput --timeout " ^ string_of_int (to_secs 1 timeout)
+ |> sos = sosN ? prefix "--sos ",
+ proof_delims = tstp_proof_delims,
+ known_failures = [],
+ conj_sym_kind = Axiom,
+ prem_kind = Hypothesis,
+ formats = [THF, FOF],
+ best_slices = fn ctxt =>
+ (* FUDGE *)
+ [(0.667, (false, (150, "simple_higher", sosN))),
+ (0.333, (true, (50, "simple_higher", no_sosN)))]
+ |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
+ else I)}
-val spass_force_sos =
- Attrib.setup_config_bool @{binding atp_spass_force_sos} (K false)
+val leo2 = (leo2N, leo2_config)
+
+
+(* Satallax *)
+
+val satallax_config : atp_config =
+ {exec = ("SATALLAX_HOME", "satallax"),
+ required_execs = [],
+ arguments =
+ fn _ => fn _ => fn _ => fn timeout => fn _ =>
+ "-t " ^ string_of_int (to_secs 1 timeout),
+ proof_delims = tstp_proof_delims,
+ known_failures = [(ProofMissing, "SZS status Theorem")],
+ conj_sym_kind = Axiom,
+ prem_kind = Hypothesis,
+ formats = [THF],
+ best_slices = K [(1.0, (true, (100, "simple_higher", "")))] (* FUDGE *)}
+
+val satallax = (satallaxN, satallax_config)
+
+
+(* SPASS *)
(* The "-VarWeight=3" option helps the higher-order problems, probably by
counteracting the presence of "hAPP". *)
@@ -260,7 +300,7 @@
[(0.333, (false, (150, "mangled_tags", sosN))),
(0.333, (false, (300, "poly_tags?", sosN))),
(0.334, (true, (50, "mangled_tags?", no_sosN)))]
- |> (if Config.get ctxt spass_force_sos then hd #> apfst (K 1.0) #> single
+ |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
val spass = (spassN, spass_config)
@@ -268,9 +308,6 @@
(* Vampire *)
-val vampire_force_sos =
- Attrib.setup_config_bool @{binding atp_vampire_force_sos} (K false)
-
val vampire_config : atp_config =
{exec = ("VAMPIRE_HOME", "vampire"),
required_execs = [],
@@ -301,7 +338,7 @@
[(0.333, (false, (150, "poly_guards", sosN))),
(0.334, (true, (50, "mangled_guards?", no_sosN))),
(0.333, (false, (500, "mangled_tags?", sosN)))]
- |> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single
+ |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
val vampire = (vampireN, vampire_config)
@@ -411,26 +448,26 @@
val remote_e =
remotify_atp e "EP" ["1.0", "1.1", "1.2"]
(K (750, "mangled_tags?") (* FUDGE *))
+val remote_leo2 =
+ remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
+ (K (100, "simple_higher") (* FUDGE *))
+val remote_satallax =
+ remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
+ (K (100, "simple_higher") (* FUDGE *))
val remote_vampire =
remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
(K (200, "mangled_guards?") (* FUDGE *))
val remote_z3_atp =
remotify_atp z3_atp "Z3" ["2.18"] (K (250, "mangled_guards?") (* FUDGE *))
-val remote_leo2 =
- remote_atp leo2N "LEO-II" ["1.2.6"] [] [] Axiom Hypothesis [THF]
- (K (100, "simple_higher") (* FUDGE *))
-val remote_satallax =
- remote_atp satallaxN "Satallax" ["2.0"] [] [] Axiom Hypothesis [THF]
- (K (64, "simple_higher") (* FUDGE *))
-val remote_sine_e =
- remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
+val remote_e_sine =
+ remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
Conjecture [FOF] (K (500, "mangled_guards?") (* FUDGE *))
val remote_snark =
remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
[("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
[TFF, FOF] (K (100, "simple") (* FUDGE *))
-val remote_tofof_e =
- remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
+val remote_e_tofof =
+ remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config)
Axiom Hypothesis [TFF] (K (150, "simple") (* FUDGE *))
val remote_waldmeister =
remote_atp waldmeisterN "Waldmeister" ["710"]
@@ -461,9 +498,9 @@
Synchronized.change systems (fn _ => get_systems ())
val atps =
- [e, spass, vampire, z3_atp, remote_e, remote_vampire, remote_z3_atp,
- remote_leo2, remote_satallax, remote_sine_e, remote_snark, remote_tofof_e,
- remote_waldmeister]
+ [e, leo2, satallax, spass, vampire, z3_atp, remote_e, remote_leo2,
+ remote_satallax, remote_vampire, remote_z3_atp, remote_e_sine, remote_snark,
+ remote_e_tofof, remote_waldmeister]
val setup = fold add_atp atps
end;
--- a/src/HOL/Tools/ATP/atp_translate.ML Tue Aug 09 08:07:22 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Aug 09 18:52:18 2011 +0200
@@ -31,6 +31,13 @@
Guards of polymorphism * type_level * type_heaviness |
Tags of polymorphism * type_level * type_heaviness
+ val no_lambdasN : string
+ val concealedN : string
+ val liftingN : string
+ val combinatorsN : string
+ val hybridN : string
+ val lambdasN : string
+ val smartN : string
val bound_var_prefix : string
val schematic_var_prefix : string
val fixed_var_prefix : string
@@ -88,11 +95,10 @@
val unmangled_const_name : string -> string
val helper_table : ((string * bool) * thm list) list
val factsN : string
- val introduce_combinators : Proof.context -> term -> term
val prepare_atp_problem :
Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
- -> bool -> (term list -> term list * term list) -> bool -> bool -> term list
- -> term -> ((string * locality) * term) list
+ -> bool -> string -> bool -> bool -> term list -> term
+ -> ((string * locality) * term) list
-> string problem * string Symtab.table * int * int
* (string * locality) list vector * int list * int Symtab.table
val atp_problem_weights : string problem -> (string * real) list
@@ -106,6 +112,14 @@
type name = string * string
+val no_lambdasN = "no_lambdas"
+val concealedN = "concealed"
+val liftingN = "lifting"
+val combinatorsN = "combinators"
+val hybridN = "hybrid"
+val lambdasN = "lambdas"
+val smartN = "smart"
+
val generate_info = false (* experimental *)
fun isabelle_info s =
@@ -606,6 +620,29 @@
| _ => type_enc)
| format => (format, type_enc))
+fun lift_lambdas ctxt type_enc =
+ map (close_form o Envir.eta_contract) #> rpair ctxt
+ #-> Lambda_Lifting.lift_lambdas
+ (if polymorphism_of_type_enc type_enc = Polymorphic then
+ SOME polymorphic_free_prefix
+ else
+ NONE)
+ Lambda_Lifting.is_quantifier
+ #> fst
+
+fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
+ intentionalize_def t
+ | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
+ let
+ fun lam T t = Abs (Name.uu, T, t)
+ val (head, args) = strip_comb t ||> rev
+ val head_T = fastype_of head
+ val n = length args
+ val arg_Ts = head_T |> binder_types |> take n |> rev
+ val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
+ in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
+ | intentionalize_def t = t
+
type translated_formula =
{name : string,
locality : locality,
@@ -834,8 +871,13 @@
| (false, "c_All") => tweak_ho_quant tptp_ho_forall T args
| (false, "c_Ex") => tweak_ho_quant tptp_ho_exists T args
| (false, s) =>
- if is_tptp_equal s then IConst (`I tptp_equal, T, [])
- else IConst (proxy_base |>> prefix const_prefix, T, T_args)
+ if is_tptp_equal s andalso length args = 2 then
+ IConst (`I tptp_equal, T, [])
+ else
+ (* Use a proxy even for partially applied THF equality, because
+ the LEO-II and Satallax parsers complain about not being
+ able to infer the type of "=". *)
+ IConst (proxy_base |>> prefix const_prefix, T, T_args)
| _ => IConst (name, T, [])
else
IConst (proxy_base |>> prefix const_prefix, T, T_args)
@@ -1918,9 +1960,36 @@
val explicit_apply = NONE (* for experiments *)
fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc sound
- exporter trans_lambdas readable_names preproc hyp_ts concl_t facts =
+ exporter lambda_trans readable_names preproc hyp_ts concl_t facts =
let
val (format, type_enc) = choose_format [format] type_enc
+ val lambda_trans =
+ if lambda_trans = smartN then
+ if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
+ else if lambda_trans = lambdasN andalso
+ not (is_type_enc_higher_order type_enc) then
+ error ("Lambda translation method incompatible with first-order \
+ \encoding.")
+ else
+ lambda_trans
+ val trans_lambdas =
+ if lambda_trans = no_lambdasN then
+ rpair []
+ else if lambda_trans = concealedN then
+ lift_lambdas ctxt type_enc ##> K []
+ else if lambda_trans = liftingN then
+ lift_lambdas ctxt type_enc
+ else if lambda_trans = combinatorsN then
+ map (introduce_combinators ctxt) #> rpair []
+ else if lambda_trans = hybridN then
+ lift_lambdas ctxt type_enc
+ ##> maps (fn t => [t, introduce_combinators ctxt
+ (intentionalize_def t)])
+ else if lambda_trans = lambdasN then
+ map (Envir.eta_contract) #> rpair []
+ else
+ error ("Unknown lambda translation method: " ^
+ quote lambda_trans ^ ".")
val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
hyp_ts concl_t facts
--- a/src/HOL/Tools/Metis/metis_translate.ML Tue Aug 09 08:07:22 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Tue Aug 09 18:52:18 2011 +0200
@@ -197,7 +197,7 @@
*)
val (atp_problem, _, _, _, _, _, sym_tab) =
prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false
- (rpair []) false false [] @{prop False} props
+ no_lambdasN false false [] @{prop False} props
(*
val _ = tracing ("ATP PROBLEM: " ^
cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Aug 09 08:07:22 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Aug 09 18:52:18 2011 +0200
@@ -199,7 +199,7 @@
(* 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 =
- [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, sine_eN, waldmeisterN]
+ [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, e_sineN, waldmeisterN]
|> map_filter (remotify_prover_if_not_installed ctxt)
|> avoid_too_many_threads ctxt (Multithreading.max_threads_value (),
max_default_remote_threads)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Aug 09 08:07:22 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Aug 09 18:52:18 2011 +0200
@@ -60,12 +60,6 @@
type prover =
params -> (string -> minimize_command) -> prover_problem -> prover_result
- val concealedN : string
- val liftingN : string
- val combinatorsN : string
- val hybridN : string
- val lambdasN : string
- val smartN : string
val dest_dir : string Config.T
val problem_prefix : string Config.T
val measure_run_time : bool Config.T
@@ -335,13 +329,6 @@
(* configuration attributes *)
-val concealedN = "concealed"
-val liftingN = "lifting"
-val combinatorsN = "combinators"
-val hybridN = "hybrid"
-val lambdasN = "lambdas"
-val smartN = "smart"
-
(* Empty string means create files in Isabelle's temporary files directory. *)
val dest_dir =
Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
@@ -527,56 +514,6 @@
| NONE => type_enc_from_string best_type_enc)
|> choose_format formats
-fun lift_lambdas ctxt type_enc =
- map (close_form o Envir.eta_contract) #> rpair ctxt
- #-> Lambda_Lifting.lift_lambdas
- (if polymorphism_of_type_enc type_enc = Polymorphic then
- SOME polymorphic_free_prefix
- else
- NONE)
- Lambda_Lifting.is_quantifier
- #> fst
-
-fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
- intentionalize_def t
- | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
- let
- fun lam T t = Abs (Name.uu, T, t)
- val (head, args) = strip_comb t ||> rev
- val head_T = fastype_of head
- val n = length args
- val arg_Ts = head_T |> binder_types |> take n |> rev
- val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
- in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
- | intentionalize_def t = t
-
-fun translate_atp_lambdas ctxt type_enc =
- Config.get ctxt atp_lambda_translation
- |> (fn trans =>
- if trans = smartN then
- if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
- else if trans = lambdasN andalso
- not (is_type_enc_higher_order type_enc) then
- error ("Lambda translation method incompatible with first-order \
- \encoding.")
- else
- trans)
- |> (fn trans =>
- if trans = concealedN then
- lift_lambdas ctxt type_enc ##> K []
- else if trans = liftingN then
- lift_lambdas ctxt type_enc
- else if trans = combinatorsN then
- map (introduce_combinators ctxt) #> rpair []
- else if trans = hybridN then
- lift_lambdas ctxt type_enc
- ##> maps (fn t => [t, introduce_combinators ctxt
- (intentionalize_def t)])
- else if trans = lambdasN then
- map (Envir.eta_contract) #> rpair []
- else
- error ("Unknown lambda translation method: " ^ quote trans ^ "."))
-
val metis_minimize_max_time = seconds 2.0
fun choose_minimize_command minimize_command name preplay =
@@ -708,7 +645,8 @@
val (atp_problem, pool, conjecture_offset, facts_offset,
fact_names, typed_helpers, sym_tab) =
prepare_atp_problem ctxt format conj_sym_kind prem_kind
- type_enc sound false (translate_atp_lambdas ctxt type_enc)
+ type_enc sound false
+ (Config.get ctxt atp_lambda_translation)
(Config.get ctxt atp_readable_names) true hyp_ts concl_t
facts
fun weights () = atp_problem_weights atp_problem
--- a/src/Pure/Syntax/parser.ML Tue Aug 09 08:07:22 2011 +0200
+++ b/src/Pure/Syntax/parser.ML Tue Aug 09 18:52:18 2011 +0200
@@ -747,7 +747,7 @@
in get_prods (connected_with chains nts nts) [] end;
-fun PROCESSS ctxt warned prods chains Estate i c states =
+fun PROCESSS ctxt prods chains Estate i c states =
let
fun all_prods_for nt = prods_for prods chains true c [nt];
@@ -773,14 +773,6 @@
val tk_prods = all_prods_for nt;
val States' = mk_states i min_prec nt (get_RHS min_prec tk_prods);
in (Inttab.update (nt, (min_prec, [])) used, States') end);
-
- val _ =
- if not (! warned) andalso
- length new_states + length States > Config.get ctxt branching_level then
- (Context_Position.if_visible ctxt warning
- "Currently parsed expression could be extremely ambiguous";
- warned := true)
- else ();
in
processS used' (new_states @ States) (S :: Si, Sii)
end
@@ -803,7 +795,7 @@
in processS Inttab.empty states ([], []) end;
-fun produce ctxt warned prods tags chains stateset i indata prev_token =
+fun produce ctxt prods tags chains stateset i indata prev_token =
(case Array.sub (stateset, i) of
[] =>
let
@@ -821,10 +813,10 @@
[] => s
| c :: cs =>
let
- val (si, sii) = PROCESSS ctxt warned prods chains stateset i c s;
+ val (si, sii) = PROCESSS ctxt prods chains stateset i c s;
val _ = Array.update (stateset, i, si);
val _ = Array.update (stateset, i + 1, sii);
- in produce ctxt warned prods tags chains stateset (i + 1) cs c end));
+ in produce ctxt prods tags chains stateset (i + 1) cs c end));
fun get_trees states = map_filter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE) states;
@@ -841,7 +833,7 @@
val _ = Array.update (Estate, 0, S0);
in
get_trees
- (produce ctxt (Unsynchronized.ref false) prods tags chains Estate 0 indata Lexicon.eof)
+ (produce ctxt prods tags chains Estate 0 indata Lexicon.eof)
end;
--- a/src/Tools/eqsubst.ML Tue Aug 09 08:07:22 2011 +0200
+++ b/src/Tools/eqsubst.ML Tue Aug 09 18:52:18 2011 +0200
@@ -108,10 +108,6 @@
val searchf_bt_unify_valid :
searchinfo -> term -> match Seq.seq Seq.seq
- (* syntax tools *)
- val ith_syntax : int list parser
- val options_syntax : bool parser
-
(* Isar level hooks *)
val eqsubst_asm_meth : Proof.context -> int list -> thm list -> Proof.method
val eqsubst_meth : Proof.context -> int list -> thm list -> Proof.method
@@ -546,23 +542,15 @@
fun eqsubst_asm_meth ctxt occL inthms =
SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
-(* syntax for options, given "(asm)" will give back true, without
- gives back false *)
-val options_syntax =
- (Args.parens (Args.$$$ "asm") >> (K true)) ||
- (Scan.succeed false);
-
-val ith_syntax =
- Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0];
-
(* combination method that takes a flag (true indicates that subst
should be done to an assumption, false = apply to the conclusion of
the goal) as well as the theorems to use *)
val setup =
Method.setup @{binding subst}
- (Scan.lift (options_syntax -- ith_syntax) -- Attrib.thms >>
- (fn ((asmflag, occL), inthms) => fn ctxt =>
- (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms))
+ (Args.mode "asm" -- Scan.lift (Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
+ Attrib.thms >>
+ (fn ((asm, occL), inthms) => fn ctxt =>
+ (if asm then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms))
"single-step substitution";
end;