# HG changeset patch
# User haftmann
# Date 1290550266 -3600
# Node ID 23904fa13e0389a9cc51f47ed59fe278be2377fa
# Parent  c059d550afecd98c6c8df00333d8a8724f7b814f# Parent  05f4885cbbe073ac6ef1cbf0101e78c839bf669c
merged

diff -r 05f4885cbbe0 -r 23904fa13e03 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/IsaMakefile	Tue Nov 23 23:11:06 2010 +0100
@@ -349,9 +349,11 @@
   Tools/SMT/smt_setup_solvers.ML \
   Tools/SMT/smt_solver.ML \
   Tools/SMT/smt_translate.ML \
+  Tools/SMT/smt_utils.ML \
   Tools/SMT/z3_interface.ML \
   Tools/SMT/z3_model.ML \
   Tools/SMT/z3_proof_literals.ML \
+  Tools/SMT/z3_proof_methods.ML \
   Tools/SMT/z3_proof_parser.ML \
   Tools/SMT/z3_proof_reconstruction.ML \
   Tools/SMT/z3_proof_tools.ML \
diff -r 05f4885cbbe0 -r 23904fa13e03 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Nov 23 23:11:06 2010 +0100
@@ -15,9 +15,8 @@
 
 fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "
 fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): "
-fun metis_tag smt id =
-  "#" ^ string_of_int id ^ " " ^ (if smt then "smt" else "metis") ^
-  " (sledgehammer): "
+fun reconstructor_tag reconstructor id =
+  "#" ^ string_of_int id ^ " " ^ (!reconstructor) ^ " (sledgehammer): "
 
 val separator = "-----"
 
@@ -33,7 +32,7 @@
   time_prover: int,
   time_prover_fail: int}
 
-datatype me_data = MeData of {
+datatype re_data = ReData of {
   calls: int,
   success: int,
   nontriv_calls: int,
@@ -61,15 +60,15 @@
 fun make_min_data (succs, ab_ratios) =
   MinData{succs=succs, ab_ratios=ab_ratios}
 
-fun make_me_data (calls,success,nontriv_calls,nontriv_success,proofs,time,
+fun make_re_data (calls,success,nontriv_calls,nontriv_success,proofs,time,
                   timeout,lemmas,posns) =
-  MeData{calls=calls, success=success, nontriv_calls=nontriv_calls,
+  ReData{calls=calls, success=success, nontriv_calls=nontriv_calls,
          nontriv_success=nontriv_success, proofs=proofs, time=time,
          timeout=timeout, lemmas=lemmas, posns=posns}
 
 val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0, 0, 0)
 val empty_min_data = make_min_data (0, 0)
-val empty_me_data = make_me_data (0, 0, 0, 0, 0, 0, 0, (0,0,0), [])
+val empty_re_data = make_re_data (0, 0, 0, 0, 0, 0, 0, (0,0,0), [])
 
 fun tuple_of_sh_data (ShData {calls, success, nontriv_calls, nontriv_success,
                               lemmas, max_lems, time_isa,
@@ -78,53 +77,54 @@
 
 fun tuple_of_min_data (MinData {succs, ab_ratios}) = (succs, ab_ratios)
 
-fun tuple_of_me_data (MeData {calls, success, nontriv_calls, nontriv_success,
+fun tuple_of_re_data (ReData {calls, success, nontriv_calls, nontriv_success,
   proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls,
   nontriv_success, proofs, time, timeout, lemmas, posns)
 
 
-datatype metis = Unminimized | Minimized | UnminimizedFT | MinimizedFT
+datatype reconstructor_mode =
+  Unminimized | Minimized | UnminimizedFT | MinimizedFT
 
 datatype data = Data of {
   sh: sh_data,
   min: min_data,
-  me_u: me_data, (* metis with unminimized set of lemmas *)
-  me_m: me_data, (* metis with minimized set of lemmas *)
-  me_uft: me_data, (* metis with unminimized set of lemmas and fully-typed *)
-  me_mft: me_data, (* metis with minimized set of lemmas and fully-typed *)
+  re_u: re_data, (* reconstructor with unminimized set of lemmas *)
+  re_m: re_data, (* reconstructor with minimized set of lemmas *)
+  re_uft: re_data, (* reconstructor with unminimized set of lemmas and fully-typed *)
+  re_mft: re_data, (* reconstructor with minimized set of lemmas and fully-typed *)
   mini: bool   (* with minimization *)
   }
 
-fun make_data (sh, min, me_u, me_m, me_uft, me_mft, mini) =
-  Data {sh=sh, min=min, me_u=me_u, me_m=me_m, me_uft=me_uft, me_mft=me_mft,
+fun make_data (sh, min, re_u, re_m, re_uft, re_mft, mini) =
+  Data {sh=sh, min=min, re_u=re_u, re_m=re_m, re_uft=re_uft, re_mft=re_mft,
     mini=mini}
 
 val empty_data = make_data (empty_sh_data, empty_min_data,
-  empty_me_data, empty_me_data, empty_me_data, empty_me_data, false)
+  empty_re_data, empty_re_data, empty_re_data, empty_re_data, false)
 
-fun map_sh_data f (Data {sh, min, me_u, me_m, me_uft, me_mft, mini}) =
+fun map_sh_data f (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) =
   let val sh' = make_sh_data (f (tuple_of_sh_data sh))
-  in make_data (sh', min, me_u, me_m, me_uft, me_mft, mini) end
+  in make_data (sh', min, re_u, re_m, re_uft, re_mft, mini) end
 
-fun map_min_data f (Data {sh, min, me_u, me_m, me_uft, me_mft, mini}) =
+fun map_min_data f (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) =
   let val min' = make_min_data (f (tuple_of_min_data min))
-  in make_data (sh, min', me_u, me_m, me_uft, me_mft, mini) end
+  in make_data (sh, min', re_u, re_m, re_uft, re_mft, mini) end
 
-fun map_me_data f m (Data {sh, min, me_u, me_m, me_uft, me_mft, mini}) =
+fun map_re_data f m (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) =
   let
     fun map_me g Unminimized   (u, m, uft, mft) = (g u, m, uft, mft)
       | map_me g Minimized     (u, m, uft, mft) = (u, g m, uft, mft)
       | map_me g UnminimizedFT (u, m, uft, mft) = (u, m, g uft, mft)
       | map_me g MinimizedFT   (u, m, uft, mft) = (u, m, uft, g mft)
 
-    val f' = make_me_data o f o tuple_of_me_data
+    val f' = make_re_data o f o tuple_of_re_data
 
-    val (me_u', me_m', me_uft', me_mft') =
-      map_me f' m (me_u, me_m, me_uft, me_mft)
-  in make_data (sh, min, me_u', me_m', me_uft', me_mft', mini) end
+    val (re_u', re_m', re_uft', re_mft') =
+      map_me f' m (re_u, re_m, re_uft, re_mft)
+  in make_data (sh, min, re_u', re_m', re_uft', re_mft', mini) end
 
-fun set_mini mini (Data {sh, min, me_u, me_m, me_uft, me_mft, ...}) =
-  make_data (sh, min, me_u, me_m, me_uft, me_mft, mini)
+fun set_mini mini (Data {sh, min, re_u, re_m, re_uft, re_mft, ...}) =
+  make_data (sh, min, re_u, re_m, re_uft, re_mft, mini)
 
 fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n));
 
@@ -170,39 +170,39 @@
 fun inc_min_ab_ratios r = map_min_data
   (fn (succs, ab_ratios) => (succs, ab_ratios+r))
 
-val inc_metis_calls = map_me_data
+val inc_reconstructor_calls = map_re_data
   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
     => (calls + 1, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns))
 
-val inc_metis_success = map_me_data
+val inc_reconstructor_success = map_re_data
   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
     => (calls, success + 1, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns))
 
-val inc_metis_nontriv_calls = map_me_data
+val inc_reconstructor_nontriv_calls = map_re_data
   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
     => (calls, success, nontriv_calls + 1, nontriv_success, proofs, time, timeout, lemmas,posns))
 
-val inc_metis_nontriv_success = map_me_data
+val inc_reconstructor_nontriv_success = map_re_data
   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
     => (calls, success, nontriv_calls, nontriv_success + 1, proofs, time, timeout, lemmas,posns))
 
-val inc_metis_proofs = map_me_data
+val inc_reconstructor_proofs = map_re_data
   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
     => (calls, success, nontriv_calls, nontriv_success, proofs + 1, time, timeout, lemmas,posns))
 
-fun inc_metis_time m t = map_me_data
+fun inc_reconstructor_time m t = map_re_data
  (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
   => (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns)) m
 
-val inc_metis_timeout = map_me_data
+val inc_reconstructor_timeout = map_re_data
   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
     => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout + 1, lemmas,posns))
 
-fun inc_metis_lemmas m n = map_me_data
+fun inc_reconstructor_lemmas m n = map_re_data
   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
     => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, inc_max n lemmas, posns)) m
 
-fun inc_metis_posns m pos = map_me_data
+fun inc_reconstructor_posns m pos = map_re_data
   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
     => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns)) m
 
@@ -243,26 +243,25 @@
     (if triv then "[T]" else "")
   end
 
