make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"

--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Mar 29 15:50:18 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Mar 29 18:44:24 2010 +0200
@@ -54,7 +54,8 @@
 structure ATP_Manager : ATP_MANAGER =
 struct
 
-type relevance_override = Sledgehammer_Fact_Filter.relevance_override
+open Sledgehammer_Fact_Filter
+open Sledgehammer_Proof_Reconstruct
 
 (** parameters, problems, results, and provers **)
 
@@ -322,6 +323,7 @@
   | SOME prover =>
       let
         val {context = ctxt, facts, goal} = Proof.goal proof_state;
+        val n = Logic.count_prems (prop_of goal)
         val desc =
           "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
             Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
@@ -334,9 +336,8 @@
                relevance_override = relevance_override, axiom_clauses = NONE,
                filtered_clauses = NONE}
             val message = #message (prover params timeout problem)
-              handle Sledgehammer_HOL_Clause.TRIVIAL =>   (* FIXME !? *)
-                  "Try this command: " ^
-                  Markup.markup Markup.sendback "by metis" ^ "."
+              handle Sledgehammer_HOL_Clause.TRIVIAL =>
+                  metis_line i n []
                 | ERROR msg => ("Error: " ^ msg);
             val _ = unregister message (Thread.self ());
           in () end);

--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Mon Mar 29 15:50:18 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Mon Mar 29 18:44:24 2010 +0200
@@ -14,7 +14,7 @@
   val linear_minimize : 'a minimize_fun
   val binary_minimize : 'a minimize_fun
   val minimize_theorems :
-    params -> (string * thm list) minimize_fun -> prover -> string
+    params -> (string * thm list) minimize_fun -> prover -> string -> int
     -> Proof.state -> (string * thm list) list
     -> (string * thm list) list option * string
 end;
@@ -23,6 +23,7 @@
 struct
 
 open Sledgehammer_Fact_Preprocessor
+open Sledgehammer_Proof_Reconstruct
 open ATP_Manager
 
 type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
@@ -111,7 +112,7 @@
 (* wrapper for calling external prover *)
 
 fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover
-        timeout subgoalno state filtered name_thms_pairs =
+        timeout subgoal state filtered name_thms_pairs =
   let
     val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^
                       " theorems... ")
@@ -119,7 +120,7 @@
     val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
     val {context = ctxt, facts, goal} = Proof.goal state
     val problem =
-     {subgoal = subgoalno, goal = (ctxt, (facts, goal)),
+     {subgoal = subgoal, goal = (ctxt, (facts, goal)),
       relevance_override = {add = [], del = [], only = false},
       axiom_clauses = SOME axclauses, filtered_clauses = filtered}
     val (result, proof) = produce_answer (prover params timeout problem)
@@ -130,7 +131,7 @@
 (* minimalization of thms *)
 
 fun minimize_theorems (params as {minimize_timeout, ...}) gen_min prover
-                      prover_name state name_thms_pairs =
+                      prover_name i state name_thms_pairs =
   let
     val msecs = Time.toMilliseconds minimize_timeout
     val _ =
@@ -138,9 +139,10 @@
         " theorems, ATP: " ^ prover_name ^
         ", time limit: " ^ string_of_int msecs ^ " ms")
     val test_thms_fun =
-      sledgehammer_test_theorems params prover minimize_timeout 1 state
+      sledgehammer_test_theorems params prover minimize_timeout i state
     fun test_thms filtered thms =
       case test_thms_fun filtered thms of (Success _, _) => true | _ => false
