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 (* Hack: Could return false positives (e.g., a user happens to declare a
45 constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
46 val is_skolem_const_name =
48 #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
50 val index_in_shape : int -> int list list -> int =
51 find_index o exists o curry (op =)
52 fun is_axiom_clause_number thm_names num = num <= Vector.length thm_names
53 fun is_conjecture_clause_number conjecture_shape num =
54 index_in_shape num conjecture_shape >= 0
56 fun ugly_name NONE s = s
57 | ugly_name (SOME the_pool) s =
58 case Symtab.lookup (snd the_pool) s of
62 fun smart_lambda v t =
65 List.last (space_explode skolem_infix (Long_Name.base_name s))
66 | Var ((s, _), _) => s
68 | _ => "", fastype_of v, abstract_over (v, t))
69 fun forall_of v t = HOLogic.all_const (fastype_of v) $ smart_lambda v t
71 datatype ('a, 'b, 'c, 'd, 'e) raw_step =
72 Definition of 'a * 'b * 'c |
73 Inference of 'a * 'd * 'e list
75 (**** PARSING OF TSTP FORMAT ****)
77 fun strip_spaces_in_list [] = ""
78 | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1
79 | strip_spaces_in_list [c1, c2] =
80 strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2]
81 | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) =
82 if Char.isSpace c1 then
83 strip_spaces_in_list (c2 :: c3 :: cs)
84 else if Char.isSpace c2 then
85 if Char.isSpace c3 then
86 strip_spaces_in_list (c1 :: c3 :: cs)
88 str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^
89 strip_spaces_in_list (c3 :: cs)
91 str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
92 val strip_spaces = strip_spaces_in_list o String.explode
94 (* Syntax trees, either term list or formulae *)
95 datatype node = IntLeaf of int | StrNode of string * node list
97 fun str_leaf s = StrNode (s, [])
99 fun scons (x, y) = StrNode ("cons", [x, y])
100 val slist_of = List.foldl scons (str_leaf "nil")
102 (*Strings enclosed in single quotes, e.g. filenames*)
103 val parse_quoted = $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode;
105 (*Integer constants, typically proof line numbers*)
106 val parse_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
108 val parse_dollar_name =
109 Scan.repeat ($$ "$") -- Symbol.scan_id >> (fn (ss, s) => implode ss ^ s)
111 (* needed for SPASS's output format *)
112 fun repair_name _ "$true" = "c_True"
113 | repair_name _ "$false" = "c_False"
114 | repair_name _ "$$e" = "c_equal" (* seen in Vampire 11 proofs *)
115 | repair_name _ "equal" = "c_equal" (* probably not needed *)
116 | repair_name pool s = ugly_name pool s
117 (* Generalized first-order terms, which include file names, numbers, etc. *)
118 (* The "x" argument is not strictly necessary, but without it Poly/ML loops
119 forever at compile time. *)
120 fun parse_term pool x =
121 (parse_quoted >> str_leaf
122 || parse_integer >> IntLeaf
123 || (parse_dollar_name >> repair_name pool)
124 -- Scan.optional ($$ "(" |-- parse_terms pool --| $$ ")") [] >> StrNode
125 || $$ "(" |-- parse_term pool --| $$ ")"
126 || $$ "[" |-- Scan.optional (parse_terms pool) [] --| $$ "]" >> slist_of) x
127 and parse_terms pool x =
128 (parse_term pool ::: Scan.repeat ($$ "," |-- parse_term pool)) x
130 fun negate_node u = StrNode ("c_Not", [u])
131 fun equate_nodes u1 u2 = StrNode ("c_equal", [u1, u2])
133 (* Apply equal or not-equal to a term. *)
134 fun repair_predicate_term (u, NONE) = u
135 | repair_predicate_term (u1, SOME (NONE, u2)) = equate_nodes u1 u2
136 | repair_predicate_term (u1, SOME (SOME _, u2)) =
137 negate_node (equate_nodes u1 u2)
138 fun parse_predicate_term pool =
139 parse_term pool -- Scan.option (Scan.option ($$ "!") --| $$ "="
141 >> repair_predicate_term
142 fun parse_literal pool x =
143 ($$ "~" |-- parse_literal pool >> negate_node || parse_predicate_term pool) x
144 fun parse_literals pool =
145 parse_literal pool ::: Scan.repeat ($$ "|" |-- parse_literal pool)
146 fun parse_parenthesized_literals pool =
147 $$ "(" |-- parse_literals pool --| $$ ")" || parse_literals pool
148 fun parse_clause pool =
149 parse_parenthesized_literals pool
150 ::: Scan.repeat ($$ "|" |-- parse_parenthesized_literals pool)
153 fun ints_of_node (IntLeaf n) = cons n
154 | ints_of_node (StrNode (_, us)) = fold ints_of_node us
155 val parse_tstp_annotations =
156 Scan.optional ($$ "," |-- parse_term NONE
157 --| Scan.option ($$ "," |-- parse_terms NONE)
158 >> (fn source => ints_of_node source [])) []
160 fun parse_definition pool =
161 $$ "(" |-- parse_literal NONE --| Scan.this_string "<=>"
162 -- parse_clause pool --| $$ ")"
164 (* Syntax: cnf(<num>, <formula_role>, <cnf_formula> <annotations>).
165 The <num> could be an identifier, but we assume integers. *)
166 fun finish_tstp_definition_line (num, (u, us)) = Definition (num, u, us)
167 fun finish_tstp_inference_line ((num, us), deps) = Inference (num, us, deps)
168 fun parse_tstp_line pool =
169 ((Scan.this_string "fof" -- $$ "(") |-- parse_integer --| $$ ","
170 --| Scan.this_string "definition" --| $$ "," -- parse_definition pool
171 --| parse_tstp_annotations --| $$ ")" --| $$ "."
172 >> finish_tstp_definition_line)
173 || ((Scan.this_string "cnf" -- $$ "(") |-- parse_integer --| $$ ","
174 --| Symbol.scan_id --| $$ "," -- parse_clause pool
175 -- parse_tstp_annotations --| $$ ")" --| $$ "."
176 >> finish_tstp_inference_line)
178 (**** PARSING OF SPASS OUTPUT ****)
180 (* SPASS returns clause references of the form "x.y". We ignore "y", whose role
181 is not clear anyway. *)
182 val parse_dot_name = parse_integer --| $$ "." --| parse_integer
184 val parse_spass_annotations =
185 Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name
186 --| Scan.option ($$ ","))) []
188 (* It is not clear why some literals are followed by sequences of stars and/or
189 pluses. We ignore them. *)
190 fun parse_decorated_predicate_term pool =
191 parse_predicate_term pool --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")
193 fun parse_horn_clause pool =
194 Scan.repeat (parse_decorated_predicate_term pool) --| $$ "|" --| $$ "|"
195 -- Scan.repeat (parse_decorated_predicate_term pool) --| $$ "-" --| $$ ">"
196 -- Scan.repeat (parse_decorated_predicate_term pool)
197 >> (fn (([], []), []) => [str_leaf "c_False"]
198 | ((clauses1, clauses2), clauses3) =>
199 map negate_node (clauses1 @ clauses2) @ clauses3)
201 (* Syntax: <num>[0:<inference><annotations>]
202 <cnf_formulas> || <cnf_formulas> -> <cnf_formulas>. *)
203 fun finish_spass_line ((num, deps), us) = Inference (num, us, deps)
204 fun parse_spass_line pool =
205 parse_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
206 -- parse_spass_annotations --| $$ "]" -- parse_horn_clause pool --| $$ "."
209 fun parse_line pool = parse_tstp_line pool || parse_spass_line pool
210 fun parse_lines pool = Scan.repeat1 (parse_line pool)
211 fun parse_proof pool =
212 fst o Scan.finite Symbol.stopper
213 (Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
215 o explode o strip_spaces
217 (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
219 exception NODE of node list
221 (*If string s has the prefix s1, return the result of deleting it.*)
222 fun strip_prefix s1 s =
223 if String.isPrefix s1 s
224 then SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
227 (*Invert the table of translations between Isabelle and ATPs*)
228 val type_const_trans_table_inv =
229 Symtab.make (map swap (Symtab.dest type_const_trans_table));
231 fun invert_type_const c =
232 case Symtab.lookup type_const_trans_table_inv c of
236 (* Type variables are given the basic sort "HOL.type". Some will later be
237 constrained by information from type literals, or by type inference. *)
238 fun type_from_node _ (u as IntLeaf _) = raise NODE [u]
239 | type_from_node tfrees (u as StrNode (a, us)) =
240 let val Ts = map (type_from_node tfrees) us in
241 case strip_prefix tconst_prefix a of
242 SOME b => Type (invert_type_const b, Ts)
244 if not (null us) then
245 raise NODE [u] (* only "tconst"s have type arguments *)
246 else case strip_prefix tfree_prefix a of
248 let val s = "'" ^ b in
249 TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
252 case strip_prefix tvar_prefix a of
253 SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
255 (* Variable from the ATP, say "X1" *)
256 Type_Infer.param 0 (a, HOLogic.typeS)
259 (*Invert the table of translations between Isabelle and ATPs*)
260 val const_trans_table_inv =
261 Symtab.update ("fequal", @{const_name "op ="})
262 (Symtab.make (map swap (Symtab.dest const_trans_table)))
264 fun invert_const c = c |> Symtab.lookup const_trans_table_inv |> the_default c
266 (*The number of type arguments of a constant, zero if it's monomorphic*)
267 fun num_type_args thy s =
268 length (Sign.const_typargs thy (s, Sign.the_const_type thy s))
270 fun fix_atp_variable_name s =
272 fun subscript_name s n = s ^ nat_subscript n
273 val s = String.map Char.toLower s
275 case space_explode "_" s of
276 [_] => (case take_suffix Char.isDigit (String.explode s) of
277 (cs1 as _ :: _, cs2 as _ :: _) =>
278 subscript_name (String.implode cs1)
279 (the (Int.fromString (String.implode cs2)))
281 | [s1, s2] => (case Int.fromString s2 of
282 SOME n => subscript_name s1 n
287 (* First-order translation. No types are known for variables. "HOLogic.typeT"
288 should allow them to be inferred.*)
289 fun term_from_node thy full_types tfrees =
291 fun aux opt_T args u =
293 IntLeaf _ => raise NODE [u]
294 | StrNode ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1
295 | StrNode ("hAPP", [u1, u2]) => aux opt_T (u2 :: args) u1
296 | StrNode ("c_Not", [u1]) => @{const Not} $ aux (SOME @{typ bool}) [] u1
298 if a = type_wrapper_name then
301 aux (SOME (type_from_node tfrees typ_u)) args term_u
303 else case strip_prefix const_prefix a of
305 list_comb (Const (@{const_name "op ="}, HOLogic.typeT),
306 map (aux NONE []) us)
309 val c = invert_const b
310 val num_type_args = num_type_args thy c
311 val actual_num_type_args = if full_types then 0 else num_type_args
312 val num_term_args = length us - actual_num_type_args
313 val ts = map (aux NONE []) (take num_term_args us @ args)
315 Const (c, if full_types then
317 SOME T => map fastype_of ts ---> T
319 if num_type_args = 0 then
320 Sign.const_instance thy (c, [])
322 raise Fail ("no type information for " ^ quote c)
324 (* Extra args from "hAPP" come after any arguments
325 given directly to the constant. *)
326 Sign.const_instance thy (c,
327 map (type_from_node tfrees)
328 (drop num_term_args us)))
329 in list_comb (t, ts) end
330 | NONE => (* a free or schematic variable *)
332 val ts = map (aux NONE []) (us @ args)
333 val T = map fastype_of ts ---> HOLogic.typeT
335 case strip_prefix fixed_var_prefix a of
336 SOME b => Free (b, T)
338 case strip_prefix schematic_var_prefix a of
339 SOME b => Var ((b, 0), T)
341 (* Variable from the ATP, say "X1" *)
342 Var ((fix_atp_variable_name a, 0), T)
343 in list_comb (t, ts) end
346 (* Type class literal applied to a type. Returns triple of polarity, class,
348 fun type_constraint_from_node pos tfrees (StrNode ("c_Not", [u])) =
349 type_constraint_from_node (not pos) tfrees u
350 | type_constraint_from_node pos tfrees u = case u of
351 IntLeaf _ => raise NODE [u]
353 (case (strip_prefix class_prefix a,
354 map (type_from_node tfrees) us) of
355 (SOME b, [T]) => (pos, b, T)
356 | _ => raise NODE [u])
358 (** Accumulate type constraints in a clause: negative type literals **)
360 fun add_var (key, z) = Vartab.map_default (key, []) (cons z)
362 fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl)
363 | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl)
364 | add_type_constraint _ = I
366 fun is_positive_literal (@{const Not} $ _) = false
367 | is_positive_literal t = true
369 fun negate_term thy (Const (@{const_name All}, T) $ Abs (s, T', t')) =
370 Const (@{const_name Ex}, T) $ Abs (s, T', negate_term thy t')
371 | negate_term thy (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
372 Const (@{const_name All}, T) $ Abs (s, T', negate_term thy t')
373 | negate_term thy (@{const "op -->"} $ t1 $ t2) =
374 @{const "op &"} $ t1 $ negate_term thy t2
375 | negate_term thy (@{const "op &"} $ t1 $ t2) =
376 @{const "op |"} $ negate_term thy t1 $ negate_term thy t2
377 | negate_term thy (@{const "op |"} $ t1 $ t2) =
378 @{const "op &"} $ negate_term thy t1 $ negate_term thy t2
379 | negate_term _ (@{const Not} $ t) = t
380 | negate_term _ t = @{const Not} $ t
382 fun clause_for_literals _ [] = HOLogic.false_const
383 | clause_for_literals _ [lit] = lit
384 | clause_for_literals thy lits =
385 case List.partition is_positive_literal lits of
386 (pos_lits as _ :: _, neg_lits as _ :: _) =>
388 $ foldr1 HOLogic.mk_conj (map (negate_term thy) neg_lits)
389 $ foldr1 HOLogic.mk_disj pos_lits
390 | _ => foldr1 HOLogic.mk_disj lits
392 (* Final treatment of the list of "real" literals from a clause.
393 No "real" literals means only type information. *)
394 fun finish_clause _ [] = HOLogic.true_const
395 | finish_clause thy lits =
396 lits |> filter_out (curry (op =) HOLogic.false_const) |> rev
397 |> clause_for_literals thy
399 (*Accumulate sort constraints in vt, with "real" literals in lits.*)
400 fun lits_of_nodes thy full_types tfrees =
402 fun aux (vt, lits) [] = (vt, finish_clause thy lits)
403 | aux (vt, lits) (u :: us) =
404 aux (add_type_constraint
405 (type_constraint_from_node true tfrees u) vt, lits) us
407 aux (vt, term_from_node thy full_types tfrees (SOME @{typ bool})
411 (* Update TVars with detected sort constraints. It's not totally clear when
412 this code is necessary. *)
413 fun repair_tvar_sorts vt =
415 fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
416 | do_type (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi))
417 | do_type (TFree z) = TFree z
418 fun do_term (Const (a, T)) = Const (a, do_type T)
419 | do_term (Free (a, T)) = Free (a, do_type T)
420 | do_term (Var (xi, T)) = Var (xi, do_type T)
421 | do_term (t as Bound _) = t
422 | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t)
423 | do_term (t1 $ t2) = do_term t1 $ do_term t2
424 in not (Vartab.is_empty vt) ? do_term end
426 fun unskolemize_term t =
428 |> filter (is_skolem_const_name o fst) |> map Const
429 |> rpair t |-> fold forall_of
431 val combinator_table =
432 [(@{const_name COMBI}, @{thm COMBI_def_raw}),
433 (@{const_name COMBK}, @{thm COMBK_def_raw}),
434 (@{const_name COMBB}, @{thm COMBB_def_raw}),
435 (@{const_name COMBC}, @{thm COMBC_def_raw}),
436 (@{const_name COMBS}, @{thm COMBS_def_raw})]
438 fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2))
439 | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t')
440 | uncombine_term (t as Const (x as (s, _))) =
441 (case AList.lookup (op =) combinator_table s of
442 SOME thm => thm |> prop_of |> specialize_type @{theory} x |> Logic.dest_equals |> snd
444 | uncombine_term t = t
446 (* Interpret a list of syntax trees as a clause, given by "real" literals and
447 sort constraints. "vt" holds the initial sort constraints, from the
448 conjecture clauses. *)
449 fun clause_of_nodes ctxt full_types tfrees us =
451 val thy = ProofContext.theory_of ctxt
452 val (vt, t) = lits_of_nodes thy full_types tfrees (Vartab.empty, []) us
453 in repair_tvar_sorts vt t end
454 fun check_formula ctxt =
455 Type_Infer.constrain @{typ bool}
456 #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
459 (**** Translation of TSTP files to Isar Proofs ****)
461 fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
462 | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
464 fun decode_line full_types tfrees (Definition (num, u, us)) ctxt =
466 val t1 = clause_of_nodes ctxt full_types tfrees [u]
467 val vars = snd (strip_comb t1)
468 val frees = map unvarify_term vars
469 val unvarify_args = subst_atomic (vars ~~ frees)
470 val t2 = clause_of_nodes ctxt full_types tfrees us
472 HOLogic.eq_const HOLogic.typeT $ t1 $ t2
473 |> unvarify_args |> uncombine_term |> check_formula ctxt
476 (Definition (num, t1, t2),
477 fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
479 | decode_line full_types tfrees (Inference (num, us, deps)) ctxt =
481 val t = us |> clause_of_nodes ctxt full_types tfrees
482 |> unskolemize_term |> uncombine_term |> check_formula ctxt
484 (Inference (num, t, deps),
485 fold Variable.declare_term (OldTerm.term_frees t) ctxt)
487 fun decode_lines ctxt full_types tfrees lines =
488 fst (fold_map (decode_line full_types tfrees) lines ctxt)
490 fun aint_inference _ (Definition _) = true
491 | aint_inference t (Inference (_, t', _)) = not (t aconv t')
493 (* No "real" literals means only type information (tfree_tcs, clsrel, or
495 val is_only_type_information = curry (op aconv) HOLogic.true_const
497 fun replace_one_dep (old, new) dep = if dep = old then new else [dep]
498 fun replace_deps_in_line _ (line as Definition _) = line
499 | replace_deps_in_line p (Inference (num, t, deps)) =
500 Inference (num, t, fold (union (op =) o replace_one_dep p) deps [])
502 (*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ
503 only in type information.*)
504 fun add_line _ _ (line as Definition _) lines = line :: lines
505 | add_line conjecture_shape thm_names (Inference (num, t, [])) lines =
506 (* No dependencies: axiom, conjecture clause, or internal axioms or
507 definitions (Vampire). *)
508 if is_axiom_clause_number thm_names num then
509 (* Axioms are not proof lines. *)
510 if is_only_type_information t then
511 map (replace_deps_in_line (num, [])) lines
512 (* Is there a repetition? If so, replace later line by earlier one. *)
513 else case take_prefix (aint_inference t) lines of
514 (_, []) => lines (*no repetition of proof line*)
515 | (pre, Inference (num', _, _) :: post) =>
516 pre @ map (replace_deps_in_line (num', [num])) post
517 else if is_conjecture_clause_number conjecture_shape num then
518 Inference (num, t, []) :: lines
520 map (replace_deps_in_line (num, [])) lines
521 | add_line _ _ (Inference (num, t, deps)) lines =
522 (* Type information will be deleted later; skip repetition test. *)
523 if is_only_type_information t then
524 Inference (num, t, deps) :: lines
525 (* Is there a repetition? If so, replace later line by earlier one. *)
526 else case take_prefix (aint_inference t) lines of
527 (* FIXME: Doesn't this code risk conflating proofs involving different
529 (_, []) => Inference (num, t, deps) :: lines
530 | (pre, Inference (num', t', _) :: post) =>
531 Inference (num, t', deps) ::
532 pre @ map (replace_deps_in_line (num', [num])) post
534 (* Recursively delete empty lines (type information) from the proof. *)
535 fun add_nontrivial_line (Inference (num, t, [])) lines =
536 if is_only_type_information t then delete_dep num lines
537 else Inference (num, t, []) :: lines
538 | add_nontrivial_line line lines = line :: lines
539 and delete_dep num lines =
540 fold_rev add_nontrivial_line (map (replace_deps_in_line (num, [])) lines) []
542 (* ATPs sometimes reuse free variable names in the strangest ways. Surprisingly,
543 removing the offending lines often does the trick. *)
544 fun is_bad_free frees (Free x) = not (member (op =) frees x)
545 | is_bad_free _ _ = false
547 (* Vampire is keen on producing these. *)
548 fun is_trivial_formula (@{const Not} $ (Const (@{const_name "op ="}, _)
549 $ t1 $ t2)) = (t1 aconv t2)
550 | is_trivial_formula t = false
552 fun add_desired_line _ _ _ _ _ (line as Definition _) (j, lines) =
554 | add_desired_line ctxt isar_shrink_factor conjecture_shape thm_names frees
555 (Inference (num, t, deps)) (j, lines) =
557 if is_axiom_clause_number thm_names num orelse
558 is_conjecture_clause_number conjecture_shape num orelse
559 (not (is_only_type_information t) andalso
560 null (Term.add_tvars t []) andalso
561 not (exists_subterm (is_bad_free frees) t) andalso
562 not (is_trivial_formula t) andalso
563 (null lines orelse (* last line must be kept *)
564 (length deps >= 2 andalso j mod isar_shrink_factor = 0))) then
565 Inference (num, t, deps) :: lines (* keep line *)
567 map (replace_deps_in_line (num, deps)) lines) (* drop line *)
569 (** EXTRACTING LEMMAS **)
571 (* A list consisting of the first number in each line is returned.
572 TSTP: Interesting lines have the form "cnf(108, axiom, ...)", where the
573 number (108) is extracted.
574 SPASS: Lines have the form "108[0:Inp] ...", where the first number (108) is
576 fun extract_clause_numbers_in_atp_proof atp_proof =
578 val tokens_of = String.tokens (not o is_ident_char)
579 fun extract_num ("cnf" :: num :: "axiom" :: _) = Int.fromString num
580 | extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num
581 | extract_num _ = NONE
582 in atp_proof |> split_lines |> map_filter (extract_num o tokens_of) end
584 fun apply_command _ 1 = "by "
585 | apply_command 1 _ = "apply "
586 | apply_command i _ = "prefer " ^ string_of_int i ^ " apply "
587 fun metis_command i n [] = apply_command i n ^ "metis"
588 | metis_command i n ss =
589 apply_command i n ^ "(metis " ^ space_implode " " ss ^ ")"
590 fun metis_line i n xs =
591 "Try this command: " ^
592 Markup.markup Markup.sendback (metis_command i n xs) ^ ".\n"
593 fun minimize_line _ [] = ""
594 | minimize_line minimize_command facts =
595 case minimize_command facts of
598 "To minimize the number of lemmas, try this command: " ^
599 Markup.markup Markup.sendback command ^ ".\n"
601 val unprefix_chained = perhaps (try (unprefix chained_prefix))
603 fun metis_proof_text (minimize_command, atp_proof, thm_names, goal, i) =
606 atp_proof |> extract_clause_numbers_in_atp_proof
607 |> filter (is_axiom_clause_number thm_names)
608 |> map (fn i => Vector.sub (thm_names, i - 1))
609 val (chained_lemmas, other_lemmas) =
610 raw_lemmas |> List.partition (String.isPrefix chained_prefix)
611 |>> map (unprefix chained_prefix)
612 |> pairself (sort_distinct string_ord)
613 val lemmas = other_lemmas @ chained_lemmas
614 val n = Logic.count_prems (prop_of goal)
616 (metis_line i n other_lemmas ^ minimize_line minimize_command lemmas,
620 (** Isar proof construction and manipulation **)
622 fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
623 (union (op =) ls1 ls2, union (op =) ss1 ss2)
625 type label = string * int
626 type facts = label list * string list
628 datatype qualifier = Show | Then | Moreover | Ultimately
631 Fix of (string * typ) list |
633 Assume of label * term |
634 Have of qualifier list * label * term * byline
637 CaseSplit of step list list * facts
639 fun smart_case_split [] facts = ByMetis facts
640 | smart_case_split proofs facts = CaseSplit (proofs, facts)
643 val assum_prefix = "A"
644 val fact_prefix = "F"
646 fun string_for_label (s, num) = s ^ string_of_int num
648 fun add_fact_from_dep thm_names num =
649 if is_axiom_clause_number thm_names num then
650 apsnd (insert (op =) (Vector.sub (thm_names, num - 1)))
652 apfst (insert (op =) (raw_prefix, num))
654 fun forall_vars t = fold_rev forall_of (map Var (Term.add_vars t [])) t
656 fun step_for_line _ _ (Definition (num, t1, t2)) = Let (t1, t2)
657 | step_for_line _ _ (Inference (num, t, [])) = Assume ((raw_prefix, num), t)
658 | step_for_line thm_names j (Inference (num, t, deps)) =
659 Have (if j = 1 then [Show] else [], (raw_prefix, num),
661 ByMetis (fold (add_fact_from_dep thm_names) deps ([], [])))
663 fun proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
664 atp_proof conjecture_shape thm_names params frees =
667 atp_proof ^ "$" (* the $ sign acts as a sentinel *)
669 |> decode_lines ctxt full_types tfrees
670 |> rpair [] |-> fold_rev (add_line conjecture_shape thm_names)
671 |> rpair [] |-> fold_rev add_nontrivial_line
672 |> rpair (0, []) |-> fold_rev (add_desired_line ctxt isar_shrink_factor
673 conjecture_shape thm_names frees)
676 (if null params then [] else [Fix params]) @
677 map2 (step_for_line thm_names) (length lines downto 1) lines
681 val no_label = ("", ~1)
683 fun no_show qs = not (member (op =) qs Show)
685 (* When redirecting proofs, we keep information about the labels seen so far in
686 the "backpatches" data structure. The first component indicates which facts
687 should be associated with forthcoming proof steps. The second component is a
688 pair ("keep_ls", "drop_ls"), where "keep_ls" are the labels to keep and
689 "drop_ls" are those that should be dropped in a case split. *)
690 type backpatches = (label * facts) list * (label list * label list)
692 fun used_labels_of_step (Have (_, _, _, by)) =
694 ByMetis (ls, _) => ls
695 | CaseSplit (proofs, (ls, _)) =>
696 fold (union (op =) o used_labels_of) proofs ls)
697 | used_labels_of_step _ = []
698 and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []
700 fun new_labels_of_step (Fix _) = []
701 | new_labels_of_step (Let _) = []
702 | new_labels_of_step (Assume (l, _)) = [l]
703 | new_labels_of_step (Have (_, l, _, _)) = [l]
704 val new_labels_of = maps new_labels_of_step
709 | aux proof_tail (proofs as (proof1 :: _)) =
710 if exists null proofs then
712 else if forall (curry (op =) (hd proof1) o hd) (tl proofs) then
713 aux (hd proof1 :: proof_tail) (map tl proofs)
714 else case hd proof1 of
715 Have ([], l, t, by) =>
716 if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t')
717 | _ => false) (tl proofs) andalso
718 not (exists (member (op =) (maps new_labels_of proofs))
719 (used_labels_of proof_tail)) then
720 SOME (l, t, map rev proofs, proof_tail)
724 in aux [] o map rev end
726 fun case_split_qualifiers proofs =
727 case length proofs of
732 fun redirect_proof thy conjecture_shape hyp_ts concl_t proof =
734 val concl_ls = map (pair raw_prefix) (List.last conjecture_shape)
735 fun find_hyp num = nth hyp_ts (index_in_shape num conjecture_shape)
736 fun first_pass ([], contra) = ([], contra)
737 | first_pass ((step as Fix _) :: proof, contra) =
738 first_pass (proof, contra) |>> cons step
739 | first_pass ((step as Let _) :: proof, contra) =
740 first_pass (proof, contra) |>> cons step
741 | first_pass ((step as Assume (l as (_, num), t)) :: proof, contra) =
742 if member (op =) concl_ls l then
743 first_pass (proof, contra ||> cons step)
745 first_pass (proof, contra) |>> cons (Assume (l, find_hyp num))
746 | first_pass ((step as Have (qs, l, t, ByMetis (ls, ss))) :: proof,
748 if exists (member (op =) (fst contra)) ls then
749 first_pass (proof, contra |>> cons l ||> cons step)
751 first_pass (proof, contra) |>> cons step
752 | first_pass _ = raise Fail "malformed proof"
753 val (proof_top, (contra_ls, contra_proof)) =
754 first_pass (proof, (concl_ls, []))
755 val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst
756 fun backpatch_labels patches ls =
757 fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
758 fun second_pass end_qs ([], assums, patches) =
759 ([Have (end_qs, no_label,
760 if length assums < length concl_ls then
761 clause_for_literals thy (map (negate_term thy o fst) assums)
764 ByMetis (backpatch_labels patches (map snd assums)))], patches)
765 | second_pass end_qs (Assume (l, t) :: proof, assums, patches) =
766 second_pass end_qs (proof, (t, l) :: assums, patches)
767 | second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums,
769 if member (op =) (snd (snd patches)) l andalso
770 not (AList.defined (op =) (fst patches) l) then
771 second_pass end_qs (proof, assums, patches ||> apsnd (append ls))
773 (case List.partition (member (op =) contra_ls) ls of
774 ([contra_l], co_ls) =>
778 patches |>> cons (contra_l, (l :: co_ls, ss)))
779 |>> cons (if member (op =) (fst (snd patches)) l then
780 Assume (l, negate_term thy t)
782 Have (qs, l, negate_term thy t,
783 ByMetis (backpatch_label patches l)))
785 second_pass end_qs (proof, assums,
786 patches |>> cons (contra_l, (co_ls, ss)))
787 | (contra_ls as _ :: _, co_ls) =>
792 if member (op =) concl_ls l then
796 val drop_ls = filter (curry (op <>) l) contra_ls
800 patches ||> apfst (insert (op =) l)
801 ||> apsnd (union (op =) drop_ls))
804 val facts = (co_ls, [])
806 (case join_proofs proofs of
807 SOME (l, t, proofs, proof_tail) =>
808 Have (case_split_qualifiers proofs @
809 (if null proof_tail then end_qs else []), l, t,
810 smart_case_split proofs facts) :: proof_tail
812 [Have (case_split_qualifiers proofs @ end_qs, no_label,
813 concl_t, smart_case_split proofs facts)],
816 | _ => raise Fail "malformed proof")
817 | second_pass _ _ = raise Fail "malformed proof"
819 second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst
820 in proof_top @ proof_bottom end
822 val kill_duplicate_assumptions_in_proof =
824 fun relabel_facts subst =
825 apfst (map (fn l => AList.lookup (op =) subst l |> the_default l))
826 fun do_step (step as Assume (l, t)) (proof, subst, assums) =
827 (case AList.lookup (op aconv) assums t of
828 SOME l' => (proof, (l, l') :: subst, assums)
829 | NONE => (step :: proof, subst, (t, l) :: assums))
830 | do_step (Have (qs, l, t, by)) (proof, subst, assums) =
833 ByMetis facts => ByMetis (relabel_facts subst facts)
834 | CaseSplit (proofs, facts) =>
835 CaseSplit (map do_proof proofs, relabel_facts subst facts)) ::
836 proof, subst, assums)
837 | do_step step (proof, subst, assums) = (step :: proof, subst, assums)
838 and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
841 val then_chain_proof =
844 | aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof
845 | aux l' (Have (qs, l, t, by) :: proof) =
848 Have (if member (op =) ls l' then
850 ByMetis (filter_out (curry (op =) l') ls, ss))
852 (qs, l, t, ByMetis (ls, ss)))
853 | CaseSplit (proofs, facts) =>
854 Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) ::
856 | aux _ (step :: proof) = step :: aux no_label proof
859 fun kill_useless_labels_in_proof proof =
861 val used_ls = used_labels_of proof
862 fun do_label l = if member (op =) used_ls l then l else no_label
863 fun do_step (Assume (l, t)) = Assume (do_label l, t)
864 | do_step (Have (qs, l, t, by)) =
865 Have (qs, do_label l, t,
867 CaseSplit (proofs, facts) =>
868 CaseSplit (map (map do_step) proofs, facts)
870 | do_step step = step
871 in map do_step proof end
873 fun prefix_for_depth n = replicate_string (n + 1)
877 fun aux _ _ _ [] = []
878 | aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) =
880 Assume (l, t) :: aux subst depth (next_assum, next_fact) proof
882 let val l' = (prefix_for_depth depth assum_prefix, next_assum) in
884 aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof
886 | aux subst depth (next_assum, next_fact) (Have (qs, l, t, by) :: proof) =
888 val (l', subst, next_fact) =
890 (l, subst, next_fact)
893 val l' = (prefix_for_depth depth fact_prefix, next_fact)
894 in (l', (l, l') :: subst, next_fact + 1) end
897 case AList.lookup (op =) subst l of
899 | NONE => raise Fail ("unknown label " ^
900 quote (string_for_label l))))
903 ByMetis facts => ByMetis (relabel_facts facts)
904 | CaseSplit (proofs, facts) =>
905 CaseSplit (map (aux subst (depth + 1) (1, 1)) proofs,
908 Have (qs, l', t, by) ::
909 aux subst depth (next_assum, next_fact) proof
911 | aux subst depth nextp (step :: proof) =
912 step :: aux subst depth nextp proof
913 in aux [] 0 (1, 1) end
915 fun string_for_proof ctxt i n =
917 fun fix_print_mode f x =
918 setmp_CRITICAL show_no_free_types true
919 (setmp_CRITICAL show_types true
920 (Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
921 (print_mode_value ())) f)) x
922 fun do_indent ind = replicate_string (ind * indent_size) " "
924 maybe_quote s ^ " :: " ^
925 maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
926 fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
928 (if member (op =) qs Moreover then "moreover " else "") ^
929 (if member (op =) qs Ultimately then "ultimately " else "") ^
930 (if member (op =) qs Then then
931 if member (op =) qs Show then "thus" else "hence"
933 if member (op =) qs Show then "show" else "have")
934 val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
935 fun do_facts (ls, ss) =
937 val ls = ls |> sort_distinct (prod_ord string_ord int_ord)
938 val ss = ss |> map unprefix_chained |> sort_distinct string_ord
939 in metis_command 1 1 (map string_for_label ls @ ss) end
940 and do_step ind (Fix xs) =
941 do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
942 | do_step ind (Let (t1, t2)) =
943 do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
944 | do_step ind (Assume (l, t)) =
945 do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
946 | do_step ind (Have (qs, l, t, ByMetis facts)) =
947 do_indent ind ^ do_have qs ^ " " ^
948 do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n"
949 | do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) =
950 space_implode (do_indent ind ^ "moreover\n")
951 (map (do_block ind) proofs) ^
952 do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^
953 do_facts facts ^ "\n"
954 and do_steps prefix suffix ind steps =
955 let val s = implode (map (do_step ind) steps) in
956 replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
957 String.extract (s, ind * indent_size,
958 SOME (size s - ind * indent_size - 1)) ^
961 and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
962 (* One-step proofs are pointless; better use the Metis one-liner
964 and do_proof [Have (_, _, _, ByMetis _)] = ""
966 (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
967 do_indent 0 ^ "proof -\n" ^
968 do_steps "" "" 1 proof ^
969 do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n"
972 fun isar_proof_text (pool, debug, full_types, isar_shrink_factor, ctxt,
974 (minimize_command, atp_proof, thm_names, goal, i) =
976 val thy = ProofContext.theory_of ctxt
977 val (params, hyp_ts, concl_t) = strip_subgoal goal i
978 val frees = fold Term.add_frees (concl_t :: hyp_ts) []
979 val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
980 val n = Logic.count_prems (prop_of goal)
981 val (one_line_proof, lemma_names) =
982 metis_proof_text (minimize_command, atp_proof, thm_names, goal, i)
983 fun isar_proof_for () =
984 case proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
985 atp_proof conjecture_shape thm_names params
987 |> redirect_proof thy conjecture_shape hyp_ts concl_t
988 |> kill_duplicate_assumptions_in_proof
990 |> kill_useless_labels_in_proof
992 |> string_for_proof ctxt i n of
994 | proof => "\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
999 try isar_proof_for ()
1000 |> the_default "Warning: The Isar proof construction failed.\n"
1001 in (one_line_proof ^ isar_proof, lemma_names) end
1003 fun proof_text isar_proof isar_params other_params =
1004 (if isar_proof then isar_proof_text isar_params else metis_proof_text)