merged

--- a/CONTRIBUTORS	Thu Mar 13 11:19:27 2025 +0100
+++ b/CONTRIBUTORS	Thu Mar 13 15:49:15 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	Thu Mar 13 11:19:27 2025 +0100
+++ b/NEWS	Thu Mar 13 15:49:15 2025 +0100
@@ -4,6 +4,57 @@
 (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
+
+* Theory "HOL.Relations":
+  - Changed definition of predicate refl_on to not constrain the domain and
+    range of the relation. To get the old semantics, explicitely use the
+    formula "r ⊂ A × A ∧ refl_on A r". INCOMPATIBILITY.
+
+* Theory "HOL.Wellfounded":
+  - Added lemmas.
+      bex_rtrancl_min_element_if_wf_on
+      bex_rtrancl_min_element_if_wfp_on
+      wf_on_lex_prod[intro]
+      wfp_on_iff_wfp
+
+* Theory "HOL.Order_Relation":
+  - Added lemmas.
+      antisym_relation_of[simp]
+      asym_relation_of[simp]
+      irrefl_relation_ofD
+      refl_relation_ofD
+      sym_relation_of[simp]
+      total_relation_ofD
+      trans_relation_of[simp]
+
+* Theory "HOL.Equiv_Relation":
+  - Strengthened lemmas. Minor INCOMPATIBILITY.
+      sym_trans_comp_subset
+  - Added lemmas.
+      quotient_disj_strong
+
+* Theory "HOL-Library.Multiset":
+  - Renamed lemmas. Minor INCOMPATIBILITY.
+      filter_image_mset ~> filter_mset_image_mset
+  - Removed lemmas.
+      size_multiset_sum_mset[simp]
+  - Added lemmas.
+      filter_mset_eq_mempty_iff[simp]
+      filter_mset_mono_strong
+      filter_mset_sum_list
+      set_mset_sum_list[simp]
+      size_mset_sum_mset_conv[simp]
+
+
 New in Isabelle2025 (March 2025)
 --------------------------------
 

--- a/src/Doc/Sledgehammer/document/root.tex	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Thu Mar 13 15:49:15 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/Algebra/Coset.thy	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Algebra/Coset.thy	Thu Mar 13 15:49:15 2025 +0100
@@ -673,7 +673,7 @@
   interpret group G by fact
   show ?thesis
   proof (intro equivI)
-    have "rcong H \<subseteq> carrier G \<times> carrier G"
+    show "rcong H \<subseteq> carrier G \<times> carrier G"
       by (auto simp add: r_congruent_def)
     thus "refl_on (carrier G) (rcong H)"
       by (auto simp add: r_congruent_def refl_on_def)

--- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Thu Mar 13 15:49:15 2025 +0100
@@ -1104,7 +1104,16 @@
 
 lemma natLeq_Preorder: "Preorder natLeq"
   unfolding preorder_on_def
-  by (auto simp add: natLeq_Refl natLeq_trans)
+proof (intro conjI)
+  show "natLeq \<subseteq> Field natLeq \<times> Field natLeq"
+    unfolding natLeq_def Field_def by blast
+next
+  show "Refl natLeq"
+    using natLeq_Refl .
+next
+  show "trans natLeq"
+    using natLeq_trans .
+qed
 
 lemma natLeq_antisym: "antisym natLeq"
   unfolding antisym_def natLeq_def by auto

--- a/src/HOL/BNF_Wellorder_Constructions.thy	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/BNF_Wellorder_Constructions.thy	Thu Mar 13 15:49:15 2025 +0100
@@ -56,8 +56,24 @@
   unfolding trans_def Field_def by blast
 
 lemma Preorder_Restr:
-  "Preorder r \<Longrightarrow> Preorder(Restr r A)"
-  unfolding preorder_on_def by (simp add: Refl_Restr trans_Restr)
+  assumes "Preorder r"
+  shows "Preorder(Restr r A)"
+  unfolding preorder_on_def
+proof (intro conjI)
+  have "r \<subseteq> Field r \<times> Field r" and "Refl r" and "trans r"
+    using \<open>Preorder r\<close>
+    by (simp_all only: preorder_on_def)
+
+  show "Restr r A \<subseteq> Field (Restr r A) \<times> Field (Restr r A)"
+    using \<open>r \<subseteq> Field r \<times> Field r\<close>
+    by (auto simp add: Field_def)
+
+  show "Refl (Restr r A)"
+    using Refl_Restr[OF \<open>Refl r\<close>] .
+
+  show "trans (Restr r A)"
+    using trans_Restr[OF \<open>trans r\<close>] .
+qed
 
 lemma Partial_order_Restr:
   "Partial_order r \<Longrightarrow> Partial_order(Restr r A)"
@@ -867,6 +883,18 @@
   "inj_on f (Field r) \<Longrightarrow> (dir_image r f) - Id = dir_image (r - Id) f"
   unfolding inj_on_def Field_def dir_image_def by auto
 
+lemma dir_image_subset:
+  assumes "r \<subseteq> A \<times> B"
+  shows "dir_image r f \<subseteq> f ` A \<times> f ` B"
+proof (rule subsetI)
+  fix x
+  assume "x \<in> dir_image r f"
+  then obtain a b where "x = (f a, f b)" and "(a, b) \<in> r"
+    unfolding dir_image_def by blast
+  thus "x \<in> f ` A \<times> f ` B"
+    using \<open>r \<subseteq> A \<times> B\<close> by auto
+qed
+
 lemma Refl_dir_image:
   assumes "Refl r"
   shows "Refl(dir_image r f)"
@@ -903,8 +931,23 @@
 qed
 
 lemma Preorder_dir_image:
-  "\<lbrakk>Preorder r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> Preorder (dir_image r f)"
-  by (simp add: preorder_on_def Refl_dir_image trans_dir_image)
+  assumes "Preorder r" and inj: "inj_on f (Field r)"
+  shows "Preorder (dir_image r f)"
+  unfolding preorder_on_def
+proof (intro conjI)
+  have "r \<subseteq> Field r \<times> Field r" and "Refl r" and "trans r"
+    using \<open>Preorder r\<close> by (simp_all only: preorder_on_def)
+
+  show "dir_image r f \<subseteq> Field (dir_image r f) \<times> Field (dir_image r f)"
+    using dir_image_subset[OF \<open>r \<subseteq> Field r \<times> Field r\<close>]
+    unfolding dir_image_Field .
+
+  show "Refl (dir_image r f)"
+    using Refl_dir_image[OF \<open>Refl r\<close>] .
+
+  show "trans (dir_image r f)"
+    using trans_dir_image[OF \<open>trans r\<close> inj] .
+qed
 
 lemma antisym_dir_image:
   assumes AN: "antisym r" and INJ: "inj_on f (Field r)"
@@ -1060,6 +1103,13 @@
   qed
 qed
 
+lemma bsqr_subset:
+  assumes "r \<subseteq> Field r \<times> Field r"
+  shows "bsqr r \<subseteq> Field (bsqr r) \<times> Field (bsqr r)"
+  using \<open>r \<subseteq> Field r \<times> Field r\<close>
+  unfolding Field_bsqr
+  by (auto simp add: bsqr_def)
+
 lemma bsqr_Refl: "Refl(bsqr r)"
   by(unfold refl_on_def Field_bsqr, auto simp add: bsqr_def)
 
@@ -1302,8 +1352,16 @@
 lemma bsqr_Linear_order:
   assumes "Well_order r"
   shows "Linear_order(bsqr r)"
-  unfolding order_on_defs
-  using assms bsqr_Refl bsqr_Trans bsqr_antisym bsqr_Total by blast
+proof -
+  have "r \<subseteq> Field r \<times> Field r"
+    using \<open>Well_order r\<close>
+    by (simp only: order_on_defs)
+
+  thus ?thesis
+    unfolding order_on_defs
+    using assms bsqr_Refl bsqr_Trans bsqr_antisym bsqr_Total bsqr_subset[OF \<open>r \<subseteq> Field r \<times> Field r\<close>]
+    by auto
+qed
 
 lemma bsqr_Well_order:
   assumes "Well_order r"

--- a/src/HOL/BNF_Wellorder_Embedding.thy	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/BNF_Wellorder_Embedding.thy	Thu Mar 13 15:49:15 2025 +0100
@@ -223,7 +223,7 @@
     unfolding Field_def by auto
   {assume "(a,b) \<in> r"
     hence "a \<in> under r b \<and> b \<in> under r b"
-      using Refl by(auto simp add: under_def refl_on_def)
+      using Refl by (auto simp add: under_def refl_on_def Field_def)
     hence "a = b"
       using EMB 1 ***
       by (auto simp add: embed_def bij_betw_def inj_on_def)
@@ -231,7 +231,7 @@
   moreover
   {assume "(b,a) \<in> r"
     hence "a \<in> under r a \<and> b \<in> under r a"
-      using Refl by(auto simp add: under_def refl_on_def)
+      using Refl by (auto simp add: under_def refl_on_def Field_def)
     hence "a = b"
       using EMB 1 ***
       by (auto simp add: embed_def bij_betw_def inj_on_def)

--- a/src/HOL/Cardinals/Order_Union.thy	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Cardinals/Order_Union.thy	Thu Mar 13 15:49:15 2025 +0100
@@ -89,7 +89,7 @@
 
 lemma Osum_Preorder:
   "\<lbrakk>Field r Int Field r' = {}; Preorder r; Preorder r'\<rbrakk> \<Longrightarrow> Preorder (r Osum r')"
-  unfolding preorder_on_def using Osum_Refl Osum_trans by blast
+  unfolding preorder_on_def using Osum_Refl Osum_trans Restr_Field by blast
 
 lemma Osum_antisym:
   assumes FLD: "Field r Int Field r' = {}" and

--- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Thu Mar 13 15:49:15 2025 +0100
@@ -52,7 +52,9 @@
 qed
 
 lemma osum_Preorder: "\<lbrakk>Preorder r; Preorder r'\<rbrakk> \<Longrightarrow> Preorder (r +o r')"
-  unfolding preorder_on_def using osum_Refl osum_trans by blast
+  unfolding preorder_on_def using osum_Refl osum_trans
+  by (metis inf.cobounded2[of "r +o r'" "Field (r +o r') \<times> Field (r +o r')"]
+      Restr_Field[of "r +o r'"])
 
 lemma osum_antisym: "\<lbrakk>antisym r; antisym r'\<rbrakk> \<Longrightarrow> antisym (r +o r')"
   unfolding antisym_def osum_def by auto
@@ -178,7 +180,9 @@
   using assms by (clarsimp simp: trans_def antisym_def oprod_def) (metis FieldI1 FieldI2)
 
 lemma oprod_Preorder: "\<lbrakk>Preorder r; Preorder r'; antisym r; antisym r'\<rbrakk> \<Longrightarrow> Preorder (r *o r')"
-  unfolding preorder_on_def using oprod_Refl oprod_trans by blast
+  unfolding preorder_on_def using oprod_Refl oprod_trans
+  by (metis Restr_Field[of "r *o r'"]
+      inf.cobounded2[of "r *o r'" "Field (r *o r') \<times> Field (r *o r')"])
 
 lemma oprod_antisym: "\<lbrakk>antisym r; antisym r'\<rbrakk> \<Longrightarrow> antisym (r *o r')"
   unfolding antisym_def oprod_def by auto
@@ -588,7 +592,7 @@
 qed
 
 lemma oexp_Preorder: "Preorder oexp"
-  unfolding preorder_on_def using oexp_Refl oexp_trans by blast
+  unfolding preorder_on_def using oexp_Refl oexp_trans Restr_Field[of oexp] by blast
 
 lemma oexp_antisym: "antisym oexp"
 proof (unfold antisym_def, safe, rule ccontr)

--- a/src/HOL/Cardinals/Wellorder_Constructions.thy	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Cardinals/Wellorder_Constructions.thy	Thu Mar 13 15:49:15 2025 +0100
@@ -96,7 +96,8 @@
 lemma ofilter_ordLeq:
   assumes "Well_order r" and "ofilter r A"
   shows "Restr r A \<le>o r"
-by (metis assms inf.orderE ofilter_embed ofilter_subset_ordLeq refl_on_def wo_rel.Field_ofilter wo_rel.REFL wo_rel.intro)
+  by (metis Well_order_Restr[of r A] assms ofilter_embed[of r A] ordLess_iff[of r "Restr r A"]
+      ordLess_or_ordLeq[of r "Restr r A"])
 
 corollary under_Restr_ordLeq:
   "Well_order r \<Longrightarrow> Restr r (under r a) \<le>o r"
@@ -334,7 +335,7 @@
   have bb: "b \<in> Field r" using bA unfolding underS_def Field_def by auto
   assume "\<forall>a\<in>A.  b \<notin> underS a"
   hence 0: "\<forall>a \<in> A. (a,b) \<in> r" using A bA unfolding underS_def
-    by simp (metis REFL in_mono max2_def max2_greater refl_on_domain)
+    using bb in_notinI[of b] by blast
   have "(supr A, b) \<in> r"
     by (simp add: "0" A bb supr_least)
   thus False
@@ -605,7 +606,7 @@
   assumes isLimOrd and "i \<in> Field r"
   shows "succ i \<in> Field r"
   using assms unfolding isLimOrd_def isSuccOrd_def
-  by (metis REFL in_notinI refl_on_domain succ_smallest)
+  using FieldI1[of "succ i" _ r] in_notinI[of i] succ_smallest[of i] by blast
 
 lemma isLimOrd_aboveS:
   assumes l: isLimOrd and i: "i \<in> Field r"

--- a/src/HOL/Cardinals/Wellorder_Extension.thy	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Cardinals/Wellorder_Extension.thy	Thu Mar 13 15:49:15 2025 +0100
@@ -87,7 +87,9 @@
       "\<And>r. r \<in> R \<Longrightarrow> downset_on (Field r) p" and
       "\<And>r. r \<in> R \<Longrightarrow> extension_on (Field r) r p"
       using Chains_wo [OF \<open>R \<in> Chains I\<close>] by (simp_all add: order_on_defs)
-    have "Refl (\<Union>R)" using \<open>\<forall>r\<in>R. Refl r\<close>  unfolding refl_on_def by fastforce
+    have "(\<Union>R) \<subseteq> Field (\<Union>R) \<times> Field (\<Union>R)"
+      using Restr_Field by blast
+    moreover have "Refl (\<Union>R)" using \<open>\<forall>r\<in>R. Refl r\<close>  unfolding refl_on_def by fastforce
     moreover have "trans (\<Union>R)"
       by (rule chain_subset_trans_Union [OF subch \<open>\<forall>r\<in>R. trans r\<close>])
     moreover have "antisym (\<Union>R)"
@@ -130,10 +132,13 @@
     let ?s = "{(y, x) | y. y \<in> Field m}"
     let ?m = "insert (x, x) m \<union> ?s"
     have Fm: "Field ?m = insert x (Field m)" by (auto simp: Field_def)
-    have "Refl m" and "trans m" and "antisym m" and "Total m" and "wf (m - Id)"
+    have "Refl m" and "trans m" and "antisym m" and "Total m" and "wf (m - Id)" and
+      "m \<subseteq> Field m \<times> Field m"
       using \<open>Well_order m\<close> by (simp_all add: order_on_defs)
     txt \<open>We show that the extension is a wellorder.\<close>
-    have "Refl ?m" using \<open>Refl m\<close> Fm by (auto simp: refl_on_def)
+    have "?m \<subseteq> Field ?m \<times> Field ?m"
+      using \<open>m \<subseteq> Field m \<times> Field m\<close> by auto
+    moreover have "Refl ?m" using \<open>Refl m\<close> Fm by (auto simp: refl_on_def)
     moreover have "trans ?m" using \<open>trans m\<close> \<open>x \<notin> Field m\<close>
       unfolding trans_def Field_def Domain_unfold Domain_converse [symmetric] by blast
     moreover have "antisym ?m" using \<open>antisym m\<close> \<open>x \<notin> Field m\<close>
@@ -160,7 +165,7 @@
       \<open>downset_on (Field m) p\<close> and \<open>downset_on (Field ?m) p\<close> and
       \<open>extension_on (Field m) m p\<close> and \<open>extension_on (Field ?m) ?m p\<close> and
       \<open>Refl m\<close> and \<open>x \<notin> Field m\<close>
-      by (auto simp: I_def init_seg_of_def refl_on_def)
+      by (auto simp: I_def init_seg_of_def refl_on_def dest: well_order_on_domain)
     ultimately
     \<comment> \<open>This contradicts maximality of m:\<close>
     show False using max and \<open>x \<notin> Field m\<close> unfolding Field_def by blast
@@ -199,7 +204,8 @@
   from \<open>p \<subseteq> r\<close> have "p \<subseteq> ?r" using \<open>Field p \<subseteq> A\<close> by (auto simp: Field_def)
   have "Refl r" "trans r" "antisym r" "Total r" "wf (r - Id)"
     using \<open>Well_order r\<close> by (simp_all add: order_on_defs)
-  have "refl_on A ?r" using \<open>Refl r\<close> by (auto simp: refl_on_def univ)
+  have "?r \<subseteq> A \<times> A" by blast
+  moreover have "refl_on A ?r" using \<open>Refl r\<close> by (auto simp: refl_on_def univ)
   moreover have "trans ?r" using \<open>trans r\<close>
     unfolding trans_def by blast
   moreover have "antisym ?r" using \<open>antisym r\<close>

--- a/src/HOL/Cardinals/Wellorder_Relation.thy	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Cardinals/Wellorder_Relation.thy	Thu Mar 13 15:49:15 2025 +0100
@@ -218,7 +218,7 @@
 next
   fix b assume "(suc B, b) \<in> r"
   thus "b \<in> Field r"
-    using REFL refl_on_def[of _ r] by auto
+    by (simp add: FieldI2)
 next
   fix a b
   assume 1: "(suc B, b) \<in> r" and 2: "a \<in> B"

--- a/src/HOL/Equiv_Relations.thy	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Equiv_Relations.thy	Thu Mar 13 15:49:15 2025 +0100
@@ -11,14 +11,14 @@
 subsection \<open>Equivalence relations -- set version\<close>
 
 definition equiv :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool"
-  where "equiv A r \<longleftrightarrow> refl_on A r \<and> sym r \<and> trans r"
+  where "equiv A r \<longleftrightarrow> r \<subseteq> A \<times> A \<and> refl_on A r \<and> sym r \<and> trans r"
 
-lemma equivI: "refl_on A r \<Longrightarrow> sym r \<Longrightarrow> trans r \<Longrightarrow> equiv A r"
+lemma equivI: "r \<subseteq> A \<times> A \<Longrightarrow> refl_on A r \<Longrightarrow> sym r \<Longrightarrow> trans r \<Longrightarrow> equiv A r"
   by (simp add: equiv_def)
 
 lemma equivE:
   assumes "equiv A r"
-  obtains "refl_on A r" and "sym r" and "trans r"
+  obtains "r \<subseteq> A \<times> A" and "refl_on A r" and "sym r" and "trans r"
   using assms by (simp add: equiv_def)
 
 text \<open>
@@ -27,27 +27,51 @@
   First half: \<open>equiv A r \<Longrightarrow> r\<inverse> O r = r\<close>.
 \<close>
 
-lemma sym_trans_comp_subset: "sym r \<Longrightarrow> trans r \<Longrightarrow> r\<inverse> O r \<subseteq> r"
-  unfolding trans_def sym_def converse_unfold by blast
+lemma sym_trans_comp_subset:
+  assumes "r \<subseteq> A \<times> A" and "sym_on A r" and "trans_on A r"
+  shows "r\<inverse> O r \<subseteq> r"
+proof (rule subsetI)
+  fix p
+  assume "p \<in> r\<inverse> O r"
+  then obtain x y z where "p = (x, z)" and "(y, x) \<in> r" and "(y, z) \<in> r"
+    by auto
+  hence "x \<in> A" and "y \<in> A" and "z \<in> A"
+    using \<open>r \<subseteq> A \<times> A\<close> by auto
+  have "(x, y) \<in> r"
+    using \<open>(y, x) \<in> r\<close> \<open>x \<in> A\<close> \<open>y \<in> A\<close> \<open>sym_on A r\<close> by (simp add: sym_on_def)
+  hence "(x, z) \<in> r"
+    using \<open>trans_on A r\<close>[THEN trans_onD, OF \<open>x \<in> A\<close> \<open>y \<in> A\<close> \<open>z \<in> A\<close>] \<open>(y, z) \<in> r\<close> by blast
+  thus "p \<in> r"
+    unfolding \<open>p = (x, z)\<close> .
+qed
 
-lemma refl_on_comp_subset: "refl_on A r \<Longrightarrow> r \<subseteq> r\<inverse> O r"
+lemma refl_on_comp_subset: "r \<subseteq> A \<times> A \<Longrightarrow> refl_on A r \<Longrightarrow> r \<subseteq> r\<inverse> O r"
   unfolding refl_on_def by blast
 
 lemma equiv_comp_eq: "equiv A r \<Longrightarrow> r\<inverse> O r = r"
-  unfolding equiv_def
-  by (iprover intro: sym_trans_comp_subset refl_on_comp_subset equalityI)
+proof (rule subset_antisym)
+  show "equiv A r \<Longrightarrow> r\<inverse> O r \<subseteq> r"
+    by (rule sym_trans_comp_subset[of r A]) (auto elim: equivE intro: sym_on_subset trans_on_subset)
+next
+  show "equiv A r \<Longrightarrow> r \<subseteq> r\<inverse> O r"
+    by (rule refl_on_comp_subset[of r A]) (auto elim: equivE)
+qed
 
 text \<open>Second half.\<close>
 
 lemma comp_equivI:
   assumes "r\<inverse> O r = r" "Domain r = A"
   shows "equiv A r"
-proof -
+proof (rule equivI)
+  show "r \<subseteq> A \<times> A"
+    using assms by auto
+
   have *: "\<And>x y. (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r"
     using assms by blast
-  show ?thesis
-    unfolding equiv_def refl_on_def sym_def trans_def
-    using assms by (auto intro: *)
+
+  thus "refl_on A r" "sym r" "trans r"
+    unfolding refl_on_def sym_def trans_def
+    using assms by auto
 qed
 
 
@@ -57,8 +81,19 @@
   \<comment> \<open>lemma for the next result\<close>
   unfolding equiv_def trans_def sym_def by blast
 
-theorem equiv_class_eq: "equiv A r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> r``{a} = r``{b}"
-  by (intro equalityI equiv_class_subset; force simp add: equiv_def sym_def)
+theorem equiv_class_eq:
+  assumes "equiv A r" and "(a, b) \<in> r"
+  shows "r``{a} = r``{b}"
+proof (intro subset_antisym equiv_class_subset[OF \<open>equiv A r\<close>])
+  show "(a, b) \<in> r"
+    using \<open>(a, b) \<in> r\<close> .
+next
+  have "sym r"
+    using \<open>equiv A r\<close> by (auto elim: equivE)
+  thus "(b, a) \<in> r"
+    using \<open>(a, b) \<in> r\<close>
+    by (auto dest: symD)
+qed
 
 lemma equiv_class_self: "equiv A r \<Longrightarrow> a \<in> A \<Longrightarrow> a \<in> r``{a}"
   unfolding equiv_def refl_on_def by blast
@@ -100,8 +135,30 @@
 lemma Union_quotient: "equiv A r \<Longrightarrow> \<Union>(A//r) = A"
   unfolding equiv_def refl_on_def quotient_def by blast
 
+lemma quotient_disj_strong:
+  assumes "r \<subseteq> A \<times> A" and "sym_on A r" and "trans_on A r" and "X \<in> A//r" and "Y \<in> A//r"
+  shows "X = Y \<or> X \<inter> Y = {}"
+proof -
+  obtain x where "x \<in> A" and "X = {x'. (x, x') \<in> r}"
+    using \<open>X \<in> A//r\<close> unfolding quotient_def UN_iff by blast
+
+  moreover obtain y where "y \<in> A" and "Y = {y'. (y, y') \<in> r}"
+    using \<open>Y \<in> A//r\<close> unfolding quotient_def UN_iff by blast
+
+  have f8: "\<forall>a aa. (aa, a) \<in> r \<or> (a, aa) \<notin> r"
+    using \<open>r \<subseteq> A \<times> A\<close>[unfolded subset_eq] \<open>sym_on A r\<close>[THEN sym_onD] by blast
+  have f9: "\<forall>a aa ab. (aa, ab) \<in> r \<or> (aa, a) \<notin> r \<or> (a, ab) \<notin> r"
+    using \<open>r \<subseteq> A \<times> A\<close>[unfolded subset_eq] \<open>trans_on A r\<close>[THEN trans_onD] by blast
+  then have "\<forall>a aa. aa \<in> Y \<or> (y, a) \<notin> r \<or> (a, aa) \<notin> r"
+    using \<open>Y = {y'. (y, y') \<in> r}\<close> by simp
+  then show ?thesis
+    using f9 f8 \<open>X = {x'. (x, x') \<in> r}\<close> \<open>Y = {y'. (y, y') \<in> r}\<close>
+      Collect_cong disjoint_iff_not_equal mem_Collect_eq by blast
+qed
+
 lemma quotient_disj: "equiv A r \<Longrightarrow> X \<in> A//r \<Longrightarrow> Y \<in> A//r \<Longrightarrow> X = Y \<or> X \<inter> Y = {}"
