src/HOL/TPTP/sledgehammer_tactics.ML
author wenzelm
Sun Sep 18 20:33:48 2016 +0200 (2016-09-18)
changeset 63915 bab633745c7f
parent 62738 fe827c6fa8c5
permissions -rw-r--r--
tuned proofs;
blanchet@47790
     1
(*  Title:      HOL/TPTP/sledgehammer_tactics.ML
bulwahn@40633
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@42071
     3
    Copyright   2010, 2011
bulwahn@40633
     4
bulwahn@40633
     5
Sledgehammer as a tactic.
bulwahn@40633
     6
*)
bulwahn@40633
     7
bulwahn@40633
     8
signature SLEDGEHAMMER_TACTICS =
bulwahn@40633
     9
sig
blanchet@48292
    10
  type fact_override = Sledgehammer_Fact.fact_override
blanchet@44462
    11
blanchet@57754
    12
  val sledgehammer_with_metis_tac : Proof.context -> (string * string) list -> fact_override ->
blanchet@57812
    13
    thm list -> int -> tactic
blanchet@57754
    14
  val sledgehammer_as_oracle_tac : Proof.context -> (string * string) list -> fact_override ->
blanchet@57812
    15
    thm list -> int -> tactic
bulwahn@40633
    16
end;
bulwahn@40633
    17
bulwahn@40633
    18
structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
bulwahn@40633
    19
struct
blanchet@42071
    20
blanchet@48299
    21
open Sledgehammer_Util
blanchet@48287
    22
open Sledgehammer_Fact
blanchet@55201
    23
open Sledgehammer_Prover
blanchet@55212
    24
open Sledgehammer_Prover_ATP
blanchet@55205
    25
open Sledgehammer_Prover_Minimize
blanchet@48381
    26
open Sledgehammer_MaSh
blanchet@55198
    27
open Sledgehammer_Commands
blanchet@44462
    28
blanchet@57812
    29
fun run_prover override_params fact_override chained i n ctxt goal =
bulwahn@40633
    30
  let
blanchet@55205
    31
    val thy = Proof_Context.theory_of ctxt
blanchet@48299
    32
    val mode = Normal
blanchet@55205
    33
    val params as {provers, max_facts, ...} = default_params thy override_params
blanchet@44429
    34
    val name = hd provers
blanchet@48299
    35
    val prover = get_prover ctxt mode name
blanchet@54126
    36
    val default_max_facts = default_max_facts_of_prover ctxt name
blanchet@52196
    37
    val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt
blanchet@48299
    38
    val ho_atp = exists (is_ho_atp ctxt) provers
wenzelm@58928
    39
    val keywords = Thy_Header.get_keywords' ctxt
blanchet@48299
    40
    val css_table = clasimpset_rule_table_of ctxt
bulwahn@40921
    41
    val facts =
wenzelm@58921
    42
      nearly_all_facts ctxt ho_atp fact_override keywords css_table chained hyp_ts concl_t
blanchet@57812
    43
      |> relevant_facts ctxt params name (the_default default_max_facts max_facts) fact_override
blanchet@57812
    44
        hyp_ts concl_t
blanchet@51010
    45
      |> hd |> snd
bulwahn@40633
    46
    val problem =
blanchet@54141
    47
      {comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
blanchet@62738
    48
       factss = [("", facts)], found_proof = I}
bulwahn@40633
    49
  in
blanchet@57754
    50
    (case prover params problem of
bulwahn@40921
    51
      {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
bulwahn@40921
    52
    | _ => NONE)
blanchet@51010
    53
    handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
bulwahn@40633
    54
  end
bulwahn@40633
    55
blanchet@57812
    56
fun sledgehammer_with_metis_tac ctxt override_params fact_override chained i th =
blanchet@48292
    57
  let val override_params = override_params @ [("preplay_timeout", "0")] in
blanchet@57812
    58
    (case run_prover override_params fact_override chained i i ctxt th of
blanchet@47766
    59
      SOME facts =>
blanchet@47766
    60
      Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt
blanchet@57812
    61
        (maps (thms_of_name ctxt) facts) i th
blanchet@57812
    62
    | NONE => Seq.empty)
blanchet@47766
    63
  end
bulwahn@40633
    64
blanchet@57812
    65
fun sledgehammer_as_oracle_tac ctxt override_params fact_override chained i th =
bulwahn@40633
    66
  let
blanchet@47766
    67
    val override_params =
blanchet@47766
    68
      override_params @
blanchet@47766
    69
      [("preplay_timeout", "0"),
blanchet@47766
    70
       ("minimize", "false")]
blanchet@57812
    71
    val xs = run_prover override_params fact_override chained i i ctxt th
blanchet@57812
    72
  in
wenzelm@59498
    73
    if is_some xs then ALLGOALS (Skip_Proof.cheat_tac ctxt) th else Seq.empty
blanchet@57812
    74
  end
blanchet@41357
    75
bulwahn@40633
    76
end;