5 Sledgehammer as a tactic. |
5 Sledgehammer as a tactic. |
6 *) |
6 *) |
7 |
7 |
8 signature SLEDGEHAMMER_TACTICS = |
8 signature SLEDGEHAMMER_TACTICS = |
9 sig |
9 sig |
|
10 type relevance_override = Sledgehammer_Filter.relevance_override |
|
11 |
10 val sledgehammer_with_metis_tac : |
12 val sledgehammer_with_metis_tac : |
11 Proof.context -> (string * string) list -> int -> tactic |
13 Proof.context -> (string * string) list -> relevance_override -> int |
|
14 -> tactic |
12 val sledgehammer_as_oracle_tac : |
15 val sledgehammer_as_oracle_tac : |
13 Proof.context -> (string * string) list -> int -> tactic |
16 Proof.context -> (string * string) list -> relevance_override -> int |
|
17 -> tactic |
14 end; |
18 end; |
15 |
19 |
16 structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS = |
20 structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS = |
17 struct |
21 struct |
18 |
22 |
19 fun run_atp override_params i n ctxt goal = |
23 open Sledgehammer_Filter |
|
24 |
|
25 fun run_atp override_params relevance_override i n ctxt goal = |
20 let |
26 let |
21 val chained_ths = [] (* a tactic has no chained ths *) |
27 val chained_ths = [] (* a tactic has no chained ths *) |
22 val params as {provers, relevance_thresholds, max_relevant, slicing, ...} = |
28 val params as {provers, relevance_thresholds, max_relevant, slicing, ...} = |
23 Sledgehammer_Isar.default_params ctxt override_params |
29 Sledgehammer_Isar.default_params ctxt override_params |
24 val name = hd provers |
30 val name = hd provers |
28 Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing name |
34 Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing name |
29 val is_built_in_const = |
35 val is_built_in_const = |
30 Sledgehammer_Provers.is_built_in_const_for_prover ctxt name |
36 Sledgehammer_Provers.is_built_in_const_for_prover ctxt name |
31 val relevance_fudge = |
37 val relevance_fudge = |
32 Sledgehammer_Provers.relevance_fudge_for_prover ctxt name |
38 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 |
39 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i |
35 val facts = |
40 val facts = |
36 Sledgehammer_Filter.nearly_all_facts ctxt relevance_override chained_ths |
41 Sledgehammer_Filter.nearly_all_facts ctxt relevance_override chained_ths |
37 hyp_ts concl_t |
42 hyp_ts concl_t |
38 |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds |
43 |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds |
60 |> Token.source_proper |
65 |> Token.source_proper |
61 |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE |
66 |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE |
62 |> Source.exhaust |
67 |> Source.exhaust |
63 end |
68 end |
64 |
69 |
65 fun sledgehammer_with_metis_tac ctxt override_params i th = |
70 fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th = |
66 case run_atp override_params i i ctxt th of |
71 case run_atp override_params relevance_override i i ctxt th of |
67 SOME facts => |
72 SOME facts => |
68 Metis_Tactics.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th |
73 Metis_Tactics.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th |
69 | NONE => Seq.empty |
74 | NONE => Seq.empty |
70 |
75 |
71 fun sledgehammer_as_oracle_tac ctxt override_params i th = |
76 fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th = |
72 let |
77 let |
73 val thy = Proof_Context.theory_of ctxt |
78 val thy = Proof_Context.theory_of ctxt |
74 val xs = run_atp (override_params @ [("sound", "true")]) i i ctxt th |
79 val xs = run_atp (override_params @ [("sound", "true")]) relevance_override |
|
80 i i ctxt th |
75 in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end |
81 in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end |
76 |
82 |
77 end; |
83 end; |