eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -10,7 +10,6 @@
 sig
   type fact = Sledgehammer_Fact.fact
   type fact_override = Sledgehammer_Fact.fact_override
-  type minimize_command = Sledgehammer_Proof_Methods.minimize_command
   type mode = Sledgehammer_Prover.mode
   type params = Sledgehammer_Prover.params
 
@@ -21,8 +20,7 @@
 
   val string_of_factss : (string * fact list) list -> string
   val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override ->
-    ((string * string list) list -> string -> minimize_command) -> Proof.state ->
-    bool * (string * Proof.state)
+    Proof.state -> bool * (string * Proof.state)
 end;
 
 structure Sledgehammer : SLEDGEHAMMER =
@@ -90,7 +88,7 @@
   end
 
 fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, timeout, preplay_timeout,
-      expect, ...}) mode output_result minimize_command only learn
+      expect, ...}) mode output_result only learn
     {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name =
   let
     val ctxt = Proof.context_of state
@@ -154,7 +152,7 @@
 
     fun really_go () =
       problem
-      |> get_minimizing_prover ctxt mode learn name params minimize_command
+      |> get_minimizing_prover ctxt mode learn name params
       |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} =>
           print_used_facts used_facts used_from
         | _ => ())
@@ -235,7 +233,7 @@
       (if filter = "" then "" else quote filter ^ ": ") ^ string_of_facts facts) factss)
 
 fun run_sledgehammer (params as {verbose, spy, blocking, provers, max_facts, ...}) mode
-    output_result i (fact_override as {only, ...}) minimize_command state =
+    output_result i (fact_override as {only, ...}) state =
   if null provers then
     error "No prover is set."
   else
@@ -292,7 +290,7 @@
               {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
                factss = factss}
             val learn = mash_learn_proof ctxt params (prop_of goal) all_facts
-            val launch = launch_prover params mode output_result minimize_command only learn
+            val launch = launch_prover params mode output_result only learn
           in
             if mode = Auto_Try then
               (unknownN, state)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -31,7 +31,6 @@
 val z3N = "z3"
 
 val runN = "run"
-val minN = "min"
 val messagesN = "messages"
 val supported_proversN = "supported_provers"
 val kill_allN = "kill_all"
@@ -119,9 +118,6 @@
    ("dont_try0", "try0"),
    ("no_smt_proofs", "smt_proofs")]
 
-val params_not_for_minimize =
-  ["provers", "blocking", "fact_filter", "max_facts", "fact_thresholds", "slice", "minimize"];
-
 val property_dependent_params = ["provers", "timeout"]
 
 fun is_known_raw_param s =
@@ -318,31 +314,6 @@
 
 (* Sledgehammer the given subgoal *)
 
-fun is_raw_param_relevant_for_minimize (name, _) = not (member (op =) params_not_for_minimize name)
-
-fun string_of_raw_param (key, values) =
-  key ^ (case implode_param values of "" => "" | value => " = " ^ value)
-
-fun nice_string_of_raw_param (p as (key, ["false"])) =
-    (case AList.find (op =) negated_alias_params key of
-       [neg] => neg
-     | _ => string_of_raw_param p)
-  | nice_string_of_raw_param p = string_of_raw_param p
-
-fun minimize_command override_params i more_override_params prover_name fact_names =
-  let
-    val params =
-      (override_params |> filter_out (AList.defined (op =) more_override_params o fst)) @
-      more_override_params
-      |> filter is_raw_param_relevant_for_minimize
-      |> map nice_string_of_raw_param
-      |> cons prover_name
-      |> space_implode ", "
-  in
-    sledgehammerN ^ " " ^ minN ^ (if params = "" then "" else enclose " [" "]" params) ^
-    " (" ^ space_implode " " fact_names ^ ")" ^ (if i = 1 then "" else " " ^ string_of_int i)
-  end
-
 val default_learn_prover_timeout = 2.0
 
 fun hammer_away override_params subcommand opt_i fact_override state =
@@ -355,19 +326,9 @@
   in
     if subcommand = runN then
       let val i = the_default 1 opt_i in
-        run_sledgehammer (get_params Normal thy override_params) Normal NONE i fact_override
-          (minimize_command override_params i) state
-        |> K ()
+        ignore (run_sledgehammer (get_params Normal thy override_params) Normal NONE i fact_override
+          state)
       end
