1 (* Title: Tools/solve_direct.ML
2 Author: Timothy Bourke and Gerwin Klein, NICTA
4 Check whether a newly stated theorem can be solved directly by an
5 existing theorem. Duplicate lemmas can be detected in this way.
7 The implementation relies critically on the Find_Theorems solves
11 signature SOLVE_DIRECT =
13 val auto : bool Unsynchronized.ref
14 val max_solutions : int Unsynchronized.ref
15 val setup : theory -> theory
18 structure Solve_Direct : SOLVE_DIRECT =
21 val solve_directN = "solve_direct"
25 val auto = Unsynchronized.ref false;
26 val max_solutions = Unsynchronized.ref 5;
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.")) ());
35 fun solve_direct auto state =
37 val ctxt = Proof.context_of state;
39 val crits = [(true, Find_Theorems.Solves)];
40 fun find g = snd (Find_Theorems.find_theorems ctxt (SOME g) (SOME (! max_solutions)) false crits);
42 fun prt_result (goal, results) =
45 (if auto then "Auto " else "") ^ solve_directN ^ ": " ^
47 NONE => "The current goal"
48 | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));
51 (msg ^ " can be solved directly with")
52 (map (Find_Theorems.pretty_thm ctxt) results)
55 fun seek_against_goal () =
56 (case try Proof.simple_goal state of
58 | SOME {goal = st, ...} =>
60 val subgoals = Drule.strip_imp_prems (Thm.cprop_of st);
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)
69 (case try seek_against_goal () of
70 SOME (SOME results) =>
71 (true, state |> (if auto then
73 (fn () => Pretty.chunks
75 Pretty.markup Markup.hilite (message results)])
77 tap (fn _ => priority (Pretty.string_of
78 (Pretty.chunks (message results))))))
79 | _ => (false, state))
82 val invoke_solve_direct = fst o solve_direct false
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)))
92 fun auto_solve_direct state =
93 if not (!auto) then (false, state) else solve_direct true state
95 val setup = Auto_Tools.register_tool (solve_directN, auto_solve_direct)