1 (* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML |
1 (* Title: HOL/Tools/Sledgehammer/sledgehammer_minimize.ML |
2 Author: Philipp Meyer, TU Muenchen |
2 Author: Philipp Meyer, TU Muenchen |
3 Author: Jasmin Blanchette, TU Muenchen |
3 Author: Jasmin Blanchette, TU Muenchen |
4 |
4 |
5 Minimization of theorem list for Metis using automatic theorem provers. |
5 Minimization of theorem list for Metis using automatic theorem provers. |
6 *) |
6 *) |
7 |
7 |
8 signature SLEDGEHAMMER_FACT_MINIMIZE = |
8 signature SLEDGEHAMMER_MINIMIZE = |
9 sig |
9 sig |
10 type locality = Sledgehammer_Fact_Filter.locality |
10 type locality = Sledgehammer_Filter.locality |
11 type params = Sledgehammer.params |
11 type params = Sledgehammer.params |
12 |
12 |
13 val minimize_theorems : |
13 val minimize_theorems : |
14 params -> int -> int -> Proof.state -> ((string * locality) * thm list) list |
14 params -> int -> int -> Proof.state -> ((string * locality) * thm list) list |
15 -> ((string * locality) * thm list) list option * string |
15 -> ((string * locality) * thm list) list option * string |
16 val run_minimize : params -> int -> Facts.ref list -> Proof.state -> unit |
16 val run_minimize : params -> int -> Facts.ref list -> Proof.state -> unit |
17 end; |
17 end; |
18 |
18 |
19 structure Sledgehammer_Fact_Minimize : SLEDGEHAMMER_FACT_MINIMIZE = |
19 structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE = |
20 struct |
20 struct |
21 |
21 |
22 open ATP_Systems |
22 open ATP_Systems |
23 open Sledgehammer_Util |
23 open Sledgehammer_Util |
24 open Sledgehammer_Fact_Filter |
24 open Sledgehammer_Filter |
25 open Sledgehammer_Proof_Reconstruct |
25 open Sledgehammer_Reconstruct |
26 open Sledgehammer |
26 open Sledgehammer |
27 |
27 |
28 (* wrapper for calling external prover *) |
28 (* wrapper for calling external prover *) |
29 |
29 |
30 fun string_for_failure Unprovable = "Unprovable." |
30 fun string_for_failure Unprovable = "Unprovable." |