+    val n = state |> Proof.raw_goal |> #goal |> prop_of |> Logic.count_prems
   in
     (* try prove first to check result and get used theorems *)
     (case test_thms_fun NONE name_thms_pairs of
@@ -157,13 +159,7 @@
           val min_names = sort_distinct string_ord (map fst min_thms)
           val _ = priority (cat_lines
             ["Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
-        in
-          (SOME min_thms,
-           "Try this command: " ^
-           Markup.markup Markup.sendback
-                         ("by (metis " ^ space_implode " " min_names ^ ")")
-           ^ ".")
-        end
+        in (SOME min_thms, metis_line i n min_names) end
     | (Timeout, _) =>
         (NONE, "Timeout: You may need to increase the time limit of " ^
           string_of_int msecs ^ " ms. Invoke \"atp_minimize [time=...]\".")
@@ -172,8 +168,7 @@
     | (Failure, _) =>
         (NONE, "Failure: No proof with the theorems supplied"))
     handle Sledgehammer_HOL_Clause.TRIVIAL =>
-        (SOME [], "Trivial: Try this command: " ^
-                  Markup.markup Markup.sendback "by metis" ^ ".")
+        (SOME [], metis_line i n [])
       | ERROR msg => (NONE, "Error: " ^ msg)
   end
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Mar 29 15:50:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Mar 29 18:44:24 2010 +0200
@@ -80,6 +80,8 @@
 structure Sledgehammer_FOL_Clause : SLEDGEHAMMER_FOL_CLAUSE =
 struct
 
+open Sledgehammer_Util
+
 val schematic_var_prefix = "V_";
 val fixed_var_prefix = "v_";
 
@@ -184,8 +186,7 @@
    solved in 3.7 and perhaps in earlier versions too.) *)
 (* 32-bit hash, so we expect no collisions. *)
 fun controlled_length dfg s =
-  if dfg andalso size s > 60 then Word.toString (hashw_string (s, 0w0))
-  else s;
+  if dfg andalso size s > 60 then Word.toString (hashw_string (s, 0w0)) else s;
 
 fun lookup_const dfg c =
     case Symtab.lookup const_trans_table c of

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Mar 29 15:50:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Mar 29 18:44:24 2010 +0200
@@ -144,7 +144,7 @@
 fun get_params thy = extract_params thy (default_raw_params thy)
 fun default_params thy = get_params thy o map (apsnd single)
 
-fun atp_minimize_command override_params old_style_args fact_refs state =
+fun atp_minimize_command override_params old_style_args i fact_refs state =
   let
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
@@ -176,7 +176,7 @@
       | NONE => error ("Unknown ATP: " ^ quote atp))
     val name_thms_pairs = theorems_from_refs ctxt fact_refs
   in
-    writeln (#2 (minimize_theorems params linear_minimize prover atp state
+    writeln (#2 (minimize_theorems params linear_minimize prover atp i state
                                    name_thms_pairs))
   end
 
@@ -202,7 +202,8 @@
       sledgehammer (get_params thy override_params) (the_default 1 opt_i)
                    relevance_override state
     else if subcommand = minimizeN then
