adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
1 (* Title: HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
2 Author: Lawrence C Paulson and Claire Quigley, Cambridge University Computer Laboratory
3 Author: Jasmin Blanchette, TU Muenchen
5 Transfer of proofs from external provers.
8 signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
10 type minimize_command = string list -> string
11 type name_pool = Sledgehammer_FOL_Clause.name_pool
13 val invert_const: string -> string
14 val invert_type_const: string -> string
15 val num_type_args: theory -> string -> int
16 val strip_prefix: string -> string -> string option
17 val metis_line: int -> int -> string list -> string
19 minimize_command * string * string vector * thm * int
20 -> string * string list
22 name_pool option * bool * bool * int * Proof.context * int list list
23 -> minimize_command * string * string vector * thm * int
24 -> string * string list
26 bool -> name_pool option * bool * bool * int * Proof.context * int list list
27 -> minimize_command * string * string vector * thm * int
28 -> string * string list
31 structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
34 open Sledgehammer_Util
35 open Sledgehammer_FOL_Clause
36 open Sledgehammer_HOL_Clause
37 open Sledgehammer_Fact_Preprocessor
39 type minimize_command = string list -> string
41 fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
42 fun is_head_digit s = Char.isDigit (String.sub (s, 0))
44 val index_in_shape : int -> int list list -> int =
45 find_index o exists o curry (op =)
46 fun is_axiom_clause_number thm_names num = num <= Vector.length thm_names
47 fun is_conjecture_clause_number conjecture_shape num =
48 index_in_shape num conjecture_shape >= 0
50 fun ugly_name NONE s = s
51 | ugly_name (SOME the_pool) s =
52 case Symtab.lookup (snd the_pool) s of
56 fun smart_lambda v t =
59 List.last (space_explode skolem_infix (Long_Name.base_name s))
60 | Var ((s, _), _) => s
62 | _ => "", fastype_of v, abstract_over (v, t))
63 fun forall_of v t = HOLogic.all_const (fastype_of v) $ smart_lambda v t
65 datatype ('a, 'b, 'c, 'd, 'e) raw_step =
66 Definition of 'a * 'b * 'c |
67 Inference of 'a * 'd * 'e list
69 (**** PARSING OF TSTP FORMAT ****)
71 fun strip_spaces_in_list [] = ""
72 | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1
73 | strip_spaces_in_list [c1, c2] =
74 strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2]
75 | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) =
76 if Char.isSpace c1 then
77 strip_spaces_in_list (c2 :: c3 :: cs)
78 else if Char.isSpace c2 then
79 if Char.isSpace c3 then
80 strip_spaces_in_list (c1 :: c3 :: cs)
82 str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^
83 strip_spaces_in_list (c3 :: cs)
85 str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
86 val strip_spaces = strip_spaces_in_list o String.explode
88 (* Syntax trees, either term list or formulae *)
89 datatype node = IntLeaf of int | StrNode of string * node list
91 fun str_leaf s = StrNode (s, [])
93 fun scons (x, y) = StrNode ("cons", [x, y])
94 val slist_of = List.foldl scons (str_leaf "nil")
96 (*Strings enclosed in single quotes, e.g. filenames*)
97 val parse_quoted = $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode;
99 (*Integer constants, typically proof line numbers*)
100 val parse_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
102 val parse_dollar_name =
103 Scan.repeat ($$ "$") -- Symbol.scan_id >> (fn (ss, s) => implode ss ^ s)
105 (* needed for SPASS's output format *)
106 fun repair_name _ "$true" = "c_True"
107 | repair_name _ "$false" = "c_False"
108 | repair_name _ "$$e" = "c_equal" (* seen in Vampire 11 proofs *)
109 | repair_name _ "equal" = "c_equal" (* probably not needed *)
110 | repair_name pool s = ugly_name pool s
111 (* Generalized first-order terms, which include file names, numbers, etc. *)
112 (* The "x" argument is not strictly necessary, but without it Poly/ML loops
113 forever at compile time. *)
114 fun parse_term pool x =
115 (parse_quoted >> str_leaf
116 || parse_integer >> IntLeaf
117 || (parse_dollar_name >> repair_name pool)
118 -- Scan.optional ($$ "(" |-- parse_terms pool --| $$ ")") [] >> StrNode
119 || $$ "(" |-- parse_term pool --| $$ ")"
120 || $$ "[" |-- Scan.optional (parse_terms pool) [] --| $$ "]" >> slist_of) x
121 and parse_terms pool x =
122 (parse_term pool ::: Scan.repeat ($$ "," |-- parse_term pool)) x
124 fun negate_node u = StrNode ("c_Not", [u])
125 fun equate_nodes u1 u2 = StrNode ("c_equal", [u1, u2])
127 (* Apply equal or not-equal to a term. *)
128 fun repair_predicate_term (u, NONE) = u
129 | repair_predicate_term (u1, SOME (NONE, u2)) = equate_nodes u1 u2
130 | repair_predicate_term (u1, SOME (SOME _, u2)) =
131 negate_node (equate_nodes u1 u2)
132 fun parse_predicate_term pool =
133 parse_term pool -- Scan.option (Scan.option ($$ "!") --| $$ "="
135 >> repair_predicate_term
136 fun parse_literal pool x =
137 ($$ "~" |-- parse_literal pool >> negate_node || parse_predicate_term pool) x
138 fun parse_literals pool =
139 parse_literal pool ::: Scan.repeat ($$ "|" |-- parse_literal pool)
140 fun parse_parenthesized_literals pool =
141 $$ "(" |-- parse_literals pool --| $$ ")" || parse_literals pool
142 fun parse_clause pool =
143 parse_parenthesized_literals pool
144 ::: Scan.repeat ($$ "|" |-- parse_parenthesized_literals pool)
147 fun ints_of_node (IntLeaf n) = cons n
148 | ints_of_node (StrNode (_, us)) = fold ints_of_node us
149 val parse_tstp_annotations =
150 Scan.optional ($$ "," |-- parse_term NONE
151 --| Scan.option ($$ "," |-- parse_terms NONE)
152 >> (fn source => ints_of_node source [])) []
154 fun parse_definition pool =
155 $$ "(" |-- parse_literal NONE --| Scan.this_string "<=>"
156 -- parse_clause pool --| $$ ")"
158 (* Syntax: cnf(<num>, <formula_role>, <cnf_formula> <annotations>).
159 The <num> could be an identifier, but we assume integers. *)
160 fun finish_tstp_definition_line (num, (u, us)) = Definition (num, u, us)
161 fun finish_tstp_inference_line ((num, us), deps) = Inference (num, us, deps)
162 fun parse_tstp_line pool =
163 ((Scan.this_string "fof" -- $$ "(") |-- parse_integer --| $$ ","
164 --| Scan.this_string "definition" --| $$ "," -- parse_definition pool
165 --| parse_tstp_annotations --| $$ ")" --| $$ "."
166 >> finish_tstp_definition_line)
167 || ((Scan.this_string "cnf" -- $$ "(") |-- parse_integer --| $$ ","
168 --| Symbol.scan_id --| $$ "," -- parse_clause pool
169 -- parse_tstp_annotations --| $$ ")" --| $$ "."
170 >> finish_tstp_inference_line)
172 (**** PARSING OF SPASS OUTPUT ****)
174 (* SPASS returns clause references of the form "x.y". We ignore "y", whose role
175 is not clear anyway. *)
176 val parse_dot_name = parse_integer --| $$ "." --| parse_integer
178 val parse_spass_annotations =
179 Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name
180 --| Scan.option ($$ ","))) []
182 (* It is not clear why some literals are followed by sequences of stars and/or
183 pluses. We ignore them. *)
184 fun parse_decorated_predicate_term pool =
185 parse_predicate_term pool --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")
187 fun parse_horn_clause pool =
188 Scan.repeat (parse_decorated_predicate_term pool) --| $$ "|" --| $$ "|"
189 -- Scan.repeat (parse_decorated_predicate_term pool) --| $$ "-" --| $$ ">"
190 -- Scan.repeat (parse_decorated_predicate_term pool)
191 >> (fn (([], []), []) => [str_leaf "c_False"]
192 | ((clauses1, clauses2), clauses3) =>
193 map negate_node (clauses1 @ clauses2) @ clauses3)
195 (* Syntax: <num>[0:<inference><annotations>]
196 <cnf_formulas> || <cnf_formulas> -> <cnf_formulas>. *)
197 fun finish_spass_line ((num, deps), us) = Inference (num, us, deps)
198 fun parse_spass_line pool =
199 parse_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
200 -- parse_spass_annotations --| $$ "]" -- parse_horn_clause pool --| $$ "."
203 fun parse_line pool = parse_tstp_line pool || parse_spass_line pool
204 fun parse_lines pool = Scan.repeat1 (parse_line pool)
205 fun parse_proof pool =
206 fst o Scan.finite Symbol.stopper
207 (Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
209 o explode o strip_spaces
211 (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
213 exception NODE of node list
215 (*If string s has the prefix s1, return the result of deleting it.*)
216 fun strip_prefix s1 s =
217 if String.isPrefix s1 s
218 then SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
221 (*Invert the table of translations between Isabelle and ATPs*)
222 val type_const_trans_table_inv =
223 Symtab.make (map swap (Symtab.dest type_const_trans_table));
225 fun invert_type_const c =
226 case Symtab.lookup type_const_trans_table_inv c of
230 (* Type variables are given the basic sort "HOL.type". Some will later be
231 constrained by information from type literals, or by type inference. *)
232 fun type_from_node _ (u as IntLeaf _) = raise NODE [u]
233 | type_from_node tfrees (u as StrNode (a, us)) =
234 let val Ts = map (type_from_node tfrees) us in
235 case strip_prefix tconst_prefix a of
236 SOME b => Type (invert_type_const b, Ts)
238 if not (null us) then
239 raise NODE [u] (* only "tconst"s have type arguments *)
240 else case strip_prefix tfree_prefix a of
242 let val s = "'" ^ b in
243 TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
246 case strip_prefix tvar_prefix a of
247 SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
249 (* Variable from the ATP, say "X1" *)
250 Type_Infer.param 0 (a, HOLogic.typeS)
253 (*Invert the table of translations between Isabelle and ATPs*)
254 val const_trans_table_inv =
255 Symtab.update ("fequal", @{const_name "op ="})
256 (Symtab.make (map swap (Symtab.dest const_trans_table)))
258 fun invert_const c = c |> Symtab.lookup const_trans_table_inv |> the_default c
260 (* The number of type arguments of a constant, zero if it's monomorphic. For
261 (instances of) Skolem pseudoconstants, this information is encoded in the
263 fun num_type_args thy s =
264 if String.isPrefix skolem_theory_name s then
265 s |> unprefix skolem_theory_name
266 |> space_explode skolem_infix |> hd
267 |> space_explode "_" |> List.last |> Int.fromString |> the
269 (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
271 fun fix_atp_variable_name s =
273 fun subscript_name s n = s ^ nat_subscript n
274 val s = String.map Char.toLower s
276 case space_explode "_" s of
277 [_] => (case take_suffix Char.isDigit (String.explode s) of
278 (cs1 as _ :: _, cs2 as _ :: _) =>
279 subscript_name (String.implode cs1)
280 (the (Int.fromString (String.implode cs2)))
282 | [s1, s2] => (case Int.fromString s2 of
283 SOME n => subscript_name s1 n
288 (* First-order translation. No types are known for variables. "HOLogic.typeT"
289 should allow them to be inferred.*)
290 fun term_from_node thy full_types tfrees =
292 fun aux opt_T args u =
294 IntLeaf _ => raise NODE [u]
295 | StrNode ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1
296 | StrNode ("hAPP", [u1, u2]) => aux opt_T (u2 :: args) u1
297 | StrNode ("c_Not", [u1]) => @{const Not} $ aux (SOME @{typ bool}) [] u1
299 if a = type_wrapper_name then
302 aux (SOME (type_from_node tfrees typ_u)) args term_u
304 else case strip_prefix const_prefix a of
306 list_comb (Const (@{const_name "op ="}, HOLogic.typeT),
307 map (aux NONE []) us)
310 val c = invert_const b
311 val num_type_args = num_type_args thy c
312 val actual_num_type_args = if full_types then 0 else num_type_args
313 val num_term_args = length us - actual_num_type_args
314 val ts = map (aux NONE []) (take num_term_args us @ args)
316 Const (c, if full_types then
318 SOME T => map fastype_of ts ---> T
320 if num_type_args = 0 then
321 Sign.const_instance thy (c, [])
323 raise Fail ("no type information for " ^ quote c)
325 (* Extra args from "hAPP" come after any arguments
326 given directly to the constant. *)
327 if String.isPrefix skolem_theory_name c then
328 map fastype_of ts ---> HOLogic.typeT
330 Sign.const_instance thy (c,
331 map (type_from_node tfrees)
332 (drop num_term_args us)))
333 in list_comb (t, ts) end
334 | NONE => (* a free or schematic variable *)
336 val ts = map (aux NONE []) (us @ args)
337 val T = map fastype_of ts ---> HOLogic.typeT
339 case strip_prefix fixed_var_prefix a of
340 SOME b => Free (b, T)
342 case strip_prefix schematic_var_prefix a of
343 SOME b => Var ((b, 0), T)
345 (* Variable from the ATP, say "X1" *)
346 Var ((fix_atp_variable_name a, 0), T)
347 in list_comb (t, ts) end
350 (* Type class literal applied to a type. Returns triple of polarity, class,
352 fun type_constraint_from_node pos tfrees (StrNode ("c_Not", [u])) =
353 type_constraint_from_node (not pos) tfrees u
354 | type_constraint_from_node pos tfrees u = case u of
355 IntLeaf _ => raise NODE [u]
357 (case (strip_prefix class_prefix a,
358 map (type_from_node tfrees) us) of
359 (SOME b, [T]) => (pos, b, T)
360 | _ => raise NODE [u])
362 (** Accumulate type constraints in a clause: negative type literals **)
364 fun add_var (key, z) = Vartab.map_default (key, []) (cons z)
366 fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl)
367 | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl)
368 | add_type_constraint _ = I
370 fun is_positive_literal (@{const Not} $ _) = false
371 | is_positive_literal t = true
373 fun negate_term thy (Const (@{const_name All}, T) $ Abs (s, T', t')) =
374 Const (@{const_name Ex}, T) $ Abs (s, T', negate_term thy t')
375 | negate_term thy (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
376 Const (@{const_name All}, T) $ Abs (s, T', negate_term thy t')
377 | negate_term thy (@{const "op -->"} $ t1 $ t2) =
378 @{const "op &"} $ t1 $ negate_term thy t2
379 | negate_term thy (@{const "op &"} $ t1 $ t2) =
380 @{const "op |"} $ negate_term thy t1 $ negate_term thy t2
381 | negate_term thy (@{const "op |"} $ t1 $ t2) =
382 @{const "op &"} $ negate_term thy t1 $ negate_term thy t2
383 | negate_term _ (@{const Not} $ t) = t
384 | negate_term _ t = @{const Not} $ t
386 fun clause_for_literals _ [] = HOLogic.false_const
387 | clause_for_literals _ [lit] = lit
388 | clause_for_literals thy lits =
389 case List.partition is_positive_literal lits of
390 (pos_lits as _ :: _, neg_lits as _ :: _) =>
392 $ foldr1 HOLogic.mk_conj (map (negate_term thy) neg_lits)
393 $ foldr1 HOLogic.mk_disj pos_lits
394 | _ => foldr1 HOLogic.mk_disj lits
396 (* Final treatment of the list of "real" literals from a clause.
397 No "real" literals means only type information. *)
398 fun finish_clause _ [] = HOLogic.true_const
399 | finish_clause thy lits =
400 lits |> filter_out (curry (op =) HOLogic.false_const) |> rev
401 |> clause_for_literals thy
403 (*Accumulate sort constraints in vt, with "real" literals in lits.*)
404 fun lits_of_nodes thy full_types tfrees =
406 fun aux (vt, lits) [] = (vt, finish_clause thy lits)
407 | aux (vt, lits) (u :: us) =
408 aux (add_type_constraint
409 (type_constraint_from_node true tfrees u) vt, lits) us
411 aux (vt, term_from_node thy full_types tfrees (SOME @{typ bool})
415 (* Update TVars with detected sort constraints. It's not totally clear when
416 this code is necessary. *)
417 fun repair_tvar_sorts vt =
419 fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
420 | do_type (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi))
421 | do_type (TFree z) = TFree z
422 fun do_term (Const (a, T)) = Const (a, do_type T)
423 | do_term (Free (a, T)) = Free (a, do_type T)
424 | do_term (Var (xi, T)) = Var (xi, do_type T)
425 | do_term (t as Bound _) = t
426 | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t)
427 | do_term (t1 $ t2) = do_term t1 $ do_term t2
428 in not (Vartab.is_empty vt) ? do_term end
430 fun unskolemize_term t =
432 |> filter (is_skolem_const_name o fst) |> map Const
433 |> rpair t |-> fold forall_of
435 val combinator_table =
436 [(@{const_name COMBI}, @{thm COMBI_def_raw}),
437 (@{const_name COMBK}, @{thm COMBK_def_raw}),
438 (@{const_name COMBB}, @{thm COMBB_def_raw}),
439 (@{const_name COMBC}, @{thm COMBC_def_raw}),
440 (@{const_name COMBS}, @{thm COMBS_def_raw})]
442 fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2))
443 | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t')
444 | uncombine_term (t as Const (x as (s, _))) =
445 (case AList.lookup (op =) combinator_table s of
446 SOME thm => thm |> prop_of |> specialize_type @{theory} x |> Logic.dest_equals |> snd
448 | uncombine_term t = t
450 (* Interpret a list of syntax trees as a clause, given by "real" literals and
451 sort constraints. "vt" holds the initial sort constraints, from the
452 conjecture clauses. *)
453 fun clause_of_nodes ctxt full_types tfrees us =
455 val thy = ProofContext.theory_of ctxt
456 val (vt, t) = lits_of_nodes thy full_types tfrees (Vartab.empty, []) us
457 in repair_tvar_sorts vt t end
458 fun check_formula ctxt =
459 Type_Infer.constrain @{typ bool}
460 #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
463 (**** Translation of TSTP files to Isar Proofs ****)
465 fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
466 | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
468 fun decode_line full_types tfrees (Definition (num, u, us)) ctxt =
470 val t1 = clause_of_nodes ctxt full_types tfrees [u]
471 val vars = snd (strip_comb t1)
472 val frees = map unvarify_term vars
473 val unvarify_args = subst_atomic (vars ~~ frees)
474 val t2 = clause_of_nodes ctxt full_types tfrees us
476 HOLogic.eq_const HOLogic.typeT $ t1 $ t2
477 |> unvarify_args |> uncombine_term |> check_formula ctxt
480 (Definition (num, t1, t2),
481 fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
483 | decode_line full_types tfrees (Inference (num, us, deps)) ctxt =
485 val t = us |> clause_of_nodes ctxt full_types tfrees
486 |> unskolemize_term |> uncombine_term |> check_formula ctxt
488 (Inference (num, t, deps),
489 fold Variable.declare_term (OldTerm.term_frees t) ctxt)
491 fun decode_lines ctxt full_types tfrees lines =
492 fst (fold_map (decode_line full_types tfrees) lines ctxt)
494 fun aint_actual_inference _ (Definition _) = true
495 | aint_actual_inference t (Inference (_, t', _)) = not (t aconv t')
497 (* No "real" literals means only type information (tfree_tcs, clsrel, or
499 val is_only_type_information = curry (op aconv) HOLogic.true_const
501 fun replace_one_dep (old, new) dep = if dep = old then new else [dep]
502 fun replace_deps_in_line _ (line as Definition _) = line
503 | replace_deps_in_line p (Inference (num, t, deps)) =
504 Inference (num, t, fold (union (op =) o replace_one_dep p) deps [])
506 (*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ
507 only in type information.*)
508 fun add_line _ _ (line as Definition _) lines = line :: lines
509 | add_line conjecture_shape thm_names (Inference (num, t, [])) lines =
510 (* No dependencies: axiom, conjecture clause, or internal axioms or
511 definitions (Vampire). *)
512 if is_axiom_clause_number thm_names num then
513 (* Axioms are not proof lines. *)
514 if is_only_type_information t then
515 map (replace_deps_in_line (num, [])) lines
516 (* Is there a repetition? If so, replace later line by earlier one. *)
517 else case take_prefix (aint_actual_inference t) lines of
518 (_, []) => lines (*no repetition of proof line*)
519 | (pre, Inference (num', _, _) :: post) =>
520 pre @ map (replace_deps_in_line (num', [num])) post
521 else if is_conjecture_clause_number conjecture_shape num then
522 Inference (num, t, []) :: lines
524 map (replace_deps_in_line (num, [])) lines
525 | add_line _ _ (Inference (num, t, deps)) lines =
526 (* Type information will be deleted later; skip repetition test. *)
527 if is_only_type_information t then
528 Inference (num, t, deps) :: lines
529 (* Is there a repetition? If so, replace later line by earlier one. *)
530 else case take_prefix (aint_actual_inference t) lines of
531 (* FIXME: Doesn't this code risk conflating proofs involving different
533 (_, []) => Inference (num, t, deps) :: lines
534 | (pre, Inference (num', t', _) :: post) =>
535 Inference (num, t', deps) ::
536 pre @ map (replace_deps_in_line (num', [num])) post
538 (* Recursively delete empty lines (type information) from the proof. *)
539 fun add_nontrivial_line (Inference (num, t, [])) lines =
540 if is_only_type_information t then delete_dep num lines
541 else Inference (num, t, []) :: lines
542 | add_nontrivial_line line lines = line :: lines
543 and delete_dep num lines =
544 fold_rev add_nontrivial_line (map (replace_deps_in_line (num, [])) lines) []
546 (* ATPs sometimes reuse free variable names in the strangest ways. Removing
547 offending lines often does the trick. *)
548 fun is_bad_free frees (Free x) = not (member (op =) frees x)
549 | is_bad_free _ _ = false
551 (* Vampire is keen on producing these. *)
552 fun is_trivial_formula (@{const Not} $ (Const (@{const_name "op ="}, _)
553 $ t1 $ t2)) = (t1 aconv t2)
554 | is_trivial_formula t = false
556 fun add_desired_line _ _ _ _ _ (line as Definition (num, _, _)) (j, lines) =
557 (j, line :: map (replace_deps_in_line (num, [])) lines)
558 | add_desired_line ctxt isar_shrink_factor conjecture_shape thm_names frees
559 (Inference (num, t, deps)) (j, lines) =
561 if is_axiom_clause_number thm_names num orelse
562 is_conjecture_clause_number conjecture_shape num orelse
563 (not (is_only_type_information t) andalso
564 null (Term.add_tvars t []) andalso
565 not (exists_subterm (is_bad_free frees) t) andalso
566 not (is_trivial_formula t) andalso
567 (null lines orelse (* last line must be kept *)
568 (length deps >= 2 andalso j mod isar_shrink_factor = 0))) then
569 Inference (num, t, deps) :: lines (* keep line *)
571 map (replace_deps_in_line (num, deps)) lines) (* drop line *)
573 (** EXTRACTING LEMMAS **)
575 (* A list consisting of the first number in each line is returned.
576 TSTP: Interesting lines have the form "cnf(108, axiom, ...)", where the
577 number (108) is extracted.
578 SPASS: Lines have the form "108[0:Inp] ...", where the first number (108) is
580 fun extract_clause_numbers_in_atp_proof atp_proof =
582 val tokens_of = String.tokens (not o is_ident_char)
583 fun extract_num ("cnf" :: num :: "axiom" :: _) = Int.fromString num
584 | extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num
585 | extract_num _ = NONE
586 in atp_proof |> split_lines |> map_filter (extract_num o tokens_of) end
589 val no_label = ("", ~1)
592 val assum_prefix = "A"
593 val fact_prefix = "F"
595 fun string_for_label (s, num) = s ^ string_of_int num
597 fun metis_using [] = ""
599 "using " ^ space_implode " " (map string_for_label ls) ^ " "
600 fun metis_apply _ 1 = "by "
601 | metis_apply 1 _ = "apply "
602 | metis_apply i _ = "prefer " ^ string_of_int i ^ " apply "
603 fun metis_itself [] = "metis"
604 | metis_itself ss = "(metis " ^ space_implode " " ss ^ ")"
605 fun metis_command i n (ls, ss) =
606 metis_using ls ^ metis_apply i n ^ metis_itself ss
607 fun metis_line i n ss =
608 "Try this command: " ^
609 Markup.markup Markup.sendback (metis_command i n ([], ss)) ^ ".\n"
610 fun minimize_line _ [] = ""
611 | minimize_line minimize_command facts =
612 case minimize_command facts of
615 "To minimize the number of lemmas, try this command: " ^
616 Markup.markup Markup.sendback command ^ ".\n"
618 val unprefix_chained = perhaps (try (unprefix chained_prefix))
620 fun metis_proof_text (minimize_command, atp_proof, thm_names, goal, i) =
623 atp_proof |> extract_clause_numbers_in_atp_proof
624 |> filter (is_axiom_clause_number thm_names)
625 |> map (fn i => Vector.sub (thm_names, i - 1))
626 val (chained_lemmas, other_lemmas) =
627 raw_lemmas |> List.partition (String.isPrefix chained_prefix)
628 |>> map (unprefix chained_prefix)
629 |> pairself (sort_distinct string_ord)
630 val lemmas = other_lemmas @ chained_lemmas
631 val n = Logic.count_prems (prop_of goal)
633 (metis_line i n other_lemmas ^ minimize_line minimize_command lemmas,
637 (** Isar proof construction and manipulation **)
639 fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
640 (union (op =) ls1 ls2, union (op =) ss1 ss2)
642 type label = string * int
643 type facts = label list * string list
645 datatype qualifier = Show | Then | Moreover | Ultimately
648 Fix of (string * typ) list |
650 Assume of label * term |
651 Have of qualifier list * label * term * byline
654 CaseSplit of step list list * facts
656 fun smart_case_split [] facts = ByMetis facts
657 | smart_case_split proofs facts = CaseSplit (proofs, facts)
659 fun add_fact_from_dep thm_names num =
660 if is_axiom_clause_number thm_names num then
661 apsnd (insert (op =) (Vector.sub (thm_names, num - 1)))
663 apfst (insert (op =) (raw_prefix, num))
665 fun forall_vars t = fold_rev forall_of (map Var (Term.add_vars t [])) t
667 fun step_for_line _ _ (Definition (num, t1, t2)) = Let (t1, t2)
668 | step_for_line _ _ (Inference (num, t, [])) = Assume ((raw_prefix, num), t)
669 | step_for_line thm_names j (Inference (num, t, deps)) =
670 Have (if j = 1 then [Show] else [], (raw_prefix, num),
672 ByMetis (fold (add_fact_from_dep thm_names) deps ([], [])))
674 fun proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
675 atp_proof conjecture_shape thm_names params frees =
678 atp_proof ^ "$" (* the $ sign acts as a sentinel *)
680 |> decode_lines ctxt full_types tfrees
681 |> rpair [] |-> fold_rev (add_line conjecture_shape thm_names)
682 |> rpair [] |-> fold_rev add_nontrivial_line
683 |> rpair (0, []) |-> fold_rev (add_desired_line ctxt isar_shrink_factor
684 conjecture_shape thm_names frees)
687 (if null params then [] else [Fix params]) @
688 map2 (step_for_line thm_names) (length lines downto 1) lines
691 (* When redirecting proofs, we keep information about the labels seen so far in
692 the "backpatches" data structure. The first component indicates which facts
693 should be associated with forthcoming proof steps. The second component is a
694 pair ("assum_ls", "drop_ls"), where "assum_ls" are the labels that should
695 become assumptions and "drop_ls" are the labels that should be dropped in a
697 type backpatches = (label * facts) list * (label list * label list)
699 fun used_labels_of_step (Have (_, _, _, by)) =
701 ByMetis (ls, _) => ls
702 | CaseSplit (proofs, (ls, _)) =>
703 fold (union (op =) o used_labels_of) proofs ls)
704 | used_labels_of_step _ = []
705 and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []
707 fun new_labels_of_step (Fix _) = []
708 | new_labels_of_step (Let _) = []
709 | new_labels_of_step (Assume (l, _)) = [l]
710 | new_labels_of_step (Have (_, l, _, _)) = [l]
711 val new_labels_of = maps new_labels_of_step
716 | aux proof_tail (proofs as (proof1 :: _)) =
717 if exists null proofs then
719 else if forall (curry (op =) (hd proof1) o hd) (tl proofs) then
720 aux (hd proof1 :: proof_tail) (map tl proofs)
721 else case hd proof1 of
722 Have ([], l, t, by) =>
723 if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t')
724 | _ => false) (tl proofs) andalso
725 not (exists (member (op =) (maps new_labels_of proofs))
726 (used_labels_of proof_tail)) then
727 SOME (l, t, map rev proofs, proof_tail)
731 in aux [] o map rev end
733 fun case_split_qualifiers proofs =
734 case length proofs of
739 fun redirect_proof thy conjecture_shape hyp_ts concl_t proof =
741 (* The first pass outputs those steps that are independent of the negated
742 conjecture. The second pass flips the proof by contradiction to obtain a
743 direct proof, introducing case splits when an inference depends on
744 several facts that depend on the negated conjecture. *)
745 fun find_hyp num = nth hyp_ts (index_in_shape num conjecture_shape)
746 val concl_ls = map (pair raw_prefix) (List.last conjecture_shape)
747 val canonicalize_labels =
748 map (fn l => if member (op =) concl_ls l then hd concl_ls else l)
750 fun first_pass ([], contra) = ([], contra)
751 | first_pass ((step as Fix _) :: proof, contra) =
752 first_pass (proof, contra) |>> cons step
753 | first_pass ((step as Let _) :: proof, contra) =
754 first_pass (proof, contra) |>> cons step
755 | first_pass ((step as Assume (l as (_, num), t)) :: proof, contra) =
756 if member (op =) concl_ls l then
757 first_pass (proof, contra ||> l = hd concl_ls ? cons step)
759 first_pass (proof, contra) |>> cons (Assume (l, find_hyp num))
760 | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
762 val ls = canonicalize_labels ls
763 val step = Have (qs, l, t, ByMetis (ls, ss))
765 if exists (member (op =) (fst contra)) ls then
766 first_pass (proof, contra |>> cons l ||> cons step)
768 first_pass (proof, contra) |>> cons step
770 | first_pass _ = raise Fail "malformed proof"
771 val (proof_top, (contra_ls, contra_proof)) =
772 first_pass (proof, (concl_ls, []))
773 val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst
774 fun backpatch_labels patches ls =
775 fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
776 fun second_pass end_qs ([], assums, patches) =
777 ([Have (end_qs, no_label, concl_t,
778 ByMetis (backpatch_labels patches (map snd assums)))], patches)
779 | second_pass end_qs (Assume (l, t) :: proof, assums, patches) =
780 second_pass end_qs (proof, (t, l) :: assums, patches)
781 | second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums,
783 if member (op =) (snd (snd patches)) l andalso
784 not (member (op =) (fst (snd patches)) l) andalso
785 not (AList.defined (op =) (fst patches) l) then
786 second_pass end_qs (proof, assums, patches ||> apsnd (append ls))
788 (case List.partition (member (op =) contra_ls) ls of
789 ([contra_l], co_ls) =>
790 if member (op =) qs Show then
791 second_pass end_qs (proof, assums,
792 patches |>> cons (contra_l, (co_ls, ss)))
796 patches |>> cons (contra_l, (l :: co_ls, ss)))
797 |>> cons (if member (op =) (fst (snd patches)) l then
798 Assume (l, negate_term thy t)
800 Have (qs, l, negate_term thy t,
801 ByMetis (backpatch_label patches l)))
802 | (contra_ls as _ :: _, co_ls) =>
807 if member (op =) concl_ls l then
811 val drop_ls = filter (curry (op <>) l) contra_ls
815 patches ||> apfst (insert (op =) l)
816 ||> apsnd (union (op =) drop_ls))
819 val (assumes, facts) =
820 if member (op =) (fst (snd patches)) l then
821 ([Assume (l, negate_term thy t)], (l :: co_ls, ss))
825 (case join_proofs proofs of
826 SOME (l, t, proofs, proof_tail) =>
827 Have (case_split_qualifiers proofs @
828 (if null proof_tail then end_qs else []), l, t,
829 smart_case_split proofs facts) :: proof_tail
831 [Have (case_split_qualifiers proofs @ end_qs, no_label,
832 concl_t, smart_case_split proofs facts)],
836 | _ => raise Fail "malformed proof")
837 | second_pass _ _ = raise Fail "malformed proof"
839 second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst
840 in proof_top @ proof_bottom end
842 val kill_duplicate_assumptions_in_proof =
844 fun relabel_facts subst =
845 apfst (map (fn l => AList.lookup (op =) subst l |> the_default l))
846 fun do_step (step as Assume (l, t)) (proof, subst, assums) =
847 (case AList.lookup (op aconv) assums t of
848 SOME l' => (proof, (l, l') :: subst, assums)
849 | NONE => (step :: proof, subst, (t, l) :: assums))
850 | do_step (Have (qs, l, t, by)) (proof, subst, assums) =
853 ByMetis facts => ByMetis (relabel_facts subst facts)
854 | CaseSplit (proofs, facts) =>
855 CaseSplit (map do_proof proofs, relabel_facts subst facts)) ::
856 proof, subst, assums)
857 | do_step step (proof, subst, assums) = (step :: proof, subst, assums)
858 and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
861 val then_chain_proof =
864 | aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof
865 | aux l' (Have (qs, l, t, by) :: proof) =
868 Have (if member (op =) ls l' then
870 ByMetis (filter_out (curry (op =) l') ls, ss))
872 (qs, l, t, ByMetis (ls, ss)))
873 | CaseSplit (proofs, facts) =>
874 Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) ::
876 | aux _ (step :: proof) = step :: aux no_label proof
879 fun kill_useless_labels_in_proof proof =
881 val used_ls = used_labels_of proof
882 fun do_label l = if member (op =) used_ls l then l else no_label
883 fun do_step (Assume (l, t)) = Assume (do_label l, t)
884 | do_step (Have (qs, l, t, by)) =
885 Have (qs, do_label l, t,
887 CaseSplit (proofs, facts) =>
888 CaseSplit (map (map do_step) proofs, facts)
890 | do_step step = step
891 in map do_step proof end
893 fun prefix_for_depth n = replicate_string (n + 1)
897 fun aux _ _ _ [] = []
898 | aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) =
900 Assume (l, t) :: aux subst depth (next_assum, next_fact) proof
902 let val l' = (prefix_for_depth depth assum_prefix, next_assum) in
904 aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof
906 | aux subst depth (next_assum, next_fact) (Have (qs, l, t, by) :: proof) =
908 val (l', subst, next_fact) =
910 (l, subst, next_fact)
913 val l' = (prefix_for_depth depth fact_prefix, next_fact)
914 in (l', (l, l') :: subst, next_fact + 1) end
917 case AList.lookup (op =) subst l of
919 | NONE => raise Fail ("unknown label " ^
920 quote (string_for_label l))))
923 ByMetis facts => ByMetis (relabel_facts facts)
924 | CaseSplit (proofs, facts) =>
925 CaseSplit (map (aux subst (depth + 1) (1, 1)) proofs,
928 Have (qs, l', t, by) ::
929 aux subst depth (next_assum, next_fact) proof
931 | aux subst depth nextp (step :: proof) =
932 step :: aux subst depth nextp proof
933 in aux [] 0 (1, 1) end
935 fun string_for_proof ctxt i n =
937 fun fix_print_mode f x =
938 setmp_CRITICAL show_no_free_types true
939 (setmp_CRITICAL show_types true
940 (Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
941 (print_mode_value ())) f)) x
942 fun do_indent ind = replicate_string (ind * indent_size) " "
944 maybe_quote s ^ " :: " ^
945 maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
946 fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
948 (if member (op =) qs Moreover then "moreover " else "") ^
949 (if member (op =) qs Ultimately then "ultimately " else "") ^
950 (if member (op =) qs Then then
951 if member (op =) qs Show then "thus" else "hence"
953 if member (op =) qs Show then "show" else "have")
954 val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
955 fun do_facts (ls, ss) =
957 val ls = ls |> sort_distinct (prod_ord string_ord int_ord)
958 val ss = ss |> map unprefix_chained |> sort_distinct string_ord
959 in metis_command 1 1 (ls, ss) end
960 and do_step ind (Fix xs) =
961 do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
962 | do_step ind (Let (t1, t2)) =
963 do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
964 | do_step ind (Assume (l, t)) =
965 do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
966 | do_step ind (Have (qs, l, t, ByMetis facts)) =
967 do_indent ind ^ do_have qs ^ " " ^
968 do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n"
969 | do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) =
970 space_implode (do_indent ind ^ "moreover\n")
971 (map (do_block ind) proofs) ^
972 do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^
973 do_facts facts ^ "\n"
974 and do_steps prefix suffix ind steps =
975 let val s = implode (map (do_step ind) steps) in
976 replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
977 String.extract (s, ind * indent_size,
978 SOME (size s - ind * indent_size - 1)) ^
981 and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
982 (* One-step proofs are pointless; better use the Metis one-liner
984 and do_proof [Have (_, _, _, ByMetis _)] = ""
986 (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
987 do_indent 0 ^ "proof -\n" ^
988 do_steps "" "" 1 proof ^
989 do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n"
992 fun isar_proof_text (pool, debug, full_types, isar_shrink_factor, ctxt,
994 (minimize_command, atp_proof, thm_names, goal, i) =
996 val thy = ProofContext.theory_of ctxt
997 val (params, hyp_ts, concl_t) = strip_subgoal goal i
998 val frees = fold Term.add_frees (concl_t :: hyp_ts) []
999 val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
1000 val n = Logic.count_prems (prop_of goal)
1001 val (one_line_proof, lemma_names) =
1002 metis_proof_text (minimize_command, atp_proof, thm_names, goal, i)
1003 fun isar_proof_for () =
1004 case proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
1005 atp_proof conjecture_shape thm_names params
1007 |> redirect_proof thy conjecture_shape hyp_ts concl_t
1008 |> kill_duplicate_assumptions_in_proof
1010 |> kill_useless_labels_in_proof
1012 |> string_for_proof ctxt i n of
1014 | proof => "\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
1019 try isar_proof_for ()
1020 |> the_default "Warning: The Isar proof construction failed.\n"
1021 in (one_line_proof ^ isar_proof, lemma_names) end
1023 fun proof_text isar_proof isar_params other_params =
1024 (if isar_proof then isar_proof_text isar_params else metis_proof_text)