-    else if subcommand = minN then
-      let
-        val ctxt = ctxt |> Config.put instantiate_inducts false
-        val i = the_default 1 opt_i
-        val params = get_params Minimize thy override_params
-        val goal = prop_of (#goal (Proof.goal state))
-        val facts = nearly_all_facts ctxt false fact_override Symtab.empty Termtab.empty [] [] goal
-        val learn = mash_learn_proof ctxt params goal facts
-      in run_minimize params learn i (#add fact_override) state end
     else if subcommand = messagesN then
       messages opt_i
     else if subcommand = supported_proversN then
@@ -403,7 +364,8 @@
   Toplevel.unknown_proof o
   Toplevel.keep (hammer_away params subcommand opt_i fact_override o Toplevel.proof_of)
 
-fun string_of_raw_param (name, value) = name ^ " = " ^ implode_param value
+fun string_of_raw_param (key, values) =
+  key ^ (case implode_param values of "" => "" | value => " = " ^ value)
 
 fun sledgehammer_params_trans params =
   Toplevel.theory (fold set_default_raw_param params #> tap (fn thy =>
@@ -442,8 +404,7 @@
     val mode = if auto then Auto_Try else Try
     val i = 1
   in
-    run_sledgehammer (get_params mode thy []) mode NONE i no_fact_override (minimize_command [] i)
-      state
+    run_sledgehammer (get_params mode thy []) mode NONE i no_fact_override state
   end
 
 val _ = Try.tool_setup (sledgehammerN, (40, @{system_option auto_sledgehammer}, try_sledgehammer))
@@ -452,23 +413,23 @@
   Query_Operation.register sledgehammerN (fn {state = st, args, output_result} =>
     (case try Toplevel.proof_of st of
       SOME state =>
-        let
-          val thy = Proof.theory_of state
-          val ctxt = Proof.context_of state
-          val [provers_arg, isar_proofs_arg] = args
+      let
+        val thy = Proof.theory_of state
+        val ctxt = Proof.context_of state
+        val [provers_arg, isar_proofs_arg] = args
 
-          val override_params =
-            ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @
-              [("isar_proofs", [isar_proofs_arg]),
-               ("blocking", ["true"]),
-               ("debug", ["false"]),
-               ("verbose", ["false"]),
-               ("overlord", ["false"])])
-            |> map (normalize_raw_param ctxt)
-
-          val _ = run_sledgehammer (get_params Normal thy override_params) Normal
-            (SOME output_result) 1 no_fact_override (minimize_command override_params 1) state
-        in () end
+        val override_params =
+          ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @
+            [("isar_proofs", [isar_proofs_arg]),
+             ("blocking", ["true"]),
+             ("debug", ["false"]),
+             ("verbose", ["false"]),
+             ("overlord", ["false"])])
+          |> map (normalize_raw_param ctxt)
+      in
+        ignore (run_sledgehammer (get_params Normal thy override_params) Normal
+          (SOME output_result) 1 no_fact_override state)
+      end
     | NONE => error "Unknown proof context"))
 
 end;

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -127,8 +127,7 @@
 val skolem_methods = basic_systematic_methods
 
 fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
-    (one_line_params as ((_, one_line_play), banner, used_facts, minimize_command, subgoal,
-       subgoal_count)) =
+    (one_line_params as ((_, one_line_play), banner, used_facts, subgoal, subgoal_count)) =
   let
     val _ = if debug then Output.urgent_message "Constructing Isar proof..." else ()
 
@@ -352,8 +351,7 @@
                (case isar_proof of
                  Proof (_, _, [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)]) =>
                  let val used_facts' = filter (member (op =) gfs o fst) used_facts in
-                   ((meth, play_outcome), banner, used_facts', minimize_command, subgoal,
-                    subgoal_count)
+                   ((meth, play_outcome), banner, used_facts', subgoal, subgoal_count)
                  end)
              else
                one_line_params) ^
@@ -389,7 +387,7 @@
   | Play_Failed => true)
 
 fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
