--- a/src/Tools/auto_solve.ML Mon Oct 25 09:29:43 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,80 +0,0 @@
-(* Title: Tools/auto_solve.ML
- Author: Timothy Bourke and Gerwin Klein, NICTA
-
-Check whether a newly stated theorem can be solved directly by an
-existing theorem. Duplicate lemmas can be detected in this way.
-
-The implementation relies critically on the Find_Theorems solves
-feature.
-*)
-
-signature AUTO_SOLVE =
-sig
- val auto : bool Unsynchronized.ref
- val max_solutions : int Unsynchronized.ref
- val setup : theory -> theory
-end;
-
-structure Auto_Solve : AUTO_SOLVE =
-struct
-
-(* preferences *)
-
-val auto = Unsynchronized.ref false;
-val max_solutions = Unsynchronized.ref 5;
-
-val _ =
- ProofGeneralPgip.add_preference Preferences.category_tracing
- (Unsynchronized.setmp auto true (fn () =>
- Preferences.bool_pref auto
- "auto-solve" "Try to solve conjectures with existing theorems.") ());
-
-
-(* hook *)
-
-fun auto_solve state =
- let
- val ctxt = Proof.context_of state;
-
- val crits = [(true, Find_Theorems.Solves)];
- fun find g = snd (Find_Theorems.find_theorems ctxt (SOME g) (SOME (! max_solutions)) false crits);
-
- fun prt_result (goal, results) =
- let
- val msg =
- (case goal of
- NONE => "The current goal"
- | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));
- in
- Pretty.big_list
- (msg ^ " could be solved directly with:")
- (map (Find_Theorems.pretty_thm ctxt) results)
- end;
-
- fun seek_against_goal () =
- (case try Proof.simple_goal state of
- NONE => NONE
- | SOME {goal = st, ...} =>
- let
- val subgoals = Drule.strip_imp_prems (Thm.cprop_of st);
- val rs =
- if length subgoals = 1
- then [(NONE, find st)]
- else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;
- val results = filter_out (null o snd) rs;
- in if null results then NONE else SOME results end);
-
- fun go () =
- (case try seek_against_goal () of
- SOME (SOME results) =>
- (true, state |> Proof.goal_message
- (fn () => Pretty.chunks
- [Pretty.str "",
- Pretty.markup Markup.hilite
- (separate (Pretty.brk 0) (map prt_result results))]))
- | _ => (false, state));
- in if not (!auto) then (false, state) else go () end;
-
-val setup = Auto_Tools.register_tool ("solve", auto_solve)
-
-end;