|
1 (* Title: Tools/solve_direct.ML |
|
2 Author: Timothy Bourke and Gerwin Klein, NICTA |
|
3 |
|
4 Check whether a newly stated theorem can be solved directly by an |
|
5 existing theorem. Duplicate lemmas can be detected in this way. |
|
6 |
|
7 The implementation relies critically on the Find_Theorems solves |
|
8 feature. |
|
9 *) |
|
10 |
|
11 signature SOLVE_DIRECT = |
|
12 sig |
|
13 val auto : bool Unsynchronized.ref |
|
14 val max_solutions : int Unsynchronized.ref |
|
15 val setup : theory -> theory |
|
16 end; |
|
17 |
|
18 structure Solve_Direct : SOLVE_DIRECT = |
|
19 struct |
|
20 |
|
21 val solve_directN = "solve_direct" |
|
22 |
|
23 (* preferences *) |
|
24 |
|
25 val auto = Unsynchronized.ref false; |
|
26 val max_solutions = Unsynchronized.ref 5; |
|
27 |
|
28 val _ = |
|
29 ProofGeneralPgip.add_preference Preferences.category_tracing |
|
30 (Unsynchronized.setmp auto true (fn () => |
|
31 Preferences.bool_pref auto |
|
32 ("Auto " ^ solve_directN) |
|
33 ("Run " ^ quote solve_directN ^ " automatically.")) ()); |
|
34 |
|
35 fun solve_direct auto state = |
|
36 let |
|
37 val ctxt = Proof.context_of state; |
|
38 |
|
39 val crits = [(true, Find_Theorems.Solves)]; |
|
40 fun find g = snd (Find_Theorems.find_theorems ctxt (SOME g) (SOME (! max_solutions)) false crits); |
|
41 |
|
42 fun prt_result (goal, results) = |
|
43 let |
|
44 val msg = |
|
45 (if auto then "Auto " else "") ^ solve_directN ^ ": " ^ |
|
46 (case goal of |
|
47 NONE => "The current goal" |
|
48 | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg)); |
|
49 in |
|
50 Pretty.big_list |
|
51 (msg ^ " can be solved directly with") |
|
52 (map (Find_Theorems.pretty_thm ctxt) results) |
|
53 end; |
|
54 |
|
55 fun seek_against_goal () = |
|
56 (case try Proof.simple_goal state of |
|
57 NONE => NONE |
|
58 | SOME {goal = st, ...} => |
|
59 let |
|
60 val subgoals = Drule.strip_imp_prems (Thm.cprop_of st); |
|
61 val rs = |
|
62 if length subgoals = 1 |
|
63 then [(NONE, find st)] |
|
64 else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals; |
|
65 val results = filter_out (null o snd) rs; |
|
66 in if null results then NONE else SOME results end); |
|
67 fun message results = separate (Pretty.brk 0) (map prt_result results) |
|
68 in |
|
69 (case try seek_against_goal () of |
|
70 SOME (SOME results) => |
|
71 (true, state |> (if auto then |
|
72 Proof.goal_message |
|
73 (fn () => Pretty.chunks |
|
74 [Pretty.str "", |
|
75 Pretty.markup Markup.hilite (message results)]) |
|
76 else |
|
77 tap (fn _ => priority (Pretty.string_of |
|
78 (Pretty.chunks (message results)))))) |
|
79 | _ => (false, state)) |
|
80 end; |
|
81 |
|
82 val invoke_solve_direct = fst o solve_direct false |
|
83 |
|
84 val _ = |
|
85 Outer_Syntax.improper_command solve_directN |
|
86 "try to solve conjectures directly with existing theorems" Keyword.diag |
|
87 (Scan.succeed (Toplevel.keep (K () o invoke_solve_direct |
|
88 o Toplevel.proof_of))) |
|
89 |
|
90 (* hook *) |
|
91 |
|
92 fun auto_solve_direct state = |
|
93 if not (!auto) then (false, state) else solve_direct true state |
|
94 |
|
95 val setup = Auto_Tools.register_tool (solve_directN, auto_solve_direct) |
|
96 |
|
97 end; |