154 |
154 |
155 fun generate_proof_text () = |
155 fun generate_proof_text () = |
156 let |
156 let |
157 val (verbose, alt_metis_args, preplay_timeout, compress, try0, minimize, atp_proof0, goal) = |
157 val (verbose, alt_metis_args, preplay_timeout, compress, try0, minimize, atp_proof0, goal) = |
158 isar_params () |
158 isar_params () |
159 |
159 in |
160 val systematic_methods' = insert (op =) (Metis_Method alt_metis_args) systematic_methods |
160 if null atp_proof0 then |
161 |
161 one_line_proof_text ctxt 0 one_line_params |
162 fun massage_methods (meths as meth :: _) = |
162 else |
163 if not try0 then [meth] |
|
164 else if smt_proofs = SOME true then SMT_Method :: meths |
|
165 else meths |
|
166 |
|
167 val (params, _, concl_t) = strip_subgoal goal subgoal ctxt |
|
168 val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params |
|
169 val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd |
|
170 |
|
171 val do_preplay = preplay_timeout <> Time.zeroTime |
|
172 val compress = |
|
173 (case compress of |
|
174 NONE => if isar_proofs = NONE andalso do_preplay then 1000.0 else 10.0 |
|
175 | SOME n => n) |
|
176 |
|
177 fun is_fixed ctxt = Variable.is_declared ctxt orf Name.is_skolem |
|
178 fun skolems_of ctxt t = Term.add_frees t [] |> filter_out (is_fixed ctxt o fst) |> rev |
|
179 |
|
180 fun get_role keep_role ((num, _), role, t, rule, _) = |
|
181 if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE |
|
182 |
|
183 val atp_proof = |
|
184 fold_rev add_line_pass1 atp_proof0 [] |
|
185 |> add_lines_pass2 [] |
|
186 |
|
187 val conjs = |
|
188 map_filter (fn (name, role, _, _, _) => |
|
189 if member (op =) [Conjecture, Negated_Conjecture] role then SOME name else NONE) |
|
190 atp_proof |
|
191 val assms = map_filter (Option.map fst o get_role (curry (op =) Hypothesis)) atp_proof |
|
192 |
|
193 fun add_lemma ((l, t), rule) ctxt = |
|
194 let |
163 let |
195 val (skos, meths) = |
164 val systematic_methods' = insert (op =) (Metis_Method alt_metis_args) systematic_methods |
196 (if is_skolemize_rule rule then (skolems_of ctxt t, skolem_methods) |
165 |
197 else if is_arith_rule rule then ([], arith_methods) |
166 fun massage_methods (meths as meth :: _) = |
198 else ([], rewrite_methods)) |
167 if not try0 then [meth] |
199 ||> massage_methods |
168 else if smt_proofs = SOME true then SMT_Method :: meths |
|
169 else meths |
|
170 |
|
171 val (params, _, concl_t) = strip_subgoal goal subgoal ctxt |
|
172 val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params |
|
173 val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd |
|
174 |
|
175 val do_preplay = preplay_timeout <> Time.zeroTime |
|
176 val compress = |
|
177 (case compress of |
|
178 NONE => if isar_proofs = NONE andalso do_preplay then 1000.0 else 10.0 |
|
179 | SOME n => n) |
|
180 |
|
181 fun is_fixed ctxt = Variable.is_declared ctxt orf Name.is_skolem |
|
182 fun skolems_of ctxt t = Term.add_frees t [] |> filter_out (is_fixed ctxt o fst) |> rev |
|
183 |
|
184 fun get_role keep_role ((num, _), role, t, rule, _) = |
|
185 if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE |
|
186 |
|
187 val atp_proof = |
|
188 fold_rev add_line_pass1 atp_proof0 [] |
|
189 |> add_lines_pass2 [] |
|
190 |
|
191 val conjs = |
|
192 map_filter (fn (name, role, _, _, _) => |
|
193 if member (op =) [Conjecture, Negated_Conjecture] role then SOME name else NONE) |
|
194 atp_proof |
|
195 val assms = map_filter (Option.map fst o get_role (curry (op =) Hypothesis)) atp_proof |
|
196 |
|
197 fun add_lemma ((l, t), rule) ctxt = |
|
198 let |
|
199 val (skos, meths) = |
|
200 (if is_skolemize_rule rule then (skolems_of ctxt t, skolem_methods) |
|
201 else if is_arith_rule rule then ([], arith_methods) |
|
202 else ([], rewrite_methods)) |
|
203 ||> massage_methods |
|
204 in |
|
205 (Prove ([], skos, l, t, [], ([], []), meths, ""), |
|
206 ctxt |> not (null skos) ? (Variable.add_fixes (map fst skos) #> snd)) |
|
207 end |
|
208 |
|
209 val (lems, _) = |
|
210 fold_map add_lemma (map_filter (get_role (curry (op =) Lemma)) atp_proof) ctxt |
|
211 |
|
212 val bot = #1 (List.last atp_proof) |
|
213 |
|
214 val refute_graph = |
|
215 atp_proof |
|
216 |> map (fn (name, _, _, _, from) => (from, name)) |
|
217 |> make_refute_graph bot |
|
218 |> fold (Atom_Graph.default_node o rpair ()) conjs |
|
219 |
|
220 val axioms = axioms_of_refute_graph refute_graph conjs |
|
221 |
|
222 val tainted = tainted_atoms_of_refute_graph refute_graph conjs |
|
223 val is_clause_tainted = exists (member (op =) tainted) |
|
224 val steps = |
|
225 Symtab.empty |
|
226 |> fold (fn (name as (s, _), role, t, rule, _) => |
|
227 Symtab.update_new (s, (rule, t |
|
228 |> (if is_clause_tainted [name] then |
|
229 HOLogic.dest_Trueprop |
|
230 #> role <> Conjecture ? s_not |
|
231 #> fold exists_of (map Var (Term.add_vars t [])) |
|
232 #> HOLogic.mk_Trueprop |
|
233 else |
|
234 I)))) |
|
235 atp_proof |
|
236 |
|
237 fun is_referenced_in_step _ (Let _) = false |
|
238 | is_referenced_in_step l (Prove (_, _, _, _, subs, (ls, _), _, _)) = |
|
239 member (op =) ls l orelse exists (is_referenced_in_proof l) subs |
|
240 and is_referenced_in_proof l (Proof (_, _, steps)) = |
|
241 exists (is_referenced_in_step l) steps |
|
242 |
|
243 fun insert_lemma_in_step lem |
|
244 (step as Prove (qs, fix, l, t, subs, (ls, gs), meths, comment)) = |
|
245 let val l' = the (label_of_isar_step lem) in |
|
246 if member (op =) ls l' then |
|
247 [lem, step] |
|
248 else |
|
249 let val refs = map (is_referenced_in_proof l') subs in |
|
250 if length (filter I refs) = 1 then |
|
251 let |
|
252 val subs' = map2 (fn false => I | true => insert_lemma_in_proof lem) refs |
|
253 subs |
|
254 in |
|
255 [Prove (qs, fix, l, t, subs', (ls, gs), meths, comment)] |
|
256 end |
|
257 else |
|
258 [lem, step] |
|
259 end |
|
260 end |
|
261 and insert_lemma_in_steps lem [] = [lem] |
|
262 | insert_lemma_in_steps lem (step :: steps) = |
|
263 if is_referenced_in_step (the (label_of_isar_step lem)) step then |
|
264 insert_lemma_in_step lem step @ steps |
|
265 else |
|
266 step :: insert_lemma_in_steps lem steps |
|
267 and insert_lemma_in_proof lem (Proof (fix, assms, steps)) = |
|
268 Proof (fix, assms, insert_lemma_in_steps lem steps) |
|
269 |
|
270 val rule_of_clause_id = fst o the o Symtab.lookup steps o fst |
|
271 |
|
272 val finish_off = close_form #> rename_bound_vars |
|
273 |
|
274 fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> finish_off |
|
275 | prop_of_clause names = |
|
276 let |
|
277 val lits = |
|
278 map (HOLogic.dest_Trueprop o snd) (map_filter (Symtab.lookup steps o fst) names) |
|
279 in |
|
280 (case List.partition (can HOLogic.dest_not) lits of |
|
281 (negs as _ :: _, pos as _ :: _) => |
|
282 s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), |
|
283 Library.foldr1 s_disj pos) |
|
284 | _ => fold (curry s_disj) lits @{term False}) |
|
285 end |
|
286 |> HOLogic.mk_Trueprop |> finish_off |
|
287 |
|
288 fun maybe_show outer c = if outer andalso eq_set (op =) (c, conjs) then [Show] else [] |
|
289 |
|
290 fun isar_steps outer predecessor accum [] = |
|
291 accum |
|
292 |> (if tainted = [] then |
|
293 (* e.g., trivial, empty proof by Z3 *) |
|
294 cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [], |
|
295 sort_facts (the_list predecessor, []), massage_methods systematic_methods', |
|
296 "")) |
|
297 else |
|
298 I) |
|
299 |> rev |
|
300 | isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) = |
|
301 let |
|
302 val l = label_of_clause c |
|
303 val t = prop_of_clause c |
|
304 val rule = rule_of_clause_id id |
|
305 val skolem = is_skolemize_rule rule |
|
306 |
|
307 val deps = ([], []) |
|
308 |> fold add_fact_of_dependency gamma |
|
309 |> is_maybe_ext_rule rule ? add_global_fact [short_thm_name ctxt ext] |
|
310 |> sort_facts |
|
311 val meths = |
|
312 (if skolem then skolem_methods |
|
313 else if is_arith_rule rule then arith_methods |
|
314 else if is_datatype_rule rule then datatype_methods |
|
315 else systematic_methods') |
|
316 |> massage_methods |
|
317 |
|
318 fun prove sub facts = Prove (maybe_show outer c, [], l, t, sub, facts, meths, "") |
|
319 fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs |
|
320 in |
|
321 if is_clause_tainted c then |
|
322 (case gamma of |
|
323 [g] => |
|
324 if skolem andalso is_clause_tainted g then |
|
325 let |
|
326 val skos = skolems_of ctxt (prop_of_clause g) |
|
327 val subproof = Proof (skos, [], rev accum) |
|
328 in |
|
329 isar_steps outer (SOME l) [prove [subproof] ([], [])] infs |
|
330 end |
|
331 else |
|
332 steps_of_rest (prove [] deps) |
|
333 | _ => steps_of_rest (prove [] deps)) |
|
334 else |
|
335 steps_of_rest |
|
336 (if skolem then |
|
337 (case skolems_of ctxt t of |
|
338 [] => prove [] deps |
|
339 | skos => Prove ([], skos, l, t, [], deps, meths, "")) |
|
340 else |
|
341 prove [] deps) |
|
342 end |
|
343 | isar_steps outer predecessor accum (Cases cases :: infs) = |
|
344 let |
|
345 fun isar_case (c, subinfs) = |
|
346 isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] subinfs |
|
347 val c = succedent_of_cases cases |
|
348 val l = label_of_clause c |
|
349 val t = prop_of_clause c |
|
350 val step = |
|
351 Prove (maybe_show outer c, [], l, t, |
|
352 map isar_case (filter_out (null o snd) cases), |
|
353 sort_facts (the_list predecessor, []), massage_methods systematic_methods', |
|
354 "") |
|
355 in |
|
356 isar_steps outer (SOME l) (step :: accum) infs |
|
357 end |
|
358 and isar_proof outer fix assms lems infs = |
|
359 Proof (fix, assms, |
|
360 fold_rev insert_lemma_in_steps lems (isar_steps outer NONE [] infs)) |
|
361 |
|
362 val trace = Config.get ctxt trace |
|
363 |
|
364 val canonical_isar_proof = |
|
365 refute_graph |
|
366 |> trace ? tap (tracing o prefix "Refute graph:\n" o string_of_refute_graph) |
|
367 |> redirect_graph axioms tainted bot |
|
368 |> trace ? tap (tracing o prefix "Direct proof:\n" o string_of_direct_proof) |
|
369 |> isar_proof true params assms lems |
|
370 |> postprocess_isar_proof_remove_show_stuttering |
|
371 |> postprocess_isar_proof_remove_unreferenced_steps I |
|
372 |> relabel_isar_proof_canonically |
|
373 |
|
374 val ctxt = ctxt |> enrich_context_with_local_facts canonical_isar_proof |
|
375 |
|
376 val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty |
|
377 |
|
378 val _ = fold_isar_steps (fn meth => |
|
379 K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth [])) |
|
380 (steps_of_isar_proof canonical_isar_proof) () |
|
381 |
|
382 fun str_of_preplay_outcome outcome = |
|
383 if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?" |
|
384 fun str_of_meth l meth = |
|
385 string_of_proof_method ctxt [] meth ^ " " ^ |
|
386 str_of_preplay_outcome |
|
387 (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) |
|
388 fun comment_of l = map (str_of_meth l) #> commas |
|
389 |
|
390 fun trace_isar_proof label proof = |
|
391 if trace then |
|
392 tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ |
|
393 string_of_isar_proof ctxt subgoal subgoal_count |
|
394 (comment_isar_proof comment_of proof) ^ "\n") |
|
395 else |
|
396 () |
|
397 |
|
398 fun comment_of l (meth :: _) = |
|
399 (case (verbose, |
|
400 Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)) of |
|
401 (false, Played _) => "" |
|
402 | (_, outcome) => string_of_play_outcome outcome) |
|
403 |
|
404 val (play_outcome, isar_proof) = |
|
405 canonical_isar_proof |
|
406 |> tap (trace_isar_proof "Original") |
|
407 |> compress_isar_proof ctxt compress preplay_timeout preplay_data |
|
408 |> tap (trace_isar_proof "Compressed") |
|
409 |> postprocess_isar_proof_remove_unreferenced_steps |
|
410 (keep_fastest_method_of_isar_step (!preplay_data) |
|
411 #> minimize ? minimize_isar_step_dependencies ctxt preplay_data) |
|
412 |> tap (trace_isar_proof "Minimized") |
|
413 |> `(preplay_outcome_of_isar_proof (!preplay_data)) |
|
414 ||> (comment_isar_proof comment_of |
|
415 #> chain_isar_proof |
|
416 #> kill_useless_labels_in_isar_proof |
|
417 #> relabel_isar_proof_nicely |
|
418 #> rationalize_obtains_in_isar_proofs ctxt) |
200 in |
419 in |
201 (Prove ([], skos, l, t, [], ([], []), meths, ""), |
420 (case (num_chained, add_isar_steps (steps_of_isar_proof isar_proof) 0) of |
202 ctxt |> not (null skos) ? (Variable.add_fixes (map fst skos) #> snd)) |
421 (0, 1) => |
|
422 one_line_proof_text ctxt 0 |
|
423 (if play_outcome_ord (play_outcome, one_line_play) = LESS then |
|
424 (case isar_proof of |
|
425 Proof (_, _, [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)]) => |
|
426 let |
|
427 val used_facts' = filter (fn (s, (sc, _)) => |
|
428 member (op =) gfs s andalso sc <> Chained) used_facts |
|
429 in |
|
430 ((used_facts', (meth, play_outcome)), banner, subgoal, subgoal_count) |
|
431 end) |
|
432 else |
|
433 one_line_params) ^ |
|
434 (if isar_proofs = SOME true then "\n(No Isar proof available.)" else "") |
|
435 | (_, num_steps) => |
|
436 let |
|
437 val msg = |
|
438 (if verbose then [string_of_int num_steps ^ " step" ^ plural_s num_steps] |
|
439 else []) @ |
|
440 (if do_preplay then [string_of_play_outcome play_outcome] else []) |
|
441 in |
|
442 one_line_proof_text ctxt 0 one_line_params ^ |
|
443 "\n\nIsar proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^ |
|
444 Active.sendback_markup [Markup.padding_command] |
|
445 (string_of_isar_proof ctxt subgoal subgoal_count isar_proof) |
|
446 end) |
203 end |
447 end |
204 |
|
205 val (lems, _) = |
|
206 fold_map add_lemma (map_filter (get_role (curry (op =) Lemma)) atp_proof) ctxt |
|
207 |
|
208 val bot = #1 (List.last atp_proof) |
|
209 |
|
210 val refute_graph = |
|
211 atp_proof |
|
212 |> map (fn (name, _, _, _, from) => (from, name)) |
|
213 |> make_refute_graph bot |
|
214 |> fold (Atom_Graph.default_node o rpair ()) conjs |
|
215 |
|
216 val axioms = axioms_of_refute_graph refute_graph conjs |
|
217 |
|
218 val tainted = tainted_atoms_of_refute_graph refute_graph conjs |
|
219 val is_clause_tainted = exists (member (op =) tainted) |
|
220 val steps = |
|
221 Symtab.empty |
|
222 |> fold (fn (name as (s, _), role, t, rule, _) => |
|
223 Symtab.update_new (s, (rule, t |
|
224 |> (if is_clause_tainted [name] then |
|
225 HOLogic.dest_Trueprop |
|
226 #> role <> Conjecture ? s_not |
|
227 #> fold exists_of (map Var (Term.add_vars t [])) |
|
228 #> HOLogic.mk_Trueprop |
|
229 else |
|
230 I)))) |
|
231 atp_proof |
|
232 |
|
233 fun is_referenced_in_step _ (Let _) = false |
|
234 | is_referenced_in_step l (Prove (_, _, _, _, subs, (ls, _), _, _)) = |
|
235 member (op =) ls l orelse exists (is_referenced_in_proof l) subs |
|
236 and is_referenced_in_proof l (Proof (_, _, steps)) = |
|
237 exists (is_referenced_in_step l) steps |
|
238 |
|
239 fun insert_lemma_in_step lem |
|
240 (step as Prove (qs, fix, l, t, subs, (ls, gs), meths, comment)) = |
|
241 let val l' = the (label_of_isar_step lem) in |
|
242 if member (op =) ls l' then |
|
243 [lem, step] |
|
244 else |
|
245 let val refs = map (is_referenced_in_proof l') subs in |
|
246 if length (filter I refs) = 1 then |
|
247 let |
|
248 val subs' = map2 (fn false => I | true => insert_lemma_in_proof lem) refs subs |
|
249 in |
|
250 [Prove (qs, fix, l, t, subs', (ls, gs), meths, comment)] |
|
251 end |
|
252 else |
|
253 [lem, step] |
|
254 end |
|
255 end |
|
256 and insert_lemma_in_steps lem [] = [lem] |
|
257 | insert_lemma_in_steps lem (step :: steps) = |
|
258 if is_referenced_in_step (the (label_of_isar_step lem)) step then |
|
259 insert_lemma_in_step lem step @ steps |
|
260 else |
|
261 step :: insert_lemma_in_steps lem steps |
|
262 and insert_lemma_in_proof lem (Proof (fix, assms, steps)) = |
|
263 Proof (fix, assms, insert_lemma_in_steps lem steps) |
|
264 |
|
265 val rule_of_clause_id = fst o the o Symtab.lookup steps o fst |
|
266 |
|
267 val finish_off = close_form #> rename_bound_vars |
|
268 |
|
269 fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> finish_off |
|
270 | prop_of_clause names = |
|
271 let |
|
272 val lits = |
|
273 map (HOLogic.dest_Trueprop o snd) (map_filter (Symtab.lookup steps o fst) names) |
|
274 in |
|
275 (case List.partition (can HOLogic.dest_not) lits of |
|
276 (negs as _ :: _, pos as _ :: _) => |
|
277 s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos) |
|
278 | _ => fold (curry s_disj) lits @{term False}) |
|
279 end |
|
280 |> HOLogic.mk_Trueprop |> finish_off |
|
281 |
|
282 fun maybe_show outer c = if outer andalso eq_set (op =) (c, conjs) then [Show] else [] |
|
283 |
|
284 fun isar_steps outer predecessor accum [] = |
|
285 accum |
|
286 |> (if tainted = [] then |
|
287 (* e.g., trivial, empty proof by Z3 *) |
|
288 cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [], |
|
289 sort_facts (the_list predecessor, []), massage_methods systematic_methods', "")) |
|
290 else |
|
291 I) |
|
292 |> rev |
|
293 | isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) = |
|
294 let |
|
295 val l = label_of_clause c |
|
296 val t = prop_of_clause c |
|
297 val rule = rule_of_clause_id id |
|
298 val skolem = is_skolemize_rule rule |
|
299 |
|
300 val deps = ([], []) |
|
301 |> fold add_fact_of_dependency gamma |
|
302 |> is_maybe_ext_rule rule ? add_global_fact [short_thm_name ctxt ext] |
|
303 |> sort_facts |
|
304 val meths = |
|
305 (if skolem then skolem_methods |
|
306 else if is_arith_rule rule then arith_methods |
|
307 else if is_datatype_rule rule then datatype_methods |
|
308 else systematic_methods') |
|
309 |> massage_methods |
|
310 |
|
311 fun prove sub facts = Prove (maybe_show outer c, [], l, t, sub, facts, meths, "") |
|
312 fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs |
|
313 in |
|
314 if is_clause_tainted c then |
|
315 (case gamma of |
|
316 [g] => |
|
317 if skolem andalso is_clause_tainted g then |
|
318 let |
|
319 val skos = skolems_of ctxt (prop_of_clause g) |
|
320 val subproof = Proof (skos, [], rev accum) |
|
321 in |
|
322 isar_steps outer (SOME l) [prove [subproof] ([], [])] infs |
|
323 end |
|
324 else |
|
325 steps_of_rest (prove [] deps) |
|
326 | _ => steps_of_rest (prove [] deps)) |
|
327 else |
|
328 steps_of_rest |
|
329 (if skolem then |
|
330 (case skolems_of ctxt t of |
|
331 [] => prove [] deps |
|
332 | skos => Prove ([], skos, l, t, [], deps, meths, "")) |
|
333 else |
|
334 prove [] deps) |
|
335 end |
|
336 | isar_steps outer predecessor accum (Cases cases :: infs) = |
|
337 let |
|
338 fun isar_case (c, subinfs) = |
|
339 isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] subinfs |
|
340 val c = succedent_of_cases cases |
|
341 val l = label_of_clause c |
|
342 val t = prop_of_clause c |
|
343 val step = |
|
344 Prove (maybe_show outer c, [], l, t, |
|
345 map isar_case (filter_out (null o snd) cases), |
|
346 sort_facts (the_list predecessor, []), massage_methods systematic_methods', "") |
|
347 in |
|
348 isar_steps outer (SOME l) (step :: accum) infs |
|
349 end |
|
350 and isar_proof outer fix assms lems infs = |
|
351 Proof (fix, assms, fold_rev insert_lemma_in_steps lems (isar_steps outer NONE [] infs)) |
|
352 |
|
353 val trace = Config.get ctxt trace |
|
354 |
|
355 val canonical_isar_proof = |
|
356 refute_graph |
|
357 |> trace ? tap (tracing o prefix "Refute graph:\n" o string_of_refute_graph) |
|
358 |> redirect_graph axioms tainted bot |
|
359 |> trace ? tap (tracing o prefix "Direct proof:\n" o string_of_direct_proof) |
|
360 |> isar_proof true params assms lems |
|
361 |> postprocess_isar_proof_remove_show_stuttering |
|
362 |> postprocess_isar_proof_remove_unreferenced_steps I |
|
363 |> relabel_isar_proof_canonically |
|
364 |
|
365 val ctxt = ctxt |> enrich_context_with_local_facts canonical_isar_proof |
|
366 |
|
367 val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty |
|
368 |
|
369 val _ = fold_isar_steps (fn meth => |
|
370 K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth [])) |
|
371 (steps_of_isar_proof canonical_isar_proof) () |
|
372 |
|
373 fun str_of_preplay_outcome outcome = |
|
374 if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?" |
|
375 fun str_of_meth l meth = |
|
376 string_of_proof_method ctxt [] meth ^ " " ^ |
|
377 str_of_preplay_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) |
|
378 fun comment_of l = map (str_of_meth l) #> commas |
|
379 |
|
380 fun trace_isar_proof label proof = |
|
381 if trace then |
|
382 tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ |
|
383 string_of_isar_proof ctxt subgoal subgoal_count |
|
384 (comment_isar_proof comment_of proof) ^ "\n") |
|
385 else |
|
386 () |
|
387 |
|
388 fun comment_of l (meth :: _) = |
|
389 (case (verbose, |
|
390 Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)) of |
|
391 (false, Played _) => "" |
|
392 | (_, outcome) => string_of_play_outcome outcome) |
|
393 |
|
394 val (play_outcome, isar_proof) = |
|
395 canonical_isar_proof |
|
396 |> tap (trace_isar_proof "Original") |
|
397 |> compress_isar_proof ctxt compress preplay_timeout preplay_data |
|
398 |> tap (trace_isar_proof "Compressed") |
|
399 |> postprocess_isar_proof_remove_unreferenced_steps |
|
400 (keep_fastest_method_of_isar_step (!preplay_data) |
|
401 #> minimize ? minimize_isar_step_dependencies ctxt preplay_data) |
|
402 |> tap (trace_isar_proof "Minimized") |
|
403 |> `(preplay_outcome_of_isar_proof (!preplay_data)) |
|
404 ||> (comment_isar_proof comment_of |
|
405 #> chain_isar_proof |
|
406 #> kill_useless_labels_in_isar_proof |
|
407 #> relabel_isar_proof_nicely |
|
408 #> rationalize_obtains_in_isar_proofs ctxt) |
|
409 in |
|
410 (case (num_chained, add_isar_steps (steps_of_isar_proof isar_proof) 0) of |
|
411 (0, 1) => |
|
412 one_line_proof_text ctxt 0 |
|
413 (if play_outcome_ord (play_outcome, one_line_play) = LESS then |
|
414 (case isar_proof of |
|
415 Proof (_, _, [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)]) => |
|
416 let |
|
417 val used_facts' = filter (fn (s, (sc, _)) => |
|
418 member (op =) gfs s andalso sc <> Chained) used_facts |
|
419 in |
|
420 ((used_facts', (meth, play_outcome)), banner, subgoal, subgoal_count) |
|
421 end) |
|
422 else |
|
423 one_line_params) ^ |
|
424 (if isar_proofs = SOME true then "\n(No Isar proof available.)" |
|
425 else "") |
|
426 | (_, num_steps) => |
|
427 let |
|
428 val msg = |
|
429 (if verbose then [string_of_int num_steps ^ " step" ^ plural_s num_steps] else []) @ |
|
430 (if do_preplay then [string_of_play_outcome play_outcome] else []) |
|
431 in |
|
432 one_line_proof_text ctxt 0 one_line_params ^ |
|
433 "\n\nIsar proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^ |
|
434 Active.sendback_markup [Markup.padding_command] |
|
435 (string_of_isar_proof ctxt subgoal subgoal_count isar_proof) |
|
436 end) |
|
437 end |
448 end |
438 in |
449 in |
439 if debug then |
450 if debug then |
440 generate_proof_text () |
451 generate_proof_text () |
441 else |
452 else |