src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
author blanchet
Mon Jun 02 17:34:26 2014 +0200 (2014-06-02 ago)
changeset 57158 f028d93798e6
parent 57154 f0eff6393a32
child 57245 f6bf6d5341ee
permissions -rw-r--r--
simplified counterexample handling
blanchet@55202
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_isar.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@55202
     8
signature SLEDGEHAMMER_ISAR =
blanchet@49883
     9
sig
blanchet@54771
    10
  type atp_step_name = ATP_Proof.atp_step_name
blanchet@54495
    11
  type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
blanchet@53586
    12
  type 'a atp_proof = 'a ATP_Proof.atp_proof
blanchet@49914
    13
  type stature = ATP_Problem_Generate.stature
blanchet@55287
    14
  type one_line_params = Sledgehammer_Proof_Methods.one_line_params
blanchet@49914
    15
blanchet@55222
    16
  val trace : bool Config.T
blanchet@55222
    17
blanchet@49914
    18
  type isar_params =
blanchet@55296
    19
    bool * (string option * string option) * Time.time * real * bool * bool
blanchet@55288
    20
    * (term, string) atp_step list * thm
blanchet@49914
    21
blanchet@55296
    22
  val proof_text : Proof.context -> bool -> bool option -> bool option -> (unit -> isar_params) ->
blanchet@55296
    23
    int -> one_line_params -> string
blanchet@49883
    24
end;
blanchet@49883
    25
blanchet@55202
    26
structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
blanchet@49883
    27
struct
blanchet@49883
    28
blanchet@49883
    29
open ATP_Util
blanchet@49914
    30
open ATP_Problem
blanchet@49883
    31
open ATP_Proof
blanchet@49883
    32
open ATP_Proof_Reconstruct
blanchet@49918
    33
open Sledgehammer_Util
blanchet@55287
    34
open Sledgehammer_Proof_Methods
blanchet@55202
    35
open Sledgehammer_Isar_Proof
blanchet@55202
    36
open Sledgehammer_Isar_Preplay
blanchet@55202
    37
open Sledgehammer_Isar_Compress
blanchet@55202
    38
open Sledgehammer_Isar_Minimize
blanchet@49914
    39
blanchet@49914
    40
structure String_Redirect = ATP_Proof_Redirect(
blanchet@53586
    41
  type key = atp_step_name
blanchet@49914
    42
  val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s')
blanchet@49914
    43
  val string_of = fst)
blanchet@49914
    44
blanchet@49883
    45
open String_Redirect
blanchet@49883
    46
blanchet@55222
    47
val trace = Attrib.setup_config_bool @{binding sledgehammer_isar_trace} (K false)
blanchet@55222
    48
blanchet@54769
    49
val e_skolemize_rules = ["skolemize", "shift_quantors"]
blanchet@54836
    50
val spass_pirate_datatype_rule = "DT"
blanchet@54746
    51
val vampire_skolemisation_rule = "skolemisation"
blanchet@54746
    52
(* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *)
blanchet@54753
    53
val z3_skolemize_rule = "sk"
blanchet@54753
    54
val z3_th_lemma_rule = "th-lemma"
blanchet@54746
    55
blanchet@54772
    56
val skolemize_rules =
blanchet@54772
    57
  e_skolemize_rules @ [spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule]
blanchet@54746
    58
blanchet@54769
    59
val is_skolemize_rule = member (op =) skolemize_rules
blanchet@54755
    60
val is_arith_rule = String.isPrefix z3_th_lemma_rule
blanchet@54836
    61
val is_datatype_rule = String.isPrefix spass_pirate_datatype_rule
blanchet@54755
    62
blanchet@54501
    63
fun raw_label_of_num num = (num, 0)
blanchet@49914
    64
blanchet@54501
    65
fun label_of_clause [(num, _)] = raw_label_of_num num
blanchet@54501
    66
  | label_of_clause c = (space_implode "___" (map (fst o raw_label_of_num o fst) c), 0)
blanchet@50005
    67
blanchet@54505
    68
