1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 10:14:18 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 10:14:18 2014 +0100
     1.3 @@ -296,7 +296,7 @@
     1.4  
     1.5          fun str_of_meth l meth =
     1.6            string_of_proof_method meth ^ " " ^
     1.7 -          str_of_preplay_outcome (preplay_outcome_of_isar_step (!preplay_data) l meth)
     1.8 +          str_of_preplay_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)
     1.9          fun comment_of l = map (str_of_meth l) #> commas
    1.10  
    1.11          fun trace_isar_proof label proof =
    1.12 @@ -314,7 +314,8 @@
    1.13            |> try0_isar ? try0_isar_proof ctxt preplay_timeout preplay_data
    1.14            |> tap (trace_isar_proof "Tried0")
    1.15            |> postprocess_isar_proof_remove_unreferenced_steps
    1.16 -               (try0_isar ? minimize_isar_step_dependencies ctxt preplay_data)
    1.17 +               (keep_fastest_method_of_isar_step (!preplay_data)
    1.18 +                #> try0_isar(*### minimize*) ? minimize_isar_step_dependencies ctxt preplay_data)
    1.19            |> tap (trace_isar_proof "Minimized")
    1.20            |> `(preplay_outcome_of_isar_proof (!preplay_data))
    1.21            ||> chain_isar_proof

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 10:14:18 2014 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 10:14:18 2014 +0100
     2.3 @@ -156,7 +156,8 @@
     2.4                  try the_single sub_steps
     2.5  
     2.6                (* only touch proofs that can be preplayed sucessfully *)
     2.7 -              val Played time' = Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l' meth')
     2.8 +              val Played time' =
     2.9 +                Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l' meth')
    2.10  
    2.11                (* merge steps *)
    2.12                val subs'' = subs @ nontriv_subs
    2.13 @@ -183,7 +184,7 @@
    2.14            if subproofs = [] then
    2.15              step
    2.16            else
    2.17 -            (case Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l meth) of
    2.18 +            (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
    2.19                Played time => elim_one_subproof time qs fix l t lfs gfs meths subproofs []
    2.20              | _ => step)
    2.21  
    2.22 @@ -223,12 +224,13 @@
    2.23                val succ_meths = map (hd o snd o the o byline_of_isar_step) succs
    2.24  
    2.25                (* only touch steps that can be preplayed successfully *)
    2.26 -              val Played time = Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l meth)
    2.27 +              val Played time =
    2.28 +                Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)
    2.29  
    2.30                val succs' = map (try_merge cand #> the) succs
    2.31  
    2.32                val times0 = map2 ((fn Played time => time) o Lazy.force oo
    2.33 -                preplay_outcome_of_isar_step (!preplay_data)) labels succ_meths
    2.34 +                preplay_outcome_of_isar_step_for_method (!preplay_data)) labels succ_meths
    2.35                val time_slice = time_mult (1.0 / (Real.fromInt (length labels))) time
    2.36                val timeouts = map (curry Time.+ time_slice #> time_mult merge_timeout_slack) times0
    2.37  

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Mon Feb 03 10:14:18 2014 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Mon Feb 03 10:14:18 2014 +0100
     3.3 @@ -11,6 +11,7 @@
     3.4    type isar_proof = Sledgehammer_Isar_Proof.isar_proof
     3.5    type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
     3.6  
     3.7 +  val keep_fastest_method_of_isar_step : isar_preplay_data -> isar_step -> isar_step
     3.8    val minimize_isar_step_dependencies : Proof.context -> isar_preplay_data Unsynchronized.ref ->
     3.9      isar_step -> isar_step
    3.10    val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof ->
    3.11 @@ -24,12 +25,16 @@
    3.12  open Sledgehammer_Isar_Proof
    3.13  open Sledgehammer_Isar_Preplay
    3.14  
    3.15 +fun keep_fastest_method_of_isar_step preplay_data
    3.16 +      (Prove (qs, xs, l, t, subproofs, (facts, _))) =
    3.17 +    Prove (qs, xs, l, t, subproofs, (facts, [fastest_method_of_isar_step preplay_data l]))
    3.18 +  | keep_fastest_method_of_isar_step _ step = step
    3.19 +
    3.20  val slack = seconds 0.1
    3.21  
    3.22 -fun minimize_isar_step_dependencies _ _ (step as Let _) = step
    3.23 -  | minimize_isar_step_dependencies ctxt preplay_data
    3.24 +fun minimize_isar_step_dependencies ctxt preplay_data
    3.25        (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths as meth :: _))) =
    3.26 -    (case Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l meth) of
    3.27 +    (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
    3.28        Played time =>
    3.29        let
    3.30          fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths))
    3.31 @@ -51,6 +56,7 @@
    3.32          step'
    3.33        end
    3.34      | _ => step (* don't touch steps that time out or fail *))
    3.35 +  | minimize_isar_step_dependencies _ _ step = step
    3.36  
    3.37  fun postprocess_isar_proof_remove_unreferenced_steps postproc_step =
    3.38    let

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 10:14:18 2014 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 10:14:18 2014 +0100
     4.3 @@ -22,8 +22,9 @@
     4.4    val set_preplay_outcomes_of_isar_step : Proof.context -> Time.time ->
     4.5      isar_preplay_data Unsynchronized.ref -> isar_step ->
     4.6      (proof_method * play_outcome Lazy.lazy) list -> unit
     4.7 -  val preplay_outcome_of_isar_step : isar_preplay_data -> label -> proof_method ->
     4.8 +  val preplay_outcome_of_isar_step_for_method : isar_preplay_data -> label -> proof_method ->
     4.9      play_outcome Lazy.lazy
    4.10 +  val fastest_method_of_isar_step : isar_preplay_data -> label -> proof_method
    4.11    val preplay_outcome_of_isar_proof : isar_preplay_data -> isar_proof -> play_outcome
    4.12  end;
    4.13  
    4.14 @@ -180,16 +181,20 @@
    4.15      end
    4.16    | set_preplay_outcomes_of_isar_step _ _ _ _ _ = ()
    4.17  
    4.18 -fun preplay_outcome_of_isar_step preplay_data l meth =
    4.19 -  (case Canonical_Label_Tab.lookup preplay_data l of
    4.20 -    SOME meths_outcomes =>
    4.21 -    (case AList.lookup (op =) meths_outcomes meth of
    4.22 -      SOME outcome => outcome
    4.23 -    | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method")
    4.24 -  | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label")
    4.25 +fun preplay_outcome_of_isar_step_for_method preplay_data l meth =
    4.26 +  let val SOME meths_outcomes = Canonical_Label_Tab.lookup preplay_data l in
    4.27 +    the (AList.lookup (op =) meths_outcomes meth)
    4.28 +  end
    4.29  
    4.30 -fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, (_, meth :: _))) =
    4.31 -    Lazy.force (preplay_outcome_of_isar_step preplay_data l meth)
    4.32 +fun fastest_method_of_isar_step preplay_data l =
    4.33 +  the (Canonical_Label_Tab.lookup preplay_data l)
    4.34 +  |> map (fn (meth, outcome) =>
    4.35 +       (meth, Time.toMilliseconds (case Lazy.force outcome of Played time => time | _ => one_year)))
    4.36 +  |> sort (int_ord o pairself snd)
    4.37 +  |> hd |> fst
    4.38 +
    4.39 +fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, (_, meths))) =
    4.40 +    Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data l (the_single meths))
    4.41    | forced_outcome_of_step _ _ = Played Time.zeroTime
    4.42  
    4.43  fun preplay_outcome_of_isar_proof preplay_data (Proof (_, _, steps)) =

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Mon Feb 03 10:14:18 2014 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Mon Feb 03 10:14:18 2014 +0100
     5.3 @@ -33,7 +33,7 @@
     5.4        (step as Prove (_, _, l, _, _, (_, meths as meth :: _))) =
     5.5      let
     5.6        val timeout =
     5.7 -        (case Lazy.force (preplay_outcome_of_isar_step (!preplay_data) l meth) of
     5.8 +        (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
     5.9            Played time => Time.+ (time, slack)
    5.10          | _ => preplay_timeout)
    5.11