src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
author wenzelm
Tue Jun 06 13:13:25 2017 +0200 (2017-06-06)
changeset 66020 a31760eee09d
parent 61756 21c2b1f691d1
child 67399 eab6ce8368fa
permissions -rw-r--r--
discontinued obsolete print mode;
blanchet@55202
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
smolkas@50263
     2
    Author:     Jasmin Blanchette, TU Muenchen
smolkas@50263
     3
    Author:     Steffen Juilf Smolka, TU Muenchen
smolkas@50263
     4
smolkas@50263
     5
Basic data structures for representing and basic methods
smolkas@50263
     6
for dealing with Isar proof texts.
smolkas@50263
     7
*)
smolkas@50263
     8
blanchet@55202
     9
signature SLEDGEHAMMER_ISAR_PROOF =
smolkas@50259
    10
sig
blanchet@55287
    11
  type proof_method = Sledgehammer_Proof_Methods.proof_method
blanchet@55285
    12
wenzelm@51239
    13
  type label = string * int
blanchet@54816
    14
  type facts = label list * string list (* local and global facts *)
smolkas@50268
    15
smolkas@51178
    16
  datatype isar_qualifier = Show | Then
smolkas@50268
    17
smolkas@52454
    18
  datatype isar_proof =
blanchet@54700
    19
    Proof of (string * typ) list * (label * term) list * isar_step list
smolkas@51179
    20
  and isar_step =
smolkas@50268
    21
    Let of term * term |
blanchet@55280
    22
    Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list
blanchet@55299
    23
      * facts * proof_method list * string
smolkas@52592
    24
smolkas@51179
    25
  val no_label : label
smolkas@50268
    26
smolkas@52592
    27
  val label_ord : label * label -> order
blanchet@51998
    28
  val string_of_label : label -> string
blanchet@57776
    29
  val sort_facts : facts -> facts
smolkas@52592
    30
blanchet@55260
    31
  val steps_of_isar_proof : isar_proof -> isar_step list
blanchet@55223
    32
  val label_of_isar_step : isar_step -> label option
blanchet@55279
    33
  val facts_of_isar_step : isar_step -> facts
blanchet@55279
    34
  val proof_methods_of_isar_step : isar_step -> proof_method list
smolkas@51179
    35
