1 (* Title: HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
2 Author: Jasmin Blanchette, TU Muenchen
3 Author: Steffen Juilf Smolka, TU Muenchen
5 Isar proof reconstruction from ATP proofs.
8 signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
10 type 'a proof = 'a ATP_Proof.proof
11 type stature = ATP_Problem_Generate.stature
13 datatype reconstructor =
14 Metis of string * string |
18 Played of reconstructor * Time.time |
19 Trust_Playable of reconstructor * Time.time option |
20 Failed_to_Play of reconstructor
22 type minimize_command = string list -> string
23 type one_line_params =
24 play * string * (string * stature) list * minimize_command * int * int
26 bool * bool * Time.time option * real * string Symtab.table
27 * (string * stature) list vector * int Symtab.table * string proof * thm
30 val string_for_reconstructor : reconstructor -> string
31 val lam_trans_from_atp_proof : string proof -> string -> string
32 val is_typed_helper_used_in_atp_proof : string proof -> bool
33 val used_facts_in_atp_proof :
34 Proof.context -> (string * stature) list vector -> string proof ->
35 (string * stature) list
36 val used_facts_in_unsound_atp_proof :
37 Proof.context -> (string * stature) list vector -> 'a proof ->
39 val one_line_proof_text : int -> one_line_params -> string
41 Proof.context -> bool option -> isar_params -> one_line_params -> string
43 Proof.context -> bool option -> isar_params -> int -> one_line_params
47 structure Sledgehammer_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
53 open ATP_Problem_Generate
54 open ATP_Proof_Reconstruct
55 open Sledgehammer_Util
56 open Sledgehammer_Proof
57 open Sledgehammer_Annotate
58 open Sledgehammer_Compress
60 structure String_Redirect = ATP_Proof_Redirect(
62 val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s')
68 (** reconstructors **)
70 datatype reconstructor =
71 Metis of string * string |
75 Played of reconstructor * Time.time |
76 Trust_Playable of reconstructor * Time.time option |
77 Failed_to_Play of reconstructor
81 fun string_for_reconstructor (Metis (type_enc, lam_trans)) =
82 metis_call type_enc lam_trans
83 | string_for_reconstructor SMT = smtN
86 (** fact extraction from ATP proofs **)
88 fun find_first_in_list_vector vec key =
89 Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
90 | (_, value) => value) NONE vec
92 val unprefix_fact_number = space_implode "_" o tl o space_explode "_"
94 fun resolve_one_named_fact fact_names s =
95 case try (unprefix fact_prefix) s of
97 let val s' = s' |> unprefix_fact_number |> unascii_of in
98 s' |> find_first_in_list_vector fact_names |> Option.map (pair s')
101 fun resolve_fact fact_names = map_filter (resolve_one_named_fact fact_names)
102 fun is_fact fact_names = not o null o resolve_fact fact_names
104 fun resolve_one_named_conjecture s =
105 case try (unprefix conjecture_prefix) s of
106 SOME s' => Int.fromString s'
109 val resolve_conjecture = map_filter resolve_one_named_conjecture
110 val is_conjecture = not o null o resolve_conjecture
112 val ascii_of_lam_fact_prefix = ascii_of lam_fact_prefix
114 (* overapproximation (good enough) *)
115 fun is_lam_lifted s =
116 String.isPrefix fact_prefix s andalso
117 String.isSubstring ascii_of_lam_fact_prefix s
119 val is_combinator_def = String.isPrefix (helper_prefix ^ combinator_prefix)
121 fun is_axiom_used_in_proof pred =
122 exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false)
124 fun lam_trans_from_atp_proof atp_proof default =
125 case (is_axiom_used_in_proof is_combinator_def atp_proof,
126 is_axiom_used_in_proof is_lam_lifted atp_proof) of
127 (false, false) => default
128 | (false, true) => liftingN
129 (* | (true, true) => combs_and_liftingN -- not supported by "metis" *)
130 | (true, _) => combsN
132 val is_typed_helper_name =
133 String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix
135 fun is_typed_helper_used_in_atp_proof atp_proof =
136 is_axiom_used_in_proof is_typed_helper_name atp_proof
138 fun add_non_rec_defs fact_names accum =
139 Vector.foldl (fn (facts, facts') =>
140 union (op =) (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts)
144 val isa_ext = Thm.get_name_hint @{thm ext}
145 val isa_short_ext = Long_Name.base_name isa_ext
148 if Thm.eq_thm_prop (@{thm ext},
149 singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then
154 val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg"
155 val leo2_unfold_def_rule = "unfold_def"
157 fun add_fact ctxt fact_names ((_, ss), _, _, rule, deps) =
158 (if rule = leo2_extcnf_equal_neg_rule then
159 insert (op =) (ext_name ctxt, (Global, General))
160 else if rule = leo2_unfold_def_rule then
161 (* LEO 1.3.3 does not record definitions properly, leading to missing
162 dependencies in the TSTP proof. Remove the next line once this is
164 add_non_rec_defs fact_names
165 else if rule = satallax_coreN then
167 (* Satallax doesn't include definitions in its unsatisfiable cores, so
168 we assume the worst and include them all here. *)
169 [(ext_name ctxt, (Global, General))] |> add_non_rec_defs fact_names
173 #> (if null deps then union (op =) (resolve_fact fact_names ss) else I)
175 fun used_facts_in_atp_proof ctxt fact_names atp_proof =
176 if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names
177 else fold (add_fact ctxt fact_names) atp_proof []
179 fun used_facts_in_unsound_atp_proof _ _ [] = NONE
180 | used_facts_in_unsound_atp_proof ctxt fact_names atp_proof =
181 let val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof in
182 if forall (fn (_, (sc, _)) => sc = Global) used_facts andalso
183 not (is_axiom_used_in_proof (is_conjecture o single) atp_proof) then
184 SOME (map fst used_facts)
190 (** one-liner reconstructor proofs **)
192 fun show_time NONE = ""
193 | show_time (SOME ext_time) = " (" ^ string_from_ext_time ext_time ^ ")"
195 (* FIXME: Various bugs, esp. with "unfolding"
196 fun unusing_chained_facts _ 0 = ""
197 | unusing_chained_facts used_chaineds num_chained =
198 if length used_chaineds = num_chained then ""
199 else if null used_chaineds then "(* using no facts *) "
200 else "(* using only " ^ space_implode " " used_chaineds ^ " *) "
203 fun apply_on_subgoal _ 1 = "by "
204 | apply_on_subgoal 1 _ = "apply "
205 | apply_on_subgoal i n =
206 "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
208 fun using_labels [] = ""
210 "using " ^ space_implode " " (map string_for_label ls) ^ " "
212 fun command_call name [] =
213 name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
214 | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
216 fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) =
217 (* unusing_chained_facts used_chaineds num_chained ^ *)
218 using_labels ls ^ apply_on_subgoal i n ^
219 command_call (string_for_reconstructor reconstr) ss
221 fun try_command_line banner time command =
222 banner ^ ": " ^ Active.sendback_markup command ^ show_time time ^ "."
224 fun minimize_line _ [] = ""
225 | minimize_line minimize_command ss =
226 case minimize_command ss of
229 "\nTo minimize: " ^ Active.sendback_markup command ^ "."
231 fun split_used_facts facts =
232 facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
233 |> pairself (sort_distinct (string_ord o pairself fst))
235 type minimize_command = string list -> string
236 type one_line_params =
237 play * string * (string * stature) list * minimize_command * int * int
239 fun one_line_proof_text num_chained
240 (preplay, banner, used_facts, minimize_command, subgoal,
243 val (chained, extra) = split_used_facts used_facts
244 val (failed, reconstr, ext_time) =
246 Played (reconstr, time) => (false, reconstr, (SOME (false, time)))
247 | Trust_Playable (reconstr, time) =>
252 if time = Time.zeroTime then NONE else SOME (true, time))
253 | Failed_to_Play reconstr => (true, reconstr, NONE)
256 |> reconstructor_command reconstr subgoal subgoal_count (map fst chained)
259 enclose "One-line proof reconstruction failed: "
260 ".\n(Invoking \"sledgehammer\" with \"[strict]\" might \
263 try_command_line banner ext_time)
264 in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end
267 (** Isar proof construction and manipulation **)
269 val assume_prefix = "a"
270 val have_prefix = "f"
273 fun raw_label_for_name (num, ss) =
274 case resolve_conjecture ss of
275 [j] => (conjecture_prefix, j)
276 | _ => (raw_prefix ^ ascii_of num, 0)
278 fun label_of_clause [name] = raw_label_for_name name
279 | label_of_clause c = (space_implode "___" (map (fst o raw_label_for_name) c), 0)
281 fun add_fact_from_dependencies fact_names (names as [(_, ss)]) =
282 if is_fact fact_names ss then
283 apsnd (union (op =) (map fst (resolve_fact fact_names ss)))
285 apfst (insert (op =) (label_of_clause names))
286 | add_fact_from_dependencies fact_names names =
287 apfst (insert (op =) (label_of_clause names))
289 fun repair_name "$true" = "c_True"
290 | repair_name "$false" = "c_False"
291 | repair_name "$$e" = tptp_equal (* seen in Vampire proofs *)
293 if is_tptp_equal s orelse
294 (* seen in Vampire proofs *)
295 (String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s) then
300 fun infer_formula_types ctxt =
301 Type.constraint HOLogic.boolT
303 (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
305 val combinator_table =
306 [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def [abs_def]}),
307 (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def [abs_def]}),
308 (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def [abs_def]}),
309 (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def [abs_def]}),
310 (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def [abs_def]})]
312 fun uncombine_term thy =
314 fun aux (t1 $ t2) = betapply (pairself aux (t1, t2))
315 | aux (Abs (s, T, t')) = Abs (s, T, aux t')
316 | aux (t as Const (x as (s, _))) =
317 (case AList.lookup (op =) combinator_table s of
318 SOME thm => thm |> prop_of |> specialize_type thy x
319 |> Logic.dest_equals |> snd
324 fun decode_line sym_tab (name, role, u, rule, deps) ctxt =
326 val thy = Proof_Context.theory_of ctxt
327 val t = u |> prop_from_atp ctxt true sym_tab
328 |> uncombine_term thy |> infer_formula_types ctxt
330 ((name, role, t, rule, deps),
331 fold Variable.declare_term (Misc_Legacy.term_frees t) ctxt)
333 fun decode_lines ctxt sym_tab lines =
334 fst (fold_map (decode_line sym_tab) lines ctxt)
336 fun replace_one_dependency (old, new) dep =
337 if is_same_atp_step dep old then new else [dep]
338 fun replace_dependencies_in_line p (name, role, t, rule, deps) =
339 (name, role, t, rule, fold (union (op =) o replace_one_dependency p) deps [])
341 (* No "real" literals means only type information (tfree_tcs, clsrel, or
343 fun is_only_type_information t = t aconv @{term True}
345 fun s_maybe_not role = role <> Conjecture ? s_not
347 fun is_same_inference (role, t) (_, role', t', _, _) =
348 s_maybe_not role t aconv s_maybe_not role' t'
350 (* Discard facts; consolidate adjacent lines that prove the same formula, since
351 they differ only in type information.*)
352 fun add_line fact_names (name as (_, ss), role, t, rule, []) lines =
353 (* No dependencies: fact, conjecture, or (for Vampire) internal facts or
355 if is_conjecture ss then
356 (name, role, t, rule, []) :: lines
357 else if is_fact fact_names ss then
358 (* Facts are not proof lines. *)
359 if is_only_type_information t then
360 map (replace_dependencies_in_line (name, [])) lines
364 map (replace_dependencies_in_line (name, [])) lines
365 | add_line _ (line as (name, role, t, _, _)) lines =
366 (* Type information will be deleted later; skip repetition test. *)
367 if is_only_type_information t then
369 (* Is there a repetition? If so, replace later line by earlier one. *)
370 else case take_prefix (not o is_same_inference (role, t)) lines of
371 (_, []) => line :: lines
372 | (pre, (name', _, _, _, _) :: post) =>
373 line :: pre @ map (replace_dependencies_in_line (name', [name])) post
375 val waldmeister_conjecture_num = "1.0.0.0"
377 val repair_waldmeister_endgame =
379 fun do_tail (name, _, t, rule, deps) =
380 (name, Negated_Conjecture, s_not t, rule, deps)
382 | do_body ((line as ((num, _), _, _, _, _)) :: lines) =
383 if num = waldmeister_conjecture_num then map do_tail (line :: lines)
384 else line :: do_body lines
387 (* Recursively delete empty lines (type information) from the proof. *)
388 fun add_nontrivial_line (line as (name, _, t, _, [])) lines =
389 if is_only_type_information t then delete_dependency name lines
391 | add_nontrivial_line line lines = line :: lines
392 and delete_dependency name lines =
393 fold_rev add_nontrivial_line
394 (map (replace_dependencies_in_line (name, [])) lines) []
396 (* ATPs sometimes reuse free variable names in the strangest ways. Removing
397 offending lines often does the trick. *)
398 fun is_bad_free frees (Free x) = not (member (op =) frees x)
399 | is_bad_free _ _ = false
401 val e_skolemize_rule = "skolemize"
402 val vampire_skolemisation_rule = "skolemisation"
404 val is_skolemize_rule =
405 member (op =) [e_skolemize_rule, vampire_skolemisation_rule]
407 fun add_desired_line fact_names frees (name as (_, ss), role, t, rule, deps)
410 if is_fact fact_names ss orelse
411 is_conjecture ss orelse
412 is_skolemize_rule rule orelse
413 (* the last line must be kept *)
415 (not (is_only_type_information t) andalso
416 null (Term.add_tvars t []) andalso
417 not (exists_subterm (is_bad_free frees) t) andalso
418 length deps >= 2 andalso
419 (* kill next to last line, which usually results in a trivial step *)
421 (name, role, t, rule, deps) :: lines (* keep line *)
423 map (replace_dependencies_in_line (name, deps)) lines) (* drop line *)
427 fun string_for_proof ctxt type_enc lam_trans i n proof =
429 val register_fixes = map Free #> fold Variable.auto_fixes
430 fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt)
431 fun of_indent ind = replicate_string (ind * indent_size) " "
432 fun of_moreover ind = of_indent ind ^ "moreover\n"
433 fun of_label l = if l = no_label then "" else string_for_label l ^ ": "
434 fun of_obtain qs nr =
435 (if nr>1 orelse (nr=1 andalso member (op=) qs Then)
437 else if nr=1 orelse member (op=) qs Then
440 fun of_show_have qs = if member (op=) qs Show then "show" else "have"
441 fun of_thus_hence qs = if member (op=) qs Show then "thus" else "hence"
443 if nr>1 orelse (nr=1 andalso member (op=) qs Then)
444 then "ultimately " ^ of_show_have qs
445 else if nr=1 orelse member (op=) qs Then
446 then of_thus_hence qs
448 fun add_term term (s, ctxt)=
449 (s ^ (annotate_types ctxt term
450 |> with_vanilla_print_mode (Syntax.string_of_term ctxt)
453 ctxt |> Variable.auto_fixes term)
454 val reconstr = Metis (type_enc, lam_trans)
455 fun of_metis ind options (ls, ss) =
456 "\n" ^ of_indent (ind + 1) ^ options ^
457 reconstructor_command reconstr 1 1 [] 0
458 (ls |> sort_distinct (prod_ord string_ord int_ord),
459 ss |> sort_distinct string_ord)
461 maybe_quote s ^ " :: " ^
462 maybe_quote (simplify_spaces (with_vanilla_print_mode
463 (Syntax.string_of_typ ctxt) T))
464 fun add_frees xs (s, ctxt) =
465 (s ^ space_implode " and " (map of_free xs), ctxt |> register_fixes xs)
467 | add_fix ind xs = add_suffix (of_indent ind ^ "fix ")
470 fun add_assm ind (l, t) =
471 add_suffix (of_indent ind ^ "assume " ^ of_label l)
474 fun add_assms ind assms = fold (add_assm ind) assms
475 fun add_step_post ind l t facts options =
476 add_suffix (of_label l)
478 #> add_suffix (of_metis ind options facts ^ "\n")
479 fun of_subproof ind ctxt proof =
482 val s = of_proof ind ctxt proof
486 replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
487 String.extract (s, ind * indent_size,
488 SOME (size s - ind * indent_size - 1)) ^
491 and of_subproofs _ _ _ [] = ""
492 | of_subproofs ind ctxt qs subproofs =
493 (if member (op=) qs Then then of_moreover ind else "") ^
494 space_implode (of_moreover ind) (map (of_subproof ind ctxt) subproofs)
495 and add_step_pre ind qs subproofs (s, ctxt) =
496 (s ^ of_subproofs ind ctxt qs subproofs ^ of_indent ind, ctxt)
497 and add_step ind (Let (t1, t2)) =
498 add_suffix (of_indent ind ^ "let ")
503 | add_step ind (Prove (qs, l, t, By_Metis (subproofs, facts))) =
504 add_step_pre ind qs subproofs
505 #> add_suffix (of_prove qs (length subproofs) ^ " ")
506 #> add_step_post ind l t facts ""
507 | add_step ind (Obtain (qs, Fix xs, l, t, By_Metis (subproofs, facts))) =
508 add_step_pre ind qs subproofs
509 #> add_suffix (of_obtain qs (length subproofs) ^ " ")
511 #> add_suffix " where "
512 (* The new skolemizer puts the arguments in the same order as the ATPs
513 (E and Vampire -- but see also "atp_proof_reconstruct.ML" regarding
515 #> add_step_post ind l t facts
516 (if exists (fn (_, T) => length (binder_types T) > 1) xs then
517 "using [[metis_new_skolem]] "
520 and add_steps ind = fold (add_step ind)
521 and of_proof ind ctxt (Proof (Fix xs, Assume assms, steps)) =
524 |> add_assms ind assms
525 |> add_steps ind steps
528 (* One-step proofs are pointless; better use the Metis one-liner
531 Proof (Fix [], Assume [], [Prove (_, _, _, By_Metis ([], _))]) => ""
532 | _ => (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
533 of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
534 of_indent 0 ^ (if n <> 1 then "next" else "qed")
537 fun add_labels_of_step step =
538 case byline_of_step step of
540 | SOME (By_Metis (subproofs, (ls, _))) =>
541 union (op =) ls #> fold add_labels_of_proof subproofs
542 and add_labels_of_proof proof = fold add_labels_of_step (steps_of_proof proof)
544 fun kill_useless_labels_in_proof proof =
546 val used_ls = add_labels_of_proof proof []
547 fun do_label l = if member (op =) used_ls l then l else no_label
548 fun do_assms (Assume assms) = Assume (map (apfst do_label) assms)
549 fun do_step (Obtain (qs, xs, l, t, By_Metis (subproofs, facts))) =
550 Obtain (qs, xs, do_label l, t, By_Metis (map do_proof subproofs, facts))
551 | do_step (Prove (qs, l, t, By_Metis (subproofs, facts))) =
552 Prove (qs, do_label l, t, By_Metis (map do_proof subproofs, facts))
553 | do_step step = step
554 and do_proof (Proof (fix, assms, steps)) =
555 Proof (fix, do_assms assms, map do_step steps)
556 in do_proof proof end
558 fun prefix_for_depth n = replicate_string (n + 1)
562 fun fresh_label depth prefix (old as (l, subst, next)) =
566 let val l' = (prefix_for_depth depth prefix, next) in
567 (l', (l, l') :: subst, next + 1)
570 apfst (maps (the_list o AList.lookup (op =) subst))
571 fun do_assm depth (l, t) (subst, next) =
573 val (l, subst, next) =
574 (l, subst, next) |> fresh_label depth assume_prefix
576 ((l, t), (subst, next))
578 fun do_assms subst depth (Assume assms) =
579 fold_map (do_assm depth) assms (subst, 1)
582 fun do_steps _ _ _ [] = []
583 | do_steps subst depth next (Obtain (qs, xs, l, t, by) :: steps) =
585 val (l, subst, next) =
586 (l, subst, next) |> fresh_label depth have_prefix
587 val by = by |> do_byline subst depth
588 in Obtain (qs, xs, l, t, by) :: do_steps subst depth next steps end
589 | do_steps subst depth next (Prove (qs, l, t, by) :: steps) =
591 val (l, subst, next) =
592 (l, subst, next) |> fresh_label depth have_prefix
593 val by = by |> do_byline subst depth
594 in Prove (qs, l, t, by) :: do_steps subst depth next steps end
595 | do_steps subst depth next (step :: steps) =
596 step :: do_steps subst depth next steps
597 and do_proof subst depth (Proof (fix, assms, steps)) =
598 let val (assms, subst) = do_assms subst depth assms in
599 Proof (fix, assms, do_steps subst depth 1 steps)
601 and do_byline subst depth (By_Metis (subproofs, facts)) =
602 By_Metis (do_proofs subst depth subproofs, do_facts subst facts)
603 and do_proofs subst depth = map (do_proof subst (depth + 1))
606 val chain_direct_proof =
608 fun do_qs_lfs NONE lfs = ([], lfs)
609 | do_qs_lfs (SOME l0) lfs =
610 if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0)
612 fun chain_step lbl (Obtain (qs, xs, l, t,
613 By_Metis (subproofs, (lfs, gfs)))) =
614 let val (qs', lfs) = do_qs_lfs lbl lfs in
615 Obtain (qs' @ qs, xs, l, t,
616 By_Metis (chain_proofs subproofs, (lfs, gfs)))
618 | chain_step lbl (Prove (qs, l, t, By_Metis (subproofs, (lfs, gfs)))) =
619 let val (qs', lfs) = do_qs_lfs lbl lfs in
620 Prove (qs' @ qs, l, t, By_Metis (chain_proofs subproofs, (lfs, gfs)))
622 | chain_step _ step = step
623 and chain_steps _ [] = []
624 | chain_steps (prev as SOME _) (i :: is) =
625 chain_step prev i :: chain_steps (label_of_step i) is
626 | chain_steps _ (i :: is) = i :: chain_steps (label_of_step i) is
627 and chain_proof (Proof (fix, Assume assms, steps)) =
628 Proof (fix, Assume assms,
629 chain_steps (try (List.last #> fst) assms) steps)
630 and chain_proofs proofs = map (chain_proof) proofs
634 bool * bool * Time.time option * real * string Symtab.table
635 * (string * stature) list vector * int Symtab.table * string proof * thm
637 fun isar_proof_text ctxt isar_proofs
638 (debug, verbose, preplay_timeout, isar_compress, pool, fact_names, sym_tab,
640 (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
642 val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
643 val frees = fold Term.add_frees (concl_t :: hyp_ts) []
644 val one_line_proof = one_line_proof_text 0 one_line_params
646 if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
648 val lam_trans = lam_trans_from_atp_proof atp_proof metis_default_lam_trans
649 val preplay = preplay_timeout <> SOME Time.zeroTime
651 fun isar_proof_of () =
655 |> clean_up_atp_proof_dependencies
656 |> nasty_atp_proof pool
657 |> map_term_names_in_atp_proof repair_name
658 |> decode_lines ctxt sym_tab
659 |> repair_waldmeister_endgame
660 |> rpair [] |-> fold_rev (add_line fact_names)
661 |> rpair [] |-> fold_rev add_nontrivial_line
663 |-> fold_rev (add_desired_line fact_names frees)
665 val conj_name = conjecture_prefix ^ string_of_int (length hyp_ts)
667 atp_proof |> map_filter
668 (fn (name as (_, ss), _, _, _, []) =>
669 if member (op =) ss conj_name then SOME name else NONE
672 atp_proof |> map_filter
673 (fn (name as (_, ss), _, _, _, []) =>
674 (case resolve_conjecture ss of
676 if j = length hyp_ts then NONE
677 else SOME (raw_label_for_name name, nth hyp_ts j)
680 val bot = atp_proof |> List.last |> #1
683 |> map (fn (name, _, _, _, from) => (from, name))
684 |> make_refute_graph bot
685 |> fold (Atom_Graph.default_node o rpair ()) conjs
686 val axioms = axioms_of_refute_graph refute_graph conjs
687 val tainted = tainted_atoms_of_refute_graph refute_graph conjs
688 val is_clause_tainted = exists (member (op =) tainted)
691 |> fold (fn (name as (s, _), role, t, rule, _) =>
692 Symtab.update_new (s, (rule,
693 t |> (if is_clause_tainted [name] then
695 #> fold exists_of (map Var (Term.add_vars t []))
699 fun is_clause_skolemize_rule [(s, _)] =
700 Option.map (is_skolemize_rule o fst) (Symtab.lookup steps s) =
702 | is_clause_skolemize_rule _ = false
703 (* The assumptions and conjecture are "prop"s; the other formulas are
705 fun prop_of_clause [(s, ss)] =
706 (case resolve_conjecture ss of
707 [j] => if j = length hyp_ts then concl_t else nth hyp_ts j
708 | _ => the_default ("", @{term False}) (Symtab.lookup steps s)
709 |> snd |> HOLogic.mk_Trueprop |> close_form)
710 | prop_of_clause names =
712 val lits = map snd (map_filter (Symtab.lookup steps o fst) names)
714 case List.partition (can HOLogic.dest_not) lits of
715 (negs as _ :: _, pos as _ :: _) =>
716 s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs),
717 Library.foldr1 s_disj pos)
718 | _ => fold (curry s_disj) lits @{term False}
720 |> HOLogic.mk_Trueprop |> close_form
721 fun isar_proof_of_direct_proof infs =
723 fun maybe_show outer c =
724 (outer andalso length c = 1 andalso subset (op =) (c, conjs))
726 val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
728 Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
729 fun do_steps _ _ accum [] = rev accum
730 | do_steps outer _ accum (Have (gamma, c) :: infs) =
732 val l = label_of_clause c
733 val t = prop_of_clause c
736 (fold (add_fact_from_dependencies fact_names)
738 fun prove by = Prove (maybe_show outer c [], l, t, by)
739 fun do_rest lbl step =
740 do_steps outer (SOME lbl) (step :: accum) infs
742 if is_clause_tainted c then
745 if is_clause_skolemize_rule g andalso
746 is_clause_tainted g then
749 Proof (Fix (skolems_of (prop_of_clause g)),
750 Assume [], rev accum)
752 do_steps outer (SOME l)
753 [prove (By_Metis ([subproof], no_facts))] []
757 | _ => do_rest l (prove by)
759 if is_clause_skolemize_rule c then
760 do_rest l (Obtain ([], Fix (skolems_of t), l, t, by))
764 | do_steps outer predecessor accum (Cases cases :: infs) =
766 fun do_case (c, infs) =
767 do_proof false [] [(label_of_clause c, prop_of_clause c)] infs
768 val c = succedent_of_cases cases
769 val l = label_of_clause c
770 val t = prop_of_clause c
772 (Prove (maybe_show outer c [], l, t, By_Metis
773 (map do_case cases, (the_list predecessor, []))))
775 do_steps outer (SOME l) (step :: accum) infs
777 and do_proof outer fix assms infs =
778 Proof (Fix fix, Assume assms, do_steps outer NONE [] infs)
780 do_proof true params assms infs
783 val cleanup_labels_in_proof =
785 #> kill_useless_labels_in_proof
787 val (isar_proof, (preplay_fail, preplay_time)) =
789 |> redirect_graph axioms tainted bot
790 |> isar_proof_of_direct_proof
791 |> (if not preplay andalso isar_compress <= 1.0 then
792 rpair (false, (true, seconds 0.0))
794 compress_proof debug ctxt type_enc lam_trans preplay
796 (if isar_proofs = SOME true then isar_compress else 1000.0))
797 |>> cleanup_labels_in_proof
799 string_for_proof ctxt type_enc lam_trans subgoal subgoal_count
804 if isar_proofs = SOME true then
805 "\nNo structured proof available (proof too simple)."
813 val num_steps = add_metis_steps (steps_of_proof isar_proof) 0
814 in [string_of_int num_steps ^ " step" ^ plural_s num_steps] end
818 [(if preplay_fail then "may fail, " else "") ^
819 Sledgehammer_Preplay.string_of_preplay_time preplay_time]
823 "\n\nStructured proof "
824 ^ (commas msg |> not (null msg) ? enclose "(" ")")
825 ^ ":\n" ^ Active.sendback_markup isar_text
831 else case try isar_proof_of () of
833 | NONE => if isar_proofs = SOME true then
834 "\nWarning: The Isar proof construction failed."
837 in one_line_proof ^ isar_proof end
839 fun isar_proof_would_be_a_good_idea preplay =
841 Played (reconstr, _) => reconstr = SMT
842 | Trust_Playable _ => true
843 | Failed_to_Play _ => true
845 fun proof_text ctxt isar_proofs isar_params num_chained
846 (one_line_params as (preplay, _, _, _, _, _)) =
847 (if isar_proofs = SOME true orelse
848 (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then
849 isar_proof_text ctxt isar_proofs isar_params
851 one_line_proof_text num_chained) one_line_params