fun add_fact_of_dependencies [(_, ss as _ :: _)] = apsnd (union (op =) ss)
blanchet@54505
    69
  | add_fact_of_dependencies names = apfst (insert (op =) (label_of_clause names))
blanchet@49914
    70
blanchet@56126
    71
fun is_True_prop t = t aconv @{prop True}
blanchet@54758
    72
blanchet@54799
    73
fun add_line_pass1 (line as (name, role, t, rule, [])) lines =
blanchet@54770
    74
    (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or
blanchet@54770
    75
       definitions. *)
blanchet@57056
    76
    if role = Conjecture orelse role = Negated_Conjecture then line :: lines
blanchet@57056
    77
    else if is_True_prop t then map (replace_dependencies_in_line (name, [])) lines
blanchet@57056
    78
    else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then line :: lines
blanchet@57056
    79
    else if role = Axiom then lines (* axioms (facts) need no proof lines *)
blanchet@57056
    80
    else map (replace_dependencies_in_line (name, [])) lines
blanchet@54755
    81
  | add_line_pass1 line lines = line :: lines
blanchet@49914
    82
blanchet@56130
    83
fun add_lines_pass2 res _ [] = rev res
blanchet@56130
    84
  | add_lines_pass2 res prev_t ((line as (name, role, t, rule, deps)) :: lines) =
blanchet@55184
    85
    let
blanchet@55184
    86
      val is_last_line = null lines
blanchet@55184
    87
blanchet@55184
    88
      fun looks_interesting () =
blanchet@56130
    89
        not (is_True_prop t) andalso not (t aconv prev_t) andalso null (Term.add_tvars t []) andalso
blanchet@56130
    90
        length deps >= 2 andalso not (can the_single lines)
blanchet@55184
    91
blanchet@55184
    92
      fun is_skolemizing_line (_, _, _, rule', deps') =
blanchet@55184
    93
        is_skolemize_rule rule' andalso member (op =) deps' name
blanchet@55184
    94
      fun is_before_skolemize_rule () = exists is_skolemizing_line lines
blanchet@55184
    95
    in
blanchet@55184
    96
      if role <> Plain orelse is_skolemize_rule rule orelse is_arith_rule rule orelse
blanchet@55184
    97
         is_datatype_rule rule orelse is_last_line orelse looks_interesting () orelse
blanchet@55184
    98
         is_before_skolemize_rule () then
blanchet@56130
    99
        add_lines_pass2 (line :: res) t lines
blanchet@55184
   100
      else
blanchet@56130
   101
        add_lines_pass2 res t (map (replace_dependencies_in_line (name, deps)) lines)
blanchet@55184
   102
    end
blanchet@49914
   103
blanchet@49914
   104
type isar_params =
blanchet@55296
   105
  bool * (string option * string option) * Time.time * real * bool * bool
blanchet@55288
   106
  * (term, string) atp_step list * thm
blanchet@49914
   107
blanchet@56852
   108
val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method]
blanchet@56097
   109
val simp_based_methods = [Auto_Method, Simp_Method, Fastforce_Method, Force_Method]
blanchet@55323
   110
val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method]
blanchet@55311
   111
blanchet@55311
   112
val arith_methods = basic_arith_methods @ simp_based_methods @ basic_systematic_methods
blanchet@55311
   113
val datatype_methods = [Simp_Method, Simp_Size_Method]
blanchet@55311
   114
val systematic_methods0 = basic_systematic_methods @ basic_arith_methods @ simp_based_methods @
blanchet@55311
   115
  [Metis_Method (SOME no_typesN, NONE)]
blanchet@55311
   116
val rewrite_methods = simp_based_methods @ basic_systematic_methods @ basic_arith_methods
blanchet@55311
   117
val skolem_methods = basic_systematic_methods
blanchet@54766
   118
blanchet@55297
   119
fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
blanchet@49918
   120
    (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
blanchet@49883
   121
  let
blanchet@56097
   122
    val _ = if debug then Output.urgent_message "Constructing Isar proof..." else ()
blanchet@56097
   123
blanchet@49883
   124
    fun isar_proof_of () =
blanchet@49883
   125
      let
fleury@57154
   126
        val (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, minimize,
fleury@57154
   127
          atp_proof, goal) = isar_params ()
blanchet@55257
   128
blanchet@55311
   129
        val systematic_methods = insert (op =) (Metis_Method alt_metis_args) systematic_methods0
blanchet@55168
   130
blanchet@55311
   131
        fun massage_methods (meths as meth :: _) =
blanchet@55297
   132
          if not try0_isar then [meth]
blanchet@56081
   133
          else if smt_proofs = SOME true then SMT2_Method :: meths
blanchet@55297
   134
          else meths
blanchet@55273
   135
blanchet@55168
   136
        val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
blanchet@55264
   137
        val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
blanchet@55264
   138
        val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd
blanchet@55168
   139
blanchet@55168
   140
        val do_preplay = preplay_timeout <> Time.zeroTime
blanchet@55253
   141
        val compress_isar = if isar_proofs = NONE andalso do_preplay then 1000.0 else compress_isar
blanchet@55168
   142
wenzelm@55948
   143
        val is_fixed = Variable.is_declared ctxt orf Name.is_skolem
blanchet@55168
   144
        fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
blanchet@55168
   145
blanchet@55168
   146
        fun get_role keep_role ((num, _), role, t, rule, _) =
blanchet@55168
   147
          if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE
blanchet@55168
   148
blanchet@49883
   149
        val atp_proof =
blanchet@49883
   150
          atp_proof
blanchet@54755
   151
          |> rpair [] |-> fold_rev add_line_pass1
blanchet@56130
   152
          |> add_lines_pass2 [] Term.dummy
blanchet@54700
   153
blanchet@54535
   154
        val conjs =
blanchet@54700
   155
          map_filter (fn (name, role, _, _, _) =>
blanchet@54700
   156
              if member (op =) [Conjecture, Negated_Conjecture] role then SOME name else NONE)
blanchet@54700
   157
            atp_proof
blanchet@54751
   158
        val assms = map_filter (Option.map fst o get_role (curry (op =) Hypothesis)) atp_proof
blanchet@54700
   159
        val lems =
blanchet@54700
   160
          map_filter (get_role (curry (op =) Lemma)) atp_proof
blanchet@54751
   161
          |> map (fn ((l, t), rule) =>
blanchet@54753
   162
            let
blanchet@55244
   163
              val (skos, meths) =
blanchet@55273
   164
                (if is_skolemize_rule rule then (skolems_of t, skolem_methods)
blanchet@55273
   165
                 else if is_arith_rule rule then ([], arith_methods)
blanchet@55273
   166
                 else ([], rewrite_methods))
blanchet@55311
   167
                ||> massage_methods
blanchet@54753
   168
            in
blanchet@55299
   169
              Prove ([], skos, l, t, [], ([], []), meths, "")
blanchet@54753
   170
            end)
blanchet@54700
   171
blanchet@51212
   172
        val bot = atp_proof |> List.last |> #1
blanchet@54700
   173
blanchet@51145
   174
        val refute_graph =
blanchet@51212
   175
          atp_proof
blanchet@51212
   176
          |> map (fn (name, _, _, _, from) => (from, name))
blanchet@51212
   177
          |> make_refute_graph bot
blanchet@51212
   178
          |> fold (Atom_Graph.default_node o rpair ()) conjs
blanchet@54700
   179
blanchet@51145
   180
        val axioms = axioms_of_refute_graph refute_graph conjs
blanchet@54700
   181
blanchet@51145
   182
        val tainted = tainted_atoms_of_refute_graph refute_graph conjs
blanchet@51156
   183
        val is_clause_tainted = exists (member (op =) tainted)
blanchet@50676
   184
        val steps =
blanchet@49883
   185
          Symtab.empty
blanchet@51201
   186
          |> fold (fn (name as (s, _), role, t, rule, _) =>
blanchet@54758
   187
              Symtab.update_new (s, (rule, t
blanchet@54758
   188
                |> (if is_clause_tainted [name] then
blanchet@54768
   189
                      HOLogic.dest_Trueprop
blanchet@54768
   190
                      #> role <> Conjecture ? s_not
blanchet@54758
   191
                      #> fold exists_of (map Var (Term.add_vars t []))
blanchet@54768
   192
                      #> HOLogic.mk_Trueprop
blanchet@54758
   193
                    else
blanchet@54758
   194
                      I))))
blanchet@54758
   195
            atp_proof
blanchet@54700
   196
blanchet@54755
   197
        val rule_of_clause_id = fst o the o Symtab.lookup steps o fst
blanchet@54700
   198
blanchet@54757
   199
        fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> close_form
blanchet@50016
   200
          | prop_of_clause names =
blanchet@50676
   201
            let
blanchet@54758
   202
              val lits = map (HOLogic.dest_Trueprop o snd)
blanchet@54758
   203
                (map_filter (Symtab.lookup steps o fst) names)
blanchet@50676
   204
            in
blanchet@54754
   205
              (case List.partition (can HOLogic.dest_not) lits of
blanchet@50018
   206
                (negs as _ :: _, pos as _ :: _) =>
blanchet@54507
   207
                s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos)
blanchet@54754
   208
              | _ => fold (curry s_disj) lits @{term False})
