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