1.1 --- a/NEWS	Thu Dec 01 13:34:13 2011 +0100
     1.2 +++ b/NEWS	Thu Dec 01 13:34:14 2011 +0100
     1.3 @@ -147,7 +147,7 @@
     1.4      affecting 'rat' and 'real'.
     1.5  
     1.6  * Sledgehammer:
     1.7 -  - Added "lam_trans" option.
     1.8 +  - Added "lam_trans" and "minimize" options.
     1.9    - Renamed "slicing" ("no_slicing") option to "slice" ("dont_slice").
    1.10  
    1.11  * Metis:

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Dec 01 13:34:13 2011 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Dec 01 13:34:14 2011 +0100
     2.3 @@ -96,6 +96,7 @@
     2.4     ("isar_proof", "false"),
     2.5     ("isar_shrink_factor", "1"),
     2.6     ("slice", "true"),
     2.7 +   ("minimize", "smart"),
     2.8     ("preplay_timeout", "4")]
     2.9  
    2.10  val alias_params =
    2.11 @@ -107,7 +108,8 @@
    2.12     ("non_blocking", "blocking"),
    2.13     ("unsound", "sound"),
    2.14     ("no_isar_proof", "isar_proof"),
    2.15 -   ("dont_slice", "slice")]
    2.16 +   ("dont_slice", "slice"),
    2.17 +   ("dont_minimize", "minimize")]
    2.18  
    2.19  val params_for_minimize =
    2.20    ["debug", "verbose", "overlord", "type_enc", "sound", "lam_trans",
    2.21 @@ -290,6 +292,8 @@
    2.22      val isar_proof = lookup_bool "isar_proof"
    2.23      val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
    2.24      val slice = mode <> Auto_Try andalso lookup_bool "slice"
    2.25 +    val minimize =
    2.26 +      if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
    2.27      val timeout =
    2.28        (if mode = Auto_Try then NONE else lookup_time "timeout") |> the_timeout
    2.29      val preplay_timeout =
    2.30 @@ -302,8 +306,9 @@
    2.31       lam_trans = lam_trans, relevance_thresholds = relevance_thresholds,
    2.32       max_relevant = max_relevant, max_mono_iters = max_mono_iters,
    2.33       max_new_mono_instances = max_new_mono_instances,  isar_proof = isar_proof,
    2.34 -     isar_shrink_factor = isar_shrink_factor, slice = slice, timeout = timeout,
    2.35 -     preplay_timeout = preplay_timeout, expect = expect}
    2.36 +     isar_shrink_factor = isar_shrink_factor, slice = slice,
    2.37 +     minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
    2.38 +     expect = expect}
    2.39    end
    2.40  
    2.41  fun get_params mode = extract_params mode o default_raw_params

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Dec 01 13:34:13 2011 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Dec 01 13:34:14 2011 +0100
     3.3 @@ -66,7 +66,8 @@
     3.4         max_relevant = SOME (length facts), max_mono_iters = max_mono_iters,
     3.5         max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
     3.6         isar_shrink_factor = isar_shrink_factor, slice = false,
     3.7 -       timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
     3.8 +       minimize = SOME false, timeout = timeout,
     3.9 +       preplay_timeout = preplay_timeout, expect = ""}
    3.10      val problem =
    3.11        {state = state, goal = goal, subgoal = i, subgoal_count = n,
    3.12         facts = facts, smt_filter = NONE}

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Dec 01 13:34:13 2011 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Dec 01 13:34:14 2011 +0100
     4.3 @@ -34,6 +34,7 @@
     4.4       isar_proof: bool,
     4.5       isar_shrink_factor: int,
     4.6       slice: bool,
     4.7 +     minimize: bool option,
     4.8       timeout: Time.time,
     4.9       preplay_timeout: Time.time,
    4.10       expect: string}
    4.11 @@ -297,6 +298,7 @@
    4.12     isar_proof: bool,
    4.13     isar_shrink_factor: int,
    4.14     slice: bool,
    4.15 +   minimize: bool option,
    4.16     timeout: Time.time,
    4.17     preplay_timeout: Time.time,
    4.18     expect: string}

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Dec 01 13:34:13 2011 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Dec 01 13:34:14 2011 +0100
     5.3 @@ -75,8 +75,8 @@
     5.4  fun adjust_reconstructor_params override_params
     5.5          ({debug, verbose, overlord, blocking, provers, type_enc, sound,
     5.6           lam_trans, relevance_thresholds, max_relevant, max_mono_iters,
     5.7 -         max_new_mono_instances, isar_proof, isar_shrink_factor, slice, timeout,
     5.8 -         preplay_timeout, expect} : params) =
     5.9 +         max_new_mono_instances, isar_proof, isar_shrink_factor, slice,
    5.10 +         minimize, timeout, preplay_timeout, expect} : params) =
    5.11    let
    5.12      fun lookup_override name default_value =
    5.13        case AList.lookup (op =) override_params name of
    5.14 @@ -93,11 +93,13 @@
    5.15       relevance_thresholds = relevance_thresholds,
    5.16       max_mono_iters = max_mono_iters,
    5.17       max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
    5.18 -     isar_shrink_factor = isar_shrink_factor, slice = slice, timeout = timeout,
    5.19 -     preplay_timeout = preplay_timeout, expect = expect}
    5.20 +     isar_shrink_factor = isar_shrink_factor, slice = slice,
    5.21 +     minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
    5.22 +     expect = expect}
    5.23    end
    5.24  
    5.25 -fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...})
    5.26 +fun minimize ctxt mode name
    5.27 +             (params as {debug, verbose, isar_proof, minimize, ...})
    5.28               ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
    5.29               (result as {outcome, used_facts, run_time, preplay, message,
    5.30                           message_tail} : prover_result) =
    5.31 @@ -106,7 +108,7 @@
    5.32    else
    5.33      let
    5.34        val num_facts = length used_facts
    5.35 -      val ((minimize, (minimize_name, params)), preplay) =
    5.36 +      val ((perhaps_minimize, (minimize_name, params)), preplay) =
    5.37          if mode = Normal then
    5.38            if num_facts >= Config.get ctxt auto_minimize_min_facts then
    5.39              ((true, (name, params)), preplay)
    5.40 @@ -116,10 +118,10 @@
    5.41                  0.001
    5.42                  * Real.fromInt ((num_facts + 1) * Time.toMilliseconds time)
    5.43                  <= Config.get ctxt auto_minimize_max_time
    5.44 -              val prover_fast_enough = can_min_fast_enough run_time
    5.45 +              fun prover_fast_enough () = can_min_fast_enough run_time
    5.46              in
    5.47                if isar_proof then
    5.48 -                ((prover_fast_enough, (name, params)), preplay)
    5.49 +                ((prover_fast_enough (), (name, params)), preplay)
    5.50                else
    5.51                  let val preplay = preplay () in
    5.52                    (case preplay of
    5.53 @@ -130,13 +132,14 @@
    5.54                                        adjust_reconstructor_params
    5.55                                            override_params params))
    5.56                       else
    5.57 -                       (prover_fast_enough, (name, params))
    5.58 -                   | _ => (prover_fast_enough, (name, params)),
    5.59 +                       (prover_fast_enough (), (name, params))
    5.60 +                   | _ => (prover_fast_enough (), (name, params)),
    5.61                     K preplay)
    5.62                  end
    5.63              end
    5.64          else
    5.65            ((false, (name, params)), preplay)
    5.66 +      val minimize = minimize |> the_default perhaps_minimize
    5.67        val (used_facts, (preplay, message, _)) =
    5.68          if minimize then
    5.69            minimize_facts minimize_name params (not verbose) subgoal