28 |
28 |
29 fun run_prover override_params fact_override chained i n ctxt goal = |
29 fun run_prover override_params fact_override chained i n ctxt goal = |
30 let |
30 let |
31 val thy = Proof_Context.theory_of ctxt |
31 val thy = Proof_Context.theory_of ctxt |
32 val mode = Normal |
32 val mode = Normal |
33 val params as {provers, max_facts, ...} = default_params thy override_params |
33 val params as {provers, induction_rules, max_facts, ...} = default_params thy override_params |
34 val name = hd provers |
34 val name = hd provers |
35 val prover = get_prover ctxt mode name |
35 val prover = get_prover ctxt mode name |
36 val default_max_facts = default_max_facts_of_prover ctxt name |
36 val default_max_facts = default_max_facts_of_prover ctxt name |
37 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt |
37 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt |
38 val ho_atp = exists (is_ho_atp ctxt) provers |
38 val ho_atp = exists (is_ho_atp ctxt) provers |
39 val keywords = Thy_Header.get_keywords' ctxt |
39 val keywords = Thy_Header.get_keywords' ctxt |
40 val css_table = clasimpset_rule_table_of ctxt |
40 val css_table = clasimpset_rule_table_of ctxt |
|
41 val induction_rules = the_default (if ho_atp then Instantiate else Exclude) induction_rules |
41 val facts = |
42 val facts = |
42 nearly_all_facts ctxt ho_atp fact_override keywords css_table chained hyp_ts concl_t |
43 nearly_all_facts ctxt induction_rules fact_override keywords css_table chained hyp_ts concl_t |
43 |> relevant_facts ctxt params name (the_default default_max_facts max_facts) fact_override |
44 |> relevant_facts ctxt params name (the_default default_max_facts max_facts) fact_override |
44 hyp_ts concl_t |
45 hyp_ts concl_t |
45 |> hd |> snd |
46 |> hd |> snd |
46 val problem = |
47 val problem = |
47 {comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, |
48 {comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, |