simplified byline, isar_qualifier
authorsmolkas
Mon Feb 18 12:16:02 2013 +0100 (2013-02-18)
changeset 5117806689dbfe072
parent 51177 e8c9755fd14e
child 51179 0d5f8812856f
simplified byline, isar_qualifier
src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
     1.1 --- a/src/HOL/Sledgehammer.thy	Mon Feb 18 11:33:43 2013 +0100
     1.2 +++ b/src/HOL/Sledgehammer.thy	Mon Feb 18 12:16:02 2013 +0100
     1.3 @@ -11,6 +11,7 @@
     1.4  keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl
     1.5  begin
     1.6  
     1.7 +
     1.8  ML_file "Tools/Sledgehammer/async_manager.ML"
     1.9  ML_file "Tools/Sledgehammer/sledgehammer_util.ML"
    1.10  ML_file "Tools/Sledgehammer/sledgehammer_fact.ML"
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Mon Feb 18 11:33:43 2013 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Mon Feb 18 12:16:02 2013 +0100
     2.3 @@ -34,7 +34,6 @@
     2.4  fun get i v = Vector.sub (v, i)
     2.5  fun replace x i v = Vector.update (v, i, x)
     2.6  fun update f i v = replace (get i v |> f) i v
     2.7 -fun v_map_index f v = Vector.foldr (op::) nil v |> map_index f |> Vector.fromList
     2.8  fun v_fold_index f v s =
     2.9    Vector.foldl (fn (x, (i, s)) => (i+1, f (i, x) s)) (0, s) v |> snd
    2.10  
    2.11 @@ -69,7 +68,7 @@
    2.12        val metis_fail = fn () => !metis_fail
    2.13      end
    2.14  
    2.15 -    (* compress proof on top level - do not compress case splits *)
    2.16 +    (* compress proof on top level - do not compress subproofs *)
    2.17      fun compress_top_level on_top_level ctxt proof =
    2.18      let
    2.19        (* proof vector *)
    2.20 @@ -87,13 +86,13 @@
    2.21        val lookup_indices = map_filter (Label_Table.lookup label_index_table)
    2.22  
    2.23        (* proof references *)
    2.24 -      fun refs (Obtain (_, _, _, _, By_Metis (lfs, _))) = lookup_indices lfs
    2.25 -        | refs (Prove (_, _, _, By_Metis (lfs, _))) = lookup_indices lfs
    2.26 -        | refs (Prove (_, _, _, Case_Split cases)) = maps (maps refs) cases
    2.27 -        | refs (Prove (_, _, _, Subblock proof)) = maps refs proof
    2.28 +      fun refs (Obtain (_, _, _, _, By_Metis (subproofs, (lfs, _)))) =
    2.29 +              maps (maps refs) subproofs @ lookup_indices lfs
    2.30 +        | refs (Prove (_, _, _, By_Metis (subproofs, (lfs, _)))) =
    2.31 +              maps (maps refs) subproofs @ lookup_indices lfs
    2.32          | refs _ = []
    2.33        val refed_by_vect =
    2.34 -        Vector.tabulate (n, (fn _ => []))
    2.35 +        Vector.tabulate (n, K [])
    2.36          |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) proof
    2.37          |> Vector.map rev (* after rev, indices are sorted in ascending order *)
    2.38  
    2.39 @@ -113,11 +112,10 @@
    2.40  
    2.41        (* cache metis preplay times in lazy time vector *)
    2.42        val metis_time =
    2.43 -        v_map_index
    2.44 +        Vector.map
    2.45            (if not preplay then K (zero_preplay_time) #> Lazy.value
    2.46             else
    2.47 -             apsnd the (* step *)
    2.48 -             #> apfst (fn i => try (get (i-1) #> the) proof_vect) (* succedent *)
    2.49 +             the
    2.50               #> try_metis debug type_enc lam_trans ctxt preplay_timeout
    2.51               #> handle_metis_fail
    2.52               #> Lazy.lazy)
    2.53 @@ -129,18 +127,20 @@
    2.54            zero_preplay_time lazy_time_vector
    2.55  
    2.56        (* Merging *)
    2.57 -      fun merge (Prove (_, label1, _, By_Metis (lfs1, gfs1))) step2 =
    2.58 +      fun merge (Prove (_, label1, _, By_Metis (subproofs1, (lfs1, gfs1))))
    2.59 +                                                                        step2 =
    2.60            let
    2.61 -            val (step_constructor, lfs2, gfs2) =
    2.62 +            val (step_constructor, (subproofs2, (lfs2, gfs2))) =
    2.63                (case step2 of
    2.64 -                (Prove (qs2, label2, t, By_Metis (lfs2, gfs2))) =>
    2.65 -                  (fn by => Prove (qs2, label2, t, by), lfs2, gfs2)
    2.66 -              | (Obtain (qs2, xs, label2, t, By_Metis (lfs2, gfs2))) =>
    2.67 -                  (fn by => Obtain (qs2, xs, label2, t, by), lfs2, gfs2)
    2.68 +                Prove (qs2, label2, t, By_Metis x) =>
    2.69 +                  (fn by => Prove (qs2, label2, t, by), x)
    2.70 +              | Obtain (qs2, xs, label2, t, By_Metis x) =>
    2.71 +                  (fn by => Obtain (qs2, xs, label2, t, by), x)
    2.72                | _ => error "sledgehammer_compress: unmergeable Isar steps" )
    2.73              val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1
    2.74              val gfs = union (op =) gfs1 gfs2
    2.75 -          in step_constructor (By_Metis (lfs, gfs)) end
    2.76 +            val subproofs = subproofs1 @ subproofs2
    2.77 +          in step_constructor (By_Metis (subproofs, (lfs, gfs))) end
    2.78          | merge _ _ = error "sledgehammer_compress: unmergeable Isar steps"
    2.79  
    2.80        fun try_merge metis_time (s1, i) (s2, j) =
    2.81 @@ -156,8 +156,8 @@
    2.82                  val s12 = merge s1 s2
    2.83                  val timeout = time_mult merge_timeout_slack (Time.+(t1, t2))
    2.84                in
    2.85 -                case try_metis_quietly debug type_enc lam_trans ctxt timeout
    2.86 -                (NONE, s12) () of
    2.87 +                case try_metis_quietly debug type_enc lam_trans
    2.88 +                                                        ctxt timeout s12 () of
    2.89                    (true, _) => (NONE, metis_time)
    2.90                  | exact_time =>
    2.91                    (SOME s12, metis_time
    2.92 @@ -218,28 +218,25 @@
    2.93            | enrich_with_step _ = I
    2.94          val rich_ctxt = fold enrich_with_step proof ctxt
    2.95  
    2.96 -        (* compress subproofs (case_splits and subblocks) and top-levl *)
    2.97 +        (* compress subproofs and top-levl proof *)
    2.98          val ((proof, top_level_time), lower_level_time) =
    2.99 -          proof |> do_subproof rich_ctxt
   2.100 +          proof |> do_subproofs rich_ctxt
   2.101                  |>> compress_top_level on_top_level rich_ctxt
   2.102        in
   2.103          (proof, add_preplay_time lower_level_time top_level_time)
   2.104        end
   2.105  
   2.106 -    and do_subproof ctxt proof =
   2.107 +    and do_subproofs ctxt proof =
   2.108        let
   2.109 -        fun compress_each_and_collect_time compress candidates =
   2.110 -          let fun f_m cand time = compress cand ||> add_preplay_time time
   2.111 -          in fold_map f_m candidates zero_preplay_time end
   2.112 -        val compress_subproof =
   2.113 +        fun compress_each_and_collect_time compress subproofs =
   2.114 +          let fun f_m proof time = compress proof ||> add_preplay_time time
   2.115 +          in fold_map f_m subproofs zero_preplay_time end
   2.116 +        val compress_subproofs =
   2.117            compress_each_and_collect_time (do_proof false ctxt)
   2.118 -        fun compress (Prove (qs, l, t, Case_Split cases)) =
   2.119 -            let val (cases, time) = compress_subproof cases
   2.120 -            in (Prove (qs, l, t, Case_Split cases), time) end
   2.121 -          | compress (Prove (qs, l, t, Subblock proof)) =
   2.122 -            let val ([proof], time) = compress_subproof [proof]
   2.123 -            in (Prove (qs, l, t, Subblock proof), time) end
   2.124 -          | compress step = (step, zero_preplay_time)
   2.125 +        fun compress (Prove (qs, l, t, By_Metis(subproofs, facts))) =
   2.126 +              let val (subproofs, time) = compress_subproofs subproofs
   2.127 +              in (Prove (qs, l, t, By_Metis(subproofs, facts)), time) end
   2.128 +          | compress atomic_step = (atomic_step, zero_preplay_time)
   2.129        in
   2.130          compress_each_and_collect_time compress proof
   2.131        end
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Mon Feb 18 11:33:43 2013 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Mon Feb 18 12:16:02 2013 +0100
     3.3 @@ -14,9 +14,9 @@
     3.4    val add_preplay_time : preplay_time -> preplay_time -> preplay_time
     3.5    val string_of_preplay_time : preplay_time -> string
     3.6    val try_metis : bool -> string -> string -> Proof.context ->
     3.7 -    Time.time -> (isar_step option * isar_step) -> unit -> preplay_time
     3.8 +    Time.time -> isar_step -> unit -> preplay_time
     3.9    val try_metis_quietly : bool -> string -> string -> Proof.context ->
    3.10 -    Time.time -> (isar_step option * isar_step) -> unit -> preplay_time
    3.11 +    Time.time -> isar_step -> unit -> preplay_time
    3.12  end
    3.13  
    3.14  structure Sledgehammer_Preplay : SLEDGEHAMMER_PREPLAY =
    3.15 @@ -55,13 +55,30 @@
    3.16      |> op @
    3.17      |> maps (thms_of_name ctxt)
    3.18  
    3.19 -exception ZEROTIME
    3.20 -fun try_metis debug type_enc lam_trans ctxt timeout (succedent, step) =
    3.21 +(* *)
    3.22 +fun thm_of_term ctxt = Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
    3.23 +fun fact_of_subproof ctxt proof =
    3.24    let
    3.25 -    val (t, byline, obtain) =
    3.26 +    val (fixed_frees, assms, concl) = split_proof proof
    3.27 +    val var_idx = maxidx_of_term concl + 1
    3.28 +    fun var_of_free (x, T) = Var((x, var_idx), T)
    3.29 +    val substitutions =
    3.30 +      map (`var_of_free #> swap #> apfst Free) fixed_frees
    3.31 +    val assms = assms |> map snd
    3.32 +  in
    3.33 +    Logic.list_implies(assms, concl)
    3.34 +      |> subst_free substitutions
    3.35 +      |> thm_of_term ctxt
    3.36 +  end
    3.37 +
    3.38 +exception ZEROTIME
    3.39 +fun try_metis debug type_enc lam_trans ctxt timeout step =
    3.40 +  let
    3.41 +    val (t, subproofs, fact_names, obtain) =
    3.42        (case step of
    3.43 -        Prove (_, _, t, byline) => (t, byline, false)
    3.44 -      | Obtain (_, xs, _, t, byline) =>
    3.45 +        Prove (_, _, t, By_Metis (subproofs, fact_names)) =>
    3.46 +            (t, subproofs, fact_names, false)
    3.47 +      | Obtain (_, xs, _, t, By_Metis (subproofs, fact_names)) =>
    3.48          (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
    3.49             (see ~~/src/Pure/Isar/obtain.ML) *)
    3.50          let
    3.51 @@ -77,39 +94,12 @@
    3.52            val prop =
    3.53              Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
    3.54          in
    3.55 -          (prop, byline, true)
    3.56 +          (prop, subproofs, fact_names, true)
    3.57          end
    3.58        | _ => raise ZEROTIME)
    3.59 -    val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
    3.60      val facts =
    3.61 -      (case byline of
    3.62 -        By_Metis fact_names => resolve_fact_names ctxt fact_names
    3.63 -      | Case_Split cases =>
    3.64 -        (case the succedent of
    3.65 -            Assume (_, t) => make_thm t
    3.66 -          | Obtain (_, _, _, t, _) => make_thm t
    3.67 -          | Prove (_, _, t, _) => make_thm t
    3.68 -          | _ => error "preplay error: unexpected succedent of case split")
    3.69 -        :: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t)
    3.70 -                        | _ => error "preplay error: malformed case split")
    3.71 -                   #> make_thm) cases
    3.72 -      | Subblock proof =>
    3.73 -        let
    3.74 -          val (steps, last_step) = split_last proof
    3.75 -          val concl =
    3.76 -            (case last_step of
    3.77 -              Prove (_, _, t, _) => t
    3.78 -            | _ => error "preplay error: unexpected conclusion of subblock")
    3.79 -          (* TODO: assuming Fix may only occur at the beginning of a subblock,
    3.80 -             this can be optimized *)
    3.81 -          val fixed_frees = fold (fn Fix xs => append xs | _ => I) steps []
    3.82 -          val var_idx = maxidx_of_term concl + 1
    3.83 -          fun var_of_free (x, T) = Var((x, var_idx), T)
    3.84 -          val substitutions =
    3.85 -            map (`var_of_free #> swap #> apfst Free) fixed_frees
    3.86 -        in
    3.87 -          concl |> subst_free substitutions |> make_thm |> single
    3.88 -        end)
    3.89 +      map (fact_of_subproof ctxt) subproofs @
    3.90 +      resolve_fact_names ctxt fact_names
    3.91      val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug
    3.92                      |> obtain ? Config.put Metis_Tactic.new_skolem true
    3.93      val goal =
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Mon Feb 18 11:33:43 2013 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Mon Feb 18 12:16:02 2013 +0100
     4.3 @@ -9,9 +9,11 @@
     4.4  signature SLEDGEHAMMER_PROOF =
     4.5  sig
     4.6  	type label = string * int
     4.7 +  val no_label : label
     4.8    type facts = label list * string list
     4.9 +  val no_facts : facts
    4.10  
    4.11 -  datatype isar_qualifier = Show | Then | Ultimately
    4.12 +  datatype isar_qualifier = Show | Then
    4.13  
    4.14    datatype isar_step =
    4.15      Fix of (string * typ) list |
    4.16 @@ -21,22 +23,26 @@
    4.17        isar_qualifier list * (string * typ) list * label * term * byline |
    4.18      Prove of isar_qualifier list * label * term * byline
    4.19    and byline =
    4.20 -    By_Metis of facts |
    4.21 -    Case_Split of isar_step list list |
    4.22 -    Subblock of isar_step list
    4.23 +    By_Metis of isar_step list list * facts
    4.24  
    4.25    val string_for_label : label -> string
    4.26    val metis_steps_top_level : isar_step list -> int
    4.27    val metis_steps_total : isar_step list -> int
    4.28 +  val term_of_assm : isar_step -> term
    4.29 +  val term_of_prove : isar_step -> term
    4.30 +  val split_proof :
    4.31 +    isar_step list -> (string * typ) list * (label * term) list * term
    4.32  end
    4.33  
    4.34  structure Sledgehammer_Proof : SLEDGEHAMMER_PROOF =
    4.35  struct
    4.36  
    4.37  type label = string * int
    4.38 +val no_label = ("", ~1)
    4.39  type facts = label list * string list
    4.40 +val no_facts = ([],[])
    4.41  
    4.42 -datatype isar_qualifier = Show | Then | Ultimately
    4.43 +datatype isar_qualifier = Show | Then
    4.44  
    4.45  datatype isar_step =
    4.46    Fix of (string * typ) list |
    4.47 @@ -45,9 +51,7 @@
    4.48    Obtain of isar_qualifier list * (string * typ) list * label * term * byline |
    4.49    Prove of isar_qualifier list * label * term * byline
    4.50  and byline =
    4.51 -  By_Metis of facts |
    4.52 -  Case_Split of isar_step list list |
    4.53 -  Subblock of isar_step list
    4.54 +  By_Metis of isar_step list list * facts
    4.55  
    4.56  fun string_for_label (s, num) = s ^ string_of_int num
    4.57  
    4.58 @@ -55,12 +59,33 @@
    4.59    fold (fn Obtain _ => Integer.add 1 | Prove _ => Integer.add 1 | _ => I)
    4.60         proof 0
    4.61  fun metis_steps_total proof =
    4.62 -  fold (fn Obtain _ => Integer.add 1
    4.63 -         | Prove (_, _, _, By_Metis _) => Integer.add 1
    4.64 -         | Prove (_, _, _, Case_Split cases) =>
    4.65 -           Integer.add (fold (Integer.add o metis_steps_total) cases 1)
    4.66 -         | Prove (_, _, _, Subblock subproof) =>
    4.67 -           Integer.add (metis_steps_total subproof + 1)
    4.68 -         | _ => I) proof 0
    4.69 +  let
    4.70 +    fun add_substeps subproofs i =
    4.71 +      Integer.add (fold Integer.add (map metis_steps_total subproofs) i)
    4.72 +  in
    4.73 +    fold
    4.74 +    (fn Obtain (_, _, _, _, By_Metis (subproofs, _)) => add_substeps subproofs 1
    4.75 +      | Prove (_, _, _, By_Metis (subproofs, _)) => add_substeps subproofs 1
    4.76 +      | _ => I)
    4.77 +    proof 0
    4.78 +  end
    4.79 +
    4.80 +fun term_of_assm (Assume (_, t)) = t
    4.81 +  | term_of_assm _ = error "sledgehammer proof: unexpected constructor"
    4.82 +fun term_of_prove (Prove (_, _, t, _)) = t
    4.83 +  | term_of_prove _ = error "sledgehammer proof: unexpected constructor"
    4.84 +
    4.85 +fun split_proof proof =
    4.86 +  let
    4.87 +    fun split_step step (fixes, assms, _) =
    4.88 +      (case step of
    4.89 +        Fix xs   => (xs@fixes, assms,    step)
    4.90 +      | Assume a => (fixes,    a::assms, step)
    4.91 +      | _        => (fixes,    assms,    step))
    4.92 +    val (fixes, assms, concl) =
    4.93 +      fold split_step proof ([], [], Let (Term.dummy, Term.dummy)) (* FIXME: hack *)
    4.94 +  in
    4.95 +    (rev fixes, rev assms, term_of_prove concl)
    4.96 +  end
    4.97  
    4.98  end
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Feb 18 11:33:43 2013 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Feb 18 12:16:02 2013 +0100
     5.3 @@ -456,23 +456,29 @@
     5.4         map (replace_dependencies_in_line (name, deps)) lines)  (* drop line *)
     5.5  
     5.6  val indent_size = 2
     5.7 -val no_label = ("", ~1)
     5.8  
     5.9  fun string_for_proof ctxt type_enc lam_trans i n =
    5.10    let
    5.11 +    fun maybe_show qs = if member (op =) qs Show then "show" else "have"
    5.12      fun of_indent ind = replicate_string (ind * indent_size) " "
    5.13      fun of_free (s, T) =
    5.14        maybe_quote s ^ " :: " ^
    5.15        maybe_quote (simplify_spaces (with_vanilla_print_mode
    5.16          (Syntax.string_of_typ ctxt) T))
    5.17      val of_frees = space_implode " and " o map of_free
    5.18 +    fun maybe_moreover ind qs nr_subproofs =
    5.19 +        if member (op =) qs Then andalso nr_subproofs > 0
    5.20 +          then of_indent ind ^ "moreover\n"
    5.21 +          else ""
    5.22      fun of_label l = if l = no_label then "" else string_for_label l ^ ": "
    5.23 -    fun of_have qs =
    5.24 -      (if member (op =) qs Ultimately then "ultimately " else "") ^
    5.25 -      (if member (op =) qs Then then
    5.26 -         if member (op =) qs Show then "thus" else "hence"
    5.27 -       else
    5.28 -         if member (op =) qs Show then "show" else "have")
    5.29 +    fun of_have qs nr_subproofs =
    5.30 +      if (member (op =) qs Then andalso nr_subproofs>0) orelse (nr_subproofs>1)
    5.31 +        then "ultimately " ^ maybe_show qs
    5.32 +        else
    5.33 +          (if member (op =) qs Then orelse nr_subproofs>0 then
    5.34 +             if member (op =) qs Show then "thus" else "hence"
    5.35 +           else
    5.36 +             maybe_show qs)
    5.37      fun of_obtain qs xs =
    5.38        (if member (op =) qs Then then "then " else "") ^ "obtain " ^
    5.39        of_frees xs ^ " where"
    5.40 @@ -492,21 +498,19 @@
    5.41          of_indent ind ^ "let " ^ of_term t1 ^ " = " ^ of_term t2 ^ "\n"
    5.42        | of_step ind (Assume (l, t)) =
    5.43          of_indent ind ^ "assume " ^ of_label l ^ of_term t ^ "\n"
    5.44 -      | of_step ind (Obtain (qs, xs, l, t, By_Metis facts)) =
    5.45 +      | of_step ind (Obtain (qs, xs, l, t, By_Metis (subproofs, facts))) =      (* FIXME *)
    5.46 +        maybe_moreover ind qs (length subproofs) ^
    5.47 +        of_subproofs ind subproofs ^
    5.48          of_indent ind ^ of_obtain qs xs ^ " " ^
    5.49          of_label l ^ of_term t ^
    5.50          (* The new skolemizer puts the arguments in the same order as the ATPs
    5.51             (E and Vampire -- but see also "atp_proof_reconstruct.ML" regarding
    5.52             Vampire). *)
    5.53          of_metis ind "using [[metis_new_skolem]] " facts ^ "\n"
    5.54 -      | of_step ind (Prove (qs, l, t, By_Metis facts)) =
    5.55 -        of_prove ind qs l t facts
    5.56 -      | of_step ind (Prove (qs, l, t, Case_Split proofs)) =
    5.57 -        implode (map (prefix (of_indent ind ^ "moreover\n") o of_block ind)
    5.58 -                     proofs) ^
    5.59 -        of_prove ind qs l t ([], [])
    5.60 -      | of_step ind (Prove (qs, l, t, Subblock proof)) =
    5.61 -        of_block ind proof ^ of_prove ind qs l t ([], [])
    5.62 +      | of_step ind (Prove (qs, l, t, By_Metis (subproofs, facts))) =
    5.63 +        maybe_moreover ind qs (length subproofs) ^
    5.64 +        of_subproofs ind subproofs ^
    5.65 +        of_prove ind qs (length subproofs) l t facts
    5.66      and of_steps prefix suffix ind steps =
    5.67        let val s = implode (map (of_step ind) steps) in
    5.68          replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
    5.69 @@ -515,39 +519,39 @@
    5.70          suffix ^ "\n"
    5.71        end
    5.72      and of_block ind proof = of_steps "{ " " }" (ind + 1) proof
    5.73 -    and of_prove ind qs l t facts =
    5.74 -      of_indent ind ^ of_have qs ^ " " ^ of_label l ^ of_term t ^
    5.75 +    and of_subproofs ind subproofs =
    5.76 +        subproofs
    5.77 +          |> map (of_block ind)
    5.78 +          |> space_implode (of_indent ind ^ "moreover\n")
    5.79 +    and of_prove ind qs nr_subproofs l t facts =
    5.80 +      of_indent ind ^ of_have qs nr_subproofs ^ " " ^ of_label l ^ of_term t ^
    5.81        of_metis ind "" facts ^ "\n"
    5.82      (* One-step proofs are pointless; better use the Metis one-liner
    5.83         directly. *)
    5.84 -    and of_proof [Prove (_, _, _, By_Metis _)] = ""
    5.85 +    and of_proof [Prove (_, _, _, By_Metis ([], _))] = ""
    5.86        | of_proof proof =
    5.87          (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
    5.88          of_indent 0 ^ "proof -\n" ^ of_steps "" "" 1 proof ^ of_indent 0 ^
    5.89          (if n <> 1 then "next" else "qed")
    5.90    in of_proof end
    5.91  
    5.92 -fun used_labels_of_step (Obtain (_, _, _, _, By_Metis (ls, _))) = ls
    5.93 -  | used_labels_of_step (Prove (_, _, _, by)) =
    5.94 -    (case by of
    5.95 -       By_Metis (ls, _) => ls
    5.96 -     | Case_Split proofs => fold (union (op =) o used_labels_of) proofs []
    5.97 -     | Subblock proof => used_labels_of proof)
    5.98 -  | used_labels_of_step _ = []
    5.99 -and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []
   5.100 +fun add_labels_of_step (Obtain (_, _, _, _, By_Metis (subproofs, (ls, _)))) =
   5.101 +      union (op =) (add_labels_of_proofs subproofs ls)
   5.102 +  | add_labels_of_step (Prove (_, _, _, By_Metis (subproofs, (ls, _)))) =
   5.103 +      union (op =) (add_labels_of_proofs subproofs ls)
   5.104 +  | add_labels_of_step _ = I
   5.105 +and add_labels_of_proof proof = fold add_labels_of_step proof
   5.106 +and add_labels_of_proofs proofs = fold add_labels_of_proof proofs
   5.107  
   5.108  fun kill_useless_labels_in_proof proof =
   5.109    let
   5.110 -    val used_ls = used_labels_of proof
   5.111 +    val used_ls = add_labels_of_proof proof []
   5.112      fun do_label l = if member (op =) used_ls l then l else no_label
   5.113      fun do_step (Assume (l, t)) = Assume (do_label l, t)
   5.114 -      | do_step (Obtain (qs, xs, l, t, by)) = Obtain (qs, xs, do_label l, t, by)
   5.115 -      | do_step (Prove (qs, l, t, by)) =
   5.116 -        Prove (qs, do_label l, t,
   5.117 -               case by of
   5.118 -                 Case_Split proofs => Case_Split (map do_proof proofs)
   5.119 -               | Subblock proof => Subblock (do_proof proof)
   5.120 -               | _ => by)
   5.121 +      | do_step (Obtain (qs, xs, l, t, By_Metis (subproofs, facts))) =
   5.122 +          Obtain (qs, xs, do_label l, t, By_Metis (map do_proof subproofs, facts))
   5.123 +      | do_step (Prove (qs, l, t, By_Metis (subproofs, facts))) =
   5.124 +          Prove (qs, do_label l, t, By_Metis (map do_proof subproofs, facts))
   5.125        | do_step step = step
   5.126      and do_proof proof = map do_step proof
   5.127    in do_proof proof end
   5.128 @@ -565,12 +569,9 @@
   5.129          end
   5.130      fun do_facts subst =
   5.131        apfst (maps (the_list o AList.lookup (op =) subst))
   5.132 -    fun do_byline subst depth nexts by =
   5.133 -      case by of
   5.134 -        By_Metis facts => By_Metis (do_facts subst facts)
   5.135 -      | Case_Split proofs =>
   5.136 -        Case_Split (map (do_proof subst (depth + 1) (1, 1)) proofs)
   5.137 -      | Subblock proof => Subblock (do_proof subst depth nexts proof)
   5.138 +    fun do_byline subst depth nexts (By_Metis (subproofs, facts)) =
   5.139 +      By_Metis
   5.140 +        (map (do_proof subst (depth + 1) (1, 1)) subproofs, do_facts subst facts)
   5.141      and do_proof _ _ _ [] = []
   5.142        | do_proof subst depth (next_assum, next_have) (Assume (l, t) :: proof) =
   5.143          if l = no_label then
   5.144 @@ -608,27 +609,27 @@
   5.145        | label_of (Obtain (_, _, l, _, _)) = SOME l
   5.146        | label_of (Prove (_, l, _, _)) = SOME l
   5.147        | label_of _ = NONE
   5.148 -    fun chain_step (SOME l0)
   5.149 -                   (step as Obtain (qs, xs, l, t, By_Metis (lfs, gfs))) =
   5.150 -        if member (op =) lfs l0 then
   5.151 -          Obtain (Then :: qs, xs, l, t, By_Metis (lfs |> remove (op =) l0, gfs))
   5.152 -        else
   5.153 -          step
   5.154 -      | chain_step (SOME l0)
   5.155 -                   (step as Prove (qs, l, t, By_Metis (lfs, gfs))) =
   5.156 -        if member (op =) lfs l0 then
   5.157 -          Prove (Then :: qs, l, t, By_Metis (lfs |> remove (op =) l0, gfs))
   5.158 -        else
   5.159 -          step
   5.160 -      | chain_step _ (Prove (qs, l, t, Case_Split proofs)) =
   5.161 -        Prove (qs, l, t, Case_Split (map (chain_proof NONE) proofs))
   5.162 -      | chain_step _ (Prove (qs, l, t, Subblock proof)) =
   5.163 -        Prove (qs, l, t, Subblock (chain_proof NONE proof))
   5.164 +    fun do_qs_lfs NONE lfs = ([], lfs)
   5.165 +      | do_qs_lfs (SOME l0) lfs =
   5.166 +        if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0)
   5.167 +        else ([], lfs)
   5.168 +    fun chain_step lbl (Obtain (qs, xs, l, t,
   5.169 +                                        By_Metis (subproofs, (lfs, gfs)))) =
   5.170 +        let val (qs', lfs) = do_qs_lfs lbl lfs in
   5.171 +          Obtain (qs' @ qs, xs, l, t,
   5.172 +            By_Metis (chain_proofs subproofs, (lfs, gfs)))
   5.173 +        end
   5.174 +      | chain_step lbl (Prove (qs, l, t, By_Metis (subproofs, (lfs, gfs)))) =
   5.175 +        let val (qs', lfs) = do_qs_lfs lbl lfs in
   5.176 +          Prove (qs' @ qs, l, t,
   5.177 +            By_Metis (chain_proofs subproofs, (lfs, gfs)))
   5.178 +        end
   5.179        | chain_step _ step = step
   5.180      and chain_proof _ [] = []
   5.181        | chain_proof (prev as SOME _) (i :: is) =
   5.182          chain_step prev i :: chain_proof (label_of i) is
   5.183        | chain_proof _ (i :: is) = i :: chain_proof (label_of i) is
   5.184 +    and chain_proofs proofs = map (chain_proof NONE) proofs
   5.185    in chain_proof NONE end
   5.186  
   5.187  type isar_params =
   5.188 @@ -721,16 +722,16 @@
   5.189                | _ => fold (curry s_disj) lits @{term False}
   5.190              end
   5.191              |> HOLogic.mk_Trueprop |> close_form
   5.192 -        fun isar_proof_of_direct_proof outer accum [] =
   5.193 +        fun isar_proof_of_direct_proof outer predecessor accum [] =
   5.194              rev accum |> outer ? (append assms
   5.195                                    #> not (null params) ? cons (Fix params))
   5.196 -          | isar_proof_of_direct_proof outer accum (inf :: infs) =
   5.197 +          | isar_proof_of_direct_proof outer predecessor accum (inf :: infs) =
   5.198              let
   5.199                fun maybe_show outer c =
   5.200                  (outer andalso length c = 1 andalso subset (op =) (c, conjs))
   5.201                  ? cons Show
   5.202 -              fun do_rest step =
   5.203 -                isar_proof_of_direct_proof outer (step :: accum) infs
   5.204 +              fun do_rest lbl step =
   5.205 +                isar_proof_of_direct_proof outer lbl (step :: accum) infs
   5.206                val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
   5.207                fun skolems_of t =
   5.208                  Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
   5.209 @@ -741,8 +742,9 @@
   5.210                    val l = label_of_clause c
   5.211                    val t = prop_of_clause c
   5.212                    val by =
   5.213 -                    By_Metis (fold (add_fact_from_dependencies fact_names) gamma
   5.214 -                                   ([], []))
   5.215 +                    By_Metis ([],
   5.216 +                      (fold (add_fact_from_dependencies fact_names)
   5.217 +                            gamma no_facts))
   5.218                    fun prove outer = Prove (maybe_show outer c [], l, t, by)
   5.219                  in
   5.220                    if is_clause_tainted c then
   5.221 @@ -751,33 +753,35 @@
   5.222                        if is_clause_skolemize_rule g andalso
   5.223                           is_clause_tainted g then
   5.224                          let
   5.225 -                          val proof =
   5.226 +                          val subproof =
   5.227                              Fix (skolems_of (prop_of_clause g)) :: rev accum
   5.228                          in
   5.229 -                          isar_proof_of_direct_proof outer
   5.230 -                              [Prove (maybe_show outer c [Then],
   5.231 +                          isar_proof_of_direct_proof outer l
   5.232 +                              [Prove (maybe_show outer c [],
   5.233                                        label_of_clause c, prop_of_clause c,
   5.234 -                                      Subblock proof)] []
   5.235 +                                      By_Metis ([subproof], no_facts))] []
   5.236                          end
   5.237                        else
   5.238 -                        do_rest (prove outer)
   5.239 -                    | _ => do_rest (prove outer)
   5.240 +                        do_rest l (prove outer)
   5.241 +                    | _ => do_rest l (prove outer)
   5.242                    else
   5.243                      if is_clause_skolemize_rule c then
   5.244 -                      do_rest (Obtain ([], skolems_of t, l, t, by))
   5.245 +                      do_rest l (Obtain ([], skolems_of t, l, t, by))
   5.246                      else
   5.247 -                      do_rest (prove outer)
   5.248 +                      do_rest l (prove outer)
   5.249                  end
   5.250                | Cases cases =>
   5.251                  let
   5.252                    fun do_case (c, infs) =
   5.253                      Assume (label_of_clause c, prop_of_clause c) ::
   5.254 -                    isar_proof_of_direct_proof false [] infs
   5.255 +                    isar_proof_of_direct_proof false no_label [] infs
   5.256                    val c = succedent_of_cases cases
   5.257 +                  val l = label_of_clause c
   5.258                  in
   5.259 -                  do_rest (Prove (maybe_show outer c [Ultimately],
   5.260 -                                  label_of_clause c, prop_of_clause c,
   5.261 -                                  Case_Split (map do_case cases)))
   5.262 +                  do_rest l
   5.263 +                    (Prove (maybe_show outer c [],
   5.264 +                            l, prop_of_clause c,
   5.265 +                            By_Metis (map do_case cases, ([predecessor], []))))
   5.266                  end
   5.267              end
   5.268          val cleanup_labels_in_proof =
   5.269 @@ -787,7 +791,7 @@
   5.270          val (isar_proof, (preplay_fail, preplay_time)) =
   5.271            refute_graph
   5.272            |> redirect_graph axioms tainted bot
   5.273 -          |> isar_proof_of_direct_proof true []
   5.274 +          |> isar_proof_of_direct_proof true no_label []
   5.275            |> (if not preplay andalso isar_compress <= 1.0 then
   5.276                  rpair (false, (true, seconds 0.0))
   5.277                else