renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
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 chained_hint: string
14 val invert_const: string -> string
15 val invert_type_const: string -> string
16 val num_type_args: theory -> string -> int
17 val strip_prefix: string -> string -> string option
18 val metis_line: int -> int -> string list -> string
20 minimize_command * string * string vector * thm * int
21 -> string * string list
23 name_pool option * bool * bool * int * Proof.context * int list list
24 -> minimize_command * string * string vector * thm * int
25 -> string * string list
27 bool -> name_pool option * bool * bool * int * Proof.context * int list list
28 -> minimize_command * string * string vector * thm * int
29 -> string * string list
32 structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
35 open Sledgehammer_Util
36 open Sledgehammer_FOL_Clause
37 open Sledgehammer_HOL_Clause
38 open Sledgehammer_Fact_Preprocessor
40 type minimize_command = string list -> string
42 fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
43 fun is_head_digit s = Char.isDigit (String.sub (s, 0))
45 (* Hack: Could return false positives (e.g., a user happens to declare a
46 constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
47 val is_skolem_const_name =
49 #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
51 val index_in_shape : int -> int list list -> int =
52 find_index o exists o curry (op =)
53 fun is_axiom_clause_number thm_names num = num <= Vector.length thm_names
54 fun is_conjecture_clause_number conjecture_shape num =
55 index_in_shape num conjecture_shape >= 0
57 fun ugly_name NONE s = s
58 | ugly_name (SOME the_pool) s =
59 case Symtab.lookup (snd the_pool) s of
63 fun smart_lambda v t =
66 List.last (space_explode skolem_infix (Long_Name.base_name s))
67 | Var ((s, _), _) => s
69 | _ => "", fastype_of v, abstract_over (v, t))
70 fun forall_of v t = HOLogic.all_const (fastype_of v) $ smart_lambda v t
72 datatype ('a, 'b, 'c, 'd, 'e) raw_step =
73 Definition of 'a * 'b * 'c |
74 Inference of 'a * 'd * 'e list
76 (**** PARSING OF TSTP FORMAT ****)
78 fun strip_spaces_in_list [] = ""
79 | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1
80 | strip_spaces_in_list [c1, c2] =
81 strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2]
82 | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) =
83 if Char.isSpace c1 then
84 strip_spaces_in_list (c2 :: c3 :: cs)
85 else if Char.isSpace c2 then
86 if Char.isSpace c3 then
87 strip_spaces_in_list (c1 :: c3 :: cs)
89 str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^
90 strip_spaces_in_list (c3 :: cs)
92 str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
93 val strip_spaces = strip_spaces_in_list o String.explode
95 (* Syntax trees, either term list or formulae *)
96 datatype node = IntLeaf of int | StrNode of string * node list
98 fun str_leaf s = StrNode (s, [])
100 fun scons (x, y) = StrNode ("cons", [x, y])
101 val slist_of = List.foldl scons (str_leaf "nil")
103 (*Strings enclosed in single quotes, e.g. filenames*)
104 val parse_quoted = $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode;
106 (*Integer constants, typically proof line numbers*)
107 val parse_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
109 val parse_dollar_name =
110 Scan.repeat ($$ "$") -- Symbol.scan_id >> (fn (ss, s) => implode ss ^ s)
112 (* needed for SPASS's output format *)
113 fun repair_name _ "$true" = "c_True"
114 | repair_name _ "$false" = "c_False"
115 | repair_name _ "$$e" = "c_equal" (* seen in Vampire 11 proofs *)
116 | repair_name _ "equal" = "c_equal" (* probably not needed *)
117 | repair_name pool s = ugly_name pool s
118 (* Generalized first-order terms, which include file names, numbers, etc. *)
119 (* The "x" argument is not strictly necessary, but without it Poly/ML loops
120 forever at compile time. *)
121 fun parse_term pool x =
122 (parse_quoted >> str_leaf
123 || parse_integer >> IntLeaf
124 || (parse_dollar_name >> repair_name pool)
125 -- Scan.optional ($$ "(" |-- parse_terms pool --| $$ ")") [] >> StrNode
126 || $$ "(" |-- parse_term pool --| $$ ")"
127 || $$ "[" |-- Scan.optional (parse_terms pool) [] --| $$ "]" >> slist_of) x
128 and parse_terms pool x =
129 (parse_term pool ::: Scan.repeat ($$ "," |-- parse_term pool)) x
131 fun negate_node u = StrNode ("c_Not", [u])
132 fun equate_nodes u1 u2 = StrNode ("c_equal", [u1, u2])
134 (* Apply equal or not-equal to a term. *)
135 fun repair_predicate_term (u, NONE) = u
136 | repair_predicate_term (u1, SOME (NONE, u2)) = equate_nodes u1 u2
137 | repair_predicate_term (u1, SOME (SOME _, u2)) =
138 negate_node (equate_nodes u1 u2)
139 fun parse_predicate_term pool =
140 parse_term pool -- Scan.option (Scan.option ($$ "!") --| $$ "="
142 >> repair_predicate_term
143 fun parse_literal pool x =
144 ($$ "~" |-- parse_literal pool >> negate_node || parse_predicate_term pool) x
145 fun parse_literals pool =
146 parse_literal pool ::: Scan.repeat ($$ "|" |-- parse_literal pool)
147 fun parse_parenthesized_literals pool =
148 $$ "(" |-- parse_literals pool --| $$ ")" || parse_literals pool
149 fun parse_clause pool =
150 parse_parenthesized_literals pool
151 ::: Scan.repeat ($$ "|" |-- parse_parenthesized_literals pool)
154 fun ints_of_node (IntLeaf n) = cons n
155 | ints_of_node (StrNode (_, us)) = fold ints_of_node us
156 val parse_tstp_annotations =
157 Scan.optional ($$ "," |-- parse_term NONE
158 --| Scan.option ($$ "," |-- parse_terms NONE)
159 >> (fn source => ints_of_node source [])) []
161 fun parse_definition pool =
162 $$ "(" |-- parse_literal NONE --| Scan.this_string "<=>"
163 -- parse_clause pool --| $$ ")"
165 (* Syntax: cnf(<num>, <formula_role>, <cnf_formula> <annotations>).
166 The <num> could be an identifier, but we assume integers. *)
167 fun finish_tstp_definition_line (num, (u, us)) = Definition (num, u, us)
168 fun finish_tstp_inference_line ((num, us), deps) = Inference (num, us, deps)
169 fun parse_tstp_line pool =
170 ((Scan.this_string "fof" -- $$ "(") |-- parse_integer --| $$ ","
171 --| Scan.this_string "definition" --| $$ "," -- parse_definition pool
172 --| parse_tstp_annotations --| $$ ")" --| $$ "."
173 >> finish_tstp_definition_line)
174 || ((Scan.this_string "cnf" -- $$ "(") |-- parse_integer --| $$ ","
175 --| Symbol.scan_id --| $$ "," -- parse_clause pool
176 -- parse_tstp_annotations --| $$ ")" --| $$ "."
177 >> finish_tstp_inference_line)
179 (**** PARSING OF SPASS OUTPUT ****)
181 (* SPASS returns clause references of the form "x.y". We ignore "y", whose role
182 is not clear anyway. *)
183 val parse_dot_name = parse_integer --| $$ "." --| parse_integer
185 val parse_spass_annotations =
186 Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name
187 --| Scan.option ($$ ","))) []
189 (* It is not clear why some literals are followed by sequences of stars and/or
190 pluses. We ignore them. *)
191 fun parse_decorated_predicate_term pool =
192 parse_predicate_term pool --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")
194 fun parse_horn_clause pool =
195 Scan.repeat (parse_decorated_predicate_term pool) --| $$ "|" --| $$ "|"
196 -- Scan.repeat (parse_decorated_predicate_term pool) --| $$ "-" --| $$ ">"
197 -- Scan.repeat (parse_decorated_predicate_term pool)
198 >> (fn (([], []), []) => [str_leaf "c_False"]
199 | ((clauses1, clauses2), clauses3) =>
200 map negate_node (clauses1 @ clauses2) @ clauses3)
202 (* Syntax: <num>[0:<inference><annotations>]
203 <cnf_formulas> || <cnf_formulas> -> <cnf_formulas>. *)
204 fun finish_spass_line ((num, deps), us) = Inference (num, us, deps)
205 fun parse_spass_line pool =
206 parse_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
207 -- parse_spass_annotations --| $$ "]" -- parse_horn_clause pool --| $$ "."
210 fun parse_line pool = parse_tstp_line pool || parse_spass_line pool
211 fun parse_lines pool = Scan.repeat1 (parse_line pool)
212 fun parse_proof pool =
213 fst o Scan.finite Symbol.stopper
214 (Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
216 o explode o strip_spaces
218 (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
220 exception NODE of node list
222 (*If string s has the prefix s1, return the result of deleting it.*)
223 fun strip_prefix s1 s =
224 if String.isPrefix s1 s
225 then SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
228 (*Invert the table of translations between Isabelle and ATPs*)
229 val type_const_trans_table_inv =
230 Symtab.make (map swap (Symtab.dest type_const_trans_table));
232 fun invert_type_const c =
233 case Symtab.lookup type_const_trans_table_inv c of
237 (* Type variables are given the basic sort "HOL.type". Some will later be
238 constrained by information from type literals, or by type inference. *)
239 fun type_from_node _ (u as IntLeaf _) = raise NODE [u]
240 | type_from_node tfrees (u as StrNode (a, us)) =
241 let val Ts = map (type_from_node tfrees) us in
242 case strip_prefix tconst_prefix a of
243 SOME b => Type (invert_type_const b, Ts)
245 if not (null us) then
246 raise NODE [u] (* only "tconst"s have type arguments *)
247 else case strip_prefix tfree_prefix a of
249 let val s = "'" ^ b in
250 TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
253 case strip_prefix tvar_prefix a of
254 SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
256 (* Variable from the ATP, say "X1" *)
257 Type_Infer.param 0 (a, HOLogic.typeS)
260 (*Invert the table of translations between Isabelle and ATPs*)
261 val const_trans_table_inv =
262 Symtab.update ("fequal", @{const_name "op ="})
263 (Symtab.make (map swap (Symtab.dest const_trans_table)))
265 fun invert_const c = c |> Symtab.lookup const_trans_table_inv |> the_default c
267 (*The number of type arguments of a constant, zero if it's monomorphic*)
268 fun num_type_args thy s =
269 length (Sign.const_typargs thy (s, Sign.the_const_type thy s))
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 Sign.const_instance thy (c,
328 map (type_from_node tfrees)
329 (drop num_term_args us)))
330 in list_comb (t, ts) end
331 | NONE => (* a free or schematic variable *)
333 val ts = map (aux NONE []) (us @ args)
334 val T = map fastype_of ts ---> HOLogic.typeT
336 case strip_prefix fixed_var_prefix a of
337 SOME b => Free (b, T)
339 case strip_prefix schematic_var_prefix a of
340 SOME b => Var ((b, 0), T)
342 (* Variable from the ATP, say "X1" *)
343 Var ((fix_atp_variable_name a, 0), T)
344 in list_comb (t, ts) end
347 (* Type class literal applied to a type. Returns triple of polarity, class,
349 fun type_constraint_from_node pos tfrees (StrNode ("c_Not", [u])) =
350 type_constraint_from_node (not pos) tfrees u
351 | type_constraint_from_node pos tfrees u = case u of
352 IntLeaf _ => raise NODE [u]
354 (case (strip_prefix class_prefix a,
355 map (type_from_node tfrees) us) of
356 (SOME b, [T]) => (pos, b, T)
357 | _ => raise NODE [u])
359 (** Accumulate type constraints in a clause: negative type literals **)
361 fun add_var (key, z) = Vartab.map_default (key, []) (cons z)
363 fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl)
364 | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl)
365 | add_type_constraint _ = I
367 fun is_positive_literal (@{const Not} $ _) = false
368 | is_positive_literal t = true
370 fun negate_term thy (Const (@{const_name All}, T) $ Abs (s, T', t')) =
371 Const (@{const_name Ex}, T) $ Abs (s, T', negate_term thy t')
372 | negate_term thy (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
373 Const (@{const_name All}, T) $ Abs (s, T', negate_term thy t')
374 | negate_term thy (@{const "op -->"} $ t1 $ t2) =
375 @{const "op &"} $ t1 $ negate_term thy t2
376 | negate_term thy (@{const "op &"} $ t1 $ t2) =
377 @{const "op |"} $ negate_term thy t1 $ negate_term thy t2
378 | negate_term thy (@{const "op |"} $ t1 $ t2) =
379 @{const "op &"} $ negate_term thy t1 $ negate_term thy t2
380 | negate_term _ (@{const Not} $ t) = t
381 | negate_term _ t = @{const Not} $ t
383 fun clause_for_literals _ [] = HOLogic.false_const
384 | clause_for_literals _ [lit] = lit
385 | clause_for_literals thy lits =
386 case List.partition is_positive_literal lits of
387 (pos_lits as _ :: _, neg_lits as _ :: _) =>
389 $ foldr1 HOLogic.mk_conj (map (negate_term thy) neg_lits)
390 $ foldr1 HOLogic.mk_disj pos_lits
391 | _ => foldr1 HOLogic.mk_disj lits
393 (* Final treatment of the list of "real" literals from a clause.
394 No "real" literals means only type information. *)
395 fun finish_clause _ [] = HOLogic.true_const
396 | finish_clause thy lits =
397 lits |> filter_out (curry (op =) HOLogic.false_const) |> rev
398 |> clause_for_literals thy
400 (*Accumulate sort constraints in vt, with "real" literals in lits.*)
401 fun lits_of_nodes thy full_types tfrees =
403 fun aux (vt, lits) [] = (vt, finish_clause thy lits)
404 | aux (vt, lits) (u :: us) =
405 aux (add_type_constraint
406 (type_constraint_from_node true tfrees u) vt, lits) us
408 aux (vt, term_from_node thy full_types tfrees (SOME @{typ bool})
412 (* Update TVars with detected sort constraints. It's not totally clear when
413 this code is necessary. *)
414 fun repair_tvar_sorts vt =
416 fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
417 | do_type (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi))
418 | do_type (TFree z) = TFree z
419 fun do_term (Const (a, T)) = Const (a, do_type T)
420 | do_term (Free (a, T)) = Free (a, do_type T)
421 | do_term (Var (xi, T)) = Var (xi, do_type T)
422 | do_term (t as Bound _) = t
423 | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t)
424 | do_term (t1 $ t2) = do_term t1 $ do_term t2
425 in not (Vartab.is_empty vt) ? do_term end
427 fun unskolemize_term t =
429 |> filter (is_skolem_const_name o fst) |> map Const
430 |> rpair t |-> fold forall_of
432 val combinator_table =
433 [(@{const_name COMBI}, @{thm COMBI_def_raw}),
434 (@{const_name COMBK}, @{thm COMBK_def_raw}),
435 (@{const_name COMBB}, @{thm COMBB_def_raw}),
436 (@{const_name COMBC}, @{thm COMBC_def_raw}),
437 (@{const_name COMBS}, @{thm COMBS_def_raw})]
439 fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2))
440 | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t')
441 | uncombine_term (t as Const (x as (s, _))) =
442 (case AList.lookup (op =) combinator_table s of
443 SOME thm => thm |> prop_of |> specialize_type @{theory} x |> Logic.dest_equals |> snd
445 | uncombine_term t = t
447 (* Interpret a list of syntax trees as a clause, given by "real" literals and
448 sort constraints. "vt" holds the initial sort constraints, from the
449 conjecture clauses. *)
450 fun clause_of_nodes ctxt full_types tfrees us =
452 val thy = ProofContext.theory_of ctxt
453 val (vt, t) = lits_of_nodes thy full_types tfrees (Vartab.empty, []) us
454 in repair_tvar_sorts vt t end
455 fun check_formula ctxt =
456 Type_Infer.constrain @{typ bool}
457 #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
460 (**** Translation of TSTP files to Isar Proofs ****)
462 fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
463 | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
465 fun decode_line full_types tfrees (Definition (num, u, us)) ctxt =
467 val t1 = clause_of_nodes ctxt full_types tfrees [u]
468 val vars = snd (strip_comb t1)
469 val frees = map unvarify_term vars
470 val unvarify_args = subst_atomic (vars ~~ frees)
471 val t2 = clause_of_nodes ctxt full_types tfrees us
473 HOLogic.eq_const HOLogic.typeT $ t1 $ t2
474 |> unvarify_args |> uncombine_term |> check_formula ctxt
477 (Definition (num, t1, t2),
478 fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
480 | decode_line full_types tfrees (Inference (num, us, deps)) ctxt =
482 val t = us |> clause_of_nodes ctxt full_types tfrees
483 |> unskolemize_term |> uncombine_term |> check_formula ctxt
485 (Inference (num, t, deps),
486 fold Variable.declare_term (OldTerm.term_frees t) ctxt)
488 fun decode_lines ctxt full_types tfrees lines =
489 fst (fold_map (decode_line full_types tfrees) lines ctxt)
491 fun aint_inference _ (Definition _) = true
492 | aint_inference t (Inference (_, t', _)) = not (t aconv t')
494 (* No "real" literals means only type information (tfree_tcs, clsrel, or
496 val is_only_type_information = curry (op aconv) HOLogic.true_const
498 fun replace_one_dep (old, new) dep = if dep = old then new else [dep]
499 fun replace_deps_in_line _ (line as Definition _) = line
500 | replace_deps_in_line p (Inference (num, t, deps)) =
501 Inference (num, t, fold (union (op =) o replace_one_dep p) deps [])
503 (*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ
504 only in type information.*)
505 fun add_line _ _ (line as Definition _) lines = line :: lines
506 | add_line conjecture_shape thm_names (Inference (num, t, [])) lines =
507 (* No dependencies: axiom, conjecture clause, or internal axioms or
508 definitions (Vampire). *)
509 if is_axiom_clause_number thm_names num then
510 (* Axioms are not proof lines. *)
511 if is_only_type_information t then
512 map (replace_deps_in_line (num, [])) lines
513 (* Is there a repetition? If so, replace later line by earlier one. *)
514 else case take_prefix (aint_inference t) lines of
515 (_, []) => lines (*no repetition of proof line*)
516 | (pre, Inference (num', _, _) :: post) =>
517 pre @ map (replace_deps_in_line (num', [num])) post
518 else if is_conjecture_clause_number conjecture_shape num then
519 Inference (num, t, []) :: lines
521 map (replace_deps_in_line (num, [])) lines
522 | add_line _ _ (Inference (num, t, deps)) lines =
523 (* Type information will be deleted later; skip repetition test. *)
524 if is_only_type_information t then
525 Inference (num, t, deps) :: lines
526 (* Is there a repetition? If so, replace later line by earlier one. *)
527 else case take_prefix (aint_inference t) lines of
528 (* FIXME: Doesn't this code risk conflating proofs involving different
530 (_, []) => Inference (num, t, deps) :: lines
531 | (pre, Inference (num', t', _) :: post) =>
532 Inference (num, t', deps) ::
533 pre @ map (replace_deps_in_line (num', [num])) post
535 (* Recursively delete empty lines (type information) from the proof. *)
536 fun add_nontrivial_line (Inference (num, t, [])) lines =
537 if is_only_type_information t then delete_dep num lines
538 else Inference (num, t, []) :: lines
539 | add_nontrivial_line line lines = line :: lines
540 and delete_dep num lines =
541 fold_rev add_nontrivial_line (map (replace_deps_in_line (num, [])) lines) []
543 (* ATPs sometimes reuse free variable names in the strangest ways. Surprisingly,
544 removing the offending lines often does the trick. *)
545 fun is_bad_free frees (Free x) = not (member (op =) frees x)
546 | is_bad_free _ _ = false
548 (* Vampire is keen on producing these. *)
549 fun is_trivial_formula (@{const Not} $ (Const (@{const_name "op ="}, _)
550 $ t1 $ t2)) = (t1 aconv t2)
551 | is_trivial_formula t = false
553 fun add_desired_line _ _ _ _ _ (line as Definition _) (j, lines) =
555 | add_desired_line ctxt isar_shrink_factor conjecture_shape thm_names frees
556 (Inference (num, t, deps)) (j, lines) =
558 if is_axiom_clause_number thm_names num orelse
559 is_conjecture_clause_number conjecture_shape num orelse
560 (not (is_only_type_information t) andalso
561 null (Term.add_tvars t []) andalso
562 not (exists_subterm (is_bad_free frees) t) andalso
563 not (is_trivial_formula t) andalso
564 (null lines orelse (* last line must be kept *)
565 (length deps >= 2 andalso j mod isar_shrink_factor = 0))) then
566 Inference (num, t, deps) :: lines (* keep line *)
568 map (replace_deps_in_line (num, deps)) lines) (* drop line *)
570 (** EXTRACTING LEMMAS **)
572 (* A list consisting of the first number in each line is returned.
573 TSTP: Interesting lines have the form "cnf(108, axiom, ...)", where the
574 number (108) is extracted.
575 SPASS: Lines have the form "108[0:Inp] ...", where the first number (108) is
577 fun extract_clause_numbers_in_atp_proof atp_proof =
579 val tokens_of = String.tokens (not o is_ident_char)
580 fun extract_num ("cnf" :: num :: "axiom" :: _) = Int.fromString num
581 | extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num
582 | extract_num _ = NONE
583 in atp_proof |> split_lines |> map_filter (extract_num o tokens_of) end
585 (* Used to label theorems chained into the goal. *)
586 val chained_hint = "sledgehammer_chained"
588 fun apply_command _ 1 = "by "
589 | apply_command 1 _ = "apply "
590 | apply_command i _ = "prefer " ^ string_of_int i ^ " apply "
591 fun metis_command i n [] = apply_command i n ^ "metis"
592 | metis_command i n ss =
593 apply_command i n ^ "(metis " ^ space_implode " " ss ^ ")"
594 fun metis_line i n xs =
595 "Try this command: " ^
596 Markup.markup Markup.sendback (metis_command i n xs) ^ ".\n"
597 fun minimize_line _ [] = ""
598 | minimize_line minimize_command facts =
599 case minimize_command facts of
602 "To minimize the number of lemmas, try this command: " ^
603 Markup.markup Markup.sendback command ^ ".\n"
605 fun metis_proof_text (minimize_command, atp_proof, thm_names, goal, i) =
608 atp_proof |> extract_clause_numbers_in_atp_proof
609 |> filter (is_axiom_clause_number thm_names)
610 |> map (fn i => Vector.sub (thm_names, i - 1))
611 |> filter_out (fn s => s = "??.unknown" orelse s = chained_hint)
612 |> sort_distinct string_ord
613 val n = Logic.count_prems (prop_of goal)
614 in (metis_line i n lemmas ^ minimize_line minimize_command lemmas, lemmas) end
616 (** Isar proof construction and manipulation **)
618 fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
619 (union (op =) ls1 ls2, union (op =) ss1 ss2)
621 type label = string * int
622 type facts = label list * string list
624 datatype qualifier = Show | Then | Moreover | Ultimately
627 Fix of (string * typ) list |
629 Assume of label * term |
630 Have of qualifier list * label * term * byline
633 CaseSplit of step list list * facts
635 fun smart_case_split [] facts = ByMetis facts
636 | smart_case_split proofs facts = CaseSplit (proofs, facts)
639 val assum_prefix = "A"
640 val fact_prefix = "F"
642 fun string_for_label (s, num) = s ^ string_of_int num
644 fun add_fact_from_dep thm_names num =
645 if is_axiom_clause_number thm_names num then
646 apsnd (insert (op =) (Vector.sub (thm_names, num - 1)))
648 apfst (insert (op =) (raw_prefix, num))
650 fun forall_vars t = fold_rev forall_of (map Var (Term.add_vars t [])) t
652 fun step_for_line _ _ (Definition (num, t1, t2)) = Let (t1, t2)
653 | step_for_line _ _ (Inference (num, t, [])) = Assume ((raw_prefix, num), t)
654 | step_for_line thm_names j (Inference (num, t, deps)) =
655 Have (if j = 1 then [Show] else [], (raw_prefix, num),
657 ByMetis (fold (add_fact_from_dep thm_names) deps ([], [])))
659 fun proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
660 atp_proof conjecture_shape thm_names params frees =
663 atp_proof ^ "$" (* the $ sign acts as a sentinel *)
665 |> decode_lines ctxt full_types tfrees
666 |> rpair [] |-> fold_rev (add_line conjecture_shape thm_names)
667 |> rpair [] |-> fold_rev add_nontrivial_line
668 |> rpair (0, []) |-> fold_rev (add_desired_line ctxt isar_shrink_factor
669 conjecture_shape thm_names frees)
672 (if null params then [] else [Fix params]) @
673 map2 (step_for_line thm_names) (length lines downto 1) lines
677 val no_label = ("", ~1)
679 fun no_show qs = not (member (op =) qs Show)
681 (* When redirecting proofs, we keep information about the labels seen so far in
682 the "backpatches" data structure. The first component indicates which facts
683 should be associated with forthcoming proof steps. The second component is a
684 pair ("keep_ls", "drop_ls"), where "keep_ls" are the labels to keep and
685 "drop_ls" are those that should be dropped in a case split. *)
686 type backpatches = (label * facts) list * (label list * label list)
688 fun used_labels_of_step (Have (_, _, _, by)) =
690 ByMetis (ls, _) => ls
691 | CaseSplit (proofs, (ls, _)) =>
692 fold (union (op =) o used_labels_of) proofs ls)
693 | used_labels_of_step _ = []
694 and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []
696 fun new_labels_of_step (Fix _) = []
697 | new_labels_of_step (Let _) = []
698 | new_labels_of_step (Assume (l, _)) = [l]
699 | new_labels_of_step (Have (_, l, _, _)) = [l]
700 val new_labels_of = maps new_labels_of_step
705 | aux proof_tail (proofs as (proof1 :: _)) =
706 if exists null proofs then
708 else if forall (curry (op =) (hd proof1) o hd) (tl proofs) then
709 aux (hd proof1 :: proof_tail) (map tl proofs)
710 else case hd proof1 of
711 Have ([], l, t, by) =>
712 if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t')
713 | _ => false) (tl proofs) andalso
714 not (exists (member (op =) (maps new_labels_of proofs))
715 (used_labels_of proof_tail)) then
716 SOME (l, t, map rev proofs, proof_tail)
720 in aux [] o map rev end
722 fun case_split_qualifiers proofs =
723 case length proofs of
728 fun redirect_proof thy conjecture_shape hyp_ts concl_t proof =
730 val concl_ls = map (pair raw_prefix) (List.last conjecture_shape)
731 fun find_hyp num = nth hyp_ts (index_in_shape num conjecture_shape)
732 fun first_pass ([], contra) = ([], contra)
733 | first_pass ((step as Fix _) :: proof, contra) =
734 first_pass (proof, contra) |>> cons step
735 | first_pass ((step as Let _) :: proof, contra) =
736 first_pass (proof, contra) |>> cons step
737 | first_pass ((step as Assume (l as (_, num), t)) :: proof, contra) =
738 if member (op =) concl_ls l then
739 first_pass (proof, contra ||> cons step)
741 first_pass (proof, contra) |>> cons (Assume (l, find_hyp num))
742 | first_pass ((step as Have (qs, l, t, ByMetis (ls, ss))) :: proof,
744 if exists (member (op =) (fst contra)) ls then
745 first_pass (proof, contra |>> cons l ||> cons step)
747 first_pass (proof, contra) |>> cons step
748 | first_pass _ = raise Fail "malformed proof"
749 val (proof_top, (contra_ls, contra_proof)) =
750 first_pass (proof, (concl_ls, []))
751 val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst
752 fun backpatch_labels patches ls =
753 fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
754 fun second_pass end_qs ([], assums, patches) =
755 ([Have (end_qs, no_label,
756 if length assums < length concl_ls then
757 clause_for_literals thy (map (negate_term thy o fst) assums)
760 ByMetis (backpatch_labels patches (map snd assums)))], patches)
761 | second_pass end_qs (Assume (l, t) :: proof, assums, patches) =
762 second_pass end_qs (proof, (t, l) :: assums, patches)
763 | second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums,
765 if member (op =) (snd (snd patches)) l andalso
766 not (AList.defined (op =) (fst patches) l) then
767 second_pass end_qs (proof, assums, patches ||> apsnd (append ls))
769 (case List.partition (member (op =) contra_ls) ls of
770 ([contra_l], co_ls) =>
774 patches |>> cons (contra_l, (l :: co_ls, ss)))
775 |>> cons (if member (op =) (fst (snd patches)) l then
776 Assume (l, negate_term thy t)
778 Have (qs, l, negate_term thy t,
779 ByMetis (backpatch_label patches l)))
781 second_pass end_qs (proof, assums,
782 patches |>> cons (contra_l, (co_ls, ss)))
783 | (contra_ls as _ :: _, co_ls) =>
788 if member (op =) concl_ls l then
792 val drop_ls = filter (curry (op <>) l) contra_ls
796 patches ||> apfst (insert (op =) l)
797 ||> apsnd (union (op =) drop_ls))
800 val facts = (co_ls, [])
802 (case join_proofs proofs of
803 SOME (l, t, proofs, proof_tail) =>
804 Have (case_split_qualifiers proofs @
805 (if null proof_tail then end_qs else []), l, t,
806 smart_case_split proofs facts) :: proof_tail
808 [Have (case_split_qualifiers proofs @ end_qs, no_label,
809 concl_t, smart_case_split proofs facts)],
812 | _ => raise Fail "malformed proof")
813 | second_pass _ _ = raise Fail "malformed proof"
815 second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst
816 in proof_top @ proof_bottom end
818 val kill_duplicate_assumptions_in_proof =
820 fun relabel_facts subst =
821 apfst (map (fn l => AList.lookup (op =) subst l |> the_default l))
822 fun do_step (step as Assume (l, t)) (proof, subst, assums) =
823 (case AList.lookup (op aconv) assums t of
824 SOME l' => (proof, (l, l') :: subst, assums)
825 | NONE => (step :: proof, subst, (t, l) :: assums))
826 | do_step (Have (qs, l, t, by)) (proof, subst, assums) =
829 ByMetis facts => ByMetis (relabel_facts subst facts)
830 | CaseSplit (proofs, facts) =>
831 CaseSplit (map do_proof proofs, relabel_facts subst facts)) ::
832 proof, subst, assums)
833 | do_step step (proof, subst, assums) = (step :: proof, subst, assums)
834 and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
837 val then_chain_proof =
840 | aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof
841 | aux l' (Have (qs, l, t, by) :: proof) =
844 Have (if member (op =) ls l' then
846 ByMetis (filter_out (curry (op =) l') ls, ss))
848 (qs, l, t, ByMetis (ls, ss)))
849 | CaseSplit (proofs, facts) =>
850 Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) ::
852 | aux _ (step :: proof) = step :: aux no_label proof
855 fun kill_useless_labels_in_proof proof =
857 val used_ls = used_labels_of proof
858 fun do_label l = if member (op =) used_ls l then l else no_label
859 fun do_step (Assume (l, t)) = Assume (do_label l, t)
860 | do_step (Have (qs, l, t, by)) =
861 Have (qs, do_label l, t,
863 CaseSplit (proofs, facts) =>
864 CaseSplit (map (map do_step) proofs, facts)
866 | do_step step = step
867 in map do_step proof end
869 fun prefix_for_depth n = replicate_string (n + 1)
873 fun aux _ _ _ [] = []
874 | aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) =
876 Assume (l, t) :: aux subst depth (next_assum, next_fact) proof
878 let val l' = (prefix_for_depth depth assum_prefix, next_assum) in
880 aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof
882 | aux subst depth (next_assum, next_fact) (Have (qs, l, t, by) :: proof) =
884 val (l', subst, next_fact) =
886 (l, subst, next_fact)
889 val l' = (prefix_for_depth depth fact_prefix, next_fact)
890 in (l', (l, l') :: subst, next_fact + 1) end
893 case AList.lookup (op =) subst l of
895 | NONE => raise Fail ("unknown label " ^
896 quote (string_for_label l))))
899 ByMetis facts => ByMetis (relabel_facts facts)
900 | CaseSplit (proofs, facts) =>
901 CaseSplit (map (aux subst (depth + 1) (1, 1)) proofs,
904 Have (qs, l', t, by) ::
905 aux subst depth (next_assum, next_fact) proof
907 | aux subst depth nextp (step :: proof) =
908 step :: aux subst depth nextp proof
909 in aux [] 0 (1, 1) end
911 fun string_for_proof ctxt i n =
913 fun fix_print_mode f =
914 PrintMode.setmp (filter (curry (op =) Symbol.xsymbolsN)
915 (print_mode_value ())) f
916 fun do_indent ind = replicate_string (ind * indent_size) " "
918 maybe_quote s ^ " :: " ^
919 maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
920 fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
922 (if member (op =) qs Moreover then "moreover " else "") ^
923 (if member (op =) qs Ultimately then "ultimately " else "") ^
924 (if member (op =) qs Then then
925 if member (op =) qs Show then "thus" else "hence"
927 if member (op =) qs Show then "show" else "have")
928 val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
929 fun do_facts (ls, ss) =
931 val ls = ls |> sort_distinct (prod_ord string_ord int_ord)
932 val ss = ss |> sort_distinct string_ord
933 in metis_command 1 1 (map string_for_label ls @ ss) end
934 and do_step ind (Fix xs) =
935 do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
936 | do_step ind (Let (t1, t2)) =
937 do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
938 | do_step ind (Assume (l, t)) =
939 do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
940 | do_step ind (Have (qs, l, t, ByMetis facts)) =
941 do_indent ind ^ do_have qs ^ " " ^
942 do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n"
943 | do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) =
944 space_implode (do_indent ind ^ "moreover\n")
945 (map (do_block ind) proofs) ^
946 do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^
947 do_facts facts ^ "\n"
948 and do_steps prefix suffix ind steps =
949 let val s = implode (map (do_step ind) steps) in
950 replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
951 String.extract (s, ind * indent_size,
952 SOME (size s - ind * indent_size - 1)) ^
955 and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
956 (* One-step proofs are pointless; better use the Metis one-liner
958 and do_proof [Have (_, _, _, ByMetis _)] = ""
960 (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
961 do_indent 0 ^ "proof -\n" ^
962 do_steps "" "" 1 proof ^
963 do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n"
966 fun isar_proof_text (pool, debug, full_types, isar_shrink_factor, ctxt,
968 (minimize_command, atp_proof, thm_names, goal, i) =
970 val thy = ProofContext.theory_of ctxt
971 val (params, hyp_ts, concl_t) = strip_subgoal goal i
972 val frees = fold Term.add_frees (concl_t :: hyp_ts) []
973 val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
974 val n = Logic.count_prems (prop_of goal)
975 val (one_line_proof, lemma_names) =
976 metis_proof_text (minimize_command, atp_proof, thm_names, goal, i)
977 fun isar_proof_for () =
978 case proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
979 atp_proof conjecture_shape thm_names params
981 |> redirect_proof thy conjecture_shape hyp_ts concl_t
982 |> kill_duplicate_assumptions_in_proof
984 |> kill_useless_labels_in_proof
986 |> string_for_proof ctxt i n of
988 | proof => "\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
993 try isar_proof_for ()
994 |> the_default "Warning: The Isar proof construction failed.\n"
995 in (one_line_proof ^ isar_proof, lemma_names) end
997 fun proof_text isar_proof isar_params other_params =
998 (if isar_proof then isar_proof_text isar_params else metis_proof_text)