-      atp_minimize_command override_params [] (#add relevance_override) state
+      atp_minimize_command override_params [] (the_default 1 opt_i)
+                           (#add relevance_override) state
     else if subcommand = messagesN then
       messages opt_i
     else if subcommand = available_atpsN then
@@ -287,7 +288,7 @@
     "minimize theorem list with external prover" K.diag
     (parse_minimize_args -- parse_fact_refs >> (fn (args, fact_refs) =>
       Toplevel.no_timing o Toplevel.unknown_proof o
-        Toplevel.keep (atp_minimize_command [] args fact_refs
+        Toplevel.keep (atp_minimize_command [] args 1 fact_refs
                        o Toplevel.proof_of)))
 
 val _ =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Mar 29 15:50:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Mar 29 18:44:24 2010 +0200
@@ -14,6 +14,7 @@
   val strip_prefix: string -> string -> string option
   val setup: theory -> theory
   val is_proof_well_formed: string -> bool
+  val metis_line: int -> int -> string list -> string
   val metis_lemma_list: bool -> string ->
     string * string vector * (int * int) * Proof.context * thm * int -> string * string list
   val structured_isar_proof: string ->
@@ -427,12 +428,15 @@
                stringify_deps thm_names ((lno,lname)::deps_map) lines
            end;
 
-val proofstart = "proof (neg_clausify)\n";
+fun isar_proof_start i =
+  (if i = 1 then "" else "prefer " ^ string_of_int i ^ "\n") ^
+  "proof (neg_clausify)\n";
+fun isar_fixes [] = ""
+  | isar_fixes ts = "  fix " ^ space_implode " " ts ^ "\n";
+fun isar_proof_end 1 = "qed"
+  | isar_proof_end _ = "next"
 
-fun isar_header [] = proofstart
-  | isar_header ts = proofstart ^ "fix " ^ space_implode " " ts ^ "\n";
-
-fun isar_proof_from_tstp_file cnfs ctxt th sgno thm_names =
+fun isar_proof_from_tstp_file cnfs ctxt goal i thm_names =
   let
     val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: start\n")
     val tuples = map (dest_tstp o tstp_line o explode) cnfs
@@ -448,7 +452,7 @@
     val (_, lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
     val _ = trace_proof_msg (fn () =>
       Int.toString (length lines) ^ " lines extracted\n")
-    val (ccls, fixes) = neg_conjecture_clauses ctxt th sgno
+    val (ccls, fixes) = neg_conjecture_clauses ctxt goal i
     val _ = trace_proof_msg (fn () =>
       Int.toString (length ccls) ^ " conjecture clauses\n")
     val ccls = map forall_intr_vars ccls
@@ -456,8 +460,12 @@
                               (fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls
     val body = isar_proof_body ctxt (map prop_of ccls)
                                (stringify_deps thm_names [] lines)
+    val n = Logic.count_prems (prop_of goal)
     val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: finishing\n")
-  in isar_header (map #1 fixes) ^ implode body ^ "qed\n" end
+  in
+    isar_proof_start i ^ isar_fixes (map #1 fixes) ^ implode body ^
+    isar_proof_end n ^ "\n"
+  end
   handle STREE _ => error "Could not extract proof (ATP output malformed?)";
 
 
@@ -534,22 +542,30 @@
 val chained_hint = "CHAINED";
 val kill_chained = filter_out (curry (op =) chained_hint)
 
-(* metis-command *)
-fun metis_line [] = "by metis"
-  | metis_line xs = "by (metis " ^ space_implode " " xs ^ ")"
-
+fun apply_command _ 1 = "by "
+  | apply_command 1 _ = "apply "
+  | apply_command i _ = "prefer " ^ string_of_int i ^ " apply "
+fun metis_command i n [] =
+    apply_command i n ^ "metis"
+  | metis_command i n xs =
+    apply_command i n ^ "(metis " ^ space_implode " " xs ^ ")"
+fun metis_line i n xs =
+  "Try this command: " ^
+  Markup.markup Markup.sendback (metis_command i n xs) ^ ".\n" 
 fun minimize_line _ [] = ""
-  | minimize_line name lemmas =
+  | minimize_line name xs =
       "To minimize the number of lemmas, try this command:\n" ^
       Markup.markup Markup.sendback
                     ("sledgehammer minimize [atps = " ^ name ^ "] (" ^
-                     space_implode " " (kill_chained lemmas) ^ ")") ^ "."
+                     space_implode " " xs ^ ")") ^ "."
 
-fun metis_lemma_list dfg name result =
-  let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result in
-    ("Try this command: " ^
-     Markup.markup Markup.sendback (metis_line (kill_chained lemmas)) ^ ".\n" ^
-     minimize_line name lemmas ^
+fun metis_lemma_list dfg name (result as (_, _, _, _, goal, subgoalno)) =
+  let
+    val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result
+    val n = Logic.count_prems (prop_of goal)
+    val xs = kill_chained lemmas
+  in
+    (metis_line subgoalno n xs ^ minimize_line name xs ^
      (if used_conj then
         ""
       else
@@ -572,11 +588,8 @@
       if member (op =) tokens chained_hint then ""
       else isar_proof_from_tstp_file cnfs ctxt goal subgoalno thm_names
   in
-    (* Hack: The " \n" shouldn't be part of the markup. This is a workaround
-       for a strange ProofGeneral bug, whereby the first two letters of the word
-       "proof" are not highlighted. *)
-    (one_line_proof ^ "\n\nStructured proof:" ^
-     Markup.markup Markup.sendback (" \n" ^ isar_proof), lemma_names)
+    (one_line_proof ^ "\nStructured proof:\n" ^
+     Markup.markup Markup.sendback isar_proof, lemma_names)
   end
 
 end;