src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
author blanchet
Thu Nov 21 12:29:29 2013 +0100 (2013-11-21 ago)
changeset 54546 8b403a7a8c44
parent 54535 59737a43e044
child 54699 65c4fd04b5b2
permissions -rw-r--r--
fixed spying so that the envirnoment variables are queried at run-time not at build-time
blanchet@49883
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
blanchet@49883
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@49883
     3
    Author:     Steffen Juilf Smolka, TU Muenchen
blanchet@49883
     4
blanchet@49914
     5
Isar proof reconstruction from ATP proofs.
blanchet@49883
     6
*)
blanchet@49883
     7
blanchet@52374
     8
signature SLEDGEHAMMER_RECONSTRUCT =
blanchet@49883
     9
sig
blanchet@54495
    10
  type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
blanchet@53586
    11
  type 'a atp_proof = 'a ATP_Proof.atp_proof
blanchet@49914
    12
  type stature = ATP_Problem_Generate.stature
blanchet@54495
    13
  type one_line_params = Sledgehammer_Reconstructor.one_line_params
blanchet@49914
    14
blanchet@49914
    15
  type isar_params =
blanchet@54505
    16
    bool * bool * string * string * Time.time option * real * bool * (term, string) atp_step list *
blanchet@54505
    17
    thm
blanchet@49914
    18
blanchet@49883
    19
  val isar_proof_text :
wenzelm@53052
    20
    Proof.context -> bool option -> isar_params -> one_line_params -> string
blanchet@49883
    21
  val proof_text :
blanchet@54500
    22
    Proof.context -> bool option -> (unit -> isar_params) -> int -> one_line_params -> string
blanchet@49883
    23
end;
blanchet@49883
    24
blanchet@52374
    25
structure Sledgehammer_Reconstruct : SLEDGEHAMMER_RECONSTRUCT =
blanchet@49883
    26
struct
blanchet@49883
    27
blanchet@49883
    28
open ATP_Util
blanchet@49914
    29
open ATP_Problem
blanchet@49883
    30
open ATP_Proof
blanchet@49883
    31
open ATP_Problem_Generate
blanchet@49883
    32
open ATP_Proof_Reconstruct
blanchet@49918
    33
open Sledgehammer_Util
smolkas@52555
    34
open Sledgehammer_Reconstructor
smolkas@50264
    35
open Sledgehammer_Proof
smolkas@50258
    36
open Sledgehammer_Annotate
smolkas@52555
    37
open Sledgehammer_Print
smolkas@52556
    38
open Sledgehammer_Preplay
smolkas@51130
    39
open Sledgehammer_Compress
smolkas@52592
    40
open Sledgehammer_Try0
smolkas@52611
    41
open Sledgehammer_Minimize_Isar
blanchet@49914
    42
blanchet@49914
    43
structure String_Redirect = ATP_Proof_Redirect(
blanchet@53586
    44
  type key = atp_step_name
blanchet@49914
    45
  val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s')
blanchet@49914
    46
  val string_of = fst)
blanchet@49914
    47
blanchet@49883
    48
open String_Redirect
blanchet@49883
    49
blanchet@54501
    50
fun raw_label_of_num num = (num, 0)
blanchet@49914
    51
blanchet@54501
    52
fun label_of_clause [(num, _)] = raw_label_of_num num
blanchet@54501
    53
  | label_of_clause c = (space_implode "___" (map (fst o raw_label_of_num o fst) c), 0)
blanchet@50005
    54
blanchet@54505
    55
fun add_fact_of_dependencies [(_, ss as _ :: _)] = apsnd (union (op =) ss)
blanchet@54505
    56
  | add_fact_of_dependencies names = apfst (insert (op =) (label_of_clause names))
blanchet@49914
    57
blanchet@49914
    58
fun replace_one_dependency (old, new) dep =
blanchet@49914
    59
  if is_same_atp_step dep old then new else [dep]
blanchet@51201
    60