-    (one_line_params as (preplay, _, _, _, _, _)) =
+    (one_line_params as (preplay, _, _, _, _)) =
   (if isar_proofs = SOME true orelse
       (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt_proofs preplay) then
      isar_proof_text ctxt debug isar_proofs smt_proofs isar_params

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -814,7 +814,7 @@
       {comment = "Goal: " ^ goal_name, state = Proof.init ctxt, goal = goal, subgoal = 1,
        subgoal_count = 1, factss = [("", facts)]}
   in
-    get_minimizing_prover ctxt MaSh (K ()) prover params (K (K (K ""))) problem
+    get_minimizing_prover ctxt MaSh (K ()) prover params problem
   end
 
 val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -29,9 +29,8 @@
     Play_Timed_Out of Time.time |
     Play_Failed
 
-  type minimize_command = string list -> string
   type one_line_params =
-    (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
+    (proof_method * play_outcome) * string * (string * stature) list * int * int
 
   val is_proof_method_direct : proof_method -> bool
   val string_of_proof_method : Proof.context -> string list -> proof_method -> string
@@ -69,9 +68,7 @@
   Play_Timed_Out of Time.time |
   Play_Failed
 
-type minimize_command = string list -> string
-type one_line_params =
-  (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
+type one_line_params = (proof_method * play_outcome) * string * (string * stature) list * int * int
 
 fun is_proof_method_direct (Metis_Method _) = true
   | is_proof_method_direct Meson_Method = true
@@ -179,29 +176,18 @@
     (s |> s <> "" ? enclose " (" ")") ^ "."
   end
 
-fun minimize_line _ [] = ""
-  | minimize_line minimize_command ss =
-    (case minimize_command ss of
-      "" => ""
-    | command => "\nTo minimize: " ^ Active.sendback_markup [Markup.padding_command] command ^ ".")
-
 fun split_used_facts facts =
   facts
   |> List.partition (fn (_, (sc, _)) => sc = Chained)
   |> pairself (sort_distinct (string_ord o pairself fst))
 
 fun one_line_proof_text ctxt num_chained
-    ((meth, play), banner, used_facts, minimize_command, subgoal, subgoal_count) =
-  let
-    val (chained, extra) = split_used_facts used_facts
-
-    val try_line =
-      map fst extra
-      |> proof_method_command ctxt meth subgoal subgoal_count (map fst chained) num_chained
-      |> (if play = Play_Failed then enclose "One-line proof reconstruction failed: " "."
-          else try_command_line banner play)
-  in
-    try_line ^ minimize_line minimize_command (map fst (extra @ chained))
+    ((meth, play), banner, used_facts, subgoal, subgoal_count) =
+  let val (chained, extra) = split_used_facts used_facts in
+    map fst extra
+    |> proof_method_command ctxt meth subgoal subgoal_count (map fst chained) num_chained
+    |> (if play = Play_Failed then enclose "One-line proof reconstruction failed: " "."
+        else try_command_line banner play)
   end
 
 end;

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -14,7 +14,6 @@
   type fact = Sledgehammer_Fact.fact
   type proof_method = Sledgehammer_Proof_Methods.proof_method
   type play_outcome = Sledgehammer_Proof_Methods.play_outcome
-  type minimize_command = Sledgehammer_Proof_Methods.minimize_command
 
   datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
 
@@ -62,9 +61,7 @@
      message : proof_method * play_outcome -> string,
      message_tail : string}
 
-  type prover =
-    params -> ((string * string list) list -> string -> minimize_command) -> prover_problem ->
-    prover_result
+  type prover = params -> prover_problem -> prover_result
 
   val SledgehammerN : string
   val str_of_mode : mode -> string
@@ -156,9 +153,7 @@
    message : proof_method * play_outcome -> string,
    message_tail : string}
 
-type prover =
-  params -> ((string * string list) list -> string -> minimize_command)
-  -> prover_problem -> prover_result
+type prover = params -> prover_problem -> prover_result
 
 fun overlord_file_location_of_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -135,7 +135,6 @@
     ({debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, fact_filter,
      max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs,
      slice, minimize, timeout, preplay_timeout, ...} : params)
-    minimize_command
     ({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   let
     val thy = Proof.theory_of state
@@ -388,8 +387,7 @@
                   end
 
                 val one_line_params =
-                  (preplay, proof_banner mode name, used_facts, minimize_command [] name, subgoal,
-                   subgoal_count)
+                  (preplay, proof_banner mode name, used_facts, subgoal, subgoal_count)
                 val num_chained = length (#facts (Proof.goal state))
               in
                 proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -102,7 +102,7 @@
     val problem =
       {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
        factss = [("", facts)]}
-    val result as {outcome, used_facts, run_time, ...} = prover params (K (K (K ""))) problem
+    val result as {outcome, used_facts, run_time, ...} = prover params problem
   in
     print silent (fn () =>
       (case outcome of
@@ -253,8 +253,8 @@
       | NONE => result)
     end
 
-fun get_minimizing_prover ctxt mode do_learn name params minimize_command problem =
-  get_prover ctxt mode name params minimize_command problem
+fun get_minimizing_prover ctxt mode do_learn name params problem =
+  get_prover ctxt mode name params problem
   |> maybe_minimize mode do_learn name params problem
 
 fun run_minimize (params as {provers, ...}) do_learn i refs state =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -179,7 +179,7 @@
 
 fun run_smt2_solver mode name (params as {debug, verbose, isar_proofs, compress, try0, smt_proofs,
       minimize, preplay_timeout, ...})
-    minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
+    ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   let
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
@@ -209,8 +209,7 @@
                   goal)
 
                val one_line_params =
-                 (preplay, proof_banner mode name, used_facts, minimize_command [] name, subgoal,
-                  subgoal_count)
+                 (preplay, proof_banner mode name, used_facts, subgoal, subgoal_count)
                val num_chained = length (#facts (Proof.goal state))
              in
                proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params