231 val _ = app (start_prover_thread params birth_time death_time i n |
231 val _ = app (start_prover_thread params birth_time death_time i n |
232 relevance_override minimize_command |
232 relevance_override minimize_command |
233 state) atps |
233 state) atps |
234 in () end |
234 in () end |
235 |
235 |
236 fun minimize override_params i fact_refs state = |
236 fun minimize override_params i frefs state = |
237 let |
237 let |
238 val thy = Proof.theory_of state |
238 val thy = Proof.theory_of state |
239 val ctxt = Proof.context_of state |
239 val ctxt = Proof.context_of state |
240 val theorems_from_refs = |
240 val chained_ths = #facts (Proof.goal state) |
241 map o pairf Facts.string_of_ref o ProofContext.get_fact |
241 fun theorems_from_ref ctxt fref = |
242 val name_thms_pairs = theorems_from_refs ctxt fact_refs |
242 let |
|
243 val ths = ProofContext.get_fact ctxt fref |
|
244 val name = Facts.string_of_ref fref |
|
245 |> forall (member Thm.eq_thm chained_ths) ths |
|
246 ? prefix chained_prefix |
|
247 in (name, ths) end |
|
248 val name_thms_pairs = map (theorems_from_ref ctxt) frefs |
243 in |
249 in |
244 case subgoal_count state of |
250 case subgoal_count state of |
245 0 => priority "No subgoal!" |
251 0 => priority "No subgoal!" |
246 | n => priority (#2 (minimize_theorems (get_params thy override_params) i n |
252 | n => priority (#2 (minimize_theorems (get_params thy override_params) i n |
247 state name_thms_pairs)) |
253 state name_thms_pairs)) |
265 val is_raw_param_relevant_for_minimize = |
271 val is_raw_param_relevant_for_minimize = |
266 member (op =) params_for_minimize o fst o unalias_raw_param |
272 member (op =) params_for_minimize o fst o unalias_raw_param |
267 fun string_for_raw_param (key, values) = |
273 fun string_for_raw_param (key, values) = |
268 key ^ (case space_implode " " values of "" => "" | value => " = " ^ value) |
274 key ^ (case space_implode " " values of "" => "" | value => " = " ^ value) |
269 |
275 |
270 fun minimize_command override_params i atp_name facts = |
276 fun minimize_command override_params i atp_name fact_names = |
271 sledgehammerN ^ " " ^ minimizeN ^ " [atp = " ^ atp_name ^ |
277 sledgehammerN ^ " " ^ minimizeN ^ " [atp = " ^ atp_name ^ |
272 (override_params |> filter is_raw_param_relevant_for_minimize |
278 (override_params |> filter is_raw_param_relevant_for_minimize |
273 |> implode o map (prefix ", " o string_for_raw_param)) ^ |
279 |> implode o map (prefix ", " o string_for_raw_param)) ^ |
274 "] (" ^ space_implode " " facts ^ ")" ^ |
280 "] (" ^ space_implode " " fact_names ^ ")" ^ |
275 (if i = 1 then "" else " " ^ string_of_int i) |
281 (if i = 1 then "" else " " ^ string_of_int i) |
276 |
282 |
277 fun hammer_away override_params subcommand opt_i relevance_override state = |
283 fun hammer_away override_params subcommand opt_i relevance_override state = |
278 let |
284 let |
279 val thy = Proof.theory_of state |
285 val thy = Proof.theory_of state |