-  unfolding quotient_def equiv_def trans_def sym_def by blast
+  by (rule quotient_disj_strong[of r A X Y])
+    (auto elim: equivE intro: sym_on_subset trans_on_subset)
 
 lemma quotient_eqI:
   assumes "equiv A r" "X \<in> A//r" "Y \<in> A//r" and xy: "x \<in> X" "y \<in> Y" "(x, y) \<in> r"
@@ -109,8 +166,11 @@
 proof -
   obtain a b where "a \<in> A" and a: "X = r `` {a}" and "b \<in> A" and b: "Y = r `` {b}"
     using assms by (auto elim!: quotientE)
-  then have "(a,b) \<in> r"
-      using xy \<open>equiv A r\<close> unfolding equiv_def sym_def trans_def by blast
+  moreover have "sym r" and "trans r"
+    using \<open>equiv A r\<close>
+    by (auto elim: equivE)
+  ultimately have "(a,b) \<in> r"
+      using xy unfolding sym_def trans_def by blast
   then show ?thesis
     unfolding a b by (rule equiv_class_eq [OF \<open>equiv A r\<close>])
 qed

--- a/src/HOL/Fun.thy	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Fun.thy	Thu Mar 13 15:49:15 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/Induct/QuoDataType.thy	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Induct/QuoDataType.thy	Thu Mar 13 15:49:15 2025 +0100
@@ -50,6 +50,7 @@
 
 theorem equiv_msgrel: "equiv UNIV msgrel"
 proof (rule equivI)
