src/HOL/ex/sledgehammer_tactics.ML
author blanchet
Sun May 22 14:51:42 2011 +0200 (2011-05-22)
changeset 42944 9e620869a576
parent 42642 f5b4b9d4acda
child 43004 20e9caff1f86
permissions -rw-r--r--
improved Waldmeister support -- even run it by default on unit equational goals
     1 (*  Title:      HOL/ex/sledgehammer_tactics.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2010, 2011
     4 
     5 Sledgehammer as a tactic.
     6 *)
     7 
     8 signature SLEDGEHAMMER_TACTICS =
     9 sig
    10   val sledgehammer_with_metis_tac : Proof.context -> int -> tactic
    11   val sledgehammer_as_unsound_oracle_tac : Proof.context -> int -> tactic
    12   val sledgehammer_as_oracle_tac : Proof.context -> int -> tactic
    13 end;
    14 
    15 structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
    16 struct
    17 
    18 fun run_atp force_full_types timeout i n ctxt goal name =
    19   let
    20     val chained_ths = [] (* a tactic has no chained ths *)
    21     val params as {relevance_thresholds, max_relevant, slicing, ...} =
    22       ((if force_full_types then [("full_types", "true")] else [])
    23        @ [("timeout", string_of_int (Time.toSeconds timeout))])
    24        (* @ [("overlord", "true")] *)
    25       |> Sledgehammer_Isar.default_params ctxt
    26     val prover = Sledgehammer_Provers.get_prover ctxt false name
    27     val default_max_relevant =
    28       Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing name
    29     val is_built_in_const =
    30       Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
    31     val relevance_fudge =
    32       Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
    33     val relevance_override = {add = [], del = [], only = false}
    34     val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
    35     val facts =
    36       Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
    37           (the_default default_max_relevant max_relevant) (K true)
    38           is_built_in_const relevance_fudge relevance_override chained_ths
    39           hyp_ts concl_t
    40     val problem =
    41       {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
    42        facts = map Sledgehammer_Provers.Untranslated_Fact facts,
    43        smt_filter = NONE}
    44   in
    45     (case prover params (K "") problem of
    46       {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
    47     | _ => NONE)
    48       handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
    49   end
    50 
    51 val atp = "e" (* or "vampire" or "spass" etc. *)
    52 
    53 fun thms_of_name ctxt name =
    54   let
    55     val lex = Keyword.get_lexicons
    56     val get = maps (Proof_Context.get_fact ctxt o fst)
    57   in
    58     Source.of_string name
    59     |> Symbol.source
    60     |> Token.source {do_recover=SOME false} lex Position.start
    61     |> Token.source_proper
    62     |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
    63     |> Source.exhaust
    64   end
    65 
    66 fun sledgehammer_with_metis_tac ctxt i th =
    67   let
    68     val timeout = Time.fromSeconds 30
    69   in
    70     case run_atp false timeout i i ctxt th atp of
    71       SOME facts =>
    72       Metis_Tactics.metis_tac ctxt (maps (thms_of_name ctxt) facts) i th
    73     | NONE => Seq.empty
    74   end
    75 
    76 fun generic_sledgehammer_as_oracle_tac force_full_types ctxt i th =
    77   let
    78     val thy = Proof_Context.theory_of ctxt
    79     val timeout = Time.fromSeconds 30
    80     val xs = run_atp force_full_types timeout i i ctxt th atp
    81   in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
    82 
    83 val sledgehammer_as_unsound_oracle_tac =
    84   generic_sledgehammer_as_oracle_tac false
    85 val sledgehammer_as_oracle_tac = generic_sledgehammer_as_oracle_tac true
    86 
    87 end;