initial work on Magnushammer-inspured tactic hammer (from Jasmin)

--- a/src/HOL/Sledgehammer.thy	Tue Feb 25 15:54:41 2025 +0100
+++ b/src/HOL/Sledgehammer.thy	Tue Feb 25 17:37:41 2025 +0100
@@ -29,6 +29,7 @@
 ML_file \<open>Tools/Sledgehammer/sledgehammer_prover.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_atp.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_smt.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_tactic.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_prover_minimize.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_mepo.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_mash.ML\<close>

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Feb 25 15:54:41 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Feb 25 17:37:41 2025 +0100
@@ -51,6 +51,7 @@
 open Sledgehammer_ATP_Systems
 open Sledgehammer_Prover
 open Sledgehammer_Prover_ATP
+open Sledgehammer_Prover_Tactic
 open Sledgehammer_Prover_Minimize
 open Sledgehammer_MaSh
 
@@ -437,7 +438,7 @@
         extra_extra0)) =
         ATP_Slice (format0, the_default type_enc0 type_enc, the_default lam_trans0 lam_trans,
           the_default uncurried_aliases0 uncurried_aliases, extra_extra0)
-      | adjust_extra (extra as SMT_Slice _) = extra
+      | adjust_extra extra = extra
 
     fun adjust_slice max_slice_size
         ((slice_size0, abduce0, falsify0, num_facts0, fact_filter0), extra) =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Tue Feb 25 15:54:41 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Tue Feb 25 17:37:41 2025 +0100
@@ -25,6 +25,7 @@
 open Sledgehammer_ATP_Systems
 open Sledgehammer_Prover
 open Sledgehammer_Prover_SMT
+open Sledgehammer_Prover_Tactic
 open Sledgehammer_Prover_Minimize
 open Sledgehammer_MaSh
 open Sledgehammer
@@ -170,7 +171,7 @@
 (* The first ATP of the list is used by Auto Sledgehammer. *)
 fun default_provers_param_value ctxt =
   \<comment> \<open>see also \<^system_option>\<open>sledgehammer_provers\<close>\<close>
-  filter (is_prover_installed ctxt) (smts ctxt @ local_atps)
+  filter (is_prover_installed ctxt) (smt_solvers ctxt @ local_atps @ tactic_provers)
   |> implode_param
 
 fun set_default_raw_param param thy =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Feb 25 15:54:41 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Feb 25 17:37:41 2025 +0100
@@ -160,7 +160,7 @@
           isar_params ()
       in
         if null atp_proof0 then
-          one_line_proof_text ctxt 0 one_line_params
+          one_line_proof_text one_line_params
         else
           let
             val systematic_methods' = insert (op =) (Metis_Method alt_metis_args) systematic_methods
