# HG changeset patch
# User Lukas Bartl
# Date 1734979096 -3600
# Node ID 8b4340d82248789794f4dd2faba0bf6529fc7573
# Parent  2f70c60cdbb2c20f3bdca6099a0cfd4dc6ce2765
Rename "suggest_of" to "instantiate"

diff -r 2f70c60cdbb2 -r 8b4340d82248 NEWS
--- a/NEWS	Wed Jan 08 05:38:13 2025 +0100
+++ b/NEWS	Mon Dec 23 19:38:16 2024 +0100
@@ -240,7 +240,7 @@
       . E 3.1 -- with patch on Windows/Cygwin for proper interrupts
   - Added instantiations of facts using the "of" attribute
     (e.g. "assms(1)[of x]"), which can be activated using the
-    Sledgehammer option "suggest_of" (default: smart, i.e. only if
+    Sledgehammer option "instantiate" (default: smart, i.e. only if
     preplaying failed).  This uses Metis internally to infer the
     variable instantiations (see below).
   - Added extensionality (fact "ext") to some "metis (lifting)" calls.
@@ -248,7 +248,7 @@
 
 * Metis:
   - Added inference of variable instantiations, which can be activated
-    using the configuration option "metis_suggest_of" (default: false).
+    using the configuration option "metis_instantiate" (default: false).
     This outputs a suggestion with instantiations of the facts using the
     "of" attribute (e.g. "assms(1)[of x]").
 
diff -r 2f70c60cdbb2 -r 8b4340d82248 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Jan 08 05:38:13 2025 +0100
+++ b/src/HOL/List.thy	Mon Dec 23 19:38:16 2024 +0100
@@ -4429,7 +4429,7 @@
   have 1: "x \<notin> set ?pref" by (metis (full_types) set_takeWhileD)
   have 2: "xs = ?pref @ x # tl ?rest"
     by (metis rest append_eq_conv_conj hd_Cons_tl takeWhile_eq_take)
-  have "count_list (tl ?rest) x = n"using [[metis_suggest_of]]
+  have "count_list (tl ?rest) x = n"
     using assms rest 1 2 count_notin count_list_append[of ?pref "x # tl ?rest" x] by simp
   with 1 2 show ?thesis by blast
 qed
diff -r 2f70c60cdbb2 -r 8b4340d82248 src/HOL/Tools/Metis/metis_instantiations.ML
--- a/src/HOL/Tools/Metis/metis_instantiations.ML	Wed Jan 08 05:38:13 2025 +0100
+++ b/src/HOL/Tools/Metis/metis_instantiations.ML	Mon Dec 23 19:38:16 2024 +0100
@@ -21,14 +21,14 @@
     mth : Metis_Thm.thm
   }
 
-  val suggest_of : bool Config.T
-  val suggest_undefined : bool Config.T
+  val instantiate : bool Config.T
+  val instantiate_undefined : bool Config.T
   val metis_call : string -> string -> string
   val table_of_thm_inst : thm * inst -> cterm Vars.table
   val pretty_name_inst : Proof.context -> string * inst -> Pretty.T
   val string_of_name_inst : Proof.context -> string * inst -> string
   val infer_thm_insts : infer_params -> (thm * inst) list option
-  val suggest_of_call : infer_params -> thm -> unit
+  val instantiate_call : infer_params -> thm -> unit
 end;
 
 structure Metis_Instantiations : METIS_INSTANTIATIONS =
@@ -58,9 +58,9 @@
 }
 
 (* Config option to enable suggestion of of-instantiations (e.g. "assms(1)[of x]") *)
-val suggest_of = Attrib.setup_config_bool @{binding "metis_suggest_of"} (K false)
+val instantiate = Attrib.setup_config_bool @{binding "metis_instantiate"} (K false)
 (* Config option to allow instantiation of variables with "undefined" *)
-val suggest_undefined = Attrib.setup_config_bool @{binding "metis_suggest_undefined"} (K true)
+val instantiate_undefined = Attrib.setup_config_bool @{binding "metis_instantiate_undefined"} (K true)
 
 fun metis_call type_enc lam_trans =
   let
@@ -184,7 +184,7 @@
     (* "undefined" if allowed and not using new_skolem, "_" otherwise. *)
     val undefined_pattern =
       (* new_skolem uses schematic variables which should not be instantiated with "undefined" *)
-      if not new_skolem andalso Config.get ctxt suggest_undefined then
+      if not new_skolem andalso Config.get ctxt instantiate_undefined then
         Const o (pair @{const_name "undefined"})
       else
         Term.dummy_pattern
@@ -408,7 +408,7 @@
   end
 
 (* Infer variable instantiations and suggest of-instantiations *)
-fun suggest_of_call infer_params st =
+fun instantiate_call infer_params st =
   infer_thm_insts infer_params
   |> Option.mapPartial (Option.filter (not o thm_insts_trivial))
   |> Option.app (write_command infer_params st)
diff -r 2f70c60cdbb2 -r 8b4340d82248 src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Wed Jan 08 05:38:13 2025 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Mon Dec 23 19:38:16 2024 +0100
@@ -13,8 +13,8 @@
 
   val trace : bool Config.T
   val verbose : bool Config.T
-  val suggest_of : bool Config.T
-  val suggest_undefined : bool Config.T
+  val instantiate : bool Config.T
+  val instantiate_undefined : bool Config.T
   val new_skolem : bool Config.T
   val advisory_simp : bool Config.T
   val pretty_name_inst : Proof.context -> string * inst -> Pretty.T
@@ -304,11 +304,11 @@
 (* Metis tactic to prove a subgoal and optionally suggest of-instantiations *)
 fun metis_tac' th_name type_encs lam_trans ctxt ths i =
   let
