# HG changeset patch
# User Lukas Bartl
# Date 1736425117 -3600
# Node ID 4d15005da582dc757014507c754aac9023ca30ed
# Parent  1db8d9ee94ea6cc8106b5fb6ca00d6e599b6c3bf
tuned documentation and order of instantiated facts

diff -r 1db8d9ee94ea -r 4d15005da582 CONTRIBUTORS
--- 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
diff -r 1db8d9ee94ea -r 4d15005da582 src/Doc/Sledgehammer/document/root.tex
--- 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}
diff -r 1db8d9ee94ea -r 4d15005da582 src/HOL/Tools/Metis/metis_instantiations.ML
--- 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.
 *)
diff -r 1db8d9ee94ea -r 4d15005da582 src/HOL/Tools/Sledgehammer/sledgehammer_instantiations.ML
--- 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