1.1 --- a/src/Tools/auto_solve.ML	Tue Mar 31 21:31:23 2009 +0200
     1.2 +++ b/src/Tools/auto_solve.ML	Tue Mar 31 22:23:33 2009 +0200
     1.3 @@ -1,11 +1,11 @@
     1.4 -(*  Title:      Pure/Tools/auto_solve.ML
     1.5 +(*  Title:      Tools/auto_solve.ML
     1.6      Author:     Timothy Bourke and Gerwin Klein, NICTA
     1.7  
     1.8  Check whether a newly stated theorem can be solved directly by an
     1.9 -existing theorem. Duplicate lemmas can be detected in this way.
    1.10 +existing theorem.  Duplicate lemmas can be detected in this way.
    1.11  
    1.12 -The implemenation is based in part on Berghofer and Haftmann's
    1.13 -Pure/codegen.ML. It relies critically on the FindTheorems solves
    1.14 +The implementation is based in part on Berghofer and Haftmann's
    1.15 +quickcheck.ML.  It relies critically on the FindTheorems solves
    1.16  feature.
    1.17  *)
    1.18  
    1.19 @@ -29,24 +29,15 @@
    1.20    let
    1.21      val ctxt = Proof.context_of state;
    1.22  
    1.23 -    fun conj_to_list [] = []
    1.24 -      | conj_to_list (t::ts) =
    1.25 -        (Conjunction.dest_conjunction t
    1.26 -         |> (fn (t1, t2) => conj_to_list (t1::t2::ts)))
    1.27 -        handle TERM _ => t::conj_to_list ts;
    1.28 -
    1.29      val crits = [(true, FindTheorems.Solves)];
    1.30 -    fun find g = (NONE, snd (FindTheorems.find_theorems ctxt g (SOME (! limit)) false crits));
    1.31 -    fun find_cterm g =
    1.32 -      (SOME g, snd (FindTheorems.find_theorems ctxt
    1.33 -          (SOME (Goal.init g)) (SOME (! limit)) false crits));
    1.34 +    fun find g = snd (FindTheorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits);
    1.35  
    1.36      fun prt_result (goal, results) =
    1.37        let
    1.38          val msg =
    1.39            (case goal of
    1.40              NONE => "The current goal"
    1.41 -          | SOME g => Syntax.string_of_term ctxt (Thm.term_of g));
    1.42 +          | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));
    1.43        in
    1.44          Pretty.big_list
    1.45            (msg ^ " could be solved directly with:")
    1.46 @@ -54,22 +45,17 @@
    1.47        end;
    1.48  
    1.49      fun seek_against_goal () =
    1.50 -      let
    1.51 -        val goal = try Proof.get_goal state
    1.52 -          |> Option.map (#2 o #2);
    1.53 -
    1.54 -        val goals = goal
    1.55 -          |> Option.map (fn g => cprem_of g 1)
    1.56 -          |> the_list
    1.57 -          |> conj_to_list;
    1.58 -
    1.59 -        val rs =
    1.60 -          if length goals = 1
    1.61 -          then [find goal]
    1.62 -          else map find_cterm goals;
    1.63 -        val results = filter_out (null o snd) rs;
    1.64 -
    1.65 -      in if null results then NONE else SOME results end;
    1.66 +      (case try Proof.get_goal state of
    1.67 +        NONE => NONE
    1.68 +      | SOME (_, (_, goal)) =>
    1.69 +          let
    1.70 +            val subgoals = Conjunction.dest_conjunctions (Thm.cprem_of goal 1);
    1.71 +            val rs =
    1.72 +              if length subgoals = 1
    1.73 +              then [(NONE, find goal)]
    1.74 +              else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;
    1.75 +            val results = filter_out (null o snd) rs;
    1.76 +          in if null results then NONE else SOME results end);
    1.77  
    1.78      fun go () =
    1.79        let
    1.80 @@ -84,7 +70,7 @@
    1.81                  [Pretty.str "",
    1.82                    Pretty.markup Markup.hilite
    1.83                      (separate (Pretty.brk 0) (map prt_result results))])
    1.84 -        | NONE => state)
    1.85 +        | _ => state)
    1.86        end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state);
    1.87    in
    1.88      if int andalso ! auto andalso not (! Toplevel.quiet)