merged
authordesharna
Fri, 28 Mar 2025 08:24:07 +0100
changeset 82365 7fee9141da5e
parent 82364 5af097d05e99 (diff)
parent 82354 35a219e372b0 (current diff)
child 82366 7816e7be7bc7
merged
--- a/src/HOL/HOL.thy	Fri Mar 28 00:26:18 2025 +0000
+++ b/src/HOL/HOL.thy	Fri Mar 28 08:24:07 2025 +0100
@@ -5,7 +5,7 @@
 section \<open>The basis of Higher-Order Logic\<close>
 
 theory HOL
-imports Pure Tools.Code_Generator
+imports Pure Try0 Tools.Code_Generator
 keywords
   "try" "solve_direct" "quickcheck" "print_coercions" "print_claset"
     "print_induct_rules" :: diag and
@@ -34,6 +34,12 @@
 ML_file \<open>~~/src/Tools/subtyping.ML\<close>
 ML_file \<open>~~/src/Tools/case_product.ML\<close>
 
+ML \<open>
+val _ =
+  Try.tool_setup
+   {name = "try0", weight = 30, auto_option = \<^system_option>\<open>auto_methods\<close>,
+    body = fn auto => fst o Try0.generic_try0 (if auto then Try0.Auto_Try else Try0.Try) NONE Try0.empty_facts}
+\<close>
 
 ML \<open>Plugin_Name.declare_setup \<^binding>\<open>extraction\<close>\<close>
 
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Mar 28 00:26:18 2025 +0000
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Mar 28 08:24:07 2025 +0100
@@ -148,7 +148,7 @@
   let
     val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (Proof_Context.init_global thy)
   in
-    case Try0.try0 (SOME (seconds 5.0)) [] state of
+    case Try0.try0 (SOME (seconds 5.0)) Try0.empty_facts state of
       [] => (Unsolved, [])
     | _ => (Solved, [])
   end
--- a/src/HOL/Sledgehammer.thy	Fri Mar 28 00:26:18 2025 +0000
+++ b/src/HOL/Sledgehammer.thy	Fri Mar 28 08:24:07 2025 +0100
@@ -7,7 +7,7 @@
 section \<open>Sledgehammer: Isabelle--ATP Linkup\<close>
 
 theory Sledgehammer
-imports Presburger SMT Try0
+imports Presburger SMT Try0_HOL
 keywords
   "sledgehammer" :: diag and
   "sledgehammer_params" :: thy_decl
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Fri Mar 28 00:26:18 2025 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Fri Mar 28 08:24:07 2025 +0100
@@ -216,7 +216,7 @@
 
 end
 
-val try0 = not o null o Try0.try0 (SOME (Time.fromSeconds 5)) []
+val try0 = not o null o Try0.try0 (SOME (Time.fromSeconds 5)) Try0.empty_facts
 
 fun make_action ({arguments, timeout, output_dir, ...} : Mirabelle.action_context) =
   let
--- a/src/HOL/Tools/Mirabelle/mirabelle_try0.ML	Fri Mar 28 00:26:18 2025 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle_try0.ML	Fri Mar 28 08:24:07 2025 +0100
@@ -12,9 +12,10 @@
 fun make_action ({timeout, ...} : Mirabelle.action_context) =
   let
     val generous_timeout = Time.scale 10.0 timeout
+    val try0 = Try0.try0 (SOME timeout) Try0.empty_facts
 
     fun run ({pre, ...} : Mirabelle.command) =
-      if Timeout.apply generous_timeout (not o null o Try0.try0 (SOME timeout) []) pre then
+      if Timeout.apply generous_timeout (not o null o try0) pre then
         "succeeded"
       else
         ""
--- a/src/HOL/Tools/Nunchaku/nunchaku_commands.ML	Fri Mar 28 00:26:18 2025 +0000
+++ b/src/HOL/Tools/Nunchaku/nunchaku_commands.ML	Fri Mar 28 08:24:07 2025 +0100
@@ -246,7 +246,7 @@
 
 fun run_chaku override_params mode i state0 =
   let
