--- a/CONTRIBUTORS Fri Oct 25 16:57:17 2024 +0200
+++ b/CONTRIBUTORS Fri Oct 25 17:01:23 2024 +0200
@@ -6,6 +6,9 @@
Contributions to this Isabelle version
--------------------------------------
+* October 2024: Lukas Bartl, LMU München
+ Inference of variable instantiations with Metis
+
* April - October 2024: Thomas Lindae and Fabian Huch, TU München
Improvements to the language server for Isabelle/VSCode.
--- a/NEWS Fri Oct 25 16:57:17 2024 +0200
+++ b/NEWS Fri Oct 25 17:01:23 2024 +0200
@@ -90,6 +90,21 @@
*** HOL ***
+* Sledgehammer:
+ - 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
+ preplaying failed). This uses Metis internally to infer the
+ variable instantiations (see below).
+ - Added extensionality (fact "ext") to some "metis (lifting)" calls.
+ - Use pretty-printing to format suggested one-line proofs.
+
+* Metis:
+ - Added inference of variable instantiations, which can be activated
+ using the configuration option "metis_suggest_of" (default: false).
+ This outputs a suggestion with instantiations of the facts using the
+ "of" attribute (e.g. "assms(1)[of x]").
+
* Various declaration bundles support adhoc modification of notation,
notably like this:
@@ -153,8 +168,8 @@
image_mset_diff_if_inj
minus_add_mset_if_not_in_lhs[simp]
-* Transitioinal theory "Divides" moved to "HOL-Library.Divides" and
-supposed to be removed in a furure release. Minor INCOMPATIBILITY.
+* Transitional theory "Divides" moved to "HOL-Library.Divides" and
+supposed to be removed in a future release. Minor INCOMPATIBILITY.
Import "HOL-Library.Divides" and keep an eye on theorems prefixed with
"Divides." to ease transition.
--- a/src/Doc/Sledgehammer/document/root.tex Fri Oct 25 16:57:17 2024 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Fri Oct 25 17:01:23 2024 +0200
@@ -59,16 +59,19 @@
\Large A User's Guide to Sledgehammer for Isabelle/HOL}
\author{\hbox{} \\
Jasmin Blanchette \\
-{\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\[4\smallskipamount]
+{\normalsize Institut f\"ur Informatik, Ludwig-Maximilians-Universit\"at M\"unchen} \\[4\smallskipamount]
{\normalsize with contributions from} \\[4\smallskipamount]
Martin Desharnais \\
{\normalsize Forschungsinstitut CODE, Universit\"at der Bundeswehr M\"unchen} \\[4\smallskipamount]
Lawrence C. Paulson \\
-{\normalsize Computer Laboratory, University of Cambridge} \\
+{\normalsize Computer Laboratory, University of Cambridge} \\[4\smallskipamount]
+Lukas Bartl \\
+{\normalsize Institut f\"ur Informatik, Ludwig-Maximilians-Universit\"at M\"unchen} \\
\hbox{}}
\maketitle
+\newpage
\tableofcontents
\setlength{\parskip}{.7em plus .2em minus .1em}
@@ -313,7 +316,7 @@
\point{Familiarize yourself with the main options}
-Sledgehammer's options are fully documented in \S\ref{command-syntax}. Many of
+Sledgehammer's options are fully documented in \S\ref{option-reference}. Many of
the options are very specialized, but serious users of the tool should at least
familiarize themselves with the following options:
@@ -820,8 +823,8 @@
Alias for \textit{provers}.
\opsmartfalse{falsify}{dont\_falsify}
-Specifies whether Sledgehammer should look for falsifications or for proofs. By
-default, it looks for both.
+Specifies whether Sledgehammer should look for falsifications or for proofs. If
+the option is set to \textit{smart}, it looks for both.
A falsification indicates that the goal, taken as an axiom, would be
inconsistent with some specific background facts if it were added as a lemma,
@@ -836,10 +839,10 @@
and found to be sufficient to prove the goal.
Abduction is currently supported only by E. If the option is set to
-\textit{smart} (the default), abduction is enabled only in some of the E time
-slices, and at most one candidate missing assumption is displayed. You can
-disable abduction altogether by setting the option to 0 or enable it in all
-time slices by setting it to a nonzero value.
+\textit{smart}, abduction is enabled only in some of the E time slices, and at
+most one candidate missing assumption is displayed. You can disable abduction
+altogether by setting the option to 0 or enable it in all time slices by setting
+it to a nonzero value.
\optrueonly{dont\_abduce}
Alias for ``\textit{abduce} = 0''.
@@ -1199,12 +1202,26 @@
\optrue{try0}{dont\_try0}
Specifies whether standard proof methods such as \textit{auto} and
-\textit{blast} should be tried as alternatives to \textit{metis} in Isar proofs.
-The collection of methods is roughly the same as for the \textbf{try0} command.
+\textit{blast} should be tried as alternatives to \textit{metis} or
+\textit{smt}. The collection of methods is roughly the same as
+for the \textbf{try0} command.
\optrue{smt\_proofs}{no\_smt\_proofs}
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}
+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}
+\textasciigrave \textit{A}" \textit{g B} "\textit{g} \textasciigrave
+\textit{B}"]). This can make the proof methods faster and more intelligible. If
+the option is set to \textit{smart} (the default), variable instantiations are
+inferred only if proof reconstruction failed or timed out.
+
+When using \textit{metis} directly, enable the configuration
+option [[\textit{metis\_suggest\_of}]] to directly get a suggestion with
+instantiations of facts using \textbf{of} from a successful proof.
\end{enum}
--- a/src/HOL/Metis.thy Fri Oct 25 16:57:17 2024 +0200
+++ b/src/HOL/Metis.thy Fri Oct 25 17:01:23 2024 +0200
@@ -44,6 +44,7 @@
ML_file \<open>Tools/Metis/metis_generate.ML\<close>
ML_file \<open>Tools/Metis/metis_reconstruct.ML\<close>
+ML_file \<open>Tools/Metis/metis_instantiations.ML\<close>
ML_file \<open>Tools/Metis/metis_tactic.ML\<close>
hide_const (open) select fFalse fTrue fNot fComp fconj fdisj fimplies fAll fEx fequal lambda
--- a/src/HOL/Sledgehammer.thy Fri Oct 25 16:57:17 2024 +0200
+++ b/src/HOL/Sledgehammer.thy Fri Oct 25 17:01:23 2024 +0200
@@ -18,6 +18,7 @@
ML_file \<open>Tools/Sledgehammer/sledgehammer_util.ML\<close>
ML_file \<open>Tools/Sledgehammer/sledgehammer_fact.ML\<close>
ML_file \<open>Tools/Sledgehammer/sledgehammer_proof_methods.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_instantiations.ML\<close>
ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_annotate.ML\<close>
ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_proof.ML\<close>
ML_file \<open>Tools/Sledgehammer/sledgehammer_isar_preplay.ML\<close>
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Fri Oct 25 16:57:17 2024 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Fri Oct 25 17:01:23 2024 +0200
@@ -49,9 +49,11 @@
val used_facts_in_atp_proof : Proof.context -> (string * stature) list -> string atp_proof ->
(string * stature) list
val atp_proof_prefers_lifting : string atp_proof -> bool
+ val is_lam_def_used_in_atp_proof : string atp_proof -> bool
val is_typed_helper_used_in_atp_proof : string atp_proof -> bool
val replace_dependencies_in_line : atp_step_name * atp_step_name list -> ('a, 'b) atp_step ->
('a, 'b) atp_step
+ val uncombine_term : theory -> term -> term
val termify_atp_proof : Proof.context -> string -> ATP_Problem.atp_format ->
ATP_Problem_Generate.type_enc -> string Symtab.table -> (string * term) list ->
int Symtab.table -> string atp_proof -> (term, string) atp_step list
@@ -573,6 +575,9 @@
(is_axiom_used_in_proof is_combinator_def atp_proof,
is_axiom_used_in_proof is_lam_lifted atp_proof) = (false, true)
+val is_lam_def_used_in_atp_proof =
+ is_axiom_used_in_proof (is_combinator_def orf is_lam_lifted)
+
val is_typed_helper_name =
String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix
--- a/src/HOL/Tools/ATP/atp_util.ML Fri Oct 25 16:57:17 2024 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Fri Oct 25 17:01:23 2024 +0200
@@ -19,7 +19,9 @@
val find_enclosed : string -> string -> string -> string list
val nat_subscript : int -> string
val unquote_tvar : string -> string
+ val content_of_pretty : Pretty.T -> string
val maybe_quote : Proof.context -> string -> string
+ val pretty_maybe_quote : Proof.context -> Pretty.T -> Pretty.T
val string_of_ext_time : bool * Time.time -> string
val string_of_time : Time.time -> string
val type_instance : theory -> typ -> typ -> bool
@@ -51,6 +53,8 @@
val short_thm_name : Proof.context -> thm -> string
val map_prod : ('a -> 'b) -> ('c -> 'd) -> 'a * 'c -> 'b * 'd
val compare_length_with : 'a list -> int -> order
+ val scan_and_trace_multi_thm : Context.generic * Token.T list ->
+ (thm list * Token.T list) * (Context.generic * Token.T list)
val forall2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
end;
@@ -140,10 +144,13 @@
val unquote_tvar = perhaps (try (unprefix "'"))
val unquery_var = perhaps (try (unprefix "?"))
+(* unformatted string without markup *)
+val content_of_pretty = Protocol_Message.clean_output o Pretty.unformatted_string_of
+
val is_long_identifier = forall Symbol_Pos.is_identifier o Long_Name.explode
-fun maybe_quote ctxt y =
+fun gen_maybe_quote content_of cartouche quote ctxt y =
let
- val s = Protocol_Message.clean_output y
+ val s = content_of y
val is_literal = Keyword.is_literal (Thy_Header.get_keywords' ctxt)
val q = if Config.get ctxt proof_cartouches then cartouche else quote
in
@@ -151,6 +158,8 @@
not (is_long_identifier (unquery_var s))) orelse
is_literal s) ? q
end
+val maybe_quote = gen_maybe_quote Protocol_Message.clean_output cartouche quote
+val pretty_maybe_quote = gen_maybe_quote content_of_pretty Pretty.cartouche Pretty.quote
fun string_of_ext_time (plus, time) =
let val us = Time.toMicroseconds time in
@@ -432,4 +441,12 @@
fun compare_length_with [] n = if n < 0 then GREATER else if n = 0 then EQUAL else LESS
| compare_length_with (_ :: xs) n = if n <= 0 then GREATER else compare_length_with xs (n - 1)
+(* Scan Attrib.multi_thm and store the input tokens *)
+fun scan_and_trace_multi_thm (context, toks) =
+ let
+ val (thms, (context', toks')) = Attrib.multi_thm (context, toks)
+ in
+ ((thms, take (length toks - length toks') toks), (context', toks'))
+ end
+
end;
--- a/src/HOL/Tools/Meson/meson.ML Fri Oct 25 16:57:17 2024 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Fri Oct 25 17:01:23 2024 +0200
@@ -16,7 +16,7 @@
val size_of_subgoals: thm -> int
val has_too_many_clauses: Proof.context -> term -> bool
val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
- val finish_cnf: thm list -> thm list
+ val finish_cnf: bool -> thm list -> thm list
val presimplified_consts : string list
val presimplify: simp_options -> Proof.context -> thm -> thm
val make_nnf: simp_options -> Proof.context -> thm -> thm
@@ -277,7 +277,7 @@
(*Simplify a clause by applying reflexivity to its negated equality literals*)
fun refl_clause th =
let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (Thm.concl_of th))
- in zero_var_indexes (refl_clause_aux neqs th) end
+ in refl_clause_aux neqs th end
handle TERM _ => th; (*probably dest_Trueprop on a weird theorem*)
@@ -408,8 +408,11 @@
fun make_cnf old_skolem_ths th ctxt =
cnf old_skolem_ths ctxt (th, [])
-(*Generalization, removal of redundant equalities, removal of tautologies.*)
-fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths);
+(*Generalization, optional removal of redundant equalities, removal of tautologies.*)
+fun finish_cnf refl ths = ths
+ |> refl ? map refl_clause
+ |> map zero_var_indexes
+ |> filter (not o is_taut)
(**** Generation of contrapositives ****)
--- a/src/HOL/Tools/Meson/meson_clausify.ML Fri Oct 25 16:57:17 2024 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Fri Oct 25 17:01:23 2024 +0200
@@ -7,6 +7,7 @@
signature MESON_CLAUSIFY =
sig
+ type clause_options = {new_skolem : bool, combs : bool, refl : bool}
val new_skolem_var_prefix : string
val new_nonskolem_var_prefix : string
val is_zapped_var_name : string -> bool
@@ -15,13 +16,15 @@
val introduce_combinators_in_theorem : Proof.context -> thm -> thm
val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool
val ss_only : thm list -> Proof.context -> Proof.context
- val cnf_axiom : Meson.simp_options -> Proof.context -> bool -> bool -> int -> thm
+ val cnf_axiom : Meson.simp_options -> Proof.context -> clause_options -> int -> thm
-> (thm * term) option * thm list
end;
structure Meson_Clausify : MESON_CLAUSIFY =
struct
+type clause_options = {new_skolem : bool, combs : bool, refl : bool}
+
(* the extra "Meson" helps prevent clashes (FIXME) *)
val new_skolem_var_prefix = "MesonSK"
val new_nonskolem_var_prefix = "MesonV"
@@ -367,7 +370,7 @@
end
(* Convert a theorem to CNF, with additional premises due to skolemization. *)
-fun cnf_axiom simp_options ctxt0 new_skolem combinators ax_no th =
+fun cnf_axiom simp_options ctxt0 {new_skolem, combs, refl} ax_no th =
let
val choice_ths = Meson.choice_theorems (Proof_Context.theory_of ctxt0)
val (opt, (nnf_th, ctxt1)) =
@@ -387,10 +390,10 @@
(opt |> Option.map (I #>> singleton (Variable.export ctxt2 ctxt0)
##> (Thm.term_of #> HOLogic.dest_Trueprop
#> singleton (Variable.export_terms ctxt2 ctxt0))),
- cnf_ths |> map (combinators ? introduce_combinators_in_theorem ctxt2
+ cnf_ths |> map (combs ? introduce_combinators_in_theorem ctxt2
#> (case opt of SOME (_, ct) => intr_imp ct | NONE => I))
|> Variable.export ctxt2 ctxt0
- |> Meson.finish_cnf
+ |> Meson.finish_cnf refl
|> map (Thm.close_derivation \<^here>))
end
handle THM _ => (NONE, [])
--- a/src/HOL/Tools/Meson/meson_tactic.ML Fri Oct 25 16:57:17 2024 +0200
+++ b/src/HOL/Tools/Meson/meson_tactic.ML Fri Oct 25 17:01:23 2024 +0200
@@ -17,7 +17,7 @@
let val ctxt' = put_claset HOL_cs ctxt
in
Meson.meson_tac ctxt' (maps (snd o Meson_Clausify.cnf_axiom Meson.simp_options_all_true ctxt'
- false true 0) ths)
+ {new_skolem = false, combs = true, refl = true} 0) ths)
end
(* This is part of a workaround to avoid freezing schematic variables in \<^text>\<open>using\<close> facts. See
--- a/src/HOL/Tools/Metis/metis_generate.ML Fri Oct 25 16:57:17 2024 +0200
+++ b/src/HOL/Tools/Metis/metis_generate.ML Fri Oct 25 17:01:23 2024 +0200
@@ -29,6 +29,8 @@
val metis_name_table : ((string * int) * ((type_enc -> string) * bool)) list
val reveal_old_skolem_terms : (string * term) list -> term -> term
val reveal_lam_lifted : (string * term) list -> term -> term
+ val eliminate_lam_wrappers : term -> term
+ val have_common_thm : Proof.context -> thm list -> thm list -> bool
val generate_metis_problem : Proof.context -> type_enc -> string -> thm list -> thm list ->
int Symtab.table * (Metis_Thm.thm * isa_thm) list * (unit -> (string * int) list)
* ((string * term) list * (string * term) list)
@@ -194,6 +196,11 @@
| eliminate_lam_wrappers (Abs (s, T, t)) = Abs (s, T, eliminate_lam_wrappers t)
| eliminate_lam_wrappers t = t
+(* Designed to work also with monomorphic instances of polymorphic theorems. *)
+fun have_common_thm ctxt ths1 ths2 =
+ exists (member (Term.aconv_untyped o apply2 Thm.prop_of) ths1)
+ (map (Meson.make_meta_clause ctxt) ths2)
+
(* Function to generate metis clauses, including comb and type clauses *)
fun generate_metis_problem ctxt type_enc lam_trans conj_clauses fact_clauses =
let
@@ -225,6 +232,12 @@
val (atp_problem, _, lifted, sym_tab) =
generate_atp_problem ctxt true CNF Hypothesis type_enc Metis lam_trans false false false []
\<^prop>\<open>False\<close> props
+
+ val _ = trace_msg ctxt (fn () => cat_lines ("OLD SKOLEM TERMS" ::
+ (old_skolems |> map (fn (s, t) => s ^ ": " ^ Syntax.string_of_term ctxt t))))
+ val _ = trace_msg ctxt (fn () => cat_lines ("LIFTED LAMBDAS" ::
+ (lifted |> map (fn (s, t) => s ^ ": " ^ Syntax.string_of_term ctxt t))))
+
(*
val _ = tracing ("ATP PROBLEM: " ^
cat_lines (lines_of_atp_problem CNF atp_problem))
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Metis/metis_instantiations.ML Fri Oct 25 17:01:23 2024 +0200
@@ -0,0 +1,416 @@
+(* Title: HOL/Tools/Metis/metis_instantiations.ML
+ Author: Lukas Bartl, LMU Muenchen
+
+Inference of Variable Instantiations for Metis.
+*)
+
+signature METIS_INSTANTIATIONS =
+sig
+ type inst
+
+ type infer_params = {
+ ctxt : Proof.context,
+ type_enc : string,
+ lam_trans : string,
+ th_name : thm -> string option,
+ new_skolem : bool,
+ th_cls_pairs : (thm * thm list) list,
+ lifted : (string * term) list,
+ sym_tab : int Symtab.table,
+ axioms : (Metis_Thm.thm * thm) list,
+ mth : Metis_Thm.thm
+ }
+
+ val suggest_of : bool Config.T
+ val suggest_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
+end;
+
+structure Metis_Instantiations : METIS_INSTANTIATIONS =
+struct
+
+open ATP_Problem_Generate
+open ATP_Proof_Reconstruct
+open Metis_Generate
+open Metis_Reconstruct
+
+(* Type of variable instantiations of a theorem. This is a list of (certified)
+ * terms suitably ordered for an of-instantiation of the theorem. *)
+type inst = cterm list
+
+(* Params needed for inference of variable instantiations *)
+type infer_params = {
+ ctxt : Proof.context,
+ type_enc : string,
+ lam_trans : string,
+ th_name : thm -> string option,
+ new_skolem : bool,
+ th_cls_pairs : (thm * thm list) list,
+ lifted : (string * term) list,
+ sym_tab : int Symtab.table,
+ axioms : (Metis_Thm.thm * thm) list,
+ mth : Metis_Thm.thm
+}
+
+(* 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)
+(* Config option to allow instantiation of variables with "undefined" *)
+val suggest_undefined = Attrib.setup_config_bool @{binding "metis_suggest_undefined"} (K true)
+
+fun metis_call type_enc lam_trans =
+ let
+ val type_enc =
+ case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases type_enc of
+ [alias] => alias
+ | _ => type_enc
+ val opts =
+ [] |> lam_trans <> default_metis_lam_trans ? cons lam_trans
+ |> type_enc <> partial_typesN ? cons type_enc
+ in
+ metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")")
+ end
+
+(* Variables of a theorem ordered the same way as in of-instantiations
+ * (cf. Rule_Insts.of_rule) *)
+fun of_vars_of_thm th = Vars.build (Vars.add_vars (Thm.full_prop_of th)) |> Vars.list_set
+
+(* "_" terms are used for variables without instantiation *)
+val is_dummy_cterm = Term.is_dummy_pattern o Thm.term_of
+val thm_insts_trivial = forall (forall is_dummy_cterm o snd)
+
+fun table_of_thm_inst (th, cts) =
+ of_vars_of_thm th ~~ cts
+ |> filter_out (is_dummy_cterm o snd)
+ |> Vars.make
+
+fun open_attrib name =
+ case try (unsuffix "]") name of
+ NONE => name ^ "["
+ | SOME name' => name' ^ ", "
+
+fun pretty_inst_cterm ctxt ct =
+ let
+ val pretty = Syntax.pretty_term ctxt (Thm.term_of ct)
+ val is_dummy = ATP_Util.content_of_pretty pretty = "_"
+ in
+ (* Do not quote single "_" *)
+ pretty |> not is_dummy ? ATP_Util.pretty_maybe_quote ctxt
+ end
+
+(* Pretty of-instantiation *)
+fun pretty_name_inst ctxt (name, inst) =
+ case drop_suffix is_dummy_cterm inst of
+ [] => Pretty.str name
+ | cts =>
+ map (pretty_inst_cterm ctxt) cts
+ |> Pretty.breaks o cons (Pretty.str "of")
+ |> Pretty.enclose (open_attrib name) "]"
+
+val string_of_name_inst = Pretty.string_of oo pretty_name_inst
+
+(* Infer Metis axioms with corresponding subtitutions *)
+fun infer_metis_axiom_substs mth =
+ let
+ fun add_metis_axiom_substs msubst mth =
+ case Metis_Thm.inference mth of
+ (Metis_Thm.Axiom, []) => cons (msubst, mth)
+ | (Metis_Thm.Metis_Subst, _) =>
+ (case Metis_Proof.thmToInference mth of
+ Metis_Proof.Metis_Subst (msubst', par) =>
+ add_metis_axiom_substs (Metis_Subst.compose msubst' msubst) par
+ | _ => raise Fail "expected Metis_Subst")
+ | (_, pars) => fold (add_metis_axiom_substs msubst) pars
+ in
+ add_metis_axiom_substs Metis_Subst.empty mth []
+ end
+
+(* Variables are renamed during clausification by importing and exporting
+ * theorems. Do the same here to find the right variable. *)
+fun import_export_thm ctxt th =
+ let
+ (* cf. Meson_Clausify.nnf_axiom *)
+ val (import_th, import_ctxt) =
+ Drule.zero_var_indexes th
+ |> (fn th' => Variable.import true [th'] ctxt)
+ |>> the_single o snd
+ (* cf. Meson_Clausify.cnf_axiom *)
+ val export_th = import_th
+ |> singleton (Variable.export import_ctxt ctxt)
+ in
+ (* cf. Meson.finish_cnf *)
+ Drule.zero_var_indexes export_th
+ end
+
+(* Find the theorem corresponding to a Metis axiom if it has a name.
+ * "Theorems" are Isabelle theorems given to the metis tactic.
+ * "Axioms" are clauses given to the Metis prover. *)
+fun metis_axiom_to_thm {ctxt, th_name, th_cls_pairs, axioms, ...} (msubst, maxiom) =
+ let
+ val axiom = lookth axioms maxiom
+ in
+ List.find (have_common_thm ctxt [axiom] o snd) th_cls_pairs
+ |> Option.mapPartial (fn (th, _) => th_name th |> Option.map (pair th))
+ |> Option.map (pair (msubst, maxiom, axiom))
+ end
+
+(* Build a table : term Vartab.table list Thmtab.table that maps a theorem to a
+ * list of variable substitutions (theorems can be instantiated multiple times)
+ * from Metis substitutions *)
+fun metis_substs_to_table {ctxt, type_enc, lifted, new_skolem, sym_tab, ...} th_of_vars th_msubsts =
+ let
+ val _ = trace_msg ctxt (K "AXIOM SUBSTITUTIONS")
+ val type_enc = type_enc_of_string Strict type_enc
+ val thy = Proof_Context.theory_of ctxt
+
+ (* Replace Skolem terms with "_" because they are unknown to the user
+ * (cf. Metis_Generate.reveal_old_skolem_terms) *)
+ val dummy_old_skolem_terms = map_aterms
+ (fn t as Const (s, T) =>
+ if String.isPrefix old_skolem_const_prefix s
+ then Term.dummy_pattern T
+ else t
+ | t => t)
+
+ (* Infer types and replace "_" terms/types with schematic variables *)
+ val infer_types_pattern =
+ singleton (Type_Infer_Context.infer_types_finished
+ (Proof_Context.set_mode Proof_Context.mode_pattern ctxt))
+
+ (* "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
+ Const o (pair @{const_name "undefined"})
+ else
+ Term.dummy_pattern
+
+ (* Instantiate schematic and free variables *)
+ val inst_vars_frees = map_aterms
+ (fn t as Free (x, T) =>
+ (* an unfixed/internal free variable is unknown/inaccessible to the user,
+ * so we replace it with "_" *)
+ if not (Variable.is_fixed ctxt x) orelse Name.is_internal (Variable.revert_fixed ctxt x)
+ then Term.dummy_pattern T
+ else t
+ | Var (_, T) =>
+ (* a schematic variable can be replaced with any term,
+ * so we replace it with "undefined" *)
+ undefined_pattern T
+ | t => t)
+
+ (* Remove arguments of "_" unknown functions because the functions could
+ * change (e.g. instantiations can change Skolem functions).
+ * Type inference also introduces arguments (cf. Term.replace_dummy_patterns). *)
+ fun eliminate_dummy_args (t $ u) =
+ let
+ val t' = eliminate_dummy_args t
+ in
+ if Term.is_dummy_pattern t' then
+ Term.dummy_pattern (Term.fastype_of t' |> Term.range_type)
+ else
+ t' $ eliminate_dummy_args u
+ end
+ | eliminate_dummy_args (Abs (s, T, t)) = Abs (s, T, eliminate_dummy_args t)
+ | eliminate_dummy_args t = t
+
+ (* Polish Isabelle term, s.t. it can be displayed
+ * (cf. Metis_Reconstruct.polish_hol_terms and ATP_Proof_Reconstruct.termify_line) *)
+ val polish_term =
+ reveal_lam_lifted lifted (* reveal lifted lambdas *)
+ #> dummy_old_skolem_terms (* eliminate Skolem terms *)
+ #> infer_types_pattern (* type inference *)
+ #> eliminate_lam_wrappers (* eliminate Metis.lambda wrappers *)
+ #> uncombine_term thy (* eliminate Meson.COMB* terms *)
+ #> Envir.beta_eta_contract (* simplify lambda terms *)
+ #> simplify_bool (* simplify boolean terms *)
+ #> Term.show_dummy_patterns (* reveal "_" that have been replaced by type inference *)
+ #> inst_vars_frees (* eliminate schematic and free variables *)
+ #> eliminate_dummy_args (* eliminate arguments of "_" (unknown functions) *)
+
+ (* Translate a Metis substitution to Isabelle *)
+ fun add_subst_to_table ((msubst, maxiom, axiom), (th, name)) th_substs_table =
+ let
+ val _ = trace_msg ctxt (fn () => "Metis axiom: " ^ Metis_Thm.toString maxiom)
+ val _ = trace_msg ctxt (fn () => "Metis substitution: " ^ Metis_Subst.toString msubst)
+ val _ = trace_msg ctxt (fn () => "Isabelle axiom: " ^ Thm.string_of_thm ctxt axiom)
+ val _ = trace_msg ctxt (fn () => "Isabelle theorem: " ^
+ Thm.string_of_thm ctxt th ^ " (" ^ name ^ ")")
+
+ (* Only indexnames of variables without types
+ * because types can change during clausification *)
+ val vars =
+ inter (op =) (map fst (of_vars_of_thm axiom))
+ (map fst (Thmtab.lookup th_of_vars th |> the))
+
+ (* Translate Metis variable and term to Isabelle *)
+ fun translate_var_term (mvar, mt) =
+ Metis_Name.toString mvar
+ (* cf. remove_typeinst in Metis_Reconstruct.inst_inference *)
+ |> unprefix_and_unascii schematic_var_prefix
+ (* cf. find_var in Metis_Reconstruct.inst_inference *)
+ |> Option.mapPartial (fn name => List.find (fn (a, _) => a = name) vars)
+ (* cf. subst_translation in Metis_Reconstruct.inst_inference *)
+ |> Option.map (fn var => (var, hol_term_of_metis ctxt type_enc sym_tab mt))
+
+ (* Build the substitution table and instantiate the remaining schematic variables *)
+ fun build_subst_table substs =
+ let
+ (* Variable of the axiom that didn't get instantiated by Metis,
+ * the type is later set via type unification *)
+ val undefined_term = undefined_pattern (TVar ((Name.aT, 0), []))
+ in
+ Vartab.build (vars |> fold (fn var => Vartab.default
+ (var, AList.lookup (op =) substs var |> the_default undefined_term)))
+ end
+
+ val raw_substs =
+ Metis_Subst.toList msubst
+ |> map_filter translate_var_term
+ val _ = if null raw_substs then () else
+ trace_msg ctxt (fn () => cat_lines ("Raw Isabelle substitution:" ::
+ (raw_substs |> map (fn (var, t) =>
+ Term.string_of_vname var ^ " |-> " ^
+ Syntax.string_of_term ctxt t))))
+
+ val subst = raw_substs
+ |> map (apsnd polish_term)
+ |> build_subst_table
+ val _ = trace_msg ctxt (fn () =>
+ if Vartab.is_empty subst then
+ "No Isabelle substitution"
+ else
+ cat_lines ("Final Isabelle substitution:" ::
+ (Vartab.dest subst |> map (fn (var ,t) =>
+ Term.string_of_vname var ^ " |-> " ^
+ Syntax.string_of_term ctxt t))))
+
+ (* Try to merge the substitution with another substitution of the theorem *)
+ fun insert_subst [] = [subst]
+ | insert_subst (subst' :: substs') =
+ Vartab.merge Term.aconv_untyped (subst', subst) :: substs'
+ handle Vartab.DUP _ => subst' :: insert_subst substs'
+ in
+ Thmtab.lookup th_substs_table th
+ |> insert_subst o these
+ |> (fn substs => Thmtab.update (th, substs) th_substs_table)
+ end
+ in
+ fold add_subst_to_table th_msubsts Thmtab.empty
+ end
+
+(* Build variable instantiations : thm * inst list from the table *)
+fun table_to_thm_insts ctxt th_of_vars th_substs_table =
+ let
+ val thy = Proof_Context.theory_of ctxt
+
+ (* Unify types of a variable with the term for instantiation
+ * (cf. Drule.infer_instantiate_types, Metis_Reconstruct.cterm_incr_types) *)
+ fun unify (tyenv, maxidx) T t =
+ let
+ val t' = Term.map_types (Logic.incr_tvar (maxidx + 1)) t
+ val U = Term.fastype_of t'
+ val maxidx' = Term.maxidx_term t' maxidx
+ in
+ (t', Sign.typ_unify thy (T, U) (tyenv, maxidx'))
+ end
+
+ (* Instantiate type variables with a type unifier or a dummy type
+ * (cf. Drule.infer_instantiate_types) *)
+ fun inst_unifier (ts, tyenv) =
+ let
+ val instT =
+ TVars.build (tyenv |> Vartab.fold (fn (xi, (S, T)) =>
+ TVars.add ((xi, S), Envir.norm_type tyenv T)))
+ val dummy_tvars = Term.map_types (map_type_tvar (K Term.dummyT))
+ in
+ map (dummy_tvars o Term_Subst.instantiate (instT, Vars.empty)) ts
+ end
+
+ (* Build variable instantiations from a substitution table and instantiate
+ * the remaining schematic variables with "_" *)
+ fun add_subst th subst =
+ let
+ val of_vars = Thmtab.lookup th_of_vars th |> the
+
+ fun unify_or_dummy (var, T) unify_params =
+ Vartab.lookup subst var
+ |> Option.map (unify unify_params T)
+ |> the_default (Term.dummy_pattern T, unify_params)
+ in
+ fold_map unify_or_dummy of_vars (Vartab.empty, Thm.maxidx_of th)
+ |> inst_unifier o apsnd fst
+ |> map (Thm.cterm_of ctxt)
+ |> cons o pair th
+ end
+ in
+ Thmtab.fold_rev (fn (th, substs) => fold (add_subst th) substs) th_substs_table []
+ end
+
+fun really_infer_thm_insts (infer_params as {ctxt, th_name, th_cls_pairs, mth, ...}) =
+ let
+ (* Compute the theorem variables ordered as in of-instantiations.
+ * import_export_thm is used to get the same variables as in axioms. *)
+ val th_of_vars =
+ Thmtab.build (th_cls_pairs |> fold (fn (th, _) => Thmtab.default
+ (th, of_vars_of_thm (import_export_thm ctxt th))))
+
+ val th_insts =
+ infer_metis_axiom_substs mth
+ |> map_filter (metis_axiom_to_thm infer_params)
+ |> metis_substs_to_table infer_params th_of_vars
+ |> table_to_thm_insts ctxt th_of_vars
+
+ val _ = trace_msg ctxt (fn () => cat_lines ("THEOREM INSTANTIATIONS" ::
+ (if thm_insts_trivial th_insts then
+ ["No instantiation available"]
+ else
+ th_insts |> maps (fn th_inst as (th, _) =>
+ let
+ val table = table_of_thm_inst th_inst
+ in
+ if Vars.is_empty table then
+ []
+ else
+ "Theorem " ^ Thm.string_of_thm ctxt th ^ " (" ^ the (th_name th) ^ "):" ::
+ (Vars.dest table |> map (fn (var, ct) =>
+ Syntax.string_of_term ctxt (Var var) ^ " |-> " ^
+ Syntax.string_of_term ctxt (Thm.term_of ct)))
+ end))))
+ in
+ th_insts
+ end
+
+(* Infer variable instantiations *)
+fun infer_thm_insts (infer_params as {ctxt, ...}) =
+ \<^try>\<open>SOME (really_infer_thm_insts infer_params)
+ catch exn => (trace_msg ctxt (fn () => Runtime.exn_message exn); NONE)\<close>
+
+(* Write suggested command with of-instantiations *)
+fun write_command {ctxt, type_enc, lam_trans, th_name, ...} st th_insts =
+ let
+ val _ = trace_msg ctxt (K "SUGGEST OF-INSTANTIATIONS")
+ val apply_str = if Thm.nprems_of st = 0 then "by" else "apply"
+ val command_str = th_insts
+ |> map (pretty_name_inst ctxt o apfst (the o th_name))
+ |> cons (Pretty.str (metis_call type_enc lam_trans))
+ |> Pretty.enclose (apply_str ^ " (") ")" o Pretty.breaks
+ |> Pretty.symbolic_string_of (* markup string *)
+ in
+ writeln ("Found variable instantiations, try this:" ^
+ (* Add optional markup break (command may need multiple lines) *)
+ Markup.markup (Markup.break {width = 1, indent = 2}) " " ^
+ Active.sendback_markup_command command_str)
+ end
+
+(* Infer variable instantiations and suggest of-instantiations *)
+fun suggest_of_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)
+
+end;
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Oct 25 16:57:17 2024 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Oct 25 17:01:23 2024 +0200
@@ -13,6 +13,8 @@
exception METIS_RECONSTRUCT of string * string
+ val hol_term_of_metis : Proof.context -> type_enc -> int Symtab.table ->
+ Metis_Term.term -> term
val hol_clause_of_metis : Proof.context -> type_enc -> int Symtab.table ->
(string * term) list * (string * term) list -> Metis_Thm.thm -> term
val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
@@ -78,6 +80,7 @@
(fn () => " final term: " ^ Syntax.string_of_term ctxt t ^
" of type " ^ Syntax.string_of_typ ctxt (type_of t))) ts'
in ts' end
+ handle ERROR msg => raise METIS_RECONSTRUCT ("hol_terms_of_metis", msg)
@@ -201,22 +204,24 @@
res (th1', th2)
handle TERM z =>
let
- val ps = []
+ val tyenv = []
|> fold (Term.add_vars o Thm.prop_of) [th1', th2]
|> AList.group (op =)
|> maps (fn ((s, _), T :: Ts) => map (fn T' => (Free (s, T), Free (s, T'))) Ts)
|> rpair Envir.init
|-> fold (Pattern.unify (Context.Proof ctxt))
- |> Envir.type_env |> Vartab.dest
- |> map (fn (x, (S, T)) => ((x, S), Thm.ctyp_of ctxt T))
+ |> Envir.type_env
+ val instT =
+ TVars.build (tyenv |> Vartab.fold (fn (x, (S, T)) =>
+ TVars.add ((x, S), Thm.ctyp_of ctxt (Envir.norm_type tyenv T))))
in
(*The unifier, which is invoked from "Thm.bicompose", will sometimes refuse to unify
"?a::?'a" with "?a::?'b" or "?a::nat" and throw a "TERM" exception (with "add_ffpair" as
first argument). We then perform unification of the types of variables by hand and try
again. We could do this the first time around but this error occurs seldom and we don't
want to break existing proofs in subtle ways or slow them down.*)
- if null ps then raise TERM z
- else res (apply2 (Drule.instantiate_normalize (TVars.make ps, Vars.empty)) (th1', th2))
+ if TVars.is_empty instT then raise TERM z
+ else res (apply2 (Drule.instantiate_normalize (instT, Vars.empty)) (th1', th2))
end
end
--- a/src/HOL/Tools/Metis/metis_tactic.ML Fri Oct 25 16:57:17 2024 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Fri Oct 25 17:01:23 2024 +0200
@@ -9,15 +9,21 @@
signature METIS_TACTIC =
sig
+ type inst
+
val trace : bool Config.T
val verbose : bool Config.T
+ val suggest_of : bool Config.T
+ val suggest_undefined : bool Config.T
val new_skolem : bool Config.T
val advisory_simp : bool Config.T
- val metis_tac_unused : string list -> string -> Proof.context -> thm list -> int -> thm ->
- thm list * thm Seq.seq
+ val pretty_name_inst : Proof.context -> string * inst -> Pretty.T
+ val string_of_name_inst : Proof.context -> string * inst -> string
val metis_tac : string list -> string -> Proof.context -> thm list -> int -> tactic
val metis_method : (string list option * string option) * thm list -> Proof.context -> thm list ->
tactic
+ val metis_infer_thm_insts : (string list option * string option) * thm list -> Proof.context ->
+ thm list -> int -> thm -> (thm * inst) list option
val metis_lam_transs : string list
val parse_metis_options : (string list option * string option) parser
end
@@ -29,15 +35,11 @@
open ATP_Proof_Reconstruct
open Metis_Generate
open Metis_Reconstruct
+open Metis_Instantiations
val new_skolem = Attrib.setup_config_bool \<^binding>\<open>metis_new_skolem\<close> (K false)
val advisory_simp = Attrib.setup_config_bool \<^binding>\<open>metis_advisory_simp\<close> (K true)
-(* Designed to work also with monomorphic instances of polymorphic theorems. *)
-fun have_common_thm ctxt ths1 ths2 =
- exists (member (Term.aconv_untyped o apply2 Thm.prop_of) ths1)
- (map (Meson.make_meta_clause ctxt) ths2)
-
(*Determining which axiom clauses are actually used*)
fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
| used_axioms _ _ = NONE
@@ -79,6 +81,10 @@
if Meson_Clausify.is_quasi_lambda_free (Thm.prop_of th) then th
else
let
+ (* increment indexes to prevent (type) variable clashes *)
+ fun resolve_lambdaI th =
+ Meson.first_order_resolve ctxt th
+ (Thm.incr_indexes (Thm.maxidx_of th + 1) @{thm Metis.eq_lambdaI})
fun conv first ctxt ct =
if Meson_Clausify.is_quasi_lambda_free (Thm.term_of ct) then Thm.reflexive ct
else
@@ -87,8 +93,8 @@
if first then
(case add_vars_and_frees u [] of
[] =>
- Conv.abs_conv (conv false o snd) ctxt ct
- |> (fn th => Meson.first_order_resolve ctxt th @{thm Metis.eq_lambdaI})
+ Conv.abs_conv (conv false o snd) ctxt ct
+ |> resolve_lambdaI
| v :: _ =>
Abs (Name.uu, fastype_of v, abstract_over (v, Thm.term_of ct)) $ v
|> Thm.cterm_of ctxt
@@ -130,21 +136,10 @@
| ord => ord)
in {weight = weight, precedence = precedence} end
-fun metis_call type_enc lam_trans =
- let
- val type_enc =
- (case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases type_enc of
- [alias] => alias
- | _ => type_enc)
- val opts =
- [] |> type_enc <> partial_typesN ? cons type_enc
- |> lam_trans <> default_metis_lam_trans ? cons lam_trans
- in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end
-
exception METIS_UNPROVABLE of unit
(* Main function to start Metis proof and reconstruction *)
-fun FOL_SOLVE unused type_encs lam_trans ctxt cls ths0 =
+fun FOL_SOLVE infer_params th_name type_encs lam_trans clausify_refl ctxt cls0 ths0 =
let
val thy = Proof_Context.theory_of ctxt
@@ -152,22 +147,22 @@
val do_lams = lam_trans = liftingN ? introduce_lam_wrappers ctxt
val th_cls_pairs =
map_index (fn (j, th) =>
- (Thm.get_name_hint th,
+ (th,
th
|> Drule.eta_contraction_rule
- |> Meson_Clausify.cnf_axiom Meson.simp_options_all_true ctxt new_skolem
- (lam_trans = combsN) j
+ |> Meson_Clausify.cnf_axiom Meson.simp_options_all_true ctxt
+ {new_skolem = new_skolem, combs = (lam_trans = combsN), refl = clausify_refl} j
||> map do_lams))
ths0
val ths = maps (snd o snd) th_cls_pairs
val dischargers = map (fst o snd) th_cls_pairs
- val cls = cls |> map (Drule.eta_contraction_rule #> do_lams)
+ val cls = cls0 |> map (Drule.eta_contraction_rule #> do_lams)
val _ = trace_msg ctxt (K "FOL_SOLVE: CONJECTURE CLAUSES")
val _ = List.app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) cls
- val type_enc :: fallback_type_encs = type_encs
- val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
- val type_enc = type_enc_of_string Strict type_enc
+ val type_enc_str :: fallback_type_encs = type_encs
+ val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc_str)
+ val type_enc = type_enc_of_string Strict type_enc_str
val (sym_tab, axioms, ord_info, concealed) =
generate_metis_problem ctxt type_enc lam_trans cls ths
@@ -192,7 +187,7 @@
fun fall_back () =
(verbose_warning ctxt
("Falling back on " ^ quote (metis_call (hd fallback_type_encs) lam_trans) ^ "...");
- FOL_SOLVE unused fallback_type_encs lam_trans ctxt cls ths0)
+ FOL_SOLVE infer_params th_name fallback_type_encs lam_trans clausify_refl ctxt cls0 ths0)
in
(case filter (fn t => Thm.prop_of t aconv \<^prop>\<open>False\<close>) cls of
false_th :: _ => [false_th RS @{thm FalseE}]
@@ -210,12 +205,31 @@
val _ = trace_msg ctxt (K "METIS COMPLETED; clauses actually used:")
val _ = List.app (fn th => trace_msg ctxt (fn () => Thm.string_of_thm ctxt th)) used
- val unused_th_cls_pairs = filter_out (have_common_thm ctxt used o #2 o #2) th_cls_pairs
- val _ = unused := maps (#2 o #2) unused_th_cls_pairs;
+ val (used_ths, unused_ths) =
+ List.partition (have_common_thm ctxt used o #2 o #2) th_cls_pairs
+ |> apply2 (map #1)
val _ =
- if not (null unused_th_cls_pairs) then
+ if exists is_some (map th_name used_ths) then
+ infer_params := SOME ({
+ ctxt = ctxt',
+ type_enc = type_enc_str,
+ lam_trans = lam_trans,
+ th_name = th_name,
+ new_skolem = new_skolem,
+ th_cls_pairs = map (apsnd snd) th_cls_pairs,
+ lifted = fst concealed,
+ sym_tab = sym_tab,
+ axioms = axioms,
+ mth = mth
+ })
+ else ();
+ val _ =
+ if not (null unused_ths) then
verbose_warning ctxt ("Unused theorems: " ^
- commas_quote (map (Proof_Context.print_thm_name ctxt o #1) unused_th_cls_pairs))
+ commas_quote (unused_ths |> map (fn th =>
+ th_name th
+ |> the_default (Proof_Context.print_thm_name ctxt
+ (Thm.get_name_hint th)))))
else ();
val _ =
if not (null cls) andalso not (have_common_thm ctxt used cls) then
@@ -242,7 +256,7 @@
single
#> Meson.make_clauses_unsorted ctxt
#> combinators ? map (Meson_Clausify.introduce_combinators_in_theorem ctxt)
- #> Meson.finish_cnf
+ #> Meson.finish_cnf true
fun preskolem_tac ctxt st0 =
(if exists (Meson.has_too_many_clauses ctxt)
@@ -252,21 +266,62 @@
else
all_tac) st0
-fun metis_tac_unused type_encs0 lam_trans ctxt ths i st0 =
+fun metis_tac_infer_params th_name type_encs0 lam_trans clausify_refl ctxt ths i =
let
- val unused = Unsynchronized.ref []
+ val infer_params = Unsynchronized.ref NONE
val type_encs = if null type_encs0 then partial_type_encs else type_encs0
val _ = trace_msg ctxt (fn () =>
"Metis called with theorems\n" ^ cat_lines (map (Thm.string_of_thm ctxt) ths))
val type_encs = type_encs |> maps unalias_type_enc
val combs = (lam_trans = combsN)
- fun tac clause = resolve_tac ctxt (FOL_SOLVE unused type_encs lam_trans ctxt clause ths) 1
- val seq = Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt combs)) tac ctxt i st0
+ fun tac clause = resolve_tac ctxt
+ (FOL_SOLVE infer_params th_name type_encs lam_trans clausify_refl ctxt clause ths) 1
in
- (!unused, seq)
+ Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt combs)) tac ctxt i
+ #> Seq.map (fn st => (!infer_params, st))
end
-fun metis_tac type_encs lam_trans ctxt ths i = snd o metis_tac_unused type_encs lam_trans ctxt ths i
+(* Theorem name functions *)
+(* No theorem name (infer_thm_insts won't be called) *)
+val no_th_name = K NONE
+(* Name hint as theorem name (theorems in ths get a name but perhaps "??.unknown") *)
+fun th_name_hint ths =
+ Option.filter (member Thm.eq_thm ths)
+ #> Option.map (Thm_Name.print o Thm.get_name_hint)
+(* Use multi_thm with input string to get theorem name (only if part of multi_ths) *)
+fun th_name_multi_thm multi_ths th =
+ let
+ fun index_of_th ths = find_index (curry Thm.eq_thm th) ths + 1
+ fun make_name ([_], name) = name
+ (* This doesn't work if name already has attributes or is indexed,
+ * but provides much more information than "??.unknown" name hint *)
+ | make_name (ths, name) = name ^ "(" ^ string_of_int (index_of_th ths) ^ ")"
+ in
+ List.find (fn (ths, _) => member Thm.eq_thm ths th) multi_ths
+ |> Option.map make_name
+ end
+
+(* 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
+ (fn (NONE, st) => st
+ | (SOME infer_params, st) => tap (suggest_of_call infer_params) st)
+ else
+ snd
+ in
+ (* "clausify_refl" (removal of redundant equalities) renames variables,
+ * 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
+ end
+
+(* Metis tactic without theorem name, therefore won't suggest of-instantiations *)
+val metis_tac = metis_tac' no_th_name
(* Whenever "X" has schematic type variables, we treat "using X by metis" as "by (metis X)" to
prevent "Subgoal.FOCUS" from freezing the type variables. We don't do it for nonschematic facts
@@ -274,13 +329,37 @@
extensionality not being applied) and brings few benefits. *)
val has_tvar = exists_type (exists_subtype (fn TVar _ => true | _ => false)) o Thm.prop_of
-fun metis_method ((override_type_encs, lam_trans), ths) ctxt facts =
- let val (schem_facts, nonschem_facts) = List.partition has_tvar facts in
+(* Metis method to prove the goal and optionally suggest of-instantiations *)
+fun metis_method' th_name ((override_type_encs, lam_trans), ths) ctxt facts =
+ let
+ val (schem_facts, nonschem_facts) = List.partition has_tvar facts
+ in
HEADGOAL (Method.insert_tac ctxt nonschem_facts THEN'
- CHANGED_PROP o metis_tac (these override_type_encs)
+ CHANGED_PROP o metis_tac' th_name (these override_type_encs)
(the_default default_metis_lam_trans lam_trans) ctxt (schem_facts @ ths))
end
+(* Metis method without theorem name, therefore won't suggest of-instantiations *)
+val metis_method = metis_method' no_th_name
+
+(* Metis method with input strings for better theorem names in of-instantiations *)
+fun metis_method_multi_thms (opts, multi_ths) =
+ metis_method' (th_name_multi_thm multi_ths) (opts, maps fst multi_ths)
+
+(* Use Metis to infer variable instantiations of theorems *)
+fun metis_infer_thm_insts ((override_type_encs, lam_trans), ths) ctxt facts i =
+ let
+ val (schem_facts, nonschem_facts) = List.partition has_tvar facts
+ val insert_tac = Method.insert_tac ctxt nonschem_facts i
+ val metis_tac =
+ metis_tac_infer_params (th_name_hint ths) (these override_type_encs)
+ (the_default default_metis_lam_trans lam_trans) false ctxt (schem_facts @ ths) i
+ in
+ Seq.THEN (insert_tac, metis_tac)
+ #> Seq.map (Option.mapPartial infer_thm_insts o fst)
+ #> Option.mapPartial fst o Seq.pull
+ end
+
val metis_lam_transs = [opaque_liftingN, liftingN, combsN]
fun set_opt _ x NONE = SOME x
@@ -303,10 +382,22 @@
|> (case s' of SOME s' => consider_opt s' | _ => I)))
(NONE, NONE)
+(* Parse multi_thm with input string *)
+val parse_multi_thm =
+ let
+ (* Remove spaces before and after "[]():," *)
+ val strip_spaces =
+ ATP_Util.strip_spaces false (not o member (op =) (String.explode "[]():,"))
+ in
+ ATP_Util.scan_and_trace_multi_thm
+ >> apsnd (map Token.unparse #> implode_space #> strip_spaces)
+ end
+
val _ =
Theory.setup
(Method.setup \<^binding>\<open>metis\<close>
- (Scan.lift parse_metis_options -- Attrib.thms >> (METHOD oo metis_method))
+ (Scan.lift parse_metis_options -- Scan.repeat parse_multi_thm
+ >> (METHOD oo metis_method_multi_thms))
"Metis for FOL and HOL problems")
end;
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Fri Oct 25 16:57:17 2024 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Fri Oct 25 17:01:23 2024 +0200
@@ -196,8 +196,8 @@
preplay_results
|> map
(fn (meth, (play_outcome, used_facts)) =>
- "Preplay: " ^
- Sledgehammer_Proof_Methods.string_of_proof_method (map fst used_facts) meth ^
+ "Preplay: " ^ Sledgehammer_Proof_Methods.string_of_proof_method
+ (map (ATP_Util.content_of_pretty o fst) used_facts) meth ^
" (" ^ Sledgehammer_Proof_Methods.string_of_play_outcome play_outcome ^ ")")
|> cat_lines
else
@@ -211,7 +211,7 @@
(case time_prover of NONE => "" | SOME ms => ", ATP " ^ string_of_int ms ^ "ms") ^
") [" ^ prover_name ^ "]: "
in
- (sledgehamer_outcome, triv_str ^ outcome_msg ^ msg ^
+ (sledgehamer_outcome, triv_str ^ outcome_msg ^ Protocol_Message.clean_output msg ^
(if exhaustive_preplay_msg = "" then "" else ("\n" ^ exhaustive_preplay_msg)),
change_data #> inc_sh_time_isa cpu_time)
end
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Oct 25 16:57:17 2024 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Oct 25 17:01:23 2024 +0200
@@ -277,12 +277,7 @@
val indent_size = 2
-fun pretty_maybe_quote ctxt pretty =
- let val s = Pretty.unformatted_string_of pretty in
- if ATP_Util.maybe_quote ctxt s = s then pretty
- else if Config.get ctxt ATP_Util.proof_cartouches then Pretty.cartouche pretty
- else Pretty.quote pretty
- end
+val pretty_maybe_quote = ATP_Util.pretty_maybe_quote
val hashw = ATP_Util.hashw
val hashw_string = ATP_Util.hashw_string
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 25 16:57:17 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 25 17:01:23 2024 +0200
@@ -19,7 +19,7 @@
type prover_problem = Sledgehammer_Prover.prover_problem
type prover_result = Sledgehammer_Prover.prover_result
- type preplay_result = proof_method * (play_outcome * (string * stature) list)
+ type preplay_result = proof_method * (play_outcome * (Pretty.T * stature) list)
datatype sledgehammer_outcome =
SH_Some of prover_result * preplay_result list
@@ -44,6 +44,7 @@
open Sledgehammer_Util
open Sledgehammer_Fact
open Sledgehammer_Proof_Methods
+open Sledgehammer_Instantiations
open Sledgehammer_Isar_Proof
open Sledgehammer_Isar_Preplay
open Sledgehammer_Isar_Minimize
@@ -53,7 +54,7 @@
open Sledgehammer_Prover_Minimize
open Sledgehammer_MaSh
-type preplay_result = proof_method * (play_outcome * (string * stature) list)
+type preplay_result = proof_method * (play_outcome * (Pretty.T * stature) list)
datatype sledgehammer_outcome =
SH_Some of prover_result * preplay_result list
@@ -101,8 +102,8 @@
else
let
val ctxt = Proof.context_of state
- val used_facts = filter_out (fn (_, (sc, _)) => sc = Chained) used_facts
- val fact_names = map fst used_facts
+ val name_of_fact = content_of_pretty o fst
+ val fact_names = map name_of_fact used_facts
val {facts = chained, ...} = Proof.goal state
val goal_t = Logic.get_goal (Thm.prop_of goal) i
@@ -128,20 +129,19 @@
val (time', used_names') =
minimized_isar_step ctxt chained time (mk_step [meth])
||> (facts_of_isar_step #> snd)
- val used_facts' = filter (member (op =) used_names' o fst) used_facts
+ val used_facts' =
+ filter (member (op =) used_names' o name_of_fact) used_facts
in
- (meth, Played time', used_facts')
+ (meth, (Played time', used_facts'))
end
- | _ => (meth, play_outcome, used_facts)))
- val any_succeeded = exists (fn (_, Played _, _) => true | _ => false) ress'
+ | _ => (meth, (play_outcome, used_facts))))
+ val any_succeeded = exists (fn (_, (Played _, _)) => true | _ => false) ress'
in
try_methss (ress' @ ress) (if any_succeeded then [] else methss)
end
in
try_methss [] methss
end)
- |> map (fn (meth, play_outcome, used_facts) =>
- (meth, (play_outcome, filter_out (fn (_, (sc, _)) => sc = Chained) used_facts)))
|> sort (play_outcome_ord o apply2 (fn (_, (play_outcome, _)) => play_outcome))
fun select_one_line_proof used_facts preferred_meth preplay_results =
@@ -155,7 +155,6 @@
(case AList.lookup (op =) preplay_results preferred_meth of
SOME (outcome, _) => outcome
| NONE => Play_Timed_Out Time.zeroTime))))
- |> apfst (filter_out (fn (_, (sc, _)) => sc = Chained))
fun launch_prover (params as {verbose, spy, slices, timeout, ...}) mode learn
(problem as {state, subgoal, factss, ...} : prover_problem)
@@ -222,27 +221,54 @@
|> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res)))
end
-fun preplay_prover_result ({minimize, preplay_timeout, ...} : params) state goal subgoal
+fun preplay_prover_result ({verbose, suggest_of, minimize, preplay_timeout, ...} : params)
+ state goal subgoal
(result as {outcome, used_facts, preferred_methss, message, ...} : prover_result) =
let
- val (output, chosen_preplay_outcome) =
+ val used_facts0 = filter_out (fn (_, (sc, _)) => sc = Chained) used_facts
+ val pretty_used_facts0 = map (apfst Pretty.str) used_facts0
+ val (output, pretty_used_facts, preplay_results) =
if outcome = SOME ATP_Proof.TimedOut then
- (SH_TimeOut, select_one_line_proof used_facts (fst preferred_methss) [])
+ (SH_TimeOut, pretty_used_facts0, [])
else if outcome = SOME ATP_Proof.OutOfResources then
- (SH_ResourcesOut, select_one_line_proof used_facts (fst preferred_methss) [])
+ (SH_ResourcesOut, pretty_used_facts0, [])
else if is_some outcome then
- (SH_None, select_one_line_proof used_facts (fst preferred_methss) [])
+ (SH_None, pretty_used_facts0, [])
else
let
- val preplay_results =
- play_one_line_proofs minimize preplay_timeout used_facts state goal subgoal
- (snd preferred_methss)
- val chosen_preplay_outcome =
- select_one_line_proof used_facts (fst preferred_methss) preplay_results
+ 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
+ val instantiate_timeout = Time.scale 5.0 preplay_timeout
+ val suggest_of = if null used_facts0 then SOME false else suggest_of
+ val (preplay_results, pretty_used_facts) =
+ (case suggest_of of
+ SOME false => preplay pretty_used_facts0
+ | SOME true =>
+ (* Always try to infer variable instantiations *)
+ instantiate_facts state verbose instantiate_timeout goal subgoal used_facts0
+ |> the_default pretty_used_facts0
+ |> preplay
+ | NONE =>
+ let
+ val preplay_results0 = preplay pretty_used_facts0
+ in
+ if preplay_succeeded preplay_results0 then
+ preplay_results0
+ else
+ (* Preplay failed, now try to infer variable instantiations *)
+ instantiate_facts state verbose instantiate_timeout goal subgoal used_facts0
+ |> Option.map preplay
+ |> the_default preplay_results0
+ end)
in
- (SH_Some (result, preplay_results), chosen_preplay_outcome)
+ (SH_Some (result, preplay_results), pretty_used_facts, preplay_results)
end
- fun output_message () = message (fn () => chosen_preplay_outcome)
+ fun chosen_preplay_outcome () =
+ select_one_line_proof pretty_used_facts (fst preferred_methss) preplay_results
+ fun output_message () = message chosen_preplay_outcome
in
(output, output_message)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Oct 25 16:57:17 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Oct 25 17:01:23 2024 +0200
@@ -71,6 +71,7 @@
("compress", "smart"),
("try0", "true"),
("smt_proofs", "true"),
+ ("suggest_of", "smart"),
("minimize", "true"),
("slices", string_of_int (12 * Multithreading.max_threads ())),
("preplay_timeout", "1")]
@@ -94,7 +95,8 @@
("no_isar_proofs", "isar_proofs"),
("dont_minimize", "minimize"),
("dont_try0", "try0"),
- ("no_smt_proofs", "smt_proofs")]
+ ("no_smt_proofs", "smt_proofs"),
+ ("dont_suggest_of", "suggest_of")]
val property_dependent_params = ["provers", "timeout"]
@@ -264,6 +266,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 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"
@@ -277,8 +280,8 @@
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,
- minimize = minimize, slices = slices, timeout = timeout, preplay_timeout = preplay_timeout,
- expect = expect}
+ suggest_of = suggest_of, minimize = minimize, slices = slices, timeout = timeout,
+ preplay_timeout = preplay_timeout, expect = expect}
end
fun get_params mode = extract_params mode o default_raw_params
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Oct 25 16:57:17 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Oct 25 17:01:23 2024 +0200
@@ -158,7 +158,7 @@
let
val ths = Attrib.eval_thms ctxt [xthm]
val bracket =
- implode (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src ctxt) args)
+ implode (map (enclose "[" "]" o content_of_pretty o Token.pretty_src ctxt) args)
fun nth_name j =
(case xref of
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_instantiations.ML Fri Oct 25 17:01:23 2024 +0200
@@ -0,0 +1,104 @@
+(* Title: HOL/Tools/Metis/metis_instantiations.ML
+ Author: Lukas Bartl, LMU Muenchen
+
+Inference of Variable Instantiations with Metis.
+*)
+
+signature SLEDGEHAMMER_INSTANTIATIONS =
+sig
+ type stature = ATP_Problem_Generate.stature
+
+ val instantiate_facts : Proof.state -> bool -> Time.time -> thm -> int ->
+ (string * stature) list -> (Pretty.T * stature) list option
+end;
+
+structure Sledgehammer_Instantiations : SLEDGEHAMMER_INSTANTIATIONS =
+struct
+
+open ATP_Util
+open ATP_Problem_Generate
+open ATP_Proof_Reconstruct
+open Sledgehammer_Proof_Methods
+open Sledgehammer_Util
+
+(* metis with different options, last two with extensionality *)
+fun metis_methods ctxt =
+ let
+ val ext_facts = [short_thm_name ctxt ext]
+ in
+ [Metis_Method (NONE, NONE, []),
+ Metis_Method (SOME really_full_type_enc, SOME liftingN, []),
+ Metis_Method (SOME no_typesN, SOME liftingN, ext_facts),
+ Metis_Method (SOME full_typesN, SOME liftingN, ext_facts)]
+ end
+
+(* Infer variable instantiations using metis with the given options
+ * (cf. tac_of_metis in Sledgehammer_Proof_Methods.tac_of_proof_method) *)
+fun infer_thm_insts (Metis_Method (type_enc_opt, lam_trans_opt, additional_fact_names)) thms ctxt =
+ let
+ val additional_facts = maps (thms_of_name ctxt) additional_fact_names
+ val ctxt = ctxt
+ |> Config.put Metis_Tactic.verbose false
+ |> Config.put Metis_Tactic.trace false
+ in
+ Metis_Tactic.metis_infer_thm_insts ((Option.map single type_enc_opt, lam_trans_opt),
+ additional_facts @ thms) ctxt
+ end
+
+(* Infer variable instantiations of theorems with timeout *)
+fun timed_infer_thm_insts ctxt verbose timeout chained goal subgoal fact_thms metis_method =
+ let
+ val thms = maps snd fact_thms
+ val timing = Timing.start ()
+ val opt_thm_insts =
+ try (Timeout.apply timeout (infer_thm_insts metis_method thms ctxt chained subgoal)) goal
+ |> Option.join
+ val {cpu = time, ...} = Timing.result timing
+ val _ =
+ if verbose then
+ (let
+ val meth_str = string_of_proof_method (map (fst o fst) fact_thms) metis_method
+ val time_str = string_of_time time
+ in
+ if is_some opt_thm_insts then
+ writeln ("Inferred variable instantiations with " ^ meth_str ^
+ " (" ^ time_str ^ ")")
+ else
+ writeln ("Could not infer variable instantiations with " ^ meth_str ^
+ " (tried " ^ time_str ^ ")")
+ end)
+ else
+ ()
+ in
+ opt_thm_insts
+ end
+
+(* Try to infer variable instantiations of facts and instantiate them
+ * using of-instantiations (e.g. "assms(1)[of x]") *)
+fun instantiate_facts state verbose timeout goal subgoal facts =
+ let
+ val ctxt = Proof.context_of state
+ val {facts = chained, ...} = Proof.goal state
+ val goal = Thm.solve_constraints goal (* avoid exceptions *)
+ val fact_thms = AList.make (thms_of_name ctxt o fst) facts
+ val timed_infer_thm_insts =
+ timed_infer_thm_insts ctxt verbose timeout chained goal subgoal fact_thms
+ fun infer_thm_insts [] = NONE
+ | infer_thm_insts (metis_method :: metis_methods) =
+ (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))
+ in
+ infer_thm_insts (metis_methods ctxt)
+ |> Option.map (map_filter fact_of_thm_inst)
+ |> verbose ? tap (Option.app (fn inst_facts =>
+ Pretty.str "Instantiated facts:" :: map fst inst_facts
+ |> Pretty.block o Pretty.breaks
+ |> Pretty.writeln))
+ end
+
+end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Oct 25 16:57:17 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Oct 25 17:01:23 2024 +0200
@@ -16,7 +16,7 @@
val trace : bool Config.T
type isar_params =
- bool * (string option * string option) * Time.time * real option * bool * bool
+ bool * (string option * string option * string list) * Time.time * real option * bool * bool
* (term, string) atp_step list * thm
val proof_text : Proof.context -> bool -> bool option -> bool -> (unit -> isar_params) -> int ->
@@ -132,11 +132,11 @@
end
type isar_params =
- bool * (string option * string option) * Time.time * real option * bool * bool
+ bool * (string option * string option * string list) * Time.time * real option * bool * bool
* (term, string) atp_step list * thm
val basic_systematic_methods =
- [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method, Argo_Method]
+ [Metis_Method (NONE, NONE, []), Meson_Method, Blast_Method, SATx_Method, Argo_Method]
val basic_simp_based_methods =
[Auto_Method, Simp_Method, Fastforce_Method, Force_Method]
val basic_arith_methods =
@@ -145,7 +145,7 @@
val arith_methods = basic_arith_methods @ basic_simp_based_methods @ basic_systematic_methods
val systematic_methods =
basic_systematic_methods @ basic_arith_methods @ basic_simp_based_methods @
- [Metis_Method (SOME full_typesN, NONE), Metis_Method (SOME no_typesN, NONE)]
+ [Metis_Method (SOME full_typesN, NONE, []), Metis_Method (SOME no_typesN, NONE, [])]
val rewrite_methods = basic_simp_based_methods @ basic_systematic_methods @ basic_arith_methods
val skolem_methods = Moura_Method :: systematic_methods
@@ -483,11 +483,11 @@
let
val used_facts' =
map_filter (fn s =>
- if exists (fn (s', (sc, _)) => s' = s andalso sc = Chained)
- used_facts then
+ if exists (fn (p, (sc, _)) => content_of_pretty p = s andalso
+ sc = Chained) used_facts then
NONE
else
- SOME (s, (Global, General))) gfs
+ SOME (Pretty.str s, (Global, General))) gfs
in
((used_facts', (meth, play_outcome)), banner, subgoal, subgoal_count)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Fri Oct 25 16:57:17 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Fri Oct 25 17:01:23 2024 +0200
@@ -14,7 +14,7 @@
SMT_Verit of string
datatype proof_method =
- Metis_Method of string option * string option |
+ Metis_Method of string option * string option * string list |
Meson_Method |
SMT_Method of SMT_backend |
SATx_Method |
@@ -36,9 +36,10 @@
Play_Failed
type one_line_params =
- ((string * stature) list * (proof_method * play_outcome)) * string * int * int
+ ((Pretty.T * stature) list * (proof_method * play_outcome)) * string * int * int
val is_proof_method_direct : proof_method -> bool
+ val pretty_proof_method : string -> string -> Pretty.T list -> proof_method -> Pretty.T
val string_of_proof_method : string list -> proof_method -> string
val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
val string_of_play_outcome : play_outcome -> string
@@ -52,13 +53,14 @@
open ATP_Util
open ATP_Problem_Generate
open ATP_Proof_Reconstruct
+open Sledgehammer_Util
datatype SMT_backend =
SMT_Z3 |
SMT_Verit of string
datatype proof_method =
- Metis_Method of string option * string option |
+ Metis_Method of string option * string option * string list |
Meson_Method |
SMT_Method of SMT_backend |
SATx_Method |
@@ -80,7 +82,7 @@
Play_Failed
type one_line_params =
- ((string * stature) list * (proof_method * play_outcome)) * string * int * int
+ ((Pretty.T * stature) list * (proof_method * play_outcome)) * string * int * int
fun is_proof_method_direct (Metis_Method _) = true
| is_proof_method_direct Meson_Method = true
@@ -91,7 +93,13 @@
fun is_proof_method_multi_goal Auto_Method = true
| is_proof_method_multi_goal _ = false
-fun maybe_paren s = s |> not (Symbol_Pos.is_identifier s) ? enclose "(" ")"
+fun pretty_paren prefix suffix = Pretty.enclose (prefix ^ "(") (")" ^ suffix)
+fun pretty_maybe_paren prefix suffix [pretty] =
+ if Symbol_Pos.is_identifier (content_of_pretty pretty) then
+ Pretty.block [Pretty.str prefix, pretty, Pretty.str suffix]
+ else
+ pretty_paren prefix suffix [pretty]
+ | pretty_maybe_paren prefix suffix pretties = pretty_paren prefix suffix pretties
(*
Combine indexed fact names for pretty-printing.
@@ -99,35 +107,36 @@
Combines only adjacent same names.
Input should not have same name with and without index.
*)
-fun merge_indexed_facts (ss: string list) :string list =
+fun merge_indexed_facts (facts: Pretty.T list) : Pretty.T list =
let
- fun split (s: string) : string * string =
- if String.isPrefix "\<open>" s then (s,"")
- else
- case first_field "(" s of
- NONE => (s,"")
- | SOME (name,isp) => (name, String.substring (isp, 0, size isp - 1))
+ fun split (p: Pretty.T) : (string * string) option =
+ try (unsuffix ")" o content_of_pretty) p
+ |> Option.mapPartial (first_field "(")
+
+ fun add_pretty (name,is) = (SOME (name,is),Pretty.str (name ^ "(" ^ is ^ ")"))
- fun merge ((name1,is1) :: (name2,is2) :: zs) =
+ fun merge ((SOME (name1,is1),p1) :: (y as (SOME (name2,is2),_)) :: zs) =
if name1 = name2
- then merge ((name1,is1 ^ "," ^ is2) :: zs)
- else (name1,is1) :: merge ((name2,is2) :: zs)
- | merge xs = xs;
-
- fun parents is = if is = "" then "" else "(" ^ is ^ ")"
+ then merge (add_pretty (name1,is1 ^ "," ^ is2) :: zs)
+ else p1 :: merge (y :: zs)
+ | merge ((_,p) :: ys) = p :: merge ys
+ | merge [] = []
in
- map (fn (name,is) => name ^ parents is) (merge (map split ss))
+ merge (map (`split) facts)
end
-fun string_of_proof_method ss meth =
+fun pretty_proof_method prefix suffix facts meth =
let
val meth_s =
(case meth of
- Metis_Method (NONE, NONE) => "metis"
- | Metis_Method (type_enc_opt, lam_trans_opt) =>
- "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
+ Metis_Method (NONE, NONE, additional_fact_names) =>
+ implode_space ("metis" :: additional_fact_names)
+ | Metis_Method (type_enc_opt, lam_trans_opt, additional_fact_names) =>
+ implode_space ("metis" ::
+ "(" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")" ::
+ additional_fact_names)
| Meson_Method => "meson"
| SMT_Method SMT_Z3 => "smt (z3)"
| SMT_Method (SMT_Verit strategy) =>
@@ -135,7 +144,7 @@
| SATx_Method => "satx"
| Argo_Method => "argo"
| Blast_Method => "blast"
- | Simp_Method => if null ss then "simp" else "simp add:"
+ | Simp_Method => if null facts then "simp" else "simp add:"
| Auto_Method => "auto"
| Fastforce_Method => "fastforce"
| Force_Method => "force"
@@ -145,19 +154,25 @@
| Algebra_Method => "algebra"
| Order_Method => "order")
in
- maybe_paren (implode_space (meth_s :: merge_indexed_facts ss))
+ pretty_maybe_paren prefix suffix
+ (Pretty.str meth_s :: merge_indexed_facts facts |> Pretty.breaks)
end
+fun string_of_proof_method ss =
+ pretty_proof_method "" "" (map Pretty.str ss)
+ #> content_of_pretty
+
fun tac_of_proof_method ctxt (local_facts, global_facts) meth =
let
- fun tac_of_metis (type_enc_opt, lam_trans_opt) =
+ fun tac_of_metis (type_enc_opt, lam_trans_opt, additional_fact_names) =
let
+ val additional_facts = maps (thms_of_name ctxt) additional_fact_names
val ctxt = ctxt
|> Config.put Metis_Tactic.verbose false
|> Config.put Metis_Tactic.trace false
in
SELECT_GOAL (Metis_Tactic.metis_method ((Option.map single type_enc_opt, lam_trans_opt),
- global_facts) ctxt local_facts)
+ additional_facts @ global_facts) ctxt local_facts)
end
fun tac_of_smt SMT_Z3 = SMT_Solver.smt_tac
@@ -207,27 +222,36 @@
(* FIXME *)
fun proof_method_command meth i n used_chaineds _(*num_chained*) extras =
let
- val (indirect_ss, direct_ss) =
+ val (indirect_facts, direct_facts) =
if is_proof_method_direct meth then ([], extras) else (extras, [])
+ val suffix =
+ if is_proof_method_multi_goal meth andalso n <> 1 then "[1]" else ""
in
- (if null indirect_ss then ""
- else "using " ^ implode_space (merge_indexed_facts indirect_ss) ^ " ") ^
- apply_on_subgoal i n ^ string_of_proof_method direct_ss meth ^
- (if is_proof_method_multi_goal meth andalso n <> 1 then "[1]" else "")
+ (if null indirect_facts then []
+ else Pretty.str "using" :: merge_indexed_facts indirect_facts) @
+ [pretty_proof_method (apply_on_subgoal i n) suffix direct_facts meth]
+ |> Pretty.block o Pretty.breaks
+ |> Pretty.symbolic_string_of (* markup string *)
end
fun try_command_line banner play command =
let val s = string_of_play_outcome play in
- banner ^ Active.sendback_markup_command command ^ (s |> s <> "" ? enclose " (" ")")
+ (* Add optional markup break (command may need multiple lines) *)
+ banner ^ Markup.markup (Markup.break {width = 1, indent = 2}) " " ^
+ Active.sendback_markup_command command ^ (s |> s <> "" ? enclose " (" ")")
end
+val failed_command_line =
+ prefix ("One-line proof reconstruction failed:" ^
+ (* 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) =
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
- |> (if play = Play_Failed then prefix "One-line proof reconstruction failed: "
- else try_command_line banner play)
+ |> (if play = Play_Failed then failed_command_line else try_command_line banner play)
end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Oct 25 16:57:17 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Oct 25 17:01:23 2024 +0200
@@ -47,6 +47,7 @@
compress : real option,
try0 : bool,
smt_proofs : bool,
+ suggest_of : bool option,
minimize : bool,
slices : int,
timeout : Time.time,
@@ -78,7 +79,7 @@
used_from : fact list,
preferred_methss : proof_method * proof_method list list,
run_time : Time.time,
- message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string}
+ message : (unit -> (Pretty.T * stature) list * (proof_method * play_outcome)) -> string}
type prover = params -> prover_problem -> prover_slice -> prover_result
@@ -88,7 +89,9 @@
val overlord_file_location_of_prover : string -> string * string
val proof_banner : mode -> string -> string
val is_atp : string -> bool
- val bunches_of_proof_methods : Proof.context -> bool -> bool -> string -> proof_method list list
+ val bunches_of_metis_methods : Proof.context -> bool -> bool -> proof_method list list
+ val bunches_of_smt_methods : Proof.context -> proof_method list list
+ val bunches_of_proof_methods : Proof.context -> bool -> bool -> bool -> proof_method list list
val facts_of_filter : string -> (string * fact list) list -> fact list
val facts_of_basic_slice : base_slice -> (string * fact list) list -> fact list
val is_fact_chained : (('a * stature) * 'b) -> bool
@@ -107,7 +110,6 @@
open ATP_Problem
open ATP_Problem_Generate
open ATP_Proof_Reconstruct
-open Metis_Tactic
open Sledgehammer_Fact
open Sledgehammer_Proof_Methods
open Sledgehammer_ATP_Systems
@@ -158,6 +160,7 @@
compress : real option,
try0 : bool,
smt_proofs : bool,
+ suggest_of : bool option,
minimize : bool,
slices : int,
timeout : Time.time,
@@ -201,7 +204,7 @@
used_from : fact list,
preferred_methss : proof_method * proof_method list list,
run_time : Time.time,
- message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string}
+ message : (unit -> (Pretty.T * stature) list * (proof_method * play_outcome)) -> string}
type prover = params -> prover_problem -> prover_slice -> prover_result
@@ -209,30 +212,58 @@
fun proof_banner mode prover_name =
(case mode of
- Auto_Try => "Auto Sledgehammer (" ^ prover_name ^ ") found a proof: "
- | Try => "Sledgehammer (" ^ prover_name ^ ") found a proof: "
- | _ => "Try this: ")
+ Auto_Try => "Auto Sledgehammer (" ^ prover_name ^ ") found a proof:"
+ | Try => "Sledgehammer (" ^ prover_name ^ ") found a proof:"
+ | _ => "Try this:")
+
+fun bunches_of_metis_methods ctxt needs_full_types needs_lam_defs =
+ let
+ (* metis without options (preferred) *)
+ val preferred_method = Metis_Method (NONE, NONE, [])
-fun bunches_of_proof_methods ctxt smt_proofs needs_full_types desperate_lam_trans =
+ (* metis with different options *)
+ val desperate_lam_trans = if needs_lam_defs then liftingN else opaque_liftingN
+ val option_methods =
+ Metis_Method (SOME full_typesN, NONE, []) ::
+ Metis_Method (NONE, SOME liftingN, []) ::
+ Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans, []) ::
+ (if needs_full_types then
+ [Metis_Method (SOME really_full_type_enc, NONE, []),
+ Metis_Method (SOME full_typesN, SOME desperate_lam_trans, [])]
+ else
+ [Metis_Method (SOME no_typesN, SOME desperate_lam_trans, [])])
+
+ (* metis with extensionality (often needed for lifting) *)
+ val ext_facts = [short_thm_name ctxt ext]
+ val ext_methods =
+ Metis_Method (NONE, SOME liftingN, ext_facts) ::
+ (if not needs_lam_defs then
+ []
+ else if needs_full_types then
+ [Metis_Method (SOME full_typesN, SOME liftingN, ext_facts)]
+ else
+ [Metis_Method (SOME no_typesN, SOME liftingN, ext_facts)])
+ in
+ [[preferred_method], option_methods, ext_methods]
+ end
+
+fun bunches_of_smt_methods ctxt =
+ [map (SMT_Method o SMT_Verit) (Verit_Strategies.all_veriT_stgies (Context.Proof ctxt)),
+ [SMT_Method SMT_Z3]]
+
+fun bunches_of_proof_methods ctxt smt_proofs needs_full_types needs_lam_defs =
let
val misc_methodss =
[[Simp_Method, Auto_Method, Blast_Method, Linarith_Method, Meson_Method,
- Metis_Method (NONE, NONE), Fastforce_Method, Force_Method, Presburger_Method,
+ Metis_Method (NONE, NONE, []), Fastforce_Method, Force_Method, Presburger_Method,
Argo_Method, Order_Method]]
val metis_methodss =
- [Metis_Method (SOME full_typesN, NONE) ::
- Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans) ::
- (if needs_full_types then
- [Metis_Method (SOME really_full_type_enc, NONE),
- Metis_Method (SOME full_typesN, SOME desperate_lam_trans)]
- else
- [Metis_Method (SOME no_typesN, SOME desperate_lam_trans)])]
+ tl (bunches_of_metis_methods ctxt needs_full_types needs_lam_defs)
val smt_methodss =
if smt_proofs then
- [map (SMT_Method o SMT_Verit) (Verit_Strategies.all_veriT_stgies (Context.Proof ctxt)),
- [SMT_Method SMT_Z3]]
+ bunches_of_smt_methods ctxt
else
[]
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Oct 25 16:57:17 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Oct 25 17:01:23 2024 +0200
@@ -295,14 +295,15 @@
()
val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
- val preferred = Metis_Method (NONE, NONE)
+ val needs_lam_defs =
+ good_lam_trans = keep_lamsN orelse is_lam_def_used_in_atp_proof atp_proof
+ val preferred = Metis_Method (NONE, NONE, [])
val preferred_methss =
(preferred,
if try0 then
- bunches_of_proof_methods ctxt smt_proofs needs_full_types
- (if atp_proof_prefers_lifting atp_proof then liftingN else opaque_liftingN)
+ bunches_of_proof_methods ctxt smt_proofs needs_full_types needs_lam_defs
else
- [[preferred]])
+ bunches_of_metis_methods ctxt needs_full_types needs_lam_defs)
in
(NONE, used_facts, preferred_methss,
fn preplay =>
@@ -328,8 +329,8 @@
|> local_name = zipperpositionN ? regroup_zipperposition_skolems
|> factify_atp_proof (map fst used_from) hyp_ts concl_t
in
- (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0,
- minimize, full_atp_proof, goal)
+ (verbose, (metis_type_enc, metis_lam_trans, []), preplay_timeout, compress,
+ try0, minimize, full_atp_proof, goal)
end
val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Oct 25 16:57:17 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Oct 25 17:01:23 2024 +0200
@@ -24,7 +24,7 @@
val minimize_facts : (thm list -> unit) -> string -> params -> prover_slice -> bool -> int ->
int -> Proof.state -> thm -> ((string * stature) * thm list) list ->
((string * stature) * thm list) list option
- * ((unit -> (string * stature) list * (proof_method * play_outcome)) -> string)
+ * ((unit -> (Pretty.T * stature) list * (proof_method * play_outcome)) -> string)
val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover
end;
@@ -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,
- minimize, preplay_timeout, induction_rules, ...} : params)
+ suggest_of, minimize, preplay_timeout, induction_rules, ...} : params)
(slice as ((_, _, falsify, _, fact_filter), slice_extra)) silent (prover : prover) timeout i n
state goal facts =
let
@@ -98,8 +98,8 @@
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,
- minimize = minimize, slices = 1, timeout = timeout, preplay_timeout = preplay_timeout,
- expect = ""}
+ suggest_of = suggest_of, minimize = minimize, slices = 1, timeout = timeout,
+ preplay_timeout = preplay_timeout, expect = ""}
val problem =
{comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
factss = [("", facts)], has_already_found_something = K false, found_something = K ()}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Fri Oct 25 16:57:17 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Fri Oct 25 17:01:23 2024 +0200
@@ -141,12 +141,14 @@
if smt_proofs then
SMT_Method (if name = "z3" then SMT_Z3 else SMT_Verit "default")
else
- Metis_Method (NONE, NONE);
+ Metis_Method (NONE, NONE, []);
val methss =
if try0 then
- bunches_of_proof_methods ctxt smt_proofs false liftingN
+ bunches_of_proof_methods ctxt smt_proofs false true
+ else if smt_proofs then
+ bunches_of_smt_methods ctxt
else
- [[preferred]]
+ bunches_of_metis_methods ctxt false true
in
((preferred, methss),
fn preplay =>
@@ -154,8 +156,8 @@
val _ = if verbose then writeln "Generating proof text..." else ()
fun isar_params () =
- (verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (),
- goal)
+ (verbose, (NONE, NONE, []), preplay_timeout, compress, try0, minimize,
+ atp_proof (), goal)
val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count)
val num_chained = length (#facts (Proof.goal state))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Oct 25 16:57:17 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Oct 25 17:01:23 2024 +0200
@@ -115,14 +115,12 @@
fun thms_of_name ctxt name =
let
- val get = maps (Proof_Context.get_fact ctxt o fst)
val keywords = Thy_Header.get_keywords' ctxt
in
- Symbol_Pos.explode (name, Position.start)
- |> Token.tokenize keywords {strict = false}
+ Token.explode keywords Position.start name
|> filter Token.is_proper
|> Source.of_list
- |> Source.source Token.stopper (Parse.thms1 >> get)
+ |> Source.source' (Context.Proof ctxt) Token.stopper Attrib.multi_thm
|> Source.exhaust
end