src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
author blanchet
Tue Nov 06 15:15:33 2012 +0100 (2012-11-06)
changeset 50020 6b9611abcd4c
parent 50019 930a10e674ef
child 50048 fb024bbf4b65
permissions -rw-r--r--
renamed Sledgehammer option
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Author:     Steffen Juilf Smolka, TU Muenchen
     4 
     5 Isar proof reconstruction from ATP proofs.
     6 *)
     7 
     8 signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
     9 sig
    10   type 'a proof = 'a ATP_Proof.proof
    11   type stature = ATP_Problem_Generate.stature
    12 
    13   datatype reconstructor =
    14     Metis of string * string |
    15     SMT
    16 
    17   datatype play =
    18     Played of reconstructor * Time.time |
    19     Trust_Playable of reconstructor * Time.time option |
    20     Failed_to_Play of reconstructor
    21 
    22   type minimize_command = string list -> string
    23   type one_line_params =
    24     play * string * (string * stature) list * minimize_command * int * int
    25   type isar_params =
    26     bool * bool * Time.time * real * string Symtab.table
    27     * (string * stature) list vector * int Symtab.table * string proof * thm
    28 
    29   val smtN : string
    30   val string_for_reconstructor : reconstructor -> string
    31   val thms_of_name : Proof.context -> string -> thm list
    32   val lam_trans_from_atp_proof : string proof -> string -> string
    33   val is_typed_helper_used_in_atp_proof : string proof -> bool
    34   val used_facts_in_atp_proof :
    35     Proof.context -> (string * stature) list vector -> string proof ->
    36     (string * stature) list
    37   val used_facts_in_unsound_atp_proof :
    38     Proof.context -> (string * stature) list vector -> 'a proof ->
    39     string list option
    40   val one_line_proof_text : int -> one_line_params -> string
    41   val isar_proof_text :
    42     Proof.context -> bool -> isar_params -> one_line_params -> string
    43   val proof_text :
    44     Proof.context -> bool -> isar_params -> int -> one_line_params -> string
    45 end;
    46 
    47 structure Sledgehammer_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
    48 struct
    49 
    50 open ATP_Util
    51 open ATP_Problem
    52 open ATP_Proof
    53 open ATP_Problem_Generate
    54 open ATP_Proof_Reconstruct
    55 open Sledgehammer_Util
    56 
    57 structure String_Redirect = ATP_Proof_Redirect(
    58   type key = step_name
    59   val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s')
    60   val string_of = fst)
    61 
    62 open String_Redirect
    63 
    64 
    65 (** reconstructors **)
    66 
    67 datatype reconstructor =
    68   Metis of string * string |
    69   SMT
    70 
    71 datatype play =
    72   Played of reconstructor * Time.time |
    73   Trust_Playable of reconstructor * Time.time option |
    74   Failed_to_Play of reconstructor
    75 
    76 val smtN = "smt"
    77 
    78 fun string_for_reconstructor (Metis (type_enc, lam_trans)) =
    79     metis_call type_enc lam_trans
    80   | string_for_reconstructor SMT = smtN
    81 
    82 fun thms_of_name ctxt name =
    83   let
    84     val lex = Keyword.get_lexicons
    85     val get = maps (Proof_Context.get_fact ctxt o fst)
    86   in
    87     Source.of_string name
    88     |> Symbol.source
    89     |> Token.source {do_recover = SOME false} lex Position.start
    90     |> Token.source_proper
    91     |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
    92     |> Source.exhaust
    93   end
    94 
    95 
    96 (** fact extraction from ATP proofs **)
    97 
    98 fun find_first_in_list_vector vec key =
    99   Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
   100                  | (_, value) => value) NONE vec
   101 
   102 val unprefix_fact_number = space_implode "_" o tl o space_explode "_"
   103 
   104 fun resolve_one_named_fact fact_names s =
   105   case try (unprefix fact_prefix) s of
   106     SOME s' =>
   107     let val s' = s' |> unprefix_fact_number |> unascii_of in
   108       s' |> find_first_in_list_vector fact_names |> Option.map (pair s')
   109     end
   110   | NONE => NONE
   111 fun resolve_fact fact_names = map_filter (resolve_one_named_fact fact_names)
   112 fun is_fact fact_names = not o null o resolve_fact fact_names
   113 
   114 fun resolve_one_named_conjecture s =
   115   case try (unprefix conjecture_prefix) s of
   116     SOME s' => Int.fromString s'
   117   | NONE => NONE
   118 
   119 val resolve_conjecture = map_filter resolve_one_named_conjecture
   120 val is_conjecture = not o null o resolve_conjecture
   121 
   122 val ascii_of_lam_fact_prefix = ascii_of lam_fact_prefix
   123 
   124 (* overapproximation (good enough) *)
   125 fun is_lam_lifted s =
   126   String.isPrefix fact_prefix s andalso
   127   String.isSubstring ascii_of_lam_fact_prefix s
   128 
   129 val is_combinator_def = String.isPrefix (helper_prefix ^ combinator_prefix)
   130 
   131 fun is_axiom_used_in_proof pred =
   132   exists (fn Inference_Step ((_, ss), _, _, _, []) => exists pred ss
   133            | _ => false)
   134 
   135 fun lam_trans_from_atp_proof atp_proof default =
   136   case (is_axiom_used_in_proof is_combinator_def atp_proof,
   137         is_axiom_used_in_proof is_lam_lifted atp_proof) of
   138     (false, false) => default
   139   | (false, true) => liftingN
   140 (*  | (true, true) => combs_and_liftingN -- not supported by "metis" *)
   141   | (true, _) => combsN
   142 
   143 val is_typed_helper_name =
   144   String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix
   145 fun is_typed_helper_used_in_atp_proof atp_proof =
   146   is_axiom_used_in_proof is_typed_helper_name atp_proof
   147 
   148 fun add_non_rec_defs fact_names accum =
   149   Vector.foldl (fn (facts, facts') =>
   150       union (op =) (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts)
   151             facts')
   152     accum fact_names
   153 
   154 val isa_ext = Thm.get_name_hint @{thm ext}
   155 val isa_short_ext = Long_Name.base_name isa_ext
   156 
   157 fun ext_name ctxt =
   158   if Thm.eq_thm_prop (@{thm ext},
   159          singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then
   160     isa_short_ext
   161   else
   162     isa_ext
   163 
   164 val leo2_ext = "extcnf_equal_neg"
   165 val leo2_unfold_def = "unfold_def"
   166 
   167 fun add_fact ctxt fact_names (Inference_Step ((_, ss), _, _, rule, deps)) =
   168     (if rule = leo2_ext then
   169        insert (op =) (ext_name ctxt, (Global, General))
   170      else if rule = leo2_unfold_def then
   171        (* LEO 1.3.3 does not record definitions properly, leading to missing
   172          dependencies in the TSTP proof. Remove the next line once this is
   173          fixed. *)
   174        add_non_rec_defs fact_names
   175      else if rule = satallax_coreN then
   176        (fn [] =>
   177            (* Satallax doesn't include definitions in its unsatisfiable cores,
   178               so we assume the worst and include them all here. *)
   179            [(ext_name ctxt, (Global, General))] |> add_non_rec_defs fact_names
   180          | facts => facts)
   181      else
   182        I)
   183     #> (if null deps then union (op =) (resolve_fact fact_names ss)
   184         else I)
   185   | add_fact _ _ _ = I
   186 
   187 fun used_facts_in_atp_proof ctxt fact_names atp_proof =
   188   if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names
   189   else fold (add_fact ctxt fact_names) atp_proof []
   190 
   191 fun used_facts_in_unsound_atp_proof _ _ [] = NONE
   192   | used_facts_in_unsound_atp_proof ctxt fact_names atp_proof =
   193     let val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof in
   194       if forall (fn (_, (sc, _)) => sc = Global) used_facts andalso
   195          not (is_axiom_used_in_proof (is_conjecture o single) atp_proof) then
   196         SOME (map fst used_facts)
   197       else
   198         NONE
   199     end
   200 
   201 
   202 (** one-liner reconstructor proofs **)
   203 
   204 fun string_for_label (s, num) = s ^ string_of_int num
   205 
   206 fun show_time NONE = ""
   207   | show_time (SOME ext_time) = " (" ^ string_from_ext_time ext_time ^ ")"
   208 
   209 (* FIXME: Various bugs, esp. with "unfolding"
   210 fun unusing_chained_facts _ 0 = ""
   211   | unusing_chained_facts used_chaineds num_chained =
   212     if length used_chaineds = num_chained then ""
   213     else if null used_chaineds then "(* using no facts *) "
   214     else "(* using only " ^ space_implode " " used_chaineds ^ " *) "
   215 *)
   216 
   217 fun apply_on_subgoal _ 1 = "by "
   218   | apply_on_subgoal 1 _ = "apply "
   219   | apply_on_subgoal i n =
   220     "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
   221 
   222 fun using_labels [] = ""
   223   | using_labels ls =
   224     "using " ^ space_implode " " (map string_for_label ls) ^ " "
   225 
   226 fun command_call name [] =
   227     name |> not (Lexicon.is_identifier name) ? enclose "(" ")"
   228   | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
   229 
   230 fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) =
   231   (* unusing_chained_facts used_chaineds num_chained ^ *)
   232   using_labels ls ^ apply_on_subgoal i n ^
   233   command_call (string_for_reconstructor reconstr) ss
   234 
   235 fun try_command_line banner time command =
   236   banner ^ ": " ^ Markup.markup Isabelle_Markup.sendback command ^
   237   show_time time ^ "."
   238 
   239 fun minimize_line _ [] = ""
   240   | minimize_line minimize_command ss =
   241     case minimize_command ss of
   242       "" => ""
   243     | command =>
   244       "\nTo minimize: " ^ Markup.markup Isabelle_Markup.sendback command ^ "."
   245 
   246 fun split_used_facts facts =
   247   facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
   248         |> pairself (sort_distinct (string_ord o pairself fst))
   249 
   250 type minimize_command = string list -> string
   251 type one_line_params =
   252   play * string * (string * stature) list * minimize_command * int * int
   253 
   254 fun one_line_proof_text num_chained
   255         (preplay, banner, used_facts, minimize_command, subgoal,
   256          subgoal_count) =
   257   let
   258     val (chained, extra) = split_used_facts used_facts
   259     val (failed, reconstr, ext_time) =
   260       case preplay of
   261         Played (reconstr, time) => (false, reconstr, (SOME (false, time)))
   262       | Trust_Playable (reconstr, time) =>
   263         (false, reconstr,
   264          case time of
   265            NONE => NONE
   266          | SOME time =>
   267            if time = Time.zeroTime then NONE else SOME (true, time))
   268       | Failed_to_Play reconstr => (true, reconstr, NONE)
   269     val try_line =
   270       ([], map fst extra)
   271       |> reconstructor_command reconstr subgoal subgoal_count (map fst chained)
   272                                num_chained
   273       |> (if failed then
   274             enclose "One-line proof reconstruction failed: "
   275                      ".\n(Invoking \"sledgehammer\" with \"[strict]\" might \
   276                      \solve this.)"
   277           else
   278             try_command_line banner ext_time)
   279   in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end
   280 
   281 
   282 (** Isar proof construction and manipulation **)
   283 
   284 type label = string * int
   285 type facts = label list * string list
   286 
   287 datatype isar_qualifier = Show | Then | Moreover | Ultimately
   288 
   289 datatype isar_step =
   290   Fix of (string * typ) list |
   291   Let of term * term |
   292   Assume of label * term |
   293   Prove of isar_qualifier list * label * term * byline
   294 and byline =
   295   By_Metis of facts |
   296   Case_Split of isar_step list list * facts
   297 
   298 val assume_prefix = "a"
   299 val have_prefix = "f"
   300 val raw_prefix = "x"
   301 
   302 fun raw_label_for_name (num, ss) =
   303   case resolve_conjecture ss of
   304     [j] => (conjecture_prefix, j)
   305   | _ => (raw_prefix ^ ascii_of num, 0)
   306 
   307 fun label_of_clause [name] = raw_label_for_name name
   308   | label_of_clause c = (space_implode "___" (map fst c), 0)
   309 
   310 fun add_fact_from_dependencies fact_names (names as [(_, ss)]) =
   311     if is_fact fact_names ss then
   312       apsnd (union (op =) (map fst (resolve_fact fact_names ss)))
   313     else
   314       apfst (insert (op =) (label_of_clause names))
   315   | add_fact_from_dependencies fact_names names =
   316     apfst (insert (op =) (label_of_clause names))
   317 
   318 fun repair_name "$true" = "c_True"
   319   | repair_name "$false" = "c_False"
   320   | repair_name "$$e" = tptp_equal (* seen in Vampire proofs *)
   321   | repair_name s =
   322     if is_tptp_equal s orelse
   323        (* seen in Vampire proofs *)
   324        (String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s) then
   325       tptp_equal
   326     else
   327       s
   328 
   329 fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
   330   | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
   331 
   332 fun infer_formula_types ctxt =
   333   Type.constraint HOLogic.boolT
   334   #> Syntax.check_term
   335          (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
   336 
   337 val combinator_table =
   338   [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def [abs_def]}),
   339    (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def [abs_def]}),
   340    (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def [abs_def]}),
   341    (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def [abs_def]}),
   342    (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def [abs_def]})]
   343 
   344 fun uncombine_term thy =
   345   let
   346     fun aux (t1 $ t2) = betapply (pairself aux (t1, t2))
   347       | aux (Abs (s, T, t')) = Abs (s, T, aux t')
   348       | aux (t as Const (x as (s, _))) =
   349         (case AList.lookup (op =) combinator_table s of
   350            SOME thm => thm |> prop_of |> specialize_type thy x
   351                            |> Logic.dest_equals |> snd
   352          | NONE => t)
   353       | aux t = t
   354   in aux end
   355 
   356 fun decode_line sym_tab (Definition_Step (name, phi1, phi2)) ctxt =
   357     let
   358       val thy = Proof_Context.theory_of ctxt
   359       val t1 = prop_from_atp ctxt true sym_tab phi1
   360       val vars = snd (strip_comb t1)
   361       val frees = map unvarify_term vars
   362       val unvarify_args = subst_atomic (vars ~~ frees)
   363       val t2 = prop_from_atp ctxt true sym_tab phi2
   364       val (t1, t2) =
   365         HOLogic.eq_const HOLogic.typeT $ t1 $ t2
   366         |> unvarify_args |> uncombine_term thy |> infer_formula_types ctxt
   367         |> HOLogic.dest_eq
   368     in
   369       (Definition_Step (name, t1, t2),
   370        fold Variable.declare_term (maps Misc_Legacy.term_frees [t1, t2]) ctxt)
   371     end
   372   | decode_line sym_tab (Inference_Step (name, role, u, rule, deps)) ctxt =
   373     let
   374       val thy = Proof_Context.theory_of ctxt
   375       val t = u |> prop_from_atp ctxt true sym_tab
   376                 |> uncombine_term thy |> infer_formula_types ctxt
   377     in
   378       (Inference_Step (name, role, t, rule, deps),
   379        fold Variable.declare_term (Misc_Legacy.term_frees t) ctxt)
   380     end
   381 fun decode_lines ctxt sym_tab lines =
   382   fst (fold_map (decode_line sym_tab) lines ctxt)
   383 
   384 fun replace_one_dependency (old, new) dep =
   385   if is_same_atp_step dep old then new else [dep]
   386 fun replace_dependencies_in_line _ (line as Definition_Step _) = line
   387   | replace_dependencies_in_line p
   388         (Inference_Step (name, role, t, rule, deps)) =
   389     Inference_Step (name, role, t, rule,
   390                     fold (union (op =) o replace_one_dependency p) deps [])
   391 
   392 (* No "real" literals means only type information (tfree_tcs, clsrel, or
   393    clsarity). *)
   394 fun is_only_type_information t = t aconv @{term True}
   395 
   396 fun is_same_inference _ (Definition_Step _) = false
   397   | is_same_inference t (Inference_Step (_, _, t', _, _)) = t aconv t'
   398 
   399 (* Discard facts; consolidate adjacent lines that prove the same formula, since
   400    they differ only in type information.*)
   401 fun add_line _ (line as Definition_Step _) lines = line :: lines
   402   | add_line fact_names (Inference_Step (name as (_, ss), role, t, rule, []))
   403              lines =
   404     (* No dependencies: fact, conjecture, or (for Vampire) internal facts or
   405        definitions. *)
   406     if is_fact fact_names ss then
   407       (* Facts are not proof lines. *)
   408       if is_only_type_information t then
   409         map (replace_dependencies_in_line (name, [])) lines
   410       (* Is there a repetition? If so, replace later line by earlier one. *)
   411       else case take_prefix (not o is_same_inference t) lines of
   412         (_, []) => lines (* no repetition of proof line *)
   413       | (pre, Inference_Step (name', _, _, _, _) :: post) =>
   414         pre @ map (replace_dependencies_in_line (name', [name])) post
   415       | _ => raise Fail "unexpected inference"
   416     else if is_conjecture ss then
   417       Inference_Step (name, role, t, rule, []) :: lines
   418     else
   419       map (replace_dependencies_in_line (name, [])) lines
   420   | add_line _ (Inference_Step (name, role, t, rule, deps)) lines =
   421     (* Type information will be deleted later; skip repetition test. *)
   422     if is_only_type_information t then
   423       Inference_Step (name, role, t, rule, deps) :: lines
   424     (* Is there a repetition? If so, replace later line by earlier one. *)
   425     else case take_prefix (not o is_same_inference t) lines of
   426       (* FIXME: Doesn't this code risk conflating proofs involving different
   427          types? *)
   428        (_, []) => Inference_Step (name, role, t, rule, deps) :: lines
   429      | (pre, Inference_Step (name', role, t', rule, _) :: post) =>
   430        Inference_Step (name, role, t', rule, deps) ::
   431        pre @ map (replace_dependencies_in_line (name', [name])) post
   432      | _ => raise Fail "unexpected inference"
   433 
   434 val waldmeister_conjecture_num = "1.0.0.0"
   435 
   436 val repair_waldmeister_endgame =
   437   let
   438     fun do_tail (Inference_Step (name, role, t, rule, deps)) =
   439         Inference_Step (name, role, s_not t, rule, deps)
   440       | do_tail line = line
   441     fun do_body [] = []
   442       | do_body ((line as Inference_Step ((num, _), _, _, _, _)) :: lines) =
   443         if num = waldmeister_conjecture_num then map do_tail (line :: lines)
   444         else line :: do_body lines
   445       | do_body (line :: lines) = line :: do_body lines
   446   in do_body end
   447 
   448 (* Recursively delete empty lines (type information) from the proof. *)
   449 fun add_nontrivial_line (line as Inference_Step (name, _, t, _, [])) lines =
   450     if is_only_type_information t then delete_dependency name lines
   451     else line :: lines
   452   | add_nontrivial_line line lines = line :: lines
   453 and delete_dependency name lines =
   454   fold_rev add_nontrivial_line
   455            (map (replace_dependencies_in_line (name, [])) lines) []
   456 
   457 (* ATPs sometimes reuse free variable names in the strangest ways. Removing
   458    offending lines often does the trick. *)
   459 fun is_bad_free frees (Free x) = not (member (op =) frees x)
   460   | is_bad_free _ _ = false
   461 
   462 fun add_desired_line _ _ (line as Definition_Step (name, _, _)) (j, lines) =
   463     (j, line :: map (replace_dependencies_in_line (name, [])) lines)
   464   | add_desired_line fact_names frees
   465         (Inference_Step (name as (_, ss), role, t, rule, deps)) (j, lines) =
   466     (j + 1,
   467      if is_fact fact_names ss orelse
   468         is_conjecture ss orelse
   469         (* the last line must be kept *)
   470         j = 0 orelse
   471         (not (is_only_type_information t) andalso
   472          null (Term.add_tvars t []) andalso
   473          not (exists_subterm (is_bad_free frees) t) andalso
   474          length deps >= 2 andalso
   475          (* kill next to last line, which usually results in a trivial step *)
   476          j <> 1) then
   477        Inference_Step (name, role, t, rule, deps) :: lines  (* keep line *)
   478      else
   479        map (replace_dependencies_in_line (name, deps)) lines)  (* drop line *)
   480 
   481 (** Type annotations **)
   482 
   483 fun post_traverse_term_type' f _ (t as Const (_, T)) s = f t T s
   484   | post_traverse_term_type' f _ (t as Free (_, T)) s = f t T s
   485   | post_traverse_term_type' f _ (t as Var (_, T)) s = f t T s
   486   | post_traverse_term_type' f env (t as Bound i) s = f t (nth env i) s
   487   | post_traverse_term_type' f env (Abs (x, T1, b)) s =
   488     let
   489       val ((b', s'), T2) = post_traverse_term_type' f (T1 :: env) b s
   490     in f (Abs (x, T1, b')) (T1 --> T2) s' end
   491   | post_traverse_term_type' f env (u $ v) s =
   492     let
   493       val ((u', s'), Type (_, [_, T])) = post_traverse_term_type' f env u s
   494       val ((v', s''), _) = post_traverse_term_type' f env v s'
   495     in f (u' $ v') T s'' end
   496 
   497 fun post_traverse_term_type f s t =
   498   post_traverse_term_type' (fn t => fn T => fn s => (f t T s, T)) [] t s |> fst
   499 fun post_fold_term_type f s t =
   500   post_traverse_term_type (fn t => fn T => fn s => (t, f t T s)) s t |> snd
   501 
   502 (* Data structures, orders *)
   503 val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord)
   504 
   505 structure Var_Set_Tab = Table(
   506   type key = indexname list
   507   val ord = list_ord Term_Ord.fast_indexname_ord)
   508 
   509 (* (1) Generalize Types *)
   510 fun generalize_types ctxt t =
   511   t |> map_types (fn _ => dummyT)
   512     |> Syntax.check_term
   513          (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
   514 
   515 (* (2) Typing-spot Table *)
   516 local
   517 fun key_of_atype (TVar (z, _)) =
   518     Ord_List.insert Term_Ord.fast_indexname_ord z
   519   | key_of_atype _ = I
   520 fun key_of_type T = fold_atyps key_of_atype T []
   521 fun update_tab t T (tab, pos) =
   522   (case key_of_type T of
   523      [] => tab
   524    | key =>
   525      let val cost = (size_of_typ T, (size_of_term t, pos)) in
   526        case Var_Set_Tab.lookup tab key of
   527          NONE => Var_Set_Tab.update_new (key, cost) tab
   528        | SOME old_cost =>
   529          (case cost_ord (cost, old_cost) of
   530             LESS => Var_Set_Tab.update (key, cost) tab
   531           | _ => tab)
   532      end,
   533    pos + 1)
   534 in
   535 val typing_spot_table =
   536   post_fold_term_type update_tab (Var_Set_Tab.empty, 0) #> fst
   537 end
   538 
   539 (* (3) Reverse-Greedy *)
   540 fun reverse_greedy typing_spot_tab =
   541   let
   542     fun update_count z =
   543       fold (fn tvar => fn tab =>
   544         let val c = Vartab.lookup tab tvar |> the_default 0 in
   545           Vartab.update (tvar, c + z) tab
   546         end)
   547     fun superfluous tcount =
   548       forall (fn tvar => the (Vartab.lookup tcount tvar) > 1)
   549     fun drop_superfluous (tvars, (_, (_, spot))) (spots, tcount) =
   550       if superfluous tcount tvars then (spots, update_count ~1 tvars tcount)
   551       else (spot :: spots, tcount)
   552     val (typing_spots, tvar_count_tab) =
   553       Var_Set_Tab.fold
   554         (fn kv as (k, _) => apfst (cons kv) #> apsnd (update_count 1 k))
   555         typing_spot_tab ([], Vartab.empty)
   556       |>> sort_distinct (rev_order o cost_ord o pairself snd)
   557   in fold drop_superfluous typing_spots ([], tvar_count_tab) |> fst end
   558 
   559 (* (4) Introduce Annotations *)
   560 fun introduce_annotations thy spots t t' =
   561   let
   562     val get_types = post_fold_term_type (K cons) []
   563     fun match_types tp =
   564       fold (Sign.typ_match thy) (op ~~ (pairself get_types tp)) Vartab.empty
   565     fun unica' b x [] = if b then [x] else []
   566       | unica' b x (y :: ys) =
   567         if x = y then unica' false x ys
   568         else unica' true y ys |> b ? cons x
   569     fun unica ord xs =
   570       case sort ord xs of x :: ys => unica' true x ys | [] => []
   571     val add_all_tfree_namesT = fold_atyps (fn TFree (x, _) => cons x | _ => I)
   572     fun erase_unica_tfrees env =
   573       let
   574         val unica =
   575           Vartab.fold (add_all_tfree_namesT o snd o snd) env []
   576           |> unica fast_string_ord
   577         val erase_unica = map_atyps
   578           (fn T as TFree (s, _) =>
   579               if Ord_List.member fast_string_ord unica s then dummyT else T
   580             | T => T)
   581       in Vartab.map (K (apsnd erase_unica)) env end
   582     val env = match_types (t', t) |> erase_unica_tfrees
   583     fun get_annot env (TFree _) = (false, (env, dummyT))
   584       | get_annot env (T as TVar (v, S)) =
   585         let val T' = Envir.subst_type env T in
   586           if T' = dummyT then (false, (env, dummyT))
   587           else (true, (Vartab.update (v, (S, dummyT)) env, T'))
   588         end
   589       | get_annot env (Type (S, Ts)) =
   590         (case fold_rev (fn T => fn (b, (env, Ts)) =>
   591                   let
   592                     val (b', (env', T)) = get_annot env T
   593                   in (b orelse b', (env', T :: Ts)) end)
   594                 Ts (false, (env, [])) of
   595            (true, (env', Ts)) => (true, (env', Type (S, Ts)))
   596          | (false, (env', _)) => (false, (env', dummyT)))
   597     fun post1 _ T (env, cp, ps as p :: ps', annots) =
   598         if p <> cp then
   599           (env, cp + 1, ps, annots)
   600         else
   601           let val (_, (env', T')) = get_annot env T in
   602             (env', cp + 1, ps', (p, T') :: annots)
   603           end
   604       | post1 _ _ accum = accum
   605     val (_, _, _, annots) = post_fold_term_type post1 (env, 0, spots, []) t'
   606     fun post2 t _ (cp, annots as (p, T) :: annots') =
   607         if p <> cp then (t, (cp + 1, annots))
   608         else (Type.constraint T t, (cp + 1, annots'))
   609       | post2 t _ x = (t, x)
   610   in post_traverse_term_type post2 (0, rev annots) t |> fst end
   611 
   612 (* (5) Annotate *)
   613 fun annotate_types ctxt t =
   614   let
   615     val thy = Proof_Context.theory_of ctxt
   616     val t' = generalize_types ctxt t
   617     val typing_spots =
   618       t' |> typing_spot_table
   619          |> reverse_greedy
   620          |> sort int_ord
   621   in introduce_annotations thy typing_spots t t' end
   622 
   623 val indent_size = 2
   624 val no_label = ("", ~1)
   625 
   626 fun string_for_proof ctxt type_enc lam_trans i n =
   627   let
   628     fun fix_print_mode f x =
   629       Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
   630                                (print_mode_value ())) f x
   631     fun do_indent ind = replicate_string (ind * indent_size) " "
   632     fun do_free (s, T) =
   633       maybe_quote s ^ " :: " ^
   634       maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
   635     fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
   636     fun do_have qs =
   637       (if member (op =) qs Moreover then "moreover " else "") ^
   638       (if member (op =) qs Ultimately then "ultimately " else "") ^
   639       (if member (op =) qs Then then
   640          if member (op =) qs Show then "thus" else "hence"
   641        else
   642          if member (op =) qs Show then "show" else "have")
   643     val do_term =
   644       maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
   645       o annotate_types ctxt
   646     val reconstr = Metis (type_enc, lam_trans)
   647     fun do_facts ind (ls, ss) =
   648       "\n" ^ do_indent (ind + 1) ^
   649       reconstructor_command reconstr 1 1 [] 0
   650           (ls |> sort_distinct (prod_ord string_ord int_ord),
   651            ss |> sort_distinct string_ord)
   652     and do_step ind (Fix xs) =
   653         do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
   654       | do_step ind (Let (t1, t2)) =
   655         do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
   656       | do_step ind (Assume (l, t)) =
   657         do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
   658       | do_step ind (Prove (qs, l, t, By_Metis facts)) =
   659         do_indent ind ^ do_have qs ^ " " ^
   660         do_label l ^ do_term t ^ do_facts ind facts ^ "\n"
   661       | do_step ind (Prove (qs, l, t, Case_Split (proofs, facts))) =
   662         implode (map (prefix (do_indent ind ^ "moreover\n") o do_block ind)
   663                      proofs) ^
   664         do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^
   665         do_facts ind facts ^ "\n"
   666     and do_steps prefix suffix ind steps =
   667       let val s = implode (map (do_step ind) steps) in
   668         replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
   669         String.extract (s, ind * indent_size,
   670                         SOME (size s - ind * indent_size - 1)) ^
   671         suffix ^ "\n"
   672       end
   673     and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
   674     (* One-step proofs are pointless; better use the Metis one-liner
   675        directly. *)
   676     and do_proof [Prove (_, _, _, By_Metis _)] = ""
   677       | do_proof proof =
   678         (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
   679         do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^
   680         (if n <> 1 then "next" else "qed")
   681   in do_proof end
   682 
   683 fun used_labels_of_step (Prove (_, _, _, by)) =
   684     (case by of
   685        By_Metis (ls, _) => ls
   686      | Case_Split (proofs, (ls, _)) =>
   687        fold (union (op =) o used_labels_of) proofs ls)
   688   | used_labels_of_step _ = []
   689 and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []
   690 
   691 fun kill_useless_labels_in_proof proof =
   692   let
   693     val used_ls = used_labels_of proof
   694     fun do_label l = if member (op =) used_ls l then l else no_label
   695     fun do_step (Assume (l, t)) = Assume (do_label l, t)
   696       | do_step (Prove (qs, l, t, by)) =
   697         Prove (qs, do_label l, t,
   698                case by of
   699                  Case_Split (proofs, facts) =>
   700                  Case_Split (map (map do_step) proofs, facts)
   701                | _ => by)
   702       | do_step step = step
   703   in map do_step proof end
   704 
   705 fun prefix_for_depth n = replicate_string (n + 1)
   706 
   707 val relabel_proof =
   708   let
   709     fun aux _ _ _ [] = []
   710       | aux subst depth (next_assum, next_have) (Assume (l, t) :: proof) =
   711         if l = no_label then
   712           Assume (l, t) :: aux subst depth (next_assum, next_have) proof
   713         else
   714           let val l' = (prefix_for_depth depth assume_prefix, next_assum) in
   715             Assume (l', t) ::
   716             aux ((l, l') :: subst) depth (next_assum + 1, next_have) proof
   717           end
   718       | aux subst depth (next_assum, next_have)
   719             (Prove (qs, l, t, by) :: proof) =
   720         let
   721           val (l', subst, next_have) =
   722             if l = no_label then
   723               (l, subst, next_have)
   724             else
   725               let val l' = (prefix_for_depth depth have_prefix, next_have) in
   726                 (l', (l, l') :: subst, next_have + 1)
   727               end
   728           val relabel_facts =
   729             apfst (maps (the_list o AList.lookup (op =) subst))
   730           val by =
   731             case by of
   732               By_Metis facts => By_Metis (relabel_facts facts)
   733             | Case_Split (proofs, facts) =>
   734               Case_Split (map (aux subst (depth + 1) (1, 1)) proofs,
   735                           relabel_facts facts)
   736         in
   737           Prove (qs, l', t, by) :: aux subst depth (next_assum, next_have) proof
   738         end
   739       | aux subst depth nextp (step :: proof) =
   740         step :: aux subst depth nextp proof
   741   in aux [] 0 (1, 1) end
   742 
   743 val merge_timeout_slack = 1.2
   744 
   745 val label_ord = prod_ord int_ord fast_string_ord o pairself swap
   746 
   747 structure Label_Table = Table(
   748   type key = label
   749   val ord = label_ord)
   750 
   751 fun shrink_proof debug ctxt type_enc lam_trans preplay preplay_timeout
   752                  isar_shrink proof =
   753   let
   754     (* clean vector interface *)
   755     fun get i v = Vector.sub (v, i)
   756     fun replace x i v = Vector.update (v, i, x)
   757     fun update f i v = replace (get i v |> f) i v
   758     fun v_fold_index f v s =
   759       Vector.foldl (fn (x, (i, s)) => (i+1, f (i, x) s)) (0, s) v |> snd
   760 
   761     (* Queue interface to table *)
   762     fun pop tab key =
   763       let val v = hd (Inttab.lookup_list tab key) in
   764         (v, Inttab.remove_list (op =) (key, v) tab)
   765       end
   766     fun pop_max tab = pop tab (the (Inttab.max_key tab))
   767     val is_empty = Inttab.is_empty
   768     fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab
   769 
   770     (* proof vector *)
   771     val proof_vect = proof |> map SOME |> Vector.fromList
   772     val n = Vector.length proof_vect
   773     val n_target = Real.fromInt n / isar_shrink |> Real.round
   774 
   775     (* table for mapping from label to proof position *)
   776     fun update_table (i, Prove (_, label, _, _)) =
   777         Label_Table.update_new (label, i)
   778       | update_table _ = I
   779     val label_index_table = fold_index update_table proof Label_Table.empty
   780 
   781     (* proof references *)
   782     fun refs (Prove (_, _, _, By_Metis (refs, _))) =
   783       map (the o Label_Table.lookup label_index_table) refs
   784       | refs _ = []
   785     val refed_by_vect =
   786       Vector.tabulate (n, (fn _ => []))
   787       |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) proof
   788       |> Vector.map rev (* after rev, indices are sorted in ascending order *)
   789 
   790     (* candidates for elimination, use table as priority queue (greedy
   791        algorithm) *)
   792     fun cost (Prove (_, _ , t, _)) = Term.size_of_term t
   793       | cost _ = 0
   794     val cand_ord =  rev_order o prod_ord int_ord int_ord
   795     val cand_tab =
   796       v_fold_index
   797         (fn (i, [_]) => cons (get i proof_vect |> the |> cost, i)
   798         | _ => I) refed_by_vect []
   799       |> Inttab.make_list
   800 
   801     (* Enrich context with local facts *)
   802     val thy = Proof_Context.theory_of ctxt
   803     fun enrich_ctxt' (Prove (_, label, t, _)) ctxt =
   804         Proof_Context.put_thms false
   805             (string_for_label label, SOME [Skip_Proof.make_thm thy t]) ctxt
   806       | enrich_ctxt' _ ctxt = ctxt
   807     val rich_ctxt = fold enrich_ctxt' proof ctxt
   808 
   809     (* Timing *)
   810     fun take_time timeout tac arg =
   811       let val timing = Timing.start () in
   812         (TimeLimit.timeLimit timeout tac arg;
   813          Timing.result timing |> #cpu |> SOME)
   814         handle _ => NONE
   815       end
   816     val sum_up_time =
   817       Vector.foldl
   818         ((fn (SOME t, (b, s)) => (b, t + s)
   819            | (NONE, (_, s)) => (true, preplay_timeout + s)) o apfst Lazy.force)
   820         (false, seconds 0.0)
   821 
   822     (* Metis Preplaying *)
   823     fun try_metis timeout (Prove (_, _, t, By_Metis fact_names)) =
   824       if not preplay then (fn () => SOME (seconds 0.0)) else
   825         let
   826           val facts =
   827             fact_names
   828             |>> map string_for_label |> op @
   829             |> map (the_single o thms_of_name rich_ctxt)
   830           val goal =
   831             Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t
   832           fun tac {context = ctxt, prems = _} =
   833             Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1
   834         in
   835           take_time timeout (fn () => goal tac)
   836         end
   837 
   838     (* Lazy metis time vector, cache *)
   839     val metis_time =
   840       Vector.map (Lazy.lazy o try_metis preplay_timeout o the) proof_vect
   841 
   842     (* Merging *)
   843     fun merge (Prove (qs1, label1, _, By_Metis (lfs1, gfs1)))
   844               (Prove (qs2, label2 , t, By_Metis (lfs2, gfs2))) =
   845       let
   846         val qs = inter (op =) qs1 qs2 (* FIXME: Is this correct? *)
   847           |> member (op =) (union (op =) qs1 qs2) Ultimately ? cons Ultimately
   848           |> member (op =) qs2 Show ? cons Show
   849         val ls = remove (op =) label1 lfs2 |> union (op =) lfs1
   850         val ss = union (op =) gfs1 gfs2
   851       in Prove (qs, label2, t, By_Metis (ls, ss)) end
   852     fun try_merge metis_time (s1, i) (s2, j) =
   853       (case get i metis_time |> Lazy.force of
   854         NONE => (NONE, metis_time)
   855       | SOME t1 =>
   856         (case get j metis_time |> Lazy.force of
   857           NONE => (NONE, metis_time)
   858         | SOME t2 =>
   859           let
   860             val s12 = merge s1 s2
   861             val timeout =
   862               t1 + t2 |> Time.toReal |> curry Real.* merge_timeout_slack
   863                       |> Time.fromReal
   864           in
   865             case try_metis timeout s12 () of
   866               NONE => (NONE, metis_time)
   867             | some_t12 =>
   868               (SOME s12, metis_time
   869                          |> replace (seconds 0.0 |> SOME |> Lazy.value) i
   870                          |> replace (Lazy.value some_t12) j)
   871 
   872           end))
   873 
   874     fun merge_steps metis_time proof_vect refed_by cand_tab n' =
   875       if is_empty cand_tab orelse n' <= n_target orelse n'<3 then
   876         (sum_up_time metis_time,
   877          Vector.foldr
   878            (fn (NONE, proof) => proof | (SOME s, proof) => s :: proof)
   879            [] proof_vect)
   880       else
   881         let
   882           val (i, cand_tab) = pop_max cand_tab
   883           val j = get i refed_by |> the_single
   884           val s1 = get i proof_vect |> the
   885           val s2 = get j proof_vect |> the
   886         in
   887           case try_merge metis_time (s1, i) (s2, j) of
   888             (NONE, metis_time) =>
   889             merge_steps metis_time proof_vect refed_by cand_tab n'
   890           | (s, metis_time) => let
   891             val refs = refs s1
   892             val refed_by = refed_by |> fold
   893               (update (Ord_List.remove int_ord i #> Ord_List.insert int_ord j)) refs
   894             val new_candidates =
   895               fold (fn (i, [_]) => cons (cost (get i proof_vect |> the), i)
   896                      | _ => I)
   897                 (map (fn i => (i, get i refed_by)) refs) []
   898             val cand_tab = add_list cand_tab new_candidates
   899             val proof_vect = proof_vect |> replace NONE i |> replace s j
   900           in
   901             merge_steps metis_time proof_vect refed_by cand_tab (n' - 1)
   902           end
   903         end
   904   in
   905     merge_steps metis_time proof_vect refed_by_vect cand_tab n
   906   end
   907 
   908 val chain_direct_proof =
   909   let
   910     fun succedent_of_step (Prove (_, label, _, _)) = SOME label
   911       | succedent_of_step (Assume (label, _)) = SOME label
   912       | succedent_of_step _ = NONE
   913     fun chain_inf (SOME label0)
   914                   (step as Prove (qs, label, t, By_Metis (lfs, gfs))) =
   915         if member (op =) lfs label0 then
   916           Prove (Then :: qs, label, t,
   917                  By_Metis (filter_out (curry (op =) label0) lfs, gfs))
   918         else
   919           step
   920       | chain_inf _ (Prove (qs, label, t, Case_Split (proofs, facts))) =
   921         Prove (qs, label, t, Case_Split ((map (chain_proof NONE) proofs), facts))
   922       | chain_inf _ step = step
   923     and chain_proof _ [] = []
   924       | chain_proof (prev as SOME _) (i :: is) =
   925         chain_inf prev i :: chain_proof (succedent_of_step i) is
   926       | chain_proof _ (i :: is) =
   927         i :: chain_proof (succedent_of_step i) is
   928   in chain_proof NONE end
   929 
   930 type isar_params =
   931   bool * bool * Time.time * real * string Symtab.table
   932   * (string * stature) list vector * int Symtab.table * string proof * thm
   933 
   934 fun isar_proof_text ctxt isar_proofs
   935     (debug, verbose, preplay_timeout, isar_shrink, pool, fact_names, sym_tab,
   936      atp_proof, goal)
   937     (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
   938   let
   939     val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
   940     val frees = fold Term.add_frees (concl_t :: hyp_ts) []
   941     val one_line_proof = one_line_proof_text 0 one_line_params
   942     val type_enc =
   943       if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
   944       else partial_typesN
   945     val lam_trans = lam_trans_from_atp_proof atp_proof metis_default_lam_trans
   946     val preplay = preplay_timeout <> seconds 0.0
   947 
   948     fun isar_proof_of () =
   949       let
   950         val atp_proof =
   951           atp_proof
   952           |> clean_up_atp_proof_dependencies
   953           |> nasty_atp_proof pool
   954           |> map_term_names_in_atp_proof repair_name
   955           |> decode_lines ctxt sym_tab
   956           |> rpair [] |-> fold_rev (add_line fact_names)
   957           |> repair_waldmeister_endgame
   958           |> rpair [] |-> fold_rev add_nontrivial_line
   959           |> rpair (0, [])
   960           |-> fold_rev (add_desired_line fact_names frees)
   961           |> snd
   962         val conj_name = conjecture_prefix ^ string_of_int (length hyp_ts)
   963         val conjs =
   964           atp_proof |> map_filter
   965             (fn Inference_Step (name as (_, ss), _, _, _, []) =>
   966                 if member (op =) ss conj_name then SOME name else NONE
   967               | _ => NONE)
   968         val assms =
   969           atp_proof |> map_filter
   970             (fn Inference_Step (name as (_, ss), _, _, _, []) =>
   971                 (case resolve_conjecture ss of
   972                    [j] =>
   973                    if j = length hyp_ts then NONE
   974                    else SOME (Assume (raw_label_for_name name, nth hyp_ts j))
   975                  | _ => NONE)
   976               | _ => NONE)
   977         fun dep_of_step (Definition_Step _) = NONE
   978           | dep_of_step (Inference_Step (name, _, _, _, from)) =
   979             SOME (from, name)
   980         val ref_graph = atp_proof |> map_filter dep_of_step |> make_ref_graph
   981         val axioms = axioms_of_ref_graph ref_graph conjs
   982         val tainted = tainted_atoms_of_ref_graph ref_graph conjs
   983         val props =
   984           Symtab.empty
   985           |> fold (fn Definition_Step _ => I (* FIXME *)
   986                     | Inference_Step (name as (s, ss), role, t, _, _) =>
   987                       Symtab.update_new (s,
   988                         if member (op = o apsnd fst) tainted s then
   989                           t |> role <> Conjecture ? s_not
   990                             |> fold exists_of (map Var (Term.add_vars t []))
   991                         else
   992                           t))
   993                   atp_proof
   994         (* The assumptions and conjecture are props; the rest are bools. *)
   995         fun prop_of_clause [name as (s, ss)] =
   996             (case resolve_conjecture ss of
   997                [j] => if j = length hyp_ts then concl_t else nth hyp_ts j
   998              | _ => the_default @{term False} (Symtab.lookup props s)
   999                     |> HOLogic.mk_Trueprop |> close_form)
  1000           | prop_of_clause names =
  1001             let val lits = map_filter (Symtab.lookup props o fst) names in
  1002               case List.partition (can HOLogic.dest_not) lits of
  1003                 (negs as _ :: _, pos as _ :: _) =>
  1004                 HOLogic.mk_imp
  1005                   (Library.foldr1 s_conj (map HOLogic.dest_not negs),
  1006                    Library.foldr1 s_disj pos)
  1007               | _ => fold (curry s_disj) lits @{term False}
  1008             end
  1009             |> HOLogic.mk_Trueprop |> close_form
  1010         fun maybe_show outer c =
  1011           (outer andalso length c = 1 andalso subset (op =) (c, conjs))
  1012           ? cons Show
  1013         fun do_have outer qs (gamma, c) =
  1014           Prove (maybe_show outer c qs, label_of_clause c, prop_of_clause c,
  1015                  By_Metis (fold (add_fact_from_dependencies fact_names) gamma
  1016                                 ([], [])))
  1017         fun do_inf outer (Have z) = do_have outer [] z
  1018           | do_inf outer (Cases cases) =
  1019             let val c = succedent_of_cases cases in
  1020               Prove (maybe_show outer c [Ultimately], label_of_clause c,
  1021                      prop_of_clause c,
  1022                      Case_Split (map (do_case false) cases, ([], [])))
  1023             end
  1024         and do_case outer (c, infs) =
  1025           Assume (label_of_clause c, prop_of_clause c) ::
  1026           map (do_inf outer) infs
  1027         val (ext_time, isar_proof) =
  1028           ref_graph
  1029           |> redirect_graph axioms tainted
  1030           |> map (do_inf true)
  1031           |> append assms
  1032           |> shrink_proof debug ctxt type_enc lam_trans preplay
  1033                  preplay_timeout (if isar_proofs then isar_shrink else 1000.0)
  1034        (* ||> reorder_proof_to_minimize_jumps (* ? *) *)
  1035           ||> chain_direct_proof
  1036           ||> kill_useless_labels_in_proof
  1037           ||> relabel_proof
  1038           ||> not (null params) ? cons (Fix params)
  1039         val num_steps = length isar_proof
  1040         val isar_text =
  1041           string_for_proof ctxt type_enc lam_trans subgoal subgoal_count
  1042                            isar_proof
  1043       in
  1044         case isar_text of
  1045           "" =>
  1046           if isar_proofs then
  1047             "\nNo structured proof available (proof too short)."
  1048           else
  1049             ""
  1050         | _ =>
  1051           "\n\nStructured proof" ^
  1052           (if verbose then
  1053              " (" ^ string_of_int num_steps ^ " step" ^ plural_s num_steps ^
  1054              (if preplay then ", " ^ string_from_ext_time ext_time
  1055               else "") ^ ")"
  1056            else if preplay then
  1057              " (" ^ string_from_ext_time ext_time ^ ")"
  1058            else
  1059              "") ^ ":\n" ^ Markup.markup Isabelle_Markup.sendback isar_text
  1060       end
  1061     val isar_proof =
  1062       if debug then
  1063         isar_proof_of ()
  1064       else case try isar_proof_of () of
  1065         SOME s => s
  1066       | NONE => if isar_proofs then
  1067                   "\nWarning: The Isar proof construction failed."
  1068                 else
  1069                   ""
  1070   in one_line_proof ^ isar_proof end
  1071 
  1072 fun proof_text ctxt isar_proofs isar_params num_chained
  1073                (one_line_params as (preplay, _, _, _, _, _)) =
  1074   (if case preplay of Failed_to_Play _ => true | _ => isar_proofs then
  1075      isar_proof_text ctxt isar_proofs isar_params
  1076    else
  1077      one_line_proof_text num_chained) one_line_params
  1078 
  1079 end;