1 (* Title: HOL/ex/sledgehammer_tactics.ML
2 Author: Jasmin Blanchette, TU Muenchen
5 Sledgehammer as a tactic.
8 signature SLEDGEHAMMER_TACTICS =
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
16 structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
19 fun run_atp override_params i n ctxt goal =
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
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
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
36 Sledgehammer_Filter.nearly_all_facts ctxt relevance_override chained_ths
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
42 {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
43 facts = map Sledgehammer_Provers.Untranslated_Fact facts,
46 (case prover params (K (K "")) problem of
47 {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
49 handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
52 fun thms_of_name ctxt name =
54 val lex = Keyword.get_lexicons
55 val get = maps (Proof_Context.get_fact ctxt o fst)
59 |> Token.source {do_recover=SOME false} lex Position.start
60 |> Token.source_proper
61 |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
65 fun sledgehammer_with_metis_tac ctxt override_params i th =
66 case run_atp override_params i i ctxt th of
68 Metis_Tactics.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th
71 fun sledgehammer_as_oracle_tac ctxt override_params i th =
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