blanchet@50018
   209
            end
blanchet@50016
   210
            |> HOLogic.mk_Trueprop |> close_form
blanchet@54700
   211
blanchet@55169
   212
        fun maybe_show outer c = (outer andalso eq_set (op =) (c, conjs)) ? cons Show
blanchet@54700
   213
blanchet@54700
   214
        fun isar_steps outer predecessor accum [] =
blanchet@54700
   215
            accum
blanchet@54700
   216
            |> (if tainted = [] then
blanchet@54700
   217
                  cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
blanchet@55311
   218
                    (the_list predecessor, []), massage_methods systematic_methods, ""))
blanchet@54700
   219
                else
blanchet@54700
   220
                  I)
blanchet@54700
   221
            |> rev
blanchet@54755
   222
          | isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) =
blanchet@54700
   223
            let
blanchet@54700
   224
              val l = label_of_clause c
blanchet@54700
   225
              val t = prop_of_clause c
blanchet@54755
   226
              val rule = rule_of_clause_id id
blanchet@54755
   227
              val skolem = is_skolemize_rule rule
blanchet@54755
   228
blanchet@55279
   229
              val deps = fold add_fact_of_dependencies gamma ([], [])
blanchet@55244
   230
              val meths =
blanchet@55273
   231
                (if skolem then skolem_methods
blanchet@55273
   232
                 else if is_arith_rule rule then arith_methods
blanchet@55273
   233
                 else if is_datatype_rule rule then datatype_methods
blanchet@55311
   234
                 else systematic_methods)
blanchet@55311
   235
                |> massage_methods
blanchet@55280
   236
blanchet@55299
   237
              fun prove sub facts = Prove (maybe_show outer c [], [], l, t, sub, facts, meths, "")
blanchet@55280
   238
              fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs
blanchet@54700
   239
            in
blanchet@54700
   240
              if is_clause_tainted c then
blanchet@54712
   241
                (case gamma of
blanchet@54700
   242
                  [g] =>
blanchet@54755
   243
                  if skolem andalso is_clause_tainted g then
blanchet@54751
   244
                    let val subproof = Proof (skolems_of (prop_of_clause g), [], rev accum) in
blanchet@55280
   245
                      isar_steps outer (SOME l) [prove [subproof] ([], [])] infs
blanchet@54700
   246
                    end
blanchet@51148
   247
                  else
blanchet@55280
   248
                    steps_of_rest (prove [] deps)
blanchet@55280
   249
                | _ => steps_of_rest (prove [] deps))
blanchet@54700
   250
              else
blanchet@55299
   251
                steps_of_rest (if skolem then Prove ([], skolems_of t, l, t, [], deps, meths, "")
blanchet@55280
   252
                  else prove [] deps)
