# HG changeset patch
# User paulson
# Date 1740750638 0
# Node ID dd28f282ddc294cb59b7855f75f6ae7f192f68d6
# Parent  24d83211de9a1a9c04949f47f31fb892b70084df# Parent  cbf9f856d3e000c6dcc99e8f965e8e7f8102e444
merged

diff -r cbf9f856d3e0 -r dd28f282ddc2 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Fri Feb 28 13:50:18 2025 +0000
+++ b/src/HOL/Tools/try0.ML	Fri Feb 28 13:50:38 2025 +0000
@@ -11,6 +11,8 @@
   type xthm = Facts.ref * Token.src list
   type tagged_xthm = xthm * modifier list
   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
 end
 
@@ -66,47 +68,7 @@
 
 type result = {name: string, command: string, time: Time.time, state: Proof.state}
 
-fun apply_named_method (name, ((all_goals, run_if_auto_try), attrs)) mode timeout_opt tagged st :
-  result option =
-  if mode <> Auto_Try orelse run_if_auto_try then
-    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
-  else NONE
+local
 
 val full_attrs = [(Simp, "simp"), (Intro, "intro"), (Elim, "elim"), (Dest, "dest")]
 val clas_attrs = [(Intro, "intro"), (Elim, "elim"), (Dest, "dest")]
@@ -115,7 +77,7 @@
 val no_attrs = []
 
 (* name * ((all_goals, run_if_auto_try), tags *)
-val named_methods =
+val raw_named_methods =
   [("simp", ((false, true), simp_attrs)),
    ("auto", ((true, true), full_attrs)),
    ("blast", ((false, true), clas_attrs)),
@@ -131,7 +93,69 @@
    ("satx", ((false, false), no_attrs)),
    ("order", ((false, true), no_attrs))]
 
-val apply_methods = map apply_named_method named_methods
+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
+
+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 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)
+
+end
+
+val maybe_apply_methods = map maybe_apply_proof_method named_methods
 
 fun time_string time = string_of_int (Time.toMilliseconds time) ^ " ms"
 fun tool_time_string (s, time) = s ^ ": " ^ time_string time
@@ -166,12 +190,12 @@
         |> the_list
   in
     if mode = Normal then
-      "Trying " ^ implode_space (Try.serial_commas "and" (map (quote o fst) named_methods)) ^
+      "Trying " ^ implode_space (Try.serial_commas "and" (map quote named_methods)) ^
       "..."
       |> writeln
     else
       ();
-    (case get_results apply_methods of
+    (case get_results maybe_apply_methods of
       [] => (if mode = Normal then writeln "No proof found" else (); ((false, (noneN, [])), []))
     | results as {name, command, ...} :: _ =>
       let