-    val suggest_of = Config.get ctxt suggest_of
-    val suggest_of_tac =
-      if suggest_of then
+    val instantiate = Config.get ctxt instantiate
+    val instantiate_tac =
+      if instantiate then
         (fn (NONE, st) => st
-          | (SOME infer_params, st) => tap (suggest_of_call infer_params) st)
+          | (SOME infer_params, st) => tap (instantiate_call infer_params) st)
       else
         snd
   in
@@ -316,8 +316,8 @@
      * which is bad for inferring variable instantiations.  Metis doesn't need
      * it, so we set it to "false" when we want to infer variable instantiations.
      * We don't do it always because we don't want to break existing proofs. *)
-    metis_tac_infer_params th_name type_encs lam_trans (not suggest_of) ctxt ths i
-    #> Seq.map suggest_of_tac
+    metis_tac_infer_params th_name type_encs lam_trans (not instantiate) ctxt ths i
+    #> Seq.map instantiate_tac
   end
 
 (* Metis tactic without theorem name, therefore won't suggest of-instantiations *)
diff -r 2f70c60cdbb2 -r 8b4340d82248 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Jan 08 05:38:13 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Dec 23 19:38:16 2024 +0100
@@ -221,7 +221,7 @@
    |> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res)))
  end
 
-fun preplay_prover_result ({verbose, suggest_of, minimize, preplay_timeout, ...} : params)
+fun preplay_prover_result ({verbose, instantiate, minimize, preplay_timeout, ...} : params)
     state goal subgoal
     (result as {outcome, used_facts, preferred_methss, message, ...} : prover_result) =
   let
@@ -242,9 +242,9 @@
           fun preplay_succeeded ((_, (Played _, _)) :: _, _) = true
             | preplay_succeeded _ = false
           val instantiate_timeout = Time.scale 5.0 preplay_timeout
-          val suggest_of = if null used_facts0 then SOME false else suggest_of
+          val instantiate = if null used_facts0 then SOME false else instantiate
           val (preplay_results, pretty_used_facts) =
-            (case suggest_of of
+            (case instantiate of
               SOME false => preplay pretty_used_facts0
             | SOME true =>
               (* Always try to infer variable instantiations *)
diff -r 2f70c60cdbb2 -r 8b4340d82248 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Jan 08 05:38:13 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Dec 23 19:38:16 2024 +0100
@@ -71,7 +71,7 @@
    ("compress", "smart"),
    ("try0", "true"),
    ("smt_proofs", "true"),
-   ("suggest_of", "smart"),
+   ("instantiate", "smart"),
    ("minimize", "true"),
    ("slices", string_of_int (12 * Multithreading.max_threads ())),
    ("preplay_timeout", "1"),
@@ -97,7 +97,7 @@
    ("dont_minimize", "minimize"),
    ("dont_try0", "try0"),
    ("no_smt_proofs", "smt_proofs"),
-   ("dont_suggest_of", "suggest_of")]
+   ("dont_instantiate", "instantiate")]
 
 val property_dependent_params = ["provers", "timeout"]
 
@@ -267,7 +267,7 @@
     val compress = Option.map (curry Real.max 1.0) (lookup_option lookup_real "compress")
     val try0 = lookup_bool "try0"
     val smt_proofs = lookup_bool "smt_proofs"
-    val suggest_of = lookup_option lookup_bool "suggest_of"
+    val instantiate = lookup_option lookup_bool "instantiate"
     val minimize = mode <> Auto_Try andalso lookup_bool "minimize"
     val slices = if mode = Auto_Try then 1 else Int.max (1, lookup_int "slices")
     val timeout = lookup_time "timeout"
@@ -283,7 +283,7 @@
      fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances, max_proofs = max_proofs,
      isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs,
-     suggest_of = suggest_of, minimize = minimize, slices = slices, timeout = timeout,
+     instantiate = instantiate, minimize = minimize, slices = slices, timeout = timeout,
      preplay_timeout = preplay_timeout, expect = expect, cache_dir = cache_dir}
   end
 
diff -r 2f70c60cdbb2 -r 8b4340d82248 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed Jan 08 05:38:13 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Dec 23 19:38:16 2024 +0100
@@ -47,7 +47,7 @@
      compress : real option,
      try0 : bool,
      smt_proofs : bool,
-     suggest_of : bool option,
+     instantiate : bool option,
      minimize : bool,
      slices : int,
      timeout : Time.time,
@@ -162,7 +162,7 @@
    compress : real option,
    try0 : bool,
    smt_proofs : bool,
-   suggest_of : bool option,
+   instantiate : bool option,
    minimize : bool,
    slices : int,
    timeout : Time.time,
diff -r 2f70c60cdbb2 -r 8b4340d82248 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Wed Jan 08 05:38:13 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Mon Dec 23 19:38:16 2024 +0100
@@ -82,7 +82,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,
-      suggest_of, minimize, preplay_timeout, induction_rules, cache_dir, ...} : params)
+      instantiate, minimize, preplay_timeout, induction_rules, cache_dir, ...} : params)
     (slice as ((_, _, falsify, _, fact_filter), slice_extra)) silent (prover : prover) timeout i n
     state goal facts =
   let
@@ -98,7 +98,7 @@
        fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters,
        max_new_mono_instances = max_new_mono_instances, max_proofs = 1,
        isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs,
-       suggest_of = suggest_of, minimize = minimize, slices = 1, timeout = timeout,
+       instantiate = instantiate, minimize = minimize, slices = 1, timeout = timeout,
        preplay_timeout = preplay_timeout, expect = "", cache_dir = cache_dir}
     val problem =
       {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,