+  show "msgrel \<subseteq> UNIV \<times> UNIV" by simp
   show "refl msgrel" by (simp add: refl_on_def msgrel_refl)
   show "sym msgrel" by (simp add: sym_def, blast intro: msgrel.SYM)
   show "trans msgrel" by (simp add: trans_def, blast intro: msgrel.TRANS)

--- a/src/HOL/Induct/QuoNestedDataType.thy	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Induct/QuoNestedDataType.thy	Thu Mar 13 15:49:15 2025 +0100
@@ -50,6 +50,7 @@
 
 theorem equiv_exprel: "equiv UNIV exprel"
 proof (rule equivI)
+  show "exprel \<subseteq> UNIV \<times> UNIV" by simp
   show "refl exprel" by (simp add: refl_on_def exprel_refl)
   show "sym exprel" by (simp add: sym_def, blast intro: exprel.SYM)
   show "trans exprel" by (simp add: trans_def, blast intro: exprel.TRANS)

--- a/src/HOL/Library/Disjoint_Sets.thy	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Library/Disjoint_Sets.thy	Thu Mar 13 15:49:15 2025 +0100
@@ -389,7 +389,7 @@
   assumes r: "equiv A r"
   shows "partition_on A (A // r)"
 proof (rule partition_onI)
-  from r have "refl_on A r"
+  from r have "r \<subseteq> A \<times> A" and "refl_on A r"
     by (auto elim: equivE)
   then show "\<Union>(A // r) = A" "{} \<notin> A // r"
     by (auto simp: refl_on_def quotient_def)
@@ -408,9 +408,10 @@
   have "A = \<Union>P"
     using P by (auto simp: partition_on_def)
 
-  have "{(x, y). \<exists>p \<in> P. x \<in> p \<and> y \<in> p} \<subseteq> A \<times> A"
+  show "{(x, y). \<exists>p \<in> P. x \<in> p \<and> y \<in> p} \<subseteq> A \<times> A"
     unfolding \<open>A = \<Union>P\<close> by blast
-  then show "refl_on A {(x, y). \<exists>p\<in>P. x \<in> p \<and> y \<in> p}"
+
+  show "refl_on A {(x, y). \<exists>p\<in>P. x \<in> p \<and> y \<in> p}"
     unfolding refl_on_def \<open>A = \<Union>P\<close> by auto
 next
   show "trans {(x, y). \<exists>p\<in>P. x \<in> p \<and> y \<in> p}"

