src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML

+(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML
+    Author:     Philipp Meyer, TU Muenchen
+    Author:     Jasmin Blanchette, TU Muenchen
+
+Minimization of theorem list for Metis using automatic theorem provers.
+*)
+
+signature SLEDGEHAMMER_FACT_MINIMIZE =
+sig
+  type locality = Sledgehammer_Fact_Filter.locality
+  type params = Sledgehammer.params
+
+  val minimize_theorems :
+    params -> int -> int -> Proof.state -> ((string * locality) * thm list) list
+    -> ((string * locality) * thm list) list option * string
+  val run_minimize : params -> int -> Facts.ref list -> Proof.state -> unit
+end;
+
+structure Sledgehammer_Fact_Minimize : SLEDGEHAMMER_FACT_MINIMIZE =
+struct
+
+open ATP_Systems
+open Sledgehammer_Util
+open Sledgehammer_Fact_Filter
+open Sledgehammer_Proof_Reconstruct
+open Sledgehammer
+
+(* wrapper for calling external prover *)
+
+fun string_for_failure Unprovable = "Unprovable."
+  | string_for_failure TimedOut = "Timed out."
+  | string_for_failure _ = "Unknown error."
+
+fun n_theorems names =
+  let val n = length names in
+    string_of_int n ^ " theorem" ^ plural_s n ^
+    (if n > 0 then
+       ": " ^ (names |> map fst
+                     |> sort_distinct string_ord |> space_implode " ")
+     else
+       "")
+  end
+
+fun test_theorems ({debug, verbose, overlord, atps, full_types, isar_proof,
+                    isar_shrink_factor, ...} : params)
+                  (prover : prover) explicit_apply timeout subgoal state
+                  axioms =
+  let
+    val _ =
+      priority ("Testing " ^ n_theorems (map fst axioms) ^ "...")
+    val params =
+      {blocking = true, debug = debug, verbose = verbose, overlord = overlord,
+       atps = atps, full_types = full_types, explicit_apply = explicit_apply,
+       relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
+       theory_relevant = NONE, isar_proof = isar_proof,
+       isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""}
+    val axioms = maps (fn (n, ths) => map (pair n) ths) axioms
+    val {context = ctxt, facts, goal} = Proof.goal state
+    val problem =
+     {subgoal = subgoal, goal = (ctxt, (facts, goal)),
+      relevance_override = {add = [], del = [], only = false},
+      axioms = SOME axioms}
+    val result as {outcome, used_thm_names, ...} = prover params (K "") problem
+  in
+    priority (case outcome of
+                NONE =>
+                if length used_thm_names = length axioms then
+                  "Found proof."
+                else
+                  "Found proof with " ^ n_theorems used_thm_names ^ "."
+              | SOME failure => string_for_failure failure);
+    result
+  end
+
+(* minimalization of thms *)
+
+fun filter_used_facts used = filter (member (op =) used o fst)
+
+fun sublinear_minimize _ [] p = p
+  | sublinear_minimize test (x :: xs) (seen, result) =
+    case test (xs @ seen) of
+      result as {outcome = NONE, proof, used_thm_names, ...} : prover_result =>
+      sublinear_minimize test (filter_used_facts used_thm_names xs)
+                         (filter_used_facts used_thm_names seen, result)
+    | _ => sublinear_minimize test xs (x :: seen, result)
+
+(* Give the ATP some slack. The ATP gets further slack because the Sledgehammer
+   preprocessing time is included in the estimate below but isn't part of the
+   timeout. *)
+val fudge_msecs = 1000
+
+fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set."
+  | minimize_theorems (params as {debug, atps = atp :: _, full_types,
+                                  isar_proof, isar_shrink_factor, timeout, ...})
+                      i n state axioms =
+  let
+    val thy = Proof.theory_of state
+    val prover = get_prover_fun thy atp
+    val msecs = Time.toMilliseconds timeout
+    val _ = priority ("Sledgehammer minimize: ATP " ^ quote atp ^ ".")
+    val {context = ctxt, 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) axioms))
+    fun do_test timeout =
+      test_theorems params prover explicit_apply timeout i state
+    val timer = Timer.startRealTimer ()
+  in
+    (case do_test timeout axioms of
+       result as {outcome = NONE, pool, used_thm_names,
+                  conjecture_shape, ...} =>
+       let
+         val time = Timer.checkRealTimer timer
+         val new_timeout =
+           Int.min (msecs, Time.toMilliseconds time + fudge_msecs)
+           |> Time.fromMilliseconds
+         val (min_thms, {proof, axiom_names, ...}) =
+           sublinear_minimize (do_test new_timeout)
+               (filter_used_facts used_thm_names axioms) ([], result)
+         val n = length min_thms
+         val _ = priority (cat_lines
+           ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^
+            (case length (filter (curry (op =) Chained o snd o fst) min_thms) of
+               0 => ""
+             | n => " (including " ^ Int.toString n ^ " chained)") ^ ".")
+       in
+         (SOME min_thms,
+          proof_text isar_proof
+              (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
+              (full_types, K "", proof, axiom_names, goal, i) |> fst)
+       end
+     | {outcome = SOME TimedOut, ...} =>
+       (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
+              \option (e.g., \"timeout = " ^
+              string_of_int (10 + msecs div 1000) ^ " s\").")
+     | {outcome = SOME UnknownError, ...} =>
+       (* Failure sometimes mean timeout, unfortunately. *)
+       (NONE, "Failure: No proof was found with the current time limit. You \
+              \can increase the time limit using the \"timeout\" \
+              \option (e.g., \"timeout = " ^
+              string_of_int (10 + msecs div 1000) ^ " s\").")
+     | {message, ...} => (NONE, "ATP error: " ^ message))
+    handle ERROR msg => (NONE, "Error: " ^ msg)
+  end
+
+fun run_minimize params i refs state =
+  let
+    val ctxt = Proof.context_of state
+    val reserved = reserved_isar_keyword_table ()
+    val chained_ths = #facts (Proof.goal state)
+    val axioms =
+      maps (map (apsnd single)
+            o name_thm_pairs_from_ref ctxt reserved chained_ths) refs
+  in
+    case subgoal_count state of
+      0 => priority "No subgoal!"
+    | n =>
+      (kill_atps (); priority (#2 (minimize_theorems params i n state axioms)))
+  end
+
+end;