20 explicit_apply: bool, |
20 explicit_apply: bool, |
21 relevance_threshold: real, |
21 relevance_threshold: real, |
22 relevance_decay: real, |
22 relevance_decay: real, |
23 max_relevant_per_iter: int option, |
23 max_relevant_per_iter: int option, |
24 theory_relevant: bool option, |
24 theory_relevant: bool option, |
25 defs_relevant: bool, |
|
26 isar_proof: bool, |
25 isar_proof: bool, |
27 isar_shrink_factor: int, |
26 isar_shrink_factor: int, |
28 timeout: Time.time} |
27 timeout: Time.time} |
29 type problem = |
28 type problem = |
30 {subgoal: int, |
29 {subgoal: int, |
89 explicit_apply: bool, |
88 explicit_apply: bool, |
90 relevance_threshold: real, |
89 relevance_threshold: real, |
91 relevance_decay: real, |
90 relevance_decay: real, |
92 max_relevant_per_iter: int option, |
91 max_relevant_per_iter: int option, |
93 theory_relevant: bool option, |
92 theory_relevant: bool option, |
94 defs_relevant: bool, |
|
95 isar_proof: bool, |
93 isar_proof: bool, |
96 isar_shrink_factor: int, |
94 isar_shrink_factor: int, |
97 timeout: Time.time} |
95 timeout: Time.time} |
98 |
96 |
99 type problem = |
97 type problem = |
214 {exec, required_execs, arguments, has_incomplete_mode, proof_delims, |
212 {exec, required_execs, arguments, has_incomplete_mode, proof_delims, |
215 known_failures, default_max_relevant_per_iter, default_theory_relevant, |
213 known_failures, default_max_relevant_per_iter, default_theory_relevant, |
216 explicit_forall, use_conjecture_for_hypotheses} |
214 explicit_forall, use_conjecture_for_hypotheses} |
217 ({debug, verbose, overlord, full_types, explicit_apply, |
215 ({debug, verbose, overlord, full_types, explicit_apply, |
218 relevance_threshold, relevance_decay, |
216 relevance_threshold, relevance_decay, |
219 max_relevant_per_iter, theory_relevant, |
217 max_relevant_per_iter, theory_relevant, isar_proof, |
220 defs_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params) |
218 isar_shrink_factor, timeout, ...} : params) |
221 minimize_command |
219 minimize_command |
222 ({subgoal, goal, relevance_override, axioms} : problem) = |
220 ({subgoal, goal, relevance_override, axioms} : problem) = |
223 let |
221 let |
224 val (ctxt, (_, th)) = goal; |
222 val (ctxt, (_, th)) = goal; |
225 val thy = ProofContext.theory_of ctxt |
223 val thy = ProofContext.theory_of ctxt |
232 val the_axioms = |
230 val the_axioms = |
233 case axioms of |
231 case axioms of |
234 SOME axioms => axioms |
232 SOME axioms => axioms |
235 | NONE => |
233 | NONE => |
236 (relevant_facts full_types relevance_threshold relevance_decay |
234 (relevant_facts full_types relevance_threshold relevance_decay |
237 defs_relevant |
|
238 (the_default default_max_relevant_per_iter |
235 (the_default default_max_relevant_per_iter |
239 max_relevant_per_iter) |
236 max_relevant_per_iter) |
240 (the_default default_theory_relevant theory_relevant) |
237 (the_default default_theory_relevant theory_relevant) |
241 relevance_override goal hyp_ts concl_t |
238 relevance_override goal hyp_ts concl_t |
242 |> tap ((fn n => print_v (fn () => |
239 |> tap ((fn n => print_v (fn () => |