--- a/src/HOL/Library/Multiset.thy	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Library/Multiset.thy	Thu Mar 13 15:49:15 2025 +0100
@@ -1299,10 +1299,16 @@
 lemma multiset_filter_subset[simp]: "filter_mset f M \<subseteq># M"
   by (simp add: mset_subset_eqI)
 
+lemma filter_mset_mono_strong:
+  assumes "A \<subseteq># B" "\<And>x. x \<in># A \<Longrightarrow> P x \<Longrightarrow> Q x"
+  shows   "filter_mset P A \<subseteq># filter_mset Q B"
+  by (rule mset_subset_eqI) (insert assms, auto simp: mset_subset_eq_count count_eq_zero_iff)
+
+(* TODO: rename to filter_mset_mono_strong *)
 lemma multiset_filter_mono:
   assumes "A \<subseteq># B"
   shows "filter_mset f A \<subseteq># filter_mset f B"
-  by (metis assms filter_sup_mset subset_mset.order_iff)
+  using filter_mset_mono_strong[OF \<open>A \<subseteq># B\<close>] .
 
 lemma filter_mset_eq_conv:
   "filter_mset P M = N \<longleftrightarrow> N \<subseteq># M \<and> (\<forall>b\<in>#N. P b) \<and> (\<forall>a\<in>#M - N. \<not> P a)" (is "?P \<longleftrightarrow> ?Q")
@@ -1331,6 +1337,9 @@
   qed
 qed
 
+lemma filter_mset_eq_mempty_iff[simp]: "filter_mset P A = {#} \<longleftrightarrow> (\<forall>x. x \<in># A \<longrightarrow> \<not> P x)"
+  by (auto simp: multiset_eq_iff count_eq_zero_iff)
+
 lemma filter_filter_mset: "filter_mset P (filter_mset Q M) = {#x \<in># M. Q x \<and> P x#}"
   by (auto simp: multiset_eq_iff)
 
@@ -1739,7 +1748,7 @@
      image_mset f (filter_mset P A) + image_mset g (filter_mset (\<lambda>x. \<not>P x) A)"
   by (induction A) auto
 
-lemma filter_image_mset:
+lemma filter_mset_image_mset:
   "filter_mset P (image_mset f A) = image_mset f (filter_mset (\<lambda>x. P (f x)) A)"
   by (induction A) auto
 
@@ -2817,6 +2826,12 @@
 lemma mset_concat: "mset (concat xss) = (\<Sum>xs\<leftarrow>xss. mset xs)"
   by (induction xss) auto
 
+lemma set_mset_sum_list [simp]: "set_mset (sum_list xs) = (\<Union>x\<in>set xs. set_mset x)"
+  by (induction xs) auto
+
+lemma filter_mset_sum_list: "filter_mset P (sum_list xs) = sum_list (map (filter_mset P) xs)"
+  by (induction xs) simp_all
+
 lemma sum_mset_singleton_mset [simp]: "(\<Sum>x\<in>#A. {#f x#}) = image_mset f A"
   by (induction A) auto
 
@@ -2829,9 +2844,32 @@
 lemma Union_image_single_mset[simp]: "\<Sum>\<^sub># (image_mset (\<lambda>x. {#x#}) m) = m"
   by(induction m) auto
 
-lemma size_multiset_sum_mset [simp]: "size (\<Sum>X\<in>#A. X :: 'a multiset) = (\<Sum>X\<in>#A. size X)"
+lemma size_mset_sum_mset_conv [simp]: "size (\<Sum>\<^sub># A :: 'a multiset) = (\<Sum>X\<in>#A. size X)"
   by (induction A) auto
 
+lemma sum_mset_image_mset_mono_strong:
+  assumes "A \<subseteq># B" and f_subeq_g: "\<And>x. x \<in># A \<Longrightarrow> f x \<subseteq># g x"
+  shows "(\<Sum>x\<in>#A. f x) \<subseteq># (\<Sum>x\<in>#B. g x)"
+proof -
+  define B' where
+    "B' = B - A"
+
+  have "B = A + B'"
+    using B'_def assms(1) by fastforce
+
+  have "\<Sum>\<^sub># (image_mset f A) \<subseteq># \<Sum>\<^sub># (image_mset g A)"
+    using f_subeq_g by (induction A) (auto intro!: subset_mset.add_mono)
+  also have "\<dots> \<subseteq># \<Sum>\<^sub># (image_mset g A) + \<Sum>\<^sub># (image_mset g B')"
+    by simp
+  also have "\<dots> = \<Sum>\<^sub># (image_mset g A + image_mset g B')"
+    by simp
+  also have "\<dots> = \<Sum>\<^sub># (image_mset g (A + B'))"
+    by simp
+  also have "\<dots> = \<Sum>\<^sub># (image_mset g B)"
+    unfolding \<open>B = A + B'\<close> ..
+  finally show ?thesis .
+qed
+
 context comm_monoid_mult
 begin
 

--- a/src/HOL/Library/Saturated.thy	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Library/Saturated.thy	Thu Mar 13 15:49:15 2025 +0100
@@ -129,7 +129,7 @@
     case True thus ?thesis by (simp add: sat_eq_iff)
   next
     case False thus ?thesis
-      by (simp add: sat_eq_iff nat_mult_min_left add_mult_distrib min_add_distrib_left min_add_distrib_right min.assoc min.absorb2)
+      by (simp add: sat_eq_iff nat_mult_min_left add_mult_distrib min_add_distrib_left min_add_distrib_right min.assoc)
   qed
 qed (simp_all add: sat_eq_iff mult.commute)
 
@@ -251,4 +251,48 @@
     by (auto simp: bot_sat_def)
 qed
 
+
+subsection \<open>Enumeration\<close>
+
+lemma inj_on_sat_of_nat:
+  shows "inj_on (of_nat :: nat \<Rightarrow> 'a::len sat) {0..<LENGTH('a)}"
+by (rule inj_onI) (simp add: sat_eq_iff)
+
+lemma UNIV_sat_eq_of_nat:
+  shows "(UNIV :: 'a::len sat set) = of_nat ` {0..LENGTH('a)}" (is "?lhs = ?rhs")
+proof -
+  have "x \<in> ?rhs" for x :: "'a sat"
+    by (simp add: image_eqI[where x="nat_of x"] sat_eq_iff)
+  then show ?thesis
+    by blast
+qed
+
+instantiation sat :: (len) enum
+begin
+
+definition enum_sat :: "'a sat list" where
+  "enum_sat = map of_nat [0..<Suc(LENGTH('a))]"
+
+definition enum_all_sat :: "('a sat \<Rightarrow> bool) \<Rightarrow> bool" where
+  "enum_all_sat = All"
+
+definition enum_ex_sat :: "('a sat \<Rightarrow> bool) \<Rightarrow> bool" where
+  "enum_ex_sat = Ex"
+
+instance
+proof intro_classes
+  show "UNIV = set (enum_class.enum :: 'a sat list)"
+    by (simp only: enum_sat_def UNIV_sat_eq_of_nat set_map flip: atLeastAtMost_upt)
+  show "distinct (enum_class.enum :: 'a sat list)"
+    by (clarsimp simp: enum_sat_def distinct_map inj_on_sat_of_nat sat_eq_iff)
+qed (simp_all add: enum_all_sat_def enum_ex_sat_def)
+
 end
+
+lemma enum_sat_code [code]:
+  fixes P :: "'a::len sat \<Rightarrow> bool"
+  shows "Enum.enum_all P \<longleftrightarrow> list_all P Enum.enum"
+    and "Enum.enum_ex P \<longleftrightarrow> list_ex P Enum.enum"
+by (simp_all add: enum_all_sat_def enum_ex_sat_def enum_UNIV list_all_iff list_ex_iff)
+
+end

--- a/src/HOL/Library/Sublist.thy	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Library/Sublist.thy	Thu Mar 13 15:49:15 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/List.thy	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/List.thy	Thu Mar 13 15:49:15 2025 +0100
@@ -2488,6 +2488,11 @@
   "(\<And>x. x \<in> set xs \<Longrightarrow> P(x)) \<Longrightarrow> dropWhile P (xs @ ys) = dropWhile P ys"
   by (induct xs) auto
 
+lemma dropWhile_id[simp]:
+    "(\<And>x. x \<in> set xs \<Longrightarrow> \<not> P x) \<Longrightarrow> dropWhile P xs = xs"
+using takeWhile_dropWhile_id[of P xs] takeWhile_eq_Nil_iff[of P xs]
+by fastforce
+
 lemma dropWhile_append3:
   "\<not> P y \<Longrightarrow>dropWhile P (xs @ y # ys) = dropWhile P xs @ y # ys"
   by (induct xs) auto
@@ -5644,14 +5649,20 @@
 
 lemma
   assumes "sorted_wrt f xs"
-  shows sorted_wrt_take: "sorted_wrt f (take n xs)"
-  and   sorted_wrt_drop: "sorted_wrt f (drop n xs)"
+  shows sorted_wrt_take[simp]: "sorted_wrt f (take n xs)"
+  and   sorted_wrt_drop[simp]: "sorted_wrt f (drop n xs)"
 proof -
   from assms have "sorted_wrt f (take n xs @ drop n xs)" by simp
   thus "sorted_wrt f (take n xs)" and "sorted_wrt f (drop n xs)"
     unfolding sorted_wrt_append by simp_all
 qed
 
+lemma sorted_wrt_dropWhile[simp]: "sorted_wrt R xs \<Longrightarrow> sorted_wrt R (dropWhile P xs)"
+by (auto dest: sorted_wrt_drop simp: dropWhile_eq_drop)
+
+lemma sorted_wrt_takeWhile[simp]: "sorted_wrt R xs \<Longrightarrow> sorted_wrt R (takeWhile P xs)"
+by (subst takeWhile_eq_take) (auto dest: sorted_wrt_take)
+
 lemma sorted_wrt_filter:
   "sorted_wrt f xs \<Longrightarrow> sorted_wrt f (filter P xs)"
 by (induction xs) auto
@@ -6500,6 +6511,10 @@
     by standard simp
 qed (simp_all add: sorted_list_of_set_def)
 
+lemma ex1_sorted_list_for_set_if_finite:
+  "finite X \<Longrightarrow> \<exists>!xs. sorted_wrt (<) xs \<and> set xs = X"
+  by (metis sorted_list_of_set.finite_set_strict_sorted strict_sorted_equal)
+
 text \<open>Alias theorems for backwards compatibility and ease of use.\<close>
 lemmas sorted_list_of_set = sorted_list_of_set.sorted_key_list_of_set and
        sorted_list_of_set_empty = sorted_list_of_set.sorted_key_list_of_set_empty and
@@ -7632,7 +7647,7 @@
 qed
 
 theorem equiv_listrel: "equiv A r \<Longrightarrow> equiv (lists A) (listrel r)"
-  by (simp add: equiv_def listrel_refl_on listrel_sym listrel_trans)
+  by (simp add: equiv_def listrel_subset listrel_refl_on listrel_sym listrel_trans)
 
 lemma listrel_rtrancl_refl[iff]: "(xs,xs) \<in> listrel(r\<^sup>*)"
   using listrel_refl_on[of UNIV, OF refl_rtrancl]

--- a/src/HOL/Metis_Examples/Tarski.thy	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Metis_Examples/Tarski.thy	Thu Mar 13 15:49:15 2025 +0100
@@ -60,8 +60,8 @@
   "Top po == greatest (\<lambda>x. True) po"
 
 definition PartialOrder :: "('a potype) set" where
-  "PartialOrder == {P. refl_on (pset P) (order P) & antisym (order P) &
-                       trans (order P)}"
+  "PartialOrder \<equiv> {P. order P \<subseteq> pset P \<times> pset P \<and>
+    refl_on (pset P) (order P) \<and> antisym (order P) \<and> trans (order P)}"
 
 definition CompleteLattice :: "('a potype) set" where
   "CompleteLattice == {cl. cl \<in> PartialOrder \<and>