blanchet@54700
   253
            end
blanchet@54700
   254
          | isar_steps outer predecessor accum (Cases cases :: infs) =
blanchet@54700
   255
            let
blanchet@55186
   256
              fun isar_case (c, subinfs) =
blanchet@55186
   257
                isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] subinfs
blanchet@54700
   258
              val c = succedent_of_cases cases
blanchet@54700
   259
              val l = label_of_clause c
blanchet@54700
   260
              val t = prop_of_clause c
blanchet@54700
   261
              val step =
blanchet@54760
   262
                Prove (maybe_show outer c [], [], l, t,
blanchet@54760
   263
                  map isar_case (filter_out (null o snd) cases),
blanchet@55311
   264
                  (the_list predecessor, []), massage_methods systematic_methods, "")
blanchet@54700
   265
            in
blanchet@54700
   266
              isar_steps outer (SOME l) (step :: accum) infs
blanchet@54700
   267
            end
blanchet@54700
   268
        and isar_proof outer fix assms lems infs =
blanchet@54700
   269
          Proof (fix, assms, lems @ isar_steps outer NONE [] infs)
blanchet@54700
   270
blanchet@55222
   271
        val trace = Config.get ctxt trace
blanchet@55214
   272
blanchet@55256
   273
        val canonical_isar_proof =
blanchet@51145
   274
          refute_graph
blanchet@55214
   275
          |> trace ? tap (tracing o prefix "Refute graph: " o string_of_refute_graph)
blanchet@51031
   276
          |> redirect_graph axioms tainted bot
blanchet@55214
   277
          |> trace ? tap (tracing o prefix "Direct proof: " o string_of_direct_proof)
blanchet@54754
   278
          |> isar_proof true params assms lems
blanchet@55213
   279
          |> postprocess_isar_proof_remove_unreferenced_steps I
blanchet@55213
   280
          |> relabel_isar_proof_canonically
blanchet@55214
   281
blanchet@55286
   282
        val ctxt = ctxt |> enrich_context_with_local_facts canonical_isar_proof
blanchet@55256
   283
blanchet@55260
   284
        val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty
blanchet@55260
   285
blanchet@55264
   286
        val _ = fold_isar_steps (fn meth =>
blanchet@57054
   287
            K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth []))
blanchet@55260
   288
          (steps_of_isar_proof canonical_isar_proof) ()
blanchet@55214
   289
blanchet@55223
   290
        fun str_of_preplay_outcome outcome =
blanchet@55223
   291
          if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"
blanchet@55223
   292
        fun str_of_meth l meth =
blanchet@56985
   293
          string_of_proof_method ctxt [] meth ^ " " ^
blanchet@55266
   294
          str_of_preplay_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)
blanchet@55244
   295
        fun comment_of l = map (str_of_meth l) #> commas
blanchet@55222
   296
blanchet@55214
   297
        fun trace_isar_proof label proof =
blanchet@55214
   298
          if trace then
blanchet@55299
   299
            tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^
blanchet@56097
   300
              string_of_isar_proof ctxt subgoal subgoal_count
blanchet@56097
   301
                (comment_isar_proof comment_of proof) ^ "\n")
blanchet@55214
   302
          else
blanchet@55214
   303
            ()
blanchet@54754
   304
blanchet@55299
   305
        fun comment_of l (meth :: _) =
blanchet@55299
   306
          (case (verbose,
blanchet@55299
   307
              Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)) of
blanchet@55299
   308
            (false, Played _) => ""
blanchet@55299
   309
          | (_, outcome) => string_of_play_outcome outcome)
blanchet@55299
   310
blanchet@54828
   311
        val (play_outcome, isar_proof) =
blanchet@55256
   312
          canonical_isar_proof
blanchet@55214
   313
          |> tap (trace_isar_proof "Original")
blanchet@57054
   314
          |> compress_isar_proof ctxt compress_isar preplay_timeout preplay_data
blanchet@55214
   315
          |> tap (trace_isar_proof "Compressed")
