make Sledgehammer's minimizer also minimize Isar proofs

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Apr 19 11:54:07 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Apr 19 15:15:21 2010 +0200
@@ -391,7 +391,7 @@
       |> Option.map (fst o read_int o explode)
       |> the_default 5
     val params = default_params thy [("minimize_timeout", Int.toString timeout)]
-    val minimize = minimize_theorems params linear_minimize prover prover_name 1
+    val minimize = minimize_theorems params prover prover_name 1
     val _ = log separator
   in
     case minimize st (these (!named_thms)) of

--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Apr 19 11:54:07 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Apr 19 15:15:21 2010 +0200
@@ -35,6 +35,7 @@
   type prover_result =
     {success: bool,
      message: string,
+     conjecture_pos: int * int,
      relevant_thm_names: string list,
      atp_run_time_in_msecs: int,
      proof: string,
@@ -90,6 +91,7 @@
 type prover_result =
   {success: bool,
    message: string,
+   conjecture_pos: int * int,
    relevant_thm_names: string list,
    atp_run_time_in_msecs: int,
    proof: string,

--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Mon Apr 19 11:54:07 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Mon Apr 19 15:15:21 2010 +0200
@@ -9,13 +9,9 @@
   type params = ATP_Manager.params
   type prover = ATP_Manager.prover
   type prover_result = ATP_Manager.prover_result
-  type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
 
-  val linear_minimize : 'a minimize_fun
-  val binary_minimize : 'a minimize_fun
   val minimize_theorems :
-    params -> (string * thm list) minimize_fun -> prover -> string -> int
-    -> Proof.state -> (string * thm list) list
+    params -> prover -> string -> int -> Proof.state -> (string * thm list) list
     -> (string * thm list) list option * string
 end;
 
@@ -27,62 +23,24 @@
 open Sledgehammer_Proof_Reconstruct
 open ATP_Manager
 
-type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
-
 (* Linear minimization algorithm *)
 
-fun linear_minimize p s =
+fun linear_minimize test s =
   let
-    fun aux [] needed = needed
-      | aux (x :: xs) needed = aux xs (needed |> not (p (xs @ needed)) ? cons x)
-  in aux s [] end;
-
-(* Binary minimalization *)
-
-local
-  fun isplit (l, r) [] = (l, r)
-    | isplit (l, r) [h] = (h :: l, r)
-    | isplit (l, r) (h1 :: h2 :: t) = isplit (h1 :: l, h2 :: r) t
-in
-  fun split lst = isplit ([], []) lst
-end
-
-local
-  fun min _ _ [] = raise Empty
-    | min _ _ [s0] = [s0]
-    | min p sup s =
-      let
-        val (l0, r0) = split s
-      in
-        if p (sup @ l0) then
-          min p sup l0
-        else if p (sup @ r0) then
-          min p sup r0
-        else
-          let
-            val l = min p (sup @ r0) l0
-            val r = min p (sup @ l) r0
-          in l @ r end
-      end
-in
-  (* return a minimal subset v of s that satisfies p
-   @pre p(s) & ~p([]) & monotone(p)
-   @post v subset s & p(v) &
-         forall e in v. ~p(v \ e)
-   *)
-  fun binary_minimize p s =
-    case min p [] s of
-      [x] => if p [] then [] else [x]
-    | m => m
-end
+    fun aux [] p = p
+      | aux (x :: xs) (needed, result) =
+        case test (xs @ needed) of
+          SOME result => aux xs (needed, result)
+        | NONE => aux xs (x :: needed, result)
+  in aux s end
 
 
 (* failure check and producing answer *)
 
-datatype 'a prove_result = Success of 'a | Failure | Timeout | Error
+datatype outcome = Success | Failure | Timeout | Error
 
-val string_of_result =
-  fn Success _ => "Success"
+val string_of_outcome =
+  fn Success => "Success"
    | Failure => "Failure"
    | Timeout => "Timeout"
    | Error => "Error"
@@ -94,26 +52,19 @@
    ("# Cannot determine problem status within resource limit", Timeout),
    ("Error", Error)]
 
-fun produce_answer ({success, proof, internal_thm_names, filtered_clauses, ...}
-                    : prover_result) =
+fun outcome_of_result (result as {success, proof, ...} : prover_result) =
   if success then
-    (Success (Vector.foldr (op ::) [] internal_thm_names, filtered_clauses),
-     proof)
-  else
-    let
-      val failure = failure_strings |> get_first (fn (s, t) =>
-          if String.isSubstring s proof then SOME (t, proof) else NONE)
-    in
-      (case failure of
-        SOME res => res
-      | NONE => (Failure, proof))
-    end
-
+    Success
+  else case get_first (fn (s, outcome) =>
+                          if String.isSubstring s proof then SOME outcome
+                          else NONE) failure_strings of
+    SOME outcome => outcome
+  | NONE => Failure
 
 (* wrapper for calling external prover *)
 
 fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover
-        timeout subgoal state filtered name_thms_pairs =
+        timeout subgoal state filtered_clauses name_thms_pairs =
   let
     val num_theorems = length name_thms_pairs
     val _ = priority ("Testing " ^ string_of_int num_theorems ^
@@ -124,50 +75,61 @@
     val problem =
      {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)
-    val _ = priority (string_of_result result)
-  in (result, proof) end
-
+      axiom_clauses = SOME axclauses, filtered_clauses = filtered_clauses}
+  in
+    `outcome_of_result (prover params timeout problem)
+    |>> tap (priority o string_of_outcome)
+  end
 
 (* minimalization of thms *)
 
-fun minimize_theorems (params as {minimize_timeout, ...}) gen_min prover
-                      prover_name i state name_thms_pairs =
+fun minimize_theorems (params as {minimize_timeout, isar_proof, modulus,
+                                  sorts, ...})
+                      prover atp_name i state name_thms_pairs =
   let
     val msecs = Time.toMilliseconds minimize_timeout
     val _ =
       priority ("Minimize called with " ^ string_of_int (length name_thms_pairs) ^
-        " theorems, ATP: " ^ prover_name ^
+        " theorems, ATP: " ^ atp_name ^
         ", time limit: " ^ string_of_int msecs ^ " ms")
     val test_thms_fun =
       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
+      case test_thms_fun filtered thms of
+        (Success, result) => SOME result
+      | _ => NONE
+
+    val {context = ctxt, facts, goal} = Proof.goal state;
+    val n = Logic.count_prems (prop_of goal)
   in
     (* try prove first to check result and get used theorems *)
     (case test_thms_fun NONE name_thms_pairs of
-      (Success (used, filtered), _) =>
+      (Success, result as {internal_thm_names, filtered_clauses,
+                           ...}) =>
         let
-          val ordered_used = sort_distinct string_ord used
+          val used = internal_thm_names |> Vector.foldr (op ::) []
+                                        |> sort_distinct string_ord
           val to_use =
-            if length ordered_used < length name_thms_pairs then
-              filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
+            if length used < length name_thms_pairs then
+              filter (fn (name1, _) => List.exists (curry (op =) name1) used)
+                     name_thms_pairs
             else name_thms_pairs
-          val min_thms =
-            if null to_use then []
-            else gen_min (test_thms (SOME filtered)) to_use
-          val min_names = sort_distinct string_ord (map fst min_thms)
+          val (min_thms, {conjecture_pos, proof, internal_thm_names, ...}) =
+            linear_minimize (test_thms (SOME filtered_clauses)) to_use
+                            ([], result)
           val _ = priority (cat_lines
             ["Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
-        in (SOME min_thms, metis_line i n min_names) end
+        in
+          (SOME min_thms,
+           proof_text isar_proof true modulus sorts atp_name
+                      (proof, internal_thm_names, conjecture_pos, ctxt, goal, i)
+           |> fst)
+        end
     | (Timeout, _) =>
         (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
                \option (e.g., \"timeout = " ^
                string_of_int (10 + msecs div 1000) ^ " s\").")
-    | (Error, msg) =>
-        (NONE, "Error in prover: " ^ msg)
+    | (Error, {message, ...}) => (NONE, "ATP error: " ^ message)
     | (Failure, _) =>
         (* Failure sometimes mean timeout, unfortunately. *)
         (NONE, "Failure: No proof was found with the current time limit. You \

--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Mon Apr 19 11:54:07 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Mon Apr 19 15:15:21 2010 +0200
@@ -67,7 +67,7 @@
   | (failure :: _) => SOME failure
 
 fun generic_prover overlord get_facts prepare write_file cmd args failure_strs
-        produce_answer name ({debug, full_types, ...} : params)
+        proof_text name ({debug, full_types, ...} : params)
         ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
          : problem) =
   let
@@ -142,20 +142,22 @@
         File.write (Path.explode (Path.implode probfile ^ "_proof"))
                    ("% " ^ timestamp () ^ "\n" ^ proof)
 
-    val (((proof, atp_run_time_in_msecs), rc), conj_pos) =
+    val (((proof, atp_run_time_in_msecs), rc), conjecture_pos) =
       with_path cleanup export run_on (prob_pathname subgoal);
 
     (* Check for success and print out some information on failure. *)
     val failure = find_failure failure_strs proof;
     val success = rc = 0 andalso is_none failure;
     val (message, relevant_thm_names) =
-      if is_some failure then ("ATP failed to find a proof.\n", [])
-      else if rc <> 0 then ("ATP error: " ^ proof ^ ".\n", [])
+      if is_some failure then
+        ("ATP failed to find a proof.\n", [])
+      else if rc <> 0 then
+        ("ATP error: " ^ proof ^ ".\n", [])
       else
-        (produce_answer name (proof, internal_thm_names, conj_pos, ctxt, th,
-                              subgoal));
+        proof_text name (proof, internal_thm_names, conjecture_pos, ctxt, th,
+                         subgoal)
   in
-    {success = success, message = message,
+    {success = success, message = message, conjecture_pos = conjecture_pos,
      relevant_thm_names = relevant_thm_names,
      atp_run_time_in_msecs = atp_run_time_in_msecs, proof = proof,
      internal_thm_names = internal_thm_names,
@@ -179,10 +181,8 @@
       (prepare_clauses higher_order false)
       (write_tptp_file (overlord andalso not isar_proof)) command
       (arguments timeout) failure_strs
-      (if supports_isar_proofs andalso isar_proof then
-         structured_isar_proof modulus sorts
-       else
-         metis_lemma_list false) name params;
+      (proof_text (supports_isar_proofs andalso isar_proof) false modulus sorts)
+      name params
 
 fun tptp_prover name p = (name, generic_tptp_prover (name, p));
 
@@ -237,7 +237,8 @@
                           higher_order follow_defs max_new_clauses
                           (the_default prefers_theory_relevant theory_relevant))
       (prepare_clauses higher_order true) write_dfg_file command
-      (arguments timeout) failure_strs (metis_lemma_list true) name params;
+      (arguments timeout) failure_strs (metis_proof_text false false)
+      name params
 
 fun dfg_prover (name, p) = (name, generic_dfg_prover (name, p));
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Apr 19 11:54:07 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Apr 19 15:15:21 2010 +0200
@@ -183,27 +183,27 @@
     fun get_time_limit_arg s =
       (case Int.fromString s of
         SOME t => Time.fromSeconds t
-      | NONE => error ("Invalid time limit: " ^ quote s))
+      | NONE => error ("Invalid time limit: " ^ quote s ^ "."))
     fun get_opt (name, a) (p, t) =
       (case name of
         "time" => (p, get_time_limit_arg a)
       | "atp" => (a, t)
-      | n => error ("Invalid argument: " ^ n))
+      | n => error ("Invalid argument: " ^ n ^ "."))
     val {atps, minimize_timeout, ...} = get_params thy override_params
     val (atp, timeout) = fold get_opt old_style_args (hd atps, minimize_timeout)
     val params =
       get_params thy
-          [("atps", [atp]),
-           ("minimize_timeout",
-            [string_of_int (Time.toMilliseconds timeout) ^ " ms"])]
+          (override_params @
+           [("atps", [atp]),
+            ("minimize_timeout",
+             [string_of_int (Time.toMilliseconds timeout) ^ " ms"])])
     val prover =
       (case get_prover thy atp of
         SOME prover => prover
-      | NONE => error ("Unknown ATP: " ^ quote atp))
+      | 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 i state
-                                   name_thms_pairs))
+    priority (#2 (minimize_theorems params prover atp i state name_thms_pairs))
   end
 
 val runN = "run"

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Apr 19 11:54:07 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Apr 19 15:15:21 2010 +0200
@@ -14,10 +14,18 @@
   val strip_prefix: string -> string -> string option
   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: int -> bool -> string ->
-    string * string vector * (int * int) * Proof.context * thm * int -> string * string list
+  val metis_proof_text:
+    bool -> bool -> string
+    -> string * string vector * (int * int) * Proof.context * thm * int
+    -> string * string list
+  val isar_proof_text:
+    bool -> int -> bool -> string
+    -> string * string vector * (int * int) * Proof.context * thm * int
+    -> string * string list
+  val proof_text:
+    bool -> bool -> int -> bool -> string
+    -> string * string vector * (int * int) * Proof.context * thm * int
+    -> string * string list
 end;
 
 structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
@@ -493,26 +501,21 @@
   exists (fn s => String.isSubstring s proof) end_proof_strs
 
 (* === EXTRACTING LEMMAS === *)
-(* lines have the form "cnf(108, axiom, ...",
-the number (108) has to be extracted)*)
-fun get_step_nums false extract =
+(* A list consisting of the first number in each line is returned.
+   TPTP: Interesting lines have the form "cnf(108, axiom, ...)", where the
+   number (108) is extracted.
+   DFG: Lines have the form "108[0:Inp] ...", where the first number (108) is
+   extracted. *)
+fun get_step_nums proof_extract =
   let
     val toks = String.tokens (not o Char.isAlphaNum)
     fun inputno ("cnf" :: ntok :: "axiom" :: _) = Int.fromString ntok
       | inputno ("cnf" :: ntok :: "negated" :: "conjecture" :: _) =
         Int.fromString ntok
+      | inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok (* DFG *)
       | inputno _ = NONE
-    val lines = split_lines extract
+    val lines = split_lines proof_extract
   in map_filter (inputno o toks) lines end
-(*String contains multiple lines. We want those of the form
-  "253[0:Inp] et cetera..."
-  A list consisting of the first number in each line is returned. *)
-|  get_step_nums true proofextract =
-  let val toks = String.tokens (not o Char.isAlphaNum)
-  fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok
-    | inputno _ = NONE
-  val lines = split_lines proofextract
-  in  map_filter (inputno o toks) lines  end
   
 (*extracting lemmas from tstp-output between the lines from above*)
 fun extract_lemmas get_step_nums (proof, thm_names, conj_count, _, _, _) =
@@ -546,28 +549,31 @@
 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 xs =
+fun minimize_line _ _ [] = ""
+  | minimize_line isar_proof atp_name xs =
       "To minimize the number of lemmas, try this command: " ^
       Markup.markup Markup.sendback
-                    ("sledgehammer minimize [atp = " ^ name ^ "] (" ^
+                    ("sledgehammer minimize [atp = " ^ atp_name ^
+                     (if isar_proof then ", isar_proof" else "") ^ "] (" ^
                      space_implode " " xs ^ ")") ^ ".\n"
 
-fun metis_lemma_list dfg name (result as (_, _, _, _, goal, i)) =
+fun metis_proof_text isar_proof minimal atp_name
+                     (result as (_, _, _, _, goal, i)) =
   let
-    val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result
+    val (lemmas, used_conj) = extract_lemmas get_step_nums result
     val n = Logic.count_prems (prop_of goal)
     val xs = kill_chained lemmas
   in
-    (metis_line i n xs ^ minimize_line name xs ^
+    (metis_line i n xs ^
+     (if minimal then "" else minimize_line isar_proof atp_name xs) ^
      (if used_conj then
         ""
       else
         "\nWarning: The goal is provable because the context is inconsistent."),
      kill_chained lemmas)
-  end;
+  end
 
-fun structured_isar_proof modulus sorts name
+fun isar_proof_text minimal modulus sorts atp_name
         (result as (proof, thm_names, conj_count, ctxt, goal, i)) =
   let
     (* We could use "split_lines", but it can return blank lines. *)
@@ -576,7 +582,8 @@
       String.translate (fn c => if Char.isSpace c then "" else str c)
     val extract = get_proof_extract proof
     val cnfs = filter (String.isPrefix "cnf(") (map kill_spaces (lines extract))
-    val (one_line_proof, lemma_names) = metis_lemma_list false name result
+    val (one_line_proof, lemma_names) =
+      metis_proof_text true minimal atp_name result
     val tokens = String.tokens (fn c => c = #" ") one_line_proof
     val isar_proof =
       if member (op =) tokens chained_hint then ""
@@ -588,4 +595,8 @@
      lemma_names)
   end
 
+fun proof_text isar_proof minimal modulus sorts =
+  if isar_proof then isar_proof_text minimal modulus sorts
+  else metis_proof_text isar_proof minimal
+
 end;