@@ -155,19 +155,26 @@
 by (simp add: monotone_def)
 
 lemma (in PO) po_subset_po:
-     "S \<subseteq> A ==> (| pset = S, order = induced S r |) \<in> PartialOrder"
-apply (simp (no_asm) add: PartialOrder_def)
-apply auto
-\<comment> \<open>refl\<close>
-apply (simp add: refl_on_def induced_def)
-apply (blast intro: reflE)
-\<comment> \<open>antisym\<close>
-apply (simp add: antisym_def induced_def)
-apply (blast intro: antisymE)
-\<comment> \<open>trans\<close>
-apply (simp add: trans_def induced_def)
-apply (blast intro: transE)
-done
+  assumes "S \<subseteq> A"
+  shows "(| pset = S, order = induced S r |) \<in> PartialOrder"
+  unfolding PartialOrder_def mem_Collect_eq potype.simps
+proof (intro conjI)
+  show "induced S r \<subseteq> S \<times> S"
+    by (metis (no_types, lifting) case_prodD induced_def mem_Collect_eq
+        mem_Sigma_iff subrelI)
+
+  show "refl_on S (induced S r)"
+    using \<open>S \<subseteq> A\<close>
+    by (simp add: induced_def reflE refl_on_def subsetD)
+
+  show "antisym (induced S r)"
+    by (metis (lifting) BNF_Def.Collect_case_prodD PO_imp_sym antisym_subset induced_def
+        prod.collapse subsetI)
+
+  show "trans (induced S r)"
+    by (metis (no_types, lifting) case_prodD case_prodI induced_def local.transE mem_Collect_eq
+        trans_on_def)
+qed
 
 lemma (in PO) indE: "[| (x, y) \<in> induced S r; S \<subseteq> A |] ==> (x, y) \<in> r"
 by (simp add: add: induced_def)
@@ -196,7 +203,7 @@
 
 lemma (in PO) dualPO: "dual cl \<in> PartialOrder"
 apply (insert cl_po)
-apply (simp add: PartialOrder_def dual_def)
+  apply (simp add: PartialOrder_def dual_def converse_Times flip: converse_subset_swap)
 done
 
 lemma Rdual:
@@ -486,8 +493,9 @@
      "[|  H = {x. (x, f x) \<in> r & x \<in> A} |] ==> (f (lub H cl), lub H cl) \<in> r"
 apply (rule lub_upper, fast)
 apply (rule_tac t = "H" in ssubst, assumption)
-apply (rule CollectI)
-by (metis (lifting) CO_refl_on lubH_le_flubH monotone_def monotone_f refl_onD1 refl_onD2)
+  apply (rule CollectI)
+  by (metis (lifting) Pi_iff f_in_funcset lubH_le_flubH lub_in_lattice
+      mem_Collect_eq monotoneE monotone_f subsetI)
 
 declare CLF.f_in_funcset[rule del] funcset_mem[rule del]
         CL.lub_in_lattice[rule del] PO.monotoneE[rule del]
@@ -533,10 +541,12 @@
 lemma (in CLF) (*lubH_is_fixp:*)
      "H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A"
 apply (simp add: fix_def)
-apply (rule conjI)
-apply (metis CO_refl_on lubH_le_flubH refl_onD1)
-apply (metis antisymE flubH_le_lubH lubH_le_flubH)
-done
+  apply (rule conjI)
+  subgoal
+    by (metis (lifting) fix_def lubH_is_fixp mem_Collect_eq)
+  subgoal
+    by (metis antisymE flubH_le_lubH lubH_le_flubH)
+  done
 
 lemma (in CLF) fix_in_H:
      "[| H = {x. (x, f x) \<in> r & x \<in> A};  x \<in> P |] ==> x \<in> H"
@@ -618,7 +628,8 @@
 declare (in CLF) CO_refl_on[simp] refl_on_def [simp]
 
 lemma (in CLF) rel_imp_elem: "(x, y) \<in> r ==> x \<in> A"
-by (metis CO_refl_on refl_onD1)
+  by (metis (no_types, lifting) A_def PartialOrder_def cl_po mem_Collect_eq
+      mem_Sigma_iff r_def subsetD)
 
 declare (in CLF) CO_refl_on[simp del]  refl_on_def [simp del]
 
@@ -626,7 +637,8 @@
 declare interval_def [simp]
 
 lemma (in CLF) interval_subset: "[| a \<in> A; b \<in> A |] ==> interval r a b \<subseteq> A"
-by (metis CO_refl_on interval_imp_mem refl_onD refl_onD2 rel_imp_elem subset_eq)
+  by (metis PO.interval_imp_mem PO.intro dualPO dualr_iff interval_dual r_def
+      rel_imp_elem subsetI)
 
 declare (in CLF) rel_imp_elem[rule del]
 declare interval_def [simp del]

--- a/src/HOL/Nonstandard_Analysis/StarDef.thy	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Nonstandard_Analysis/StarDef.thy	Thu Mar 13 15:49:15 2025 +0100
@@ -51,6 +51,7 @@
 
 lemma equiv_starrel: "equiv UNIV starrel"
 proof (rule equivI)
+  show "starrel \<subseteq> UNIV \<times> UNIV" by simp
   show "refl starrel" by (simp add: refl_on_def)
   show "sym starrel" by (simp add: sym_def eq_commute)
   show "trans starrel" by (intro transI) (auto elim: eventually_elim2)

--- a/src/HOL/Order_Relation.thy	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Order_Relation.thy	Thu Mar 13 15:49:15 2025 +0100
@@ -11,7 +11,7 @@
 
 subsection \<open>Orders on a set\<close>
 
-definition "preorder_on A r \<equiv> refl_on A r \<and> trans r"
+definition "preorder_on A r \<equiv> r \<subseteq> A \<times> A \<and> refl_on A r \<and> trans r"
 
 definition "partial_order_on A r \<equiv> preorder_on A r \<and> antisym r"
 
@@ -26,7 +26,7 @@
   strict_linear_order_on_def well_order_on_def
 
 lemma partial_order_onD:
-  assumes "partial_order_on A r" shows "refl_on A r" and "trans r" and "antisym r"
+  assumes "partial_order_on A r" shows "refl_on A r" and "trans r" and "antisym r" and "r \<subseteq> A \<times> A"
   using assms unfolding partial_order_on_def preorder_on_def by auto
 
 lemma preorder_on_empty[simp]: "preorder_on {} {}"
@@ -43,7 +43,7 @@
 
 
 lemma preorder_on_converse[simp]: "preorder_on A (r\<inverse>) = preorder_on A r"
-  by (simp add: preorder_on_def)
+  by (auto simp add: preorder_on_def)
 
 lemma partial_order_on_converse[simp]: "partial_order_on A (r\<inverse>) = partial_order_on A r"
   by (simp add: partial_order_on_def)
@@ -153,8 +153,54 @@
 definition relation_of :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set"
   where "relation_of P A \<equiv> { (a, b) \<in> A \<times> A. P a b }"
 
