src/HOL/Tools/atp_minimal.ML

+(*  Title:      HOL/Tools/atp_minimal.ML
+    Author:     Philipp Meyer, TU Muenchen
+
+Minimalization of theorem list for metis by using an external automated theorem prover
+*)
+
+structure AtpMinimal =
+struct
+
+  (* output control *)
+  fun debug str = Output.debug (fn () => str)
+  fun debug_fn f = if !Output.debugging then f() else ()
+  fun answer str = Output.writeln str
+  fun println str = Output.priority str
+
+  fun order_unique name_list = OrdList.make (String.collate Char.compare) name_list
+  fun length_string namelist = Int.toString (length namelist)
+
+  fun print_names name_thms_pairs =
+    let
+      val names = (map fst name_thms_pairs)
+      val ordered = order_unique names
+    in
+      app (fn name => (debug ("  " ^ name))) ordered
+    end
+
+  (* minimalization algorithm *)
+  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 p sup [] = raise Empty
+      | min p sup [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 minimal p s = min p [] s
+  end
+
+ (* failure check and producing answer*)
+  datatype 'a prove_result = Success of 'a | Failure | Timeout | Error
+
+  val string_of_result = fn
+    Success _ => "Success"
+  | Failure => "Failure"
+  | Timeout => "Timeout"
+  | Error => "Error"
+
+  val failure_strings =
+     [("SPASS beiseite: Ran out of time.", Timeout),
+     ("Timeout", Timeout),
+     ("time limit exceeded", Timeout),
+     ("# Cannot determine problem status within resource limit", Timeout),
+     ("Error", Error)]
+
+  fun produce_answer (success, message, result_string, thm_name_vec) =
+    if success then
+      (Success (Vector.foldr op:: [] thm_name_vec), result_string)
+    else
+      let
+        val failure = get_first (fn (s, t) => if String.isSubstring s result_string then SOME (t, result_string) else NONE) failure_strings
+      in
+        if is_some failure then
+          the failure
+        else
+          (Failure, result_string)
+      end
+
+  (* wrapper for calling external prover *)
+  fun sh_test_thms prover prover_name time_limit subgoalno state name_thms_pairs =
+    let
+      val _ = println ("Testing " ^ (length_string name_thms_pairs) ^ " theorems... ")
+      val name_thm_pairs = flat (map (fn (n, ths) => map_index (fn (i, th) => (n, th)) ths) name_thms_pairs)
+      val _ = debug_fn (fn () => print_names name_thm_pairs)
+      val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
+      val (result, proof) =
+        (produce_answer (prover time_limit (SOME axclauses) prover_name subgoalno (Proof.get_goal state)))
+      val _ = println (string_of_result result)
+      val _ = debug proof
+    in
+      (result, proof)
+    end
+
+  (* minimalization of thms *)
+  fun minimalize prover prover_name time_limit state name_thms_pairs =
+    let
+      val _ = println ("Minimize called with " ^ (length_string name_thms_pairs) ^ " theorems, prover: "
+                       ^ prover_name ^ ", time limit: " ^ (Int.toString time_limit) ^ " seconds")
+      val _ = debug_fn (fn () => app (fn (n, tl) => (debug n; app (fn t => debug ("  " ^ Display.string_of_thm t)) tl)) name_thms_pairs)
+      val test_thms_fun = sh_test_thms prover prover_name time_limit 1 state
+      fun test_thms thms = case test_thms_fun thms of (Success _, _) => true | _ => false
+    in
+      (* try proove first to check result and get used theorems *)
+      (case test_thms_fun name_thms_pairs of
+        (Success used, _) =>
+          let
+            val ordered_used = order_unique used
+            val to_use =
+              if length ordered_used < length name_thms_pairs then
+                filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
+              else
+                name_thms_pairs
+            val min_thms = (minimal test_thms to_use)
+            val min_names = order_unique (map fst min_thms)
+            val _ = println ("Minimal " ^ (length_string min_thms) ^ " theorems")
+            val _ = debug_fn (fn () => print_names min_thms)
+          in
+            answer ("Try this command: " ^ Markup.markup Markup.sendback ("apply (metis " ^ (space_implode " " min_names) ^ ")"))
+          end
+      | (Timeout, _) =>
+          answer ("Timeout: You may need to increase the time limit of " ^ (Int.toString time_limit) ^ " seconds. Call atp_minimize [time=...] ")
+      | (Error, msg) =>
+          answer ("Error in prover: " ^ msg)
+      | (Failure, _) =>
+          answer "Failure: No proof with the theorems supplied")
+      handle ResHolClause.TOO_TRIVIAL =>
+          answer ("Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
+      | ERROR msg =>
+          answer ("Error: " ^ msg)
+    end
+
+  (* isar command and parsing input *)
+
+  local structure K = OuterKeyword and P = OuterParse and T = OuterLex in
+
+  fun get_thms context =
+    map (fn (name, interval) =>
+      let
+        val thmref = Facts.Named ((name, Position.none), interval)
+        val ths = ProofContext.get_fact context thmref
+        val name' = Facts.string_of_ref thmref
+      in
+        (name', ths)
+      end)
+
+  val default_prover = "remote_vampire"
+  val default_time_limit = 5
+
+  fun get_time_limit_arg time_string =
+    (case Int.fromString time_string of
+      SOME t => t
+    | NONE => error ("Invalid time limit: " ^ quote time_string))
+
+  val get_options =
+    let
+      val def = (default_prover, default_time_limit)
+    in
+      foldl (fn ((name, a), (p, t)) => (case name of
+        "time" => (p, (get_time_limit_arg a))
+      | "atp" => (a, t)
+      | n => error ("Invalid argument: " ^ n))) def
+    end
+
+  fun sh_min_command args thm_names state =
+    let
+      val (prover_name, time_limit) = get_options args
+      val prover =
+        case AtpManager.get_prover prover_name (Proof.theory_of state) of
+          SOME prover => prover
+        | NONE => error ("Unknown prover: " ^ quote prover_name)
+      val name_thms_pairs = get_thms (Proof.context_of state) thm_names
+    in
+      minimalize prover prover_name time_limit state name_thms_pairs
+    end
+
+  val parse_args = Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname) )) []
+  val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
+
+  val _ =
+    OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag
+      (parse_args -- parse_thm_names >> (fn (args, thm_names) =>
+        Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep ((sh_min_command args thm_names) o Toplevel.proof_of)))
+
+  end
+end
+