merged, resolving conflicts in src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML due to clones bb2ea9e80c33 + 62c039ce397c;
--- a/CONTRIBUTORS Mon Mar 03 13:19:23 2025 +0100
+++ b/CONTRIBUTORS Mon Mar 03 19:52:18 2025 +0100
@@ -3,6 +3,10 @@
listed as an author in one of the source files of this Isabelle distribution.
+Contributions to this Isabelle version
+--------------------------------------
+
+
Contributions to Isabelle2025
-----------------------------
--- a/NEWS Mon Mar 03 13:19:23 2025 +0100
+++ b/NEWS Mon Mar 03 19:52:18 2025 +0100
@@ -4,6 +4,17 @@
(Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
+New in this Isabelle version
+----------------------------
+
+* Theory "HOL.Fun":
+ - Added lemmas.
+ antimonotone_on_inf_fun
+ antimonotone_on_sup_fun
+ monotone_on_inf_fun
+ monotone_on_sup_fun
+
+
New in Isabelle2025 (March 2025)
--------------------------------
--- a/src/Doc/Sledgehammer/document/root.tex Mon Mar 03 13:19:23 2025 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Mon Mar 03 19:52:18 2025 +0100
@@ -101,9 +101,9 @@
\section{Introduction}
\label{introduction}
-Sledgehammer is a tool that applies automatic theorem provers (ATPs)
-and satisfiability-modulo-theories (SMT) solvers on the current goal, mostly
-to find proofs but also to refute the goal.%
+Sledgehammer is a tool that applies automatic theorem provers (ATPs),
+satisfiability-modulo-theories (SMT) solvers, and Isabelle proof methods on the
+current goal, mostly to find proofs but optionally also to refute the goal.%
\footnote{The distinction between ATPs and SMT solvers is mostly
historical but convenient.}
%
@@ -115,17 +115,21 @@
via the System\-On\-TPTP web service \cite{sutcliffe-2000}. The supported SMT
solvers are CVC4 \cite{cvc4}, cvc5 \cite{barbosa-et-al-cvc5}, veriT
\cite{bouton-et-al-2009}, and Z3 \cite{de-moura-2008}. These are always run
-locally.
+locally. The supported proof methods are \textit{algebra}, \textit{argo},
+\textit{auto}, \textit{blast}, \textit{fastforce}, \textit{force},
+\textit{linarith}, \textit{meson}, \textit{metis}, \textit{order},
+\textit{presburger}, \textit{satx}, and \textit{simp}. The proof method support
+is experimental and disabled by default.
-The problem passed to the automatic provers (or solvers) consists of your
-current goal together with a heuristic selection of hundreds of facts (theorems)
-from the current theory context, filtered by relevance.
+The problem passed to the ATPs, SMT solvers, or proof methods consists
+of your current goal together with a heuristic selection of facts (theorems)
+from the current theory context, filtered by likely relevance.
The result of a successful proof search is some source text that typically
-reconstructs the proof within Isabelle. For ATPs, the reconstructed proof
-typically relies on the general-purpose \textit{metis} proof method, which
-integrates the Metis ATP in Isabelle/HOL with explicit inferences going through
-the kernel. Thus its results are correct by construction.
+reconstructs the proof within Isabelle. The reconstructed proof often relies on
+the general-purpose \textit{metis} proof method, which integrates the Metis ATP
+in Isabelle/HOL with explicit inferences going through the kernel. Thus its
+results are correct by construction.
Sometimes the automatic provers might detect that the goal is inconsistent with
the background facts---or even that the background facts are inconsistent
@@ -154,7 +158,7 @@
\label{installation}
Sledgehammer is part of Isabelle, so you do not need to install it. However, it
-relies on third-party automatic provers (ATPs and SMT solvers).
+relies on third-party ATPs and SMT solvers.
Among the ATPs, agsyHOL, Alt-Ergo, E, LEO-II, Leo-III, Satallax, SPASS, Vampire,
and Zipperposition can be run locally; in addition, agsyHOL, Alt-Ergo, E,
@@ -162,7 +166,7 @@
available remotely via System\-On\-TPTP \cite{sutcliffe-2000}. The SMT solvers
CVC4, cvc5, veriT, and Z3 can be run locally.
-There are three main ways to install automatic provers on your machine:
+There are three main ways to install ATPs or SMT solvers on your machine:
\begin{sloppy}
\begin{enum}
@@ -177,7 +181,7 @@
\footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at
startup. Its value can be retrieved by executing \texttt{isabelle}
\texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.}
-file with the absolute path to the prover. For example, if the
+file with the absolute path to the system. For example, if the
\texttt{components} file does not exist yet and you extracted SPASS to
\texttt{/usr/local/spass-3.8ds}, create it with the single line
@@ -322,15 +326,13 @@
\begin{enum}
\item[\labelitemi] \textbf{\textit{provers}} (\S\ref{mode-of-operation}) specifies
-the automatic provers (ATPs and SMT solvers) that should be run whenever
-Sledgehammer is invoked (e.g., ``\textit{provers}~= \textit{cvc4 e
+the automatic provers (ATPs, SMT solvers, or proof methods) that should be run whenever
+Sledgehammer is invoked (e.g., ``\textit{provers}~= \textit{auto cvc4 e
vampire zipperposition\/}'').
\item[\labelitemi] \textbf{\textit{max\_facts}} (\S\ref{relevance-filter})
specifies the maximum number of facts that should be passed to the provers. By
-default, the value is prover-dependent but varies between about 50 and 1000. If
-the provers time out, you can try lowering this value to, say, 25 or 50 and see
-if that helps.
+default, the value is prover-dependent and varies between 0 and about 1000.
\item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies
that Isar proofs should be generated, in addition to one-line proofs. The length
@@ -421,10 +423,10 @@
\point{Why does Metis fail to reconstruct the proof?}
-There are many reasons. If Metis runs seemingly forever, that is a sign that the
-proof is too difficult for it. Metis's search is complete for first-order logic
-with equality, so if the proof was found by a superposition-based ATP such as
-E, SPASS, or Vampire, Metis should \emph{eventually} find it---in principle.
+There are many reasons. If Metis runs seemingly forever, that is a sign that
+the proof is too difficult for it. Metis's search is complete for first-order
+logic with equality, but ATPs such as E, Vampire, and Zipperposition are
+higher-order, so Metis might fail at refinding their proofs.
In some rare cases, \textit{metis} fails fairly quickly, and you get the error
message ``One-line proof reconstruction failed.'' This indicates that
@@ -437,8 +439,8 @@
\textit{mono\_tags} arguments to Metis?}
The \textit{metis}~(\textit{full\_types}) proof method
-and its cousin \textit{metis}~(\textit{mono\_tags}) are fully-typed
-versions of Metis. It is somewhat slower than \textit{metis}, but the proof
+and its relative \textit{metis}~(\textit{mono\_tags}) are fully-typed
+versions of Metis. They are somewhat slower than \textit{metis}, but the proof
search is fully typed, and it also includes more powerful rules such as the
axiom ``$x = \const{True} \mathrel{\lor} x = \const{False}$'' for reasoning in
higher-order positions (e.g., in set comprehensions). The method is tried as a
@@ -478,10 +480,10 @@
\point{Are the generated proofs minimal?}
Automatic provers frequently use many more facts than are necessary.
-Sledgehammer includes a proof minimization tool that takes a set of facts returned by
-a given prover and repeatedly calls a prover or proof method with subsets of
-those facts to find a minimal set. Reducing the number of facts typically helps
-reconstruction and declutters the proof documents.
+Sledgehammer includes a proof minimization tool that takes a set of facts
+returned by a prover and repeatedly calls a prover or proof method with subsets
+of those facts to find a minimal set. Reducing the number of facts typically
+helps reconstruction and declutters the proof documents.
\point{A strange error occurred---what should I do?}
@@ -490,15 +492,6 @@
error to the author at \authoremail.
-\point{Auto can solve it---why not Sledgehammer?}
-
-Problems can be easy for \textit{auto} and difficult for automatic provers, but
-the reverse is also true, so do not be discouraged if your first attempts fail.
-Because the system refers to all theorems known to Isabelle, it is particularly
-suitable when your goal has a short proof but requires lemmas that you do not
-know about.
-
-
\point{Why are there so many options?}
Sledgehammer's philosophy is that it should work out of the box, without user
@@ -528,8 +521,8 @@
\item[\labelitemi] \textbf{\textit{supported\_provers}:} Prints the list of
automatic provers supported by Sledgehammer. See \S\ref{installation} and
-\S\ref{mode-of-operation} for more information on how to install automatic
-provers.
+\S\ref{mode-of-operation} for more information on how to install ATPs and SMT
+solvers.
\item[\labelitemi] \textbf{\textit{refresh\_tptp}:} Refreshes the list of remote
ATPs available at System\-On\-TPTP \cite{sutcliffe-2000}.
@@ -551,9 +544,7 @@
theory to process all the available facts, learning from proofs generated by
automatic provers. The prover to use and its timeout can be set using the
\textit{prover} (\S\ref{mode-of-operation}) and \textit{timeout}
-(\S\ref{timeouts}) options. It is recommended to perform learning using a
-first-order ATP (such as E, SPASS, and Vampire) as opposed to a
-higher-order ATP or an SMT solver.
+(\S\ref{timeouts}) options.
\item[\labelitemi] \textbf{\textit{relearn\_isar}:} Same as \textit{unlearn}
followed by \textit{learn\_isar}.
@@ -687,12 +678,11 @@
\begin{enum}
\opnodefaultbrk{provers}{string}
Specifies the automatic provers to use as a space-separated list (e.g.,
-``\textit{cvc4}~\textit{e}~\textit{spass}~\textit{vampire\/}'').
+``\textit{auto}~\textit{cvc4}~\textit{e}~\textit{spass}~\textit{vampire\/}'').
Provers can be run locally or remotely; see \S\ref{installation} for
-installation instructions. By default, \textit{provers} is set to the list of
-all installed local provers.
+installation instructions.
-The following local provers are supported:
+The following local ATPs and SMT solvers are supported:
\begin{sloppy}
\begin{enum}
@@ -719,13 +709,13 @@
set the environment variable \texttt{CVC5\_SOLVER} to the complete path of the
executable, including the file name.
-\item[\labelitemi] \textbf{\textit{e}:} E is a first-order resolution prover
+\item[\labelitemi] \textbf{\textit{e}:} E is a higher-order superposition prover
developed by Stephan Schulz \cite{schulz-2019}. To use E, set the environment
variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof}
-executable and \texttt{E\_VERSION} to the version number (e.g., ``1.8''), or
+executable and \texttt{E\_VERSION} to the version number (e.g., ``3.0''), or
install the prebuilt E package from \download.
-\item[\labelitemi] \textbf{\textit{iprover}:} iProver is a pure
+\item[\labelitemi] \textbf{\textit{iprover}:} iProver is a first-order
instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}.
To use iProver, set the environment variable \texttt{IPROVER\_HOME} to the
directory that contains the \texttt{iproveropt} executable. iProver depends on
@@ -750,25 +740,26 @@
environment variable \texttt{SATALLAX\_HOME} to the directory that contains the
\texttt{satallax} executable.
-\item[\labelitemi] \textbf{\textit{spass}:} SPASS is a first-order resolution
+\item[\labelitemi] \textbf{\textit{spass}:} SPASS is a first-order superposition
prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}.
To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory
that contains the \texttt{SPASS} executable and \texttt{SPASS\_VERSION} to the
version number (e.g., ``3.8ds''), or install the prebuilt SPASS package from
\download.
-\item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a first-order
-resolution prover developed by Andrei Voronkov and his colleagues
+\item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a higher-order
+superposition prover developed by Andrei Voronkov and his colleagues
\cite{riazanov-voronkov-2002}. To use Vampire, set the environment variable
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{vampire}
executable and \texttt{VAMPIRE\_VERSION} to the version number (e.g.,
-``4.2.2'').
+``4.8'').
-\item[\labelitemi] \textbf{\textit{verit}:} veriT \cite{bouton-et-al-2009} is an
-SMT solver developed by David D\'eharbe, Pascal Fontaine, and their colleagues.
-It is designed to produce detailed proofs for reconstruction in proof
-assistants. To use veriT, set the environment variable \texttt{ISABELLE\_VERIT}
-to the complete path of the executable, including the file name.
+\item[\labelitemi] \textbf{\textit{verit}:} veriT \cite{bouton-et-al-2009} is a
+first-order SMT solver developed by David D\'eharbe, Pascal Fontaine, and their
+colleagues. It is designed to produce detailed proofs for reconstruction in
+proof assistants. To use veriT, set the environment variable
+\texttt{ISABELLE\_VERIT} to the complete path of the executable, including the
+file name.
\item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at
Microsoft Research \cite{de-moura-2008}. To use Z3, set the environment variable
@@ -780,12 +771,12 @@
Cruanes, Petar Vukmirovi\'c, and colleagues. To use Zipperposition, set the
environment variable \texttt{ZIPPERPOSITION\_HOME} to the directory that
contains the \texttt{zipperposition} executable and
-\texttt{ZIPPERPOSITION\_VERSION} to the version number (e.g., ``2.0.1'').
+\texttt{ZIPPERPOSITION\_VERSION} to the version number (e.g., ``2.1'').
\end{enum}
\end{sloppy}
-Moreover, the following remote provers are supported:
+The following remote ATPs are supported:
\begin{enum}
\item[\labelitemi] \textbf{\textit{remote\_agsyhol}:} The remote version of
@@ -817,10 +808,20 @@
version of Zipperposition runs on Geoff Sutcliffe's Miami servers.
\end{enum}
-By default, Sledgehammer runs a subset of CVC4, E, SPASS, Vampire, veriT, Z3,
-and Zipperposition in parallel, either locally or remotely---depending on the
-number of processor cores available and on which provers are actually installed.
-It is generally beneficial to run several provers in parallel.
+By default, \textit{provers} is set to a subset of CVC4, E, SPASS, Vampire,
+veriT, Z3, and Zipperposition, to be run in parallel, either locally or
+remotely---depending on the number of processor cores available and on which
+provers are actually installed. Proof methods are currently not included, due
+to their experimental status. (Proof methods can nevertheless appear in
+Isabelle proofs that reconstruct proofs originally found by ATPs or SMT
+solvers.)
+
+The following proof methods are supported:\ \textbf{\textit{algebra}},
+\textbf{\textit{argo}}, \textbf{\textit{auto}}, \textbf{\textit{blast}},
+\textbf{\textit{fastforce}}, \textbf{\textit{force}},
+\textbf{\textit{linarith}}, \textbf{\textit{meson}}, \textbf{\textit{metis}},
+\textbf{\textit{order}}, \textbf{\textit{presburger}}, \textbf{\textit{satx}},
+\textbf{\textit{simp}}.
\opnodefault{prover}{string}
Alias for \textit{provers}.
@@ -936,7 +937,7 @@
Specifies the maximum number of facts that may be returned by the relevance
filter. If the option is set to \textit{smart} (the default), it effectively
takes a value that was empirically found to be appropriate for the prover.
-Typical values lie between 50 and 1000.
+Typical values lie between 0 and 1000.
\opdefault{fact\_thresholds}{float\_pair}{\upshape 0.45~0.85}
Specifies the thresholds above which facts are considered relevant by the
@@ -955,9 +956,9 @@
Specifies the maximum number of monomorphic instances to generate beyond
\textit{max\_facts}. The higher this limit is, the more monomorphic instances
are potentially generated. Whether monomorphization takes place depends on the
-type encoding used. If the option is set to \textit{smart} (the default), it
-takes a value that was empirically found to be appropriate for the prover. For
-most provers, this value is 100.
+prover and possibly the specified type encoding. If the option is set to
+\textit{smart} (the default), it takes a value that was empirically found to be
+appropriate for the prover. For most provers, this value is 100.
\nopagebreak
{\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
@@ -966,9 +967,9 @@
Specifies the maximum number of iterations for the monomorphization fixpoint
construction. The higher this limit is, the more monomorphic instances are
potentially generated. Whether monomorphization takes place depends on the
-type encoding used. If the option is set to \textit{smart} (the default), it
-takes a value that was empirically found to be appropriate for the prover.
-For most provers, this value is 3.
+prover and possibly the specified type encoding. If the option is set to
+\textit{smart} (the default), it takes a value that was empirically found to be
+appropriate for the prover.
\nopagebreak
{\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
@@ -1247,12 +1248,12 @@
problem.
\end{enum}
-Sledgehammer emits an error if the actual outcome differs from the expected outcome. This option is
-useful for regression testing.
+Sledgehammer emits an error if the actual outcome differs from the expected
+outcome. This option is useful for regression testing.
-The expected outcomes are not mutually exclusive. More specifically, \textit{some} is accepted
-whenever \textit{some\_preplayed} is accepted as the former has strictly fewer requirements
-than the later.
+The expected outcomes are not mutually exclusive. More specifically,
+\textit{some} is accepted whenever \textit{some\_preplayed} is accepted as the
+former has strictly fewer requirements than the later.
\nopagebreak
{\small See also \textit{timeout} (\S\ref{timeouts}).}
@@ -1267,7 +1268,7 @@
Specifies the maximum number of seconds that the automatic provers should spend
searching for a proof. This excludes problem preparation and is a soft limit.
-\opdefault{slices}{int}{\upshape 12 times the number of cores detected}
+\opdefault{slices}{int}{\upshape 24 times the number of cores detected}
Specifies the number of time slices. Time slices are the basic unit for prover
invocations. They are divided among the available provers. A single prover
invocation can occupy a single slice, two slices, or more, depending on the
@@ -1299,9 +1300,9 @@
\label{mirabelle}
The \texttt{isabelle mirabelle} tool executes Sledgehammer or other advisory
-tools (e.g., Nitpick) or tactics (e.g., \textit{auto}) on all subgoals emerging
-in a theory. It is typically used to measure the success rate of a proof tool
-on some benchmark. Its command-line usage is as follows:
+tools (e.g., Nitpick) or proof methods (e.g., \textit{auto}) on all subgoals
+emerging in a theory. It is typically used to measure the success rate of a
+proof tool on some benchmark. Its command-line usage is as follows:
{\small
\begin{verbatim}
--- a/src/HOL/Fun.thy Mon Mar 03 13:19:23 2025 +0100
+++ b/src/HOL/Fun.thy Mon Mar 03 19:52:18 2025 +0100
@@ -816,18 +816,12 @@
"(\<lambda>x. x - a) ` (s \<inter> t) = ((\<lambda>x. x - a) ` s) \<inter> ((\<lambda>x. x - a) ` t)"
by(rule image_Int)(simp add: inj_on_def diff_eq_eq)
-end
-
-(* TODO: prove in group_add *)
-context ab_group_add
-begin
-
lemma translation_Compl:
"(+) a ` (- t) = - ((+) a ` t)"
proof (rule set_eqI)
fix b
show "b \<in> (+) a ` (- t) \<longleftrightarrow> b \<in> - (+) a ` t"
- by (auto simp: image_iff algebra_simps intro!: bexI [of _ "b - a"])
+ by (auto simp: image_iff algebra_simps intro!: bexI [of _ "- a + b"])
qed
end
@@ -1345,6 +1339,26 @@
for f :: "'a \<Rightarrow> 'b::semilattice_sup"
by (auto simp add: mono_def intro: Lattices.sup_least)
+lemma monotone_on_sup_fun:
+ fixes f g :: "_ \<Rightarrow> _:: semilattice_sup"
+ shows "monotone_on A P (\<le>) f \<Longrightarrow> monotone_on A P (\<le>) g \<Longrightarrow> monotone_on A P (\<le>) (f \<squnion> g)"
+ by (auto intro: monotone_onI sup_mono dest: monotone_onD simp: sup_fun_def)
+
+lemma monotone_on_inf_fun:
+ fixes f g :: "_ \<Rightarrow> _:: semilattice_inf"
+ shows "monotone_on A P (\<le>) f \<Longrightarrow> monotone_on A P (\<le>) g \<Longrightarrow> monotone_on A P (\<le>) (f \<sqinter> g)"
+ by (auto intro: monotone_onI inf_mono dest: monotone_onD simp: inf_fun_def)
+
+lemma antimonotone_on_sup_fun:
+ fixes f g :: "_ \<Rightarrow> _:: semilattice_sup"
+ shows "monotone_on A P (\<ge>) f \<Longrightarrow> monotone_on A P (\<ge>) g \<Longrightarrow> monotone_on A P (\<ge>) (f \<squnion> g)"
+ by (auto intro: monotone_onI sup_mono dest: monotone_onD simp: sup_fun_def)
+
+lemma antimonotone_on_inf_fun:
+ fixes f g :: "_ \<Rightarrow> _:: semilattice_inf"
+ shows "monotone_on A P (\<ge>) f \<Longrightarrow> monotone_on A P (\<ge>) g \<Longrightarrow> monotone_on A P (\<ge>) (f \<sqinter> g)"
+ by (auto intro: monotone_onI inf_mono dest: monotone_onD simp: inf_fun_def)
+
lemma (in linorder) min_of_mono: "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)"
by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym)
--- a/src/HOL/Library/Sublist.thy Mon Mar 03 13:19:23 2025 +0100
+++ b/src/HOL/Library/Sublist.thy Mon Mar 03 19:52:18 2025 +0100
@@ -63,11 +63,9 @@
subsection \<open>Basic properties of prefixes\<close>
-(* FIXME rm *)
theorem Nil_prefix [simp]: "prefix [] xs"
by (fact prefix_bot.bot_least)
-(* FIXME rm *)
theorem prefix_Nil [simp]: "(prefix xs []) = (xs = [])"
by (fact prefix_bot.bot_unique)
@@ -80,7 +78,7 @@
next
assume "xs = ys @ [y] \<or> prefix xs ys"
then show "prefix xs (ys @ [y])"
- by auto (metis append.assoc prefix_def)
+ using prefix_def prefix_order.order_trans by blast
qed
lemma Cons_prefix_Cons [simp]: "prefix (x # xs) (y # ys) = (x = y \<and> prefix xs ys)"
@@ -109,23 +107,26 @@
theorem prefix_append:
"prefix xs (ys @ zs) = (prefix xs ys \<or> (\<exists>us. xs = ys @ us \<and> prefix us zs))"
- apply (induct zs rule: rev_induct)
- apply force
- apply (simp flip: append_assoc)
- apply (metis append_eq_appendI)
- done
+proof (induct zs rule: rev_induct)
+ case Nil
+ then show ?case by force
+next
+ case (snoc x xs)
+ then show ?case
+ by (metis append.assoc prefix_snoc)
+qed
lemma append_one_prefix:
"prefix xs ys \<Longrightarrow> length xs < length ys \<Longrightarrow> prefix (xs @ [ys ! length xs]) ys"
- proof (unfold prefix_def)
- assume a1: "\<exists>zs. ys = xs @ zs"
- then obtain sk :: "'a list" where sk: "ys = xs @ sk" by fastforce
- assume a2: "length xs < length ys"
- have f1: "\<And>v. ([]::'a list) @ v = v" using append_Nil2 by simp
- have "[] \<noteq> sk" using a1 a2 sk less_not_refl by force
- hence "\<exists>v. xs @ hd sk # v = ys" using sk by (metis hd_Cons_tl)
- thus "\<exists>zs. ys = (xs @ [ys ! length xs]) @ zs" using f1 by fastforce
- qed
+proof (unfold prefix_def)
+ assume a1: "\<exists>zs. ys = xs @ zs"
+ then obtain sk :: "'a list" where sk: "ys = xs @ sk" by fastforce
+ assume a2: "length xs < length ys"
+ have f1: "\<And>v. ([]::'a list) @ v = v" using append_Nil2 by simp
+ have "[] \<noteq> sk" using a1 a2 sk less_not_refl by force
+ hence "\<exists>v. xs @ hd sk # v = ys" using sk by (metis hd_Cons_tl)
+ thus "\<exists>zs. ys = (xs @ [ys ! length xs]) @ zs" using f1 by fastforce
+qed
theorem prefix_length_le: "prefix xs ys \<Longrightarrow> length xs \<le> length ys"
by (auto simp add: prefix_def)
@@ -148,7 +149,7 @@
unfolding prefix_def by (metis takeWhile_dropWhile_id)
lemma prefixeq_butlast: "prefix (butlast xs) xs"
-by (simp add: butlast_conv_take take_is_prefix)
+ by (simp add: butlast_conv_take take_is_prefix)
lemma prefix_map_rightE:
assumes "prefix xs (map f ys)"
@@ -162,13 +163,13 @@
qed
lemma map_mono_prefix: "prefix xs ys \<Longrightarrow> prefix (map f xs) (map f ys)"
-by (auto simp: prefix_def)
+ by (auto simp: prefix_def)
lemma filter_mono_prefix: "prefix xs ys \<Longrightarrow> prefix (filter P xs) (filter P ys)"
-by (auto simp: prefix_def)
+ by (auto simp: prefix_def)
lemma sorted_antimono_prefix: "prefix xs ys \<Longrightarrow> sorted ys \<Longrightarrow> sorted xs"
-by (metis sorted_append prefix_def)
+ by (metis sorted_append prefix_def)
lemma prefix_length_less: "strict_prefix xs ys \<Longrightarrow> length xs < length ys"
by (auto simp: strict_prefix_def prefix_def)
@@ -281,8 +282,8 @@
subsection \<open>Prefixes\<close>
primrec prefixes where
-"prefixes [] = [[]]" |
-"prefixes (x#xs) = [] # map ((#) x) (prefixes xs)"
+ "prefixes [] = [[]]" |
+ "prefixes (x#xs) = [] # map ((#) x) (prefixes xs)"
lemma in_set_prefixes[simp]: "xs \<in> set (prefixes ys) \<longleftrightarrow> prefix xs ys"
proof (induct xs arbitrary: ys)
@@ -400,44 +401,43 @@
lemma Longest_common_prefix_unique:
\<open>\<exists>! ps. (\<forall>xs \<in> L. prefix ps xs) \<and> (\<forall>qs. (\<forall>xs \<in> L. prefix qs xs) \<longrightarrow> length qs \<le> length ps)\<close>
if \<open>L \<noteq> {}\<close>
- using that apply (rule ex_ex1I[OF Longest_common_prefix_ex])
- using that apply (auto simp add: prefix_def)
- apply (metis append_eq_append_conv_if order.antisym)
- done
+ apply (intro ex_ex1I[OF Longest_common_prefix_ex [OF that]])
+ by (meson that all_not_in_conv prefix_length_prefix prefix_order.dual_order.eq_iff)
lemma Longest_common_prefix_eq:
- "\<lbrakk> L \<noteq> {}; \<forall>xs \<in> L. prefix ps xs;
+ "\<lbrakk> L \<noteq> {}; \<forall>xs \<in> L. prefix ps xs;
\<forall>qs. (\<forall>xs \<in> L. prefix qs xs) \<longrightarrow> size qs \<le> size ps \<rbrakk>
\<Longrightarrow> Longest_common_prefix L = ps"
-unfolding Longest_common_prefix_def arg_max_def is_arg_max_linorder
-by(rule some1_equality[OF Longest_common_prefix_unique]) auto
+ unfolding Longest_common_prefix_def arg_max_def is_arg_max_linorder
+ by(rule some1_equality[OF Longest_common_prefix_unique]) auto
lemma Longest_common_prefix_prefix:
"xs \<in> L \<Longrightarrow> prefix (Longest_common_prefix L) xs"
-unfolding Longest_common_prefix_def arg_max_def is_arg_max_linorder
-by(rule someI2_ex[OF Longest_common_prefix_ex]) auto
+ unfolding Longest_common_prefix_def arg_max_def is_arg_max_linorder
+ by(rule someI2_ex[OF Longest_common_prefix_ex]) auto
lemma Longest_common_prefix_longest:
"L \<noteq> {} \<Longrightarrow> \<forall>xs\<in>L. prefix ps xs \<Longrightarrow> length ps \<le> length(Longest_common_prefix L)"
-unfolding Longest_common_prefix_def arg_max_def is_arg_max_linorder
-by(rule someI2_ex[OF Longest_common_prefix_ex]) auto
+ unfolding Longest_common_prefix_def arg_max_def is_arg_max_linorder
+ by(rule someI2_ex[OF Longest_common_prefix_ex]) auto
lemma Longest_common_prefix_max_prefix:
"L \<noteq> {} \<Longrightarrow> \<forall>xs\<in>L. prefix ps xs \<Longrightarrow> prefix ps (Longest_common_prefix L)"
-by(metis Longest_common_prefix_prefix Longest_common_prefix_longest
- prefix_length_prefix ex_in_conv)
+ by(metis Longest_common_prefix_prefix Longest_common_prefix_longest
+ prefix_length_prefix ex_in_conv)
lemma Longest_common_prefix_Nil: "[] \<in> L \<Longrightarrow> Longest_common_prefix L = []"
-using Longest_common_prefix_prefix prefix_Nil by blast
+ using Longest_common_prefix_prefix prefix_Nil by blast
-lemma Longest_common_prefix_image_Cons: "L \<noteq> {} \<Longrightarrow>
- Longest_common_prefix ((#) x ` L) = x # Longest_common_prefix L"
-apply(rule Longest_common_prefix_eq)
- apply(simp)
- apply (simp add: Longest_common_prefix_prefix)
-apply simp
-by(metis Longest_common_prefix_longest[of L] Cons_prefix_Cons Nitpick.size_list_simp(2)
- Suc_le_mono hd_Cons_tl order.strict_implies_order zero_less_Suc)
+lemma Longest_common_prefix_image_Cons:
+ assumes "L \<noteq> {}"
+ shows "Longest_common_prefix ((#) x ` L) = x # Longest_common_prefix L"
+proof (intro Longest_common_prefix_eq strip)
+ show "\<And>qs. \<forall>xs\<in>(#) x ` L. prefix qs xs \<Longrightarrow>
+ length qs \<le> length (x # Longest_common_prefix L)"
+ by (metis assms Longest_common_prefix_longest[of L] Cons_prefix_Cons Suc_le_mono hd_Cons_tl
+ image_eqI length_Cons prefix_bot.bot_least prefix_length_le)
+qed (auto simp add: assms Longest_common_prefix_prefix)
lemma Longest_common_prefix_eq_Cons: assumes "L \<noteq> {}" "[] \<notin> L" "\<forall>xs\<in>L. hd xs = x"
shows "Longest_common_prefix L = x # Longest_common_prefix {ys. x#ys \<in> L}"
@@ -450,26 +450,26 @@
lemma Longest_common_prefix_eq_Nil:
"\<lbrakk>x#ys \<in> L; y#zs \<in> L; x \<noteq> y \<rbrakk> \<Longrightarrow> Longest_common_prefix L = []"
-by (metis Longest_common_prefix_prefix list.inject prefix_Cons)
+ by (metis Longest_common_prefix_prefix list.inject prefix_Cons)
fun longest_common_prefix :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"longest_common_prefix (x#xs) (y#ys) =
+ "longest_common_prefix (x#xs) (y#ys) =
(if x=y then x # longest_common_prefix xs ys else [])" |
-"longest_common_prefix _ _ = []"
+ "longest_common_prefix _ _ = []"
lemma longest_common_prefix_prefix1:
"prefix (longest_common_prefix xs ys) xs"
-by(induction xs ys rule: longest_common_prefix.induct) auto
+ by(induction xs ys rule: longest_common_prefix.induct) auto
lemma longest_common_prefix_prefix2:
"prefix (longest_common_prefix xs ys) ys"
-by(induction xs ys rule: longest_common_prefix.induct) auto
+ by(induction xs ys rule: longest_common_prefix.induct) auto
lemma longest_common_prefix_max_prefix:
"\<lbrakk> prefix ps xs; prefix ps ys \<rbrakk>
\<Longrightarrow> prefix ps (longest_common_prefix xs ys)"
-by(induction xs ys arbitrary: ps rule: longest_common_prefix.induct)
- (auto simp: prefix_Cons)
+ by(induction xs ys arbitrary: ps rule: longest_common_prefix.induct)
+ (auto simp: prefix_Cons)
subsection \<open>Parallel lists\<close>
@@ -506,10 +506,7 @@
qed
lemma parallel_append: "a \<parallel> b \<Longrightarrow> a @ c \<parallel> b @ d"
- apply (rule parallelI)
- apply (erule parallelE, erule conjE,
- induct rule: not_prefix_induct, simp+)+
- done
+ by (meson parallelE parallelI prefixI prefix_order.trans prefix_same_cases)
lemma parallel_appendI: "xs \<parallel> ys \<Longrightarrow> x = xs @ xs' \<Longrightarrow> y = ys @ ys' \<Longrightarrow> x \<parallel> y"
by (simp add: parallel_append)
@@ -1265,31 +1262,13 @@
by (auto simp: sublist_def intro: exI[of _ "[]"])
lemma sublist_append_rightI [simp, intro]: "sublist xs (xs @ ss)"
- by (auto simp: sublist_def intro: exI[of _ "[]"])
+ by (metis append_eq_append_conv2 sublist_appendI)
lemma sublist_altdef: "sublist xs ys \<longleftrightarrow> (\<exists>ys'. prefix ys' ys \<and> suffix xs ys')"
-proof safe
- assume "sublist xs ys"
- then obtain ps ss where "ys = ps @ xs @ ss" by (auto simp: sublist_def)
- thus "\<exists>ys'. prefix ys' ys \<and> suffix xs ys'"
- by (intro exI[of _ "ps @ xs"] conjI suffix_appendI) auto
-next
- fix ys'
- assume "prefix ys' ys" "suffix xs ys'"
- thus "sublist xs ys" by (auto simp: prefix_def suffix_def)
-qed
+ by (metis append_assoc prefix_def sublist_def suffix_def)
lemma sublist_altdef': "sublist xs ys \<longleftrightarrow> (\<exists>ys'. suffix ys' ys \<and> prefix xs ys')"
-proof safe
- assume "sublist xs ys"
- then obtain ps ss where "ys = ps @ xs @ ss" by (auto simp: sublist_def)
- thus "\<exists>ys'. suffix ys' ys \<and> prefix xs ys'"
- by (intro exI[of _ "xs @ ss"] conjI suffixI) auto
-next
- fix ys'
- assume "suffix ys' ys" "prefix xs ys'"
- thus "sublist xs ys" by (auto simp: prefix_def suffix_def)
-qed
+ by (metis prefixE prefixI sublist_appendI sublist_def suffixE suffixI)
lemma sublist_Cons_right: "sublist xs (y # ys) \<longleftrightarrow> prefix xs (y # ys) \<or> sublist xs ys"
by (auto simp: sublist_def prefix_def Cons_eq_append_conv)
@@ -1453,8 +1432,8 @@
qed
private lemma list_emb_primrec:
- "list_emb = (\<lambda>uu uua uuaa. rec_list (\<lambda>P xs. List.null xs) (\<lambda>y ys ysa P xs. case xs of [] \<Rightarrow> True
- | x # xs \<Rightarrow> if P x y then ysa P xs else ysa P (x # xs)) uuaa uu uua)"
+ "list_emb = (\<lambda>uu l' l. rec_list (\<lambda>P xs. List.null xs) (\<lambda>y ys ysa P xs. case xs of [] \<Rightarrow> True
+ | x # xs \<Rightarrow> if P x y then ysa P xs else ysa P (x # xs)) l uu l')"
proof (intro ext, goal_cases)
case (1 P xs ys)
show ?case
--- a/src/HOL/Set_Interval.thy Mon Mar 03 13:19:23 2025 +0100
+++ b/src/HOL/Set_Interval.thy Mon Mar 03 19:52:18 2025 +0100
@@ -320,6 +320,30 @@
with * show "a = b \<and> b = c" by auto
qed simp
+text \<open>Quantifiers\<close>
+
+lemma ex_interval_simps:
+ "(\<exists>x \<in> {..<u}. P x) \<longleftrightarrow> (\<exists>x<u. P x)"
+ "(\<exists>x \<in> {..u}. P x) \<longleftrightarrow> (\<exists>x\<le>u. P x)"
+ "(\<exists>x \<in> {l<..}. P x) \<longleftrightarrow> (\<exists>x>l. P x)"
+ "(\<exists>x \<in> {l..}. P x) \<longleftrightarrow> (\<exists>x\<ge>l. P x)"
+ "(\<exists>x \<in> {l<..<u}. P x) \<longleftrightarrow> (\<exists>x. l<x \<and> x<u \<and> P x)"
+ "(\<exists>x \<in> {l..<u}. P x) \<longleftrightarrow> (\<exists>x. l\<le>x \<and> x<u \<and> P x)"
+ "(\<exists>x \<in> {l<..u}. P x) \<longleftrightarrow> (\<exists>x. l<x \<and> x\<le>u \<and> P x)"
+ "(\<exists>x \<in> {l..u}. P x) \<longleftrightarrow> (\<exists>x. l\<le>x \<and> x\<le>u \<and> P x)"
+ by auto
+
+lemma all_interval_simps:
+ "(\<forall>x \<in> {..<u}. P x) \<longleftrightarrow> (\<forall>x<u. P x)"
+ "(\<forall>x \<in> {..u}. P x) \<longleftrightarrow> (\<forall>x\<le>u. P x)"
+ "(\<forall>x \<in> {l<..}. P x) \<longleftrightarrow> (\<forall>x>l. P x)"
+ "(\<forall>x \<in> {l..}. P x) \<longleftrightarrow> (\<forall>x\<ge>l. P x)"
+ "(\<forall>x \<in> {l<..<u}. P x) \<longleftrightarrow> (\<forall>x. l<x \<longrightarrow> x<u \<longrightarrow> P x)"
+ "(\<forall>x \<in> {l..<u}. P x) \<longleftrightarrow> (\<forall>x. l\<le>x \<longrightarrow> x<u \<longrightarrow> P x)"
+ "(\<forall>x \<in> {l<..u}. P x) \<longleftrightarrow> (\<forall>x. l<x \<longrightarrow> x\<le>u \<longrightarrow> P x)"
+ "(\<forall>x \<in> {l..u}. P x) \<longleftrightarrow> (\<forall>x. l\<le>x \<longrightarrow> x\<le>u \<longrightarrow> P x)"
+ by auto
+
text \<open>The following results generalise their namesakes in @{theory HOL.Nat} to intervals\<close>
lemma lift_Suc_mono_le_ivl:
--- a/src/HOL/Sledgehammer.thy Mon Mar 03 13:19:23 2025 +0100
+++ b/src/HOL/Sledgehammer.thy Mon Mar 03 19:52:18 2025 +0100
@@ -29,6 +29,7 @@
ML_file \<open>Tools/Sledgehammer/sledgehammer_prover.ML\<close>
ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_atp.ML\<close>
ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_smt.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_tactic.ML\<close>
ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_minimize.ML\<close>
ML_file \<open>Tools/Sledgehammer/sledgehammer_mepo.ML\<close>
ML_file \<open>Tools/Sledgehammer/sledgehammer_mash.ML\<close>
--- a/src/HOL/TPTP/atp_problem_import.ML Mon Mar 03 13:19:23 2025 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML Mon Mar 03 19:52:18 2025 +0100
@@ -12,7 +12,7 @@
val nitpick_tptp_file : theory -> int -> string -> unit
val refute_tptp_file : theory -> int -> string -> unit
val can_tac : Proof.context -> (Proof.context -> tactic) -> term -> bool
- val SOLVE_TIMEOUT : int -> string -> tactic -> tactic
+ val SOLVE_TIMEOUT : int -> string -> tactic -> tactic
val atp_tac : local_theory -> int -> (string * string) list -> int -> term list -> string ->
int -> tactic
val smt_solver_tac : string -> local_theory -> int -> tactic
--- a/src/HOL/Tools/SMT/smt_systems.ML Mon Mar 03 13:19:23 2025 +0100
+++ b/src/HOL/Tools/SMT/smt_systems.ML Mon Mar 03 19:52:18 2025 +0100
@@ -104,13 +104,13 @@
smt_options = [(":produce-unsat-cores", "true")],
good_slices =
(* FUDGE *)
- [((2, false, false, 512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]),
- ((2, false, false, 64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]),
- ((2, false, true, 256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]),
- ((2, false, false, 1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]),
- ((2, false, false, 32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]),
- ((2, false, false, 128, meshN), ["--no-e-matching", "--full-saturate-quant"]),
- ((2, false, false, 256, meshN), ["--finite-model-find", "--fmf-inst-engine"])],
+ [((4, false, false, 512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]),
+ ((4, false, false, 64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]),
+ ((4, false, true, 256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]),
+ ((4, false, false, 1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]),
+ ((4, false, false, 32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]),
+ ((4, false, false, 128, meshN), ["--no-e-matching", "--full-saturate-quant"]),
+ ((4, false, false, 256, meshN), ["--finite-model-find", "--fmf-inst-engine"])],
outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
parse_proof = SOME (K CVC_Proof_Parse.parse_proof),
replay = NONE }
@@ -148,13 +148,13 @@
smt_options = [(":produce-proofs", "true")],
good_slices =
(* FUDGE *)
- [((2, false, false, 512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]),
- ((2, false, false, 64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]),
- ((2, false, true, 256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]),
- ((2, false, false, 1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]),
- ((2, false, false, 32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]),
- ((2, false, false, 128, meshN), ["--no-e-matching", "--full-saturate-quant"]),
- ((2, false, false, 256, meshN), ["--finite-model-find", "--fmf-inst-engine"])],
+ [((4, false, false, 512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]),
+ ((4, false, false, 64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]),
+ ((4, false, true, 256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]),
+ ((4, false, false, 1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]),
+ ((4, false, false, 32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]),
+ ((4, false, false, 128, meshN), ["--no-e-matching", "--full-saturate-quant"]),
+ ((4, false, false, 256, meshN), ["--finite-model-find", "--fmf-inst-engine"])],
outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
parse_proof = SOME (K CVC_Proof_Parse.parse_proof),
replay = SOME CVC5_Replay.replay }
@@ -193,12 +193,12 @@
smt_options = [(":produce-proofs", "true")],
good_slices =
(* FUDGE *)
- [((2, false, false, 1024, meshN), []),
- ((2, false, false, 512, mashN), []),
- ((2, false, true, 128, meshN), []),
- ((2, false, false, 64, meshN), []),
- ((2, false, false, 256, mepoN), []),
- ((2, false, false, 32, meshN), [])],
+ [((4, false, false, 1024, meshN), []),
+ ((4, false, false, 512, mashN), []),
+ ((4, false, true, 128, meshN), []),
+ ((4, false, false, 64, meshN), []),
+ ((4, false, false, 256, mepoN), []),
+ ((4, false, false, 32, meshN), [])],
outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown" "Time limit exceeded"),
parse_proof = SOME (K Lethe_Proof_Parse.parse_proof),
replay = SOME Verit_Replay.replay }
@@ -234,12 +234,12 @@
smt_options = [(":produce-proofs", "true")],
good_slices =
(* FUDGE *)
- [((2, false, false, 1024, meshN), []),
- ((2, false, false, 512, mepoN), []),
- ((2, false, false, 64, meshN), []),
- ((2, false, true, 256, meshN), []),
- ((2, false, false, 128, mashN), []),
- ((2, false, false, 32, meshN), [])],
+ [((4, false, false, 1024, meshN), []),
+ ((4, false, false, 512, mepoN), []),
+ ((4, false, false, 64, meshN), []),
+ ((4, false, true, 256, meshN), []),
+ ((4, false, false, 128, mashN), []),
+ ((4, false, false, 32, meshN), [])],
outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
parse_proof = SOME Z3_Replay.parse_proof,
replay = SOME Z3_Replay.replay }
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Mar 03 13:19:23 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Mar 03 19:52:18 2025 +0100
@@ -51,6 +51,7 @@
open Sledgehammer_ATP_Systems
open Sledgehammer_Prover
open Sledgehammer_Prover_ATP
+open Sledgehammer_Prover_Tactic
open Sledgehammer_Prover_Minimize
open Sledgehammer_MaSh
@@ -239,8 +240,9 @@
val preplay = `(fn pretty_used_facts =>
play_one_line_proofs minimize preplay_timeout pretty_used_facts
state goal subgoal (snd preferred_methss))
- fun preplay_succeeded ((_, (Played _, _)) :: _, _) = true
- | preplay_succeeded _ = false
+ fun preplay_succeeded ((_, (Played _, _)) :: _, _) _ = true
+ | preplay_succeeded _ [] = true
+ | preplay_succeeded _ _ = false
val instantiate_timeout = Time.scale 5.0 preplay_timeout
val instantiate = if null used_facts0 then SOME false else instantiate
val (preplay_results, pretty_used_facts) =
@@ -255,7 +257,7 @@
let
val preplay_results0 = preplay pretty_used_facts0
in
- if preplay_succeeded preplay_results0 then
+ if preplay_succeeded preplay_results0 (snd preferred_methss) then
preplay_results0
else
(* Preplay failed, now try to infer variable instantiations *)
@@ -437,7 +439,7 @@
extra_extra0)) =
ATP_Slice (format0, the_default type_enc0 type_enc, the_default lam_trans0 lam_trans,
the_default uncurried_aliases0 uncurried_aliases, extra_extra0)
- | adjust_extra (extra as SMT_Slice _) = extra
+ | adjust_extra extra = extra
fun adjust_slice max_slice_size
((slice_size0, abduce0, falsify0, num_facts0, fact_filter0), extra) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Mar 03 13:19:23 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Mar 03 19:52:18 2025 +0100
@@ -25,6 +25,7 @@
open Sledgehammer_ATP_Systems
open Sledgehammer_Prover
open Sledgehammer_Prover_SMT
+open Sledgehammer_Prover_Tactic
open Sledgehammer_Prover_Minimize
open Sledgehammer_MaSh
open Sledgehammer
@@ -73,7 +74,7 @@
("smt_proofs", "true"),
("instantiate", "smart"),
("minimize", "true"),
- ("slices", string_of_int (12 * Multithreading.max_threads ())),
+ ("slices", string_of_int (24 * Multithreading.max_threads ())),
("preplay_timeout", "1"),
("cache_dir", "")]
@@ -170,7 +171,7 @@
(* The first ATP of the list is used by Auto Sledgehammer. *)
fun default_provers_param_value ctxt =
\<comment> \<open>see also \<^system_option>\<open>sledgehammer_provers\<close>\<close>
- filter (is_prover_installed ctxt) (smts ctxt @ local_atps)
+ filter (is_prover_installed ctxt) (smt_solvers ctxt @ local_atps @ tactic_provers)
|> implode_param
fun set_default_raw_param param thy =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Mar 03 13:19:23 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Mar 03 19:52:18 2025 +0100
@@ -160,7 +160,7 @@
isar_params ()
in
if null atp_proof0 then
- one_line_proof_text ctxt 0 one_line_params
+ one_line_proof_text one_line_params
else
let
val systematic_methods' = insert (op =) (Metis_Method alt_metis_args) systematic_methods
@@ -475,7 +475,7 @@
in
(case (num_chained, add_isar_steps (steps_of_isar_proof isar_proof) 0) of
(0, 1) =>
- one_line_proof_text ctxt 0
+ one_line_proof_text
(if is_less (play_outcome_ord (play_outcome, one_line_play)) then
(case isar_proof of
Proof {steps = [Prove {qualifiers = [Show], facts = (_, gfs),
@@ -502,7 +502,7 @@
else []) @
(if do_preplay then [string_of_play_outcome play_outcome] else [])
in
- one_line_proof_text ctxt 0 one_line_params ^
+ one_line_proof_text one_line_params ^
(if isar_proofs <> NONE orelse (case play_outcome of Played _ => true | _ => false) then
"\n\nIsar proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
Active.sendback_markup_command
@@ -519,7 +519,7 @@
(case try generate_proof_text () of
SOME s => s
| NONE =>
- one_line_proof_text ctxt 0 one_line_params ^
+ one_line_proof_text one_line_params ^
(if isar_proofs = SOME true then "\nWarning: Isar proof construction failed" else ""))
end
@@ -535,7 +535,7 @@
(isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then
isar_proof_text ctxt debug num_chained isar_proofs smt_proofs isar_params
else
- one_line_proof_text ctxt num_chained) one_line_params
+ one_line_proof_text) one_line_params
fun abduce_text ctxt tms =
"Candidate missing assumption" ^ plural_s (length tms) ^ ":\n" ^
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Mar 03 13:19:23 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Mar 03 19:52:18 2025 +0100
@@ -159,6 +159,7 @@
Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
HEADGOAL (tac_of_proof_method ctxt assmsp meth))
handle ERROR msg => error ("Preplay error: " ^ msg)
+ | Exn.Interrupt_Breakdown => error "Preplay error"
val play_outcome = take_time timeout prove ()
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Mon Mar 03 13:19:23 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Mon Mar 03 19:52:18 2025 +0100
@@ -44,7 +44,7 @@
val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
val string_of_play_outcome : play_outcome -> string
val play_outcome_ord : play_outcome ord
- val one_line_proof_text : Proof.context -> int -> one_line_params -> string
+ val one_line_proof_text : one_line_params -> string
end;
structure Sledgehammer_Proof_Methods : SLEDGEHAMMER_PROOF_METHODS =
@@ -220,7 +220,7 @@
| apply_on_subgoal i n = "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
(* FIXME *)
-fun proof_method_command meth i n used_chaineds _(*num_chained*) extras =
+fun proof_method_command meth i n used_chaineds extras =
let
val (indirect_facts, direct_facts) =
if is_proof_method_direct meth then ([], extras) else (extras, [])
@@ -246,11 +246,10 @@
(* Add optional markup break (command may need multiple lines) *)
Markup.markup (Markup.break {width = 1, indent = 2}) " ")
-fun one_line_proof_text _ num_chained
- ((used_facts, (meth, play)), banner, subgoal, subgoal_count) =
+fun one_line_proof_text ((used_facts, (meth, play)), banner, subgoal, subgoal_count) =
let val (chained, extra) = List.partition (fn (_, (sc, _)) => sc = Chained) used_facts in
map fst extra
- |> proof_method_command meth subgoal subgoal_count (map fst chained) num_chained
+ |> proof_method_command meth subgoal subgoal_count (map fst chained)
|> (if play = Play_Failed then failed_command_line else try_command_line banner play)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Mar 03 13:19:23 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Mar 03 19:52:18 2025 +0100
@@ -72,6 +72,7 @@
datatype prover_slice_extra =
ATP_Slice of atp_slice
| SMT_Slice of string list
+ | No_Slice
type prover_slice = base_slice * prover_slice_extra
@@ -199,6 +200,7 @@
datatype prover_slice_extra =
ATP_Slice of atp_slice
| SMT_Slice of string list
+| No_Slice
type prover_slice = base_slice * prover_slice_extra
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Mar 03 13:19:23 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Mar 03 19:52:18 2025 +0100
@@ -14,6 +14,7 @@
type params = Sledgehammer_Prover.params
type prover = Sledgehammer_Prover.prover
type prover_slice = Sledgehammer_Prover.prover_slice
+ type prover_result = Sledgehammer_Prover.prover_result
val is_prover_supported : Proof.context -> string -> bool
val is_prover_installed : Proof.context -> string -> bool
@@ -22,7 +23,7 @@
val binary_min_facts : int Config.T
val minimize_facts : (thm list -> unit) -> string -> params -> prover_slice -> bool -> int ->
- int -> Proof.state -> thm -> ((string * stature) * thm list) list ->
+ int -> Proof.state -> thm -> ((string * stature) * thm list) list -> prover_result ->
((string * stature) * thm list) list option
* ((unit -> (Pretty.T * stature) list * (proof_method * play_outcome)) -> string)
val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover
@@ -43,29 +44,35 @@
open Sledgehammer_Prover
open Sledgehammer_Prover_ATP
open Sledgehammer_Prover_SMT
+open Sledgehammer_Prover_Tactic
fun is_prover_supported ctxt =
- is_atp orf is_smt_prover ctxt
+ is_atp orf is_smt_solver ctxt orf is_tactic_prover
fun is_prover_installed ctxt prover_name =
if is_atp prover_name then
let val thy = Proof_Context.theory_of ctxt in
is_atp_installed thy prover_name
end
+ else if is_smt_solver ctxt prover_name then
+ is_smt_solver_installed ctxt prover_name
else
- is_smt_prover_installed ctxt prover_name
+ true
fun get_prover ctxt mode name =
if is_atp name then run_atp mode name
- else if is_smt_prover ctxt name then run_smt_solver mode name
+ else if is_smt_solver ctxt name then run_smt_solver mode name
+ else if is_tactic_prover name then run_tactic_prover mode name
else error ("No such prover: " ^ name)
fun get_slices ctxt name =
let val thy = Proof_Context.theory_of ctxt in
if is_atp name then
map (apsnd ATP_Slice) (#good_slices (get_atp thy name ()) ctxt)
- else if is_smt_prover ctxt name then
+ else if is_smt_solver ctxt name then
map (apsnd SMT_Slice) (SMT_Solver.good_slices ctxt name)
+ else if is_tactic_prover name then
+ map (rpair No_Slice) (good_slices_of_tactic_prover name)
else
error ("No such prover: " ^ name)
end
@@ -83,7 +90,7 @@
fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs,
instantiate, minimize, preplay_timeout, induction_rules, cache_dir, ...} : params)
- (slice as ((_, _, falsify, _, fact_filter), slice_extra)) silent (prover : prover) timeout i n
+ ((_, _, falsify, _, fact_filter), slice_extra) silent (prover : prover) timeout i n
state goal facts =
let
val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^
@@ -200,7 +207,7 @@
end
fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) slice silent i n state
- goal facts =
+ goal facts result =
let
val ctxt = Proof.context_of state
val prover = get_prover ctxt Minimize prover_name
@@ -208,32 +215,37 @@
fun test timeout non_chained =
test_facts params slice silent prover timeout i n state goal (chained @ non_chained)
+
+ fun minimize used_facts (result as {run_time, ...}) =
+ let
+ val non_chained = filter_used_facts true used_facts non_chained
+ val min =
+ if length non_chained >= Config.get ctxt binary_min_facts then binary_minimize
+ else linear_minimize
+ val (min_facts, {message, ...}) =
+ min test (new_timeout timeout run_time) result non_chained
+ val min_facts_and_chained = chained @ min_facts
+ in
+ print silent (fn () => cat_lines
+ ["Minimized to " ^ n_facts (map fst min_facts)] ^
+ (case length chained of
+ 0 => ""
+ | n => " (plus " ^ string_of_int n ^ " chained)"));
+ (if learn then do_learn (maps snd min_facts_and_chained) else ());
+ (SOME min_facts_and_chained, message)
+ end
in
(print silent (fn () => "Sledgehammer minimizer: " ^ prover_name);
- (case test timeout non_chained of
- result as {outcome = NONE, used_facts, run_time, ...} =>
- let
- val non_chained = filter_used_facts true used_facts non_chained
- val min =
- if length non_chained >= Config.get ctxt binary_min_facts then binary_minimize
- else linear_minimize
- val (min_facts, {message, ...}) =
- min test (new_timeout timeout run_time) result non_chained
- val min_facts_and_chained = chained @ min_facts
- in
- print silent (fn () => cat_lines
- ["Minimized to " ^ n_facts (map fst min_facts)] ^
- (case length chained of
- 0 => ""
- | n => " (plus " ^ string_of_int n ^ " chained)"));
- (if learn then do_learn (maps snd min_facts_and_chained) else ());
- (SOME min_facts_and_chained, message)
- end
- | {outcome = SOME TimedOut, ...} =>
- (NONE, fn _ =>
- "Timeout: You can increase the time limit using the \"timeout\" option (e.g., \
- \timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\")")
- | {message, ...} => (NONE, (prefix "Prover error: " o message))))
+ if is_tactic_prover prover_name then
+ minimize (map fst facts) result
+ else
+ (case test timeout non_chained of
+ result as {outcome = NONE, used_facts, ...} => minimize used_facts result
+ | {outcome = SOME TimedOut, ...} =>
+ (NONE, fn _ =>
+ "Timeout: You can increase the time limit using the \"timeout\" option (e.g., \
+ \timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\")")
+ | {message, ...} => (NONE, (prefix "Prover error: " o message))))
handle ERROR msg => (NONE, fn _ => "Warning: " ^ msg)
end
@@ -249,7 +261,7 @@
if minimize then
minimize_facts do_learn name params slice
(not verbose orelse (mode <> Normal andalso mode <> MaSh)) subgoal subgoal_count state
- goal (filter_used_facts true used_facts (map (apsnd single) used_from))
+ goal (filter_used_facts true used_facts (map (apsnd single) used_from)) result
|>> Option.map (map fst)
else
(SOME used_facts, message)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Mar 03 13:19:23 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Mar 03 19:52:18 2025 +0100
@@ -15,11 +15,11 @@
val smt_builtins : bool Config.T
val smt_triggers : bool Config.T
- val is_smt_prover : Proof.context -> string -> bool
- val is_smt_prover_installed : Proof.context -> string -> bool
+ val is_smt_solver : Proof.context -> string -> bool
+ val is_smt_solver_installed : Proof.context -> string -> bool
val run_smt_solver : mode -> string -> prover
- val smts : Proof.context -> string list
+ val smt_solvers : Proof.context -> string list
end;
structure Sledgehammer_Prover_SMT : SLEDGEHAMMER_PROVER_SMT =
@@ -38,10 +38,10 @@
val smt_builtins = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_smt_builtins\<close> (K true)
val smt_triggers = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_smt_triggers\<close> (K true)
-val smts = sort_strings o SMT_Config.all_solvers_of
+val smt_solvers = sort_strings o SMT_Config.all_solvers_of
-val is_smt_prover = member (op =) o smts
-val is_smt_prover_installed = member (op =) o SMT_Config.available_solvers_of
+val is_smt_solver = member (op =) o smt_solvers
+val is_smt_solver_installed = member (op =) o SMT_Config.available_solvers_of
(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out
properly in the SMT module, we must interpret these here. *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML Mon Mar 03 19:52:18 2025 +0100
@@ -0,0 +1,141 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML
+ Author: Jasmin Blanchette, LMU Muenchen
+
+Isabelle tactics as Sledgehammer provers.
+*)
+
+signature SLEDGEHAMMER_PROVER_TACTIC =
+sig
+ type stature = ATP_Problem_Generate.stature
+ type mode = Sledgehammer_Prover.mode
+ type prover = Sledgehammer_Prover.prover
+ type base_slice = Sledgehammer_ATP_Systems.base_slice
+
+ val algebraN : string
+ val argoN : string
+ val autoN : string
+ val blastN : string
+ val fastforceN : string
+ val forceN : string
+ val linarithN : string
+ val mesonN : string
+ val metisN : string
+ val orderN : string
+ val presburgerN : string
+ val satxN : string
+ val simpN : string
+
+ val tactic_provers : string list
+ val is_tactic_prover : string -> bool
+ val good_slices_of_tactic_prover : string -> base_slice list
+ val run_tactic_prover : mode -> string -> prover
+end;
+
+structure Sledgehammer_Prover_Tactic : SLEDGEHAMMER_PROVER_TACTIC =
+struct
+
+open ATP_Problem_Generate
+open ATP_Proof
+open Sledgehammer_ATP_Systems
+open Sledgehammer_Proof_Methods
+open Sledgehammer_Prover
+
+val algebraN = "algebra"
+val argoN = "argo"
+val autoN = "auto"
+val blastN = "blast"
+val fastforceN = "fastforce"
+val forceN = "force"
+val linarithN = "linarith"
+val mesonN = "meson"
+val metisN = "metis"
+val orderN = "order"
+val presburgerN = "presburger"
+val satxN = "satx"
+val simpN = "simp"
+
+val tactic_provers =
+ [algebraN, argoN, autoN, blastN, fastforceN, forceN, linarithN, mesonN,
+ metisN, orderN, presburgerN, satxN, simpN]
+
+val is_tactic_prover = member (op =) tactic_provers
+
+val meshN = "mesh"
+
+fun good_slices_of_tactic_prover _ =
+ (* FUDGE *)
+ [(1, false, false, 0, meshN),
+ (1, false, false, 2, meshN),
+ (1, false, false, 8, meshN),
+ (1, false, false, 32, meshN)]
+
+fun meth_of name =
+ if name = algebraN then Algebra_Method
+ else if name = argoN then Argo_Method
+ else if name = autoN then Auto_Method
+ else if name = blastN then Blast_Method
+ else if name = fastforceN then Fastforce_Method
+ else if name = forceN then Force_Method
+ else if name = linarithN then Linarith_Method
+ else if name = mesonN then Meson_Method
+ else if name = metisN then Metis_Method (NONE, NONE, [])
+ else if name = orderN then Order_Method
+ else if name = presburgerN then Presburger_Method
+ else if name = satxN then SATx_Method
+ else if name = simpN then Simp_Method
+ else error ("Unknown tactic: " ^ quote name)
+
+fun tac_of ctxt name (local_facts, global_facts) =
+ Sledgehammer_Proof_Methods.tac_of_proof_method ctxt (local_facts, global_facts) (meth_of name)
+
+fun run_tactic_prover mode name ({slices, timeout, ...} : params)
+ ({state, goal, subgoal, subgoal_count, factss, found_something, ...} : prover_problem) slice =
+ let
+ val (basic_slice as (slice_size, _, _, _, _), No_Slice) = slice
+ val facts = facts_of_basic_slice basic_slice factss
+ val {facts = chained, ...} = Proof.goal state
+ val ctxt = Proof.context_of state
+
+ val (local_facts, global_facts) =
+ ([], [])
+ |> fold (fn ((_, (scope, _)), thm) =>
+ if scope = Global then apsnd (cons thm)
+ else if scope = Chained then I
+ else apfst (cons thm)) facts
+ |> apfst (append chained)
+
+ val run_timeout = slice_timeout slice_size slices timeout
+
+ val timer = Timer.startRealTimer ()
+
+ val out =
+ (Timeout.apply run_timeout
+ (Goal.prove ctxt [] [] (Logic.get_goal (Thm.prop_of goal) subgoal))
+ (fn {context = ctxt, ...} =>
+ HEADGOAL (tac_of ctxt name (local_facts, global_facts)));
+ NONE)
+ handle ERROR _ => SOME GaveUp
+ | Exn.Interrupt_Breakdown => SOME GaveUp
+ | Timeout.TIMEOUT _ => SOME TimedOut
+
+ val run_time = Timer.checkRealTimer timer
+
+ val (outcome, used_facts) =
+ (case out of
+ NONE =>
+ (found_something name;
+ (NONE, map fst facts))
+ | some_failure => (some_failure, []))
+
+ val message = fn _ =>
+ (case outcome of
+ NONE =>
+ one_line_proof_text ((map (apfst Pretty.str) used_facts, (meth_of name, Played run_time)),
+ proof_banner mode name, subgoal, subgoal_count)
+ | SOME failure => string_of_atp_failure failure)
+ in
+ {outcome = outcome, used_facts = used_facts, used_from = facts,
+ preferred_methss = (meth_of name, []), run_time = run_time, message = message}
+ end
+
+end;
--- a/src/HOL/Tools/try0.ML Mon Mar 03 13:19:23 2025 +0100
+++ b/src/HOL/Tools/try0.ML Mon Mar 03 19:52:18 2025 +0100
@@ -6,12 +6,14 @@
signature TRY0 =
sig
- val noneN : string
val silence_methods : bool -> Proof.context -> Proof.context
datatype modifier = Use | Simp | Intro | Elim | Dest
- type result = {name: string, command: string, time: int, state: Proof.state}
- val try0 : Time.time option -> ((Facts.ref * Token.src list) * modifier list) list ->
- Proof.state -> result list
+ type xthm = Facts.ref * Token.src list
+ type tagged_xthm = xthm * modifier list
+ type result = {name: string, command: string, time: Time.time, state: Proof.state}
+ val apply_proof_method : string -> Time.time option -> (xthm * modifier list) list ->
+ Proof.state -> result option
+ val try0 : Time.time option -> tagged_xthm list -> Proof.state -> result list
end
structure Try0 : TRY0 =
@@ -46,64 +48,27 @@
|> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source")
datatype modifier = Use | Simp | Intro | Elim | Dest
+type xthm = Facts.ref * Token.src list
+type tagged_xthm = xthm * modifier list
-fun string_of_xthm (xref, args) =
+fun string_of_xthm ((xref, args) : xthm) =
(case xref of
Facts.Fact literal => literal |> Symbol_Pos.explode0 |> Symbol_Pos.implode |> cartouche
| _ =>
Facts.string_of_ref xref) ^ implode
(map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src \<^context>) args)
-fun add_attr_text tagged (tag, src) s =
+fun add_attr_text (tagged : tagged_xthm list) (tag, src) s =
let
val fs = tagged |> filter (fn (_, tags) => member (op =) tags tag) |> map (string_of_xthm o fst)
in if null fs then s else s ^ " " ^ (if src = "" then "" else src ^ ": ") ^ implode_space fs end
-fun attrs_text tags tagged =
+fun attrs_text tags (tagged : tagged_xthm list) =
"" |> fold (add_attr_text tagged) tags
-type result = {name: string, command: string, time: int, state: Proof.state}
-
-fun apply_named_method (name, ((all_goals, run_if_auto_try), attrs)) mode timeout_opt tagged st =
- if mode <> Auto_Try orelse run_if_auto_try then
- let
- val unused =
- tagged
- |> filter
- (fn (_, tags) => not (null tags) andalso null (inter (op =) tags (attrs |> map fst)))
- |> map fst
-
- val attrs = attrs_text attrs tagged
-
- val ctxt = Proof.context_of st
+type result = {name: string, command: string, time: Time.time, state: Proof.state}
- val text =
- name ^ attrs
- |> parse_method ctxt
- |> Method.method_cmd ctxt
- |> Method.Basic
- |> (fn m => Method.Combinator (Method.no_combinator_info, Method.Select_Goals 1, [m]))
-
- val apply =
- Proof.using [Attrib.eval_thms ctxt unused |> map (rpair [] o single)]
- #> Proof.refine text #> Seq.filter_results
- val num_before = num_goals st
- val multiple_goals = all_goals andalso num_before > 1
- val (time, st') = apply_recursive multiple_goals Time.zeroTime timeout_opt apply st
- val num_after = num_goals st'
- val select = "[" ^ string_of_int (num_before - num_after) ^ "]"
- val unused = implode_space (unused |> map string_of_xthm)
- val command =
- (if unused <> "" then "using " ^ unused ^ " " else "") ^
- (if num_after = 0 then "by " else "apply ") ^
- (name ^ attrs |> attrs <> "" ? enclose "(" ")") ^
- (if multiple_goals andalso num_after > 0 then select else "")
- in
- if num_before > num_after then
- SOME {name = name, command = command, time = Time.toMilliseconds time, state = st'}
- else NONE
- end
- else NONE
+local
val full_attrs = [(Simp, "simp"), (Intro, "intro"), (Elim, "elim"), (Dest, "dest")]
val clas_attrs = [(Intro, "intro"), (Elim, "elim"), (Dest, "dest")]
@@ -112,7 +77,7 @@
val no_attrs = []
(* name * ((all_goals, run_if_auto_try), tags *)
-val named_methods =
+val raw_named_methods =
[("simp", ((false, true), simp_attrs)),
("auto", ((true, true), full_attrs)),
("blast", ((false, true), clas_attrs)),
@@ -128,10 +93,72 @@
("satx", ((false, false), no_attrs)),
("order", ((false, true), no_attrs))]
-val apply_methods = map apply_named_method named_methods
+fun apply_raw_named_method (name, ((all_goals, _), attrs)) timeout_opt tagged st :
+ result option =
+ let
+ val unused =
+ tagged
+ |> filter
+ (fn (_, tags) => not (null tags) andalso null (inter (op =) tags (attrs |> map fst)))
+ |> map fst
+
+ val attrs = attrs_text attrs tagged
+
+ val ctxt = Proof.context_of st
+
+ val text =
+ name ^ attrs
+ |> parse_method ctxt
+ |> Method.method_cmd ctxt
+ |> Method.Basic
+ |> (fn m => Method.Combinator (Method.no_combinator_info, Method.Select_Goals 1, [m]))
-fun time_string ms = string_of_int ms ^ " ms"
-fun tool_time_string (s, ms) = s ^ ": " ^ time_string ms
+ val apply =
+ Proof.using [Attrib.eval_thms ctxt unused |> map (rpair [] o single)]
+ #> Proof.refine text #> Seq.filter_results
+ val num_before = num_goals st
+ val multiple_goals = all_goals andalso num_before > 1
+ val (time, st') = apply_recursive multiple_goals Time.zeroTime timeout_opt apply st
+ val num_after = num_goals st'
+ val select = "[" ^ string_of_int (num_before - num_after) ^ "]"
+ val unused = implode_space (unused |> map string_of_xthm)
+ val command =
+ (if unused <> "" then "using " ^ unused ^ " " else "") ^
+ (if num_after = 0 then "by " else "apply ") ^
+ (name ^ attrs |> attrs <> "" ? enclose "(" ")") ^
+ (if multiple_goals andalso num_after > 0 then select else "")
+ in
+ if num_before > num_after then
+ SOME {name = name, command = command, time = time, state = st'}
+ else NONE
+ end
+
+in
+
+val named_methods = map fst raw_named_methods
+
+fun apply_proof_method name timeout_opt tagged st :
+ result option =
+ (case AList.lookup (op =) raw_named_methods name of
+ NONE => NONE
+ | SOME raw_method => apply_raw_named_method (name, raw_method) timeout_opt tagged st)
+
+fun maybe_apply_proof_method name mode timeout_opt tagged st :
+ result option =
+ (case AList.lookup (op =) raw_named_methods name of
+ NONE => NONE
+ | SOME (raw_method as ((_, run_if_auto_try), _)) =>
+ if mode <> Auto_Try orelse run_if_auto_try then
+ apply_raw_named_method (name, raw_method) timeout_opt tagged st
+ else
+ NONE)
+
+end
+
+val maybe_apply_methods = map maybe_apply_proof_method named_methods
+
+fun time_string time = string_of_int (Time.toMilliseconds time) ^ " ms"
+fun tool_time_string (s, time) = s ^ ": " ^ time_string time
(* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification
bound exceeded" warnings and the like. *)
@@ -144,25 +171,31 @@
|> Config.put Unify.unify_trace false
|> Config.put Argo_Tactic.trace "none")
-fun generic_try0 mode timeout_opt tagged st =
+fun generic_try0 mode timeout_opt (tagged : tagged_xthm list) st =
let
val st = Proof.map_contexts (silence_methods false) st
fun try_method method = method mode timeout_opt tagged st
fun get_message {command, time, ...} = "Found proof: " ^ Active.sendback_markup_command
command ^ " (" ^ time_string time ^ ")"
val print_step = Option.map (tap (writeln o get_message))
- val get_results =
- if mode = Normal
- then Par_List.map (try_method #> print_step) #> map_filter I #> sort (int_ord o apply2 #time)
- else Par_List.get_some try_method #> the_list
+ fun get_results methods : result list =
+ if mode = Normal then
+ methods
+ |> Par_List.map (try_method #> print_step)
+ |> map_filter I
+ |> sort (Time.compare o apply2 #time)
+ else
+ methods
+ |> Par_List.get_some try_method
+ |> the_list
in
if mode = Normal then
- "Trying " ^ implode_space (Try.serial_commas "and" (map (quote o fst) named_methods)) ^
+ "Trying " ^ implode_space (Try.serial_commas "and" (map quote named_methods)) ^
"..."
|> writeln
else
();
- (case get_results apply_methods of
+ (case get_results maybe_apply_methods of
[] => (if mode = Normal then writeln "No proof found" else (); ((false, (noneN, [])), []))
| results as {name, command, ...} :: _ =>
let