src/HOL/ex/sledgehammer_tactics.ML
author blanchet
Tue Aug 23 18:42:05 2011 +0200 (2011-08-23)
changeset 44429 e5506cfe1b5a
parent 44390 99ef9fd7341b
child 44462 d9a657c44380
permissions -rw-r--r--
clean up Sledgehammer tactic
     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 :
    11     Proof.context -> (string * string) list -> int -> tactic
    12   val sledgehammer_as_oracle_tac :
    13     Proof.context -> (string * string) list -> int -> tactic
    14 end;
    15 
    16 structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
    17 struct
    18 
    19 fun run_atp override_params i n ctxt goal =
    20   let
    21     val chained_ths = [] (* a tactic has no chained ths *)
    22     val params as {provers, relevance_thresholds, max_relevant, slicing, ...} =
    23       Sledgehammer_Isar.default_params ctxt override_params
    24     val name = hd provers
    25     val prover =
    26       Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal 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) = ATP_Util.strip_subgoal ctxt goal i
    35     val facts =
    36       Sledgehammer_Filter.nearly_all_facts ctxt relevance_override chained_ths
    37                                            hyp_ts concl_t
    38       |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
    39              (the_default default_max_relevant max_relevant) is_built_in_const
    40              relevance_fudge relevance_override chained_ths hyp_ts concl_t
    41     val problem =
    42       {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
    43        facts = map Sledgehammer_Provers.Untranslated_Fact facts,
    44        smt_filter = NONE}
    45   in
    46     (case prover params (K (K "")) problem of
    47       {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
    48     | _ => NONE)
    49       handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
    50   end
    51 
    52 fun thms_of_name ctxt name =
    53   let
    54     val lex = Keyword.get_lexicons
    55     val get = maps (Proof_Context.get_fact ctxt o fst)
    56   in
    57     Source.of_string name
    58     |> Symbol.source
    59     |> Token.source {do_recover=SOME false} lex Position.start
    60     |> Token.source_proper
    61     |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
    62     |> Source.exhaust
    63   end
    64 
    65 fun sledgehammer_with_metis_tac ctxt override_params i th =
    66   case run_atp override_params i i ctxt th of
    67     SOME facts =>
    68     Metis_Tactics.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
    69   | NONE => Seq.empty
    70 
    71 fun sledgehammer_as_oracle_tac ctxt override_params i th =
    72   let
    73     val thy = Proof_Context.theory_of ctxt
    74     val xs = run_atp (override_params @ [("sound", "true")]) i i ctxt th
    75   in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
    76 
    77 end;