fun replace_dependencies_in_line p (name, role, t, rule, deps) =
blanchet@51201
    61
  (name, role, t, rule, fold (union (op =) o replace_one_dependency p) deps [])
blanchet@49914
    62
blanchet@49914
    63
(* No "real" literals means only type information (tfree_tcs, clsrel, or
blanchet@49914
    64
   clsarity). *)
blanchet@49914
    65
fun is_only_type_information t = t aconv @{term True}
blanchet@49914
    66
blanchet@50905
    67
fun s_maybe_not role = role <> Conjecture ? s_not
blanchet@50905
    68
blanchet@51201
    69
fun is_same_inference (role, t) (_, role', t', _, _) =
blanchet@51201
    70
  s_maybe_not role t aconv s_maybe_not role' t'
blanchet@49914
    71
blanchet@49914
    72
(* Discard facts; consolidate adjacent lines that prove the same formula, since
blanchet@49914
    73
   they differ only in type information.*)
blanchet@54505
    74
fun add_line (name as (_, ss), role, t, rule, []) lines =
blanchet@49914
    75
    (* No dependencies: fact, conjecture, or (for Vampire) internal facts or
blanchet@49914
    76
       definitions. *)
blanchet@54535
    77
    if role = Conjecture orelse role = Negated_Conjecture orelse role = Hypothesis then
blanchet@51201
    78
      (name, role, t, rule, []) :: lines
blanchet@54505
    79
    else if role = Axiom then
blanchet@49914
    80
      (* Facts are not proof lines. *)
blanchet@54507
    81
      lines |> is_only_type_information t ? map (replace_dependencies_in_line (name, []))
blanchet@49914
    82
    else
blanchet@49914
    83
      map (replace_dependencies_in_line (name, [])) lines
blanchet@54505
    84
  | add_line (line as (name, role, t, _, _)) lines =
blanchet@49914
    85
    (* Type information will be deleted later; skip repetition test. *)
blanchet@49914
    86
    if is_only_type_information t then
blanchet@50675
    87
      line :: lines
blanchet@49914
    88
    (* Is there a repetition? If so, replace later line by earlier one. *)
blanchet@50905
    89
    else case take_prefix (not o is_same_inference (role, t)) lines of
blanchet@50675
    90
      (_, []) => line :: lines
