src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
author blanchet
Tue Jul 27 12:01:02 2010 +0200 (2010-07-27)
changeset 38007 f0a4aa17f23f
parent 37998 f1b7fb87f523
child 38014 81c23d286f0c
permissions -rw-r--r--
handle Vampire's equality proxy axiom correctly
     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
     4 
     5 Transfer of proofs from external provers.
     6 *)
     7 
     8 signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
     9 sig
    10   type minimize_command = string list -> string
    11 
    12   val metis_line: bool -> int -> int -> string list -> string
    13   val metis_proof_text:
    14     bool * minimize_command * string * string vector * thm * int
    15     -> string * string list
    16   val isar_proof_text:
    17     string Symtab.table * bool * int * Proof.context * int list
    18     -> bool * minimize_command * string * string vector * thm * int
    19     -> string * string list
    20   val proof_text:
    21     bool -> string Symtab.table * bool * int * Proof.context * int list
    22     -> bool * minimize_command * string * string vector * thm * int
    23     -> string * string list
    24 end;
    25 
    26 structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
    27 struct
    28 
    29 open Metis_Clauses
    30 open Sledgehammer_Util
    31 open Sledgehammer_Fact_Filter
    32 open Sledgehammer_TPTP_Format
    33 
    34 type minimize_command = string list -> string
    35 
    36 fun mk_anot phi = AConn (ANot, [phi])
    37 fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2])
    38 
    39 val index_in_shape : int -> int list -> int = find_index o curry (op =)
    40 fun is_axiom_clause_number thm_names num =
    41   num > 0 andalso num <= Vector.length thm_names andalso
    42   Vector.sub (thm_names, num - 1) <> ""
    43 fun is_conjecture_clause_number conjecture_shape num =
    44   index_in_shape num conjecture_shape >= 0
    45 
    46 fun negate_term (Const (@{const_name All}, T) $ Abs (s, T', t')) =
    47     Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t')
    48   | negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
    49     Const (@{const_name All}, T) $ Abs (s, T', negate_term t')
    50   | negate_term (@{const "op -->"} $ t1 $ t2) =
    51     @{const "op &"} $ t1 $ negate_term t2
    52   | negate_term (@{const "op &"} $ t1 $ t2) =
    53     @{const "op |"} $ negate_term t1 $ negate_term t2
    54   | negate_term (@{const "op |"} $ t1 $ t2) =
    55     @{const "op &"} $ negate_term t1 $ negate_term t2
    56   | negate_term (@{const Not} $ t) = t
    57   | negate_term t = @{const Not} $ t
    58 
    59 datatype ('a, 'b, 'c, 'd, 'e) raw_step =
    60   Definition of 'a * 'b * 'c |
    61   Inference of 'a * 'd * 'e list
    62 
    63 (**** PARSING OF TSTP FORMAT ****)
    64 
    65 datatype int_or_string = Str of string | Int of int
    66 
    67 (*Strings enclosed in single quotes, e.g. filenames*)
    68 val scan_quoted = $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode;
    69 
    70 val scan_dollar_name =
    71   Scan.repeat ($$ "$") -- Symbol.scan_id >> (fn (ss, s) => implode ss ^ s)
    72 
    73 (* needed for SPASS's output format *)
    74 fun repair_name _ "$true" = "c_True"
    75   | repair_name _ "$false" = "c_False"
    76   | repair_name _ "$$e" = "c_equal" (* seen in Vampire proofs *)
    77   | repair_name _ "equal" = "c_equal" (* probably not needed *)
    78   | repair_name pool s = Symtab.lookup pool s |> the_default s
    79 (* Generalized first-order terms, which include file names, numbers, etc. *)
    80 (* The "x" argument is not strictly necessary, but without it Poly/ML loops
    81    forever at compile time. *)
    82 fun parse_generalized_term x =
    83   (scan_quoted >> (fn s => ATerm (Str s, []))
    84    || scan_dollar_name
    85       -- Scan.optional ($$ "(" |-- parse_generalized_terms --| $$ ")") []
    86       >> (fn (s, gs) => ATerm (Str s, gs))
    87    || scan_integer >> (fn k => ATerm (Int k, []))
    88    || $$ "(" |-- parse_generalized_term --| $$ ")"
    89    || $$ "[" |-- Scan.optional parse_generalized_terms [] --| $$ "]"
    90       >> curry ATerm (Str "list")) x
    91 and parse_generalized_terms x =
    92   (parse_generalized_term ::: Scan.repeat ($$ "," |-- parse_generalized_term)) x
    93 fun parse_term pool x =
    94   ((scan_dollar_name >> repair_name pool)
    95     -- Scan.optional ($$ "(" |-- parse_terms pool --| $$ ")") [] >> ATerm) x
    96 and parse_terms pool x =
    97   (parse_term pool ::: Scan.repeat ($$ "," |-- parse_term pool)) x
    98 
    99 fun parse_predicate_term pool =
   100   parse_term pool -- Scan.option (Scan.option ($$ "!") --| $$ "="
   101                                   -- parse_term pool)
   102   >> (fn (u, NONE) => APred u
   103        | (u1, SOME (NONE, u2)) => APred (ATerm ("c_equal", [u1, u2]))
   104        | (u1, SOME (SOME _, u2)) =>
   105          mk_anot (APred (ATerm ("c_equal", [u1, u2]))))
   106 
   107 fun fo_term_head (ATerm (s, _)) = s
   108 
   109 (* TPTP formulas are fully parenthesized, so we don't need to worry about
   110    operator precedence. *)
   111 fun parse_formula pool x =
   112   (($$ "(" |-- parse_formula pool --| $$ ")"
   113     || ($$ "!" >> K AForall || $$ "?" >> K AExists)
   114        --| $$ "[" -- parse_terms pool --| $$ "]" --| $$ ":"
   115        -- parse_formula pool
   116        >> (fn ((q, ts), phi) => AQuant (q, map fo_term_head ts, phi))
   117     || $$ "~" |-- parse_formula pool >> mk_anot
   118     || parse_predicate_term pool)
   119    -- Scan.option ((Scan.this_string "=>" >> K AImplies
   120                     || Scan.this_string "<=>" >> K AIff
   121                     || Scan.this_string "<~>" >> K ANotIff
   122                     || Scan.this_string "<=" >> K AIf
   123                     || $$ "|" >> K AOr || $$ "&" >> K AAnd)
   124                    -- parse_formula pool)
   125    >> (fn (phi1, NONE) => phi1
   126         | (phi1, SOME (c, phi2)) => mk_aconn c (phi1, phi2))) x
   127 
   128 fun ints_of_generalized_term (ATerm (label, gs)) =
   129   fold ints_of_generalized_term gs #> (case label of Int k => cons k | _ => I)
   130 val parse_tstp_annotations =
   131   Scan.optional ($$ "," |-- parse_generalized_term
   132                    --| Scan.option ($$ "," |-- parse_generalized_terms)
   133                  >> (fn g => ints_of_generalized_term g [])) []
   134 
   135 (* Syntax: (fof|cnf)\(<num>, <formula_role>, <cnf_formula> <annotations>\).
   136    The <num> could be an identifier, but we assume integers. *)
   137  fun parse_tstp_line pool =
   138    ((Scan.this_string "fof" || Scan.this_string "cnf") -- $$ "(")
   139      |-- scan_integer --| $$ "," -- Symbol.scan_id --| $$ ","
   140      -- parse_formula pool -- parse_tstp_annotations --| $$ ")" --| $$ "."
   141     >> (fn (((num, role), phi), deps) =>
   142            case role of
   143              "definition" =>
   144              (case phi of
   145                 AConn (AIff, [phi1 as APred _, phi2]) =>
   146                 Definition (num, phi1, phi2)
   147               | APred (ATerm ("$$e", _)) =>
   148                 Inference (num, phi, deps) (* Vampire's equality proxy axiom *)
   149               | _ => raise Fail "malformed definition")
   150            | _ => Inference (num, phi, deps))
   151 
   152 (**** PARSING OF SPASS OUTPUT ****)
   153 
   154 (* SPASS returns clause references of the form "x.y". We ignore "y", whose role
   155    is not clear anyway. *)
   156 val parse_dot_name = scan_integer --| $$ "." --| scan_integer
   157 
   158 val parse_spass_annotations =
   159   Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name
   160                                          --| Scan.option ($$ ","))) []
   161 
   162 (* It is not clear why some literals are followed by sequences of stars and/or
   163    pluses. We ignore them. *)
   164 fun parse_decorated_predicate_term pool =
   165   parse_predicate_term pool --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")
   166 
   167 fun mk_horn ([], []) = APred (ATerm ("c_False", []))
   168   | mk_horn ([], pos_lits) = foldr1 (mk_aconn AOr) pos_lits
   169   | mk_horn (neg_lits, []) = mk_anot (foldr1 (mk_aconn AAnd) neg_lits)
   170   | mk_horn (neg_lits, pos_lits) =
   171     mk_aconn AImplies (foldr1 (mk_aconn AAnd) neg_lits,
   172                        foldr1 (mk_aconn AOr) pos_lits)
   173 
   174 fun parse_horn_clause pool =
   175   Scan.repeat (parse_decorated_predicate_term pool) --| $$ "|" --| $$ "|"
   176     -- Scan.repeat (parse_decorated_predicate_term pool) --| $$ "-" --| $$ ">"
   177     -- Scan.repeat (parse_decorated_predicate_term pool)
   178   >> (mk_horn o apfst (op @))
   179 
   180 (* Syntax: <num>[0:<inference><annotations>]
   181    <cnf_formulas> || <cnf_formulas> -> <cnf_formulas>. *)
   182 fun parse_spass_line pool =
   183   scan_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
   184   -- parse_spass_annotations --| $$ "]" -- parse_horn_clause pool --| $$ "."
   185   >> (fn ((num, deps), u) => Inference (num, u, deps))
   186 
   187 fun parse_line pool = parse_tstp_line pool || parse_spass_line pool
   188 fun parse_lines pool = Scan.repeat1 (parse_line pool)
   189 fun parse_proof pool =
   190   fst o Scan.finite Symbol.stopper
   191             (Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
   192                             (parse_lines pool)))
   193   o explode o strip_spaces
   194 
   195 (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
   196 
   197 exception FO_TERM of string fo_term list
   198 exception FORMULA of (string, string fo_term) formula list
   199 exception SAME of unit
   200 
   201 (* Type variables are given the basic sort "HOL.type". Some will later be
   202    constrained by information from type literals, or by type inference. *)
   203 fun type_from_fo_term tfrees (u as ATerm (a, us)) =
   204   let val Ts = map (type_from_fo_term tfrees) us in
   205     case strip_prefix_and_undo_ascii type_const_prefix a of
   206       SOME b => Type (invert_const b, Ts)
   207     | NONE =>
   208       if not (null us) then
   209         raise FO_TERM [u]  (* only "tconst"s have type arguments *)
   210       else case strip_prefix_and_undo_ascii tfree_prefix a of
   211         SOME b =>
   212         let val s = "'" ^ b in
   213           TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
   214         end
   215       | NONE =>
   216         case strip_prefix_and_undo_ascii tvar_prefix a of
   217           SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
   218         | NONE =>
   219           (* Variable from the ATP, say "X1" *)
   220           Type_Infer.param 0 (a, HOLogic.typeS)
   221   end
   222 
   223 fun fix_atp_variable_name s =
   224   let
   225     fun subscript_name s n = s ^ nat_subscript n
   226     val s = String.map Char.toLower s
   227   in
   228     case space_explode "_" s of
   229       [_] => (case take_suffix Char.isDigit (String.explode s) of
   230                 (cs1 as _ :: _, cs2 as _ :: _) =>
   231                 subscript_name (String.implode cs1)
   232                                (the (Int.fromString (String.implode cs2)))
   233               | (_, _) => s)
   234     | [s1, s2] => (case Int.fromString s2 of
   235                      SOME n => subscript_name s1 n
   236                    | NONE => s)
   237     | _ => s
   238   end
   239 
   240 (* First-order translation. No types are known for variables. "HOLogic.typeT"
   241    should allow them to be inferred.*)
   242 fun term_from_fo_term thy full_types tfrees opt_T =
   243   let
   244     fun aux opt_T extra_us u =
   245       case u of
   246         ATerm ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1
   247       | ATerm ("hAPP", [u1, u2]) => aux opt_T (u2 :: extra_us) u1
   248       | ATerm (a, us) =>
   249         if a = type_wrapper_name then
   250           case us of
   251             [typ_u, term_u] =>
   252             aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
   253           | _ => raise FO_TERM us
   254         else case strip_prefix_and_undo_ascii const_prefix a of
   255           SOME "equal" =>
   256           list_comb (Const (@{const_name "op ="}, HOLogic.typeT),
   257                      map (aux NONE []) us)
   258         | SOME b =>
   259           let
   260             val c = invert_const b
   261             val num_type_args = num_type_args thy c
   262             val (type_us, term_us) =
   263               chop (if full_types then 0 else num_type_args) us
   264             (* Extra args from "hAPP" come after any arguments given directly to
   265                the constant. *)
   266             val term_ts = map (aux NONE []) term_us
   267             val extra_ts = map (aux NONE []) extra_us
   268             val t =
   269               Const (c, if full_types then
   270                           case opt_T of
   271                             SOME T => map fastype_of term_ts ---> T
   272                           | NONE =>
   273                             if num_type_args = 0 then
   274                               Sign.const_instance thy (c, [])
   275                             else
   276                               raise Fail ("no type information for " ^ quote c)
   277                         else
   278                           Sign.const_instance thy (c,
   279                               map (type_from_fo_term tfrees) type_us))
   280           in list_comb (t, term_ts @ extra_ts) end
   281         | NONE => (* a free or schematic variable *)
   282           let
   283             val ts = map (aux NONE []) (us @ extra_us)
   284             val T = map fastype_of ts ---> HOLogic.typeT
   285             val t =
   286               case strip_prefix_and_undo_ascii fixed_var_prefix a of
   287                 SOME b => Free (b, T)
   288               | NONE =>
   289                 case strip_prefix_and_undo_ascii schematic_var_prefix a of
   290                   SOME b => Var ((b, 0), T)
   291                 | NONE =>
   292                   (* Variable from the ATP, say "X1" *)
   293                   Var ((fix_atp_variable_name a, 0), T)
   294           in list_comb (t, ts) end
   295   in aux opt_T [] end
   296 
   297 (* Type class literal applied to a type. Returns triple of polarity, class,
   298    type. *)
   299 fun type_constraint_from_formula pos tfrees (AConn (ANot, [u])) =
   300     type_constraint_from_formula (not pos) tfrees u
   301   | type_constraint_from_formula pos tfrees (phi as APred (ATerm (a, us))) =
   302     (case (strip_prefix_and_undo_ascii class_prefix a,
   303            map (type_from_fo_term tfrees) us) of
   304        (SOME b, [T]) => (pos, b, T)
   305      | _ => raise FORMULA [phi])
   306   | type_constraint_from_formula _ _ phi = raise FORMULA [phi]
   307 
   308 (** Accumulate type constraints in a clause: negative type literals **)
   309 
   310 fun add_var (key, z)  = Vartab.map_default (key, []) (cons z)
   311 
   312 fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl)
   313   | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl)
   314   | add_type_constraint _ = I
   315 
   316 fun is_positive_literal (@{const Not} $ _) = false
   317   | is_positive_literal _ = true
   318 
   319 val combinator_table =
   320   [(@{const_name COMBI}, @{thm COMBI_def_raw}),
   321    (@{const_name COMBK}, @{thm COMBK_def_raw}),
   322    (@{const_name COMBB}, @{thm COMBB_def_raw}),
   323    (@{const_name COMBC}, @{thm COMBC_def_raw}),
   324    (@{const_name COMBS}, @{thm COMBS_def_raw})]
   325 
   326 fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2))
   327   | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t')
   328   | uncombine_term (t as Const (x as (s, _))) =
   329     (case AList.lookup (op =) combinator_table s of
   330        SOME thm => thm |> prop_of |> specialize_type @{theory} x |> Logic.dest_equals |> snd
   331      | NONE => t)
   332   | uncombine_term t = t
   333 
   334 fun disjuncts (AConn (AOr, phis)) = maps disjuncts phis
   335   | disjuncts phi = [phi]
   336 
   337 (* Update schematic type variables with detected sort constraints. It's not
   338    totally clear when this code is necessary. *)
   339 fun repair_tvar_sorts (tvar_tab, t) =
   340   let
   341     fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
   342       | do_type (TVar (xi, s)) =
   343         TVar (xi, the_default s (Vartab.lookup tvar_tab xi))
   344       | do_type (TFree z) = TFree z
   345     fun do_term (Const (a, T)) = Const (a, do_type T)
   346       | do_term (Free (a, T)) = Free (a, do_type T)
   347       | do_term (Var (xi, T)) = Var (xi, do_type T)
   348       | do_term (t as Bound _) = t
   349       | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t)
   350       | do_term (t1 $ t2) = do_term t1 $ do_term t2
   351   in t |> not (Vartab.is_empty tvar_tab) ? do_term end
   352 
   353 fun s_disj (t1, @{const False}) = t1
   354   | s_disj p = HOLogic.mk_disj p
   355 
   356 fun quantify_over_free quant_s free_s body_t =
   357   case Term.add_frees body_t [] |> filter (curry (op =) free_s o fst) of
   358     [] => body_t
   359   | frees as (_, free_T) :: _ =>
   360     Abs (free_s, free_T, fold (curry abstract_over) (map Free frees) body_t)
   361 
   362  (* Interpret a list of syntax trees as a clause, given by "real" literals and
   363    sort constraints. Accumulates sort constraints in "tvar_tab", with "real"
   364    literals in "lits". *)
   365 fun prop_from_formula thy full_types tfrees =
   366    let
   367     val do_sort_constraint =
   368       add_type_constraint o type_constraint_from_formula true tfrees
   369     fun do_real_literal phi =
   370       case phi of
   371         AQuant (_, [], phi) => do_real_literal phi
   372       | AQuant (q, x :: xs, phi') =>
   373         let
   374           val body = do_real_literal (AQuant (q, xs, phi'))
   375           val quant_s = case q of
   376                           AForall => @{const_name All}
   377                         | AExists => @{const_name Ex}
   378         in quantify_over_free quant_s x body end
   379       | AConn (ANot, [phi']) => HOLogic.mk_not (do_real_literal phi')
   380       | AConn (c, [phi1, phi2]) =>
   381         (phi1, phi2)
   382         |> pairself do_real_literal
   383         |> (case c of
   384               AAnd => HOLogic.mk_conj
   385             | AOr => HOLogic.mk_disj
   386             | AImplies => HOLogic.mk_imp
   387             | AIff => (fn (t1, t2) => HOLogic.eq_const HOLogic.boolT $ t1 $ t2))
   388       | APred tm =>
   389         term_from_fo_term thy full_types tfrees (SOME @{typ bool}) tm
   390       | _ => raise FORMULA [phi]
   391     fun do_literals (tvar_tab, t) [] = (tvar_tab, t)
   392       | do_literals (tvar_tab, t) (u :: us) =
   393         (do_literals (tvar_tab |> do_sort_constraint u, t) us
   394          handle FO_TERM _ => raise SAME ()
   395               | FORMULA _ => raise SAME ())
   396         handle SAME () =>
   397                do_literals (tvar_tab, s_disj (do_real_literal u, t)) us
   398   in
   399     repair_tvar_sorts o do_literals (Vartab.empty, HOLogic.false_const)
   400     o disjuncts
   401   end
   402 
   403 fun check_formula ctxt =
   404   Type_Infer.constrain @{typ bool}
   405   #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
   406 
   407 
   408 (**** Translation of TSTP files to Isar Proofs ****)
   409 
   410 fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
   411   | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
   412 
   413 fun decode_line full_types tfrees (Definition (num, phi1, phi2)) ctxt =
   414     let
   415       val thy = ProofContext.theory_of ctxt
   416       val t1 = prop_from_formula thy full_types tfrees phi1
   417       val vars = snd (strip_comb t1)
   418       val frees = map unvarify_term vars
   419       val unvarify_args = subst_atomic (vars ~~ frees)
   420       val t2 = prop_from_formula thy full_types tfrees phi2
   421       val (t1, t2) =
   422         HOLogic.eq_const HOLogic.typeT $ t1 $ t2
   423         |> unvarify_args |> uncombine_term |> check_formula ctxt
   424         |> HOLogic.dest_eq
   425     in
   426       (Definition (num, t1, t2),
   427        fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
   428     end
   429   | decode_line full_types tfrees (Inference (num, u, deps)) ctxt =
   430     let
   431       val thy = ProofContext.theory_of ctxt
   432       val t = u |> prop_from_formula thy full_types tfrees
   433                 |> uncombine_term |> check_formula ctxt
   434     in
   435       (Inference (num, t, deps),
   436        fold Variable.declare_term (OldTerm.term_frees t) ctxt)
   437     end
   438 fun decode_lines ctxt full_types tfrees lines =
   439   fst (fold_map (decode_line full_types tfrees) lines ctxt)
   440 
   441 fun aint_actual_inference _ (Definition _) = true
   442   | aint_actual_inference t (Inference (_, t', _)) = not (t aconv t')
   443 
   444 (* No "real" literals means only type information (tfree_tcs, clsrel, or
   445    clsarity). *)
   446 val is_only_type_information = curry (op aconv) HOLogic.true_const
   447 
   448 fun replace_one_dep (old, new) dep = if dep = old then new else [dep]
   449 fun replace_deps_in_line _ (line as Definition _) = line
   450   | replace_deps_in_line p (Inference (num, t, deps)) =
   451     Inference (num, t, fold (union (op =) o replace_one_dep p) deps [])
   452 
   453 (*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ
   454   only in type information.*)
   455 fun add_line _ _ (line as Definition _) lines = line :: lines
   456   | add_line conjecture_shape thm_names (Inference (num, t, [])) lines =
   457     (* No dependencies: axiom, conjecture clause, or internal axioms or
   458        definitions (Vampire). *)
   459     if is_axiom_clause_number thm_names num then
   460       (* Axioms are not proof lines. *)
   461       if is_only_type_information t then
   462         map (replace_deps_in_line (num, [])) lines
   463       (* Is there a repetition? If so, replace later line by earlier one. *)
   464       else case take_prefix (aint_actual_inference t) lines of
   465         (_, []) => lines (*no repetition of proof line*)
   466       | (pre, Inference (num', _, _) :: post) =>
   467         pre @ map (replace_deps_in_line (num', [num])) post
   468     else if is_conjecture_clause_number conjecture_shape num then
   469       Inference (num, t, []) :: lines
   470     else
   471       map (replace_deps_in_line (num, [])) lines
   472   | add_line _ _ (Inference (num, t, deps)) lines =
   473     (* Type information will be deleted later; skip repetition test. *)
   474     if is_only_type_information t then
   475       Inference (num, t, deps) :: lines
   476     (* Is there a repetition? If so, replace later line by earlier one. *)
   477     else case take_prefix (aint_actual_inference t) lines of
   478       (* FIXME: Doesn't this code risk conflating proofs involving different
   479          types?? *)
   480        (_, []) => Inference (num, t, deps) :: lines
   481      | (pre, Inference (num', t', _) :: post) =>
   482        Inference (num, t', deps) ::
   483        pre @ map (replace_deps_in_line (num', [num])) post
   484 
   485 (* Recursively delete empty lines (type information) from the proof. *)
   486 fun add_nontrivial_line (Inference (num, t, [])) lines =
   487     if is_only_type_information t then delete_dep num lines
   488     else Inference (num, t, []) :: lines
   489   | add_nontrivial_line line lines = line :: lines
   490 and delete_dep num lines =
   491   fold_rev add_nontrivial_line (map (replace_deps_in_line (num, [])) lines) []
   492 
   493 (* ATPs sometimes reuse free variable names in the strangest ways. Removing
   494    offending lines often does the trick. *)
   495 fun is_bad_free frees (Free x) = not (member (op =) frees x)
   496   | is_bad_free _ _ = false
   497 
   498 (* Vampire is keen on producing these. *)
   499 fun is_trivial_formula (@{const Not} $ (Const (@{const_name "op ="}, _)
   500                                         $ t1 $ t2)) = (t1 aconv t2)
   501   | is_trivial_formula _ = false
   502 
   503 fun add_desired_line _ _ _ _ (line as Definition (num, _, _)) (j, lines) =
   504     (j, line :: map (replace_deps_in_line (num, [])) lines)
   505   | add_desired_line isar_shrink_factor conjecture_shape thm_names frees
   506                      (Inference (num, t, deps)) (j, lines) =
   507     (j + 1,
   508      if is_axiom_clause_number thm_names num orelse
   509         is_conjecture_clause_number conjecture_shape num orelse
   510         (not (is_only_type_information t) andalso
   511          null (Term.add_tvars t []) andalso
   512          not (exists_subterm (is_bad_free frees) t) andalso
   513          not (is_trivial_formula t) andalso
   514          (null lines orelse (* last line must be kept *)
   515           (length deps >= 2 andalso j mod isar_shrink_factor = 0))) then
   516        Inference (num, t, deps) :: lines  (* keep line *)
   517      else
   518        map (replace_deps_in_line (num, deps)) lines)  (* drop line *)
   519 
   520 (** EXTRACTING LEMMAS **)
   521 
   522 (* A list consisting of the first number in each line is returned. For TSTP,
   523    interesting lines have the form "fof(108, axiom, ...)", where the number
   524    (108) is extracted. For SPASS, lines have the form "108[0:Inp] ...", where
   525    the first number (108) is extracted. *)
   526 fun extract_formula_numbers_in_atp_proof atp_proof =
   527   let
   528     val tokens_of = String.tokens (not o Char.isAlphaNum)
   529     fun extract_num ("fof" :: num :: "axiom" :: _) = Int.fromString num
   530       | extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num
   531       | extract_num _ = NONE
   532   in atp_proof |> split_lines |> map_filter (extract_num o tokens_of) end
   533 
   534 val indent_size = 2
   535 val no_label = ("", ~1)
   536 
   537 val raw_prefix = "X"
   538 val assum_prefix = "A"
   539 val fact_prefix = "F"
   540 
   541 fun string_for_label (s, num) = s ^ string_of_int num
   542 
   543 fun metis_using [] = ""
   544   | metis_using ls =
   545     "using " ^ space_implode " " (map string_for_label ls) ^ " "
   546 fun metis_apply _ 1 = "by "
   547   | metis_apply 1 _ = "apply "
   548   | metis_apply i _ = "prefer " ^ string_of_int i ^ " apply "
   549 fun metis_name full_types = if full_types then "metisFT" else "metis"
   550 fun metis_call full_types [] = metis_name full_types
   551   | metis_call full_types ss =
   552     "(" ^ metis_name full_types ^ " " ^ space_implode " " ss ^ ")"
   553 fun metis_command full_types i n (ls, ss) =
   554   metis_using ls ^ metis_apply i n ^ metis_call full_types ss
   555 fun metis_line full_types i n ss =
   556   "Try this command: " ^
   557   Markup.markup Markup.sendback (metis_command full_types i n ([], ss)) ^ ".\n"
   558 fun minimize_line _ [] = ""
   559   | minimize_line minimize_command facts =
   560     case minimize_command facts of
   561       "" => ""
   562     | command =>
   563       "To minimize the number of lemmas, try this command: " ^
   564       Markup.markup Markup.sendback command ^ ".\n"
   565 
   566 val unprefix_chained = perhaps (try (unprefix chained_prefix))
   567 
   568 fun metis_proof_text (full_types, minimize_command, atp_proof, thm_names, goal,
   569                       i) =
   570   let
   571     val raw_lemmas =
   572       atp_proof |> extract_formula_numbers_in_atp_proof
   573                 |> filter (is_axiom_clause_number thm_names)
   574                 |> map (fn i => Vector.sub (thm_names, i - 1))
   575     val (chained_lemmas, other_lemmas) =
   576       raw_lemmas |> List.partition (String.isPrefix chained_prefix)
   577                  |>> map (unprefix chained_prefix)
   578                  |> pairself (sort_distinct string_ord)
   579     val lemmas = other_lemmas @ chained_lemmas
   580     val n = Logic.count_prems (prop_of goal)
   581   in
   582     (metis_line full_types i n other_lemmas ^
   583      minimize_line minimize_command lemmas, lemmas)
   584   end
   585 
   586 (** Isar proof construction and manipulation **)
   587 
   588 fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
   589   (union (op =) ls1 ls2, union (op =) ss1 ss2)
   590 
   591 type label = string * int
   592 type facts = label list * string list
   593 
   594 datatype qualifier = Show | Then | Moreover | Ultimately
   595 
   596 datatype step =
   597   Fix of (string * typ) list |
   598   Let of term * term |
   599   Assume of label * term |
   600   Have of qualifier list * label * term * byline
   601 and byline =
   602   ByMetis of facts |
   603   CaseSplit of step list list * facts
   604 
   605 fun smart_case_split [] facts = ByMetis facts
   606   | smart_case_split proofs facts = CaseSplit (proofs, facts)
   607 
   608 fun add_fact_from_dep thm_names num =
   609   if is_axiom_clause_number thm_names num then
   610     apsnd (insert (op =) (Vector.sub (thm_names, num - 1)))
   611   else
   612     apfst (insert (op =) (raw_prefix, num))
   613 
   614 fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t
   615 fun forall_vars t = fold_rev forall_of (map Var (Term.add_vars t [])) t
   616 
   617 fun step_for_line _ _ (Definition (_, t1, t2)) = Let (t1, t2)
   618   | step_for_line _ _ (Inference (num, t, [])) = Assume ((raw_prefix, num), t)
   619   | step_for_line thm_names j (Inference (num, t, deps)) =
   620     Have (if j = 1 then [Show] else [], (raw_prefix, num),
   621           forall_vars t,
   622           ByMetis (fold (add_fact_from_dep thm_names) deps ([], [])))
   623 
   624 fun proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
   625                          atp_proof conjecture_shape thm_names params frees =
   626   let
   627     val lines =
   628       atp_proof ^ "$" (* the $ sign acts as a sentinel (FIXME: pick it up) *)
   629       |> parse_proof pool
   630       |> decode_lines ctxt full_types tfrees
   631       |> rpair [] |-> fold_rev (add_line conjecture_shape thm_names)
   632       |> rpair [] |-> fold_rev add_nontrivial_line
   633       |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor
   634                                                conjecture_shape thm_names frees)
   635       |> snd
   636   in
   637     (if null params then [] else [Fix params]) @
   638     map2 (step_for_line thm_names) (length lines downto 1) lines
   639   end
   640 
   641 (* When redirecting proofs, we keep information about the labels seen so far in
   642    the "backpatches" data structure. The first component indicates which facts
   643    should be associated with forthcoming proof steps. The second component is a
   644    pair ("assum_ls", "drop_ls"), where "assum_ls" are the labels that should
   645    become assumptions and "drop_ls" are the labels that should be dropped in a
   646    case split. *)
   647 type backpatches = (label * facts) list * (label list * label list)
   648 
   649 fun used_labels_of_step (Have (_, _, _, by)) =
   650     (case by of
   651        ByMetis (ls, _) => ls
   652      | CaseSplit (proofs, (ls, _)) =>
   653        fold (union (op =) o used_labels_of) proofs ls)
   654   | used_labels_of_step _ = []
   655 and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []
   656 
   657 fun new_labels_of_step (Fix _) = []
   658   | new_labels_of_step (Let _) = []
   659   | new_labels_of_step (Assume (l, _)) = [l]
   660   | new_labels_of_step (Have (_, l, _, _)) = [l]
   661 val new_labels_of = maps new_labels_of_step
   662 
   663 val join_proofs =
   664   let
   665     fun aux _ [] = NONE
   666       | aux proof_tail (proofs as (proof1 :: _)) =
   667         if exists null proofs then
   668           NONE
   669         else if forall (curry (op =) (hd proof1) o hd) (tl proofs) then
   670           aux (hd proof1 :: proof_tail) (map tl proofs)
   671         else case hd proof1 of
   672           Have ([], l, t, _) => (* FIXME: should we really ignore the "by"? *)
   673           if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t')
   674                       | _ => false) (tl proofs) andalso
   675              not (exists (member (op =) (maps new_labels_of proofs))
   676                          (used_labels_of proof_tail)) then
   677             SOME (l, t, map rev proofs, proof_tail)
   678           else
   679             NONE
   680         | _ => NONE
   681   in aux [] o map rev end
   682 
   683 fun case_split_qualifiers proofs =
   684   case length proofs of
   685     0 => []
   686   | 1 => [Then]
   687   | _ => [Ultimately]
   688 
   689 fun redirect_proof conjecture_shape hyp_ts concl_t proof =
   690   let
   691     (* The first pass outputs those steps that are independent of the negated
   692        conjecture. The second pass flips the proof by contradiction to obtain a
   693        direct proof, introducing case splits when an inference depends on
   694        several facts that depend on the negated conjecture. *)
   695     fun find_hyp num = nth hyp_ts (index_in_shape num conjecture_shape)
   696     val concl_l = (raw_prefix, List.last conjecture_shape)
   697     fun first_pass ([], contra) = ([], contra)
   698       | first_pass ((step as Fix _) :: proof, contra) =
   699         first_pass (proof, contra) |>> cons step
   700       | first_pass ((step as Let _) :: proof, contra) =
   701         first_pass (proof, contra) |>> cons step
   702       | first_pass ((step as Assume (l as (_, num), _)) :: proof, contra) =
   703         if l = concl_l then
   704           first_pass (proof, contra ||> l = concl_l ? cons step)
   705         else
   706           first_pass (proof, contra) |>> cons (Assume (l, find_hyp num))
   707       | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
   708         let val step = Have (qs, l, t, ByMetis (ls, ss)) in
   709           if exists (member (op =) (fst contra)) ls then
   710             first_pass (proof, contra |>> cons l ||> cons step)
   711           else
   712             first_pass (proof, contra) |>> cons step
   713         end
   714       | first_pass _ = raise Fail "malformed proof"
   715     val (proof_top, (contra_ls, contra_proof)) =
   716       first_pass (proof, ([concl_l], []))
   717     val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst
   718     fun backpatch_labels patches ls =
   719       fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
   720     fun second_pass end_qs ([], assums, patches) =
   721         ([Have (end_qs, no_label, concl_t,
   722                 ByMetis (backpatch_labels patches (map snd assums)))], patches)
   723       | second_pass end_qs (Assume (l, t) :: proof, assums, patches) =
   724         second_pass end_qs (proof, (t, l) :: assums, patches)
   725       | second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums,
   726                             patches) =
   727         if member (op =) (snd (snd patches)) l andalso
   728            not (member (op =) (fst (snd patches)) l) andalso
   729            not (AList.defined (op =) (fst patches) l) then
   730           second_pass end_qs (proof, assums, patches ||> apsnd (append ls))
   731         else
   732           (case List.partition (member (op =) contra_ls) ls of
   733              ([contra_l], co_ls) =>
   734              if member (op =) qs Show then
   735                second_pass end_qs (proof, assums,
   736                                    patches |>> cons (contra_l, (co_ls, ss)))
   737              else
   738                second_pass end_qs
   739                            (proof, assums,
   740                             patches |>> cons (contra_l, (l :: co_ls, ss)))
   741                |>> cons (if member (op =) (fst (snd patches)) l then
   742                            Assume (l, negate_term t)
   743                          else
   744                            Have (qs, l, negate_term t,
   745                                  ByMetis (backpatch_label patches l)))
   746            | (contra_ls as _ :: _, co_ls) =>
   747              let
   748                val proofs =
   749                  map_filter
   750                      (fn l =>
   751                          if l = concl_l then
   752                            NONE
   753                          else
   754                            let
   755                              val drop_ls = filter (curry (op <>) l) contra_ls
   756                            in
   757                              second_pass []
   758                                  (proof, assums,
   759                                   patches ||> apfst (insert (op =) l)
   760                                           ||> apsnd (union (op =) drop_ls))
   761                              |> fst |> SOME
   762                            end) contra_ls
   763                val (assumes, facts) =
   764                  if member (op =) (fst (snd patches)) l then
   765                    ([Assume (l, negate_term t)], (l :: co_ls, ss))
   766                  else
   767                    ([], (co_ls, ss))
   768              in
   769                (case join_proofs proofs of
   770                   SOME (l, t, proofs, proof_tail) =>
   771                   Have (case_split_qualifiers proofs @
   772                         (if null proof_tail then end_qs else []), l, t,
   773                         smart_case_split proofs facts) :: proof_tail
   774                 | NONE =>
   775                   [Have (case_split_qualifiers proofs @ end_qs, no_label,
   776                          concl_t, smart_case_split proofs facts)],
   777                 patches)
   778                |>> append assumes
   779              end
   780            | _ => raise Fail "malformed proof")
   781        | second_pass _ _ = raise Fail "malformed proof"
   782     val proof_bottom =
   783       second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst
   784   in proof_top @ proof_bottom end
   785 
   786 val kill_duplicate_assumptions_in_proof =
   787   let
   788     fun relabel_facts subst =
   789       apfst (map (fn l => AList.lookup (op =) subst l |> the_default l))
   790     fun do_step (step as Assume (l, t)) (proof, subst, assums) =
   791         (case AList.lookup (op aconv) assums t of
   792            SOME l' => (proof, (l, l') :: subst, assums)
   793          | NONE => (step :: proof, subst, (t, l) :: assums))
   794       | do_step (Have (qs, l, t, by)) (proof, subst, assums) =
   795         (Have (qs, l, t,
   796                case by of
   797                  ByMetis facts => ByMetis (relabel_facts subst facts)
   798                | CaseSplit (proofs, facts) =>
   799                  CaseSplit (map do_proof proofs, relabel_facts subst facts)) ::
   800          proof, subst, assums)
   801       | do_step step (proof, subst, assums) = (step :: proof, subst, assums)
   802     and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
   803   in do_proof end
   804 
   805 val then_chain_proof =
   806   let
   807     fun aux _ [] = []
   808       | aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof
   809       | aux l' (Have (qs, l, t, by) :: proof) =
   810         (case by of
   811            ByMetis (ls, ss) =>
   812            Have (if member (op =) ls l' then
   813                    (Then :: qs, l, t,
   814                     ByMetis (filter_out (curry (op =) l') ls, ss))
   815                  else
   816                    (qs, l, t, ByMetis (ls, ss)))
   817          | CaseSplit (proofs, facts) =>
   818            Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) ::
   819         aux l proof
   820       | aux _ (step :: proof) = step :: aux no_label proof
   821   in aux no_label end
   822 
   823 fun kill_useless_labels_in_proof proof =
   824   let
   825     val used_ls = used_labels_of proof
   826     fun do_label l = if member (op =) used_ls l then l else no_label
   827     fun do_step (Assume (l, t)) = Assume (do_label l, t)
   828       | do_step (Have (qs, l, t, by)) =
   829         Have (qs, do_label l, t,
   830               case by of
   831                 CaseSplit (proofs, facts) =>
   832                 CaseSplit (map (map do_step) proofs, facts)
   833               | _ => by)
   834       | do_step step = step
   835   in map do_step proof end
   836 
   837 fun prefix_for_depth n = replicate_string (n + 1)
   838 
   839 val relabel_proof =
   840   let
   841     fun aux _ _ _ [] = []
   842       | aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) =
   843         if l = no_label then
   844           Assume (l, t) :: aux subst depth (next_assum, next_fact) proof
   845         else
   846           let val l' = (prefix_for_depth depth assum_prefix, next_assum) in
   847             Assume (l', t) ::
   848             aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof
   849           end
   850       | aux subst depth (next_assum, next_fact) (Have (qs, l, t, by) :: proof) =
   851         let
   852           val (l', subst, next_fact) =
   853             if l = no_label then
   854               (l, subst, next_fact)
   855             else
   856               let
   857                 val l' = (prefix_for_depth depth fact_prefix, next_fact)
   858               in (l', (l, l') :: subst, next_fact + 1) end
   859           val relabel_facts =
   860             apfst (map (fn l =>
   861                            case AList.lookup (op =) subst l of
   862                              SOME l' => l'
   863                            | NONE => raise Fail ("unknown label " ^
   864                                                  quote (string_for_label l))))
   865           val by =
   866             case by of
   867               ByMetis facts => ByMetis (relabel_facts facts)
   868             | CaseSplit (proofs, facts) =>
   869               CaseSplit (map (aux subst (depth + 1) (1, 1)) proofs,
   870                          relabel_facts facts)
   871         in
   872           Have (qs, l', t, by) ::
   873           aux subst depth (next_assum, next_fact) proof
   874         end
   875       | aux subst depth nextp (step :: proof) =
   876         step :: aux subst depth nextp proof
   877   in aux [] 0 (1, 1) end
   878 
   879 fun string_for_proof ctxt full_types i n =
   880   let
   881     fun fix_print_mode f x =
   882       setmp_CRITICAL show_no_free_types true
   883           (setmp_CRITICAL show_types true
   884                (Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
   885                                          (print_mode_value ())) f)) x
   886     fun do_indent ind = replicate_string (ind * indent_size) " "
   887     fun do_free (s, T) =
   888       maybe_quote s ^ " :: " ^
   889       maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
   890     fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
   891     fun do_have qs =
   892       (if member (op =) qs Moreover then "moreover " else "") ^
   893       (if member (op =) qs Ultimately then "ultimately " else "") ^
   894       (if member (op =) qs Then then
   895          if member (op =) qs Show then "thus" else "hence"
   896        else
   897          if member (op =) qs Show then "show" else "have")
   898     val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
   899     fun do_facts (ls, ss) =
   900       let
   901         val ls = ls |> sort_distinct (prod_ord string_ord int_ord)
   902         val ss = ss |> map unprefix_chained |> sort_distinct string_ord
   903       in metis_command full_types 1 1 (ls, ss) end
   904     and do_step ind (Fix xs) =
   905         do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
   906       | do_step ind (Let (t1, t2)) =
   907         do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
   908       | do_step ind (Assume (l, t)) =
   909         do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
   910       | do_step ind (Have (qs, l, t, ByMetis facts)) =
   911         do_indent ind ^ do_have qs ^ " " ^
   912         do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n"
   913       | do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) =
   914         space_implode (do_indent ind ^ "moreover\n")
   915                       (map (do_block ind) proofs) ^
   916         do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^
   917         do_facts facts ^ "\n"
   918     and do_steps prefix suffix ind steps =
   919       let val s = implode (map (do_step ind) steps) in
   920         replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
   921         String.extract (s, ind * indent_size,
   922                         SOME (size s - ind * indent_size - 1)) ^
   923         suffix ^ "\n"
   924       end
   925     and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
   926     (* One-step proofs are pointless; better use the Metis one-liner
   927        directly. *)
   928     and do_proof [Have (_, _, _, ByMetis _)] = ""
   929       | do_proof proof =
   930         (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
   931         do_indent 0 ^ "proof -\n" ^
   932         do_steps "" "" 1 proof ^
   933         do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n"
   934   in do_proof end
   935 
   936 fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   937                     (other_params as (full_types, _, atp_proof, thm_names, goal,
   938                                       i)) =
   939   let
   940     (* ### FIXME: avoid duplication with ATP_Systems -- and move strip_subgoal
   941        to ATP_Systems *)
   942     val (params, hyp_ts, concl_t) = strip_subgoal goal i
   943     val frees = fold Term.add_frees (concl_t :: hyp_ts) []
   944     val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
   945     val n = Logic.count_prems (prop_of goal)
   946     val (one_line_proof, lemma_names) = metis_proof_text other_params
   947     fun isar_proof_for () =
   948       case proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
   949                                 atp_proof conjecture_shape thm_names params
   950                                 frees
   951            |> redirect_proof conjecture_shape hyp_ts concl_t
   952            |> kill_duplicate_assumptions_in_proof
   953            |> then_chain_proof
   954            |> kill_useless_labels_in_proof
   955            |> relabel_proof
   956            |> string_for_proof ctxt full_types i n of
   957         "" => ""
   958       | proof => "\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
   959     val isar_proof =
   960       if debug then
   961         isar_proof_for ()
   962       else
   963         try isar_proof_for ()
   964         |> the_default "Warning: The Isar proof construction failed.\n"
   965   in (one_line_proof ^ isar_proof, lemma_names) end
   966 
   967 fun proof_text isar_proof isar_params other_params =
   968   (if isar_proof then isar_proof_text isar_params else metis_proof_text)
   969       other_params
   970 
   971 end;