+lemma refl_relation_ofD: "refl (relation_of R S) \<Longrightarrow> reflp_on S R"
+  by (auto simp: relation_of_def intro: reflp_onI dest: reflD)
+
+lemma irrefl_relation_ofD: "irrefl (relation_of R S) \<Longrightarrow> irreflp_on S R"
+  by (auto simp: relation_of_def intro: irreflp_onI dest: irreflD)
+
+lemma sym_relation_of[simp]: "sym (relation_of R S) \<longleftrightarrow> symp_on S R"
+proof (rule iffI)
+  show "sym (relation_of R S) \<Longrightarrow> symp_on S R"
+    by (auto simp: relation_of_def intro: symp_onI dest: symD)
+next
+  show "symp_on S R \<Longrightarrow> sym (relation_of R S)"
+    by (auto simp: relation_of_def intro: symI dest: symp_onD)
+qed
+
+lemma asym_relation_of[simp]: "asym (relation_of R S) \<longleftrightarrow> asymp_on S R"
+proof (rule iffI)
+  show "asym (relation_of R S) \<Longrightarrow> asymp_on S R"
+    by (auto simp: relation_of_def intro: asymp_onI dest: asymD)
+next
+  show "asymp_on S R \<Longrightarrow> asym (relation_of R S)"
+    by (auto simp: relation_of_def intro: asymI dest: asymp_onD)
+qed
+
+lemma antisym_relation_of[simp]: "antisym (relation_of R S) \<longleftrightarrow> antisymp_on S R"
+proof (rule iffI)
+  show "antisym (relation_of R S) \<Longrightarrow> antisymp_on S R"
+    by (simp add: antisym_on_def antisymp_on_def relation_of_def)
+next
+  show "antisymp_on S R \<Longrightarrow> antisym (relation_of R S)"
+    by (simp add: antisym_on_def antisymp_on_def relation_of_def)
+qed
+
+lemma trans_relation_of[simp]: "trans (relation_of R S) \<longleftrightarrow> transp_on S R"
+proof (rule iffI)
+  show "trans (relation_of R S) \<Longrightarrow> transp_on S R"
+    by (auto simp: relation_of_def intro: transp_onI dest: transD)
+next
+  show "transp_on S R \<Longrightarrow> trans (relation_of R S)"
+    by (auto simp: relation_of_def intro: transI dest: transp_onD)
+qed
+
+lemma total_relation_ofD: "total (relation_of R S) \<Longrightarrow> totalp_on S R"
+  by (auto simp: relation_of_def total_on_def intro: totalp_onI)
+
 lemma Field_relation_of:
-  assumes "refl_on A (relation_of P A)" shows "Field (relation_of P A) = A"
+  assumes "relation_of P A \<subseteq> A \<times> A" and "refl_on A (relation_of P A)"
+  shows "Field (relation_of P A) = A"
   using assms unfolding refl_on_def Field_def by auto
 
 lemma partial_order_on_relation_ofI:
@@ -163,8 +209,10 @@
     and antisym: "\<And>a b. \<lbrakk> a \<in> A; b \<in> A \<rbrakk> \<Longrightarrow> P a b \<Longrightarrow> P b a \<Longrightarrow> a = b"
   shows "partial_order_on A (relation_of P A)"
 proof -
-  from refl have "refl_on A (relation_of P A)"
-    unfolding refl_on_def relation_of_def by auto
+  have "relation_of P A \<subseteq> A \<times> A"
+    unfolding relation_of_def by auto
+  moreover have "refl_on A (relation_of P A)"
+    using refl unfolding refl_on_def relation_of_def by auto
   moreover have "trans (relation_of P A)" and "antisym (relation_of P A)"
     unfolding relation_of_def
     by (auto intro: transI dest: trans, auto intro: antisymI dest: antisym)
@@ -173,8 +221,15 @@
 qed
 
 lemma Partial_order_relation_ofI:
-  assumes "partial_order_on A (relation_of P A)" shows "Partial_order (relation_of P A)"
-  using Field_relation_of assms partial_order_on_def preorder_on_def by fastforce
+  assumes "partial_order_on A (relation_of P A)"
+  shows "Partial_order (relation_of P A)"
+proof -
+  have *: "Field (relation_of P A) = A"
+    using assms by (simp_all only: Field_relation_of partial_order_on_def preorder_on_def)
+  show ?thesis
+    unfolding *
+    using assms .
+qed
 
 
 subsection \<open>Orders on a type\<close>
@@ -197,11 +252,8 @@
 
 subsubsection \<open>Auxiliaries\<close>
 
-lemma refl_on_domain: "refl_on A r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> a \<in> A \<and> b \<in> A"
-  by (auto simp add: refl_on_def)
-
 corollary well_order_on_domain: "well_order_on A r \<Longrightarrow> (a, b) \<in> r \<Longrightarrow> a \<in> A \<and> b \<in> A"
-  by (auto simp add: refl_on_domain order_on_defs)
+  by (auto simp add: order_on_defs)
 
 lemma well_order_on_Field: "well_order_on A r \<Longrightarrow> A = Field r"
   by (auto simp add: refl_on_def Field_def order_on_defs)

--- a/src/HOL/Relation.thy	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Relation.thy	Thu Mar 13 15:49:15 2025 +0100
@@ -151,7 +151,7 @@
 subsubsection \<open>Reflexivity\<close>
 
 definition refl_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
-  where "refl_on A r \<longleftrightarrow> r \<subseteq> A \<times> A \<and> (\<forall>x\<in>A. (x, x) \<in> r)"
+  where "refl_on A r \<longleftrightarrow> (\<forall>x\<in>A. (x, x) \<in> r)"
 
 abbreviation refl :: "'a rel \<Rightarrow> bool" \<comment> \<open>reflexivity over a type\<close>
   where "refl \<equiv> refl_on UNIV"
@@ -170,7 +170,7 @@
 lemma reflp_refl_eq [pred_set_conv]: "reflp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> refl r"
   by (simp add: refl_on_def reflp_def)
 
-lemma refl_onI [intro?]: "r \<subseteq> A \<times> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> (x, x) \<in> r) \<Longrightarrow> refl_on A r"
+lemma refl_onI [intro?]: "(\<And>x. x \<in> A \<Longrightarrow> (x, x) \<in> r) \<Longrightarrow> refl_on A r"
   unfolding refl_on_def by (iprover intro!: ballI)
 
 lemma reflI: "(\<And>x. (x, x) \<in> r) \<Longrightarrow> refl r"
@@ -186,12 +186,6 @@
 lemma refl_onD: "refl_on A r \<Longrightarrow> a \<in> A \<Longrightarrow> (a, a) \<in> r"
   unfolding refl_on_def by blast
 
-lemma refl_onD1: "refl_on A r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> x \<in> A"
-  unfolding refl_on_def by blast
-
-lemma refl_onD2: "refl_on A r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> y \<in> A"
-  unfolding refl_on_def by blast
-
 lemma reflD: "refl r \<Longrightarrow> (a, a) \<in> r"
   unfolding refl_on_def by blast
 
@@ -252,10 +246,6 @@
 lemma refl_on_singleton [simp]: "refl_on {x} {(x, x)}"
 by (blast intro: refl_onI)
 
-lemma refl_on_def' [nitpick_unfold, code]:
-  "refl_on A r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<in> A \<and> y \<in> A) \<and> (\<forall>x \<in> A. (x, x) \<in> r)"
-  by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2)
-
 lemma reflp_on_equality [simp]: "reflp_on A (=)"
   by (simp add: reflp_on_def)
 
@@ -952,7 +942,7 @@
   by blast
 
 lemma refl_on_Id_on: "refl_on A (Id_on A)"
-  by (rule refl_onI [OF Id_on_subset_Times Id_onI])
+  by (rule refl_onI[OF Id_onI])
 
 lemma antisym_Id_on [simp]: "antisym (Id_on A)"
   unfolding antisym_def by blast

--- a/src/HOL/Set_Interval.thy	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Set_Interval.thy	Thu Mar 13 15:49:15 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	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Sledgehammer.thy	Thu Mar 13 15:49:15 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	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML	Thu Mar 13 15:49:15 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/BNF/bnf_gfp_tactics.ML	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Thu Mar 13 15:49:15 2025 +0100
@@ -338,18 +338,19 @@
     rtac ctxt equalityD2, rtac ctxt (mk_nth_conv n i)] 1;
 
 fun mk_equiv_lsbis_tac ctxt sbis_lsbis lsbis_incl incl_lsbis bis_Id_on bis_converse bis_O =
-  EVERY' [rtac ctxt (@{thm equiv_def} RS iffD2),
+  EVERY' [rtac ctxt @{thm equivI},
+    rtac ctxt lsbis_incl,
 
-    rtac ctxt conjI, rtac ctxt (@{thm refl_on_def} RS iffD2),
-    rtac ctxt conjI, rtac ctxt lsbis_incl, rtac ctxt ballI, rtac ctxt set_mp,
+    rtac ctxt @{thm refl_onI},
+    rtac ctxt set_mp,
     rtac ctxt incl_lsbis, rtac ctxt bis_Id_on, assume_tac ctxt, etac ctxt @{thm Id_onI},
 
-    rtac ctxt conjI, rtac ctxt (@{thm sym_def} RS iffD2),
-    rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, rtac ctxt set_mp,
+    rtac ctxt @{thm symI},
+    rtac ctxt set_mp,
     rtac ctxt incl_lsbis, rtac ctxt bis_converse, rtac ctxt sbis_lsbis, etac ctxt @{thm converseI},
 
-    rtac ctxt (@{thm trans_def} RS iffD2),
-    rtac ctxt allI, rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, rtac ctxt impI, rtac ctxt set_mp,
+    rtac ctxt @{thm transI},
+    rtac ctxt set_mp,
     rtac ctxt incl_lsbis, rtac ctxt bis_O, rtac ctxt sbis_lsbis, rtac ctxt sbis_lsbis,
     etac ctxt @{thm relcompI}, assume_tac ctxt] 1;
 

--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Thu Mar 13 15:49:15 2025 +0100
@@ -94,7 +94,7 @@
 
 val str = string_of_int
 val str3 = Real.fmt (StringCvt.FIX (SOME 3))
-fun percentage a b = string_of_int (a * 100 div b)
+fun percentage a b = Real.fmt (StringCvt.FIX (SOME 1)) (Real.fromInt (a * 100) / Real.fromInt b)
 fun ms t = Real.fromInt t / 1000.0
 fun avg_time t n =
   if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0
