1.1 --- a/src/HOL/IsaMakefile Fri Mar 19 13:02:18 2010 +0100
1.2 +++ b/src/HOL/IsaMakefile Fri Mar 19 15:07:44 2010 +0100
1.3 @@ -320,6 +320,7 @@
1.4 Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML \
1.5 Tools/Sledgehammer/sledgehammer_fol_clause.ML \
1.6 Tools/Sledgehammer/sledgehammer_hol_clause.ML \
1.7 + Tools/Sledgehammer/sledgehammer_isar.ML \
1.8 Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML \
1.9 Tools/string_code.ML \
1.10 Tools/string_syntax.ML \
2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Mar 19 13:02:18 2010 +0100
2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Mar 19 15:07:44 2010 +0100
2.3 @@ -42,8 +42,7 @@
2.4
2.5 datatype min_data = MinData of {
2.6 succs: int,
2.7 - ab_ratios: int,
2.8 - it_ratios: int
2.9 + ab_ratios: int
2.10 }
2.11
2.12 fun make_sh_data
2.13 @@ -51,8 +50,8 @@
2.14 ShData{calls=calls, success=success, lemmas=lemmas, max_lems=max_lems,
2.15 time_isa=time_isa, time_atp=time_atp, time_atp_fail=time_atp_fail}
2.16
2.17 -fun make_min_data (succs, ab_ratios, it_ratios) =
2.18 - MinData{succs=succs, ab_ratios=ab_ratios, it_ratios=it_ratios}
2.19 +fun make_min_data (succs, ab_ratios) =
2.20 + MinData{succs=succs, ab_ratios=ab_ratios}
2.21
2.22 fun make_me_data (calls,success,proofs,time,timeout,lemmas,posns) =
2.23 MeData{calls=calls, success=success, proofs=proofs, time=time,
2.24 @@ -66,8 +65,7 @@
2.25 time_atp, time_atp_fail}) = (calls, success, lemmas, max_lems, time_isa,
2.26 time_atp, time_atp_fail)
2.27
2.28 -fun tuple_of_min_data (MinData {succs, ab_ratios, it_ratios}) =
2.29 - (succs, ab_ratios, it_ratios)
2.30 +fun tuple_of_min_data (MinData {succs, ab_ratios}) = (succs, ab_ratios)
2.31
2.32 fun tuple_of_me_data (MeData {calls, success, proofs, time, timeout, lemmas,
2.33 posns}) = (calls, success, proofs, time, timeout, lemmas, posns)
2.34 @@ -147,13 +145,10 @@
2.35 => (calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail + t))
2.36
2.37 val inc_min_succs = map_min_data
2.38 - (fn (succs,ab_ratios,it_ratios) => (succs+1, ab_ratios, it_ratios))
2.39 + (fn (succs,ab_ratios) => (succs+1, ab_ratios))
2.40
2.41 fun inc_min_ab_ratios r = map_min_data
2.42 - (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios+r, it_ratios))
2.43 -
2.44 -fun inc_min_it_ratios r = map_min_data
2.45 - (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios, it_ratios+r))
2.46 + (fn (succs, ab_ratios) => (succs, ab_ratios+r))
2.47
2.48 val inc_metis_calls = map_me_data
2.49 (fn (calls,success,proofs,time,timeout,lemmas,posns)
2.50 @@ -234,10 +229,9 @@
2.51 else ()
2.52 )
2.53
2.54 -fun log_min_data log (succs, ab_ratios, it_ratios) =
2.55 +fun log_min_data log (succs, ab_ratios) =
2.56 (log ("Number of successful minimizations: " ^ string_of_int succs);
2.57 - log ("After/before ratios: " ^ string_of_int ab_ratios);
2.58 - log ("Iterations ratios: " ^ string_of_int it_ratios)
2.59 + log ("After/before ratios: " ^ string_of_int ab_ratios)
2.60 )
2.61
2.62 in
2.63 @@ -380,9 +374,10 @@
2.64
2.65 fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
2.66 let
2.67 + open ATP_Minimal
2.68 val n0 = length (these (!named_thms))
2.69 val (prover_name, prover) = get_atp (Proof.theory_of st) args
2.70 - val minimize = ATP_Minimal.minimalize prover prover_name
2.71 + val minimize = minimize_theorems linear_minimize prover prover_name
2.72 val timeout =
2.73 AList.lookup (op =) args minimize_timeoutK
2.74 |> Option.map (fst o read_int o explode)
2.75 @@ -393,7 +388,6 @@
2.76 (SOME (named_thms',its), msg) =>
2.77 (change_data id inc_min_succs;
2.78 change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));
2.79 - change_data id (inc_min_it_ratios ((100*its) div n0));
2.80 if length named_thms' = n0
2.81 then log (minimize_tag id ^ "already minimal")
2.82 else (named_thms := SOME named_thms';
3.1 --- a/src/HOL/Sledgehammer.thy Fri Mar 19 13:02:18 2010 +0100
3.2 +++ b/src/HOL/Sledgehammer.thy Fri Mar 19 15:07:44 2010 +0100
3.3 @@ -20,6 +20,7 @@
3.4 ("Tools/ATP_Manager/atp_manager.ML")
3.5 ("Tools/ATP_Manager/atp_wrapper.ML")
3.6 ("Tools/ATP_Manager/atp_minimal.ML")
3.7 + ("Tools/Sledgehammer/sledgehammer_isar.ML")
3.8 ("Tools/Sledgehammer/meson_tactic.ML")
3.9 ("Tools/Sledgehammer/metis_tactics.ML")
3.10 begin
3.11 @@ -90,6 +91,7 @@
3.12 apply (simp add: COMBC_def)
3.13 done
3.14
3.15 +
3.16 subsection {* Setup of external ATPs *}
3.17
3.18 use "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
3.19 @@ -122,6 +124,8 @@
3.20 setup {* ATP_Manager.add_prover ATP_Wrapper.remote_spass *}
3.21 setup {* ATP_Manager.add_prover ATP_Wrapper.remote_eprover *}
3.22
3.23 +use "Tools/Sledgehammer/sledgehammer_isar.ML"
3.24 +
3.25
3.26 subsection {* The MESON prover *}
3.27
4.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Mar 19 13:02:18 2010 +0100
4.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Mar 19 15:07:44 2010 +0100
4.3 @@ -282,36 +282,4 @@
4.4 val _ = List.app (fn name => start_prover name birth_time death_time 1 proof_state) provers;
4.5 in () end;
4.6
4.7 -
4.8 -
4.9 -(** Isar command syntax **)
4.10 -
4.11 -local structure K = OuterKeyword and P = OuterParse in
4.12 -
4.13 -val _ =
4.14 - OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
4.15 - (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
4.16 -
4.17 -val _ =
4.18 - OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
4.19 - (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
4.20 -
4.21 -val _ =
4.22 - OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag
4.23 - (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
4.24 - (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit)));
4.25 -
4.26 -val _ =
4.27 - OuterSyntax.improper_command "print_atps" "print external provers" K.diag
4.28 - (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
4.29 - Toplevel.keep (print_provers o Toplevel.theory_of)));
4.30 -
4.31 -val _ =
4.32 - OuterSyntax.command "sledgehammer" "call all automatic theorem provers" K.diag
4.33 - (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
4.34 - Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
4.35 -
4.36 end;
4.37 -
4.38 -end;
4.39 -
5.1 --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Mar 19 13:02:18 2010 +0100
5.2 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Mar 19 15:07:44 2010 +0100
5.3 @@ -6,27 +6,31 @@
5.4
5.5 signature ATP_MINIMAL =
5.6 sig
5.7 - val minimize: ATP_Wrapper.prover -> string -> int -> Proof.state ->
5.8 - (string * thm list) list -> ((string * thm list) list * int) option * string
5.9 - (* To be removed once TN has finished his measurements;
5.10 - the int component of the result should then be removed: *)
5.11 - val minimalize: ATP_Wrapper.prover -> string -> int -> Proof.state ->
5.12 - (string * thm list) list -> ((string * thm list) list * int) option * string
5.13 -end
5.14 + type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
5.15 + val linear_minimize : 'a minimize_fun
5.16 + val binary_minimize : 'a minimize_fun
5.17 + val minimize_theorems :
5.18 + (string * thm list) minimize_fun -> ATP_Wrapper.prover -> string -> int
5.19 + -> Proof.state -> (string * thm list) list
5.20 + -> (string * thm list) list option * string
5.21 +end;
5.22
5.23 structure ATP_Minimal : ATP_MINIMAL =
5.24 struct
5.25
5.26 -(* Linear minimization *)
5.27 +open Sledgehammer_Fact_Preprocessor
5.28
5.29 -fun lin_gen_minimize p s =
5.30 -let
5.31 - fun min [] needed = needed
5.32 - | min (x::xs) needed =
5.33 - if p(xs @ needed) then min xs needed else min xs (x::needed)
5.34 -in (min s [], length s) end;
5.35 +type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
5.36
5.37 -(* Clever minimalization algorithm *)
5.38 +(* Linear minimization algorithm *)
5.39 +
5.40 +fun linear_minimize p s =
5.41 + let
5.42 + fun aux [] needed = needed
5.43 + | aux (x :: xs) needed = aux xs (needed |> not (p (xs @ needed)) ? cons x)
5.44 + in aux s [] end;
5.45 +
5.46 +(* Binary minimalization *)
5.47
5.48 local
5.49 fun isplit (l, r) [] = (l, r)
5.50 @@ -37,24 +41,21 @@
5.51 end
5.52
5.53 local
5.54 - fun min p sup [] = raise Empty
5.55 - | min p sup [s0] = [s0]
5.56 + fun min _ _ [] = raise Empty
5.57 + | min _ _ [s0] = [s0]
5.58 | min p sup s =
5.59 let
5.60 val (l0, r0) = split s
5.61 in
5.62 - if p (sup @ l0)
5.63 - then min p sup l0
5.64 + if p (sup @ l0) then
5.65 + min p sup l0
5.66 + else if p (sup @ r0) then
5.67 + min p sup r0
5.68 else
5.69 - if p (sup @ r0)
5.70 - then min p sup r0
5.71 - else
5.72 - let
5.73 - val l = min p (sup @ r0) l0
5.74 - val r = min p (sup @ l) r0
5.75 - in
5.76 - l @ r
5.77 - end
5.78 + let
5.79 + val l = min p (sup @ r0) l0
5.80 + val r = min p (sup @ l) r0
5.81 + in l @ r end
5.82 end
5.83 in
5.84 (* return a minimal subset v of s that satisfies p
5.85 @@ -62,15 +63,10 @@
5.86 @post v subset s & p(v) &
5.87 forall e in v. ~p(v \ e)
5.88 *)
5.89 - fun minimal p s =
5.90 - let
5.91 - val count = Unsynchronized.ref 0
5.92 - fun p_count xs = (Unsynchronized.inc count; p xs)
5.93 - val v =
5.94 - (case min p_count [] s of
5.95 - [x] => if p_count [] then [] else [x]
5.96 - | m => m);
5.97 - in (v, ! count) end
5.98 + fun binary_minimize p s =
5.99 + case min p [] s of
5.100 + [x] => if p [] then [] else [x]
5.101 + | m => m
5.102 end
5.103
5.104
5.105 @@ -91,7 +87,7 @@
5.106 ("# Cannot determine problem status within resource limit", Timeout),
5.107 ("Error", Error)]
5.108
5.109 -fun produce_answer (result: ATP_Wrapper.prover_result) =
5.110 +fun produce_answer (result : ATP_Wrapper.prover_result) =
5.111 let
5.112 val {success, proof = result_string, internal_thm_names = thm_name_vec,
5.113 filtered_clauses = filtered, ...} = result
5.114 @@ -116,7 +112,7 @@
5.115 let
5.116 val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ")
5.117 val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
5.118 - val axclauses = Sledgehammer_Fact_Preprocessor.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
5.119 + val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
5.120 val {context = ctxt, facts, goal} = Proof.goal state
5.121 val problem =
5.122 {with_full_types = ! ATP_Manager.full_types,
5.123 @@ -133,7 +129,8 @@
5.124
5.125 (* minimalization of thms *)
5.126
5.127 -fun gen_minimalize gen_min prover prover_name time_limit state name_thms_pairs =
5.128 +fun minimize_theorems gen_min prover prover_name time_limit state
5.129 + name_thms_pairs =
5.130 let
5.131 val _ =
5.132 priority ("Minimize called with " ^ string_of_int (length name_thms_pairs) ^
5.133 @@ -152,15 +149,14 @@
5.134 if length ordered_used < length name_thms_pairs then
5.135 filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
5.136 else name_thms_pairs
5.137 - val (min_thms, n) =
5.138 - if null to_use then ([], 0)
5.139 + val min_thms =
5.140 + if null to_use then []
5.141 else gen_min (test_thms (SOME filtered)) to_use
5.142 val min_names = sort_distinct string_ord (map fst min_thms)
5.143 val _ = priority (cat_lines
5.144 - ["Iterations: " ^ string_of_int n (* FIXME TN remove later *),
5.145 - "Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
5.146 + ["Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
5.147 in
5.148 - (SOME (min_thms, n), "Try this command: " ^
5.149 + (SOME min_thms, "Try this command: " ^
5.150 Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")"))
5.151 end
5.152 | (Timeout, _) =>
5.153 @@ -171,67 +167,8 @@
5.154 | (Failure, _) =>
5.155 (NONE, "Failure: No proof with the theorems supplied"))
5.156 handle Sledgehammer_HOL_Clause.TRIVIAL =>
5.157 - (SOME ([], 0), "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
5.158 + (SOME [], "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
5.159 | ERROR msg => (NONE, "Error: " ^ msg)
5.160 end
5.161
5.162 -
5.163 -(* Isar command and parsing input *)
5.164 -
5.165 -local structure K = OuterKeyword and P = OuterParse and T = OuterLex in
5.166 -
5.167 -fun get_thms context =
5.168 - map (fn (name, interval) =>
5.169 - let
5.170 - val thmref = Facts.Named ((name, Position.none), interval)
5.171 - val ths = ProofContext.get_fact context thmref
5.172 - val name' = Facts.string_of_ref thmref
5.173 - in
5.174 - (name', ths)
5.175 - end)
5.176 -
5.177 -val default_prover = "remote_vampire"
5.178 -val default_time_limit = 5
5.179 -
5.180 -fun get_time_limit_arg time_string =
5.181 - (case Int.fromString time_string of
5.182 - SOME t => t
5.183 - | NONE => error ("Invalid time limit: " ^ quote time_string))
5.184 -
5.185 -fun get_opt (name, a) (p, t) =
5.186 - (case name of
5.187 - "time" => (p, get_time_limit_arg a)
5.188 - | "atp" => (a, t)
5.189 - | n => error ("Invalid argument: " ^ n))
5.190 -
5.191 -fun get_options args = fold get_opt args (default_prover, default_time_limit)
5.192 -
5.193 -val minimize = gen_minimalize lin_gen_minimize
5.194 -
5.195 -val minimalize = gen_minimalize minimal
5.196 -
5.197 -fun sh_min_command args thm_names state =
5.198 - let
5.199 - val (prover_name, time_limit) = get_options args
5.200 - val prover =
5.201 - (case ATP_Manager.get_prover (Proof.theory_of state) prover_name of
5.202 - SOME prover => prover
5.203 - | NONE => error ("Unknown prover: " ^ quote prover_name))
5.204 - val name_thms_pairs = get_thms (Proof.context_of state) thm_names
5.205 - in
5.206 - writeln (#2 (minimize prover prover_name time_limit state name_thms_pairs))
5.207 - end
5.208 -
5.209 -val parse_args =
5.210 - Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
5.211 -val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
5.212 -
5.213 -val _ =
5.214 - OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag
5.215 - (parse_args -- parse_thm_names >> (fn (args, thm_names) =>
5.216 - Toplevel.no_timing o Toplevel.unknown_proof o
5.217 - Toplevel.keep (sh_min_command args thm_names o Toplevel.proof_of)))
5.218 -
5.219 -end
5.220 -
5.221 -end
5.222 +end;
6.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri Mar 19 13:02:18 2010 +0100
6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri Mar 19 15:07:44 2010 +0100
6.3 @@ -13,7 +13,7 @@
6.4 val auto: bool Unsynchronized.ref
6.5 val default_params : theory -> (string * string) list -> params
6.6 val setup : theory -> theory
6.7 -end
6.8 +end;
6.9
6.10 structure Nitpick_Isar : NITPICK_ISAR =
6.11 struct
7.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Mar 19 13:02:18 2010 +0100
7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Mar 19 15:07:44 2010 +0100
7.3 @@ -12,7 +12,7 @@
7.4 hol_context -> (typ option * bool option) list
7.5 -> (typ option * bool option) list -> term
7.6 -> term list * term list * bool * bool * bool
7.7 -end
7.8 +end;
7.9
7.10 structure Nitpick_Preproc : NITPICK_PREPROC =
7.11 struct
8.1 --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Fri Mar 19 13:02:18 2010 +0100
8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Fri Mar 19 15:07:44 2010 +0100
8.3 @@ -8,7 +8,7 @@
8.4 signature NITPICK_TESTS =
8.5 sig
8.6 val run_all_tests : unit -> unit
8.7 -end
8.8 +end;
8.9
8.10 structure Nitpick_Tests =
8.11 struct
9.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Mar 19 13:02:18 2010 +0100
9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Mar 19 15:07:44 2010 +0100
9.3 @@ -62,7 +62,7 @@
9.4 val pstrs : string -> Pretty.T list
9.5 val unyxml : string -> string
9.6 val maybe_quote : string -> string
9.7 -end
9.8 +end;
9.9
9.10 structure Nitpick_Util : NITPICK_UTIL =
9.11 struct
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Mar 19 15:07:44 2010 +0100
10.3 @@ -0,0 +1,87 @@
10.4 +(* Title: HOL/Sledgehammer/sledgehammer_isar.ML
10.5 + Author: Jasmin Blanchette, TU Muenchen
10.6 +
10.7 +Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax.
10.8 +*)
10.9 +
10.10 +structure Sledgehammer_Isar : sig end =
10.11 +struct
10.12 +
10.13 +open ATP_Manager
10.14 +open ATP_Minimal
10.15 +
10.16 +structure K = OuterKeyword and P = OuterParse
10.17 +
10.18 +val _ =
10.19 + OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
10.20 + (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
10.21 +
10.22 +val _ =
10.23 + OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
10.24 + (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
10.25 +
10.26 +val _ =
10.27 + OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag
10.28 + (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
10.29 + (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit)));
10.30 +
10.31 +val _ =
10.32 + OuterSyntax.improper_command "print_atps" "print external provers" K.diag
10.33 + (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
10.34 + Toplevel.keep (print_provers o Toplevel.theory_of)));
10.35 +
10.36 +val _ =
10.37 + OuterSyntax.command "sledgehammer"
10.38 + "search for first-order proof using automatic theorem provers" K.diag
10.39 + (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
10.40 + Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
10.41 +
10.42 +val default_minimize_prover = "remote_vampire"
10.43 +val default_minimize_time_limit = 5
10.44 +
10.45 +fun atp_minimize_command args thm_names state =
10.46 + let
10.47 + fun theorems_from_names ctxt =
10.48 + map (fn (name, interval) =>
10.49 + let
10.50 + val thmref = Facts.Named ((name, Position.none), interval)
10.51 + val ths = ProofContext.get_fact ctxt thmref
10.52 + val name' = Facts.string_of_ref thmref
10.53 + in (name', ths) end)
10.54 + fun get_time_limit_arg time_string =
10.55 + (case Int.fromString time_string of
10.56 + SOME t => t
10.57 + | NONE => error ("Invalid time limit: " ^ quote time_string))
10.58 + fun get_opt (name, a) (p, t) =
10.59 + (case name of
10.60 + "time" => (p, get_time_limit_arg a)
10.61 + | "atp" => (a, t)
10.62 + | n => error ("Invalid argument: " ^ n))
10.63 + fun get_options args =
10.64 + fold get_opt args (default_minimize_prover, default_minimize_time_limit)
10.65 + val (prover_name, time_limit) = get_options args
10.66 + val prover =
10.67 + (case ATP_Manager.get_prover (Proof.theory_of state) prover_name of
10.68 + SOME prover => prover
10.69 + | NONE => error ("Unknown prover: " ^ quote prover_name))
10.70 + val name_thms_pairs = theorems_from_names (Proof.context_of state) thm_names
10.71 + in
10.72 + writeln (#2 (minimize_theorems linear_minimize prover prover_name time_limit
10.73 + state name_thms_pairs))
10.74 + end
10.75 +
10.76 +local structure K = OuterKeyword and P = OuterParse in
10.77 +
10.78 +val parse_args =
10.79 + Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
10.80 +val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
10.81 +
10.82 +val _ =
10.83 + OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag
10.84 + (parse_args -- parse_thm_names >> (fn (args, thm_names) =>
10.85 + Toplevel.no_timing o Toplevel.unknown_proof o
10.86 + Toplevel.keep (atp_minimize_command args thm_names o Toplevel.proof_of)))
10.87 +
10.88 +end
10.89 +
10.90 +end;