--- a/CONTRIBUTORS Thu Jan 09 23:06:17 2025 +0100
+++ b/CONTRIBUTORS Thu Jan 09 13:18:37 2025 +0100
@@ -6,7 +6,7 @@
Contributions to this Isabelle version
--------------------------------------
-* October 2024: Lukas Bartl, LMU München
+* October 2024 - January 2025: Lukas Bartl, Universität Augsburg
Inference of variable instantiations with Metis.
* April - October 2024: Thomas Lindae and Fabian Huch, TU München
--- a/src/Doc/Sledgehammer/document/root.tex Thu Jan 09 23:06:17 2025 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Jan 09 13:18:37 2025 +0100
@@ -66,7 +66,7 @@
Lawrence C. Paulson \\
{\normalsize Computer Laboratory, University of Cambridge} \\[4\smallskipamount]
Lukas Bartl \\
-{\normalsize Institut f\"ur Informatik, Ludwig-Maximilians-Universit\"at M\"unchen} \\
+{\normalsize Institut f\"ur Informatik, Universit\"at Augsburg} \\
\hbox{}}
\maketitle
@@ -631,8 +631,8 @@
\end{enum}
The \textit{metis} method also supports the Isabelle option
-[[\textit{metis\_suggest\_of}]], which tells \textit{metis} to suggest
-instantiations of facts using \textbf{of} from a successful proof.
+[[\textit{metis\_instantiate}]], which tells \textit{metis} to infer and
+suggest instantiations of facts using \textbf{of} from a successful proof.
\section{Option Reference}
\label{option-reference}
@@ -1219,7 +1219,7 @@
Specifies whether the \textit{smt} proof method should be tried in addition to
Isabelle's built-in proof methods.
-\opsmart{suggest\_of}{dont\_suggest\_of}
+\opsmart{instantiate}{dont\_instantiate}
Specifies whether Metis should try to infer variable instantiations before proof
reconstruction, which results in instantiations of facts using \textbf{of}
(e.g. \textit{map\_prod\_surj\_on}[\textbf{of} \textit{f A} "\textit{f}
--- a/src/HOL/Tools/Metis/metis_instantiations.ML Thu Jan 09 23:06:17 2025 +0100
+++ b/src/HOL/Tools/Metis/metis_instantiations.ML Thu Jan 09 13:18:37 2025 +0100
@@ -1,5 +1,5 @@
(* Title: HOL/Tools/Metis/metis_instantiations.ML
- Author: Lukas Bartl, LMU Muenchen
+ Author: Lukas Bartl, Universitaet Augsburg
Inference of Variable Instantiations for Metis.
*)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_instantiations.ML Thu Jan 09 23:06:17 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_instantiations.ML Thu Jan 09 13:18:37 2025 +0100
@@ -1,5 +1,5 @@
-(* Title: HOL/Tools/Metis/metis_instantiations.ML
- Author: Lukas Bartl, LMU Muenchen
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_instantiations.ML
+ Author: Lukas Bartl, Universitaet Augsburg
Inference of Variable Instantiations with Metis.
*)
@@ -88,13 +88,12 @@
(case timed_infer_thm_insts metis_method of
NONE => infer_thm_insts metis_methods
| thm_insts => thm_insts)
- fun fact_of_thm_inst (th, inst) =
- List.find (fn (_, ths) => member Thm.eq_thm ths th) fact_thms
- |> Option.map (apfst (rpair inst) o fst)
- |> Option.map (apfst (Metis_Tactic.pretty_name_inst ctxt))
+ fun instantiate_fact ((name, stature), ths) thm_insts =
+ List.partition (member Thm.eq_thm ths o fst) thm_insts
+ |>> map (fn (_, inst) => (Metis_Tactic.pretty_name_inst ctxt (name, inst), stature))
in
infer_thm_insts (metis_methods ctxt)
- |> Option.map (map_filter fact_of_thm_inst)
+ |> Option.map (flat o fst o fold_map instantiate_fact fact_thms)
|> verbose ? tap (Option.app (fn inst_facts =>
Pretty.str "Instantiated facts:" :: map fst inst_facts
|> Pretty.block o Pretty.breaks