automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Feb 09 17:18:58 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Feb 09 17:18:58 2011 +0100
@@ -475,14 +475,14 @@
       AList.lookup (op =) args minimize_timeoutK
       |> Option.map (fst o read_int o raw_explode)  (* FIXME Symbol.explode (?) *)
       |> the_default 5
-    val params = Sledgehammer_Isar.default_params ctxt
+    val params as {explicit_apply, ...} = Sledgehammer_Isar.default_params ctxt
       [("provers", prover_name),
        ("verbose", "true"),
        ("type_sys", type_sys),
        ("timeout", string_of_int timeout)]
     val minimize =
-      Sledgehammer_Minimize.minimize_facts prover_name params true 1
-                                           (Sledgehammer_Util.subgoal_count st)
+      Sledgehammer_Minimize.minimize_facts prover_name params
+          (SOME explicit_apply) true 1 (Sledgehammer_Util.subgoal_count st)
     val _ = log separator
   in
     case minimize st (these (!named_thms)) of

--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Feb 09 17:18:58 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Feb 09 17:18:58 2011 +0100
@@ -241,7 +241,8 @@
    has_incomplete_mode = false,
    proof_delims = [],
    known_failures =
-     [(IncompleteUnprovable, "\nsat"),
+     [(Unprovable, "\nsat"),
+      (IncompleteUnprovable, "\nunknown"),
       (ProofMissing, "\nunsat")],
    default_max_relevant = 250 (* FUDGE *),
    explicit_forall = true,

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Wed Feb 09 17:18:58 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Wed Feb 09 17:18:58 2011 +0100
@@ -28,6 +28,7 @@
   val split_used_facts :
     (string * locality) list
     -> (string * locality) list * (string * locality) list
+  val metis_proof_text : metis_params -> text_result
   val isar_proof_text : isar_params -> metis_params -> text_result
   val proof_text : bool -> isar_params -> metis_params -> text_result
 end;
@@ -165,9 +166,13 @@
     append (resolve_fact fact_names name)
   | add_fact _ _ = I
 
-fun used_facts_in_tstplike_proof fact_names =
-  atp_proof_from_tstplike_string false
-  #> rpair [] #-> fold (add_fact fact_names)
+fun used_facts_in_tstplike_proof fact_names tstplike_proof =
+  if tstplike_proof = "" then
+    Vector.foldl (op @) [] fact_names
+  else
+    tstplike_proof
+    |> atp_proof_from_tstplike_string false
+    |> rpair [] |-> fold (add_fact fact_names)
 
 val split_used_facts =
   List.partition (curry (op =) Chained o snd)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Feb 09 17:18:58 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Feb 09 17:18:58 2011 +0100
@@ -13,7 +13,7 @@
   val binary_min_facts : int Unsynchronized.ref
   val filter_used_facts : ''a list -> (''a * 'b) list -> (''a * 'b) list
   val minimize_facts :
-    string -> params -> bool -> int -> int -> Proof.state
+    string -> params -> bool option -> bool -> int -> int -> Proof.state
     -> ((string * locality) * thm list) list
     -> ((string * locality) * thm list) list option * string
   val run_minimize :
@@ -48,14 +48,24 @@
 fun print silent f = if silent then () else Output.urgent_message (f ())
 
 fun test_facts ({debug, verbose, overlord, provers, type_sys, isar_proof,
-                 isar_shrink_factor, ...} : params) silent (prover : prover)
-               explicit_apply timeout i n state facts =
+                 isar_shrink_factor, ...} : params)
+        explicit_apply_opt silent (prover : prover) timeout i n state facts =
   let
+    val thy = Proof.theory_of state
     val _ =
       print silent (fn () =>
           "Testing " ^ n_facts (map fst facts) ^
           (if verbose then " (timeout: " ^ string_from_time timeout ^ ")"
           else "") ^ "...")
+    val {goal, ...} = Proof.goal state
+    val explicit_apply =
+      case explicit_apply_opt of
+        SOME explicit_apply => explicit_apply
+      | NONE =>
+        let val (_, hyp_ts, concl_t) = strip_subgoal goal i in
+          not (forall (Meson.is_fol_term thy)
+                      (concl_t :: hyp_ts @ maps (map prop_of o snd) facts))
+        end
     val params =
       {debug = debug, verbose = false, overlord = overlord, blocking = true,
        provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
@@ -64,7 +74,6 @@
        timeout = timeout, expect = ""}
     val facts =
       facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