@@ -157,7 +157,7 @@
 
 in
 
-fun run_sledgehammer (params as {provers, ...}) output_dir keep_probs keep_proofs
+fun run_sledgehammer params output_dir keep_probs keep_proofs
     exhaustive_preplay thy_index trivial pos st =
   let
     val triv_str = if trivial then "[T] " else ""
@@ -176,7 +176,6 @@
         end
       else
         NONE
-    val prover_name = hd provers
     val (sledgehamer_outcome, msg, cpu_time) = run_sh params keep pos st
     val (time_prover, change_data, exhaustive_preplay_msg) =
       (case sledgehamer_outcome of
@@ -208,8 +207,7 @@
       | _ => (NONE, I, ""))
     val outcome_msg =
       "(SH " ^ string_of_int cpu_time ^ "ms" ^
-      (case time_prover of NONE => "" | SOME ms => ", ATP " ^ string_of_int ms ^ "ms") ^
-      ") [" ^ prover_name ^ "]: "
+      (case time_prover of NONE => "" | SOME ms => ", ATP " ^ string_of_int ms ^ "ms") ^ "): "
   in
     (sledgehamer_outcome, triv_str ^ outcome_msg ^ Protocol_Message.clean_output msg ^
        (if exhaustive_preplay_msg = "" then "" else ("\n" ^ exhaustive_preplay_msg)),

--- a/src/HOL/Tools/SMT/smt_systems.ML	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Tools/SMT/smt_systems.ML	Thu Mar 13 15:49:15 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	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Mar 13 15:49:15 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	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Mar 13 15:49:15 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)
   |> implode_param
 
 fun set_default_raw_param param thy =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Mar 13 15:49:15 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	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Thu Mar 13 15:49:15 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	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu Mar 13 15:49:15 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	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Mar 13 15:49:15 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	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Thu Mar 13 15:49:15 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	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Thu Mar 13 15:49:15 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	Thu Mar 13 15:49:15 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	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Tools/try0.ML	Thu Mar 13 15:49:15 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

--- a/src/HOL/Wellfounded.thy	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Wellfounded.thy	Thu Mar 13 15:49:15 2025 +0100
@@ -393,36 +393,88 @@
   using wfp_on_antimono_strong .
 
 
+subsubsection \<open>Equivalence between \<^const>\<open>wfp_on\<close> and \<^const>\<open>wfp\<close>\<close>
+
+lemma wfp_on_iff_wfp: "wfp_on A R \<longleftrightarrow> wfp (\<lambda>x y. R x y \<and>  x \<in> A \<and> y \<in> A)"
+  (is "?LHS \<longleftrightarrow> ?RHS")
+proof (rule iffI)
+  assume ?LHS
+  then show ?RHS
+    unfolding wfp_on_iff_ex_minimal
+    by force
+next
+  assume ?RHS
+  thus ?LHS
+  proof (rule wfp_on_antimono_strong)
+    show "A \<subseteq> UNIV"
+      using subset_UNIV .
+  next
+    show "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> R x y \<Longrightarrow> R x y \<and> x \<in> A \<and> y \<in> A"
+      by iprover
+  qed
+qed
+
+
 subsubsection \<open>Well-foundedness of transitive closure\<close>
 
+lemma bex_rtrancl_min_element_if_wf_on:
+  assumes wf: "wf_on A r" and x_in: "x \<in> A"
+  shows "\<exists>y \<in> A. (y, x) \<in> r\<^sup>* \<and> \<not>(\<exists>z \<in> A. (z, y) \<in> r)"
+  using wf
+proof (induction x rule: wf_on_induct)
+  case in_set
+  thus ?case
+    using x_in .
+next
+  case (less z)
+  show ?case                            
+  proof (cases "\<exists>y \<in> A. (y, z) \<in> r")
+    case True
+    then obtain y where "y \<in> A" and "(y, z) \<in> r"
+      by blast
+    then obtain x where "x \<in> A" and "(x, y) \<in> r\<^sup>*" and "\<not> (\<exists>w\<in>A. (w, x) \<in> r)"
+      using less.IH by blast
+    show ?thesis
+    proof (intro bexI conjI)
+      show "(x, z) \<in> r\<^sup>*"
+        using rtrancl.rtrancl_into_rtrancl[of x y r z]
+        using \<open>(x, y) \<in> r\<^sup>*\<close> \<open>(y, z) \<in> r\<close> by blast
+    next
+      show "\<not> (\<exists>z\<in>A. (z, x) \<in> r)"
+        using \<open>\<not> (\<exists>w\<in>A. (w, x) \<in> r)\<close> .
+    next
+      show "x \<in> A"
+        using \<open>x \<in> A\<close> .
+    qed
+  next
+    case False
+    show ?thesis
+    proof (intro bexI conjI)
+      show "(z, z) \<in> r\<^sup>*"
+        using rtrancl.rtrancl_refl .
+    next
+      show "\<not> (\<exists>w\<in>A. (w, z) \<in> r)"
+        using False .
+    next
+      show "z \<in> A"
+        using less.hyps .
+    qed
+  qed
+qed
+
+lemma bex_rtransclp_min_element_if_wfp_on: "wfp_on A R \<Longrightarrow> x \<in> A \<Longrightarrow> \<exists>y\<in>A. R\<^sup>*\<^sup>* y x \<and> \<not> (\<exists>z\<in>A. R z y)"
+  by (rule bex_rtrancl_min_element_if_wf_on[to_pred])
+
 lemma ex_terminating_rtranclp_strong:
   assumes wf: "wfp_on {x'. R\<^sup>*\<^sup>* x x'} R\<inverse>\<inverse>"
   shows "\<exists>y. R\<^sup>*\<^sup>* x y \<and> (\<nexists>z. R y z)"
-proof (cases "\<exists>y. R x y")
-  case True
-  with wf show ?thesis
-  proof (induction rule: Wellfounded.wfp_on_induct)
-    case in_set
-    thus ?case
-      by simp
-  next
-    case (less y)
-    have "R\<^sup>*\<^sup>* x y"
-      using less.hyps mem_Collect_eq[of _ "R\<^sup>*\<^sup>* x"] by iprover
+proof -
+  have x_in: "x \<in> {x'. R\<^sup>*\<^sup>* x x'}"
+    by simp
 
-    moreover obtain z where "R y z"
-      using less.prems by iprover
-
-    ultimately have "R\<^sup>*\<^sup>* x z"
-      using rtranclp.rtrancl_into_rtrancl[of R x y z] by iprover
-
-    show ?case
-      using \<open>R y z\<close> \<open>R\<^sup>*\<^sup>* x z\<close> less.IH[of z] rtranclp_trans[of R y z] by blast
-  qed
-next
-  case False
-  thus ?thesis
-    by blast
+  show ?thesis
+    using bex_rtransclp_min_element_if_wfp_on[OF wf x_in]
+    using rtranclp.rtrancl_into_rtrancl[of R x] by blast
 qed
 
 lemma ex_terminating_rtranclp:
@@ -1189,28 +1241,59 @@
 lemma in_lex_prod[simp]: "((a, b), (a', b')) \<in> r <*lex*> s \<longleftrightarrow> (a, a') \<in> r \<or> a = a' \<and> (b, b') \<in> s"
   by (auto simp:lex_prod_def)
 
+lemma wf_on_lex_prod[intro]:
+  assumes wfA: "wf_on A r\<^sub>A" and wfB: "wf_on B r\<^sub>B"
+  shows "wf_on (A \<times> B) (r\<^sub>A <*lex*> r\<^sub>B)"
+  unfolding wf_on_iff_ex_minimal
+proof (intro allI impI)
+  fix AB assume "AB \<subseteq> A \<times> B" and "AB \<noteq> {}"
+  hence "fst ` AB \<subseteq> A" and "snd ` AB \<subseteq> B"
+    by auto
+
+  from \<open>fst ` AB \<subseteq> A\<close> \<open>AB \<noteq> {}\<close> obtain a where
+    a_in: "a \<in> fst ` AB" and
+    a_minimal: "(\<forall>y. (y, a) \<in> r\<^sub>A \<longrightarrow> y \<notin> fst ` AB)"
+    using wfA[unfolded wf_on_iff_ex_minimal, rule_format, of "fst ` AB"]
+    by auto
+
+  from \<open>snd ` AB \<subseteq> B\<close> \<open>AB \<noteq> {}\<close> a_in obtain b where
+    b_in: "b \<in> snd ` {p \<in> AB. fst p = a}" and
+    b_minimal: "(\<forall>y. (y, b) \<in> r\<^sub>B \<longrightarrow> y \<notin> snd ` {p \<in> AB. fst p = a})"
+    using wfB[unfolded wf_on_iff_ex_minimal, rule_format, of "snd ` {p \<in> AB. fst p = a}"]
+    by blast
+
+  show "\<exists>z\<in>AB. \<forall>y. (y, z) \<in> r\<^sub>A <*lex*> r\<^sub>B \<longrightarrow> y \<notin> AB"
+  proof (rule bexI)
+    show "(a, b) \<in> AB"
+      using b_in by (simp add: image_iff)
+  next
+    show "\<forall>y. (y, (a, b)) \<in> r\<^sub>A <*lex*> r\<^sub>B \<longrightarrow> y \<notin> AB"
+    proof (intro allI impI)
+      fix p assume "(p, (a, b)) \<in> r\<^sub>A <*lex*> r\<^sub>B"
+      hence "(fst p, a) \<in> r\<^sub>A \<or> fst p = a \<and> (snd p, b) \<in> r\<^sub>B"
+        unfolding lex_prod_def by auto
+      thus "p \<notin> AB"
+      proof (elim disjE conjE)
+        assume "(fst p, a) \<in> r\<^sub>A"
+        hence "fst p \<notin> fst ` AB"
+          using a_minimal by simp
+        thus ?thesis
+          by (rule contrapos_nn) simp
+      next
+        assume "fst p = a" and "(snd p, b) \<in> r\<^sub>B"
+        hence "snd p \<notin> snd ` {p \<in> AB. fst p = a}"
+          using b_minimal by simp
+        thus "p \<notin> AB"
+          by (rule contrapos_nn) (simp add: \<open>fst p = a\<close>)
+      qed
+    qed
+  qed
+qed
+
 lemma wf_lex_prod [intro!]:
   assumes "wf ra" "wf rb"
   shows "wf (ra <*lex*> rb)"
