1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Feb 20 13:04:03 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Feb 20 14:10:51 2013 +0100
     1.3 @@ -189,20 +189,6 @@
     1.4    fun merge data : T = AList.merge (op =) (K true) data
     1.5  )
     1.6  
     1.7 -fun remotify_prover_if_supported_and_not_already_remote ctxt name =
     1.8 -  if String.isPrefix remote_prefix name then
     1.9 -    SOME name
    1.10 -  else
    1.11 -    let val remote_name = remote_prefix ^ name in
    1.12 -      if is_prover_supported ctxt remote_name then SOME remote_name else NONE
    1.13 -    end
    1.14 -
    1.15 -fun remotify_prover_if_not_installed ctxt name =
    1.16 -  if is_prover_supported ctxt name andalso is_prover_installed ctxt name then
    1.17 -    SOME name
    1.18 -  else
    1.19 -    remotify_prover_if_supported_and_not_already_remote ctxt name
    1.20 -
    1.21  fun avoid_too_many_threads _ _ [] = []
    1.22    | avoid_too_many_threads _ (0, 0) _ = []
    1.23    | avoid_too_many_threads ctxt (0, max_remote) provers =

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Feb 20 13:04:03 2013 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Feb 20 14:10:51 2013 +0100
     2.3 @@ -35,6 +35,7 @@
     2.4  open ATP_Util
     2.5  open ATP_Proof
     2.6  open ATP_Problem_Generate
     2.7 +open ATP_Systems
     2.8  open Sledgehammer_Util
     2.9  open Sledgehammer_Fact
    2.10  open Sledgehammer_Reconstruct
    2.11 @@ -296,9 +297,10 @@
    2.12                (case Lazy.force preplay of
    2.13                   Played (reconstr as Metis _, timeout) =>
    2.14                   if isar_proofs = SOME true then
    2.15 -                   (* Cheat: Assume the original prover is as fast as "metis"
    2.16 -                      for the goal it proved itself. *)
    2.17 -                   (can_min_fast_enough timeout, (name, params))
    2.18 +                   (* Cheat: Assume the selected ATP is as fast as "metis" for
    2.19 +                      the goal it proved itself. *)
    2.20 +                   (can_min_fast_enough timeout,
    2.21 +                    (isar_proof_reconstructor ctxt name, params))
    2.22                   else if can_min_fast_enough timeout then
    2.23                     (true, extract_reconstructor params reconstr
    2.24                            ||> (fn override_params =>
    2.25 @@ -334,14 +336,10 @@
    2.26        | NONE => result
    2.27      end
    2.28  
    2.29 -(* TODO: implement *)
    2.30 -fun maybe_regenerate_isar_proof result = result
    2.31 -
    2.32  fun get_minimizing_prover ctxt mode do_learn name params minimize_command
    2.33                            problem =
    2.34    get_prover ctxt mode name params minimize_command problem
    2.35    |> maybe_minimize ctxt mode do_learn name params problem
    2.36 -  |> maybe_regenerate_isar_proof
    2.37  
    2.38  fun run_minimize (params as {provers, ...}) do_learn i refs state =
    2.39    let

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Feb 20 13:04:03 2013 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Feb 20 14:10:51 2013 +0100
     3.3 @@ -110,6 +110,10 @@
     3.4    val is_unit_equational_atp : Proof.context -> string -> bool
     3.5    val is_prover_supported : Proof.context -> string -> bool
     3.6    val is_prover_installed : Proof.context -> string -> bool
     3.7 +  val remotify_prover_if_supported_and_not_already_remote :
     3.8 +    Proof.context -> string -> string option
     3.9 +  val remotify_prover_if_not_installed :
    3.10 +    Proof.context -> string -> string option
    3.11    val default_max_facts_for_prover : Proof.context -> bool -> string -> int
    3.12    val is_unit_equality : term -> bool
    3.13    val is_appropriate_prop_for_prover : Proof.context -> string -> term -> bool
    3.14 @@ -129,6 +133,7 @@
    3.15    val filter_used_facts :
    3.16      bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
    3.17      ((''a * stature) * 'b) list
    3.18 +  val isar_proof_reconstructor : Proof.context -> string -> string
    3.19    val get_prover : Proof.context -> mode -> string -> prover
    3.20  end;
    3.21  
    3.22 @@ -186,6 +191,20 @@
    3.23    is_reconstructor orf is_smt_prover ctxt orf
    3.24    is_atp_installed (Proof_Context.theory_of ctxt)
    3.25  
    3.26 +fun remotify_prover_if_supported_and_not_already_remote ctxt name =
    3.27 +  if String.isPrefix remote_prefix name then
    3.28 +    SOME name
    3.29 +  else
    3.30 +    let val remote_name = remote_prefix ^ name in
    3.31 +      if is_prover_supported ctxt remote_name then SOME remote_name else NONE
    3.32 +    end
    3.33 +
    3.34 +fun remotify_prover_if_not_installed ctxt name =
    3.35 +  if is_prover_supported ctxt name andalso is_prover_installed ctxt name then
    3.36 +    SOME name
    3.37 +  else
    3.38 +    remotify_prover_if_supported_and_not_already_remote ctxt name
    3.39 +
    3.40  fun get_slices slice slices =
    3.41    (0 upto length slices - 1) ~~ slices |> not slice ? (List.last #> single)
    3.42  
    3.43 @@ -598,19 +617,26 @@
    3.44    #> type_enc_from_string soundness
    3.45    #> adjust_type_enc format
    3.46  
    3.47 -val metis_minimize_max_time = seconds 2.0
    3.48 +fun isar_proof_reconstructor ctxt name =
    3.49 +  let val thy = Proof_Context.theory_of ctxt in
    3.50 +    if is_atp thy name then name
    3.51 +    else remotify_prover_if_not_installed ctxt eN |> the_default name
    3.52 +  end
    3.53  
    3.54 -fun choose_minimize_command params minimize_command name preplay =
    3.55 +(* See the analogous logic in the function "maybe_minimize" in
    3.56 +  "sledgehammer_minimize.ML". *)
    3.57 +fun choose_minimize_command ctxt (params as {isar_proofs, ...}) minimize_command
    3.58 +                            name preplay =
    3.59    let
    3.60 -    val (name, override_params) =
    3.61 +    val maybe_isar_name =
    3.62 +      name |> isar_proofs = SOME true ? isar_proof_reconstructor ctxt
    3.63 +    val (min_name, override_params) =
    3.64        case preplay of
    3.65 -        Played (reconstr, time) =>
    3.66 -        if Time.<= (time, metis_minimize_max_time) then
    3.67 -          extract_reconstructor params reconstr
    3.68 -        else
    3.69 -          (name, [])
    3.70 -      | _ => (name, [])
    3.71 -  in minimize_command override_params name end
    3.72 +        Played (reconstr, _) =>
    3.73 +        if isar_proofs = SOME true then (maybe_isar_name, [])
    3.74 +        else extract_reconstructor params reconstr
    3.75 +      | _ => (maybe_isar_name, [])
    3.76 +  in minimize_command override_params min_name end
    3.77  
    3.78  fun repair_monomorph_context max_iters best_max_iters max_new_instances
    3.79                               best_max_new_instances =
    3.80 @@ -795,7 +821,8 @@
    3.81              fun sel_weights () = atp_problem_selection_weights atp_problem
    3.82              fun ord_info () = atp_problem_term_order_info atp_problem
    3.83              val ord = effective_term_order ctxt name
    3.84 -            val full_proof = debug orelse isar_proofs = SOME true
    3.85 +            val full_proof =
    3.86 +              debug orelse (isar_proofs |> the_default (mode = Minimize))
    3.87              val args =
    3.88                arguments ctxt full_proof extra
    3.89                          (slice_timeout |> the_default one_day)
    3.90 @@ -917,7 +944,8 @@
    3.91                     pool, fact_names, sym_tab, atp_proof, goal)
    3.92                  val one_line_params =
    3.93                    (preplay, proof_banner mode name, used_facts,
    3.94 -                   choose_minimize_command params minimize_command name preplay,
    3.95 +                   choose_minimize_command ctxt params minimize_command name
    3.96 +                                           preplay,
    3.97                     subgoal, subgoal_count)
    3.98                  val num_chained = length (#facts (Proof.goal state))
    3.99                in
   3.100 @@ -1127,7 +1155,8 @@
   3.101              let
   3.102                val one_line_params =
   3.103                  (preplay, proof_banner mode name, used_facts,
   3.104 -                 choose_minimize_command params minimize_command name preplay,
   3.105 +                 choose_minimize_command ctxt params minimize_command name
   3.106 +                                         preplay,
   3.107                   subgoal, subgoal_count)
   3.108                val num_chained = length (#facts (Proof.goal state))
   3.109              in one_line_proof_text num_chained one_line_params end,

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