src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
author wenzelm
Thu May 27 17:41:27 2010 +0200 (2010-05-27)
changeset 37145 01aa36932739
parent 36968 62e29faa3718
child 37146 f652333bbf8e
permissions -rw-r--r--
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
     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   type name_pool = Sledgehammer_FOL_Clause.name_pool
    12 
    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
    19   val metis_proof_text:
    20     minimize_command * string * string vector * thm * int
    21     -> string * string list
    22   val isar_proof_text:
    23     name_pool option * bool * bool * int * Proof.context * int list list
    24     -> minimize_command * string * string vector * thm * int
    25     -> string * string list
    26   val proof_text:
    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
    30 end;
    31 
    32 structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
    33 struct
    34 
    35 open Sledgehammer_Util
    36 open Sledgehammer_FOL_Clause
    37 open Sledgehammer_HOL_Clause
    38 open Sledgehammer_Fact_Preprocessor
    39 
    40 type minimize_command = string list -> string
    41 
    42 fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
    43 fun is_head_digit s = Char.isDigit (String.sub (s, 0))
    44 
    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 =
    48   Long_Name.base_name
    49   #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
    50 
    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
    56 
    57 fun ugly_name NONE s = s
    58   | ugly_name (SOME the_pool) s =
    59     case Symtab.lookup (snd the_pool) s of
    60       SOME s' => s'
    61     | NONE => s
    62 
    63 fun smart_lambda v t =
    64   Abs (case v of
    65          Const (s, _) =>
    66          List.last (space_explode skolem_infix (Long_Name.base_name s))
    67        | Var ((s, _), _) => s
    68        | Free (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
    71 
    72 datatype ('a, 'b, 'c, 'd, 'e) raw_step =
    73   Definition of 'a * 'b * 'c |
    74   Inference of 'a * 'd * 'e list
    75 
    76 (**** PARSING OF TSTP FORMAT ****)
    77 
    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)
    88       else
    89         str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^
    90         strip_spaces_in_list (c3 :: cs)
    91     else
    92       str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
    93 val strip_spaces = strip_spaces_in_list o String.explode
    94 
    95 (* Syntax trees, either term list or formulae *)
    96 datatype node = IntLeaf of int | StrNode of string * node list
    97 
    98 fun str_leaf s = StrNode (s, [])
    99 
   100 fun scons (x, y) = StrNode ("cons", [x, y])
   101 val slist_of = List.foldl scons (str_leaf "nil")
   102 
   103 (*Strings enclosed in single quotes, e.g. filenames*)
   104 val parse_quoted = $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode;
   105 
   106 (*Integer constants, typically proof line numbers*)
   107 val parse_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
   108 
   109 val parse_dollar_name =
   110   Scan.repeat ($$ "$") -- Symbol.scan_id >> (fn (ss, s) => implode ss ^ s)
   111 
   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
   130 
   131 fun negate_node u = StrNode ("c_Not", [u])
   132 fun equate_nodes u1 u2 = StrNode ("c_equal", [u1, u2])
   133 
   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 ($$ "!") --| $$ "="
   141                                   -- parse_term pool)
   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)
   152   >> List.concat
   153 
   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 [])) []
   160 
   161 fun parse_definition pool =
   162   $$ "(" |-- parse_literal NONE --| Scan.this_string "<=>"
   163   -- parse_clause pool --| $$ ")"
   164 
   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)
   178 
   179 (**** PARSING OF SPASS OUTPUT ****)
   180 
   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
   184 
   185 val parse_spass_annotations =
   186   Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name
   187                                          --| Scan.option ($$ ","))) []
   188 
   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 ($$ "*" || $$ "+" || $$ " ")
   193 
   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)
   201 
   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 --| $$ "."
   208   >> finish_spass_line
   209 
   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")
   215                             (parse_lines pool)))
   216   o explode o strip_spaces
   217 
   218 (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
   219 
   220 exception NODE of node list
   221 
   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)))
   226   else NONE;
   227 
   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));
   231 
   232 fun invert_type_const c =
   233     case Symtab.lookup type_const_trans_table_inv c of
   234         SOME c' => c'
   235       | NONE => c;
   236 
   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)
   244       | NONE =>
   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
   248           SOME b =>
   249           let val s = "'" ^ b in
   250             TFree (s, AList.lookup (op =) tfrees s |> the_default HOLogic.typeS)
   251           end
   252         | NONE =>
   253           case strip_prefix tvar_prefix a of
   254             SOME b => TVar (("'" ^ b, 0), HOLogic.typeS)
   255           | NONE =>
   256             (* Variable from the ATP, say "X1" *)
   257             Type_Infer.param 0 (a, HOLogic.typeS)
   258     end
   259 
   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)))
   264 
   265 fun invert_const c = c |> Symtab.lookup const_trans_table_inv |> the_default c
   266 
   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))
   270 
   271 fun fix_atp_variable_name s =
   272   let
   273     fun subscript_name s n = s ^ nat_subscript n
   274     val s = String.map Char.toLower s
   275   in
   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)))
   281               | (_, _) => s)
   282     | [s1, s2] => (case Int.fromString s2 of
   283                      SOME n => subscript_name s1 n
   284                    | NONE => s)
   285     | _ => s
   286   end
   287 
   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 =
   291   let
   292     fun aux opt_T args u =
   293       case u of
   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
   298       | StrNode (a, us) =>
   299         if a = type_wrapper_name then
   300           case us of
   301             [term_u, typ_u] =>
   302             aux (SOME (type_from_node tfrees typ_u)) args term_u
   303           | _ => raise NODE us
   304         else case strip_prefix const_prefix a of
   305           SOME "equal" =>
   306           list_comb (Const (@{const_name "op ="}, HOLogic.typeT),
   307                      map (aux NONE []) us)
   308         | SOME b =>
   309           let
   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)
   315             val t =
   316               Const (c, if full_types then
   317                           case opt_T of
   318                             SOME T => map fastype_of ts ---> T
   319                           | NONE =>
   320                             if num_type_args = 0 then
   321                               Sign.const_instance thy (c, [])
   322                             else
   323                               raise Fail ("no type information for " ^ quote c)
   324                         else
   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 *)
   332           let
   333             val ts = map (aux NONE []) (us @ args)
   334             val T = map fastype_of ts ---> HOLogic.typeT
   335             val t =
   336               case strip_prefix fixed_var_prefix a of
   337                 SOME b => Free (b, T)
   338               | NONE =>
   339                 case strip_prefix schematic_var_prefix a of
   340                   SOME b => Var ((b, 0), T)
   341                 | NONE =>
   342                   (* Variable from the ATP, say "X1" *)
   343                   Var ((fix_atp_variable_name a, 0), T)
   344           in list_comb (t, ts) end
   345   in aux end
   346 
   347 (* Type class literal applied to a type. Returns triple of polarity, class,
   348    type. *)
   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]
   353       | StrNode (a, us) =>
   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])
   358 
   359 (** Accumulate type constraints in a clause: negative type literals **)
   360 
   361 fun add_var (key, z)  = Vartab.map_default (key, []) (cons z)
   362 
   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
   366 
   367 fun is_positive_literal (@{const Not} $ _) = false
   368   | is_positive_literal t = true
   369 
   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
   382 
   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 _ :: _) =>
   388       @{const "op -->"}
   389           $ foldr1 HOLogic.mk_conj (map (negate_term thy) neg_lits)
   390           $ foldr1 HOLogic.mk_disj pos_lits
   391     | _ => foldr1 HOLogic.mk_disj lits
   392 
   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
   399 
   400 (*Accumulate sort constraints in vt, with "real" literals in lits.*)
   401 fun lits_of_nodes thy full_types tfrees =
   402   let
   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
   407         handle NODE _ =>
   408                aux (vt, term_from_node thy full_types tfrees (SOME @{typ bool})
   409                                        [] u :: lits) us
   410   in aux end
   411 
   412 (* Update TVars with detected sort constraints. It's not totally clear when
   413    this code is necessary. *)
   414 fun repair_tvar_sorts vt =
   415   let
   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
   426 
   427 fun unskolemize_term t =
   428   Term.add_consts t []
   429   |> filter (is_skolem_const_name o fst) |> map Const
   430   |> rpair t |-> fold forall_of
   431 
   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})]
   438 
   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
   444      | NONE => t)
   445   | uncombine_term t = t
   446 
   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 =
   451   let
   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)
   458 
   459 
   460 (**** Translation of TSTP files to Isar Proofs ****)
   461 
   462 fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
   463   | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
   464 
   465 fun decode_line full_types tfrees (Definition (num, u, us)) ctxt =
   466     let
   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
   472       val (t1, t2) =
   473         HOLogic.eq_const HOLogic.typeT $ t1 $ t2
   474         |> unvarify_args |> uncombine_term |> check_formula ctxt
   475         |> HOLogic.dest_eq
   476     in
   477       (Definition (num, t1, t2),
   478        fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
   479     end
   480   | decode_line full_types tfrees (Inference (num, us, deps)) ctxt =
   481     let
   482       val t = us |> clause_of_nodes ctxt full_types tfrees
   483                  |> unskolemize_term |> uncombine_term |> check_formula ctxt
   484     in
   485       (Inference (num, t, deps),
   486        fold Variable.declare_term (OldTerm.term_frees t) ctxt)
   487     end
   488 fun decode_lines ctxt full_types tfrees lines =
   489   fst (fold_map (decode_line full_types tfrees) lines ctxt)
   490 
   491 fun aint_inference _ (Definition _) = true
   492   | aint_inference t (Inference (_, t', _)) = not (t aconv t')
   493 
   494 (* No "real" literals means only type information (tfree_tcs, clsrel, or
   495    clsarity). *)
   496 val is_only_type_information = curry (op aconv) HOLogic.true_const
   497 
   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 [])
   502 
   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
   520     else
   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
   529          types?? *)
   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
   534 
   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) []
   542 
   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
   547 
   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
   552 
   553 fun add_desired_line _ _ _ _ _ (line as Definition _) (j, lines) =
   554     (j, line :: lines)
   555   | add_desired_line ctxt isar_shrink_factor conjecture_shape thm_names frees
   556                      (Inference (num, t, deps)) (j, lines) =
   557     (j + 1,
   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 *)
   567      else
   568        map (replace_deps_in_line (num, deps)) lines)  (* drop line *)
   569 
   570 (** EXTRACTING LEMMAS **)
   571 
   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
   576    extracted. *)
   577 fun extract_clause_numbers_in_atp_proof atp_proof =
   578   let
   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
   584   
   585 (* Used to label theorems chained into the goal. *)
   586 val chained_hint = "sledgehammer_chained"
   587 
   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
   600       "" => ""
   601     | command =>
   602       "To minimize the number of lemmas, try this command: " ^
   603       Markup.markup Markup.sendback command ^ ".\n"
   604 
   605 fun metis_proof_text (minimize_command, atp_proof, thm_names, goal, i) =
   606   let
   607     val lemmas =
   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
   615 
   616 (** Isar proof construction and manipulation **)
   617 
   618 fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
   619   (union (op =) ls1 ls2, union (op =) ss1 ss2)
   620 
   621 type label = string * int
   622 type facts = label list * string list
   623 
   624 datatype qualifier = Show | Then | Moreover | Ultimately
   625 
   626 datatype step =
   627   Fix of (string * typ) list |
   628   Let of term * term |
   629   Assume of label * term |
   630   Have of qualifier list * label * term * byline
   631 and byline =
   632   ByMetis of facts |
   633   CaseSplit of step list list * facts
   634 
   635 fun smart_case_split [] facts = ByMetis facts
   636   | smart_case_split proofs facts = CaseSplit (proofs, facts)
   637 
   638 val raw_prefix = "X"
   639 val assum_prefix = "A"
   640 val fact_prefix = "F"
   641 
   642 fun string_for_label (s, num) = s ^ string_of_int num
   643 
   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)))
   647   else
   648     apfst (insert (op =) (raw_prefix, num))
   649 
   650 fun forall_vars t = fold_rev forall_of (map Var (Term.add_vars t [])) t
   651 
   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),
   656           forall_vars t,
   657           ByMetis (fold (add_fact_from_dep thm_names) deps ([], [])))
   658 
   659 fun proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
   660                          atp_proof conjecture_shape thm_names params frees =
   661   let
   662     val lines =
   663       atp_proof ^ "$" (* the $ sign acts as a sentinel *)
   664       |> parse_proof pool
   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)
   670       |> snd
   671   in
   672     (if null params then [] else [Fix params]) @
   673     map2 (step_for_line thm_names) (length lines downto 1) lines
   674   end
   675 
   676 val indent_size = 2
   677 val no_label = ("", ~1)
   678 
   679 fun no_show qs = not (member (op =) qs Show)
   680 
   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)
   687 
   688 fun used_labels_of_step (Have (_, _, _, by)) =
   689     (case by of
   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 []
   695 
   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
   701 
   702 val join_proofs =
   703   let
   704     fun aux _ [] = NONE
   705       | aux proof_tail (proofs as (proof1 :: _)) =
   706         if exists null proofs then
   707           NONE
   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)
   717           else
   718             NONE
   719         | _ => NONE
   720   in aux [] o map rev end
   721 
   722 fun case_split_qualifiers proofs =
   723   case length proofs of
   724     0 => []
   725   | 1 => [Then]
   726   | _ => [Ultimately]
   727 
   728 fun redirect_proof thy conjecture_shape hyp_ts concl_t proof =
   729   let
   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)
   740         else
   741           first_pass (proof, contra) |>> cons (Assume (l, find_hyp num))
   742       | first_pass ((step as Have (qs, l, t, ByMetis (ls, ss))) :: proof,
   743                     contra) =
   744         if exists (member (op =) (fst contra)) ls then
   745           first_pass (proof, contra |>> cons l ||> cons step)
   746         else
   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)
   758                 else
   759                   concl_t,
   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,
   764                             patches) =
   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))
   768         else
   769           (case List.partition (member (op =) contra_ls) ls of
   770              ([contra_l], co_ls) =>
   771              if no_show qs then
   772                second_pass end_qs
   773                            (proof, assums,
   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)
   777                          else
   778                            Have (qs, l, negate_term thy t,
   779                                  ByMetis (backpatch_label patches l)))
   780              else
   781                second_pass end_qs (proof, assums,
   782                                    patches |>> cons (contra_l, (co_ls, ss)))
   783            | (contra_ls as _ :: _, co_ls) =>
   784              let
   785                val proofs =
   786                  map_filter
   787                      (fn l =>
   788                          if member (op =) concl_ls l then
   789                            NONE
   790                          else
   791                            let
   792                              val drop_ls = filter (curry (op <>) l) contra_ls
   793                            in
   794                              second_pass []
   795                                  (proof, assums,
   796                                   patches ||> apfst (insert (op =) l)
   797                                           ||> apsnd (union (op =) drop_ls))
   798                              |> fst |> SOME
   799                            end) contra_ls
   800                val facts = (co_ls, [])
   801              in
   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
   807                 | NONE =>
   808                   [Have (case_split_qualifiers proofs @ end_qs, no_label,
   809                          concl_t, smart_case_split proofs facts)],
   810                 patches)
   811              end
   812            | _ => raise Fail "malformed proof")
   813        | second_pass _ _ = raise Fail "malformed proof"
   814     val proof_bottom =
   815       second_pass [Show] (contra_proof, [], ([], ([], []))) |> fst
   816   in proof_top @ proof_bottom end
   817 
   818 val kill_duplicate_assumptions_in_proof =
   819   let
   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) =
   827         (Have (qs, l, t,
   828                case by of
   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
   835   in do_proof end
   836 
   837 val then_chain_proof =
   838   let
   839     fun aux _ [] = []
   840       | aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof
   841       | aux l' (Have (qs, l, t, by) :: proof) =
   842         (case by of
   843            ByMetis (ls, ss) =>
   844            Have (if member (op =) ls l' then
   845                    (Then :: qs, l, t,
   846                     ByMetis (filter_out (curry (op =) l') ls, ss))
   847                  else
   848                    (qs, l, t, ByMetis (ls, ss)))
   849          | CaseSplit (proofs, facts) =>
   850            Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) ::
   851         aux l proof
   852       | aux _ (step :: proof) = step :: aux no_label proof
   853   in aux no_label end
   854 
   855 fun kill_useless_labels_in_proof proof =
   856   let
   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,
   862               case by of
   863                 CaseSplit (proofs, facts) =>
   864                 CaseSplit (map (map do_step) proofs, facts)
   865               | _ => by)
   866       | do_step step = step
   867   in map do_step proof end
   868 
   869 fun prefix_for_depth n = replicate_string (n + 1)
   870 
   871 val relabel_proof =
   872   let
   873     fun aux _ _ _ [] = []
   874       | aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) =
   875         if l = no_label then
   876           Assume (l, t) :: aux subst depth (next_assum, next_fact) proof
   877         else
   878           let val l' = (prefix_for_depth depth assum_prefix, next_assum) in
   879             Assume (l', t) ::
   880             aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof
   881           end
   882       | aux subst depth (next_assum, next_fact) (Have (qs, l, t, by) :: proof) =
   883         let
   884           val (l', subst, next_fact) =
   885             if l = no_label then
   886               (l, subst, next_fact)
   887             else
   888               let
   889                 val l' = (prefix_for_depth depth fact_prefix, next_fact)
   890               in (l', (l, l') :: subst, next_fact + 1) end
   891           val relabel_facts =
   892             apfst (map (fn l =>
   893                            case AList.lookup (op =) subst l of
   894                              SOME l' => l'
   895                            | NONE => raise Fail ("unknown label " ^
   896                                                  quote (string_for_label l))))
   897           val by =
   898             case by of
   899               ByMetis facts => ByMetis (relabel_facts facts)
   900             | CaseSplit (proofs, facts) =>
   901               CaseSplit (map (aux subst (depth + 1) (1, 1)) proofs,
   902                          relabel_facts facts)
   903         in
   904           Have (qs, l', t, by) ::
   905           aux subst depth (next_assum, next_fact) proof
   906         end
   907       | aux subst depth nextp (step :: proof) =
   908         step :: aux subst depth nextp proof
   909   in aux [] 0 (1, 1) end
   910 
   911 fun string_for_proof ctxt i n =
   912   let
   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) " "
   917     fun do_free (s, T) =
   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 ^ ": "
   921     fun do_have qs =
   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"
   926        else
   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) =
   930       let
   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)) ^
   953         suffix ^ "\n"
   954       end
   955     and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
   956     (* One-step proofs are pointless; better use the Metis one-liner
   957        directly. *)
   958     and do_proof [Have (_, _, _, ByMetis _)] = ""
   959       | do_proof proof =
   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"
   964   in do_proof end
   965 
   966 fun isar_proof_text (pool, debug, full_types, isar_shrink_factor, ctxt,
   967                      conjecture_shape)
   968                     (minimize_command, atp_proof, thm_names, goal, i) =
   969   let
   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
   980                                 frees
   981            |> redirect_proof thy conjecture_shape hyp_ts concl_t
   982            |> kill_duplicate_assumptions_in_proof
   983            |> then_chain_proof
   984            |> kill_useless_labels_in_proof
   985            |> relabel_proof
   986            |> string_for_proof ctxt i n of
   987         "" => ""
   988       | proof => "\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
   989     val isar_proof =
   990       if debug then
   991         isar_proof_for ()
   992       else
   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
   996 
   997 fun proof_text isar_proof isar_params other_params =
   998   (if isar_proof then isar_proof_text isar_params else metis_proof_text)
   999       other_params
  1000 
  1001 end;