merged

--- a/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML	Mon Sep 20 09:26:24 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML	Mon Sep 20 11:51:46 2010 +0200
@@ -11,7 +11,7 @@
 sig
   type mode = Metis_Translate.mode
 
-  val trace: bool Unsynchronized.ref
+  val trace : bool Unsynchronized.ref
   val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
   val replay_one_inference :
     Proof.context -> mode -> (string * term) list

--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Sep 20 09:26:24 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Sep 20 11:51:46 2010 +0200
@@ -23,7 +23,6 @@
 open Metis_Translate
 open Metis_Reconstruct
 
-val trace = Unsynchronized.ref false
 fun trace_msg msg = if !trace then tracing (msg ()) else ()
 
 val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true);
@@ -139,6 +138,8 @@
 val type_has_top_sort =
   exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
 
+val preproc_ss = HOL_basic_ss addsimps @{thms all_simps [symmetric]}
+
 fun generic_metis_tac mode ctxt ths i st0 =
   let
     val _ = trace_msg (fn () =>
@@ -147,9 +148,14 @@
     if exists_type type_has_top_sort (prop_of st0) then
       (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
     else
-      Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
-                  (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
-                  ctxt i st0
+      Tactical.SOLVED'
+          ((TRY o Simplifier.simp_tac preproc_ss)
+           THEN'
+           (REPEAT_DETERM o match_tac @{thms allI})
+           THEN'
+           TRY o Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
+                     (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
+                     ctxt) i st0
   end
 
 val metis_tac = generic_metis_tac HO

--- a/src/HOL/Tools/try.ML	Mon Sep 20 09:26:24 2010 +0200
+++ b/src/HOL/Tools/try.ML	Mon Sep 20 11:51:46 2010 +0200
@@ -58,18 +58,19 @@
     Proof.refine (Method.SelectGoals (1, Method.Basic (named_method thy name)))
   end
 
-fun do_named_method_on_first_goal name timeout_opt st =
+fun do_named_method (name, all_goals) timeout_opt st =
   do_generic timeout_opt
-             (name ^ (if nprems_of (#goal (Proof.goal st)) > 1 then "[1]"
-                      else "")) I (#goal o Proof.goal)
+             (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
 
-val all_goals_named_methods = ["auto"]
-val first_goal_named_methods =
-  ["simp", "fast", "fastsimp", "force", "best", "blast", "arith"]
-val do_methods =
-  map do_named_method_on_first_goal all_goals_named_methods @
-  map do_named_method first_goal_named_methods
+val named_methods =
+  [("simp", false), ("auto", true), ("fast", false), ("fastsimp", false),
+   ("force", false), ("blast", false), ("arith", false)]
+val do_methods = map do_named_method named_methods
 
 fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"