src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML

more tactics in tactic hammer (from Jasmin)

(*  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 algebraN : string
  val argoN : string
  val autoN : string
  val blastN : string
  val fastforceN : string
  val forceN : string
  val linarithN : string
  val mesonN : string
  val metisN : string
  val orderN : string
  val presburgerN : string
  val satxN : 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 algebraN = "algebra"
val argoN = "argo"
val autoN = "auto"
val blastN = "blast"
val fastforceN = "fastforce"
val forceN = "force"
val linarithN = "linarith"
val mesonN = "meson"
val metisN = "metis"
val orderN = "order"
val presburgerN = "presburger"
val satxN = "satx"
val simpN = "simp"

val tactic_provers =
  [algebraN, argoN, autoN, blastN, fastforceN, forceN, linarithN, mesonN,
   metisN, orderN, presburgerN, satxN, simpN]

val is_tactic_prover = member (op =) tactic_provers

val meshN = "mesh"

fun good_slices_of_tactic_prover _ =
  (* FUDGE *)
  [(1, false, false, 0, meshN),
   (1, false, false, 2, meshN),
   (1, false, false, 8, meshN),
   (1, false, false, 32, meshN)]

fun meth_of name =
  if name = algebraN then Algebra_Method
  else if name = argoN then Argo_Method
  else if name = autoN then Auto_Method
  else if name = blastN then Blast_Method
  else if name = fastforceN then Fastforce_Method
  else if name = forceN then Force_Method
  else if name = linarithN then Linarith_Method
  else if name = mesonN then Meson_Method
  else if name = metisN then Metis_Method (NONE, NONE, [])
  else if name = orderN then Order_Method
  else if name = presburgerN then Presburger_Method
  else if name = satxN then SATx_Method
  else if name = simpN then Simp_Method
  else error ("Unknown tactic: " ^ quote name)

fun tac_of ctxt name (local_facts, global_facts) =
  Sledgehammer_Proof_Methods.tac_of_proof_method ctxt (local_facts, global_facts) (meth_of name)

fun run_tactic_prover mode name ({timeout, ...} : params)
    ({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 {facts = chained, ...} = Proof.goal state
    val ctxt = Proof.context_of state

    val (local_facts, global_facts) =
      ([], [])
      |> fold (fn ((_, (scope, _)), thm) =>
        if scope = Global then apsnd (cons thm)
        else if scope = Chained then I
        else apfst (cons thm)) facts
      |> apfst (append chained)

    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 ((map (apfst Pretty.str) 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;