1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Jul 18 08:44:04 2012 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Jul 18 08:44:04 2012 +0200
     1.3 @@ -367,7 +367,7 @@
     1.4        handle List.Empty => error "No ATP available."
     1.5      fun get_prover name =
     1.6        (name, Sledgehammer_Minimize.get_minimizing_prover ctxt
     1.7 -                Sledgehammer_Provers.Normal name)
     1.8 +                Sledgehammer_Provers.Normal (K ()) name)
     1.9    in
    1.10      (case AList.lookup (op =) args proverK of
    1.11        SOME name => get_prover name
    1.12 @@ -597,7 +597,7 @@
    1.13        |> max_new_mono_instancesLST
    1.14        |> max_mono_itersLST)
    1.15      val minimize =
    1.16 -      Sledgehammer_Minimize.minimize_facts prover_name params
    1.17 +      Sledgehammer_Minimize.minimize_facts (K ()) prover_name params
    1.18            true 1 (Sledgehammer_Util.subgoal_count st)
    1.19      val _ = log separator
    1.20      val (used_facts, (preplay, message, message_tail)) =

     2.1 --- a/src/HOL/TPTP/mash_eval.ML	Wed Jul 18 08:44:04 2012 +0200
     2.2 +++ b/src/HOL/TPTP/mash_eval.ML	Wed Jul 18 08:44:04 2012 +0200
     2.3 @@ -90,7 +90,8 @@
     2.4                facts
     2.5                |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t
     2.6                |> take (the max_facts)
     2.7 -            val res as {outcome, ...} = run_prover ctxt params prover facts goal
     2.8 +            val res as {outcome, ...} =
     2.9 +              run_prover_for_mash ctxt params prover facts goal
    2.10              val _ = if is_none outcome then ok := !ok + 1 else ()
    2.11            in str_of_res heading facts res end
    2.12          val iter_s = prove iter_ok iterN iter_facts

     3.1 --- a/src/HOL/TPTP/mash_export.ML	Wed Jul 18 08:44:04 2012 +0200
     3.2 +++ b/src/HOL/TPTP/mash_export.ML	Wed Jul 18 08:44:04 2012 +0200
     3.3 @@ -146,7 +146,7 @@
     3.4                        |> fold (add_isa_dep facts) isa_deps
     3.5                        |> map fix_name
     3.6              in
     3.7 -              case run_prover ctxt params prover facts goal of
     3.8 +              case run_prover_for_mash ctxt params prover facts goal of
     3.9                  {outcome = NONE, used_facts, ...} =>
    3.10                  used_facts |> map fst |> sort string_ord
    3.11                | _ => isa_deps

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
     4.3 @@ -25,8 +25,9 @@
     4.4    val unescape_meta : string -> string
     4.5    val unescape_metas : string -> string list
     4.6    val extract_query : string -> string * string list
     4.7 -  val suggested_facts : string list -> fact list -> fact list
     4.8 -  val mesh_facts : int -> (fact list * fact list) list -> fact list
     4.9 +  val suggested_facts : string list -> ('a * thm) list -> ('a * thm) list
    4.10 +  val mesh_facts :
    4.11 +    int -> (('a * thm) list * ('a * thm) list) list -> ('a * thm) list
    4.12    val is_likely_tautology : Proof.context -> string -> thm -> bool
    4.13    val is_too_meta : thm -> bool
    4.14    val theory_ord : theory * theory -> order
    4.15 @@ -35,7 +36,7 @@
    4.16      Proof.context -> string -> theory -> status -> term list -> string list
    4.17    val isabelle_dependencies_of : unit Symtab.table -> thm -> string list
    4.18    val goal_of_thm : theory -> thm -> thm
    4.19 -  val run_prover :
    4.20 +  val run_prover_for_mash :
    4.21      Proof.context -> params -> string -> fact list -> thm -> prover_result
    4.22    val mash_RESET : Proof.context -> unit
    4.23    val mash_INIT :
    4.24 @@ -48,14 +49,14 @@
    4.25      Proof.context -> bool -> int -> string list * string list -> string list
    4.26    val mash_reset : Proof.context -> unit
    4.27    val mash_could_suggest_facts : unit -> bool
    4.28 -  val mash_can_suggest_facts : unit -> bool
    4.29 +  val mash_can_suggest_facts : Proof.context -> bool
    4.30    val mash_suggest_facts :
    4.31 -    Proof.context -> params -> string -> int -> term list -> term -> fact list
    4.32 -    -> fact list * fact list
    4.33 +    Proof.context -> params -> string -> int -> term list -> term
    4.34 +    -> ('a * thm) list -> ('a * thm) list * ('a * thm) list
    4.35    val mash_learn_thy :
    4.36      Proof.context -> params -> theory -> Time.time -> fact list -> string
    4.37    val mash_learn_proof :
    4.38 -    Proof.context -> params -> term -> thm list -> fact list -> unit
    4.39 +    Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit
    4.40    val relevant_facts :
    4.41      Proof.context -> params -> string -> int -> fact_override -> term list
    4.42      -> term -> fact list -> fact list
    4.43 @@ -300,13 +301,13 @@
    4.44  
    4.45  fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init
    4.46  
    4.47 -fun run_prover ctxt params prover facts goal =
    4.48 +fun run_prover_for_mash ctxt params prover facts goal =
    4.49    let
    4.50      val problem =
    4.51        {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
    4.52         facts = facts |> map (apfst (apfst (fn name => name ())))
    4.53                       |> map Untranslated_Fact}
    4.54 -    val prover = get_minimizing_prover ctxt Normal prover
    4.55 +    val prover = get_minimizing_prover ctxt Normal (K ()) prover
    4.56    in prover params (K (K (K ""))) problem end
    4.57  
    4.58  
    4.59 @@ -406,6 +407,15 @@
    4.60  
    4.61  (*** High-level communication with MaSh ***)
    4.62  
    4.63 +fun try_graph ctxt when def f =
    4.64 +  f ()
    4.65 +  handle Graph.CYCLES (cycle :: _) =>
    4.66 +         (trace_msg ctxt (fn () =>
    4.67 +              "Cycle involving " ^ commas cycle ^ " when " ^ when); def)
    4.68 +       | Graph.UNDEF name =>
    4.69 +         (trace_msg ctxt (fn () =>
    4.70 +              "Unknown fact " ^ quote name ^ " when " ^ when); def)
    4.71 +
    4.72  type mash_state =
    4.73    {thys : bool Symtab.table,
    4.74     fact_graph : unit Graph.T}
    4.75 @@ -414,8 +424,8 @@
    4.76  
    4.77  local
    4.78  
    4.79 -fun mash_load (state as (true, _)) = state
    4.80 -  | mash_load _ =
    4.81 +fun mash_load _ (state as (true, _)) = state
    4.82 +  | mash_load ctxt _ =
    4.83      let val path = mash_state_path () in
    4.84        (true,
    4.85         case try File.read_lines path of
    4.86 @@ -431,7 +441,9 @@
    4.87             val thys =
    4.88               Symtab.empty |> fold (add_thy true) (unescape_metas comp_thys)
    4.89                            |> fold (add_thy false) (unescape_metas incomp_thys)
    4.90 -           val fact_graph = Graph.empty |> fold add_fact_line fact_lines
    4.91 +           val fact_graph =
    4.92 +             try_graph ctxt "loading state file" Graph.empty (fn () =>
    4.93 +                 Graph.empty |> fold add_fact_line fact_lines)
    4.94           in {thys = thys, fact_graph = fact_graph} end
    4.95         | _ => empty_state)
    4.96      end
    4.97 @@ -456,10 +468,11 @@
    4.98  
    4.99  in
   4.100  
   4.101 -fun mash_map f =
   4.102 -  Synchronized.change global_state (mash_load ##> (f #> tap mash_save))
   4.103 +fun mash_map ctxt f =
   4.104 +  Synchronized.change global_state (mash_load ctxt ##> (f #> tap mash_save))
   4.105  
   4.106 -fun mash_get () = Synchronized.change_result global_state (mash_load #> `snd)
   4.107 +fun mash_get ctxt =
   4.108 +  Synchronized.change_result global_state (mash_load ctxt #> `snd)
   4.109  
   4.110  fun mash_reset ctxt =
   4.111    Synchronized.change global_state (fn _ =>
   4.112 @@ -469,17 +482,22 @@
   4.113  end
   4.114  
   4.115  fun mash_could_suggest_facts () = mash_home () <> ""
   4.116 -fun mash_can_suggest_facts () = not (Graph.is_empty (#fact_graph (mash_get ())))
   4.117 +fun mash_can_suggest_facts ctxt =
   4.118 +  not (Graph.is_empty (#fact_graph (mash_get ctxt)))
   4.119  
   4.120 -fun parents_wrt_facts facts fact_graph =
   4.121 +fun parents_wrt_facts ctxt facts fact_graph =
   4.122    let
   4.123      val graph_facts = Symtab.make (map (rpair ()) (Graph.keys fact_graph))
   4.124      val facts =
   4.125 -      [] |> fold (cons o Thm.get_name_hint o snd) facts
   4.126 -         |> filter (Symtab.defined graph_facts)
   4.127 -         |> Graph.all_preds fact_graph
   4.128 +      try_graph ctxt "when computing ancestor facts" [] (fn () =>
   4.129 +          [] |> fold (cons o Thm.get_name_hint o snd) facts
   4.130 +             |> filter (Symtab.defined graph_facts)
   4.131 +             |> Graph.all_preds fact_graph)
   4.132      val facts = Symtab.empty |> fold (fn name => Symtab.update (name, ())) facts
   4.133 -  in fact_graph |> Graph.restrict (Symtab.defined facts) |> Graph.maximals end
   4.134 +  in
   4.135 +    try_graph ctxt "when computing parent facts" [] (fn () =>
   4.136 +        fact_graph |> Graph.restrict (Symtab.defined facts) |> Graph.maximals)
   4.137 +  end
   4.138  
   4.139  (* Generate more suggestions than requested, because some might be thrown out
   4.140     later for various reasons and "meshing" gives better results with some
   4.141 @@ -493,8 +511,8 @@
   4.142                         concl_t facts =
   4.143    let
   4.144      val thy = Proof_Context.theory_of ctxt
   4.145 -    val fact_graph = #fact_graph (mash_get ())
   4.146 -    val parents = parents_wrt_facts facts fact_graph
   4.147 +    val fact_graph = #fact_graph (mash_get ctxt)
   4.148 +    val parents = parents_wrt_facts ctxt facts fact_graph
   4.149      val feats = features_of ctxt prover thy General (concl_t :: hyp_ts)
   4.150      val suggs =
   4.151        if Graph.is_empty fact_graph then []
   4.152 @@ -511,13 +529,9 @@
   4.153  fun update_fact_graph ctxt (name, parents, feats, deps) (upds, graph) =
   4.154    let
   4.155      fun maybe_add_from from (accum as (parents, graph)) =
   4.156 -      (from :: parents, Graph.add_edge_acyclic (from, name) graph)
   4.157 -      handle Graph.CYCLES _ =>
   4.158 -             (trace_msg ctxt (fn () =>
   4.159 -                  "Cycle between " ^ quote from ^ " and " ^ quote name); accum)
   4.160 -           | Graph.UNDEF _ =>
   4.161 -             (trace_msg ctxt (fn () => "Unknown node " ^ quote from); accum)
   4.162 -    val graph = graph |> Graph.new_node (name, ())
   4.163 +      try_graph ctxt "updating graph" accum (fn () =>
   4.164 +          (from :: parents, Graph.add_edge_acyclic (from, name) graph))
   4.165 +    val graph = graph |> Graph.default_node (name, ())
   4.166      val (parents, graph) = ([], graph) |> fold maybe_add_from parents
   4.167      val (deps, graph) = ([], graph) |> fold maybe_add_from deps
   4.168    in ((name, parents, feats, deps) :: upds, graph) end
   4.169 @@ -532,7 +546,7 @@
   4.170      val prover = hd provers
   4.171      fun timed_out frac =
   4.172        Time.> (Timer.checkRealTimer timer, time_mult frac timeout)
   4.173 -    val {fact_graph, ...} = mash_get ()
   4.174 +    val {fact_graph, ...} = mash_get ctxt
   4.175      val new_facts =
   4.176        facts |> filter_out (is_fact_in_graph fact_graph)
   4.177              |> sort (thm_ord o pairself snd)
   4.178 @@ -554,7 +568,7 @@
   4.179                val deps = isabelle_dependencies_of all_names th
   4.180                val upd = (name, parents, feats, deps)
   4.181              in (([name], upd :: upds), timed_out pass1_learn_timeout_factor) end
   4.182 -        val parents = parents_wrt_facts facts fact_graph
   4.183 +        val parents = parents_wrt_facts ctxt facts fact_graph
   4.184          val ((_, upds), _) =
   4.185            ((parents, []), false) |> fold do_fact new_facts |>> apsnd rev
   4.186          val n = length upds
   4.187 @@ -570,7 +584,7 @@
   4.188                fact_graph = fact_graph})
   4.189            end
   4.190        in
   4.191 -        mash_map trans;
   4.192 +        mash_map ctxt trans;
   4.193          if verbose then
   4.194            "Processed " ^ string_of_int n ^ " proof" ^ plural_s n ^
   4.195            (if verbose then
   4.196 @@ -582,7 +596,7 @@
   4.197        end
   4.198    end
   4.199  
   4.200 -fun mash_learn_proof ctxt ({provers, overlord, ...} : params) t used_ths facts =
   4.201 +fun mash_learn_proof ctxt ({provers, overlord, ...} : params) t facts used_ths =
   4.202    let
   4.203      val thy = Proof_Context.theory_of ctxt
   4.204      val prover = hd provers
   4.205 @@ -590,9 +604,9 @@
   4.206      val feats = features_of ctxt prover thy General [t]
   4.207      val deps = used_ths |> map Thm.get_name_hint
   4.208    in
   4.209 -    mash_map (fn {thys, fact_graph} =>
   4.210 +    mash_map ctxt (fn {thys, fact_graph} =>
   4.211          let
   4.212 -          val parents = parents_wrt_facts facts fact_graph
   4.213 +          val parents = parents_wrt_facts ctxt facts fact_graph
   4.214            val upds = [(name, parents, feats, deps)]
   4.215            val (upds, fact_graph) =
   4.216              ([], fact_graph) |> fold (update_fact_graph ctxt) upds
   4.217 @@ -608,19 +622,19 @@
   4.218  val short_learn_timeout_factor = 0.2
   4.219  val long_learn_timeout_factor = 4.0
   4.220  
   4.221 -fun relevant_facts ctxt (params as {fact_filter, timeout, ...}) prover max_facts
   4.222 -        ({add, only, ...} : fact_override) hyp_ts concl_t facts =
   4.223 +fun relevant_facts ctxt (params as {learn, fact_filter, timeout, ...}) prover
   4.224 +        max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts =
   4.225    if not (subset (op =) (the_list fact_filter, fact_filters)) then
   4.226      error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
   4.227    else if only then
   4.228      facts
   4.229 -  else if max_facts <= 0 then
   4.230 +  else if max_facts <= 0 orelse null facts then
   4.231      []
   4.232    else
   4.233      let
   4.234        val thy = Proof_Context.theory_of ctxt
   4.235        fun maybe_learn can_suggest =
   4.236 -        if Async_Manager.has_running_threads MaShN orelse null facts then
   4.237 +        if not learn orelse Async_Manager.has_running_threads MaShN then
   4.238            ()
   4.239          else if Time.toSeconds timeout >= min_secs_for_learning then
   4.240            let
   4.241 @@ -642,10 +656,10 @@
   4.242        val fact_filter =
   4.243          case fact_filter of
   4.244            SOME ff =>
   4.245 -          (if ff <> iterN then maybe_learn (mash_can_suggest_facts ()) else ();
   4.246 -           ff)
   4.247 +          (if ff <> iterN then maybe_learn (mash_can_suggest_facts ctxt)
   4.248 +           else (); ff)
   4.249          | NONE =>
   4.250 -          if mash_can_suggest_facts () then (maybe_learn true; meshN)
   4.251 +          if mash_can_suggest_facts ctxt then (maybe_learn true; meshN)
   4.252            else if mash_could_suggest_facts () then (maybe_learn false; iterN)
   4.253            else iterN
   4.254        val add_ths = Attrib.eval_thms ctxt add

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:04 2012 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:04 2012 +0200
     5.3 @@ -86,6 +86,7 @@
     5.4     ("strict", "false"),
     5.5     ("lam_trans", "smart"),
     5.6     ("uncurried_aliases", "smart"),
     5.7 +   ("learn", "true"),
     5.8     ("fact_filter", "smart"),
     5.9     ("max_facts", "smart"),
    5.10     ("fact_thresholds", "0.45 0.85"),
    5.11 @@ -108,6 +109,7 @@
    5.12     ("non_blocking", "blocking"),
    5.13     ("non_strict", "strict"),
    5.14     ("no_uncurried_aliases", "uncurried_aliases"),
    5.15 +   ("dont_learn", "learn"),
    5.16     ("no_isar_proof", "isar_proof"),
    5.17     ("dont_slice", "slice"),
    5.18     ("dont_minimize", "minimize")]
    5.19 @@ -296,6 +298,7 @@
    5.20      val strict = mode = Auto_Try orelse lookup_bool "strict"
    5.21      val lam_trans = lookup_option lookup_string "lam_trans"
    5.22      val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases"
    5.23 +    val learn = lookup_bool "learn"
    5.24      val fact_filter = lookup_option lookup_string "fact_filter"
    5.25      val max_facts = lookup_option lookup_int "max_facts"
    5.26      val fact_thresholds = lookup_real_pair "fact_thresholds"
    5.27 @@ -317,7 +320,7 @@
    5.28      {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
    5.29       provers = provers, type_enc = type_enc, strict = strict,
    5.30       lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
    5.31 -     fact_filter = fact_filter, max_facts = max_facts,
    5.32 +     learn = learn, fact_filter = fact_filter, max_facts = max_facts,
    5.33       fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
    5.34       max_new_mono_instances = max_new_mono_instances,  isar_proof = isar_proof,
    5.35       isar_shrink_factor = isar_shrink_factor, slice = slice,
    5.36 @@ -371,7 +374,7 @@
    5.37        run_minimize (get_params Minimize ctxt
    5.38                                 (("provers", [default_minimize_prover]) ::
    5.39                                  override_params))
    5.40 -                   (the_default 1 opt_i) (#add fact_override) state
    5.41 +                   (K ()) (the_default 1 opt_i) (#add fact_override) state
    5.42      else if subcommand = messagesN then
    5.43        messages opt_i
    5.44      else if subcommand = supported_proversN then

     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Jul 18 08:44:04 2012 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Jul 18 08:44:04 2012 +0200
     6.3 @@ -17,13 +17,15 @@
     6.4    val auto_minimize_min_facts : int Config.T
     6.5    val auto_minimize_max_time : real Config.T
     6.6    val minimize_facts :
     6.7 -    string -> params -> bool -> int -> int -> Proof.state
     6.8 +    (thm list -> unit) -> string -> params -> bool -> int -> int -> Proof.state
     6.9      -> ((string * stature) * thm list) list
    6.10      -> ((string * stature) * thm list) list option
    6.11         * ((unit -> play) * (play -> string) * string)
    6.12 -  val get_minimizing_prover : Proof.context -> mode -> string -> prover
    6.13 +  val get_minimizing_prover :
    6.14 +    Proof.context -> mode -> (thm list -> unit) -> string -> prover
    6.15    val run_minimize :
    6.16 -    params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit
    6.17 +    params -> (thm list -> unit) -> int -> (Facts.ref * Attrib.src list) list
    6.18 +    -> Proof.state -> unit
    6.19  end;
    6.20  
    6.21  structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =
    6.22 @@ -68,7 +70,7 @@
    6.23        {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
    6.24         provers = provers, type_enc = type_enc, strict = strict,
    6.25         lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
    6.26 -       fact_filter = NONE, max_facts = SOME (length facts),
    6.27 +       learn = false, fact_filter = NONE, max_facts = SOME (length facts),
    6.28         fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters,
    6.29         max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
    6.30         isar_shrink_factor = isar_shrink_factor, slice = false,
    6.31 @@ -181,8 +183,8 @@
    6.32      | p => p
    6.33    end
    6.34  
    6.35 -fun minimize_facts prover_name (params as {timeout, ...}) silent i n state
    6.36 -                   facts =
    6.37 +fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent
    6.38 +                   i n state facts =
    6.39    let
    6.40      val ctxt = Proof.context_of state
    6.41      val prover =
    6.42 @@ -202,13 +204,16 @@
    6.43               linear_minimize
    6.44           val (min_facts, {preplay, message, message_tail, ...}) =
    6.45             min test (new_timeout timeout run_time) result facts
    6.46 -         val _ = print silent (fn () => cat_lines
    6.47 -           ["Minimized to " ^ n_facts (map fst min_facts)] ^
    6.48 -            (case min_facts |> filter (fn ((_, (sc, _)), _) => sc = Chained)
    6.49 -                            |> length of
    6.50 -               0 => ""
    6.51 -             | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".")
    6.52 -       in (SOME min_facts, (preplay, message, message_tail)) end
    6.53 +       in
    6.54 +         print silent (fn () => cat_lines
    6.55 +             ["Minimized to " ^ n_facts (map fst min_facts)] ^
    6.56 +              (case min_facts |> filter (fn ((_, (sc, _)), _) => sc = Chained)
    6.57 +                              |> length of
    6.58 +                 0 => ""
    6.59 +               | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".");
    6.60 +         (if learn then do_learn (maps snd min_facts) else ());
    6.61 +         (SOME min_facts, (preplay, message, message_tail))
    6.62 +       end
    6.63       | {outcome = SOME TimedOut, preplay, ...} =>
    6.64         (NONE,
    6.65          (preplay,
    6.66 @@ -225,9 +230,10 @@
    6.67  
    6.68  fun adjust_reconstructor_params override_params
    6.69          ({debug, verbose, overlord, blocking, provers, type_enc, strict,
    6.70 -         lam_trans, uncurried_aliases, fact_filter, max_facts, fact_thresholds,
    6.71 -         max_mono_iters, max_new_mono_instances, isar_proof, isar_shrink_factor,
    6.72 -         slice, minimize, timeout, preplay_timeout, expect} : params) =
    6.73 +         lam_trans, uncurried_aliases, learn, fact_filter, max_facts,
    6.74 +         fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proof,
    6.75 +         isar_shrink_factor, slice, minimize, timeout, preplay_timeout, expect}
    6.76 +         : params) =
    6.77    let
    6.78      fun lookup_override name default_value =
    6.79        case AList.lookup (op =) override_params name of
    6.80 @@ -241,7 +247,7 @@
    6.81      {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
    6.82       provers = provers, type_enc = type_enc, strict = strict,
    6.83       lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
    6.84 -     fact_filter = fact_filter, max_facts = max_facts,
    6.85 +     learn = learn, fact_filter = fact_filter, max_facts = max_facts,
    6.86       fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
    6.87       max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
    6.88       isar_shrink_factor = isar_shrink_factor, slice = slice,
    6.89 @@ -249,7 +255,7 @@
    6.90       expect = expect}
    6.91    end
    6.92  
    6.93 -fun minimize ctxt mode name
    6.94 +fun minimize ctxt mode do_learn name
    6.95               (params as {debug, verbose, isar_proof, minimize, ...})
    6.96               ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
    6.97               (result as {outcome, used_facts, run_time, preplay, message,
    6.98 @@ -293,7 +299,7 @@
    6.99        val minimize = minimize |> the_default perhaps_minimize
   6.100        val (used_facts, (preplay, message, _)) =
   6.101          if minimize then
   6.102 -          minimize_facts minimize_name params (not verbose) subgoal
   6.103 +          minimize_facts do_learn minimize_name params (not verbose) subgoal
   6.104                           subgoal_count state
   6.105                           (filter_used_facts used_facts
   6.106                                (map (apsnd single o untranslated_fact) facts))
   6.107 @@ -319,11 +325,12 @@
   6.108        | NONE => result
   6.109      end
   6.110  
   6.111 -fun get_minimizing_prover ctxt mode name params minimize_command problem =
   6.112 +fun get_minimizing_prover ctxt mode do_learn name params minimize_command
   6.113 +                          problem =
   6.114    get_prover ctxt mode name params minimize_command problem
   6.115 -  |> minimize ctxt mode name params problem
   6.116 +  |> minimize ctxt mode do_learn name params problem
   6.117  
   6.118 -fun run_minimize (params as {provers, ...}) i refs state =
   6.119 +fun run_minimize (params as {provers, ...}) do_learn i refs state =
   6.120    let
   6.121      val ctxt = Proof.context_of state
   6.122      val reserved = reserved_isar_keyword_table ()
   6.123 @@ -339,7 +346,7 @@
   6.124               [] => error "No prover is set."
   6.125             | prover :: _ =>
   6.126               (kill_provers ();
   6.127 -              minimize_facts prover params false i n state facts
   6.128 +              minimize_facts do_learn prover params false i n state facts
   6.129                |> (fn (_, (preplay, message, message_tail)) =>
   6.130                       message (preplay ()) ^ message_tail
   6.131                       |> Output.urgent_message))

     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jul 18 08:44:04 2012 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jul 18 08:44:04 2012 +0200
     7.3 @@ -18,27 +18,28 @@
     7.4    datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize
     7.5  
     7.6    type params =
     7.7 -    {debug: bool,
     7.8 -     verbose: bool,
     7.9 -     overlord: bool,
    7.10 -     blocking: bool,
    7.11 -     provers: string list,
    7.12 -     type_enc: string option,
    7.13 -     strict: bool,
    7.14 -     lam_trans: string option,
    7.15 -     uncurried_aliases: bool option,
    7.16 -     fact_filter: string option,
    7.17 -     max_facts: int option,
    7.18 -     fact_thresholds: real * real,
    7.19 -     max_mono_iters: int option,
    7.20 -     max_new_mono_instances: int option,
    7.21 -     isar_proof: bool,
    7.22 -     isar_shrink_factor: int,
    7.23 -     slice: bool,
    7.24 -     minimize: bool option,
    7.25 -     timeout: Time.time,
    7.26 -     preplay_timeout: Time.time,
    7.27 -     expect: string}
    7.28 +    {debug : bool,
    7.29 +     verbose : bool,
    7.30 +     overlord : bool,
    7.31 +     blocking : bool,
    7.32 +     provers : string list,
    7.33 +     type_enc : string option,
    7.34 +     strict : bool,
    7.35 +     lam_trans : string option,
    7.36 +     uncurried_aliases : bool option,
    7.37 +     learn : bool,
    7.38 +     fact_filter : string option,
    7.39 +     max_facts : int option,
    7.40 +     fact_thresholds : real * real,
    7.41 +     max_mono_iters : int option,
    7.42 +     max_new_mono_instances : int option,
    7.43 +     isar_proof : bool,
    7.44 +     isar_shrink_factor : int,
    7.45 +     slice : bool,
    7.46 +     minimize : bool option,
    7.47 +     timeout : Time.time,
    7.48 +     preplay_timeout : Time.time,
    7.49 +     expect : string}
    7.50  
    7.51    type relevance_fudge =
    7.52      {local_const_multiplier : real,
    7.53 @@ -66,19 +67,19 @@
    7.54      SMT_Weighted_Fact of (string * stature) * (int option * thm)
    7.55  
    7.56    type prover_problem =
    7.57 -    {state: Proof.state,
    7.58 -     goal: thm,
    7.59 -     subgoal: int,
    7.60 -     subgoal_count: int,
    7.61 -     facts: prover_fact list}
    7.62 +    {state : Proof.state,
    7.63 +     goal : thm,
    7.64 +     subgoal : int,
    7.65 +     subgoal_count : int,
    7.66 +     facts : prover_fact list}
    7.67  
    7.68    type prover_result =
    7.69 -    {outcome: failure option,
    7.70 -     used_facts: (string * stature) list,
    7.71 -     run_time: Time.time,
    7.72 -     preplay: unit -> play,
    7.73 -     message: play -> string,
    7.74 -     message_tail: string}
    7.75 +    {outcome : failure option,
    7.76 +     used_facts : (string * stature) list,
    7.77 +     run_time : Time.time,
    7.78 +     preplay : unit -> play,
    7.79 +     message : play -> string,
    7.80 +     message_tail : string}
    7.81  
    7.82    type prover =
    7.83      params -> ((string * string list) list -> string -> minimize_command)
    7.84 @@ -306,27 +307,28 @@
    7.85  (** problems, results, ATPs, etc. **)
    7.86  
    7.87  type params =
    7.88 -  {debug: bool,
    7.89 -   verbose: bool,
    7.90 -   overlord: bool,
    7.91 -   blocking: bool,
    7.92 -   provers: string list,
    7.93 -   type_enc: string option,
    7.94 -   strict: bool,
    7.95 -   lam_trans: string option,
    7.96 -   uncurried_aliases: bool option,
    7.97 -   fact_filter: string option,
    7.98 -   max_facts: int option,
    7.99 -   fact_thresholds: real * real,
   7.100 -   max_mono_iters: int option,
   7.101 -   max_new_mono_instances: int option,
   7.102 -   isar_proof: bool,
   7.103 -   isar_shrink_factor: int,
   7.104 -   slice: bool,
   7.105 -   minimize: bool option,
   7.106 -   timeout: Time.time,
   7.107 -   preplay_timeout: Time.time,
   7.108 -   expect: string}
   7.109 +  {debug : bool,
   7.110 +   verbose : bool,
   7.111 +   overlord : bool,
   7.112 +   blocking : bool,
   7.113 +   provers : string list,
   7.114 +   type_enc : string option,
   7.115 +   strict : bool,
   7.116 +   lam_trans : string option,
   7.117 +   uncurried_aliases : bool option,
   7.118 +   learn : bool,
   7.119 +   fact_filter : string option,
   7.120 +   max_facts : int option,
   7.121 +   fact_thresholds : real * real,
   7.122 +   max_mono_iters : int option,
   7.123 +   max_new_mono_instances : int option,
   7.124 +   isar_proof : bool,
   7.125 +   isar_shrink_factor : int,
   7.126 +   slice : bool,
   7.127 +   minimize : bool option,
   7.128 +   timeout : Time.time,
   7.129 +   preplay_timeout : Time.time,
   7.130 +   expect : string}
   7.131  
   7.132  type relevance_fudge =
   7.133    {local_const_multiplier : real,
   7.134 @@ -354,19 +356,19 @@
   7.135    SMT_Weighted_Fact of (string * stature) * (int option * thm)
   7.136  
   7.137  type prover_problem =
   7.138 -  {state: Proof.state,
   7.139 -   goal: thm,
   7.140 -   subgoal: int,
   7.141 -   subgoal_count: int,
   7.142 -   facts: prover_fact list}
   7.143 +  {state : Proof.state,
   7.144 +   goal : thm,
   7.145 +   subgoal : int,
   7.146 +   subgoal_count : int,
   7.147 +   facts : prover_fact list}
   7.148  
   7.149  type prover_result =
   7.150 -  {outcome: failure option,
   7.151 -   used_facts: (string * stature) list,
   7.152 -   run_time: Time.time,
   7.153 -   preplay: unit -> play,
   7.154 -   message: play -> string,
   7.155 -   message_tail: string}
   7.156 +  {outcome : failure option,
   7.157 +   used_facts : (string * stature) list,
   7.158 +   run_time : Time.time,
   7.159 +   preplay : unit -> play,
   7.160 +   message : play -> string,
   7.161 +   message_tail : string}
   7.162  
   7.163  type prover =
   7.164    params -> ((string * string list) list -> string -> minimize_command)

     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jul 18 08:44:04 2012 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jul 18 08:44:04 2012 +0200
     8.3 @@ -86,7 +86,10 @@
     8.4                 |> take num_facts}
     8.5      fun really_go () =
     8.6        problem
     8.7 -      |> get_minimizing_prover ctxt mode name params minimize_command
     8.8 +      |> get_minimizing_prover ctxt mode
     8.9 +             (mash_learn_proof ctxt params (prop_of goal)
    8.10 +                               (map untranslated_fact facts))
    8.11 +             name params minimize_command
    8.12        |> (fn {outcome, preplay, message, message_tail, ...} =>
    8.13               (if outcome = SOME ATP_Proof.TimedOut then timeoutN
    8.14                else if is_some outcome then noneN