blanchet@54765
    36
  val fold_isar_steps : (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a
blanchet@55212
    37
  val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
blanchet@55212
    38
  val add_isar_steps : isar_step list -> int -> int
smolkas@52454
    39
blanchet@55212
    40
  structure Canonical_Label_Tab : TABLE
smolkas@52556
    41
smolkas@52556
    42
  val canonical_label_ord : (label * label) -> order
blanchet@55220
    43
blanchet@55299
    44
  val comment_isar_proof : (label -> proof_method list -> string) -> isar_proof -> isar_proof
blanchet@55220
    45
  val chain_isar_proof : isar_proof -> isar_proof
blanchet@55220
    46
  val kill_useless_labels_in_isar_proof : isar_proof -> isar_proof
blanchet@55213
    47
  val relabel_isar_proof_canonically : isar_proof -> isar_proof
blanchet@55282
    48
  val relabel_isar_proof_nicely : isar_proof -> isar_proof
blanchet@57792
    49
  val rationalize_obtains_in_isar_proofs : Proof.context -> isar_proof -> isar_proof
smolkas@52556
    50
blanchet@55299
    51
  val string_of_isar_proof : Proof.context -> int -> int -> isar_proof -> string
blanchet@54504
    52
end;
smolkas@50259
    53
blanchet@55202
    54
structure Sledgehammer_Isar_Proof : SLEDGEHAMMER_ISAR_PROOF =
smolkas@50259
    55
struct
smolkas@50259
    56
blanchet@55211
    57
open ATP_Util
blanchet@55211
    58
open ATP_Proof
blanchet@55211
    59
open ATP_Problem_Generate
blanchet@55211
    60
open ATP_Proof_Reconstruct
blanchet@55211
    61
open Sledgehammer_Util
blanchet@55287
    62
open Sledgehammer_Proof_Methods
blanchet@55211
    63
open Sledgehammer_Isar_Annotate
blanchet@55211
    64
smolkas@50259
    65
type label = string * int
blanchet@54534
    66
type facts = label list * string list (* local and global facts *)
smolkas@50259
    67
smolkas@51178
    68
datatype isar_qualifier = Show | Then
smolkas@50259
    69
smolkas@52454
    70
datatype isar_proof =
blanchet@54700
    71
  Proof of (string * typ) list * (label * term) list * isar_step list
smolkas@51179
    72
and isar_step =
smolkas@50259
    73
  Let of term * term |
blanchet@55280
    74
  Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list
blanchet@55299
    75
    * facts * proof_method list * string
smolkas@52592
    76
smolkas@51179
    77
val no_label = ("", ~1)
smolkas@50259
    78
blanchet@57776
    79
(* cf. "label_ord" below *)
blanchet@57776
    80
val assume_prefix = "a"
blanchet@57776
    81
val have_prefix = "f"
blanchet@57776
    82
blanchet@57776
    83
fun label_ord ((s1, i1), (s2, i2)) =
wenzelm@59058
    84
  (case int_ord (apply2 String.size (s1, s2)) of
blanchet@57776
    85
    EQUAL =>
blanchet@57776
    86
    (case string_ord (s1, s2) of
blanchet@57776
    87
      EQUAL => int_ord (i1, i2)
blanchet@57776
    88
    | ord => ord (* "assume" before "have" *))
blanchet@57776
    89
  | ord => ord)
smolkas@52556
    90
blanchet@51998
    91
fun string_of_label (s, num) = s ^ string_of_int num
smolkas@50259
    92
blanchet@57776
    93
(* Put the nearest local label first, since it's the most likely to be replaced by a "hence".
blanchet@57776
    94
   (Some preplaying proof methods, e.g. "blast", react poorly to fact reorderings.) *)
blanchet@57776
    95
fun sort_facts (lfs, gfs) = (sort (label_ord o swap) lfs, sort string_ord gfs)
blanchet@57776
    96
blanchet@55260
    97
fun steps_of_isar_proof (Proof (_, _, steps)) = steps
smolkas@51179
    98
blanchet@55299
    99
fun label_of_isar_step (Prove (_, _, l, _, _, _, _, _)) = SOME l
blanchet@55223
   100
  | label_of_isar_step _ = NONE
smolkas@51178
   101
blanchet@55299
   102
fun subproofs_of_isar_step (Prove (_, _, _, _, subs, _, _, _)) = subs
blanchet@55281
   103
  | subproofs_of_isar_step _ = []
smolkas@52454
   104
blanchet@55299
   105
fun facts_of_isar_step (Prove (_, _, _, _, _, facts, _, _)) = facts
blanchet@55279
   106
  | facts_of_isar_step _ = ([], [])
blanchet@55279
   107
blanchet@55299
   108
fun proof_methods_of_isar_step (Prove (_, _, _, _, _, _, meths, _)) = meths
blanchet@55279
   109
  | proof_methods_of_isar_step _ = []
smolkas@51179
   110
blanchet@55212
   111
fun fold_isar_step f step =
blanchet@55281
   112
  fold (steps_of_isar_proof #> fold_isar_steps f) (subproofs_of_isar_step step) #> f step
blanchet@55212
   113
and fold_isar_steps f = fold (fold_isar_step f)
smolkas@52454
   114
blanchet@54765
   115
fun map_isar_steps f =
smolkas@52592
   116
  let
blanchet@55212
   117
    fun map_proof (Proof (fix, assms, steps)) = Proof (fix, assms, map map_step steps)
blanchet@55212
   118
    and map_step (step as Let _) = f step
blanchet@55299
   119
      | map_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) =
blanchet@55299
   120
        f (Prove (qs, xs, l, t, map map_proof subs, facts, meths, comment))
blanchet@55212
   121
  in map_proof end
smolkas@52592
   122
blanchet@55212
   123
val add_isar_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I)
smolkas@52556
   124
blanchet@55211
   125
(* canonical proof labels: 1, 2, 3, ... in post traversal order *)
smolkas@52557
   126
fun canonical_label_ord (((_, i1), (_, i2)) : label * label) = int_ord (i1, i2)
smolkas@52556
   127
blanchet@55212
   128
structure Canonical_Label_Tab = Table(
smolkas@52556
   129
  type key = label
smolkas@52556
   130
  val ord = canonical_label_ord)
smolkas@52556
   131
blanchet@55299
   132
fun comment_isar_step comment_of (Prove (qs, xs, l, t, subs, facts, meths, _)) =
blanchet@55299
   133
    Prove (qs, xs, l, t, subs, facts, meths, comment_of l meths)