-    val state = Proof.map_contexts (Try0.silence_methods false) state0;
+    val state = Proof.map_contexts Try0_HOL.silence_methods state0;
     val thy = Proof.theory_of state;
     val ctxt = Proof.context_of state;
     val _ = List.app check_raw_param override_params;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri Mar 28 00:26:18 2025 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri Mar 28 08:24:07 2025 +0100
@@ -292,7 +292,7 @@
 fun default_params thy = get_params Normal thy o map (apsnd single)
 
 val silence_state =
-  Proof.map_contexts (Try0.silence_methods false #> Config.put SMT_Config.verbose false)
+  Proof.map_contexts (Try0_HOL.silence_methods #> Config.put SMT_Config.verbose false)
 
 (* Sledgehammer the given subgoal *)
 
--- a/src/HOL/Tools/try0.ML	Fri Mar 28 00:26:18 2025 +0000
+++ b/src/HOL/Tools/try0.ML	Fri Mar 28 08:24:07 2025 +0100
@@ -1,180 +1,130 @@
-(*  Title:      HOL/Tools/try0.ML
-    Author:     Jasmin Blanchette, TU Muenchen
+(* Title:      HOL/Tools/try0.ML
+   Author:     Jasmin Blanchette, LMU Muenchen
+   Author:     Martin Desharnais, LMU Muenchen
+   Author:     Fabian Huch, TU Muenchen
 
 Try a combination of proof methods.
 *)
 
 signature TRY0 =
 sig
-  val silence_methods : bool -> Proof.context -> Proof.context
-  datatype modifier = Use | Simp | Intro | Elim | Dest
-  type xthm = Facts.ref * Token.src list
-  type tagged_xthm = xthm * modifier list
+  val serial_commas : string -> string list -> string list
+
+  type xref = Facts.ref * Token.src list
+
+  type facts =
+    {usings: xref list,
+     simps : xref list,
+     intros : xref list,
+     elims : xref list,
+     dests : xref list}
+  val empty_facts : facts
+
   type result = {name: string, command: string, time: Time.time, state: Proof.state}
-  val apply_proof_method : string -> Time.time option -> (xthm * modifier list) list ->
-    Proof.state -> result option
-  val try0 : Time.time option -> tagged_xthm list -> Proof.state -> result list
+  type proof_method = Time.time option -> facts -> Proof.state -> result option
+  type proof_method_options = {run_if_auto_try: bool}
+
+  val register_proof_method : string -> proof_method_options -> proof_method -> unit
+  val get_proof_method : string -> proof_method option
+  val get_all_proof_method_names : unit -> string list
+
+  datatype mode = Auto_Try | Try | Normal
+  val generic_try0 : mode -> Time.time option -> facts -> Proof.state ->
+    (bool * (string * string list)) * result list
+  val try0 : Time.time option -> facts -> Proof.state -> result list
 end
 
 structure Try0 : TRY0 =
 struct
 
+fun serial_commas _ [] = ["??"]
+  | serial_commas _ [s] = [s]
+  | serial_commas conj [s1, s2] = [s1, conj, s2]
+  | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
+  | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss;
+
 val noneN = "none"
 
 datatype mode = Auto_Try | Try | Normal
 
 val default_timeout = seconds 5.0
 
-fun run_tac timeout_opt tac st =
-  let val with_timeout =
-    (case timeout_opt of SOME timeout => Timeout.apply_physical timeout | NONE => I)
-  in with_timeout (Seq.pull o tac) st |> Option.map fst end
-
-val num_goals = Thm.nprems_of o #goal o Proof.goal
-fun apply_recursive recurse elapsed0 timeout_opt apply st =
-  (case Timing.timing (Option.join o try (run_tac timeout_opt apply)) st of
-    ({elapsed, ...}, SOME st') =>
-      if recurse andalso num_goals st' > 0 andalso num_goals st' < num_goals st then
-        let val timeout_opt1 = (Option.map (fn timeout => timeout - elapsed) timeout_opt)
-        in apply_recursive recurse (elapsed0 + elapsed) timeout_opt1 apply st' end
-      else (elapsed0 + elapsed, st')
-   |_ => (elapsed0, st))
+datatype modifier = Use | Simp | Intro | Elim | Dest
+type xref = Facts.ref * Token.src list
+type tagged_xref = xref * modifier list
+type facts =
+  {usings: xref list,
+   simps : xref list,
+   intros : xref list,
+   elims : xref list,
+   dests : xref list}
 
-fun parse_method ctxt s =
-  enclose "(" ")" s
-  |> Token.explode (Thy_Header.get_keywords' ctxt) Position.start
-  |> filter Token.is_proper
-  |> Scan.read Token.stopper Method.parse
-  |> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source")
-
-datatype modifier = Use | Simp | Intro | Elim | Dest
-type xthm = Facts.ref * Token.src list
-type tagged_xthm = xthm * modifier list
-
-fun string_of_xthm ((xref, args) : xthm) =
-  (case xref of
-    Facts.Fact literal => literal |> Symbol_Pos.explode0 |> Symbol_Pos.implode |> cartouche
-  | _ =>
-      Facts.string_of_ref xref) ^ implode
-        (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src \<^context>) args)
-
-fun add_attr_text (tagged : tagged_xthm list) (tag, src) s =
-  let
-    val fs = tagged |> filter (fn (_, tags) => member (op =) tags tag) |> map (string_of_xthm o fst)
-  in if null fs then s else s ^ " " ^ (if src = "" then "" else src ^ ": ") ^ implode_space fs end
-
-fun attrs_text tags (tagged : tagged_xthm list) =
-  "" |> fold (add_attr_text tagged) tags
+val empty_facts: facts = {usings = [], simps = [], intros = [], elims = [], dests = []}
+fun union_facts (left : facts) (right : facts) : facts =
+  {usings = #usings left @ #usings right,
+   simps = #simps left @ #simps right,
+   intros = #intros left @ #intros right,
+   elims = #elims left @ #elims right,
+   dests = #dests left @ #dests right}
 
 type result = {name: string, command: string, time: Time.time, state: Proof.state}
+type proof_method = Time.time option -> facts -> Proof.state -> result option
+type proof_method_options = {run_if_auto_try: bool}
+
+val noop_proof_method : proof_method = fn _ => fn _ => fn _ => NONE
 
 local
-
-val full_attrs = [(Simp, "simp"), (Intro, "intro"), (Elim, "elim"), (Dest, "dest")]
-val clas_attrs = [(Intro, "intro"), (Elim, "elim"), (Dest, "dest")]
-val simp_attrs = [(Simp, "add")]
-val metis_attrs = [(Simp, ""), (Intro, ""), (Elim, ""), (Dest, "")]
-val no_attrs = []
-
-(* name * ((all_goals, run_if_auto_try), tags *)
-val raw_named_methods =
-  [("simp", ((false, true), simp_attrs)),
-   ("auto", ((true, true), full_attrs)),
-   ("blast", ((false, true), clas_attrs)),
-   ("metis", ((false, true), metis_attrs)),
-   ("argo", ((false, true), no_attrs)),
-   ("linarith", ((false, true), no_attrs)),
-   ("presburger", ((false, true), no_attrs)),
-   ("algebra", ((false, true), no_attrs)),
-   ("fast", ((false, false), clas_attrs)),
-   ("fastforce", ((false, false), full_attrs)),
-   ("force", ((false, false), full_attrs)),
-   ("meson", ((false, false), metis_attrs)),
-   ("satx", ((false, false), no_attrs)),
-   ("order", ((false, true), no_attrs))]
-
-fun apply_raw_named_method (name, ((all_goals, _), attrs)) timeout_opt tagged st :
-    result option =
-  let
-    val unused =
-      tagged
-      |> filter
-        (fn (_, tags) => not (null tags) andalso null (inter (op =) tags (attrs |> map fst)))
-      |> map fst
-
-    val attrs = attrs_text attrs tagged
-
-    val ctxt = Proof.context_of st
-
-    val text =
-      name ^ attrs
-      |> parse_method ctxt
-      |> Method.method_cmd ctxt
-      |> Method.Basic
-      |> (fn m => Method.Combinator (Method.no_combinator_info, Method.Select_Goals 1, [m]))
-
-    val apply =
-      Proof.using [Attrib.eval_thms ctxt unused |> map (rpair [] o single)]
-      #> Proof.refine text #> Seq.filter_results
-    val num_before = num_goals st
-    val multiple_goals = all_goals andalso num_before > 1
-    val (time, st') = apply_recursive multiple_goals Time.zeroTime timeout_opt apply st
-    val num_after = num_goals st'
-    val select = "[" ^ string_of_int (num_before - num_after)  ^ "]"
-    val unused = implode_space (unused |> map string_of_xthm)
-    val command =
-      (if unused <> "" then "using " ^ unused ^ " " else "") ^
-      (if num_after = 0 then "by " else "apply ") ^
-      (name ^ attrs |> attrs <> "" ? enclose "(" ")") ^
-      (if multiple_goals andalso num_after > 0 then select else "")
-  in
-    if num_before > num_after then
-      SOME {name = name, command = command, time = time, state = st'}
-    else NONE
-  end
-
+  val proof_methods =
+    Synchronized.var "Try0.proof_methods" (Symtab.empty : proof_method Symtab.table);
+  val auto_try_proof_methods_names =
+    Synchronized.var "Try0.auto_try_proof_methods" (Symset.empty : Symset.T);
 in
 
-val named_methods = map fst raw_named_methods
-
-fun apply_proof_method name timeout_opt tagged st :
-  result option =
-  (case AList.lookup (op =) raw_named_methods name of
-    NONE => NONE
-  | SOME raw_method => apply_raw_named_method (name, raw_method) timeout_opt tagged st)
+fun register_proof_method name ({run_if_auto_try} : proof_method_options) proof_method =
+  let
+    val () = if name = "" then error "Registering unnamed proof method" else ()
+    val () = Synchronized.change proof_methods (Symtab.update (name, proof_method))
+    val () =
+      if run_if_auto_try then
+        Synchronized.change auto_try_proof_methods_names (Symset.insert name)
+      else
+        ()
+  in () end
 
-fun maybe_apply_proof_method name mode timeout_opt tagged st :
-  result option =
-  (case AList.lookup (op =) raw_named_methods name of
-    NONE => NONE
-  | SOME (raw_method as ((_, run_if_auto_try), _)) =>
-    if mode <> Auto_Try orelse run_if_auto_try then
-      apply_raw_named_method (name, raw_method) timeout_opt tagged st
-    else
-      NONE)
+fun get_proof_method (name : string) : proof_method option =
+  Symtab.lookup (Synchronized.value proof_methods) name;
+
+fun get_all_proof_methods () : (string * proof_method) list =
+  Symtab.fold (fn x => fn xs => x :: xs) (Synchronized.value proof_methods) []
+
+fun get_all_proof_method_names () : string list =
+  Symtab.fold (fn (name, _) => fn names => name :: names) (Synchronized.value proof_methods) []
+
+fun get_all_auto_try_proof_method_names () : string list =
+  Symset.dest (Synchronized.value auto_try_proof_methods_names)
+
+fun should_auto_try_proof_method (name : string) : bool =
+  Symset.member (Synchronized.value auto_try_proof_methods_names) name
 
 end
 
-val maybe_apply_methods = map maybe_apply_proof_method named_methods
+fun get_proof_method_or_noop name =
+  (case get_proof_method name of
+    NONE => noop_proof_method
+  | SOME proof_method => proof_method)
+
+fun maybe_apply_proof_method name mode : proof_method =
+  if mode <> Auto_Try orelse should_auto_try_proof_method name then
+    get_proof_method_or_noop name
+  else
+    noop_proof_method
 
 fun time_string time = string_of_int (Time.toMilliseconds time) ^ " ms"
 fun tool_time_string (s, time) = s ^ ": " ^ time_string time
 
-(* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification
-   bound exceeded" warnings and the like. *)
-fun silence_methods debug =
-  Config.put Metis_Tactic.verbose debug
-  #> not debug ? (fn ctxt =>
-      ctxt
-      |> Simplifier_Trace.disable
-      |> Context_Position.set_visible false
-      |> Config.put Unify.unify_trace false
-      |> Config.put Argo_Tactic.trace "none")
-
-fun generic_try0 mode timeout_opt (tagged : tagged_xthm list) st =
+fun generic_try0 mode timeout_opt (facts : facts) st =
   let
-    val st = Proof.map_contexts (silence_methods false) st
-    fun try_method method = method mode timeout_opt tagged st
+    fun try_method (method : mode -> proof_method) = method mode timeout_opt facts st
     fun get_message {command, time, ...} = "Found proof: " ^ Active.sendback_markup_command
       command ^ " (" ^ time_string time ^ ")"
     val print_step = Option.map (tap (writeln o get_message))
@@ -188,11 +138,13 @@
         methods
         |> Par_List.get_some try_method
         |> the_list
+    val proof_method_names = get_all_proof_method_names ()
+    val maybe_apply_methods = map maybe_apply_proof_method proof_method_names
   in
     if mode = Normal then
-      "Trying " ^ implode_space (Try.serial_commas "and" (map quote named_methods)) ^
-      "..."
-      |> writeln
+      let val names = map quote proof_method_names in
+        writeln ("Trying " ^ implode_space (serial_commas "and" names) ^ "...")
+      end
     else
       ();
     (case get_results maybe_apply_methods of
@@ -220,29 +172,28 @@
 
 fun try0 timeout_opt = snd oo generic_try0 Normal timeout_opt
 
-fun try0_trans tagged =
+fun try0_trans (facts : facts) =
   Toplevel.keep_proof
-    (ignore o generic_try0 Normal (SOME default_timeout) tagged o Toplevel.proof_of)
+    (ignore o generic_try0 Normal (SOME default_timeout) facts o Toplevel.proof_of)
 
 val parse_fact_refs = Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse.thm)
 
 val parse_attr =
-  Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs >> (map (rpair [Simp]))
-  || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs >> (map (rpair [Intro]))
-  || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs >> (map (rpair [Elim]))
-  || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs >> (map (rpair [Dest]))
+  Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs >> (fn xrefs =>
+    {usings = [], simps = xrefs, intros = [], elims = [], dests = []})
+  || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs >> (fn xrefs =>
+    {usings = [], simps = [], intros = xrefs, elims = [], dests = []})
+  || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs >> (fn xrefs =>
+    {usings = [], simps = [], intros = [], elims = xrefs, dests = []})
+  || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs >> (fn xrefs =>
+    {usings = [], simps = [], intros = [], elims = [], dests = xrefs})
 
 fun parse_attrs x =
   (Args.parens parse_attrs
-   || Scan.repeat parse_attr >> (fn tagged => fold (curry (op @)) tagged [])) x
+   || Scan.repeat parse_attr >> (fn factss => fold union_facts factss empty_facts)) x
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>try0\<close> "try a combination of proof methods"
-    (Scan.optional parse_attrs [] #>> try0_trans)
-
-val _ =
-  Try.tool_setup
-   {name = "try0", weight = 30, auto_option = \<^system_option>\<open>auto_methods\<close>,
-    body = fn auto => fst o generic_try0 (if auto then Auto_Try else Try) NONE []}
+    (Scan.optional parse_attrs empty_facts #>> try0_trans)
 
 end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/try0_util.ML	Fri Mar 28 08:24:07 2025 +0100
@@ -0,0 +1,146 @@
+(* Title:      HOL/Tools/try0_hol.ML
+   Author:     Jasmin Blanchette, LMU Muenchen
+   Author:     Martin Desharnais, LMU Muenchen
+   Author:     Fabian Huch, TU Muenchen
+
+General-purpose functions used by Try0.
+*)
+
+signature TRY0_UTIL =
+sig
+  val string_of_xref : Try0.xref -> string
+
+  type facts_prefixes =
+    {usings: string,
+     simps : string,
+     intros : string,
+     elims : string,
+     dests : string}
+  val full_attrs : facts_prefixes
+  val clas_attrs : facts_prefixes
+  val simp_attrs : facts_prefixes
+  val metis_attrs : facts_prefixes
+  val no_attrs : facts_prefixes
+  val apply_raw_named_method : string -> bool -> facts_prefixes ->
+    (Proof.context -> Proof.context) -> Time.time option -> Try0.facts -> Proof.state ->
+    Try0.result option
+end
+
+structure Try0_Util : TRY0_UTIL = struct
+
+fun string_of_xref ((xref, args) : Try0.xref) =
+  (case xref of
+    Facts.Fact literal => literal |> Symbol_Pos.explode0 |> Symbol_Pos.implode |> cartouche
+  | _ =>
+      Facts.string_of_ref xref) ^ implode
+        (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src \<^context>) args)
+
+
+type facts_prefixes =
+  {usings: string,
+   simps : string,
+   intros : string,
+   elims : string,
+   dests : string}
+
+val no_attrs : facts_prefixes =
+  {usings = "", simps = "", intros = "", elims = "", dests = ""}
+val full_attrs : facts_prefixes =
+  {usings = "", simps = "simp", intros = "intro", elims = "elim", dests = "dest"}
+val clas_attrs : facts_prefixes =
+  {usings = "", simps = "", intros = "intro", elims = "elim", dests = "dest"}
+val simp_attrs : facts_prefixes =
+  {usings = "", simps = "add", intros = "", elims = "", dests = ""}
+val metis_attrs : facts_prefixes = no_attrs
+
+local
+
+fun parse_method ctxt s =
+  enclose "(" ")" s
+  |> Token.explode (Thy_Header.get_keywords' ctxt) Position.start
+  |> filter Token.is_proper
+  |> Scan.read Token.stopper Method.parse
+  |> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source")
+
+fun run_tac timeout_opt tac st =
+  let val with_timeout =
+    (case timeout_opt of SOME timeout => Timeout.apply_physical timeout | NONE => I)
+  in with_timeout (Seq.pull o tac) st |> Option.map fst end
+
+val num_goals = Thm.nprems_of o #goal o Proof.goal
+
+fun apply_recursive recurse elapsed0 timeout_opt apply st =
+  (case Timing.timing (Option.join o try (run_tac timeout_opt apply)) st of
+    ({elapsed, ...}, SOME st') =>
+      if recurse andalso num_goals st' > 0 andalso num_goals st' < num_goals st then
+        let val timeout_opt1 = (Option.map (fn timeout => timeout - elapsed) timeout_opt)
+        in apply_recursive recurse (elapsed0 + elapsed) timeout_opt1 apply st' end
+      else (elapsed0 + elapsed, st')
+   |_ => (elapsed0, st))
+
+in
+
+fun apply_raw_named_method (name : string) all_goals (prefixes: facts_prefixes)
+  (silence_methods : Proof.context -> Proof.context) timeout_opt (facts : Try0.facts)
+  (st : Proof.state) : Try0.result option =
+  let
+    val st = Proof.map_contexts silence_methods st
+    val ctxt = Proof.context_of st
+
+    val (unused_simps, simps_attrs) =
+      if #simps prefixes = "" then
+        (#simps facts, "")
+      else
+        ([], " " ^ #simps prefixes ^ ": " ^ space_implode "" (map string_of_xref (#simps facts)))
+
+    val (unused_intros, intros_attrs) =
+      if #intros prefixes = "" then
+        (#intros facts, "")
+      else
+        ([], " " ^ #intros prefixes ^ ": " ^ space_implode "" (map string_of_xref (#intros facts)))
+
+    val (unused_elims, elims_attrs) =
+      if #elims prefixes = "" then
+        (#elims facts, "")
+      else
+        ([], " " ^ #elims prefixes ^ ": " ^ space_implode "" (map string_of_xref (#elims facts)))
+
+    val (unused_dests, dests_attrs) =
+      if #dests prefixes = "" then
+        (#dests facts, "")
+      else
+        ([], " " ^ #dests prefixes ^ ": " ^ space_implode "" (map string_of_xref (#dests facts)))
+
+    val unused = #usings facts @ unused_simps @ unused_intros @ unused_elims @ unused_dests
+
+    val attrs = simps_attrs ^ intros_attrs ^ elims_attrs ^ dests_attrs
+    val text =
+      name ^ attrs
+      |> parse_method ctxt
+      |> Method.method_cmd ctxt
+      |> Method.Basic
+      |> (fn m => Method.Combinator (Method.no_combinator_info, Method.Select_Goals 1, [m]))
+
+    val apply =
+        Proof.using [Attrib.eval_thms ctxt unused |> map (rpair [] o single)]
+        #> Proof.refine text #> Seq.filter_results
+    val num_before = num_goals st
+    val multiple_goals = all_goals andalso num_before > 1
+    val (time, st') = apply_recursive multiple_goals Time.zeroTime timeout_opt apply st
+    val num_after = num_goals st'
+    val select = "[" ^ string_of_int (num_before - num_after)  ^ "]"
+    val unused = implode_space (unused |> map string_of_xref)
+    val command =
+      (if unused <> "" then "using " ^ unused ^ " " else "") ^
+      (if num_after = 0 then "by " else "apply ") ^
+      (name ^ attrs |> attrs <> "" ? enclose "(" ")") ^
+      (if multiple_goals andalso num_after > 0 then select else "")
+  in
+    if num_before > num_after then
+      SOME {name = name, command = command, time = time, state = st'}
+    else NONE
+  end
+
+end
+
+end
\ No newline at end of file
--- a/src/HOL/Try0.thy	Fri Mar 28 00:26:18 2025 +0000
+++ b/src/HOL/Try0.thy	Fri Mar 28 08:24:07 2025 +0100
@@ -5,10 +5,18 @@
 *)
 
 theory Try0
-  imports Presburger
+  imports Pure
   keywords "try0" :: diag
 begin
 
 ML_file \<open>Tools/try0.ML\<close>
+ML_file \<open>Tools/try0_util.ML\<close>
+
+ML \<open>
+val () =
+  Try0.register_proof_method "simp" {run_if_auto_try = true}
+    (Try0_Util.apply_raw_named_method "simp" false Try0_Util.simp_attrs Simplifier_Trace.disable)
+  handle Symtab.DUP _ => ()
+\<close>
 
 end
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Try0_HOL.thy	Fri Mar 28 08:24:07 2025 +0100
@@ -0,0 +1,65 @@
+(* Title:      HOL/Try0_HOL.thy
+   Author:     Jasmin Blanchette, LMU Muenchen
+   Author:     Martin Desharnais, LMU Muenchen
+   Author:     Fabian Huch, TU Muenchen
+*)
+theory Try0_HOL
+  imports Try0 Presburger
+begin
+
+ML \<open>
+signature TRY0_HOL =
+sig
+  val silence_methods : Proof.context -> Proof.context
+end
+
+structure Try0_HOL : TRY0_HOL = struct
+
+(* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification
+   bound exceeded" warnings and the like. *)
+fun silence_methods ctxt =
+  ctxt
+  |> Config.put Metis_Tactic.verbose false
+  |> Simplifier_Trace.disable
+  |> Context_Position.set_visible false
+  |> Config.put Unify.unify_trace false
+  |> Config.put Argo_Tactic.trace "none"
+
+local
+
+open Try0_Util
+
+(* name * (run_if_auto_try * (all_goals * tags)) *)
+val raw_named_methods =
+  [("auto", (true, (true, full_attrs))),
+   ("blast", (true, (false, clas_attrs))),
+   ("metis", (true, (false, metis_attrs))),
+   ("argo", (true, (false, no_attrs))),
+   ("linarith", (true, (false, no_attrs))),
+   ("presburger", (true, (false, no_attrs))),
+   ("algebra", (true, (false, no_attrs))),
+   ("fast", (false, (false, clas_attrs))),
+   ("fastforce", (false, (false, full_attrs))),
+   ("force", (false, (false, full_attrs))),
+   ("meson", (false, (false, metis_attrs))),
+   ("satx", (false, (false, no_attrs))),
+   ("order", (true, (false, no_attrs)))]
+
+in
+
+val () = raw_named_methods
+  |> List.app (fn (name, (run_if_auto_try, (all_goals, tags))) =>
+    let
+      val meth : Try0.proof_method =
+        Try0_Util.apply_raw_named_method name all_goals tags silence_methods
+    in
+      Try0.register_proof_method name {run_if_auto_try = run_if_auto_try} meth
+      handle Symtab.DUP _ => ()
+    end)
+
+end
+
+end
+\<close>
+
+end
\ No newline at end of file
--- a/src/Tools/try.ML	Fri Mar 28 00:26:18 2025 +0000
+++ b/src/Tools/try.ML	Fri Mar 28 08:24:07 2025 +0100
@@ -20,11 +20,7 @@
 
 (* helpers *)
 
-fun serial_commas _ [] = ["??"]
-  | serial_commas _ [s] = [s]
-  | serial_commas conj [s1, s2] = [s1, conj, s2]
-  | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
-  | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss;
+val serial_commas = Try0.serial_commas
 
 
 (* configuration *)