--- 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]").
--- 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
--- 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)
--- 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 *)
--- 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 *)
--- 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
--- 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,
--- 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,