82 |
82 |
83 val {context = ctxt, facts = chained, goal} = Proof.goal state |
83 val {context = ctxt, facts = chained, goal} = Proof.goal state |
84 val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt |
84 val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt |
85 val goal_t = Logic.list_implies (map prop_of chained @ hyp_ts, concl_t) |
85 val goal_t = Logic.list_implies (map prop_of chained @ hyp_ts, concl_t) |
86 |
86 |
87 fun try_methss [] = dont_know () |
87 fun try_methss [] [] = dont_know () |
88 | try_methss (meths :: methss) = |
88 | try_methss ress [] = (used_facts, hd (sort (play_outcome_ord o pairself snd) ress)) |
|
89 | try_methss ress (meths :: methss) = |
89 let |
90 let |
90 fun mk_step fact_names meths = |
91 fun mk_step fact_names meths = |
91 Prove ([], [], ("", 0), goal_t, [], ([], fact_names), meths, "") |
92 Prove ([], [], ("", 0), goal_t, [], ([], fact_names), meths, "") |
92 in |
93 in |
93 (case preplay_isar_step ctxt timeout [] (mk_step fact_names meths) of |
94 (case preplay_isar_step ctxt timeout [] (mk_step fact_names meths) of |
102 ||> (facts_of_isar_step #> snd) |
103 ||> (facts_of_isar_step #> snd) |
103 val used_facts' = filter (member (op =) used_names' o fst) used_facts |
104 val used_facts' = filter (member (op =) used_names' o fst) used_facts |
104 in |
105 in |
105 (used_facts', (meth, Played time')) |
106 (used_facts', (meth, Played time')) |
106 end |
107 end |
107 | _ => try_methss methss) |
108 | ress' => try_methss (ress' @ ress) methss) |
108 end |
109 end |
109 in |
110 in |
110 try_methss methss |
111 try_methss [] methss |
111 end |
112 end |
112 end |
113 end |
113 |
114 |
114 fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, minimize, timeout, |
115 fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, minimize, timeout, |
115 preplay_timeout, expect, ...}) mode output_result only learn |
116 preplay_timeout, expect, ...}) mode output_result only learn |