1 (* Title: HOL/Tools/ATP/atp_reconstruct.ML
2 Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
3 Author: Claire Quigley, Cambridge University Computer Laboratory
4 Author: Jasmin Blanchette, TU Muenchen
6 Proof reconstruction from ATP proofs.
9 signature ATP_RECONSTRUCT =
11 type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
12 type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
13 type 'a proof = 'a ATP_Proof.proof
14 type locality = ATP_Translate.locality
16 datatype reconstructor =
17 Metis of string * string |
21 Played of reconstructor * Time.time |
22 Trust_Playable of reconstructor * Time.time option |
23 Failed_to_Play of reconstructor
25 type minimize_command = string list -> string
26 type one_line_params =
27 play * string * (string * locality) list * minimize_command * int * int
29 bool * bool * int * string Symtab.table * int list list * int
30 * (string * locality) list vector * int Symtab.table * string proof * thm
34 val full_typesN : string
35 val partial_typesN : string
36 val no_typesN : string
37 val really_full_type_enc : string
38 val full_type_enc : string
39 val partial_type_enc : string
40 val no_type_enc : string
41 val full_type_encs : string list
42 val partial_type_encs : string list
43 val used_facts_in_atp_proof :
44 Proof.context -> int -> (string * locality) list vector -> string proof
45 -> (string * locality) list
46 val used_facts_in_unsound_atp_proof :
47 Proof.context -> int list list -> int -> (string * locality) list vector
48 -> 'a proof -> string list option
49 val uses_typed_helpers : int list -> 'a proof -> bool
50 val unalias_type_enc : string -> string list
51 val metis_default_lam_trans : string
52 val metis_call : string -> string -> string
53 val name_of_reconstructor : reconstructor -> string
54 val one_line_proof_text : one_line_params -> string
55 val make_tvar : string -> typ
56 val make_tfree : Proof.context -> string -> typ
58 Proof.context -> bool -> int Symtab.table -> typ option
59 -> (string, string) ho_term -> term
61 Proof.context -> bool -> int Symtab.table
62 -> (string, string, (string, string) ho_term) formula -> term
64 Proof.context -> bool -> isar_params -> one_line_params -> string
66 Proof.context -> bool -> isar_params -> one_line_params -> string
69 structure ATP_Reconstruct : ATP_RECONSTRUCT =
77 datatype reconstructor =
78 Metis of string * string |
82 Played of reconstructor * Time.time |
83 Trust_Playable of reconstructor * Time.time option |
84 Failed_to_Play of reconstructor
86 type minimize_command = string list -> string
87 type one_line_params =
88 play * string * (string * locality) list * minimize_command * int * int
90 bool * bool * int * string Symtab.table * int list list * int
91 * (string * locality) list vector * int Symtab.table * string proof * thm
93 val is_typed_helper_name =
94 String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix
96 fun find_first_in_list_vector vec key =
97 Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
98 | (_, value) => value) NONE vec
100 val unprefix_fact_number = space_implode "_" o tl o space_explode "_"
102 val vampire_step_prefix = "f" (* grrr... *)
104 val extract_step_number =
105 Int.fromString o perhaps (try (unprefix vampire_step_prefix))
107 fun resolve_one_named_fact fact_names s =
108 case try (unprefix fact_prefix) s of
110 let val s' = s' |> unprefix_fact_number |> unascii_of in
111 s' |> find_first_in_list_vector fact_names |> Option.map (pair s')
114 fun resolve_fact _ fact_names (_, SOME ss) =
115 map_filter (resolve_one_named_fact fact_names) ss
116 | resolve_fact facts_offset fact_names (num, NONE) =
117 (case extract_step_number num of
119 let val j = j - facts_offset in
120 if j > 0 andalso j <= Vector.length fact_names then
121 Vector.sub (fact_names, j - 1)
127 fun is_fact conjecture_shape = not o null o resolve_fact 0 conjecture_shape
129 fun resolve_one_named_conjecture s =
130 case try (unprefix conjecture_prefix) s of
131 SOME s' => Int.fromString s'
134 fun resolve_conjecture _ (_, SOME ss) =
135 map_filter resolve_one_named_conjecture ss
136 | resolve_conjecture conjecture_shape (num, NONE) =
137 case extract_step_number num of
138 SOME i => (case find_index (exists (curry (op =) i)) conjecture_shape of
143 fun is_conjecture conjecture_shape =
144 not o null o resolve_conjecture conjecture_shape
146 fun is_typed_helper _ (_, SOME ss) = exists is_typed_helper_name ss
147 | is_typed_helper typed_helpers (num, NONE) =
148 (case extract_step_number num of
149 SOME i => member (op =) typed_helpers i
152 val leo2_ext = "extcnf_equal_neg"
153 val isa_ext = Thm.get_name_hint @{thm ext}
154 val isa_short_ext = Long_Name.base_name isa_ext
157 if Thm.eq_thm_prop (@{thm ext},
158 singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then
163 fun add_fact _ facts_offset fact_names (Inference (name, _, _, [])) =
164 union (op =) (resolve_fact facts_offset fact_names name)
165 | add_fact ctxt _ _ (Inference (_, _, rule, _)) =
166 if rule = leo2_ext then insert (op =) (ext_name ctxt, General) else I
167 | add_fact _ _ _ _ = I
169 fun used_facts_in_atp_proof ctxt facts_offset fact_names atp_proof =
170 if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names
171 else fold (add_fact ctxt facts_offset fact_names) atp_proof []
173 fun is_conjecture_used_in_proof conjecture_shape =
174 exists (fn Inference (name, _, _, []) => is_conjecture conjecture_shape name
177 (* (quasi-)underapproximation of the truth *)
178 fun is_locality_global Local = false
179 | is_locality_global Assum = false
180 | is_locality_global Chained = false
181 | is_locality_global _ = true
183 fun used_facts_in_unsound_atp_proof _ _ _ _ [] = NONE
184 | used_facts_in_unsound_atp_proof ctxt conjecture_shape facts_offset
185 fact_names atp_proof =
188 used_facts_in_atp_proof ctxt facts_offset fact_names atp_proof
190 if forall (is_locality_global o snd) used_facts andalso
191 not (is_conjecture_used_in_proof conjecture_shape atp_proof) then
192 SOME (map fst used_facts)
197 fun uses_typed_helpers typed_helpers =
198 exists (fn Inference (name, _, _, []) => is_typed_helper typed_helpers name
202 (** Soft-core proof reconstruction: one-liners **)
207 val full_typesN = "full_types"
208 val partial_typesN = "partial_types"
209 val no_typesN = "no_types"
211 val really_full_type_enc = "mono_tags"
212 val full_type_enc = "poly_guards_query"
213 val partial_type_enc = "poly_args"
214 val no_type_enc = "erased"
216 val full_type_encs = [full_type_enc, really_full_type_enc]
217 val partial_type_encs = partial_type_enc :: full_type_encs
219 val type_enc_aliases =
220 [(full_typesN, full_type_encs),
221 (partial_typesN, partial_type_encs),
222 (no_typesN, [no_type_enc])]
224 fun unalias_type_enc s =
225 AList.lookup (op =) type_enc_aliases s |> the_default [s]
227 val metis_default_lam_trans = combinatorsN
229 fun metis_call type_enc lam_trans =
232 case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases
236 val opts = [] |> type_enc <> partial_typesN ? cons type_enc
237 |> lam_trans <> metis_default_lam_trans ? cons lam_trans
238 in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end
240 (* unfortunate leaking abstraction *)
241 fun name_of_reconstructor (Metis (type_enc, lam_trans)) =
242 metis_call type_enc lam_trans
243 | name_of_reconstructor SMT = smtN
245 fun string_for_label (s, num) = s ^ string_of_int num
247 fun show_time NONE = ""
248 | show_time (SOME ext_time) = " (" ^ string_from_ext_time ext_time ^ ")"
250 fun apply_on_subgoal _ 1 = "by "
251 | apply_on_subgoal 1 _ = "apply "
252 | apply_on_subgoal i n =
253 "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
254 fun command_call name [] =
255 name |> not (Lexicon.is_identifier name) ? enclose "(" ")"
256 | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
257 fun try_command_line banner time command =
258 banner ^ ": " ^ Markup.markup Markup.sendback command ^ show_time time ^ "."
259 fun using_labels [] = ""
261 "using " ^ space_implode " " (map string_for_label ls) ^ " "
262 fun reconstructor_command reconstr i n (ls, ss) =
263 using_labels ls ^ apply_on_subgoal i n ^
264 command_call (name_of_reconstructor reconstr) ss
265 fun minimize_line _ [] = ""
266 | minimize_line minimize_command ss =
267 case minimize_command ss of
269 | command => "\nTo minimize: " ^ Markup.markup Markup.sendback command ^ "."
271 val split_used_facts =
272 List.partition (curry (op =) Chained o snd)
273 #> pairself (sort_distinct (string_ord o pairself fst))
275 fun one_line_proof_text (preplay, banner, used_facts, minimize_command,
276 subgoal, subgoal_count) =
278 val (chained, extra) = split_used_facts used_facts
279 val (failed, reconstr, ext_time) =
281 Played (reconstr, time) => (false, reconstr, (SOME (false, time)))
282 | Trust_Playable (reconstr, time) =>
287 if time = Time.zeroTime then NONE else SOME (true, time))
288 | Failed_to_Play reconstr => (true, reconstr, NONE)
291 |> reconstructor_command reconstr subgoal subgoal_count
292 |> (if failed then enclose "One-line proof reconstruction failed: " "."
293 else try_command_line banner ext_time)
294 in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end
296 (** Hard-core proof reconstruction: structured Isar proofs **)
298 fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t
299 fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t
301 fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
302 fun make_tfree ctxt w =
303 let val ww = "'" ^ w in
304 TFree (ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1)))
308 val no_label = ("", ~1)
311 val assum_prefix = "A"
312 val have_prefix = "F"
314 fun raw_label_for_name conjecture_shape name =
315 case resolve_conjecture conjecture_shape name of
316 [j] => (conjecture_prefix, j)
317 | _ => case Int.fromString (fst name) of
318 SOME j => (raw_prefix, j)
319 | NONE => (raw_prefix ^ fst name, 0)
321 (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
323 exception HO_TERM of (string, string) ho_term list
324 exception FORMULA of (string, string, (string, string) ho_term) formula list
325 exception SAME of unit
327 (* Type variables are given the basic sort "HOL.type". Some will later be
328 constrained by information from type literals, or by type inference. *)
329 fun typ_from_atp ctxt (u as ATerm (a, us)) =
330 let val Ts = map (typ_from_atp ctxt) us in
331 case unprefix_and_unascii type_const_prefix a of
332 SOME b => Type (invert_const b, Ts)
334 if not (null us) then
335 raise HO_TERM [u] (* only "tconst"s have type arguments *)
336 else case unprefix_and_unascii tfree_prefix a of
337 SOME b => make_tfree ctxt b
339 (* Could be an Isabelle variable or a variable from the ATP, say "X1"
340 or "_5018". Sometimes variables from the ATP are indistinguishable
341 from Isabelle variables, which forces us to use a type parameter in
343 (a |> perhaps (unprefix_and_unascii tvar_prefix), HOLogic.typeS)
344 |> Type_Infer.param 0
347 (* Type class literal applied to a type. Returns triple of polarity, class,
349 fun type_constraint_from_term ctxt (u as ATerm (a, us)) =
350 case (unprefix_and_unascii class_prefix a, map (typ_from_atp ctxt) us) of
351 (SOME b, [T]) => (b, T)
352 | _ => raise HO_TERM [u]
354 (* Accumulate type constraints in a formula: negative type literals. *)
355 fun add_var (key, z) = Vartab.map_default (key, []) (cons z)
356 fun add_type_constraint false (cl, TFree (a ,_)) = add_var ((a, ~1), cl)
357 | add_type_constraint false (cl, TVar (ix, _)) = add_var (ix, cl)
358 | add_type_constraint _ _ = I
360 fun repair_variable_name f s =
362 fun subscript_name s n = s ^ nat_subscript n
363 val s = String.map f s
365 case space_explode "_" s of
366 [_] => (case take_suffix Char.isDigit (String.explode s) of
367 (cs1 as _ :: _, cs2 as _ :: _) =>
368 subscript_name (String.implode cs1)
369 (the (Int.fromString (String.implode cs2)))
371 | [s1, s2] => (case Int.fromString s2 of
372 SOME n => subscript_name s1 n
377 (* The number of type arguments of a constant, zero if it's monomorphic. For
378 (instances of) Skolem pseudoconstants, this information is encoded in the
380 fun num_type_args thy s =
381 if String.isPrefix skolem_const_prefix s then
382 s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
383 else if String.isPrefix lambda_lifted_prefix s then
384 if String.isPrefix lambda_lifted_poly_prefix s then 2 else 0
386 (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
388 fun slack_fastype_of t = fastype_of t handle TERM _ => HOLogic.typeT
390 (* First-order translation. No types are known for variables. "HOLogic.typeT"
391 should allow them to be inferred. *)
392 fun term_from_atp ctxt textual sym_tab =
394 val thy = Proof_Context.theory_of ctxt
395 (* For Metis, we use 1 rather than 0 because variable references in clauses
396 may otherwise conflict with variable constraints in the goal. At least,
397 type inference often fails otherwise. See also "axiom_inference" in
398 "Metis_Reconstruct". *)
399 val var_index = if textual then 0 else 1
400 fun do_term extra_ts opt_T u =
403 if String.isPrefix simple_type_prefix s then
404 @{const True} (* ignore TPTP type information *)
405 else if s = tptp_equal then
406 let val ts = map (do_term [] NONE) us in
407 if textual andalso length ts = 2 andalso
408 hd ts aconv List.last ts then
409 (* Vampire is keen on producing these. *)
412 list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
414 else case unprefix_and_unascii const_prefix s of
417 val ((s', s''), mangled_us) =
418 s' |> unmangled_const |>> `invert_const
420 if s' = type_tag_name then
421 case mangled_us @ us of
423 do_term extra_ts (SOME (typ_from_atp ctxt typ_u)) term_u
424 | _ => raise HO_TERM us
425 else if s' = predicator_name then
426 do_term [] (SOME @{typ bool}) (hd us)
427 else if s' = app_op_name then
428 let val extra_t = do_term [] NONE (List.last us) in
429 do_term (extra_t :: extra_ts)
431 SOME T => SOME (slack_fastype_of extra_t --> T)
433 (nth us (length us - 2))
435 else if s' = type_guard_name then
436 @{const True} (* ignore type predicates *)
439 val new_skolem = String.isPrefix new_skolem_const_prefix s''
441 length us - the_default 0 (Symtab.lookup sym_tab s)
442 val (type_us, term_us) =
443 chop num_ty_args us |>> append mangled_us
444 val term_ts = map (do_term [] NONE) term_us
446 (if not (null type_us) andalso
447 num_type_args thy s' = length type_us then
448 let val Ts = type_us |> map (typ_from_atp ctxt) in
450 SOME (Type_Infer.paramify_vars (tl Ts ---> hd Ts))
452 try (Sign.const_instance thy) (s', Ts)
459 | NONE => map slack_fastype_of term_ts --->
462 | NONE => HOLogic.typeT))
465 Var ((new_skolem_var_name_from_const s'', var_index), T)
467 Const (unproxify_const s', T)
468 in list_comb (t, term_ts @ extra_ts) end
470 | NONE => (* a free or schematic variable *)
472 val term_ts = map (do_term [] NONE) us
473 val ts = term_ts @ extra_ts
476 SOME T => map slack_fastype_of term_ts ---> T
477 | NONE => map slack_fastype_of ts ---> HOLogic.typeT
479 case unprefix_and_unascii fixed_var_prefix s of
480 SOME s => Free (s, T)
482 case unprefix_and_unascii schematic_var_prefix s of
483 SOME s => Var ((s, var_index), T)
485 Var ((s |> textual ? repair_variable_name Char.toLower,
487 in list_comb (t, ts) end
490 fun term_from_atom ctxt textual sym_tab pos (u as ATerm (s, _)) =
491 if String.isPrefix class_prefix s then
492 add_type_constraint pos (type_constraint_from_term ctxt u)
493 #> pair @{const True}
495 pair (term_from_atp ctxt textual sym_tab (SOME @{typ bool}) u)
497 val combinator_table =
498 [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}),
499 (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def_raw}),
500 (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def_raw}),
501 (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}),
502 (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def_raw})]
504 fun uncombine_term thy =
506 fun aux (t1 $ t2) = betapply (pairself aux (t1, t2))
507 | aux (Abs (s, T, t')) = Abs (s, T, aux t')
508 | aux (t as Const (x as (s, _))) =
509 (case AList.lookup (op =) combinator_table s of
510 SOME thm => thm |> prop_of |> specialize_type thy x
511 |> Logic.dest_equals |> snd
516 (* Update schematic type variables with detected sort constraints. It's not
517 totally clear whether this code is necessary. *)
518 fun repair_tvar_sorts (t, tvar_tab) =
520 fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
521 | do_type (TVar (xi, s)) =
522 TVar (xi, the_default s (Vartab.lookup tvar_tab xi))
523 | do_type (TFree z) = TFree z
524 fun do_term (Const (a, T)) = Const (a, do_type T)
525 | do_term (Free (a, T)) = Free (a, do_type T)
526 | do_term (Var (xi, T)) = Var (xi, do_type T)
527 | do_term (t as Bound _) = t
528 | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t)
529 | do_term (t1 $ t2) = do_term t1 $ do_term t2
530 in t |> not (Vartab.is_empty tvar_tab) ? do_term end
532 fun quantify_over_var quant_of var_s t =
534 val vars = [] |> Term.add_vars t |> filter (fn ((s, _), _) => s = var_s)
536 in fold_rev quant_of vars t end
538 (* Interpret an ATP formula as a HOL term, extracting sort constraints as they
539 appear in the formula. *)
540 fun prop_from_atp ctxt textual sym_tab phi =
542 fun do_formula pos phi =
544 AQuant (_, [], phi) => do_formula pos phi
545 | AQuant (q, (s, _) :: xs, phi') =>
546 do_formula pos (AQuant (q, xs, phi'))
548 #>> quantify_over_var (case q of
550 | AExists => exists_of)
551 (s |> textual ? repair_variable_name Char.toLower)
552 | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
553 | AConn (c, [phi1, phi2]) =>
554 do_formula (pos |> c = AImplies ? not) phi1
555 ##>> do_formula pos phi2
561 | ANot => raise Fail "impossible connective")
562 | AAtom tm => term_from_atom ctxt textual sym_tab pos tm
563 | _ => raise FORMULA [phi]
564 in repair_tvar_sorts (do_formula true phi Vartab.empty) end
566 fun infer_formula_types ctxt =
567 Type.constraint HOLogic.boolT
569 (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
571 fun uncombined_etc_prop_from_atp ctxt textual sym_tab =
572 let val thy = Proof_Context.theory_of ctxt in
573 prop_from_atp ctxt textual sym_tab
574 #> textual ? uncombine_term thy #> infer_formula_types ctxt
577 (**** Translation of TSTP files to Isar proofs ****)
579 fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
580 | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
582 fun decode_line sym_tab (Definition (name, phi1, phi2)) ctxt =
584 val thy = Proof_Context.theory_of ctxt
585 val t1 = prop_from_atp ctxt true sym_tab phi1
586 val vars = snd (strip_comb t1)
587 val frees = map unvarify_term vars
588 val unvarify_args = subst_atomic (vars ~~ frees)
589 val t2 = prop_from_atp ctxt true sym_tab phi2
591 HOLogic.eq_const HOLogic.typeT $ t1 $ t2
592 |> unvarify_args |> uncombine_term thy |> infer_formula_types ctxt
595 (Definition (name, t1, t2),
596 fold Variable.declare_term (maps Misc_Legacy.term_frees [t1, t2]) ctxt)
598 | decode_line sym_tab (Inference (name, u, rule, deps)) ctxt =
599 let val t = u |> uncombined_etc_prop_from_atp ctxt true sym_tab in
600 (Inference (name, t, rule, deps),
601 fold Variable.declare_term (Misc_Legacy.term_frees t) ctxt)
603 fun decode_lines ctxt sym_tab lines =
604 fst (fold_map (decode_line sym_tab) lines ctxt)
606 fun is_same_inference _ (Definition _) = false
607 | is_same_inference t (Inference (_, t', _, _)) = t aconv t'
609 (* No "real" literals means only type information (tfree_tcs, clsrel, or
611 val is_only_type_information = curry (op aconv) HOLogic.true_const
613 fun replace_one_dependency (old, new) dep =
614 if is_same_atp_step dep old then new else [dep]
615 fun replace_dependencies_in_line _ (line as Definition _) = line
616 | replace_dependencies_in_line p (Inference (name, t, rule, deps)) =
617 Inference (name, t, rule,
618 fold (union (op =) o replace_one_dependency p) deps [])
620 (* Discard facts; consolidate adjacent lines that prove the same formula, since
621 they differ only in type information.*)
622 fun add_line _ _ (line as Definition _) lines = line :: lines
623 | add_line conjecture_shape fact_names (Inference (name, t, rule, [])) lines =
624 (* No dependencies: fact, conjecture, or (for Vampire) internal facts or
626 if is_fact fact_names name then
627 (* Facts are not proof lines. *)
628 if is_only_type_information t then
629 map (replace_dependencies_in_line (name, [])) lines
630 (* Is there a repetition? If so, replace later line by earlier one. *)
631 else case take_prefix (not o is_same_inference t) lines of
632 (_, []) => lines (* no repetition of proof line *)
633 | (pre, Inference (name', _, _, _) :: post) =>
634 pre @ map (replace_dependencies_in_line (name', [name])) post
635 | _ => raise Fail "unexpected inference"
636 else if is_conjecture conjecture_shape name then
637 Inference (name, s_not t, rule, []) :: lines
639 map (replace_dependencies_in_line (name, [])) lines
640 | add_line _ _ (Inference (name, t, rule, deps)) lines =
641 (* Type information will be deleted later; skip repetition test. *)
642 if is_only_type_information t then
643 Inference (name, t, rule, deps) :: lines
644 (* Is there a repetition? If so, replace later line by earlier one. *)
645 else case take_prefix (not o is_same_inference t) lines of
646 (* FIXME: Doesn't this code risk conflating proofs involving different
648 (_, []) => Inference (name, t, rule, deps) :: lines
649 | (pre, Inference (name', t', rule, _) :: post) =>
650 Inference (name, t', rule, deps) ::
651 pre @ map (replace_dependencies_in_line (name', [name])) post
652 | _ => raise Fail "unexpected inference"
654 (* Recursively delete empty lines (type information) from the proof. *)
655 fun add_nontrivial_line (line as Inference (name, t, _, [])) lines =
656 if is_only_type_information t then delete_dependency name lines
658 | add_nontrivial_line line lines = line :: lines
659 and delete_dependency name lines =
660 fold_rev add_nontrivial_line
661 (map (replace_dependencies_in_line (name, [])) lines) []
663 (* ATPs sometimes reuse free variable names in the strangest ways. Removing
664 offending lines often does the trick. *)
665 fun is_bad_free frees (Free x) = not (member (op =) frees x)
666 | is_bad_free _ _ = false
668 fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) =
669 (j, line :: map (replace_dependencies_in_line (name, [])) lines)
670 | add_desired_line isar_shrink_factor conjecture_shape fact_names frees
671 (Inference (name, t, rule, deps)) (j, lines) =
673 if is_fact fact_names name orelse
674 is_conjecture conjecture_shape name orelse
675 (* the last line must be kept *)
677 (not (is_only_type_information t) andalso
678 null (Term.add_tvars t []) andalso
679 not (exists_subterm (is_bad_free frees) t) andalso
680 length deps >= 2 andalso j mod isar_shrink_factor = 0 andalso
681 (* kill next to last line, which usually results in a trivial step *)
683 Inference (name, t, rule, deps) :: lines (* keep line *)
685 map (replace_dependencies_in_line (name, deps)) lines) (* drop line *)
687 (** Isar proof construction and manipulation **)
689 fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
690 (union (op =) ls1 ls2, union (op =) ss1 ss2)
692 type label = string * int
693 type facts = label list * string list
695 datatype isar_qualifier = Show | Then | Moreover | Ultimately
698 Fix of (string * typ) list |
700 Assume of label * term |
701 Have of isar_qualifier list * label * term * byline
704 CaseSplit of isar_step list list * facts
706 fun smart_case_split [] facts = ByMetis facts
707 | smart_case_split proofs facts = CaseSplit (proofs, facts)
709 fun add_fact_from_dependency conjecture_shape facts_offset fact_names name =
710 if is_fact fact_names name then
711 apsnd (union (op =) (map fst (resolve_fact facts_offset fact_names name)))
713 apfst (insert (op =) (raw_label_for_name conjecture_shape name))
715 fun step_for_line _ _ _ _ (Definition (_, t1, t2)) = Let (t1, t2)
716 | step_for_line conjecture_shape _ _ _ (Inference (name, t, _, [])) =
717 Assume (raw_label_for_name conjecture_shape name, t)
718 | step_for_line conjecture_shape facts_offset fact_names j
719 (Inference (name, t, _, deps)) =
720 Have (if j = 1 then [Show] else [],
721 raw_label_for_name conjecture_shape name,
722 fold_rev forall_of (map Var (Term.add_vars t [])) t,
723 ByMetis (fold (add_fact_from_dependency conjecture_shape facts_offset
727 fun repair_name "$true" = "c_True"
728 | repair_name "$false" = "c_False"
729 | repair_name "$$e" = tptp_equal (* seen in Vampire proofs *)
731 if is_tptp_equal s orelse
732 (* seen in Vampire proofs *)
733 (String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s) then
738 fun isar_proof_from_atp_proof pool ctxt isar_shrink_factor conjecture_shape
739 facts_offset fact_names sym_tab params frees atp_proof =
743 |> clean_up_atp_proof_dependencies
744 |> nasty_atp_proof pool
745 |> map_term_names_in_atp_proof repair_name
746 |> decode_lines ctxt sym_tab
747 |> rpair [] |-> fold_rev (add_line conjecture_shape fact_names)
748 |> rpair [] |-> fold_rev add_nontrivial_line
750 |-> fold_rev (add_desired_line isar_shrink_factor conjecture_shape
754 (if null params then [] else [Fix params]) @
755 map2 (step_for_line conjecture_shape facts_offset fact_names)
756 (length lines downto 1) lines
759 (* When redirecting proofs, we keep information about the labels seen so far in
760 the "backpatches" data structure. The first component indicates which facts
761 should be associated with forthcoming proof steps. The second component is a
762 pair ("assum_ls", "drop_ls"), where "assum_ls" are the labels that should
763 become assumptions and "drop_ls" are the labels that should be dropped in a
765 type backpatches = (label * facts) list * (label list * label list)
767 fun used_labels_of_step (Have (_, _, _, by)) =
769 ByMetis (ls, _) => ls
770 | CaseSplit (proofs, (ls, _)) =>
771 fold (union (op =) o used_labels_of) proofs ls)
772 | used_labels_of_step _ = []
773 and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []
775 fun new_labels_of_step (Fix _) = []
776 | new_labels_of_step (Let _) = []
777 | new_labels_of_step (Assume (l, _)) = [l]
778 | new_labels_of_step (Have (_, l, _, _)) = [l]
779 val new_labels_of = maps new_labels_of_step
784 | aux proof_tail (proofs as (proof1 :: _)) =
785 if exists null proofs then
787 else if forall (curry (op =) (hd proof1) o hd) (tl proofs) then
788 aux (hd proof1 :: proof_tail) (map tl proofs)
789 else case hd proof1 of
790 Have ([], l, t, _) => (* FIXME: should we really ignore the "by"? *)
791 if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t')
792 | _ => false) (tl proofs) andalso
793 not (exists (member (op =) (maps new_labels_of proofs))
794 (used_labels_of proof_tail)) then
795 SOME (l, t, map rev proofs, proof_tail)
799 in aux [] o map rev end
801 fun case_split_qualifiers proofs =
802 case length proofs of
807 fun redirect_proof hyp_ts concl_t proof =
809 (* The first pass outputs those steps that are independent of the negated
810 conjecture. The second pass flips the proof by contradiction to obtain a
811 direct proof, introducing case splits when an inference depends on
812 several facts that depend on the negated conjecture. *)
813 val concl_l = (conjecture_prefix, length hyp_ts)
814 fun first_pass ([], contra) = ([], contra)
815 | first_pass ((step as Fix _) :: proof, contra) =
816 first_pass (proof, contra) |>> cons step
817 | first_pass ((step as Let _) :: proof, contra) =
818 first_pass (proof, contra) |>> cons step
819 | first_pass ((step as Assume (l as (_, j), _)) :: proof, contra) =
820 if l = concl_l then first_pass (proof, contra ||> cons step)
821 else first_pass (proof, contra) |>> cons (Assume (l, nth hyp_ts j))
822 | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
823 let val step = Have (qs, l, t, ByMetis (ls, ss)) in
824 if exists (member (op =) (fst contra)) ls then
825 first_pass (proof, contra |>> cons l ||> cons step)
827 first_pass (proof, contra) |>> cons step
829 | first_pass _ = raise Fail "malformed proof"
830 val (proof_top, (contra_ls, contra_proof)) =
831 first_pass (proof, ([concl_l], []))
832 val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst
833 fun backpatch_labels patches ls =
834 fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
835 fun second_pass end_qs ([], assums, patches) =
836 ([Have (end_qs, no_label, concl_t,
837 ByMetis (backpatch_labels patches (map snd assums)))], patches)
838 | second_pass end_qs (Assume (l, t) :: proof, assums, patches) =
839 second_pass end_qs (proof, (t, l) :: assums, patches)
840 | second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums,
842 (if member (op =) (snd (snd patches)) l andalso
843 not (member (op =) (fst (snd patches)) l) andalso
844 not (AList.defined (op =) (fst patches) l) then
845 second_pass end_qs (proof, assums, patches ||> apsnd (append ls))
846 else case List.partition (member (op =) contra_ls) ls of
847 ([contra_l], co_ls) =>
848 if member (op =) qs Show then
849 second_pass end_qs (proof, assums,
850 patches |>> cons (contra_l, (co_ls, ss)))
854 patches |>> cons (contra_l, (l :: co_ls, ss)))
855 |>> cons (if member (op =) (fst (snd patches)) l then
858 Have (qs, l, s_not t,
859 ByMetis (backpatch_label patches l)))
860 | (contra_ls as _ :: _, co_ls) =>
869 val drop_ls = filter (curry (op <>) l) contra_ls
873 patches ||> apfst (insert (op =) l)
874 ||> apsnd (union (op =) drop_ls))
877 val (assumes, facts) =
878 if member (op =) (fst (snd patches)) l then
879 ([Assume (l, s_not t)], (l :: co_ls, ss))
883 (case join_proofs proofs of
884 SOME (l, t, proofs, proof_tail) =>
885 Have (case_split_qualifiers proofs @
886 (if null proof_tail then end_qs else []), l, t,
887 smart_case_split proofs facts) :: proof_tail
889 [Have (case_split_qualifiers proofs @ end_qs, no_label,
890 concl_t, smart_case_split proofs facts)],
894 | _ => raise Fail "malformed proof")
895 | second_pass _ _ = raise Fail "malformed proof"
897 second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst
898 in proof_top @ proof_bottom end
900 (* FIXME: Still needed? Probably not. *)
901 val kill_duplicate_assumptions_in_proof =
903 fun relabel_facts subst =
904 apfst (map (fn l => AList.lookup (op =) subst l |> the_default l))
905 fun do_step (step as Assume (l, t)) (proof, subst, assums) =
906 (case AList.lookup (op aconv) assums t of
907 SOME l' => (proof, (l, l') :: subst, assums)
908 | NONE => (step :: proof, subst, (t, l) :: assums))
909 | do_step (Have (qs, l, t, by)) (proof, subst, assums) =
912 ByMetis facts => ByMetis (relabel_facts subst facts)
913 | CaseSplit (proofs, facts) =>
914 CaseSplit (map do_proof proofs, relabel_facts subst facts)) ::
915 proof, subst, assums)
916 | do_step step (proof, subst, assums) = (step :: proof, subst, assums)
917 and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
920 val then_chain_proof =
923 | aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof
924 | aux l' (Have (qs, l, t, by) :: proof) =
927 Have (if member (op =) ls l' then
929 ByMetis (filter_out (curry (op =) l') ls, ss))
931 (qs, l, t, ByMetis (ls, ss)))
932 | CaseSplit (proofs, facts) =>
933 Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) ::
935 | aux _ (step :: proof) = step :: aux no_label proof
938 fun kill_useless_labels_in_proof proof =
940 val used_ls = used_labels_of proof
941 fun do_label l = if member (op =) used_ls l then l else no_label
942 fun do_step (Assume (l, t)) = Assume (do_label l, t)
943 | do_step (Have (qs, l, t, by)) =
944 Have (qs, do_label l, t,
946 CaseSplit (proofs, facts) =>
947 CaseSplit (map (map do_step) proofs, facts)
949 | do_step step = step
950 in map do_step proof end
952 fun prefix_for_depth n = replicate_string (n + 1)
956 fun aux _ _ _ [] = []
957 | aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) =
959 Assume (l, t) :: aux subst depth (next_assum, next_fact) proof
961 let val l' = (prefix_for_depth depth assum_prefix, next_assum) in
963 aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof
965 | aux subst depth (next_assum, next_fact) (Have (qs, l, t, by) :: proof) =
967 val (l', subst, next_fact) =
969 (l, subst, next_fact)
972 val l' = (prefix_for_depth depth have_prefix, next_fact)
973 in (l', (l, l') :: subst, next_fact + 1) end
975 apfst (maps (the_list o AList.lookup (op =) subst))
978 ByMetis facts => ByMetis (relabel_facts facts)
979 | CaseSplit (proofs, facts) =>
980 CaseSplit (map (aux subst (depth + 1) (1, 1)) proofs,
983 Have (qs, l', t, by) ::
984 aux subst depth (next_assum, next_fact) proof
986 | aux subst depth nextp (step :: proof) =
987 step :: aux subst depth nextp proof
988 in aux [] 0 (1, 1) end
990 fun string_for_proof ctxt0 full_types i n =
993 ctxt0 |> Config.put show_free_types false
994 |> Config.put show_types true
995 |> Config.put show_sorts true
996 fun fix_print_mode f x =
997 Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
998 (print_mode_value ())) f x
999 fun do_indent ind = replicate_string (ind * indent_size) " "
1000 fun do_free (s, T) =
1001 maybe_quote s ^ " :: " ^
1002 maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
1003 fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
1005 (if member (op =) qs Moreover then "moreover " else "") ^
1006 (if member (op =) qs Ultimately then "ultimately " else "") ^
1007 (if member (op =) qs Then then
1008 if member (op =) qs Show then "thus" else "hence"
1010 if member (op =) qs Show then "show" else "have")
1011 val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
1013 Metis (if full_types then full_typesN else partial_typesN, combinatorsN)
1014 fun do_facts (ls, ss) =
1015 reconstructor_command reconstr 1 1
1016 (ls |> sort_distinct (prod_ord string_ord int_ord),
1017 ss |> sort_distinct string_ord)
1018 and do_step ind (Fix xs) =
1019 do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
1020 | do_step ind (Let (t1, t2)) =
1021 do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
1022 | do_step ind (Assume (l, t)) =
1023 do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
1024 | do_step ind (Have (qs, l, t, ByMetis facts)) =
1025 do_indent ind ^ do_have qs ^ " " ^
1026 do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n"
1027 | do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) =
1028 space_implode (do_indent ind ^ "moreover\n")
1029 (map (do_block ind) proofs) ^
1030 do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^
1031 do_facts facts ^ "\n"
1032 and do_steps prefix suffix ind steps =
1033 let val s = implode (map (do_step ind) steps) in
1034 replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
1035 String.extract (s, ind * indent_size,
1036 SOME (size s - ind * indent_size - 1)) ^
1039 and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
1040 (* One-step proofs are pointless; better use the Metis one-liner
1042 and do_proof [Have (_, _, _, ByMetis _)] = ""
1044 (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
1045 do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^
1046 (if n <> 1 then "next" else "qed")
1049 fun isar_proof_text ctxt isar_proof_requested
1050 (debug, full_types, isar_shrink_factor, pool, conjecture_shape,
1051 facts_offset, fact_names, sym_tab, atp_proof, goal)
1052 (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
1054 val isar_shrink_factor =
1055 (if isar_proof_requested then 1 else 2) * isar_shrink_factor
1056 val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
1057 val frees = fold Term.add_frees (concl_t :: hyp_ts) []
1058 val one_line_proof = one_line_proof_text one_line_params
1059 fun isar_proof_for () =
1061 |> isar_proof_from_atp_proof pool ctxt isar_shrink_factor
1062 conjecture_shape facts_offset fact_names sym_tab params frees
1063 |> redirect_proof hyp_ts concl_t
1064 |> kill_duplicate_assumptions_in_proof
1066 |> kill_useless_labels_in_proof
1068 |> string_for_proof ctxt full_types subgoal subgoal_count of
1070 if isar_proof_requested then
1071 "\nNo structured proof available (proof too short)."
1075 "\n\n" ^ (if isar_proof_requested then "Structured proof"
1076 else "Perhaps this will work") ^
1077 ":\n" ^ Markup.markup Markup.sendback proof
1082 case try isar_proof_for () of
1084 | NONE => if isar_proof_requested then
1085 "\nWarning: The Isar proof construction failed."
1088 in one_line_proof ^ isar_proof end
1090 fun proof_text ctxt isar_proof isar_params
1091 (one_line_params as (preplay, _, _, _, _, _)) =
1092 (if case preplay of Failed_to_Play _ => true | _ => isar_proof then
1093 isar_proof_text ctxt isar_proof isar_params
1095 one_line_proof_text) one_line_params