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