@@ -475,7 +475,7 @@
           in
             (case (num_chained, add_isar_steps (steps_of_isar_proof isar_proof) 0) of
               (0, 1) =>
-              one_line_proof_text ctxt 0
+              one_line_proof_text
                 (if is_less (play_outcome_ord (play_outcome, one_line_play)) then
                    (case isar_proof of
                      Proof {steps = [Prove {qualifiers = [Show], facts = (_, gfs),
@@ -502,7 +502,7 @@
                    else []) @
                   (if do_preplay then [string_of_play_outcome play_outcome] else [])
               in
-                one_line_proof_text ctxt 0 one_line_params ^
+                one_line_proof_text one_line_params ^
                 (if isar_proofs <> NONE orelse (case play_outcome of Played _ => true | _ => false) then
                    "\n\nIsar proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
                    Active.sendback_markup_command
@@ -519,7 +519,7 @@
       (case try generate_proof_text () of
         SOME s => s
       | NONE =>
-        one_line_proof_text ctxt 0 one_line_params ^
+        one_line_proof_text one_line_params ^
         (if isar_proofs = SOME true then "\nWarning: Isar proof construction failed" else ""))
   end
 
@@ -535,7 +535,7 @@
       (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then
      isar_proof_text ctxt debug num_chained isar_proofs smt_proofs isar_params
    else
-     one_line_proof_text ctxt num_chained) one_line_params
+     one_line_proof_text) one_line_params
 
 fun abduce_text ctxt tms =
   "Candidate missing assumption" ^ plural_s (length tms) ^ ":\n" ^

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue Feb 25 15:54:41 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue Feb 25 17:37:41 2025 +0100
@@ -44,7 +44,7 @@
   val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
   val string_of_play_outcome : play_outcome -> string
   val play_outcome_ord : play_outcome ord
-  val one_line_proof_text : Proof.context -> int -> one_line_params -> string
+  val one_line_proof_text : one_line_params -> string
 end;
 
 structure Sledgehammer_Proof_Methods : SLEDGEHAMMER_PROOF_METHODS =
@@ -220,7 +220,7 @@
   | apply_on_subgoal i n = "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
 
 (* FIXME *)
-fun proof_method_command meth i n used_chaineds _(*num_chained*) extras =
+fun proof_method_command meth i n used_chaineds extras =
   let
     val (indirect_facts, direct_facts) =
       if is_proof_method_direct meth then ([], extras) else (extras, [])
@@ -246,11 +246,10 @@
     (* 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) =
+fun one_line_proof_text ((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
+    |> proof_method_command meth subgoal subgoal_count (map fst chained)
     |> (if play = Play_Failed then failed_command_line else try_command_line banner play)
   end
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Tue Feb 25 15:54:41 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Tue Feb 25 17:37:41 2025 +0100
@@ -72,6 +72,7 @@
   datatype prover_slice_extra =
     ATP_Slice of atp_slice
   | SMT_Slice of string list
+  | No_Slice
 
   type prover_slice = base_slice * prover_slice_extra
 
@@ -199,6 +200,7 @@
 datatype prover_slice_extra =
   ATP_Slice of atp_slice
 | SMT_Slice of string list
+| No_Slice
 
 type prover_slice = base_slice * prover_slice_extra
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Tue Feb 25 15:54:41 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Tue Feb 25 17:37:41 2025 +0100
@@ -43,29 +43,35 @@
 open Sledgehammer_Prover
 open Sledgehammer_Prover_ATP
 open Sledgehammer_Prover_SMT
+open Sledgehammer_Prover_Tactic
 
 fun is_prover_supported ctxt =
-  is_atp orf is_smt_prover ctxt
+  is_atp orf is_smt_solver ctxt orf is_tactic_prover
 
 fun is_prover_installed ctxt prover_name =
   if is_atp prover_name then
     let val thy = Proof_Context.theory_of ctxt in
       is_atp_installed thy prover_name
     end
+  else if is_smt_solver ctxt prover_name then
+    is_smt_solver_installed ctxt prover_name
   else
-    is_smt_prover_installed ctxt prover_name
+    true
 
 fun get_prover ctxt mode name =
   if is_atp name then run_atp mode name
-  else if is_smt_prover ctxt name then run_smt_solver mode name
+  else if is_smt_solver ctxt name then run_smt_solver mode name
+  else if is_tactic_prover name then run_tactic_prover mode name
   else error ("No such prover: " ^ name)
 
 fun get_slices ctxt name =
   let val thy = Proof_Context.theory_of ctxt in
     if is_atp name then
       map (apsnd ATP_Slice) (#good_slices (get_atp thy name ()) ctxt)
-    else if is_smt_prover ctxt name then
+    else if is_smt_solver ctxt name then
       map (apsnd SMT_Slice) (SMT_Solver.good_slices ctxt name)
+    else if is_tactic_prover name then
+      map (rpair No_Slice) (good_slices_of_tactic_prover name)
     else
       error ("No such prover: " ^ name)
   end

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Tue Feb 25 15:54:41 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Tue Feb 25 17:37:41 2025 +0100
@@ -15,11 +15,11 @@
   val smt_builtins : bool Config.T
   val smt_triggers : bool Config.T
 
-  val is_smt_prover : Proof.context -> string -> bool
-  val is_smt_prover_installed : Proof.context -> string -> bool
+  val is_smt_solver : Proof.context -> string -> bool
+  val is_smt_solver_installed : Proof.context -> string -> bool
   val run_smt_solver : mode -> string -> prover
 
-  val smts : Proof.context -> string list
+  val smt_solvers : Proof.context -> string list
 end;
 
 structure Sledgehammer_Prover_SMT : SLEDGEHAMMER_PROVER_SMT =
@@ -38,10 +38,10 @@
 val smt_builtins = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_smt_builtins\<close> (K true)
 val smt_triggers = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_smt_triggers\<close> (K true)
 
-val smts = sort_strings o SMT_Config.all_solvers_of
+val smt_solvers = sort_strings o SMT_Config.all_solvers_of
 
-val is_smt_prover = member (op =) o smts
-val is_smt_prover_installed = member (op =) o SMT_Config.available_solvers_of
+val is_smt_solver = member (op =) o smt_solvers
+val is_smt_solver_installed = member (op =) o SMT_Config.available_solvers_of
 
 (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out
    properly in the SMT module, we must interpret these here. *)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML	Tue Feb 25 17:37:41 2025 +0100
@@ -0,0 +1,126 @@
+(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML
+    Author:     Jasmin Blanchette, LMU Muenchen
+
+Isabelle tactics as Sledgehammer provers.
+*)
+
+signature SLEDGEHAMMER_PROVER_TACTIC =
+sig
+  type stature = ATP_Problem_Generate.stature
+  type mode = Sledgehammer_Prover.mode
+  type prover = Sledgehammer_Prover.prover
+  type base_slice = Sledgehammer_ATP_Systems.base_slice
+
+  val autoN : string
+  val blastN : string
+  val simpN : string
+
+  val tactic_provers : string list
+  val is_tactic_prover : string -> bool
+  val good_slices_of_tactic_prover : string -> base_slice list
+  val run_tactic_prover : mode -> string -> prover
+end;
+
+structure Sledgehammer_Prover_Tactic : SLEDGEHAMMER_PROVER_TACTIC =
+struct
+
+open ATP_Problem_Generate
+open ATP_Proof
+open Sledgehammer_ATP_Systems
+open Sledgehammer_Proof_Methods
+open Sledgehammer_Prover
+
+val autoN = "auto"
+val blastN = "blast"
+val simpN = "simp"
+
+val tactic_provers = [autoN, blastN, simpN]
+
+val is_tactic_prover = member (op =) tactic_provers
+
+val meshN = "mesh"
+
+fun good_slices_of_tactic_prover name =
+  (* FUDGE *)
+  if name = simpN then
+    [(1, false, false, 0, meshN),
+     (1, false, false, 2, meshN),
+     (1, false, false, 8, meshN),
+     (1, false, false, 32, meshN),
+     (1, false, false, 128, meshN)]
+  else
+    [(1, false, false, 0, meshN),
+     (1, false, false, 1, meshN),
+     (1, false, false, 2, meshN),
+     (1, false, false, 4, meshN),
+     (1, false, false, 8, meshN)]
+
+(* In sync with Sledgehammer_Proof_Methods.tac_of_proof_method *)
+fun tac_of ctxt name (local_facts, global_facts) =
+  if name = autoN then
+    Method.insert_tac ctxt (local_facts @ global_facts) THEN'
+    SELECT_GOAL (Clasimp.auto_tac ctxt)
+  else if name = blastN then
+    Method.insert_tac ctxt (local_facts @ global_facts) THEN'
+    blast_tac ctxt
+  else if name = simpN then
+    Method.insert_tac ctxt local_facts THEN'
+    Simplifier.asm_full_simp_tac (ctxt addsimps global_facts)
+  else
+    error ("Unknown tactic: " ^ quote name)
+
+fun meth_of name =
+  if name = autoN then
+    Auto_Method
+  else if name = blastN then
+    Blast_Method
+  else if name = simpN then
+    Simp_Method
+  else
+    error ("Unknown tactic: " ^ quote name)
+
+fun run_tactic_prover mode name (params as {debug, verbose, isar_proofs, compress, try0, minimize,
+     timeout, ...})
+    ({state, goal, subgoal, subgoal_count, factss, found_something, ...} : prover_problem)
+    slice =
+  let
+    val (basic_slice, No_Slice) = slice
+    val facts = facts_of_basic_slice basic_slice factss
+    val ctxt = Proof.context_of state
+
+    val (local_facts, global_facts) =
+      fold (fn fact => if fst (snd (fst fact)) = Global then apsnd (cons (snd fact))
+        else apfst (cons (snd fact))) facts ([], [])
+
+    val timer = Timer.startRealTimer ()
+
+    val out =
+      (Timeout.apply timeout
+         (Goal.prove ctxt [] [] (Logic.get_goal (Thm.prop_of goal) subgoal))
+         (fn {context = ctxt, ...} =>
+            HEADGOAL (tac_of ctxt name (local_facts, global_facts)));
+       NONE)
+      handle ERROR _ => SOME GaveUp
+           | Timeout.TIMEOUT _ => SOME TimedOut
+
+    val run_time = Timer.checkRealTimer timer
+
+    val (outcome, used_facts) =
+      (case out of
+        NONE =>
+        (found_something name;
+         (NONE, map fst facts))
+      | some_failure => (some_failure, []))
+
+    val message = fn _ =>
+      (case outcome of
+        NONE =>
+        one_line_proof_text ((used_facts, (meth_of name, Played run_time)), proof_banner mode name,
+          subgoal, subgoal_count)
+      | SOME failure => string_of_atp_failure failure)
+  in
+    {outcome = outcome, used_facts = used_facts, used_from = facts,
+     preferred_methss = (meth_of name, []), run_time = run_time, message = message}
+  end
+
+end;