blanchet@51201
    91
    | (pre, (name', _, _, _, _) :: post) =>
blanchet@50675
    92
      line :: pre @ map (replace_dependencies_in_line (name', [name])) post
blanchet@49914
    93
blanchet@49914
    94
(* Recursively delete empty lines (type information) from the proof. *)
blanchet@51201
    95
fun add_nontrivial_line (line as (name, _, t, _, [])) lines =
blanchet@54507
    96
    if is_only_type_information t then delete_dependency name lines else line :: lines
blanchet@49914
    97
  | add_nontrivial_line line lines = line :: lines
blanchet@49914
    98
and delete_dependency name lines =
blanchet@49914
    99
  fold_rev add_nontrivial_line
blanchet@49914
   100
           (map (replace_dependencies_in_line (name, [])) lines) []
blanchet@49914
   101
blanchet@50675
   102
val e_skolemize_rule = "skolemize"
blanchet@50675
   103
val vampire_skolemisation_rule = "skolemisation"
blanchet@50675
   104
blanchet@50676
   105
val is_skolemize_rule =
blanchet@50676
   106
  member (op =) [e_skolemize_rule, vampire_skolemisation_rule]
blanchet@50676
   107
blanchet@54505
   108
fun add_desired_line (name as (_, ss), role, t, rule, deps) (j, lines) =
blanchet@51198
   109
  (j + 1,
blanchet@54505
   110
   if role <> Plain orelse is_skolemize_rule rule orelse
blanchet@51198
   111
      (* the last line must be kept *)
blanchet@51198
   112
      j = 0 orelse
blanchet@51198
   113
      (not (is_only_type_information t) andalso
blanchet@51198
   114
       null (Term.add_tvars t []) andalso
blanchet@51198
   115
       length deps >= 2 andalso
blanchet@51198
   116
       (* kill next to last line, which usually results in a trivial step *)
blanchet@51198
   117
       j <> 1) then
blanchet@51201
   118
     (name, role, t, rule, deps) :: lines  (* keep line *)
blanchet@51198
   119
   else
blanchet@51198
   120
     map (replace_dependencies_in_line (name, deps)) lines)  (* drop line *)
blanchet@49914
   121
blanchet@49883
   122
smolkas@52454
   123
val add_labels_of_proof =
smolkas@52454
   124
  steps_of_proof #> fold_isar_steps
blanchet@52756
   125
    (byline_of_step #> (fn SOME (By ((ls, _), _)) => union (op =) ls | _ => I))
blanchet@49914
   126
blanchet@49914
   127
fun kill_useless_labels_in_proof proof =
blanchet@49914
   128
  let
smolkas@51178
   129
    val used_ls = add_labels_of_proof proof []
blanchet@49914
   130
    fun do_label l = if member (op =) used_ls l then l else no_label
smolkas@51179
   131
    fun do_assms (Assume assms) = Assume (map (apfst do_label) assms)
smolkas@52454
   132
    fun do_step (Prove (qs, xs, l, t, subproofs, by)) =
blanchet@54501
   133
        Prove (qs, xs, do_label l, t, map do_proof subproofs, by)
blanchet@49914
   134
      | do_step step = step
smolkas@51179
   135
    and do_proof (Proof (fix, assms, steps)) =
blanchet@54501
   136
      Proof (fix, do_assms assms, map do_step steps)
smolkas@51128
   137
  in do_proof proof end
blanchet@49914
   138
blanchet@51998
   139
fun prefix_of_depth n = replicate_string (n + 1)
blanchet@49914
   140
blanchet@54501
   141
val assume_prefix = "a"
blanchet@54501
   142
val have_prefix = "f"
blanchet@54501
   143
blanchet@49914
   144
val relabel_proof =
blanchet@49914
   145
  let
smolkas@51179
   146
    fun fresh_label depth prefix (old as (l, subst, next)) =
blanchet@50672
   147
      if l = no_label then
blanchet@50672
   148
        old
blanchet@50672
   149
      else
blanchet@51998
   150
        let val l' = (prefix_of_depth depth prefix, next) in
smolkas@51179
   151
          (l', (l, l') :: subst, next + 1)
blanchet@50672
   152
        end
blanchet@54507
   153
    fun do_facts subst = apfst (maps (the_list o AList.lookup (op =) subst))
smolkas@51179
   154
    fun do_assm depth (l, t) (subst, next) =
blanchet@54507
   155
      let val (l, subst, next) = (l, subst, next) |> fresh_label depth assume_prefix in
smolkas@51179
   156
        ((l, t), (subst, next))
smolkas@51179
   157
      end
smolkas@51179
   158
    fun do_assms subst depth (Assume assms) =
blanchet@54507
   159
      fold_map (do_assm depth) assms (subst, 1) |>> Assume ||> fst
smolkas@51179
   160
    fun do_steps _ _ _ [] = []
smolkas@52454
   161
      | do_steps subst depth next (Prove (qs, xs, l, t, sub, by) :: steps) =
blanchet@50672
   162
        let
blanchet@54507
   163
          val (l, subst, next) = (l, subst, next) |> fresh_label depth have_prefix
smolkas@52454
   164
          val sub = do_proofs subst depth sub
smolkas@52626
   165
          val by = by |> do_byline subst
smolkas@52454
   166
        in Prove (qs, xs, l, t, sub, by) :: do_steps subst depth next steps end
smolkas@51179
   167
      | do_steps subst depth next (step :: steps) =
smolkas@51179
   168
        step :: do_steps subst depth next steps
smolkas@51179
   169
    and do_proof subst depth (Proof (fix, assms, steps)) =
smolkas@51179
   170
      let val (assms, subst) = do_assms subst depth assms in
smolkas@51179
   171
        Proof (fix, assms, do_steps subst depth 1 steps)
smolkas@51179
   172
      end
smolkas@52626
   173
    and do_byline subst byline =
smolkas@52592
   174
      map_facts_of_byline (do_facts subst) byline
smolkas@51179
   175
    and do_proofs subst depth = map (do_proof subst (depth + 1))
smolkas@51179
   176
  in do_proof [] 0 end
blanchet@49914
   177
blanchet@50004
   178
val chain_direct_proof =
blanchet@50004
   179
  let
smolkas@51178
   180
    fun do_qs_lfs NONE lfs = ([], lfs)
smolkas@51178
   181
      | do_qs_lfs (SOME l0) lfs =
smolkas@51178
   182
        if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0)
smolkas@51178
   183
        else ([], lfs)
smolkas@52592
   184
    fun chain_step lbl
smolkas@52592
   185
      (Prove (qs, xs, l, t, subproofs, By ((lfs, gfs), method))) =
smolkas@52453
   186
          let val (qs', lfs) = do_qs_lfs lbl lfs in
smolkas@52454
   187
            Prove (qs' @ qs, xs, l, t, chain_proofs subproofs,
smolkas@52592
   188
                   By ((lfs, gfs), method))
smolkas@52453
   189
          end
blanchet@50672
   190
      | chain_step _ step = step
smolkas@51179
   191
    and chain_steps _ [] = []
smolkas@51179
   192
      | chain_steps (prev as SOME _) (i :: is) =
smolkas@51179
   193
        chain_step prev i :: chain_steps (label_of_step i) is
smolkas@51179
   194
      | chain_steps _ (i :: is) = i :: chain_steps (label_of_step i) is
smolkas@51179
   195
    and chain_proof (Proof (fix, Assume assms, steps)) =
smolkas@51179
   196
      Proof (fix, Assume assms,
smolkas@51179
   197
             chain_steps (try (List.last #> fst) assms) steps)
smolkas@51179
   198
    and chain_proofs proofs = map (chain_proof) proofs
smolkas@51179
   199
  in chain_proof end
blanchet@49883
   200
blanchet@54505
   201
fun maybe_mk_Trueprop t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
blanchet@54505
   202
blanchet@49914
   203
type isar_params =
blanchet@54505
   204
  bool * bool * string * string * Time.time option * real * bool * (term, string) atp_step list *
blanchet@54505
   205
  thm
blanchet@49914
   206
wenzelm@53052
   207
fun isar_proof_text ctxt isar_proofs
blanchet@54500
   208
    (debug, verbose, metis_type_enc, metis_lam_trans, preplay_timeout, isar_compress,
blanchet@54505
   209
     isar_try0, atp_proof, goal)
blanchet@49918
   210
    (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
blanchet@49883
   211
  let
blanchet@52196
   212
    val (params, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
blanchet@52196
   213
    val (_, ctxt) =
blanchet@52196
   214
      params
blanchet@52196
   215
      |> map (fn (s, T) => (Binding.name s, SOME T, NoSyn))
blanchet@54507
   216
      |> (fn fixes => ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes)
wenzelm@53052
   217
    val one_line_proof = one_line_proof_text 0 one_line_params
smolkas@52556
   218
    val do_preplay = preplay_timeout <> SOME Time.zeroTime
blanchet@49883
   219
blanchet@49883
   220
    fun isar_proof_of () =
blanchet@49883
   221
      let
blanchet@49883
   222
        val atp_proof =
blanchet@49883
   223
          atp_proof
blanchet@54505
   224
          |> rpair [] |-> fold_rev add_line
blanchet@49883
   225
          |> rpair [] |-> fold_rev add_nontrivial_line
blanchet@49883
   226
          |> rpair (0, [])
blanchet@54505
   227
          |-> fold_rev add_desired_line
blanchet@49883
   228
          |> snd
blanchet@54535
   229
        val conjs =
blanchet@54535
   230
          atp_proof |> map_filter (fn (name, role, _, _, _) =>
blanchet@54535
   231
            if role = Conjecture orelse role = Negated_Conjecture then SOME name else NONE)
blanchet@50010
   232
        val assms =
blanchet@54505
   233
          atp_proof
blanchet@54535
   234
          |> map_filter (try (fn ((num, _), Hypothesis, t, _, _) => (raw_label_of_num num, t)))
blanchet@51212
   235
        val bot = atp_proof |> List.last |> #1
blanchet@51145
   236
        val refute_graph =
blanchet@51212
   237
          atp_proof
blanchet@51212
   238
          |> map (fn (name, _, _, _, from) => (from, name))
blanchet@51212
   239
          |> make_refute_graph bot
blanchet@51212
   240
          |> fold (Atom_Graph.default_node o rpair ()) conjs
blanchet@51145
   241
        val axioms = axioms_of_refute_graph refute_graph conjs
blanchet@51145
   242
        val tainted = tainted_atoms_of_refute_graph refute_graph conjs
blanchet@51156
   243
        val is_clause_tainted = exists (member (op =) tainted)
blanchet@50676
   244
        val steps =
blanchet@49883
   245
          Symtab.empty
blanchet@51201
   246
          |> fold (fn (name as (s, _), role, t, rule, _) =>
blanchet@50676
   247
                      Symtab.update_new (s, (rule,
blanchet@51156
   248
                        t |> (if is_clause_tainted [name] then
blanchet@50905
   249
                                s_maybe_not role
blanchet@50676
   250
                                #> fold exists_of (map Var (Term.add_vars t []))
blanchet@50676
   251
                              else
blanchet@50676
   252
                                I))))
blanchet@49883
   253
                  atp_proof
blanchet@51148
   254
        fun is_clause_skolemize_rule [(s, _)] =
blanchet@54505
   255
            Option.map (is_skolemize_rule o fst) (Symtab.lookup steps s) = SOME true
blanchet@50676
   256
          | is_clause_skolemize_rule _ = false
blanchet@54507
   257
        (* The assumptions and conjecture are "prop"s; the other formulas are "bool"s. *)
blanchet@54505
   258
        fun prop_of_clause [(num, _)] =
blanchet@54505
   259
            Symtab.lookup steps num |> the |> snd |> maybe_mk_Trueprop |> close_form
blanchet@50016
   260
          | prop_of_clause names =
blanchet@50676
   261
            let
blanchet@50676
   262
              val lits = map snd (map_filter (Symtab.lookup steps o fst) names)
blanchet@50676
   263
            in
blanchet@50018
   264
              case List.partition (can HOLogic.dest_not) lits of
blanchet@50018
   265
                (negs as _ :: _, pos as _ :: _) =>
blanchet@54507
   266
                s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos)
blanchet@50018
   267
              | _ => fold (curry s_disj) lits @{term False}
blanchet@50018
   268
            end
blanchet@50016
   269
            |> HOLogic.mk_Trueprop |> close_form
smolkas@51179
   270
        fun isar_proof_of_direct_proof infs =
smolkas@51179
   271
          let
smolkas@51179
   272
            fun maybe_show outer c =
blanchet@54507
   273
              (outer andalso length c = 1 andalso subset (op =) (c, conjs)) ? cons Show
smolkas@51179
   274
            val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
blanchet@54501
   275
            fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
blanchet@51976
   276
            fun do_steps outer predecessor accum [] =
blanchet@51976
   277
                accum
blanchet@51976
   278
                |> (if tainted = [] then
blanchet@54501
   279
                      cons (Prove (if outer then [Show] else [], Fix [], no_label, concl_t, [],
blanchet@54503
   280
                                   By (([the predecessor], []), MetisM)))
blanchet@51976
   281
                    else
blanchet@51976
   282
                      I)
blanchet@51976
   283
                |> rev
smolkas@51179
   284
              | do_steps outer _ accum (Have (gamma, c) :: infs) =
blanchet@50676
   285
                let
blanchet@51148
   286
                  val l = label_of_clause c
blanchet@51148
   287
                  val t = prop_of_clause c
blanchet@54505
   288
                  val by = By (fold add_fact_of_dependencies gamma no_facts, MetisM)
blanchet@54501
   289
                  fun prove sub by = Prove (maybe_show outer c [], Fix [], l, t, sub, by)
blanchet@54501
   290
                  fun do_rest l step = do_steps outer (SOME l) (step :: accum) infs
blanchet@51148
   291
                in
blanchet@51156
   292
                  if is_clause_tainted c then
blanchet@51149
   293
                    case gamma of
blanchet@51149
   294
                      [g] =>
blanchet@54501
   295
                      if is_clause_skolemize_rule g andalso is_clause_tainted g then
blanchet@51149
   296
                        let
smolkas@51178
   297
                          val subproof =
blanchet@54501
   298
                            Proof (Fix (skolems_of (prop_of_clause g)), Assume [], rev accum)
blanchet@51149
   299
                        in
blanchet@54503
   300
                          do_steps outer (SOME l) [prove [subproof] (By (no_facts, MetisM))] []
blanchet@51149
   301
                        end
blanchet@51149
   302
                      else
smolkas@52454
   303
                        do_rest l (prove [] by)
smolkas@52454
   304
                    | _ => do_rest l (prove [] by)
blanchet@51148
   305
                  else
blanchet@51149
   306
                    if is_clause_skolemize_rule c then
smolkas@52454
   307
                      do_rest l (Prove ([], Fix (skolems_of t), l, t, [], by))
blanchet@51149
   308
                    else
smolkas@52454
   309
                      do_rest l (prove [] by)
blanchet@51148
   310
                end
smolkas@51179
   311
              | do_steps outer predecessor accum (Cases cases :: infs) =
blanchet@51148
   312
                let
blanchet@51148
   313
                  fun do_case (c, infs) =
blanchet@54501
   314
                    do_proof false [] [(label_of_clause c, prop_of_clause c)] infs
blanchet@51148
   315
                  val c = succedent_of_cases cases
smolkas@51178
   316
                  val l = label_of_clause c
smolkas@51179
   317
                  val t = prop_of_clause c
smolkas@51179
   318
                  val step =
blanchet@54501
   319
                    Prove (maybe_show outer c [], Fix [], l, t,  map do_case cases,
blanchet@54503
   320
                      By ((the_list predecessor, []), MetisM))
blanchet@51149
   321
                in
smolkas@51179
   322
                  do_steps outer (SOME l) (step :: accum) infs
blanchet@51149
   323
                end
smolkas@51179
   324
            and do_proof outer fix assms infs =
smolkas@51179
   325
              Proof (Fix fix, Assume assms, do_steps outer NONE [] infs)
smolkas@51179
   326
          in
smolkas@51179
   327
            do_proof true params assms infs
smolkas@51179
   328
          end
smolkas@51179
   329
smolkas@52592
   330
        (* 60 seconds seems like a good interpreation of "no timeout" *)
smolkas@52592
   331
        val preplay_timeout = preplay_timeout |> the_default (seconds 60.0)
smolkas@52592
   332
blanchet@51741
   333
        val clean_up_labels_in_proof =
blanchet@51165
   334
          chain_direct_proof
blanchet@51165
   335
          #> kill_useless_labels_in_proof
blanchet@51165
   336
          #> relabel_proof
blanchet@53761
   337
        val (preplay_interface as {overall_preplay_stats, ...}, isar_proof) =
blanchet@51145
   338
          refute_graph
blanchet@51031
   339
          |> redirect_graph axioms tainted bot
smolkas@51179
   340
          |> isar_proof_of_direct_proof
smolkas@52556
   341
          |> relabel_proof_canonically
blanchet@54500
   342
          |> `(proof_preplay_interface debug ctxt metis_type_enc metis_lam_trans do_preplay
blanchet@53761
   343
               preplay_timeout)
smolkas@52626
   344
        val ((preplay_time, preplay_fail), isar_proof) =
smolkas@52556
   345
          isar_proof
blanchet@54501
   346
          |> compress_proof (if isar_proofs = SOME true then isar_compress else 1000.0)
blanchet@53762
   347
               preplay_interface
smolkas@52632
   348
          |> isar_try0 ? try0 preplay_timeout preplay_interface
blanchet@54501
   349
          |> minimize_dependencies_and_remove_unrefed_steps isar_try0 preplay_interface
smolkas@52626
   350
          |> `overall_preplay_stats
smolkas@52626
   351
          ||> clean_up_labels_in_proof
blanchet@54500
   352
        val isar_text =
blanchet@54500
   353
          string_of_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count isar_proof
blanchet@49883
   354
      in
blanchet@49918
   355
        case isar_text of
blanchet@49883
   356
          "" =>
blanchet@51190
   357
          if isar_proofs = SOME true then
blanchet@50671
   358
            "\nNo structured proof available (proof too simple)."
blanchet@49883
   359
          else
blanchet@49883
   360
            ""
blanchet@49883
   361
        | _ =>
blanchet@50670
   362
          let
blanchet@50670
   363
            val msg =
blanchet@51203
   364
              (if verbose then
blanchet@51203
   365
                let
smolkas@52592
   366
                  val num_steps = add_proof_steps (steps_of_proof isar_proof) 0
blanchet@51203
   367
                in [string_of_int num_steps ^ " step" ^ plural_s num_steps] end
blanchet@51203
   368
               else
blanchet@51203
   369
                 []) @
smolkas@52556
   370
              (if do_preplay then
smolkas@50924
   371
                [(if preplay_fail then "may fail, " else "") ^
smolkas@52556
   372
                   string_of_preplay_time preplay_time]
blanchet@50670
   373
               else
blanchet@50670
   374
                 [])
smolkas@50277
   375
          in
blanchet@54507
   376
            "\n\nStructured proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
blanchet@54507
   377
            Active.sendback_markup [Markup.padding_command] isar_text
smolkas@50277
   378
          end
blanchet@49883
   379
      end
blanchet@49883
   380
    val isar_proof =
blanchet@49883
   381
      if debug then
blanchet@49883
   382
        isar_proof_of ()
blanchet@49883
   383
      else case try isar_proof_of () of
blanchet@49883
   384
        SOME s => s
blanchet@51190
   385
      | NONE => if isar_proofs = SOME true then
blanchet@49883
   386
                  "\nWarning: The Isar proof construction failed."
blanchet@49883
   387
                else
blanchet@49883
   388
                  ""
blanchet@49883
   389
  in one_line_proof ^ isar_proof end
blanchet@49883
   390
blanchet@51187
   391
fun isar_proof_would_be_a_good_idea preplay =
blanchet@51187
   392
  case preplay of
blanchet@51187
   393
    Played (reconstr, _) => reconstr = SMT
blanchet@54093
   394
  | Trust_Playable _ => false
blanchet@51187
   395
  | Failed_to_Play _ => true
blanchet@51187
   396
wenzelm@53052
   397
fun proof_text ctxt isar_proofs isar_params num_chained
blanchet@49883
   398
               (one_line_params as (preplay, _, _, _, _, _)) =
blanchet@51190
   399
  (if isar_proofs = SOME true orelse
blanchet@51190
   400
      (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then
blanchet@54500
   401
     isar_proof_text ctxt isar_proofs (isar_params ())
blanchet@49883
   402
   else
wenzelm@53052
   403
     one_line_proof_text num_chained) one_line_params
blanchet@49883
   404
blanchet@49883
   405
end;