# HG changeset patch
# User blanchet
# Date 1288199673 -7200
# Node ID cd6d2b0a40962dbee55e62eb6938a093ccddd4cd
# Parent  d10b68c6e6d4c186144c908b9de0205a6bbcd90f
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)

diff -r d10b68c6e6d4 -r cd6d2b0a4096 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Oct 27 16:32:13 2010 +0200
+++ b/src/HOL/HOL.thy	Wed Oct 27 19:14:33 2010 +0200
@@ -1978,11 +1978,9 @@
 *} "solve goal by normalization"
 
 
-(*
 subsection {* Try *}
 
 setup {* Try.setup *}
-*)
 
 subsection {* Counterexample Search Units *}
 
diff -r d10b68c6e6d4 -r cd6d2b0a4096 src/HOL/Tools/try.ML
--- a/src/HOL/Tools/try.ML	Wed Oct 27 16:32:13 2010 +0200
+++ b/src/HOL/Tools/try.ML	Wed Oct 27 19:14:33 2010 +0200
@@ -2,33 +2,23 @@
     Author:     Jasmin Blanchette, TU Muenchen
 
 Try a combination of proof methods.
-
-FIXME: reintroduce or remove commented code (see also HOL.thy)
 *)
 
 signature TRY =
 sig
-(*
   val auto : bool Unsynchronized.ref
-*)
   val invoke_try : Time.time option -> Proof.state -> bool
-(*
   val setup : theory -> theory
-*)
 end;
 
 structure Try : TRY =
 struct
 
-(*
 val auto = Unsynchronized.ref false
 
 val _ =
   ProofGeneralPgip.add_preference Preferences.category_tracing
-  (Unsynchronized.setmp auto true (fn () =>
-    Preferences.bool_pref auto
-      "auto-try" "Try standard proof methods.") ());
-*)
+      (Preferences.bool_pref auto "auto-try" "Try standard proof methods.")
 
 val default_timeout = Time.fromSeconds 5
 
@@ -57,26 +47,37 @@
   let val thy = ProofContext.theory_of ctxt in
     Proof.refine (Method.SelectGoals (1, Method.Basic (named_method thy name)))
   end
+  handle ERROR _ => K Seq.empty (* e.g., the method isn't available yet *)
 
-fun do_named_method (name, all_goals) timeout_opt st =
-  do_generic timeout_opt
-             (name ^ (if all_goals andalso
-                         nprems_of (#goal (Proof.goal st)) > 1 then
-                        "[1]"
-                      else
-                        "")) I (#goal o Proof.goal)
-             (apply_named_method_on_first_goal name (Proof.context_of st)) st
+fun do_named_method (name, (all_goals, run_if_auto)) auto timeout_opt st =
+  if not auto orelse run_if_auto then
+    do_generic timeout_opt
+               (name ^ (if all_goals andalso
+                           nprems_of (#goal (Proof.goal st)) > 1 then
+                          "[1]"
+                        else
+                          "")) I (#goal o Proof.goal)
+               (apply_named_method_on_first_goal name (Proof.context_of st)) st
+  else
+    NONE
 
+(* name * (all_goals, run_if_auto) *)
 val named_methods =
-  [("simp", false), ("auto", true), ("fast", false), ("fastsimp", false),
-   ("force", false), ("blast", false), ("metis", false), ("linarith", false),
-   ("presburger", false)]
+  [("simp", (false, true)),
+   ("auto", (true, true)),
+   ("fast", (false, false)),
+   ("fastsimp", (false, false)),
+   ("force", (false, false)),
+   ("blast", (false, true)),
+   ("metis", (false, true)),
+   ("linarith", (false, true)),
+   ("presburger", (false, true))]
 val do_methods = map do_named_method named_methods
 
 fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
 
 fun do_try auto timeout_opt st =
-  case do_methods |> Par_List.map (fn f => f timeout_opt st)
+  case do_methods |> Par_List.map (fn f => f auto timeout_opt st)
                   |> map_filter I |> sort (int_ord o pairself snd) of
     [] => (if auto then () else writeln "No proof found."; (false, st))
   | xs as (s, _) :: _ =>
@@ -88,7 +89,7 @@
         Markup.markup Markup.sendback
             ((if nprems_of (#goal (Proof.goal st)) = 1 then "by" else "apply") ^
              " " ^ s) ^
-        ".\n(" ^ space_implode "; " (map time_string xs) ^ ")\n"
+        "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
     in
       (true, st |> (if auto then
                       Proof.goal_message
@@ -109,10 +110,8 @@
       (Scan.succeed (Toplevel.keep (K () o do_try false (SOME default_timeout)
                                     o Toplevel.proof_of)))
 
-(*
 fun auto_try st = if not (!auto) then (false, st) else do_try true NONE st
 
 val setup = Auto_Tools.register_tool (tryN, auto_try)
-*)
 
 end;