(*  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;