-    val {goal, ...} = Proof.goal state
     val problem =
       {state = state, goal = goal, subgoal = i, subgoal_count = n,
        facts = facts, smt_filter = NONE}
@@ -129,8 +138,8 @@
    part of the timeout. *)
 val slack_msecs = 200
 
-fun minimize_facts prover_name (params as {timeout, ...}) silent i n state
-                   facts =
+fun minimize_facts prover_name (params as {timeout, ...}) explicit_apply_opt
+                   silent i n state facts =
   let
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
@@ -139,12 +148,8 @@
     val _ = print silent (fn () => "Sledgehammer minimize: " ^
                                    quote prover_name ^ ".")
     val {goal, ...} = Proof.goal state
-    val (_, hyp_ts, concl_t) = strip_subgoal goal i
-    val explicit_apply =
-      not (forall (Meson.is_fol_term thy)
-                  (concl_t :: hyp_ts @ maps (map prop_of o snd) facts))
     fun do_test timeout =
-      test_facts params silent prover explicit_apply timeout i n state
+      test_facts params explicit_apply_opt silent prover timeout i n state
     val timer = Timer.startRealTimer ()
   in
     (case do_test timeout facts of
@@ -196,7 +201,7 @@
              [] => error "No prover is set."
            | prover :: _ =>
              (kill_provers ();
-              minimize_facts prover params false i n state facts
+              minimize_facts prover params NONE false i n state facts
               |> #2 |> Output.urgent_message)
   end
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Feb 09 17:18:58 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Feb 09 17:18:58 2011 +0100
@@ -445,26 +445,29 @@
         extract_important_message output
       else
         ""
-    val (message, used_facts) =
+    fun append_to_message message =
+      message ^
+      (if verbose then
+         "\nATP real CPU time: " ^
+         string_from_time (Time.fromMilliseconds (the msecs)) ^ "."
+       else
+         "") ^
+      (if important_message <> "" then
+         "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message
+       else
+         "")
+    val isar_params = (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
+    val metis_params =
+      (proof_banner auto, type_sys, minimize_command, tstplike_proof,
+       fact_names, goal, subgoal)
+    val (outcome, (message, used_facts)) =
       case outcome of
         NONE =>
-        proof_text isar_proof
-            (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
-            (proof_banner auto, type_sys, minimize_command, tstplike_proof,
-             fact_names, goal, subgoal)
-        |>> (fn message =>
-                message ^
-                (if verbose then
-                   "\nATP real CPU time: " ^
-                   string_from_time (Time.fromMilliseconds (the msecs)) ^ "."
-                 else
-                   "") ^
-                (if important_message <> "" then
-                   "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^
-                   important_message
-                 else
-                   ""))
-      | SOME failure => (string_for_failure "ATP" failure, [])
+        (NONE, proof_text isar_proof isar_params metis_params
+               |>> append_to_message)
+      | SOME ProofMissing =>
+        (NONE, metis_proof_text metis_params |>> append_to_message)
+      | SOME failure => (outcome, (string_for_failure "ATP" failure, []))
   in
     {outcome = outcome, message = message, used_facts = used_facts,
      run_time_in_msecs = msecs}

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Feb 09 17:18:58 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Feb 09 17:18:58 2011 +0100
@@ -44,8 +44,8 @@
 
 val auto_minimize_min_facts = Unsynchronized.ref (!binary_min_facts)
 
-fun get_minimizing_prover ctxt auto name (params as {debug, verbose, ...})
-        minimize_command
+fun get_minimizing_prover ctxt auto name
+        (params as {debug, verbose, explicit_apply, ...}) minimize_command
         (problem as {state, subgoal, subgoal_count, facts, ...}) =
   get_prover ctxt auto name params minimize_command problem
   |> (fn result as {outcome, used_facts, run_time_in_msecs, message} =>
@@ -55,8 +55,8 @@
            let
              val (used_facts, message) =
                if length used_facts >= !auto_minimize_min_facts then
-                 minimize_facts name params (not verbose) subgoal subgoal_count
-                     state
+                 minimize_facts name params (SOME explicit_apply) (not verbose)
+                     subgoal subgoal_count state
                      (filter_used_facts used_facts
                           (map (apsnd single o untranslated_fact) facts))
                  |>> Option.map (map fst)