-proof (rule wfI)
-  fix z :: "'a \<times> 'b" and P
-  assume * [rule_format]: "\<forall>u. (\<forall>v. (v, u) \<in> ra <*lex*> rb \<longrightarrow> P v) \<longrightarrow> P u"
-  obtain x y where zeq: "z = (x,y)"
-    by fastforce
-  have "P(x,y)" using \<open>wf ra\<close>
-  proof (induction x arbitrary: y rule: wf_induct_rule)
-    case (less x)
-    note lessx = less
-    show ?case using \<open>wf rb\<close> less
-    proof (induction y rule: wf_induct_rule)
-      case (less y)
-      show ?case
-        by (force intro: * less.IH lessx)
-    qed
-  qed
-  then show "P z"
-    by (simp add: zeq)
-qed auto
+  using wf_on_lex_prod[OF \<open>wf ra\<close> \<open>wf rb\<close>, unfolded UNIV_Times_UNIV] .
 
 lemma refl_lex_prod[simp]: "refl r\<^sub>B \<Longrightarrow> refl (r\<^sub>A <*lex*> r\<^sub>B)"
   by (auto intro!: reflI dest: refl_onD)

--- a/src/HOL/ZF/Games.thy	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/ZF/Games.thy	Thu Mar 13 15:49:15 2025 +0100
@@ -816,6 +816,9 @@
 
 lemma equiv_eq_game[simp]: "equiv UNIV eq_game_rel"
 proof (rule equivI)
+  show "eq_game_rel \<subseteq> UNIV \<times> UNIV"
+    by simp
+next
   show "refl eq_game_rel"
     by (auto simp only: eq_game_rel_def intro: reflI eq_game_refl)
 next

--- a/src/HOL/Zorn.thy	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/Zorn.thy	Thu Mar 13 15:49:15 2025 +0100
@@ -543,7 +543,7 @@
     unfolding relation_of_def using that by auto
   ultimately have "\<exists>m\<in>A. \<forall>a\<in>A. (m, a) \<in> relation_of P A \<longrightarrow> a = m"
     using Zorns_po_lemma[OF Partial_order_relation_ofI[OF po], rule_format] ch
-    unfolding Field_relation_of[OF partial_order_onD(1)[OF po]] by blast
+    unfolding Field_relation_of[OF partial_order_onD(4)[OF po] partial_order_onD(1)[OF po]] by blast
   then show ?thesis
     by (auto simp: relation_of_def)
 qed
@@ -749,7 +749,9 @@
     have "\<forall>r\<in>R. Refl r" and "\<forall>r\<in>R. trans r" and "\<forall>r\<in>R. antisym r"
       and "\<forall>r\<in>R. Total r" and "\<forall>r\<in>R. wf (r - Id)"
       using Chains_wo [OF \<open>R \<in> Chains I\<close>] by (simp_all add: order_on_defs)
-    have "Refl (\<Union>R)"
+    have "(\<Union> R) \<subseteq> Field (\<Union> R) \<times> Field (\<Union> R)"
+      unfolding Field_def by auto
+    moreover have "Refl (\<Union>R)"
       using \<open>\<forall>r\<in>R. Refl r\<close> unfolding refl_on_def by fastforce
     moreover have "trans (\<Union>R)"
       by (rule chain_subset_trans_Union [OF subch \<open>\<forall>r\<in>R. trans r\<close>])
@@ -798,10 +800,13 @@
     let ?m = "insert (x, x) m \<union> ?s"
     have Fm: "Field ?m = insert x (Field m)"
       by (auto simp: Field_def)
-    have "Refl m" and "trans m" and "antisym m" and "Total m" and "wf (m - Id)"
+    have "Refl m" and "trans m" and "antisym m" and "Total m" and "wf (m - Id)" and
+      "m \<subseteq> Field m \<times> Field m"
       using \<open>Well_order m\<close> by (simp_all add: order_on_defs)
 \<comment> \<open>We show that the extension is a well-order\<close>
-    have "Refl ?m"
+    have "?m \<subseteq> Field ?m \<times> Field ?m"
+      using \<open>m \<subseteq> Field m \<times> Field m\<close> by auto
+    moreover have "Refl ?m"
       using \<open>Refl m\<close> Fm unfolding refl_on_def by blast
     moreover have "trans ?m" using \<open>trans m\<close> and \<open>x \<notin> Field m\<close>
       unfolding trans_def Field_def by blast
@@ -839,9 +844,12 @@
   let ?r = "{(x, y). x \<in> A \<and> y \<in> A \<and> (x, y) \<in> r}"
   have 1: "Field ?r = A"
     using wo univ by (fastforce simp: Field_def order_on_defs refl_on_def)
-  from \<open>Well_order r\<close> have "Refl r" "trans r" "antisym r" "Total r" "wf (r - Id)"
+  from \<open>Well_order r\<close> have "Refl r" "trans r" "antisym r" "Total r" "wf (r - Id)" and
+    "r \<subseteq> Field r \<times> Field r"
     by (simp_all add: order_on_defs)
-  from \<open>Refl r\<close> have "Refl ?r"
+  have "?r \<subseteq> Field ?r \<times> Field ?r"
+      using \<open>r \<subseteq> Field r \<times> Field r\<close> by (auto simp: 1)
+  moreover from \<open>Refl r\<close> have "Refl ?r"
     by (auto simp: refl_on_def 1 univ)
   moreover from \<open>trans r\<close> have "trans ?r"
     unfolding trans_def by blast

--- a/src/HOL/ex/Tarski.thy	Thu Mar 13 11:19:27 2025 +0100
+++ b/src/HOL/ex/Tarski.thy	Thu Mar 13 15:49:15 2025 +0100
@@ -59,7 +59,8 @@
   where "Top po = greatest (\<lambda>x. True) po"
 
 definition PartialOrder :: "'a potype set"
-  where "PartialOrder = {P. refl_on (pset P) (order P) \<and> antisym (order P) \<and> trans (order P)}"
+  where "PartialOrder = {P. order P \<subseteq> pset P \<times> pset P \<and>
+    refl_on (pset P) (order P) \<and> antisym (order P) \<and> trans (order P)}"
 
 definition CompleteLattice :: "'a potype set"
   where "CompleteLattice =
@@ -159,6 +160,10 @@
 lemma po_subset_po: 
   assumes "S \<subseteq> A" shows "\<lparr>pset = S, order = induced S r\<rparr> \<in> PartialOrder"
 proof -
+  have "induced S r \<subseteq> S \<times> S"
+    by (metis (lifting) BNF_Def.Collect_case_prodD induced_def mem_Sigma_iff
+        prod.sel subrelI)
+  moreover
   have "refl_on S (induced S r)"
     using \<open>S \<subseteq> A\<close> by (auto simp: refl_on_def induced_def intro: reflE)
   moreover
@@ -197,7 +202,7 @@
   by (simp add: isLub_def isGlb_def dual_def converse_unfold)
 
 lemma (in PO) dualPO: "dual cl \<in> PartialOrder"
-  using cl_po by (simp add: PartialOrder_def dual_def)
+  using cl_po by (simp add: PartialOrder_def dual_def converse_Times flip: converse_subset_swap)
 
 lemma Rdual:
   assumes major: "\<And>S. S \<subseteq> A \<Longrightarrow> \<exists>L. isLub S po L" and "S \<subseteq> A" and "A = pset po"
@@ -453,9 +458,10 @@
     have "(lub H cl, f (lub H cl)) \<in> r"
       using assms lubH_le_flubH by blast
     then have "(f (lub H cl), f (f (lub H cl))) \<in> r"
-      by (meson PO_imp_refl_on monotoneE monotone_f refl_on_domain)
+      by (metis (lifting) PiE assms f_in_funcset lub_in_lattice mem_Collect_eq
+          monotoneE monotone_f subsetI)
     then have "f (lub H cl) \<in> H"
-      by (metis (no_types, lifting) PO_imp_refl_on assms mem_Collect_eq refl_on_domain)
+      using assms f_in_funcset lub_in_lattice by auto
     then show ?thesis
       by (simp add: assms lub_upper)
   qed
@@ -510,7 +516,7 @@
 subsection \<open>interval\<close>
 
 lemma rel_imp_elem: "(x, y) \<in> r \<Longrightarrow> x \<in> A"
-  using CO_refl_on by (auto simp: refl_on_def)
+  using A_def PartialOrder_def cl_po r_def by blast
 
 lemma interval_subset: "\<lbrakk>a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> interval r a b \<subseteq> A"
   by (simp add: interval_def) (blast intro: rel_imp_elem)
@@ -665,7 +671,7 @@
     using assms intY1_elem interval_imp_mem lubY_in_A unfolding intY1_def
     using lubY_le_flubY monotoneE monotone_f po.transE by blast
   then show "(f x, Top cl) \<in> r"
-    by (meson PO_imp_refl_on Top_prop refl_onD2)
+    by (metis assms f_in_funcset intY1_elem[of x] Top_prop[of "f x"] PiE[of f A "\<lambda>_. A" x])
 qed
 
 lemma intY1_mono: "monotone (\<lambda> x \<in> intY1. f x) intY1 (induced intY1 r)"