src/HOL/ex/sledgehammer_tactics.ML
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 44651 5d6a11e166cf
child 45514 973bb7846505
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     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   type relevance_override = Sledgehammer_Filter.relevance_override
    11 
    12   val sledgehammer_with_metis_tac :
    13     Proof.context -> (string * string) list -> relevance_override -> int
    14     -> tactic
    15   val sledgehammer_as_oracle_tac :
    16     Proof.context -> (string * string) list -> relevance_override -> int
    17     -> tactic
    18 end;
    19 
    20 structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
    21 struct
    22 
    23 open Sledgehammer_Filter
    24 
    25 fun run_atp override_params relevance_override i n ctxt goal =
    26   let
    27     val chained_ths = [] (* a tactic has no chained ths *)
    28     val params as {provers, relevance_thresholds, max_relevant, slicing, ...} =
    29       Sledgehammer_Isar.default_params ctxt override_params
    30     val name = hd provers
    31     val prover =
    32       Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name
    33     val default_max_relevant =
    34       Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing name
    35     val is_built_in_const =
    36       Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
    37     val relevance_fudge =
    38       Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
    39     val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
    40     val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
    41     val facts =
    42       Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override
    43                                            chained_ths hyp_ts concl_t
    44       |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
    45              (the_default default_max_relevant max_relevant) is_built_in_const
    46              relevance_fudge relevance_override chained_ths hyp_ts concl_t
    47     val problem =
    48       {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
    49        facts = map Sledgehammer_Provers.Untranslated_Fact facts,
    50        smt_filter = NONE}
    51   in
    52     (case prover params (K (K "")) problem of
    53       {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
    54     | _ => NONE)
    55       handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
    56   end
    57 
    58 fun thms_of_name ctxt name =
    59   let
    60     val lex = Keyword.get_lexicons
    61     val get = maps (Proof_Context.get_fact ctxt o fst)
    62   in
    63     Source.of_string name
    64     |> Symbol.source
    65     |> Token.source {do_recover=SOME false} lex Position.start
    66     |> Token.source_proper
    67     |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
    68     |> Source.exhaust
    69   end
    70 
    71 fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th =
    72   case run_atp override_params relevance_override i i ctxt th of
    73     SOME facts =>
    74     Metis_Tactic.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
    75   | NONE => Seq.empty
    76 
    77 fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th =
    78   let
    79     val thy = Proof_Context.theory_of ctxt
    80     val xs = run_atp (override_params @ [("sound", "true")]) relevance_override
    81                      i i ctxt th
    82   in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
    83 
    84 end;