-fun log_me_data log tag sh_calls (metis_calls, metis_success,
-     metis_nontriv_calls, metis_nontriv_success,
-     metis_proofs, metis_time, metis_timeout, (lemmas, lems_sos, lems_max),
-    metis_posns) =
- (log ("Total number of " ^ tag ^ "metis calls: " ^ str metis_calls);
-  log ("Number of successful " ^ tag ^ "metis calls: " ^ str metis_success ^
-    " (proof: " ^ str metis_proofs ^ ")");
-  log ("Number of " ^ tag ^ "metis timeouts: " ^ str metis_timeout);
-  log ("Success rate: " ^ percentage metis_success sh_calls ^ "%");
-  log ("Total number of nontrivial " ^ tag ^ "metis calls: " ^ str metis_nontriv_calls);
-  log ("Number of successful nontrivial " ^ tag ^ "metis calls: " ^ str metis_nontriv_success ^
-    " (proof: " ^ str metis_proofs ^ ")");
-  log ("Number of successful " ^ tag ^ "metis lemmas: " ^ str lemmas);
-  log ("SOS of successful " ^ tag ^ "metis lemmas: " ^ str lems_sos);
-  log ("Max number of successful " ^ tag ^ "metis lemmas: " ^ str lems_max);
-  log ("Total time for successful " ^ tag ^ "metis calls: " ^ str3 (time metis_time));
-  log ("Average time for successful " ^ tag ^ "metis calls: " ^
-    str3 (avg_time metis_time metis_success));
+fun log_re_data log tag sh_calls (re_calls, re_success, re_nontriv_calls,
+     re_nontriv_success, re_proofs, re_time, re_timeout,
+    (lemmas, lems_sos, lems_max), re_posns) =
+ (log ("Total number of " ^ tag ^ "reconstructor calls: " ^ str re_calls);
+  log ("Number of successful " ^ tag ^ "reconstructor calls: " ^ str re_success ^
+    " (proof: " ^ str re_proofs ^ ")");
+  log ("Number of " ^ tag ^ "reconstructor timeouts: " ^ str re_timeout);
+  log ("Success rate: " ^ percentage re_success sh_calls ^ "%");
+  log ("Total number of nontrivial " ^ tag ^ "reconstructor calls: " ^ str re_nontriv_calls);
+  log ("Number of successful nontrivial " ^ tag ^ "reconstructor calls: " ^ str re_nontriv_success ^
+    " (proof: " ^ str re_proofs ^ ")");
+  log ("Number of successful " ^ tag ^ "reconstructor lemmas: " ^ str lemmas);
+  log ("SOS of successful " ^ tag ^ "reconstructor lemmas: " ^ str lems_sos);
+  log ("Max number of successful " ^ tag ^ "reconstructor lemmas: " ^ str lems_max);
+  log ("Total time for successful " ^ tag ^ "reconstructor calls: " ^ str3 (time re_time));
+  log ("Average time for successful " ^ tag ^ "reconstructor calls: " ^
+    str3 (avg_time re_time re_success));
   if tag=""
-  then log ("Proved: " ^ space_implode " " (map str_of_pos metis_posns))
+  then log ("Proved: " ^ space_implode " " (map str_of_pos re_posns))
   else ()
  )
 
@@ -273,15 +272,15 @@
 
 in
 
-fun log_data id log (Data {sh, min, me_u, me_m, me_uft, me_mft, mini}) =
+fun log_data id log (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) =
   let
     val ShData {calls=sh_calls, ...} = sh
 
-    fun app_if (MeData {calls, ...}) f = if calls > 0 then f () else ()
-    fun log_me tag m =
-      log_me_data log tag sh_calls (tuple_of_me_data m)
-    fun log_metis (tag1, m1) (tag2, m2) = app_if m1 (fn () =>
-      (log_me tag1 m1; log ""; app_if m2 (fn () => log_me tag2 m2)))
+    fun app_if (ReData {calls, ...}) f = if calls > 0 then f () else ()
+    fun log_re tag m =
+      log_re_data log tag sh_calls (tuple_of_re_data m)
+    fun log_reconstructor (tag1, m1) (tag2, m2) = app_if m1 (fn () =>
+      (log_re tag1 m1; log ""; app_if m2 (fn () => log_re tag2 m2)))
   in
     if sh_calls > 0
     then
@@ -289,14 +288,14 @@
       log_sh_data log (tuple_of_sh_data sh);
       log "";
       if not mini
-      then log_metis ("", me_u) ("fully-typed ", me_uft)
+      then log_reconstructor ("", re_u) ("fully-typed ", re_uft)
       else
-        app_if me_u (fn () =>
-         (log_metis ("unminimized ", me_u) ("unminimized fully-typed ", me_uft);
+        app_if re_u (fn () =>
+         (log_reconstructor ("unminimized ", re_u) ("unminimized fully-typed ", re_uft);
           log "";
-          app_if me_m (fn () =>
+          app_if re_m (fn () =>
             (log_min_data log (tuple_of_min_data min); log "";
-             log_metis ("", me_m) ("fully-typed ", me_mft))))))
+             log_reconstructor ("", re_m) ("fully-typed ", re_mft))))))
     else ()
   end
 
@@ -330,6 +329,10 @@
 
 type locality = Sledgehammer_Filter.locality
 
+(* hack *)
+fun reconstructor_from_msg msg =
+  if String.isSubstring "metis" msg then "metis" else "smt"
+
 local
 
 datatype sh_result =
@@ -399,7 +402,7 @@
 
 in
 
-fun run_sledgehammer trivial args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
+fun run_sledgehammer trivial args reconstructor named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
   let
     val triv_str = if trivial then "[T] " else ""
     val _ = change_data id inc_sh_calls
@@ -423,6 +426,7 @@
           change_data id (inc_sh_max_lems (length names));
           change_data id (inc_sh_time_isa time_isa);
           change_data id (inc_sh_time_prover time_prover);
+          reconstructor := reconstructor_from_msg msg;
           named_thms := SOME (map_filter get_thms names);
           log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^
             string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
@@ -437,7 +441,8 @@
 
 end
 
-fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
+fun run_minimize args reconstructor named_thms id
+        ({pre=st, log, ...}: Mirabelle.run_args) =
   let
     val ctxt = Proof.context_of st
     val n0 = length (these (!named_thms))
@@ -461,43 +466,48 @@
          change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));
          if length named_thms' = n0
          then log (minimize_tag id ^ "already minimal")
-         else (named_thms := SOME named_thms';
+         else (reconstructor := reconstructor_from_msg msg;
+               named_thms := SOME named_thms';
                log (minimize_tag id ^ "succeeded:\n" ^ msg))
         )
     | (NONE, msg) => log (minimize_tag id ^ "failed: " ^ msg)
   end
 
 
-fun run_metis smt trivial full m name named_thms id
+fun run_reconstructor trivial full m name reconstructor named_thms id
     ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
   let
