minimize SMT proofs with E if Isar proofs are desired and Metis managed to preplay

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Feb 20 13:04:03 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Feb 20 14:10:51 2013 +0100
@@ -189,20 +189,6 @@
   fun merge data : T = AList.merge (op =) (K true) data
 )
 
-fun remotify_prover_if_supported_and_not_already_remote ctxt name =
-  if String.isPrefix remote_prefix name then
-    SOME name
-  else
-    let val remote_name = remote_prefix ^ name in
-      if is_prover_supported ctxt remote_name then SOME remote_name else NONE
-    end
-
-fun remotify_prover_if_not_installed ctxt name =
-  if is_prover_supported ctxt name andalso is_prover_installed ctxt name then
-    SOME name
-  else
-    remotify_prover_if_supported_and_not_already_remote ctxt name
-
 fun avoid_too_many_threads _ _ [] = []
   | avoid_too_many_threads _ (0, 0) _ = []
   | avoid_too_many_threads ctxt (0, max_remote) provers =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Feb 20 13:04:03 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Feb 20 14:10:51 2013 +0100
@@ -35,6 +35,7 @@
 open ATP_Util
 open ATP_Proof
 open ATP_Problem_Generate
+open ATP_Systems
 open Sledgehammer_Util
 open Sledgehammer_Fact
 open Sledgehammer_Reconstruct
@@ -296,9 +297,10 @@
               (case Lazy.force preplay of
                  Played (reconstr as Metis _, timeout) =>
                  if isar_proofs = SOME true then
-                   (* Cheat: Assume the original prover is as fast as "metis"
-                      for the goal it proved itself. *)
-                   (can_min_fast_enough timeout, (name, params))
+                   (* Cheat: Assume the selected ATP is as fast as "metis" for
+                      the goal it proved itself. *)
+                   (can_min_fast_enough timeout,
+                    (isar_proof_reconstructor ctxt name, params))
                  else if can_min_fast_enough timeout then
                    (true, extract_reconstructor params reconstr
                           ||> (fn override_params =>
@@ -334,14 +336,10 @@
       | NONE => result
     end
 
-(* TODO: implement *)
-fun maybe_regenerate_isar_proof result = result
-
 fun get_minimizing_prover ctxt mode do_learn name params minimize_command
                           problem =
   get_prover ctxt mode name params minimize_command problem
   |> maybe_minimize ctxt mode do_learn name params problem
-  |> maybe_regenerate_isar_proof
 
 fun run_minimize (params as {provers, ...}) do_learn i refs state =
   let

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Feb 20 13:04:03 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Feb 20 14:10:51 2013 +0100
@@ -110,6 +110,10 @@
   val is_unit_equational_atp : Proof.context -> string -> bool
   val is_prover_supported : Proof.context -> string -> bool
   val is_prover_installed : Proof.context -> string -> bool
+  val remotify_prover_if_supported_and_not_already_remote :
+    Proof.context -> string -> string option
+  val remotify_prover_if_not_installed :
+    Proof.context -> string -> string option
   val default_max_facts_for_prover : Proof.context -> bool -> string -> int
   val is_unit_equality : term -> bool
   val is_appropriate_prop_for_prover : Proof.context -> string -> term -> bool
@@ -129,6 +133,7 @@
   val filter_used_facts :
     bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
     ((''a * stature) * 'b) list
+  val isar_proof_reconstructor : Proof.context -> string -> string
   val get_prover : Proof.context -> mode -> string -> prover
 end;
 
@@ -186,6 +191,20 @@
   is_reconstructor orf is_smt_prover ctxt orf
   is_atp_installed (Proof_Context.theory_of ctxt)
 
+fun remotify_prover_if_supported_and_not_already_remote ctxt name =
+  if String.isPrefix remote_prefix name then
+    SOME name
+  else
+    let val remote_name = remote_prefix ^ name in
+      if is_prover_supported ctxt remote_name then SOME remote_name else NONE
+    end
+
+fun remotify_prover_if_not_installed ctxt name =
+  if is_prover_supported ctxt name andalso is_prover_installed ctxt name then
+    SOME name
+  else
+    remotify_prover_if_supported_and_not_already_remote ctxt name
+
 fun get_slices slice slices =
   (0 upto length slices - 1) ~~ slices |> not slice ? (List.last #> single)
 
@@ -598,19 +617,26 @@
   #> type_enc_from_string soundness
   #> adjust_type_enc format
 
-val metis_minimize_max_time = seconds 2.0
+fun isar_proof_reconstructor ctxt name =
+  let val thy = Proof_Context.theory_of ctxt in
+    if is_atp thy name then name
+    else remotify_prover_if_not_installed ctxt eN |> the_default name
+  end
 
-fun choose_minimize_command params minimize_command name preplay =
+(* See the analogous logic in the function "maybe_minimize" in
+  "sledgehammer_minimize.ML". *)
+fun choose_minimize_command ctxt (params as {isar_proofs, ...}) minimize_command
+                            name preplay =
   let
-    val (name, override_params) =
+    val maybe_isar_name =
+      name |> isar_proofs = SOME true ? isar_proof_reconstructor ctxt
+    val (min_name, override_params) =
       case preplay of
-        Played (reconstr, time) =>
-        if Time.<= (time, metis_minimize_max_time) then
-          extract_reconstructor params reconstr
-        else
-          (name, [])
-      | _ => (name, [])
-  in minimize_command override_params name end
+        Played (reconstr, _) =>
+        if isar_proofs = SOME true then (maybe_isar_name, [])
+        else extract_reconstructor params reconstr
+      | _ => (maybe_isar_name, [])
+  in minimize_command override_params min_name end
 
 fun repair_monomorph_context max_iters best_max_iters max_new_instances
                              best_max_new_instances =
@@ -795,7 +821,8 @@
             fun sel_weights () = atp_problem_selection_weights atp_problem
             fun ord_info () = atp_problem_term_order_info atp_problem
             val ord = effective_term_order ctxt name
-            val full_proof = debug orelse isar_proofs = SOME true
+            val full_proof =
+              debug orelse (isar_proofs |> the_default (mode = Minimize))
             val args =
               arguments ctxt full_proof extra
                         (slice_timeout |> the_default one_day)
@@ -917,7 +944,8 @@
                    pool, fact_names, sym_tab, atp_proof, goal)
                 val one_line_params =
                   (preplay, proof_banner mode name, used_facts,
-                   choose_minimize_command params minimize_command name preplay,
+                   choose_minimize_command ctxt params minimize_command name
+                                           preplay,
                    subgoal, subgoal_count)
                 val num_chained = length (#facts (Proof.goal state))
               in
@@ -1127,7 +1155,8 @@
             let
               val one_line_params =
                 (preplay, proof_banner mode name, used_facts,
-                 choose_minimize_command params minimize_command name preplay,
+                 choose_minimize_command ctxt params minimize_command name
+                                         preplay,
                  subgoal, subgoal_count)
               val num_chained = length (#facts (Proof.goal state))
             in one_line_proof_text num_chained one_line_params end,

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Feb 20 13:04:03 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Feb 20 14:10:51 2013 +0100
@@ -375,7 +375,6 @@
       (_, []) => line :: lines
     | (pre, Inference_Step (name', _, _, _, _) :: post) =>
       line :: pre @ map (replace_dependencies_in_line (name', [name])) post
-    | _ => raise Fail "unexpected inference"
 
 val waldmeister_conjecture_num = "1.0.0.0"