blanchet@55213
   316
          |> postprocess_isar_proof_remove_unreferenced_steps
blanchet@55266
   317
               (keep_fastest_method_of_isar_step (!preplay_data)
blanchet@57054
   318
                #> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
blanchet@55214
   319
          |> tap (trace_isar_proof "Minimized")
blanchet@55329
   320
          (* It's not clear whether this is worth the trouble (and if so, "isar_compress" has an
blanchet@55329
   321
             unnatural semantics): *)
blanchet@55329
   322
(*
blanchet@55327
   323
          |> minimize
blanchet@55329
   324
               ? (compress_isar_proof ctxt compress_isar preplay_timeout preplay_data
blanchet@55327
   325
                  #> tap (trace_isar_proof "Compressed again"))
blanchet@55329
   326
*)
blanchet@55260
   327
          |> `(preplay_outcome_of_isar_proof (!preplay_data))
blanchet@55325
   328
          ||> (comment_isar_proof comment_of
blanchet@55325
   329
               #> chain_isar_proof
blanchet@55325
   330
               #> kill_useless_labels_in_isar_proof
blanchet@55325
   331
               #> relabel_isar_proof_nicely)
blanchet@49883
   332
      in
blanchet@56097
   333
        (case string_of_isar_proof ctxt subgoal subgoal_count isar_proof of
blanchet@49883
   334
          "" =>
blanchet@55213
   335
          if isar_proofs = SOME true then "\nNo structured proof available (proof too simple)."
blanchet@55213
   336
          else ""
blanchet@55214
   337
        | isar_text =>
blanchet@50670
   338
          let
blanchet@50670
   339
            val msg =
blanchet@51203
   340
              (if verbose then
blanchet@55260
   341
                 let val num_steps = add_isar_steps (steps_of_isar_proof isar_proof) 0 in
blanchet@55213
   342
                   [string_of_int num_steps ^ " step" ^ plural_s num_steps]
blanchet@55213
   343
                 end
blanchet@51203
   344
               else
blanchet@51203
   345
                 []) @
blanchet@54828
   346
              (if do_preplay then [string_of_play_outcome play_outcome] else [])
smolkas@50277
   347
          in
blanchet@54507
   348
            "\n\nStructured proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
blanchet@54507
   349
            Active.sendback_markup [Markup.padding_command] isar_text
blanchet@54754
   350
          end)
blanchet@49883
   351
      end
blanchet@54760
   352
blanchet@56985
   353
    val one_line_proof = one_line_proof_text ctxt 0 one_line_params
blanchet@49883
   354
    val isar_proof =
blanchet@49883
   355
      if debug then
blanchet@49883
   356
        isar_proof_of ()
blanchet@54754
   357
      else
blanchet@54754
   358
        (case try isar_proof_of () of
blanchet@54754
   359
          SOME s => s
blanchet@54754
   360
        | NONE =>
blanchet@56097
   361
          if isar_proofs = SOME true then "\nWarning: Isar proof construction failed." else "")
blanchet@57056
   362
  in
blanchet@57056
   363
    one_line_proof ^ isar_proof
blanchet@57056
   364
  end
blanchet@49883
   365
blanchet@55297
   366
fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) =
blanchet@54824
   367
  (case play of
blanchet@56081
   368
    Played _ => meth = SMT2_Method andalso smt_proofs <> SOME true
blanchet@56093
   369
  | Play_Timed_Out time => Time.> (time, Time.zeroTime)
blanchet@56093
   370
  | Play_Failed => true)
blanchet@51187
   371
blanchet@55297
   372
fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
blanchet@55256
   373
    (one_line_params as (preplay, _, _, _, _, _)) =
blanchet@51190
   374
  (if isar_proofs = SOME true orelse
blanchet@55297
   375
      (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt_proofs preplay) then
blanchet@55297
   376
     isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
blanchet@49883
   377
   else
blanchet@56985
   378
     one_line_proof_text ctxt num_chained) one_line_params
blanchet@49883
   379
blanchet@49883
   380
end;