equal
deleted
inserted
replaced
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_FACT_MINIMIZE = |
9 sig |
9 sig |
|
10 type locality = Sledgehammer_Fact_Filter.locality |
10 type params = Sledgehammer.params |
11 type params = Sledgehammer.params |
11 |
12 |
12 val minimize_theorems : |
13 val minimize_theorems : |
13 params -> int -> int -> Proof.state -> ((string * bool) * thm list) list |
14 params -> int -> int -> Proof.state -> ((string * locality) * thm list) list |
14 -> ((string * bool) * thm list) list option * string |
15 -> ((string * locality) * thm list) list option * string |
15 val run_minimize : params -> int -> Facts.ref list -> Proof.state -> unit |
16 val run_minimize : params -> int -> Facts.ref list -> Proof.state -> unit |
16 end; |
17 end; |
17 |
18 |
18 structure Sledgehammer_Fact_Minimize : SLEDGEHAMMER_FACT_MINIMIZE = |
19 structure Sledgehammer_Fact_Minimize : SLEDGEHAMMER_FACT_MINIMIZE = |
19 struct |
20 struct |
118 sublinear_minimize (do_test new_timeout) |
119 sublinear_minimize (do_test new_timeout) |
119 (filter_used_facts used_thm_names axioms) ([], result) |
120 (filter_used_facts used_thm_names axioms) ([], result) |
120 val n = length min_thms |
121 val n = length min_thms |
121 val _ = priority (cat_lines |
122 val _ = priority (cat_lines |
122 ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ |
123 ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ |
123 (case length (filter (snd o fst) min_thms) of |
124 (case length (filter (curry (op =) Chained o snd o fst) min_thms) of |
124 0 => "" |
125 0 => "" |
125 | n => " (including " ^ Int.toString n ^ " chained)") ^ ".") |
126 | n => " (including " ^ Int.toString n ^ " chained)") ^ ".") |
126 in |
127 in |
127 (SOME min_thms, |
128 (SOME min_thms, |
128 proof_text isar_proof |
129 proof_text isar_proof |
147 let |
148 let |
148 val ctxt = Proof.context_of state |
149 val ctxt = Proof.context_of state |
149 val reserved = reserved_isar_keyword_table () |
150 val reserved = reserved_isar_keyword_table () |
150 val chained_ths = #facts (Proof.goal state) |
151 val chained_ths = #facts (Proof.goal state) |
151 val axioms = |
152 val axioms = |
152 maps (map (fn (name, (_, th)) => (name (), [th])) |
153 maps (map (apsnd single) |
153 o name_thm_pairs_from_ref ctxt reserved chained_ths) refs |
154 o name_thm_pairs_from_ref ctxt reserved chained_ths) refs |
154 in |
155 in |
155 case subgoal_count state of |
156 case subgoal_count state of |
156 0 => priority "No subgoal!" |
157 0 => priority "No subgoal!" |
157 | n => |
158 | n => |