blanchet@55299
   134
  | comment_isar_step _ step = step
blanchet@55299
   135
fun comment_isar_proof comment_of = map_isar_steps (comment_isar_step comment_of)
blanchet@55299
   136
blanchet@55220
   137
fun chain_qs_lfs NONE lfs = ([], lfs)
blanchet@55220
   138
  | chain_qs_lfs (SOME l0) lfs =
blanchet@57655
   139
    if member (op =) lfs l0 then ([Then], remove (op =) l0 lfs) else ([], lfs)
blanchet@57655
   140
blanchet@57286
   141
fun chain_isar_step lbl (Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment)) =
blanchet@55220
   142
    let val (qs', lfs) = chain_qs_lfs lbl lfs in
blanchet@55299
   143
      Prove (qs' @ qs, xs, l, t, map chain_isar_proof subs, (lfs, gfs), meths, comment)
blanchet@55220
   144
    end
blanchet@55220
   145
  | chain_isar_step _ step = step
blanchet@55220
   146
and chain_isar_steps _ [] = []
blanchet@57655
   147
  | chain_isar_steps prev (i :: is) =
blanchet@55223
   148
    chain_isar_step prev i :: chain_isar_steps (label_of_isar_step i) is
blanchet@55220
   149
and chain_isar_proof (Proof (fix, assms, steps)) =
blanchet@55220
   150
  Proof (fix, assms, chain_isar_steps (try (List.last #> fst) assms) steps)
blanchet@55220
   151
blanchet@55220
   152
fun kill_useless_labels_in_isar_proof proof =
blanchet@55220
   153
  let
blanchet@55220
   154
    val used_ls =
blanchet@55279
   155
      fold_isar_steps (facts_of_isar_step #> fst #> union (op =)) (steps_of_isar_proof proof) []
blanchet@55220
   156
blanchet@55220
   157
    fun kill_label l = if member (op =) used_ls l then l else no_label
blanchet@55220
   158
blanchet@55299
   159
    fun kill_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) =
blanchet@55299
   160
        Prove (qs, xs, kill_label l, t, map kill_proof subs, facts, meths, comment)
blanchet@55220
   161
      | kill_step step = step
blanchet@55220
   162
    and kill_proof (Proof (fix, assms, steps)) =
blanchet@55220
   163
      Proof (fix, map (apfst kill_label) assms, map kill_step steps)
blanchet@55220
   164
  in
blanchet@55220
   165
    kill_proof proof
blanchet@55220
   166
  end
blanchet@55220
   167
blanchet@55213
   168
fun relabel_isar_proof_canonically proof =
smolkas@52556
   169
  let
smolkas@52556
   170
    fun next_label l (next, subst) =
blanchet@54534
   171
      let val l' = ("", next) in (l', (next + 1, (l, l') :: subst)) end
smolkas@52556
   172
blanchet@55299
   173
    fun relabel_step (Prove (qs, fix, l, t, subs, (lfs, gfs), meths, comment))
blanchet@55299
   174
          (accum as (_, subst)) =
blanchet@54534
   175
        let
blanchet@55281
   176
          val lfs' = maps (the_list o AList.lookup (op =) subst) lfs
blanchet@55281
   177
          val ((subs', l'), accum') = accum
blanchet@55281
   178
            |> fold_map relabel_proof subs
blanchet@55281
   179
            ||>> next_label l
blanchet@54534
   180
        in
blanchet@55299
   181
          (Prove (qs, fix, l', t, subs', (lfs', gfs), meths, comment), accum')
blanchet@54534
   182
        end
blanchet@55281
   183
      | relabel_step step accum = (step, accum)
blanchet@55281
   184
    and relabel_proof (Proof (fix, assms, steps)) =
blanchet@55281
   185
      fold_map (fn (l, t) => next_label l #> apfst (rpair t)) assms
blanchet@55281
   186
      ##>> fold_map relabel_step steps
blanchet@55281
   187
      #>> (fn (assms, steps) => Proof (fix, assms, steps))
smolkas@52556
   188
  in
blanchet@55279
   189
    fst (relabel_proof proof (0, []))
smolkas@52556
   190
  end
smolkas@52556
   191
blanchet@55282
   192
val relabel_isar_proof_nicely =
blanchet@55220
   193
  let
blanchet@55281
   194
    fun next_label depth prefix l (accum as (next, subst)) =
blanchet@55220
   195
      if l = no_label then
blanchet@55281
   196
        (l, accum)
blanchet@55220
   197
      else
blanchet@55220
   198
        let val l' = (replicate_string (depth + 1) prefix, next) in
blanchet@55281
   199
          (l', (next + 1, (l, l') :: subst))
blanchet@55220
   200
        end
blanchet@55220
   201
blanchet@55299
   202
    fun relabel_step depth (Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment))
blanchet@55299
   203
          (accum as (_, subst)) =
blanchet@55220
   204
        let
blanchet@55281
   205
          val lfs' = maps (the_list o AList.lookup (op =) subst) lfs
blanchet@55309
   206
          val (l', accum' as (_, subst')) = next_label depth have_prefix l accum
blanchet@55281
   207
          val subs' = map (relabel_proof subst' (depth + 1)) subs
blanchet@55220
   208
        in
blanchet@55299
   209
          (Prove (qs, xs, l', t, subs', (lfs', gfs), meths, comment), accum')
blanchet@55220
   210
        end
blanchet@55281
   211
      | relabel_step _ step accum = (step, accum)
blanchet@55220
   212
    and relabel_proof subst depth (Proof (fix, assms, steps)) =
blanchet@55281
   213
      (1, subst)
blanchet@55281
   214
      |> fold_map (fn (l, t) => next_label depth assume_prefix l #> apfst (rpair t)) assms
blanchet@55281
   215
      ||>> fold_map (relabel_step depth) steps
blanchet@55281
   216
      |> (fn ((assms, steps), _) => Proof (fix, assms, steps))
blanchet@55220
   217
  in
blanchet@55220
   218
    relabel_proof [] 0
blanchet@55220
   219
  end
blanchet@55220
   220
blanchet@57793
   221
fun stutter_single_letter s = String.extract (s, 0, SOME 1) ^ s
blanchet@57793
   222
blanchet@57792
   223
fun rationalize_obtains_in_isar_proofs ctxt =
blanchet@57792
   224
  let
blanchet@57792
   225
    fun rename_obtains xs (subst, ctxt) =
blanchet@57792
   226
      let
blanchet@57792
   227
        val Ts = map snd xs
blanchet@57793
   228
        val new_names0 = map (stutter_single_letter o var_name_of_typ o body_type) Ts
blanchet@57792
   229
        val (new_names, ctxt') = Variable.variant_fixes new_names0 ctxt
blanchet@57792
   230
        val ys = map2 pair new_names Ts
blanchet@57792
   231
      in
blanchet@57792
   232
        (ys, ((map Free xs ~~ map Free ys) @ subst, ctxt'))
blanchet@57792
   233
      end
blanchet@57792
   234
blanchet@57792
   235
    fun rationalize_step (Prove (qs, xs, l, t, subs, facts, meths, comment)) subst_ctxt =
blanchet@57792
   236
        let
blanchet@57792
   237
          val (xs', subst_ctxt' as (subst', _)) = rename_obtains xs subst_ctxt
blanchet@57792
   238
          val t' = subst_atomic subst' t
blanchet@58475
   239
          val subs' = map (rationalize_proof false subst_ctxt') subs
blanchet@57792
   240
        in
blanchet@57792
   241
          (Prove (qs, xs', l, t', subs', facts, meths, comment), subst_ctxt')
blanchet@57792
   242
        end
blanchet@58476
   243
    and rationalize_proof outer (subst_ctxt as (subst, ctxt)) (Proof (fix, assms, steps)) =
blanchet@58475
   244
      let
blanchet@58475
   245
        val (fix', subst_ctxt' as (subst', _)) =
blanchet@58476
   246
          if outer then
blanchet@58476
   247
            (* last call: eliminate any remaining skolem names (from SMT proofs) *)
blanchet@58476
   248
            (fix, (subst @ map (fn x => (Free (apfst Name.skolem x), Free x)) fix, ctxt))
blanchet@58476
   249
          else
blanchet@58476
   250
            rename_obtains fix subst_ctxt
blanchet@58475
   251
      in
blanchet@58475
   252
        Proof (fix', map (apsnd (subst_atomic subst')) assms,
blanchet@58475
   253
          fst (fold_map rationalize_step steps subst_ctxt'))
blanchet@58475
   254
      end
blanchet@57792
   255
  in
blanchet@58475
   256
    rationalize_proof true ([], ctxt)
blanchet@57792
   257
  end
blanchet@57792
   258
blanchet@58087
   259
val thesis_var = ((Auto_Bind.thesisN, 0), HOLogic.boolT)
blanchet@58087
   260
blanchet@58087
   261
fun is_thesis ctxt t =
blanchet@58087
   262
  (case Vartab.lookup (Variable.binds_of ctxt) (fst thesis_var) of
blanchet@58087
   263
    SOME (_, t') => HOLogic.mk_Trueprop t' aconv t
blanchet@58087
   264
  | NONE => false)
blanchet@58087
   265
blanchet@55211
   266
val indent_size = 2
blanchet@55211
   267
blanchet@56985
   268
fun string_of_isar_proof ctxt0 i n proof =
blanchet@55211
   269
  let
wenzelm@58928
   270
    val keywords = Thy_Header.get_keywords' ctxt0
wenzelm@58928
   271
blanchet@55211
   272
    (* Make sure only type constraints inserted by the type annotation code are printed. *)
blanchet@56985
   273
    val ctxt = ctxt0
blanchet@56985
   274
      |> Config.put show_markup false
blanchet@56985
   275
      |> Config.put Printer.show_type_emphasis false
blanchet@56985
   276
      |> Config.put show_types false
blanchet@56985
   277
      |> Config.put show_sorts false
blanchet@56985
   278
      |> Config.put show_consts false
blanchet@55211
   279
blanchet@55216
   280
    fun add_str s' = apfst (suffix s')
blanchet@55211
   281
blanchet@55211
   282
    fun of_indent ind = replicate_string (ind * indent_size) " "
blanchet@55211
   283
    fun of_moreover ind = of_indent ind ^ "moreover\n"
blanchet@55211
   284
    fun of_label l = if l = no_label then "" else string_of_label l ^ ": "
blanchet@55211
   285
blanchet@55211
   286
    fun of_obtain qs nr =
blanchet@55211
   287
      (if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately "
blanchet@55211
   288
       else if nr = 1 orelse member (op =) qs Then then "then "
blanchet@55211
   289
       else "") ^ "obtain"
blanchet@55211
   290
blanchet@55211
   291
    fun of_show_have qs = if member (op =) qs Show then "show" else "have"
blanchet@61756
   292
    fun of_thus_hence qs = if member (op =) qs Show then "then show" else "then have"
blanchet@55211
   293
blanchet@55211
   294
    fun of_have qs nr =
blanchet@55211
   295
      if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately " ^ of_show_have qs
blanchet@55211
   296
      else if nr = 1 orelse member (op =) qs Then then of_thus_hence qs
blanchet@55211
   297
      else of_show_have qs
blanchet@55211
   298
blanchet@55211
   299
    fun add_term term (s, ctxt) =
blanchet@55211
   300
      (s ^ (term
blanchet@55211
   301
            |> singleton (Syntax.uncheck_terms ctxt)
blanchet@55213
   302
            |> annotate_types_in_term ctxt
wenzelm@66020
   303
            |> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of)
blanchet@55211
   304
            |> simplify_spaces
wenzelm@58928
   305
            |> maybe_quote keywords),
blanchet@57669
   306
       ctxt |> perhaps (try (Variable.auto_fixes term)))
blanchet@55211
   307
blanchet@56983
   308
    fun using_facts [] [] = ""
blanchet@56983
   309
      | using_facts ls ss = enclose "using " " " (space_implode " " (map string_of_label ls @ ss))
blanchet@55257
   310
blanchet@55211
   311
    (* Local facts are always passed via "using", which affects "meson" and "metis". This is
blanchet@55211
   312
       arguably stylistically superior, because it emphasises the structure of the proof. It is also
blanchet@61756
   313
       more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "then"
blanchet@61756
   314
       is introduced. See also "tac_of_method" in "Sledgehammer_Isar_Preplay". *)
blanchet@57287
   315
    fun of_method ls ss meth =
blanchet@57287
   316
      let val direct = is_proof_method_direct meth in
blanchet@55281
   317
        using_facts ls (if direct then [] else ss) ^
blanchet@57287
   318
        "by " ^ string_of_proof_method ctxt (if direct then ss else []) meth
blanchet@55281
   319
      end
blanchet@55211
   320
blanchet@55211
   321
    fun of_free (s, T) =
wenzelm@58928
   322
      maybe_quote keywords s ^ " :: " ^
wenzelm@66020
   323
      maybe_quote keywords (simplify_spaces (Print_Mode.setmp [] (Syntax.string_of_typ ctxt) T))
blanchet@55211
   324
blanchet@55211
   325
    fun add_frees xs (s, ctxt) =
blanchet@57669
   326
      (s ^ space_implode " and " (map of_free xs), ctxt |> fold Variable.auto_fixes (map Free xs))
blanchet@55211
   327
blanchet@55211
   328
    fun add_fix _ [] = I
blanchet@55281
   329
      | add_fix ind xs = add_str (of_indent ind ^ "fix ") #> add_frees xs #> add_str "\n"
blanchet@55211
   330
blanchet@55211
   331
    fun add_assm ind (l, t) =
blanchet@55281
   332
      add_str (of_indent ind ^ "assume " ^ of_label l) #> add_term t #> add_str "\n"
blanchet@55211
   333
blanchet@55211
   334
    fun of_subproof ind ctxt proof =
blanchet@55211
   335
      let
blanchet@55211
   336
        val ind = ind + 1
blanchet@55211
   337
        val s = of_proof ind ctxt proof
blanchet@55211
   338
        val prefix = "{ "
blanchet@55211
   339
        val suffix = " }"
blanchet@55211
   340
      in
blanchet@55211
   341
        replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
blanchet@55211
   342
        String.extract (s, ind * indent_size, SOME (size s - ind * indent_size - 1)) ^
blanchet@55211
   343
        suffix ^ "\n"
blanchet@55211
   344
      end
blanchet@55211
   345
    and of_subproofs _ _ _ [] = ""
blanchet@55281
   346
      | of_subproofs ind ctxt qs subs =
blanchet@55211
   347
        (if member (op =) qs Then then of_moreover ind else "") ^
blanchet@55281
   348
        space_implode (of_moreover ind) (map (of_subproof ind ctxt) subs)
blanchet@55281
   349
    and add_step_pre ind qs subs (s, ctxt) =
blanchet@55281
   350
      (s ^ of_subproofs ind ctxt qs subs ^ of_indent ind, ctxt)
blanchet@55211
   351
    and add_step ind (Let (t1, t2)) =
blanchet@57776
   352
        add_str (of_indent ind ^ "let ") #> add_term t1 #> add_str " = " #> add_term t2
blanchet@57776
   353
        #> add_str "\n"
blanchet@55309
   354
      | add_step ind (Prove (qs, xs, l, t, subs, (ls, ss), meth :: _, comment)) =
blanchet@55281
   355
        add_step_pre ind qs subs
blanchet@55211
   356
        #> (case xs of
blanchet@57776
   357
            [] => add_str (of_have qs (length subs) ^ " ")
blanchet@58071
   358
          | _ =>
blanchet@58071
   359
            add_str (of_obtain qs (length subs) ^ " ")
blanchet@58071
   360
            #> add_frees xs
blanchet@58071
   361
            #> add_str (" where\n" ^ of_indent (ind + 1)))
blanchet@55217
   362
        #> add_str (of_label l)
blanchet@58087
   363
        #> add_term (if is_thesis ctxt t then HOLogic.mk_Trueprop (Var thesis_var) else t)
blanchet@58054
   364
        #> add_str ("\n" ^ of_indent (ind + 1) ^ of_method ls ss meth ^
blanchet@57776
   365
          (if comment = "" then "" else " (* " ^ comment ^ " *)") ^ "\n")
blanchet@55211
   366
    and add_steps ind = fold (add_step ind)
blanchet@55211
   367
    and of_proof ind ctxt (Proof (xs, assms, steps)) =
blanchet@55281
   368
      ("", ctxt)
blanchet@55281
   369
      |> add_fix ind xs
blanchet@55281
   370
      |> fold (add_assm ind) assms
blanchet@55281
   371
      |> add_steps ind steps
blanchet@55281
   372
      |> fst
blanchet@55211
   373
  in
blanchet@57286
   374
    (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
blanchet@57287
   375
    of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
blanchet@57287
   376
    of_indent 0 ^ (if n = 1 then "qed" else "next")
blanchet@55211
   377
  end
blanchet@55211
   378
blanchet@54504
   379
end;