# HG changeset patch # User wenzelm # Date 1741027938 -3600 # Node ID cbe937aa5e90c85dc9e0bff20eee647b5dcb7d28 # Parent e4e35ffe1ccd2808c3c03d1c05edee5c6b2cfe7b# Parent dd28f282ddc294cb59b7855f75f6ae7f192f68d6 merged, resolving conflicts in src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML due to clones bb2ea9e80c33 + 62c039ce397c; diff -r e4e35ffe1ccd -r cbe937aa5e90 CONTRIBUTORS --- 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 ----------------------------- diff -r e4e35ffe1ccd -r cbe937aa5e90 NEWS --- 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) -------------------------------- diff -r e4e35ffe1ccd -r cbe937aa5e90 src/Doc/Sledgehammer/document/root.tex --- 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} diff -r e4e35ffe1ccd -r cbe937aa5e90 src/HOL/Fun.thy --- 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 @@ "(\x. x - a) ` (s \ t) = ((\x. x - a) ` s) \ ((\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 \ (+) a ` (- t) \ b \ - (+) 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 \ 'b::semilattice_sup" by (auto simp add: mono_def intro: Lattices.sup_least) +lemma monotone_on_sup_fun: + fixes f g :: "_ \ _:: semilattice_sup" + shows "monotone_on A P (\) f \ monotone_on A P (\) g \ monotone_on A P (\) (f \ g)" + by (auto intro: monotone_onI sup_mono dest: monotone_onD simp: sup_fun_def) + +lemma monotone_on_inf_fun: + fixes f g :: "_ \ _:: semilattice_inf" + shows "monotone_on A P (\) f \ monotone_on A P (\) g \ monotone_on A P (\) (f \ g)" + by (auto intro: monotone_onI inf_mono dest: monotone_onD simp: inf_fun_def) + +lemma antimonotone_on_sup_fun: + fixes f g :: "_ \ _:: semilattice_sup" + shows "monotone_on A P (\) f \ monotone_on A P (\) g \ monotone_on A P (\) (f \ g)" + by (auto intro: monotone_onI sup_mono dest: monotone_onD simp: sup_fun_def) + +lemma antimonotone_on_inf_fun: + fixes f g :: "_ \ _:: semilattice_inf" + shows "monotone_on A P (\) f \ monotone_on A P (\) g \ monotone_on A P (\) (f \ g)" + by (auto intro: monotone_onI inf_mono dest: monotone_onD simp: inf_fun_def) + lemma (in linorder) min_of_mono: "mono f \ min (f m) (f n) = f (min m n)" by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym) diff -r e4e35ffe1ccd -r cbe937aa5e90 src/HOL/Library/Sublist.thy --- 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 \Basic properties of prefixes\ -(* 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] \ 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 \ prefix xs ys)" @@ -109,23 +107,26 @@ theorem prefix_append: "prefix xs (ys @ zs) = (prefix xs ys \ (\us. xs = ys @ us \ 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 \ length xs < length ys \ prefix (xs @ [ys ! length xs]) ys" - proof (unfold prefix_def) - assume a1: "\zs. ys = xs @ zs" - then obtain sk :: "'a list" where sk: "ys = xs @ sk" by fastforce - assume a2: "length xs < length ys" - have f1: "\v. ([]::'a list) @ v = v" using append_Nil2 by simp - have "[] \ sk" using a1 a2 sk less_not_refl by force - hence "\v. xs @ hd sk # v = ys" using sk by (metis hd_Cons_tl) - thus "\zs. ys = (xs @ [ys ! length xs]) @ zs" using f1 by fastforce - qed +proof (unfold prefix_def) + assume a1: "\zs. ys = xs @ zs" + then obtain sk :: "'a list" where sk: "ys = xs @ sk" by fastforce + assume a2: "length xs < length ys" + have f1: "\v. ([]::'a list) @ v = v" using append_Nil2 by simp + have "[] \ sk" using a1 a2 sk less_not_refl by force + hence "\v. xs @ hd sk # v = ys" using sk by (metis hd_Cons_tl) + thus "\zs. ys = (xs @ [ys ! length xs]) @ zs" using f1 by fastforce +qed theorem prefix_length_le: "prefix xs ys \ length xs \ 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 \ prefix (map f xs) (map f ys)" -by (auto simp: prefix_def) + by (auto simp: prefix_def) lemma filter_mono_prefix: "prefix xs ys \ prefix (filter P xs) (filter P ys)" -by (auto simp: prefix_def) + by (auto simp: prefix_def) lemma sorted_antimono_prefix: "prefix xs ys \ sorted ys \ sorted xs" -by (metis sorted_append prefix_def) + by (metis sorted_append prefix_def) lemma prefix_length_less: "strict_prefix xs ys \ length xs < length ys" by (auto simp: strict_prefix_def prefix_def) @@ -281,8 +282,8 @@ subsection \Prefixes\ 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 \ set (prefixes ys) \ prefix xs ys" proof (induct xs arbitrary: ys) @@ -400,44 +401,43 @@ lemma Longest_common_prefix_unique: \\! ps. (\xs \ L. prefix ps xs) \ (\qs. (\xs \ L. prefix qs xs) \ length qs \ length ps)\ if \L \ {}\ - 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: - "\ L \ {}; \xs \ L. prefix ps xs; + "\ L \ {}; \xs \ L. prefix ps xs; \qs. (\xs \ L. prefix qs xs) \ size qs \ size ps \ \ 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 \ L \ 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 \ {} \ \xs\L. prefix ps xs \ length ps \ 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 \ {} \ \xs\L. prefix ps xs \ 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: "[] \ L \ 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 \ {} \ - 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 \ {}" + shows "Longest_common_prefix ((#) x ` L) = x # Longest_common_prefix L" +proof (intro Longest_common_prefix_eq strip) + show "\qs. \xs\(#) x ` L. prefix qs xs \ + length qs \ 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 \ {}" "[] \ L" "\xs\L. hd xs = x" shows "Longest_common_prefix L = x # Longest_common_prefix {ys. x#ys \ L}" @@ -450,26 +450,26 @@ lemma Longest_common_prefix_eq_Nil: "\x#ys \ L; y#zs \ L; x \ y \ \ 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 \ 'a list \ '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: "\ prefix ps xs; prefix ps ys \ \ 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 \Parallel lists\ @@ -506,10 +506,7 @@ qed lemma parallel_append: "a \ b \ a @ c \ 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 \ ys \ x = xs @ xs' \ y = ys @ ys' \ x \ 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 \ (\ys'. prefix ys' ys \ suffix xs ys')" -proof safe - assume "sublist xs ys" - then obtain ps ss where "ys = ps @ xs @ ss" by (auto simp: sublist_def) - thus "\ys'. prefix ys' ys \ 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 \ (\ys'. suffix ys' ys \ prefix xs ys')" -proof safe - assume "sublist xs ys" - then obtain ps ss where "ys = ps @ xs @ ss" by (auto simp: sublist_def) - thus "\ys'. suffix ys' ys \ 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) \ prefix xs (y # ys) \ 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 = (\uu uua uuaa. rec_list (\P xs. List.null xs) (\y ys ysa P xs. case xs of [] \ True - | x # xs \ if P x y then ysa P xs else ysa P (x # xs)) uuaa uu uua)" + "list_emb = (\uu l' l. rec_list (\P xs. List.null xs) (\y ys ysa P xs. case xs of [] \ True + | x # xs \ 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 diff -r e4e35ffe1ccd -r cbe937aa5e90 src/HOL/Set_Interval.thy --- 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 \ b = c" by auto qed simp +text \Quantifiers\ + +lemma ex_interval_simps: + "(\x \ {.. (\xx \ {..u}. P x) \ (\x\u. P x)" + "(\x \ {l<..}. P x) \ (\x>l. P x)" + "(\x \ {l..}. P x) \ (\x\l. P x)" + "(\x \ {l<.. (\x. l x P x)" + "(\x \ {l.. (\x. l\x \ x P x)" + "(\x \ {l<..u}. P x) \ (\x. l x\u \ P x)" + "(\x \ {l..u}. P x) \ (\x. l\x \ x\u \ P x)" + by auto + +lemma all_interval_simps: + "(\x \ {.. (\xx \ {..u}. P x) \ (\x\u. P x)" + "(\x \ {l<..}. P x) \ (\x>l. P x)" + "(\x \ {l..}. P x) \ (\x\l. P x)" + "(\x \ {l<.. (\x. l x P x)" + "(\x \ {l.. (\x. l\x \ x P x)" + "(\x \ {l<..u}. P x) \ (\x. l x\u \ P x)" + "(\x \ {l..u}. P x) \ (\x. l\x \ x\u \ P x)" + by auto + text \The following results generalise their namesakes in @{theory HOL.Nat} to intervals\ lemma lift_Suc_mono_le_ivl: diff -r e4e35ffe1ccd -r cbe937aa5e90 src/HOL/Sledgehammer.thy --- 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 \Tools/Sledgehammer/sledgehammer_prover.ML\ ML_file \Tools/Sledgehammer/sledgehammer_prover_atp.ML\ ML_file \Tools/Sledgehammer/sledgehammer_prover_smt.ML\ +ML_file \Tools/Sledgehammer/sledgehammer_prover_tactic.ML\ ML_file \Tools/Sledgehammer/sledgehammer_prover_minimize.ML\ ML_file \Tools/Sledgehammer/sledgehammer_mepo.ML\ ML_file \Tools/Sledgehammer/sledgehammer_mash.ML\ diff -r e4e35ffe1ccd -r cbe937aa5e90 src/HOL/TPTP/atp_problem_import.ML --- 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 diff -r e4e35ffe1ccd -r cbe937aa5e90 src/HOL/Tools/SMT/smt_systems.ML --- 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 } diff -r e4e35ffe1ccd -r cbe937aa5e90 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- 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) = diff -r e4e35ffe1ccd -r cbe937aa5e90 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML diff -r e4e35ffe1ccd -r cbe937aa5e90 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- 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 = \ \see also \<^system_option>\sledgehammer_provers\\ - 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 = diff -r e4e35ffe1ccd -r cbe937aa5e90 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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" ^ diff -r e4e35ffe1ccd -r cbe937aa5e90 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- 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 diff -r e4e35ffe1ccd -r cbe937aa5e90 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML --- 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 diff -r e4e35ffe1ccd -r cbe937aa5e90 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- 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 diff -r e4e35ffe1ccd -r cbe937aa5e90 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- 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) diff -r e4e35ffe1ccd -r cbe937aa5e90 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- 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>\sledgehammer_smt_builtins\ (K true) val smt_triggers = Attrib.setup_config_bool \<^binding>\sledgehammer_smt_triggers\ (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. *) diff -r e4e35ffe1ccd -r cbe937aa5e90 src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML --- /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; diff -r e4e35ffe1ccd -r cbe937aa5e90 src/HOL/Tools/try0.ML --- 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