-    fun metis thms ctxt =
-      (if smt then SMT_Solver.smt_tac
+    fun do_reconstructor thms ctxt =
+      (if !reconstructor = "smt" then SMT_Solver.smt_tac
        else if full then Metis_Tactics.metisFT_tac
        else Metis_Tactics.metis_tac) ctxt thms
-    fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st
+    fun apply_reconstructor thms =
+      Mirabelle.can_apply timeout (do_reconstructor thms) st
 
     fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
-      | with_time (true, t) = (change_data id (inc_metis_success m);
-          if trivial then () else change_data id (inc_metis_nontriv_success m);
-          change_data id (inc_metis_lemmas m (length named_thms));
-          change_data id (inc_metis_time m t);
-          change_data id (inc_metis_posns m (pos, trivial));
-          if name = "proof" then change_data id (inc_metis_proofs m) else ();
+      | with_time (true, t) = (change_data id (inc_reconstructor_success m);
+          if trivial then ()
+          else change_data id (inc_reconstructor_nontriv_success m);
+          change_data id (inc_reconstructor_lemmas m (length named_thms));
+          change_data id (inc_reconstructor_time m t);
+          change_data id (inc_reconstructor_posns m (pos, trivial));
+          if name = "proof" then change_data id (inc_reconstructor_proofs m)
+          else ();
           "succeeded (" ^ string_of_int t ^ ")")
-    fun timed_metis thms =
-      (with_time (Mirabelle.cpu_time apply_metis thms), true)
-      handle TimeLimit.TimeOut => (change_data id (inc_metis_timeout m);
+    fun timed_reconstructor thms =
+      (with_time (Mirabelle.cpu_time apply_reconstructor thms), true)
+      handle TimeLimit.TimeOut => (change_data id (inc_reconstructor_timeout m);
                ("timeout", false))
            | ERROR msg => ("error: " ^ msg, false)
 
     val _ = log separator
-    val _ = change_data id (inc_metis_calls m)
-    val _ = if trivial then () else change_data id (inc_metis_nontriv_calls m)
+    val _ = change_data id (inc_reconstructor_calls m)
+    val _ = if trivial then ()
+            else change_data id (inc_reconstructor_nontriv_calls m)
   in
     maps snd named_thms
-    |> timed_metis
-    |>> log o prefix (metis_tag smt id)
+    |> timed_reconstructor
+    |>> log o prefix (reconstructor_tag reconstructor id)
     |> snd
   end
 
@@ -509,38 +519,46 @@
     if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal
     then () else
     let
+      val reconstructor = Unsynchronized.ref ""
       val named_thms =
         Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
       val ctxt = Proof.context_of pre
       val (prover_name, _) = get_prover ctxt args
-      val smt = String.isSuffix "smt" prover_name (* hack *)
       val minimize = AList.defined (op =) args minimizeK
       val metis_ft = AList.defined (op =) args metis_ftK
-      val trivial = TimeLimit.timeLimit try_outer_timeout
+      val trivial = false
+(* FIXME
+       TimeLimit.timeLimit try_outer_timeout
                                    (Try.invoke_try (SOME try_inner_timeout)) pre
                     handle TimeLimit.TimeOut => false
-      fun apply_metis m1 m2 =
+*)
+      fun apply_reconstructor m1 m2 =
         if metis_ft
         then
-          if not (Mirabelle.catch_result (metis_tag smt) false
-              (run_metis smt trivial false m1 name (these (!named_thms))) id st)
+          if not (Mirabelle.catch_result (reconstructor_tag reconstructor) false
+              (run_reconstructor trivial false m1 name reconstructor
+                   (these (!named_thms))) id st)
           then
-            (Mirabelle.catch_result (metis_tag smt) false
-              (run_metis smt trivial true m2 name (these (!named_thms))) id st; ())
+            (Mirabelle.catch_result (reconstructor_tag reconstructor) false
+              (run_reconstructor trivial true m2 name reconstructor
+                   (these (!named_thms))) id st; ())
           else ()
         else
-          (Mirabelle.catch_result (metis_tag smt) false
-            (run_metis smt trivial false m1 name (these (!named_thms))) id st; ())
+          (Mirabelle.catch_result (reconstructor_tag reconstructor) false
+            (run_reconstructor trivial false m1 name reconstructor
+                 (these (!named_thms))) id st; ())
     in 
       change_data id (set_mini minimize);
-      Mirabelle.catch sh_tag (run_sledgehammer trivial args named_thms) id st;
+      Mirabelle.catch sh_tag (run_sledgehammer trivial args reconstructor
+                                               named_thms) id st;
       if is_some (!named_thms)
       then
-       (apply_metis Unminimized UnminimizedFT;
+       (apply_reconstructor Unminimized UnminimizedFT;
         if minimize andalso not (null (these (!named_thms)))
         then
-         (Mirabelle.catch minimize_tag (run_minimize args named_thms) id st;
-          apply_metis Minimized MinimizedFT)
+         (Mirabelle.catch minimize_tag
+              (run_minimize args reconstructor named_thms) id st;
+          apply_reconstructor Minimized MinimizedFT)
         else ())
       else ()
     end
diff -r 05f4885cbbe0 -r 23904fa13e03 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/SMT.thy	Tue Nov 23 23:11:06 2010 +0100
@@ -10,6 +10,7 @@
   "Tools/Datatype/datatype_selectors.ML"
   "Tools/SMT/smt_failure.ML"
   "Tools/SMT/smt_config.ML"
+  "Tools/SMT/smt_utils.ML"
   "Tools/SMT/smt_monomorph.ML"
   ("Tools/SMT/smt_builtin.ML")
   ("Tools/SMT/smt_normalize.ML")
@@ -19,6 +20,7 @@
   ("Tools/SMT/z3_proof_parser.ML")
   ("Tools/SMT/z3_proof_tools.ML")
   ("Tools/SMT/z3_proof_literals.ML")
+  ("Tools/SMT/z3_proof_methods.ML")
   ("Tools/SMT/z3_proof_reconstruction.ML")
   ("Tools/SMT/z3_model.ML")
   ("Tools/SMT/z3_interface.ML")
@@ -52,6 +54,33 @@
 
 
 
+subsection {* Quantifier weights *}
+
+text {*
+Weight annotations to quantifiers influence the priority of quantifier
+instantiations.  They should be handled with care for solvers, which support
+them, because incorrect choices of weights might render a problem unsolvable.
+*}
+
+definition weight :: "int \<Rightarrow> bool \<Rightarrow> bool" where "weight _ P = P"
+
+text {*
+Weights must be non-negative.  The value @{text 0} is equivalent to providing
+no weight at all.
+
+Weights should only be used at quantifiers and only inside triggers (if the
+quantifier has triggers).  Valid usages of weights are as follows:
+
+\begin{itemize}
+\item
+@{term "\<forall>x. trigger [[pat (P x)]] (weight 2 (P x))"}
+\item
+@{term "\<forall>x. weight 3 (P x)"}
+\end{itemize}
+*}
+
+
+
 subsection {* Distinctness *}
 
 text {*
@@ -137,6 +166,7 @@
 use "Tools/SMT/z3_proof_parser.ML"
 use "Tools/SMT/z3_proof_tools.ML"
 use "Tools/SMT/z3_proof_literals.ML"
+use "Tools/SMT/z3_proof_methods.ML"
 use "Tools/SMT/z3_proof_reconstruction.ML"
 use "Tools/SMT/z3_model.ML"
 use "Tools/SMT/smt_setup_solvers.ML"
@@ -339,7 +369,7 @@
 
 hide_type (open) pattern
 hide_const Pattern term_eq
-hide_const (open) trigger pat nopat distinct fun_app z3div z3mod
+hide_const (open) trigger pat nopat weight distinct fun_app z3div z3mod
 
 
 
diff -r 05f4885cbbe0 -r 23904fa13e03 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Nov 23 23:11:06 2010 +0100
@@ -26,7 +26,7 @@
   type 'a proof = 'a uniform_formula step list
 
   val strip_spaces : (char -> bool) -> string -> string
-  val string_for_failure : failure -> string
+  val string_for_failure : string -> failure -> string
   val extract_important_message : string -> string
   val extract_known_failure :
     (failure * string) list -> string -> failure option
@@ -75,13 +75,15 @@
   " appears to be missing. You will need to install it if you want to run \
   \ATPs remotely."
 
-fun string_for_failure Unprovable = "The ATP problem is unprovable."
-  | string_for_failure IncompleteUnprovable =
-    "The ATP cannot prove the problem."
-  | string_for_failure CantConnect = "Can't connect to remote server."
-  | string_for_failure TimedOut = "Timed out."
-  | string_for_failure OutOfResources = "The ATP ran out of resources."
-  | string_for_failure SpassTooOld =
+fun string_for_failure prover Unprovable =
+    "The " ^ prover ^ " problem is unprovable."
+  | string_for_failure prover IncompleteUnprovable =
+    "The " ^ prover ^ " cannot prove the problem."
+  | string_for_failure _ CantConnect = "Cannot connect to remote server."
+  | string_for_failure _ TimedOut = "Timed out."
+  | string_for_failure prover OutOfResources =
+    "The " ^ prover ^ " ran out of resources."
+  | string_for_failure _ SpassTooOld =
     "Isabelle requires a more recent version of SPASS with support for the \
     \TPTP syntax. To install it, download and extract the package \
     \\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \
@@ -90,21 +92,24 @@
                (Path.variable "ISABELLE_HOME_USER" ::
                 map Path.basic ["etc", "components"])))) ^
     " on a line of its own."
-  | string_for_failure VampireTooOld =
+  | string_for_failure _ VampireTooOld =
     "Isabelle requires a more recent version of Vampire. To install it, follow \
     \the instructions from the Sledgehammer manual (\"isabelle doc\
     \ sledgehammer\")."
-  | string_for_failure NoPerl = "Perl" ^ missing_message_tail
-  | string_for_failure NoLibwwwPerl =
+  | string_for_failure _ NoPerl = "Perl" ^ missing_message_tail
+  | string_for_failure _ NoLibwwwPerl =
     "The Perl module \"libwww-perl\"" ^ missing_message_tail
-  | string_for_failure MalformedInput =
-    "The ATP problem is malformed. Please report this to the Isabelle \
+  | string_for_failure prover MalformedInput =
+    "The " ^ prover ^ " problem is malformed. Please report this to the Isabelle \
     \developers."
-  | string_for_failure MalformedOutput = "The ATP output is malformed."
-  | string_for_failure Interrupted = "The ATP was interrupted."
-  | string_for_failure Crashed = "The ATP crashed."
-  | string_for_failure InternalError = "An internal ATP error occurred."
-  | string_for_failure UnknownError = "An unknown ATP error occurred."
+  | string_for_failure prover MalformedOutput =
+    "The " ^ prover ^ " output is malformed."
+  | string_for_failure prover Interrupted = "The " ^ prover ^ " was interrupted."
+  | string_for_failure prover Crashed = "The " ^ prover ^ " crashed."
+  | string_for_failure prover InternalError =
+    "An internal " ^ prover ^ " error occurred."
+  | string_for_failure prover UnknownError =
+    "An unknown " ^ prover ^ " error occurred."
 
 fun extract_delimited (begin_delim, end_delim) output =
   output |> first_field begin_delim |> the |> snd
diff -r 05f4885cbbe0 -r 23904fa13e03 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Nov 23 23:11:06 2010 +0100
@@ -186,7 +186,7 @@
     (output, 0) => split_lines output
   | (output, _) =>
     error (case extract_known_failure known_perl_failures output of
-             SOME failure => string_for_failure failure
+             SOME failure => string_for_failure "ATP" failure
            | NONE => perhaps (try (unsuffix "\n")) output ^ ".")
 
 fun find_system name [] systems = find_first (String.isPrefix name) systems
diff -r 05f4885cbbe0 -r 23904fa13e03 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue Nov 23 23:11:06 2010 +0100
@@ -13,6 +13,8 @@
 
   val trace : bool Config.T
   val trace_msg : Proof.context -> (unit -> string) -> unit
+  val verbose : bool Config.T
+  val verbose_warning : Proof.context -> string -> unit
   val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
   val untyped_aconv : term -> term -> bool
   val replay_one_inference :
@@ -30,8 +32,11 @@
 open Metis_Translate
 
 val (trace, trace_setup) = Attrib.config_bool "trace_metis" (K false)
+val (verbose, verbose_setup) = Attrib.config_bool "verbose_metis" (K true)
 
 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
+fun verbose_warning ctxt msg =
+  if Config.get ctxt verbose then warning msg else ()
 
 datatype term_or_type = SomeTerm of term | SomeType of typ
 
@@ -821,6 +826,6 @@
                     \Error when discharging Skolem assumptions.")
     end
 
-val setup = trace_setup
+val setup = trace_setup #> verbose_setup
 
 end;
diff -r 05f4885cbbe0 -r 23904fa13e03 src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Tue Nov 23 23:11:06 2010 +0100
@@ -10,6 +10,7 @@
 signature METIS_TACTICS =
 sig
   val trace : bool Config.T
+  val verbose : bool Config.T
   val type_lits : bool Config.T
   val new_skolemizer : bool Config.T
   val metis_tac : Proof.context -> thm list -> int -> tactic
@@ -103,12 +104,12 @@
                   if have_common_thm used cls then NONE else SOME name)
             in
                 if not (null cls) andalso not (have_common_thm used cls) then
-                  warning "Metis: The assumptions are inconsistent."
+                  verbose_warning ctxt "Metis: The assumptions are inconsistent"
                 else
                   ();
                 if not (null unused) then
-                  warning ("Metis: Unused theorems: " ^ commas_quote unused
-                           ^ ".")
+                  verbose_warning ctxt ("Metis: Unused theorems: " ^
+                                        commas_quote unused)
                 else
                   ();
                 case result of
@@ -154,7 +155,8 @@
         "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
   in
     if exists_type type_has_top_sort (prop_of st0) then
-      (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
+      (verbose_warning ctxt "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)
diff -r 05f4885cbbe0 -r 23904fa13e03 src/HOL/Tools/SMT/smt_builtin.ML
--- a/src/HOL/Tools/SMT/smt_builtin.ML	Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_builtin.ML	Tue Nov 23 23:11:06 2010 +0100
@@ -55,6 +55,7 @@
   (@{const_name SMT.pat}, K true),
   (@{const_name SMT.nopat}, K true),
   (@{const_name SMT.trigger}, K true),
+  (@{const_name SMT.weight}, K true),
   (@{const_name SMT.fun_app}, K true),
   (@{const_name SMT.z3div}, K true),
   (@{const_name SMT.z3mod}, K true),
diff -r 05f4885cbbe0 -r 23904fa13e03 src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Tue Nov 23 23:11:06 2010 +0100
@@ -28,12 +28,11 @@
 structure SMT_Normalize: SMT_NORMALIZE =
 struct
 
+structure U = SMT_Utils
+
 infix 2 ??
 fun (test ?? f) x = if test x then f x else x
 
-fun if_conv c cv1 cv2 ct = (if c (Thm.term_of ct) then cv1 else cv2) ct
-fun if_true_conv c cv = if_conv c cv Conv.all_conv
-
 
 
 (* simplification of trivial distincts (distinct should have at least
@@ -53,7 +52,7 @@
     "SMT.distinct [x, y] = (x ~= y)"
     by (simp_all add: distinct_def)}
   fun distinct_conv _ =
-    if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
+    U.if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
 in
 fun trivial_distinct ctxt =
   map (apsnd ((Term.exists_subterm is_trivial_distinct o Thm.prop_of) ??
@@ -71,7 +70,7 @@
 
   val thm = mk_meta_eq @{lemma
     "(case P of True => x | False => y) = (if P then x else y)" by simp}
-  val unfold_conv = if_true_conv is_bool_case (Conv.rewr_conv thm)
+  val unfold_conv = U.if_true_conv is_bool_case (Conv.rewr_conv thm)
 in
 fun rewrite_bool_cases ctxt =
   map (apsnd ((Term.exists_subterm is_bool_case o Thm.prop_of) ??
@@ -105,7 +104,7 @@
       "Int.Bit1 (- k) = - Int.Bit1 (Int.pred k)"
       by simp_all (simp add: pred_def)}
 
-  fun pos_conv ctxt = if_conv (is_strange_number ctxt)
+  fun pos_conv ctxt = U.if_conv (is_strange_number ctxt)
     (Simplifier.rewrite (Simplifier.context ctxt pos_numeral_ss))
     Conv.no_conv
 in
@@ -282,7 +281,7 @@
         | (_, ts) => forall (is_normed ctxt) ts))
 in
 fun norm_binder_conv ctxt =
-  if_conv (is_normed ctxt) Conv.all_conv (norm_conv ctxt)
+  U.if_conv (is_normed ctxt) Conv.all_conv (norm_conv ctxt)
 end
 
 fun norm_def ctxt thm =
@@ -321,13 +320,6 @@
 (* lift lambda terms into additional rules *)
 
 local
-  val meta_eq = @{cpat "op =="}
-  val meta_eqT = hd (Thm.dest_ctyp (Thm.ctyp_of_term meta_eq))
-  fun inst_meta cT = Thm.instantiate_cterm ([(meta_eqT, cT)], []) meta_eq
-  fun mk_meta_eq ct cu = Thm.mk_binop (inst_meta (Thm.ctyp_of_term ct)) ct cu
-
-  fun cert ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
-
   fun used_vars cvs ct =
     let
       val lookup = AList.lookup (op aconv) (map (` Thm.term_of) cvs)
@@ -350,7 +342,7 @@
           let
             val {T, ...} = Thm.rep_cterm ct' and n = Name.uu
             val (n', ctxt') = yield_singleton Variable.variant_fixes n ctxt
-            val cu = mk_meta_eq (cert ctxt (Free (n', T))) ct'
+            val cu = U.mk_cequals (U.certify ctxt (Free (n', T))) ct'
             val (eq, ctxt'') = yield_singleton Assumption.add_assumes cu ctxt'
             val defs' = Termtab.update (Thm.term_of ct', eq) defs
           in (apply_def cvs' eq, (ctxt'', defs')) end)
diff -r 05f4885cbbe0 -r 23904fa13e03 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Tue Nov 23 23:11:06 2010 +0100
@@ -32,7 +32,7 @@
 
   (*filter*)
   val smt_filter: bool -> Time.time -> Proof.state -> ('a * thm) list -> int ->
-    {outcome: SMT_Failure.failure option, used_facts: 'a list,
+    {outcome: SMT_Failure.failure option, used_facts: ('a * thm) list,
     run_time_in_msecs: int option}
 
   (*tactic*)
@@ -331,7 +331,7 @@
     val irs = map (pair ~1) (Thm.assume cprop :: prems @ facts)
     val rm = SOME run_remote
   in
-    split_list xrules
+    (xrules, map snd xrules)
     ||> distinct (op =) o fst o smt_solver rm ctxt' o append irs o map_index I
     |-> map_filter o try o nth
     |> (fn xs => {outcome=NONE, used_facts=xs, run_time_in_msecs=NONE})
diff -r 05f4885cbbe0 -r 23904fa13e03 src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Tue Nov 23 23:11:06 2010 +0100
@@ -13,7 +13,7 @@
     SVar of int |
     SApp of string * sterm list |
     SLet of string * sterm * sterm |
-    SQua of squant * string list * sterm spattern list * sterm
+    SQua of squant * string list * sterm spattern list * int option * sterm
 
   (* configuration options *)
   type prefixes = {sort_prefix: string, func_prefix: string}
@@ -52,6 +52,9 @@
 structure SMT_Translate: SMT_TRANSLATE =
 struct
 
+structure U = SMT_Utils
+
+
 (* intermediate term structure *)
 
 datatype squant = SForall | SExists
@@ -62,7 +65,7 @@
   SVar of int |
   SApp of string * sterm list |
   SLet of string * sterm * sterm |
-  SQua of squant * string list * sterm spattern list * sterm
+  SQua of squant * string list * sterm spattern list * int option * sterm
 
 
 
@@ -107,13 +110,6 @@
 
 (* utility functions *)
 
-val dest_funT =
-  let
-    fun dest Ts 0 T = (rev Ts, T)
-      | dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i-1) U
-      | dest _ _ T = raise TYPE ("dest_funT", [T], [])
-  in dest [] end
-
 val quantifier = (fn
     @{const_name All} => SOME SForall
   | @{const_name Ex} => SOME SExists
@@ -123,6 +119,10 @@
       if q = qname then group_quant qname (T :: Ts) u else (Ts, t)
   | group_quant _ Ts t = (Ts, t)
 
+fun dest_weight (@{const SMT.weight} $ w $ t) =
+      (SOME (snd (HOLogic.dest_number w)), t)
+  | dest_weight t = (NONE, t)
+
 fun dest_pat (Const (@{const_name pat}, _) $ t) = (t, true)
   | dest_pat (Const (@{const_name nopat}, _) $ t) = (t, false)
   | dest_pat t = raise TERM ("dest_pat", [t])
@@ -141,8 +141,9 @@
 fun dest_quant qn T t = quantifier qn |> Option.map (fn q =>
   let
     val (Ts, u) = group_quant qn [T] t
-    val (ps, b) = dest_trigger u
-  in (q, rev Ts, ps, b) end)
+    val (ps, p) = dest_trigger u
+    val (w, b) = dest_weight p
+  in (q, rev Ts, ps, w, b) end)
 
 fun fold_map_pat f (SPat ts) = fold_map f ts #>> SPat
   | fold_map_pat f (SNoPat ts) = fold_map f ts #>> SNoPat
@@ -218,6 +219,9 @@
       | (h as Free _, ts) => Term.list_comb (h, map in_term ts)
       | _ => t)
 
+    and in_weight ((c as @{const SMT.weight}) $ w $ t) = c $ w $ in_form t
+      | in_weight t = in_form t 
+
     and in_pat ((c as Const (@{const_name pat}, _)) $ t) = c $ in_term t
       | in_pat ((c as Const (@{const_name nopat}, _)) $ t) = c $ in_term t
       | in_pat t = raise TERM ("in_pat", [t])
@@ -225,8 +229,8 @@
     and in_pats ps =
       in_list @{typ "pattern list"} (in_list @{typ pattern} in_pat) ps
 
-    and in_trig ((c as @{const trigger}) $ p $ t) = c $ in_pats p $ in_form t
-      | in_trig t = in_form t
+    and in_trig ((c as @{const trigger}) $ p $ t) = c $ in_pats p $ in_weight t
+      | in_trig t = in_weight t
 
     and in_form t =
       (case Term.strip_comb t of
@@ -348,7 +352,7 @@
     and new_dtyps dts cx =
       let
         fun new_decl i t =
-          let val (Ts, T) = dest_funT i (Term.fastype_of t)
+          let val (Ts, T) = U.dest_funT i (Term.fastype_of t)
           in
             fold_map transT Ts ##>> transT T ##>>
             new_fun func_prefix t NONE #>> swap
@@ -370,9 +374,9 @@
       (case Term.strip_comb t of
         (Const (qn, _), [Abs (_, T, t1)]) =>
           (case dest_quant qn T t1 of
-            SOME (q, Ts, ps, b) =>
+            SOME (q, Ts, ps, w, b) =>
               fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>>
-              trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', b'))
+              trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', w, b'))
           | NONE => raise TERM ("intermediate", [t]))
       | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) =>
           transT T ##>> trans t1 ##>> trans t2 #>>
@@ -396,7 +400,7 @@
       | _ => raise TERM ("smt_translate", [t]))
 
     and transs t T ts =
-      let val (Us, U) = dest_funT (length ts) T
+      let val (Us, U) = U.dest_funT (length ts) T
       in
         fold_map transT Us ##>> transT U #-> (fn Up =>
         fresh_fun func_prefix t (SOME Up) ##>> fold_map trans ts #>> SApp)
diff -r 05f4885cbbe0 -r 23904fa13e03 src/HOL/Tools/SMT/smt_utils.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/smt_utils.ML	Tue Nov 23 23:11:06 2010 +0100
@@ -0,0 +1,140 @@
+(*  Title:      HOL/Tools/SMT/smt_utils.ML
+    Author:     Sascha Boehme, TU Muenchen
+
+General utility functions.
+*)
+
+signature SMT_UTILS =
+sig
+  val repeat: ('a -> 'a option) -> 'a -> 'a
+  val repeat_yield: ('a -> 'b -> ('a * 'b) option) -> 'a -> 'b -> 'a * 'b
+
+  (* types *)
+  val split_type: typ -> typ * typ
+  val dest_funT: int -> typ -> typ list * typ
+
+  (* terms *)
+  val dest_conj: term -> term * term
+  val dest_disj: term -> term * term
+
+  (* patterns and instantiations *)
+  val mk_const_pat: theory -> string -> (ctyp -> 'a) -> 'a * cterm
+  val destT1: ctyp -> ctyp
+  val destT2: ctyp -> ctyp
+  val instTs: ctyp list -> ctyp list * cterm -> cterm
+  val instT: ctyp -> ctyp * cterm -> cterm
+  val instT': cterm -> ctyp * cterm -> cterm
+
+  (* certified terms *)
+  val certify: Proof.context -> term -> cterm
+  val typ_of: cterm -> typ
+  val dest_cabs: cterm -> Proof.context -> cterm * Proof.context
+  val dest_all_cabs: cterm -> Proof.context -> cterm * Proof.context
+  val dest_cbinder: cterm -> Proof.context -> cterm * Proof.context
+  val dest_all_cbinders: cterm -> Proof.context -> cterm * Proof.context
+  val mk_cprop: cterm -> cterm
+  val dest_cprop: cterm -> cterm
+  val mk_cequals: cterm -> cterm -> cterm
+
+  (* conversions *)
+  val if_conv: (term -> bool) -> conv -> conv -> conv
+  val if_true_conv: (term -> bool) -> conv -> conv
+  val binders_conv: (Proof.context -> conv) -> Proof.context -> conv
+  val prop_conv: conv -> conv
+end
+
+structure SMT_Utils: SMT_UTILS =
+struct
+
+fun repeat f =
+  let fun rep x = (case f x of SOME y => rep y | NONE => x)
+  in rep end
+
+fun repeat_yield f =
+  let fun rep x y = (case f x y of SOME (x', y') => rep x' y' | NONE => (x, y))
+  in rep end
+
+
+(* types *)
+
+fun split_type T = (Term.domain_type T, Term.range_type T)
+
+val dest_funT =
+  let
+    fun dest Ts 0 T = (rev Ts, T)
+      | dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i-1) U
+      | dest _ _ T = raise TYPE ("not a function type", [T], [])
+  in dest [] end
+
+
+(* terms *)
+
+fun dest_conj (@{const HOL.conj} $ t $ u) = (t, u)
+  | dest_conj t = raise TERM ("not a conjunction", [t])
+
+fun dest_disj (@{const HOL.disj} $ t $ u) = (t, u)
+  | dest_disj t = raise TERM ("not a disjunction", [t])
+
+
+(* patterns and instantiations *)
+
+fun mk_const_pat thy name destT =
+  let val cpat = Thm.cterm_of thy (Const (name, Sign.the_const_type thy name))
+  in (destT (Thm.ctyp_of_term cpat), cpat) end
+
+val destT1 = hd o Thm.dest_ctyp
+val destT2 = hd o tl o Thm.dest_ctyp
+
+fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (cTs ~~ cUs, []) ct
+fun instT cU (cT, ct) = instTs [cU] ([cT], ct)
+fun instT' ct = instT (Thm.ctyp_of_term ct)
+
+
+(* certified terms *)
+
+fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
+
+fun typ_of ct = #T (Thm.rep_cterm ct) 
+
+fun dest_cabs ct ctxt =
+  (case Thm.term_of ct of
+    Abs _ =>
+      let val (n, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt
+      in (snd (Thm.dest_abs (SOME n) ct), ctxt') end
+  | _ => raise CTERM ("no abstraction", [ct]))
+
+val dest_all_cabs = repeat_yield (try o dest_cabs) 
+
+fun dest_cbinder ct ctxt =
+  (case Thm.term_of ct of
+    Const _ $ Abs _ => dest_cabs (Thm.dest_arg ct) ctxt
+  | _ => raise CTERM ("not a binder", [ct]))
+
+val dest_all_cbinders = repeat_yield (try o dest_cbinder)
+
+val mk_cprop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop})
+
+fun dest_cprop ct =
+  (case Thm.term_of ct of
+    @{const Trueprop} $ _ => Thm.dest_arg ct
+  | _ => raise CTERM ("not a property", [ct]))
+
+val equals = mk_const_pat @{theory} @{const_name "=="} destT1
+fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu
+
+
+(* conversions *)
+
+fun if_conv pred cv1 cv2 ct = if pred (Thm.term_of ct) then cv1 ct else cv2 ct
+
+fun if_true_conv pred cv = if_conv pred cv Conv.all_conv
+
+fun binders_conv cv ctxt =
+  Conv.binder_conv (binders_conv cv o snd) ctxt else_conv cv ctxt
+
+fun prop_conv cv ct =
+  (case Thm.term_of ct of
+    @{const Trueprop} $ _ => Conv.arg_conv cv ct
+  | _ => raise CTERM ("not a property", [ct]))
+
+end
diff -r 05f4885cbbe0 -r 23904fa13e03 src/HOL/Tools/SMT/smtlib_interface.ML
--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Tue Nov 23 23:11:06 2010 +0100
@@ -238,7 +238,7 @@
 fun sterm l (T.SVar i) = sep (var (l - i - 1))
   | sterm l (T.SApp (n, ts)) = app n (sterm l) ts
   | sterm _ (T.SLet _) = raise Fail "SMT-LIB: unsupported let expression"
-  | sterm l (T.SQua (q, ss, ps, t)) =
+  | sterm l (T.SQua (q, ss, ps, w, t)) =
       let
         val quant = add o (fn T.SForall => "forall" | T.SExists => "exists")
         val vs = map_index (apfst (Integer.add l)) ss
@@ -247,7 +247,12 @@
         fun pat kind ts = sep (add kind #> enclose "{" " }" (fold sub ts))
         fun pats (T.SPat ts) = pat ":pat" ts
           | pats (T.SNoPat ts) = pat ":nopat" ts
-      in par (quant q #> fold var_decl vs #> sub t #> fold pats ps) end
+        fun weight NONE = I
+          | weight (SOME i) =
+              sep (add ":weight { " #> add (string_of_int i) #> add " }")
+      in
+        par (quant q #> fold var_decl vs #> sub t #> fold pats ps #> weight w)
+      end
 
 fun ssort sorts = sort fast_string_ord sorts
 fun fsort funcs = sort (prod_ord fast_string_ord (K EQUAL)) funcs
diff -r 05f4885cbbe0 -r 23904fa13e03 src/HOL/Tools/SMT/z3_interface.ML
--- a/src/HOL/Tools/SMT/z3_interface.ML	Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_interface.ML	Tue Nov 23 23:11:06 2010 +0100
@@ -21,16 +21,13 @@
   val mk_builtin_fun: Proof.context -> sym -> cterm list -> cterm option
 
   val is_builtin_theory_term: Proof.context -> term -> bool
-
-  val mk_inst_pair: (ctyp -> 'a) -> cterm -> 'a * cterm
-  val destT1: ctyp -> ctyp
-  val destT2: ctyp -> ctyp
-  val instT': cterm -> ctyp * cterm -> cterm
 end
 
 structure Z3_Interface: Z3_INTERFACE =
 struct
 
+structure U = SMT_Utils
+
 
 (** Z3-specific builtins **)
 
@@ -163,13 +160,6 @@
   | mk_builtin_num ctxt i T =
       chained_mk_builtin_num ctxt (get_mk_builtins ctxt) i T
 
-fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (cTs ~~ cUs, []) ct
-fun instT cU (cT, ct) = instTs [cU] ([cT], ct)
-fun instT' ct = instT (Thm.ctyp_of_term ct)
-fun mk_inst_pair destT cpat = (destT (Thm.ctyp_of_term cpat), cpat)
-val destT1 = hd o Thm.dest_ctyp
-val destT2 = hd o tl o Thm.dest_ctyp
-
 val mk_true = Thm.cterm_of @{theory} (@{const Not} $ @{const False})
 val mk_false = Thm.cterm_of @{theory} @{const False}
 val mk_not = Thm.capply (Thm.cterm_of @{theory} @{const Not})
@@ -181,31 +171,34 @@
 fun mk_nary _ cu [] = cu
   | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
 
-val eq = mk_inst_pair destT1 @{cpat HOL.eq}
-fun mk_eq ct cu = Thm.mk_binop (instT' ct eq) ct cu
+val eq = U.mk_const_pat @{theory} @{const_name HOL.eq} U.destT1
+fun mk_eq ct cu = Thm.mk_binop (U.instT' ct eq) ct cu
 
-val if_term = mk_inst_pair (destT1 o destT2) @{cpat If}
-fun mk_if cc ct cu = Thm.mk_binop (Thm.capply (instT' ct if_term) cc) ct cu
+val if_term = U.mk_const_pat @{theory} @{const_name If} (U.destT1 o U.destT2)
+fun mk_if cc ct cu = Thm.mk_binop (Thm.capply (U.instT' ct if_term) cc) ct cu
 
-val nil_term = mk_inst_pair destT1 @{cpat Nil}
-val cons_term = mk_inst_pair destT1 @{cpat Cons}
+val nil_term = U.mk_const_pat @{theory} @{const_name Nil} U.destT1
+val cons_term = U.mk_const_pat @{theory} @{const_name Cons} U.destT1
 fun mk_list cT cts =
-  fold_rev (Thm.mk_binop (instT cT cons_term)) cts (instT cT nil_term)
+  fold_rev (Thm.mk_binop (U.instT cT cons_term)) cts (U.instT cT nil_term)
 
-val distinct = mk_inst_pair (destT1 o destT1) @{cpat SMT.distinct}
+val distinct = U.mk_const_pat @{theory} @{const_name SMT.distinct}
+  (U.destT1 o U.destT1)
 fun mk_distinct [] = mk_true
   | mk_distinct (cts as (ct :: _)) =
-      Thm.capply (instT' ct distinct) (mk_list (Thm.ctyp_of_term ct) cts)
+      Thm.capply (U.instT' ct distinct) (mk_list (Thm.ctyp_of_term ct) cts)
 
-val access = mk_inst_pair (Thm.dest_ctyp o destT1) @{cpat fun_app}
+val access = U.mk_const_pat @{theory} @{const_name fun_app}
+  (Thm.dest_ctyp o U.destT1)
 fun mk_access array index =
   let val cTs = Thm.dest_ctyp (Thm.ctyp_of_term array)
-  in Thm.mk_binop (instTs cTs access) array index end
+  in Thm.mk_binop (U.instTs cTs access) array index end
 
-val update = mk_inst_pair (Thm.dest_ctyp o destT1) @{cpat fun_upd}
+val update = U.mk_const_pat @{theory} @{const_name fun_upd}
+  (Thm.dest_ctyp o U.destT1)
 fun mk_update array index value =
   let val cTs = Thm.dest_ctyp (Thm.ctyp_of_term array)
-  in Thm.capply (Thm.mk_binop (instTs cTs update) array index) value end
+  in Thm.capply (Thm.mk_binop (U.instTs cTs update) array index) value end
 
 val mk_uminus = Thm.capply (Thm.cterm_of @{theory} @{const uminus (int)})
 val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (int)})
diff -r 05f4885cbbe0 -r 23904fa13e03 src/HOL/Tools/SMT/z3_model.ML
--- a/src/HOL/Tools/SMT/z3_model.ML	Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_model.ML	Tue Nov 23 23:11:06 2010 +0100
@@ -13,6 +13,9 @@
 structure Z3_Model: Z3_MODEL =
 struct
 
+structure U = SMT_Utils
+
+
 (* counterexample expressions *)
 
 datatype expr = True | False | Number of int * int option | Value of int |
@@ -214,15 +217,13 @@
 
 fun mk_fun_upd T U = Const (@{const_name fun_upd}, [T --> U, T, U, T] ---> U)
 
-fun split_type T = (Term.domain_type T, Term.range_type T)
-
 fun mk_update ([], u) _ = u
   | mk_update ([t], u) f =
-      uncurry mk_fun_upd (split_type (Term.fastype_of f)) $ f $ t $ u
+      uncurry mk_fun_upd (U.split_type (Term.fastype_of f)) $ f $ t $ u
   | mk_update (t :: ts, u) f =
       let
-        val (dT, rT) = split_type (Term.fastype_of f)
-        val (dT', rT') = split_type rT
+        val (dT, rT) = U.split_type (Term.fastype_of f)
+        val (dT', rT') = U.split_type rT
       in
         mk_fun_upd dT rT $ f $ t $
           mk_update (ts, u) (Term.absdummy (dT', Const ("_", rT')))
diff -r 05f4885cbbe0 -r 23904fa13e03 src/HOL/Tools/SMT/z3_proof_methods.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/z3_proof_methods.ML	Tue Nov 23 23:11:06 2010 +0100
@@ -0,0 +1,132 @@
+(*  Title:      HOL/Tools/SMT/z3_proof_methods.ML
+    Author:     Sascha Boehme, TU Muenchen
+
+Proof methods for Z3 proof reconstruction.
+*)
+
+signature Z3_PROOF_METHODS =
+sig
+  val prove_injectivity: Proof.context -> cterm -> thm
+end
+
+structure Z3_Proof_Methods: Z3_PROOF_METHODS =
+struct
+
+structure U = SMT_Utils
+structure T = Z3_Proof_Tools
+
+
+fun apply tac st =
+  (case Seq.pull (tac 1 st) of
+    NONE => raise THM ("tactic failed", 1, [st])
+  | SOME (st', _) => st')
+
+
+
+(* injectivity *)
+
+local
+
+val B = @{typ bool}
+fun mk_univ T = Const (@{const_name top}, T --> B)
+fun mk_inj_on T U =
+  Const (@{const_name inj_on}, (T --> U) --> (T --> B) --> B)
+fun mk_inv_into T U =
+  Const (@{const_name inv_into}, [T --> B, T --> U, U] ---> T)
+
+fun mk_inv_of ctxt ct =
+  let
+    val (dT, rT) = U.split_type (U.typ_of ct)
+    val inv = U.certify ctxt (mk_inv_into dT rT)
+    val univ = U.certify ctxt (mk_univ dT)
+  in Thm.mk_binop inv univ ct end
+
+fun mk_inj_prop ctxt ct =
+  let
+    val (dT, rT) = U.split_type (U.typ_of ct)
+    val inj = U.certify ctxt (mk_inj_on dT rT)
+    val univ = U.certify ctxt (mk_univ dT)
+  in U.mk_cprop (Thm.mk_binop inj ct univ) end
+
+
+val disjE = @{lemma "~P | Q ==> P ==> Q" by fast}
+
+fun prove_inj_prop ctxt def lhs =
+  let
+    val (ct, ctxt') = U.dest_all_cabs (Thm.rhs_of def) ctxt
+    val rule = disjE OF [Object_Logic.rulify (Thm.assume lhs)]
+  in
+    Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct))
+    |> apply (Tactic.rtac @{thm injI})
+    |> apply (Tactic.solve_tac [rule, rule RS @{thm sym}])
+    |> Goal.norm_result o Goal.finish ctxt'
+    |> singleton (Variable.export ctxt' ctxt)
+  end
+
+fun prove_rhs ctxt def lhs =
+  T.by_tac (
+    CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt)
+    THEN' REPEAT_ALL_NEW (Tactic.match_tac @{thms allI})
+    THEN' Tactic.rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs])) #>
+  Thm.elim_implies def
+
+
+fun expand thm ct =
+  let
+    val cpat = Thm.dest_arg (Thm.rhs_of thm)
+    val (cl, cr) = Thm.dest_binop (Thm.dest_arg (Thm.dest_arg1 ct))
+    val thm1 = Thm.instantiate (Thm.match (cpat, cl)) thm
+    val thm2 = Thm.instantiate (Thm.match (cpat, cr)) thm
+  in Conv.arg_conv (Conv.binop_conv (Conv.rewrs_conv [thm1, thm2])) ct end
+
+fun prove_lhs ctxt rhs =
+  let
+    val eq = Thm.symmetric (mk_meta_eq (Object_Logic.rulify (Thm.assume rhs)))
+  in
+    T.by_tac (
+      CONVERSION (U.prop_conv (U.binders_conv (K (expand eq)) ctxt))
+      THEN' Simplifier.simp_tac HOL_ss)
+  end
+
+
+fun mk_inv_def ctxt rhs =
+  let
+    val (ct, ctxt') = U.dest_all_cbinders (U.dest_cprop rhs) ctxt
+    val (cl, cv) = Thm.dest_binop ct
+    val (cg, (cargs, cf)) = Drule.strip_comb cl ||> split_last
+    val cu = fold_rev Thm.cabs cargs (mk_inv_of ctxt' (Thm.cabs cv cf))
+  in Thm.assume (U.mk_cequals cg cu) end
+
+fun prove_inj_eq ctxt ct =
+  let
+    val (lhs, rhs) = pairself U.mk_cprop (Thm.dest_binop (U.dest_cprop ct))
+    val lhs_thm = prove_lhs ctxt rhs lhs
+    val rhs_thm = prove_rhs ctxt (mk_inv_def ctxt rhs) lhs rhs
+  in lhs_thm COMP (rhs_thm COMP @{thm iffI}) end
+
+
+val swap_eq_thm = mk_meta_eq @{thm eq_commute}
+val swap_disj_thm = mk_meta_eq @{thm disj_commute}
+
+fun swap_conv dest eq =
+  U.if_true_conv ((op <) o pairself Term.size_of_term o dest)
+    (Conv.rewr_conv eq)
+
+val swap_eq_conv = swap_conv HOLogic.dest_eq swap_eq_thm
+val swap_disj_conv = swap_conv U.dest_disj swap_disj_thm
+
+fun norm_conv ctxt =
+  swap_eq_conv then_conv
+  Conv.arg1_conv (U.binders_conv (K swap_disj_conv) ctxt) then_conv
+  Conv.arg_conv (U.binders_conv (K swap_eq_conv) ctxt)
+
+in
+
+fun prove_injectivity ctxt =
+  T.by_tac (
+    CONVERSION (U.prop_conv (norm_conv ctxt))
+    THEN' CSUBGOAL (uncurry (Tactic.rtac o prove_inj_eq ctxt)))
+
+end
+
+end
diff -r 05f4885cbbe0 -r 23904fa13e03 src/HOL/Tools/SMT/z3_proof_parser.ML
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Tue Nov 23 23:11:06 2010 +0100
@@ -29,6 +29,7 @@
 structure Z3_Proof_Parser: Z3_PROOF_PARSER =
 struct
 
+structure U = SMT_Utils
 structure I = Z3_Interface
 
 
@@ -102,24 +103,20 @@
    context-independent modulo the current proof context to be able to
    use fast inference kernel rules during proof reconstruction. *)
 
-fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
-
 val maxidx_of = #maxidx o Thm.rep_cterm
 
 fun mk_inst ctxt vars =
   let
     val max = fold (Integer.max o fst) vars 0
     val ns = fst (Variable.variant_fixes (replicate (max + 1) var_prefix) ctxt)
-    fun mk (i, v) = (v, certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v))))
+    fun mk (i, v) = (v, U.certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v))))
   in map mk vars end
 
-val mk_prop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop})
-
 fun close ctxt (ct, vars) =
   let
     val inst = mk_inst ctxt vars
     val names = fold (Term.add_free_names o Thm.term_of o snd) inst []
-  in (mk_prop (Thm.instantiate_cterm ([], inst) ct), names) end
+  in (U.mk_cprop (Thm.instantiate_cterm ([], inst) ct), names) end
 
 
 fun mk_bound thy (i, T) =
@@ -134,10 +131,11 @@
           SOME cv => cv
         | _ => Thm.cterm_of thy (Var ((Name.uu, maxidx_of ct + 1), T)))
       fun dec (i, v) = if i = 0 then NONE else SOME (i-1, v)
-    in (Thm.capply (I.instT' cv q) (Thm.cabs cv ct), map_filter dec vars) end
+    in (Thm.capply (U.instT' cv q) (Thm.cabs cv ct), map_filter dec vars) end
 
-  val forall = I.mk_inst_pair (I.destT1 o I.destT1) @{cpat All}
-  val exists = I.mk_inst_pair (I.destT1 o I.destT1) @{cpat Ex}
+  fun quant name = U.mk_const_pat @{theory} name (U.destT1 o U.destT1)
+  val forall = quant @{const_name All}
+  val exists = quant @{const_name Ex}
 in
 fun mk_forall thy = fold_rev (mk_quant thy forall)
 fun mk_exists thy = fold_rev (mk_quant thy exists)
@@ -193,7 +191,7 @@
       |> Symtab.fold (Variable.declare_term o snd) terms
 
     fun cert @{const True} = not_false
-      | cert t = certify ctxt' t
+      | cert t = U.certify ctxt' t
 
   in (typs, Symtab.map (K cert) terms, Inttab.empty, Inttab.empty, [], ctxt') end
 
@@ -208,7 +206,7 @@
     SOME _ => cx
   | NONE => cx |> fresh_name (decl_prefix ^ n)
       |> (fn (m, (typs, terms, exprs, steps, vars, ctxt)) =>
-           let val upd = Symtab.update (n, certify ctxt (Free (m, T)))
+           let val upd = Symtab.update (n, U.certify ctxt (Free (m, T)))
            in (typs, upd terms, exprs, steps, vars, ctxt) end))
 
 fun mk_typ (typs, _, _, _, _, ctxt) (s as I.Sym (n, _)) = 
diff -r 05f4885cbbe0 -r 23904fa13e03 src/HOL/Tools/SMT/z3_proof_reconstruction.ML
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Tue Nov 23 23:11:06 2010 +0100
@@ -18,6 +18,7 @@
 structure P = Z3_Proof_Parser
 structure T = Z3_Proof_Tools
 structure L = Z3_Proof_Literals
+structure M = Z3_Proof_Methods
 
 fun z3_exn msg = raise SMT_Failure.SMT (SMT_Failure.Other_Failure
   ("Z3 proof reconstruction: " ^ msg))
@@ -141,7 +142,11 @@
   val remove_trigger = @{lemma "trigger t p == p"
     by (rule eq_reflection, rule trigger_def)}
 
-  val prep_rules = [@{thm Let_def}, remove_trigger, L.rewrite_true]
+  val remove_weight = @{lemma "weight w p == p"
+    by (rule eq_reflection, rule weight_def)}
+
+  val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight,
+    L.rewrite_true]
 
   fun rewrite_conv ctxt eqs = Simplifier.full_rewrite
     (Simplifier.context ctxt Simplifier.empty_ss addsimps eqs)
@@ -682,23 +687,29 @@
   val unfold_conv =
     Conv.arg_conv (Conv.binop_conv (Conv.try_conv T.unfold_distinct_conv))
   val prove_conj_disj_eq = T.with_conv unfold_conv L.prove_conj_disj_eq
+
+  fun assume_prems ctxt thm =
+    Assumption.add_assumes (Drule.cprems_of thm) ctxt
+    |>> (fn thms => fold Thm.elim_implies thms thm)
 in
 
-fun rewrite ctxt simpset ths = Thm o with_conv ctxt ths (try_apply ctxt [] [
-  named ctxt "conj/disj/distinct" prove_conj_disj_eq,
-  T.by_abstraction (true, false) ctxt [] (fn ctxt' => T.by_tac (
-    NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset)
-    THEN_ALL_NEW NAMED ctxt' "fast (logic)" (Classical.fast_tac HOL_cs))),
-  T.by_abstraction (false, true) ctxt [] (fn ctxt' => T.by_tac (
-    NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
-    THEN_ALL_NEW (
-      NAMED ctxt' "fast (theory)" (Classical.fast_tac HOL_cs)
-      ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
-  T.by_abstraction (true, true) ctxt [] (fn ctxt' => T.by_tac (
-    NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
-    THEN_ALL_NEW (
-      NAMED ctxt' "fast (full)" (Classical.fast_tac HOL_cs)
-      ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt'))))])
+fun rewrite simpset ths ct ctxt =
+  apfst Thm (assume_prems ctxt (with_conv ctxt ths (try_apply ctxt [] [
+    named ctxt "conj/disj/distinct" prove_conj_disj_eq,
+    T.by_abstraction (true, false) ctxt [] (fn ctxt' => T.by_tac (
+      NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset)
+      THEN_ALL_NEW NAMED ctxt' "fast (logic)" (Classical.fast_tac HOL_cs))),
+    T.by_abstraction (false, true) ctxt [] (fn ctxt' => T.by_tac (
+      NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
+      THEN_ALL_NEW (
+        NAMED ctxt' "fast (theory)" (Classical.fast_tac HOL_cs)
+        ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
+    T.by_abstraction (true, true) ctxt [] (fn ctxt' => T.by_tac (
+      NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
+      THEN_ALL_NEW (
+        NAMED ctxt' "fast (full)" (Classical.fast_tac HOL_cs)
+        ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
+    named ctxt "injectivity" (M.prove_injectivity ctxt)]) ct))
 
 end
 
@@ -789,9 +800,8 @@
       (* theory rules *)
     | (P.ThLemma _, _) =>  (* FIXME: use arguments *)
         (th_lemma cx simpset (map (thm_of o fst) ps) ct, cxp)
-    | (P.Rewrite, _) => (rewrite cx simpset [] ct, cxp)
-    | (P.RewriteStar, ps) =>
-        (rewrite cx simpset (map fst ps) ct, cxp)
+    | (P.Rewrite, _) => rewrite simpset [] ct cx ||> rpair ptab
+    | (P.RewriteStar, ps) => rewrite simpset (map fst ps) ct cx ||> rpair ptab
 
     | (P.NnfStar, _) => not_supported r
     | (P.CnfStar, _) => not_supported r
diff -r 05f4885cbbe0 -r 23904fa13e03 src/HOL/Tools/SMT/z3_proof_tools.ML
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Tue Nov 23 23:11:06 2010 +0100
@@ -9,7 +9,6 @@
   (* accessing and modifying terms *)
   val term_of: cterm -> term
   val prop_of: thm -> term
-  val mk_prop: cterm -> cterm
   val as_meta_eq: cterm -> cterm
 
   (* theorem nets *)
@@ -47,6 +46,7 @@
 structure Z3_Proof_Tools: Z3_PROOF_TOOLS =
 struct
 
+structure U = SMT_Utils
 structure I = Z3_Interface
 
 
@@ -58,12 +58,7 @@
 fun term_of ct = dest_prop (Thm.term_of ct)
 fun prop_of thm = dest_prop (Thm.prop_of thm)
 
-val mk_prop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop})
-
-val eq = I.mk_inst_pair I.destT1 @{cpat "op =="}
-fun mk_meta_eq_cterm ct cu = Thm.mk_binop (I.instT' ct eq) ct cu
-
-fun as_meta_eq ct = uncurry mk_meta_eq_cterm (Thm.dest_binop (Thm.dest_arg ct))
+fun as_meta_eq ct = uncurry U.mk_cequals (Thm.dest_binop (U.dest_cprop ct))
 
 
 
@@ -87,7 +82,7 @@
 (* proof combinators *)
 
 fun under_assumption f ct =
-  let val ct' = mk_prop ct
+  let val ct' = U.mk_cprop ct
   in Thm.implies_intr ct' (f (Thm.assume ct')) end
 
 fun with_conv conv prove ct =
@@ -112,7 +107,7 @@
   let
     val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1)
     val (cf, cvs) = Drule.strip_comb lhs
-    val eq = mk_meta_eq_cterm cf (fold_rev Thm.cabs cvs rhs)
+    val eq = U.mk_cequals cf (fold_rev Thm.cabs cvs rhs)
     fun apply cv th =
       Thm.combination th (Thm.reflexive cv)
       |> Conv.fconv_rule (Conv.arg_conv (Thm.beta_conversion false))
@@ -127,9 +122,6 @@
 
 local
 
-fun typ_of ct = #T (Thm.rep_cterm ct)
-fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
-
 fun abs_context ctxt = (ctxt, Termtab.empty, 1, false)
 
 fun context_of (ctxt, _, _, _) = ctxt
@@ -155,7 +147,8 @@
     | NONE =>
         let
           val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt
-          val cv = certify ctxt' (Free (n, map typ_of cvs' ---> typ_of ct))
+          val cv = U.certify ctxt'
+            (Free (n, map U.typ_of cvs' ---> U.typ_of ct))
           val cu = Drule.list_comb (cv, cvs')
           val e = (t, (cv, fold_rev Thm.cabs cvs' ct))
           val beta_norm' = beta_norm orelse not (null cvs')
diff -r 05f4885cbbe0 -r 23904fa13e03 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Nov 23 23:11:06 2010 +0100
@@ -403,21 +403,25 @@
                    important_message
                  else
                    ""))
-      | SOME failure => (string_for_failure failure, [])
+      | SOME failure => (string_for_failure "ATP" failure, [])
   in
     {outcome = outcome, message = message, used_facts = used_facts,
      run_time_in_msecs = msecs}
   end
 
-(* "SMT_Failure.Abnormal_Termination" carries the solver's return code.
-   Return codes 1 to 127 are application-specific, whereas (at least on
-   Unix) 128 to 255 are reserved for signals (e.g., SIGSEGV) and other
-   system codes. *)
+(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until
+   these are sorted out properly in the SMT module, we have to interpret these
+   ourselves. *)
+
+val z3_malformed_input_codes = [103, 110]
+val sigsegv_code = 139
 
 fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable
   | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
   | failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =
-    if code >= 128 then Crashed else IncompleteUnprovable
+    if member (op =) z3_malformed_input_codes code then MalformedInput
+    else if code = sigsegv_code then Crashed
+    else IncompleteUnprovable
   | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
   | failure_from_smt_failure _ = UnknownError
 
@@ -445,8 +449,7 @@
         val _ =
           if verbose then
             "SMT iteration with " ^ string_of_int num_facts ^ " fact" ^
-            plural_s num_facts ^ " for " ^ string_from_time iter_timeout ^
-            "..."
+            plural_s num_facts ^ " for " ^ string_from_time iter_timeout ^ "..."
             |> Output.urgent_message
           else
             ()
@@ -472,8 +475,8 @@
           | SOME (SMT_Failure.Abnormal_Termination code) =>
             (if verbose then
                "The SMT solver invoked with " ^ string_of_int num_facts ^
-               " fact" ^ plural_s num_facts ^ " terminated abnormally with \
-               \exit code " ^ string_of_int code ^ "."
+               " fact" ^ plural_s num_facts ^ " terminated abnormally with exit\
+               \code " ^ string_of_int code ^ "."
                |> (if debug then error else warning)
              else
                ();
@@ -493,35 +496,53 @@
       end
   in iter timeout 1 NONE (SOME 0) end
 
+(* taken from "Mirabelle" and generalized *)
+fun can_apply timeout tac state i =
+  let
+    val {context = ctxt, facts, goal} = Proof.goal state
+    val full_tac = Method.insert_tac facts i THEN tac ctxt i
+  in
+    case try (TimeLimit.timeLimit timeout (Seq.pull o full_tac)) goal of
+      SOME (SOME _) => true
+    | _ => false
+  end
+
+val smt_metis_timeout = seconds 0.5
+
+fun can_apply_metis state i ths =
+  can_apply smt_metis_timeout (fn ctxt => Metis_Tactics.metis_tac ctxt ths)
+            state i
+
 fun run_smt_solver auto remote (params as {debug, ...}) minimize_command
         ({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
   let
     val repair_context =
-      Config.put SMT_Config.verbose debug
+      Config.put Metis_Tactics.verbose debug
+      #> Config.put SMT_Config.verbose debug
       #> Config.put SMT_Config.monomorph_limit smt_monomorph_limit
     val state = state |> Proof.map_context repair_context
     val ctxt = Proof.context_of state
+    val thy = Proof.theory_of state
+    val smt_fact = Option.map (apsnd (Thm.transfer thy)) o try dest_Untranslated
     val {outcome, used_facts, run_time_in_msecs} =
-      smt_filter_loop params remote state subgoal
-                      (map_filter (try dest_Untranslated) facts)
+      smt_filter_loop params remote state subgoal (map_filter smt_fact facts)
+    val outcome = outcome |> Option.map failure_from_smt_failure
     val message =
       case outcome of
         NONE =>
-        try_command_line (proof_banner auto)
-                         (apply_on_subgoal subgoal subgoal_count ^
-                          command_call smtN (map fst used_facts)) ^
-        minimize_line minimize_command (map fst used_facts)
-      | SOME SMT_Failure.Time_Out => "Timed out."
-      | SOME (SMT_Failure.Abnormal_Termination code) =>
-        "The SMT solver terminated abnormally with exit code " ^
-        string_of_int code ^ "."
-      | SOME (SMT_Failure.Counterexample _) => "The SMT problem is unprovable."
-      | SOME SMT_Failure.Out_Of_Memory => "The SMT solver ran out of memory."
-      | SOME failure =>
-        SMT_Failure.string_of_failure ctxt failure
-    val outcome = outcome |> Option.map failure_from_smt_failure (* FIXME *)
+        let
+          val method =
+            if can_apply_metis state subgoal (map snd used_facts) then "metis"
+            else "smt"
+        in
+          try_command_line (proof_banner auto)
+                           (apply_on_subgoal subgoal subgoal_count ^
+                            command_call method (map (fst o fst) used_facts)) ^
+          minimize_line minimize_command (map (fst o fst) used_facts)
+        end
+      | SOME failure => string_for_failure "SMT solver" failure
   in
-    {outcome = outcome, used_facts = used_facts,
+    {outcome = outcome, used_facts = map fst used_facts,
      run_time_in_msecs = run_time_in_msecs, message = message}
   end