1.1 --- a/src/HOL/Sledgehammer.thy	Mon Feb 18 12:16:02 2013 +0100
     1.2 +++ b/src/HOL/Sledgehammer.thy	Mon Feb 18 12:16:27 2013 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4  ML_file "Tools/Sledgehammer/sledgehammer_annotate.ML"
     1.5  ML_file "Tools/Sledgehammer/sledgehammer_preplay.ML"
     1.6  ML_file "Tools/Sledgehammer/sledgehammer_compress.ML"
     1.7 -ML_file "Tools/Sledgehammer/sledgehammer_reconstruct.ML" 
     1.8 +ML_file "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
     1.9  ML_file "Tools/Sledgehammer/sledgehammer_provers.ML"
    1.10  ML_file "Tools/Sledgehammer/sledgehammer_minimize.ML"
    1.11  ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML"

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Mon Feb 18 12:16:02 2013 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML	Mon Feb 18 12:16:27 2013 +0100
     2.3 @@ -2,7 +2,7 @@
     2.4      Author:     Jasmin Blanchette, TU Muenchen
     2.5      Author:     Steffen Juilf Smolka, TU Muenchen
     2.6  
     2.7 -Supplement term with explicit type constraints that show up as 
     2.8 +Supplement term with explicit type constraints that show up as
     2.9  type annotations when printing the term.
    2.10  *)
    2.11  

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Mon Feb 18 12:16:02 2013 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Mon Feb 18 12:16:27 2013 +0100
     3.3 @@ -7,11 +7,11 @@
     3.4  
     3.5  signature SLEDGEHAMMER_COMPRESS =
     3.6  sig
     3.7 -  type isar_step = Sledgehammer_Proof.isar_step
     3.8 +  type isar_proof = Sledgehammer_Proof.isar_proof
     3.9    type preplay_time = Sledgehammer_Preplay.preplay_time
    3.10    val compress_proof :
    3.11      bool -> Proof.context -> string -> string -> bool -> Time.time option
    3.12 -    -> real -> isar_step list -> isar_step list * (bool * preplay_time)
    3.13 +    -> real -> isar_proof -> isar_proof * (bool * preplay_time)
    3.14  end
    3.15  
    3.16  structure Sledgehammer_Compress : SLEDGEHAMMER_COMPRESS =
    3.17 @@ -68,38 +68,37 @@
    3.18        val metis_fail = fn () => !metis_fail
    3.19      end
    3.20  
    3.21 -    (* compress proof on top level - do not compress subproofs *)
    3.22 -    fun compress_top_level on_top_level ctxt proof =
    3.23 +    (* compress top level steps - do not compress subproofs *)
    3.24 +    fun compress_top_level on_top_level ctxt steps =
    3.25      let
    3.26 -      (* proof vector *)
    3.27 -      val proof_vect = proof |> map SOME |> Vector.fromList
    3.28 -      val n = Vector.length proof_vect
    3.29 -      val n_metis = metis_steps_top_level proof
    3.30 +      (* proof step vector *)
    3.31 +      val step_vect = steps |> map SOME |> Vector.fromList
    3.32 +      val n = Vector.length step_vect
    3.33 +      val n_metis = add_metis_steps_top_level steps 0
    3.34        val target_n_metis = Real.fromInt n_metis / isar_compress |> Real.round
    3.35  
    3.36 -      (* table for mapping from (top-level-)label to proof position *)
    3.37 -      fun update_table (i, Assume (l, _)) = Label_Table.update_new (l, i)
    3.38 +      (* table for mapping from (top-level-)label to step_vect position *)
    3.39 +      fun update_table (i, Prove (_, l, _, _)) = Label_Table.update_new (l, i)
    3.40          | update_table (i, Obtain (_, _, l, _, _)) = Label_Table.update_new (l, i)
    3.41 -        | update_table (i, Prove (_, l, _, _)) = Label_Table.update_new (l, i)
    3.42          | update_table _ = I
    3.43 -      val label_index_table = fold_index update_table proof Label_Table.empty
    3.44 +      val label_index_table = fold_index update_table steps Label_Table.empty
    3.45        val lookup_indices = map_filter (Label_Table.lookup label_index_table)
    3.46  
    3.47 -      (* proof references *)
    3.48 -      fun refs (Obtain (_, _, _, _, By_Metis (subproofs, (lfs, _)))) =
    3.49 -              maps (maps refs) subproofs @ lookup_indices lfs
    3.50 -        | refs (Prove (_, _, _, By_Metis (subproofs, (lfs, _)))) =
    3.51 -              maps (maps refs) subproofs @ lookup_indices lfs
    3.52 -        | refs _ = []
    3.53 +      (* proof step references *)
    3.54 +      fun refs step =
    3.55 +        (case byline_of_step step of
    3.56 +          NONE => []
    3.57 +        | SOME (By_Metis (subproofs, (lfs, _))) =>
    3.58 +            maps (steps_of_proof #> maps refs) subproofs @ lookup_indices lfs)
    3.59        val refed_by_vect =
    3.60          Vector.tabulate (n, K [])
    3.61 -        |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) proof
    3.62 +        |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) steps
    3.63          |> Vector.map rev (* after rev, indices are sorted in ascending order *)
    3.64  
    3.65        (* candidates for elimination, use table as priority queue (greedy
    3.66           algorithm) *)
    3.67 -      fun add_if_cand proof_vect (i, [j]) =
    3.68 -          (case (the (get i proof_vect), the (get j proof_vect)) of
    3.69 +      fun add_if_cand step_vect (i, [j]) =
    3.70 +          (case (the (get i step_vect), the (get j step_vect)) of
    3.71              (Prove (_, _, t, By_Metis _), Prove (_, _, _, By_Metis _)) =>
    3.72                cons (Term.size_of_term t, i)
    3.73            | (Prove (_, _, t, By_Metis _), Obtain (_, _, _, _, By_Metis _)) =>
    3.74 @@ -107,7 +106,7 @@
    3.75            | _ => I)
    3.76          | add_if_cand _ _ = I
    3.77        val cand_tab =
    3.78 -        v_fold_index (add_if_cand proof_vect) refed_by_vect []
    3.79 +        v_fold_index (add_if_cand step_vect) refed_by_vect []
    3.80          |> Inttab.make_list
    3.81  
    3.82        (* cache metis preplay times in lazy time vector *)
    3.83 @@ -119,7 +118,7 @@
    3.84               #> try_metis debug type_enc lam_trans ctxt preplay_timeout
    3.85               #> handle_metis_fail
    3.86               #> Lazy.lazy)
    3.87 -          proof_vect
    3.88 +          step_vect
    3.89  
    3.90        fun sum_up_time lazy_time_vector =
    3.91          Vector.foldl
    3.92 @@ -127,17 +126,16 @@
    3.93            zero_preplay_time lazy_time_vector
    3.94  
    3.95        (* Merging *)
    3.96 -      fun merge (Prove (_, label1, _, By_Metis (subproofs1, (lfs1, gfs1))))
    3.97 -                                                                        step2 =
    3.98 +      fun merge (Prove (_, lbl1, _, By_Metis (subproofs1, (lfs1, gfs1)))) step2 =
    3.99            let
   3.100              val (step_constructor, (subproofs2, (lfs2, gfs2))) =
   3.101                (case step2 of
   3.102 -                Prove (qs2, label2, t, By_Metis x) =>
   3.103 -                  (fn by => Prove (qs2, label2, t, by), x)
   3.104 -              | Obtain (qs2, xs, label2, t, By_Metis x) =>
   3.105 -                  (fn by => Obtain (qs2, xs, label2, t, by), x)
   3.106 +                Prove (qs2, lbl2, t, By_Metis x) =>
   3.107 +                  (fn by => Prove (qs2, lbl2, t, by), x)
   3.108 +              | Obtain (qs2, xs, lbl2, t, By_Metis x) =>
   3.109 +                  (fn by => Obtain (qs2, xs, lbl2, t, by), x)
   3.110                | _ => error "sledgehammer_compress: unmergeable Isar steps" )
   3.111 -            val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1
   3.112 +            val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1
   3.113              val gfs = union (op =) gfs1 gfs2
   3.114              val subproofs = subproofs1 @ subproofs2
   3.115            in step_constructor (By_Metis (subproofs, (lfs, gfs))) end
   3.116 @@ -166,45 +164,45 @@
   3.117  
   3.118                end))
   3.119  
   3.120 -      fun merge_steps metis_time proof_vect refed_by cand_tab n' n_metis' =
   3.121 +      fun merge_steps metis_time step_vect refed_by cand_tab n' n_metis' =
   3.122          if Inttab.is_empty cand_tab
   3.123            orelse n_metis' <= target_n_metis
   3.124            orelse (on_top_level andalso n'<3)
   3.125          then
   3.126            (Vector.foldr
   3.127 -             (fn (NONE, proof) => proof | (SOME s, proof) => s :: proof)
   3.128 -             [] proof_vect,
   3.129 +             (fn (NONE, steps) => steps | (SOME s, steps) => s :: steps)
   3.130 +             [] step_vect,
   3.131             sum_up_time metis_time)
   3.132          else
   3.133            let
   3.134              val (i, cand_tab) = pop_max cand_tab
   3.135              val j = get i refed_by |> the_single
   3.136 -            val s1 = get i proof_vect |> the
   3.137 -            val s2 = get j proof_vect |> the
   3.138 +            val s1 = get i step_vect |> the
   3.139 +            val s2 = get j step_vect |> the
   3.140            in
   3.141              case try_merge metis_time (s1, i) (s2, j) of
   3.142                (NONE, metis_time) =>
   3.143 -              merge_steps metis_time proof_vect refed_by cand_tab n' n_metis'
   3.144 +              merge_steps metis_time step_vect refed_by cand_tab n' n_metis'
   3.145              | (s, metis_time) =>
   3.146              let
   3.147                val refs = refs s1
   3.148                val refed_by = refed_by |> fold
   3.149                  (update (Ord_List.remove int_ord i #> Ord_List.insert int_ord j)) refs
   3.150                val new_candidates =
   3.151 -                fold (add_if_cand proof_vect)
   3.152 +                fold (add_if_cand step_vect)
   3.153                    (map (fn i => (i, get i refed_by)) refs) []
   3.154                val cand_tab = add_list cand_tab new_candidates
   3.155 -              val proof_vect = proof_vect |> replace NONE i |> replace s j
   3.156 +              val step_vect = step_vect |> replace NONE i |> replace s j
   3.157              in
   3.158 -              merge_steps metis_time proof_vect refed_by cand_tab (n' - 1)
   3.159 +              merge_steps metis_time step_vect refed_by cand_tab (n' - 1)
   3.160                            (n_metis' - 1)
   3.161              end
   3.162            end
   3.163      in
   3.164 -      merge_steps metis_time proof_vect refed_by_vect cand_tab n n_metis
   3.165 +      merge_steps metis_time step_vect refed_by_vect cand_tab n n_metis
   3.166      end
   3.167  
   3.168 -    fun do_proof on_top_level ctxt proof =
   3.169 +    fun do_proof on_top_level ctxt (Proof (fix, assms,steps)) =
   3.170        let
   3.171          (* Enrich context with top-level facts *)
   3.172          val thy = Proof_Context.theory_of ctxt
   3.173 @@ -212,21 +210,25 @@
   3.174          fun enrich_with_fact l t =
   3.175            Proof_Context.put_thms false
   3.176              (string_for_label l, SOME [Skip_Proof.make_thm thy t])
   3.177 -        fun enrich_with_step (Assume (l, t)) = enrich_with_fact l t
   3.178 +        fun enrich_with_step (Prove (_, l, t, _)) = enrich_with_fact l t
   3.179            | enrich_with_step (Obtain (_, _, l, t, _)) = enrich_with_fact l t
   3.180 -          | enrich_with_step (Prove (_, l, t, _)) = enrich_with_fact l t
   3.181            | enrich_with_step _ = I
   3.182 -        val rich_ctxt = fold enrich_with_step proof ctxt
   3.183 +        val enrich_with_steps = fold enrich_with_step
   3.184 +        fun enrich_with_assms (Assume assms) =
   3.185 +          fold (uncurry enrich_with_fact) assms
   3.186 +        val rich_ctxt =
   3.187 +          ctxt |> enrich_with_assms assms |> enrich_with_steps steps
   3.188  
   3.189 -        (* compress subproofs and top-levl proof *)
   3.190 -        val ((proof, top_level_time), lower_level_time) =
   3.191 -          proof |> do_subproofs rich_ctxt
   3.192 +        (* compress subproofs and top-levl steps *)
   3.193 +        val ((steps, top_level_time), lower_level_time) =
   3.194 +          steps |> do_subproofs rich_ctxt
   3.195                  |>> compress_top_level on_top_level rich_ctxt
   3.196        in
   3.197 -        (proof, add_preplay_time lower_level_time top_level_time)
   3.198 +        (Proof (fix, assms, steps),
   3.199 +          add_preplay_time lower_level_time top_level_time)
   3.200        end
   3.201  
   3.202 -    and do_subproofs ctxt proof =
   3.203 +    and do_subproofs ctxt subproofs =
   3.204        let
   3.205          fun compress_each_and_collect_time compress subproofs =
   3.206            let fun f_m proof time = compress proof ||> add_preplay_time time
   3.207 @@ -238,7 +240,7 @@
   3.208                in (Prove (qs, l, t, By_Metis(subproofs, facts)), time) end
   3.209            | compress atomic_step = (atomic_step, zero_preplay_time)
   3.210        in
   3.211 -        compress_each_and_collect_time compress proof
   3.212 +        compress_each_and_collect_time compress subproofs
   3.213        end
   3.214    in
   3.215      do_proof true ctxt proof

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Mon Feb 18 12:16:02 2013 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Mon Feb 18 12:16:27 2013 +0100
     4.3 @@ -50,23 +50,25 @@
     4.4  
     4.5  (* lookup facts in context *)
     4.6  fun resolve_fact_names ctxt names =
     4.7 -  names
     4.8 +  (names
     4.9      |>> map string_for_label
    4.10      |> op @
    4.11 -    |> maps (thms_of_name ctxt)
    4.12 +    |> maps (thms_of_name ctxt))
    4.13 +  handle ERROR msg => error ("preplay error: " ^ msg)
    4.14  
    4.15  (* *)
    4.16  fun thm_of_term ctxt = Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
    4.17 -fun fact_of_subproof ctxt proof =
    4.18 +fun fact_of_proof ctxt (Proof (Fix fixed_frees, Assume assms, steps)) =
    4.19    let
    4.20 -    val (fixed_frees, assms, concl) = split_proof proof
    4.21 +    val concl = (case try List.last steps of
    4.22 +                  SOME (Prove (_, _, t, _)) => t
    4.23 +                | _ => error "preplay error: malformed subproof")
    4.24      val var_idx = maxidx_of_term concl + 1
    4.25      fun var_of_free (x, T) = Var((x, var_idx), T)
    4.26      val substitutions =
    4.27        map (`var_of_free #> swap #> apfst Free) fixed_frees
    4.28 -    val assms = assms |> map snd
    4.29    in
    4.30 -    Logic.list_implies(assms, concl)
    4.31 +    Logic.list_implies (assms |> map snd, concl)
    4.32        |> subst_free substitutions
    4.33        |> thm_of_term ctxt
    4.34    end
    4.35 @@ -78,7 +80,7 @@
    4.36        (case step of
    4.37          Prove (_, _, t, By_Metis (subproofs, fact_names)) =>
    4.38              (t, subproofs, fact_names, false)
    4.39 -      | Obtain (_, xs, _, t, By_Metis (subproofs, fact_names)) =>
    4.40 +      | Obtain (_, Fix xs, _, t, By_Metis (subproofs, fact_names)) =>
    4.41          (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
    4.42             (see ~~/src/Pure/Isar/obtain.ML) *)
    4.43          let
    4.44 @@ -98,7 +100,7 @@
    4.45          end
    4.46        | _ => raise ZEROTIME)
    4.47      val facts =
    4.48 -      map (fact_of_subproof ctxt) subproofs @
    4.49 +      map (fact_of_proof ctxt) subproofs @
    4.50        resolve_fact_names ctxt fact_names
    4.51      val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug
    4.52                      |> obtain ? Config.put Metis_Tactic.new_skolem true

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Mon Feb 18 12:16:02 2013 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Mon Feb 18 12:16:27 2013 +0100
     5.3 @@ -9,83 +9,84 @@
     5.4  signature SLEDGEHAMMER_PROOF =
     5.5  sig
     5.6  	type label = string * int
     5.7 -  val no_label : label
     5.8    type facts = label list * string list
     5.9 -  val no_facts : facts
    5.10  
    5.11    datatype isar_qualifier = Show | Then
    5.12  
    5.13 -  datatype isar_step =
    5.14 -    Fix of (string * typ) list |
    5.15 +  datatype fix = Fix of (string * typ) list
    5.16 +  datatype assms = Assume of (label * term) list
    5.17 +
    5.18 +  datatype isar_proof = 
    5.19 +    Proof of fix * assms * isar_step list
    5.20 +  and isar_step =
    5.21      Let of term * term |
    5.22 -    Assume of label * term |
    5.23 -    Obtain of
    5.24 -      isar_qualifier list * (string * typ) list * label * term * byline |
    5.25 -    Prove of isar_qualifier list * label * term * byline
    5.26 +    Prove of isar_qualifier list * label * term * byline |
    5.27 +    Obtain of isar_qualifier list * fix * label * term * byline
    5.28    and byline =
    5.29 -    By_Metis of isar_step list list * facts
    5.30 +    By_Metis of isar_proof list * facts
    5.31 +
    5.32 +  val no_label : label
    5.33 +  val no_facts : facts
    5.34  
    5.35    val string_for_label : label -> string
    5.36 -  val metis_steps_top_level : isar_step list -> int
    5.37 -  val metis_steps_total : isar_step list -> int
    5.38 -  val term_of_assm : isar_step -> term
    5.39 -  val term_of_prove : isar_step -> term
    5.40 -  val split_proof :
    5.41 -    isar_step list -> (string * typ) list * (label * term) list * term
    5.42 +  val fix_of_proof : isar_proof -> fix
    5.43 +  val assms_of_proof : isar_proof -> assms
    5.44 +  val steps_of_proof : isar_proof -> isar_step list
    5.45 +
    5.46 +  val label_of_step : isar_step -> label option
    5.47 +  val byline_of_step : isar_step -> byline option
    5.48 +
    5.49 +  val add_metis_steps_top_level : isar_step list -> int -> int
    5.50 +  val add_metis_steps : isar_step list -> int -> int
    5.51  end
    5.52  
    5.53  structure Sledgehammer_Proof : SLEDGEHAMMER_PROOF =
    5.54  struct
    5.55  
    5.56  type label = string * int
    5.57 -val no_label = ("", ~1)
    5.58  type facts = label list * string list
    5.59 -val no_facts = ([],[])
    5.60  
    5.61  datatype isar_qualifier = Show | Then
    5.62  
    5.63 -datatype isar_step =
    5.64 -  Fix of (string * typ) list |
    5.65 +datatype fix = Fix of (string * typ) list
    5.66 +datatype assms = Assume of (label * term) list
    5.67 +
    5.68 +datatype isar_proof = 
    5.69 +  Proof of fix * assms * isar_step list
    5.70 +and isar_step =
    5.71    Let of term * term |
    5.72 -  Assume of label * term |
    5.73 -  Obtain of isar_qualifier list * (string * typ) list * label * term * byline |
    5.74 -  Prove of isar_qualifier list * label * term * byline
    5.75 +  Prove of isar_qualifier list * label * term * byline |
    5.76 +  Obtain of isar_qualifier list * fix * label * term * byline
    5.77  and byline =
    5.78 -  By_Metis of isar_step list list * facts
    5.79 +  By_Metis of isar_proof list * facts
    5.80 +
    5.81 +val no_label = ("", ~1)
    5.82 +val no_facts = ([],[])
    5.83  
    5.84  fun string_for_label (s, num) = s ^ string_of_int num
    5.85  
    5.86 -fun metis_steps_top_level proof =
    5.87 -  fold (fn Obtain _ => Integer.add 1 | Prove _ => Integer.add 1 | _ => I)
    5.88 -       proof 0
    5.89 -fun metis_steps_total proof =
    5.90 -  let
    5.91 -    fun add_substeps subproofs i =
    5.92 -      Integer.add (fold Integer.add (map metis_steps_total subproofs) i)
    5.93 -  in
    5.94 -    fold
    5.95 -    (fn Obtain (_, _, _, _, By_Metis (subproofs, _)) => add_substeps subproofs 1
    5.96 -      | Prove (_, _, _, By_Metis (subproofs, _)) => add_substeps subproofs 1
    5.97 -      | _ => I)
    5.98 -    proof 0
    5.99 -  end
   5.100 +fun fix_of_proof (Proof (fix, _, _)) = fix
   5.101 +fun assms_of_proof (Proof (_, assms, _)) = assms
   5.102 +fun steps_of_proof (Proof (_, _, steps)) = steps
   5.103 +(*fun map_steps_of_proof f (Proof (fix, assms, steps)) =
   5.104 +  Proof(fix, assms, f steps)*)
   5.105  
   5.106 -fun term_of_assm (Assume (_, t)) = t
   5.107 -  | term_of_assm _ = error "sledgehammer proof: unexpected constructor"
   5.108 -fun term_of_prove (Prove (_, _, t, _)) = t
   5.109 -  | term_of_prove _ = error "sledgehammer proof: unexpected constructor"
   5.110 +fun label_of_step (Obtain (_, _, l, _, _)) = SOME l
   5.111 +  | label_of_step (Prove (_, l, _, _)) = SOME l
   5.112 +  | label_of_step _ = NONE
   5.113  
   5.114 -fun split_proof proof =
   5.115 -  let
   5.116 -    fun split_step step (fixes, assms, _) =
   5.117 -      (case step of
   5.118 -        Fix xs   => (xs@fixes, assms,    step)
   5.119 -      | Assume a => (fixes,    a::assms, step)
   5.120 -      | _        => (fixes,    assms,    step))
   5.121 -    val (fixes, assms, concl) =
   5.122 -      fold split_step proof ([], [], Let (Term.dummy, Term.dummy)) (* FIXME: hack *)
   5.123 -  in
   5.124 -    (rev fixes, rev assms, term_of_prove concl)
   5.125 -  end
   5.126 +fun byline_of_step (Obtain (_, _, _, _, byline)) = SOME byline
   5.127 +  | byline_of_step (Prove (_, _, _, byline)) = SOME byline
   5.128 +  | byline_of_step _ = NONE
   5.129 +
   5.130 +val add_metis_steps_top_level =
   5.131 +  fold (byline_of_step #> (fn SOME (By_Metis _) => Integer.add 1 | _ => I))
   5.132 +
   5.133 +fun add_metis_steps steps =
   5.134 +  fold (byline_of_step 
   5.135 +        #> (fn SOME (By_Metis (subproofs, _)) =>
   5.136 +                Integer.add 1 #> add_substeps subproofs
   5.137 +             | _ => I)) steps
   5.138 +and add_substeps subproofs = fold (steps_of_proof #> add_metis_steps) subproofs
   5.139  
   5.140  end

     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Feb 18 12:16:02 2013 +0100
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Feb 18 12:16:27 2013 +0100
     6.3 @@ -457,158 +457,190 @@
     6.4  
     6.5  val indent_size = 2
     6.6  
     6.7 -fun string_for_proof ctxt type_enc lam_trans i n =
     6.8 +fun string_for_proof ctxt type_enc lam_trans i n proof =
     6.9    let
    6.10 -    fun maybe_show qs = if member (op =) qs Show then "show" else "have"
    6.11 +    val register_fixes = map Free #> fold Variable.auto_fixes
    6.12 +    fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt)
    6.13      fun of_indent ind = replicate_string (ind * indent_size) " "
    6.14 -    fun of_free (s, T) =
    6.15 -      maybe_quote s ^ " :: " ^
    6.16 -      maybe_quote (simplify_spaces (with_vanilla_print_mode
    6.17 -        (Syntax.string_of_typ ctxt) T))
    6.18 -    val of_frees = space_implode " and " o map of_free
    6.19 -    fun maybe_moreover ind qs nr_subproofs =
    6.20 -        if member (op =) qs Then andalso nr_subproofs > 0
    6.21 -          then of_indent ind ^ "moreover\n"
    6.22 -          else ""
    6.23 +    fun of_moreover ind = of_indent ind ^ "moreover\n"
    6.24      fun of_label l = if l = no_label then "" else string_for_label l ^ ": "
    6.25 -    fun of_have qs nr_subproofs =
    6.26 -      if (member (op =) qs Then andalso nr_subproofs>0) orelse (nr_subproofs>1)
    6.27 -        then "ultimately " ^ maybe_show qs
    6.28 -        else
    6.29 -          (if member (op =) qs Then orelse nr_subproofs>0 then
    6.30 -             if member (op =) qs Show then "thus" else "hence"
    6.31 -           else
    6.32 -             maybe_show qs)
    6.33 -    fun of_obtain qs xs =
    6.34 -      (if member (op =) qs Then then "then " else "") ^ "obtain " ^
    6.35 -      of_frees xs ^ " where"
    6.36 -    val of_term =
    6.37 -      annotate_types ctxt
    6.38 -      #> with_vanilla_print_mode (Syntax.string_of_term ctxt)
    6.39 -      #> simplify_spaces
    6.40 -      #> maybe_quote
    6.41 +    fun of_obtain qs nr =
    6.42 +      (if nr>1 orelse (nr=1 andalso member (op=) qs Then)
    6.43 +        then "ultimately "
    6.44 +      else if nr=1 orelse member (op=) qs Then
    6.45 +        then "then "
    6.46 +        else "") ^ "obtain"
    6.47 +    fun of_show_have qs = if member (op=) qs Show then "show" else "have"
    6.48 +    fun of_thus_hence qs = if member (op=) qs Show then "thus" else "hence"
    6.49 +    fun of_prove qs nr =
    6.50 +      if nr>1 orelse (nr=1 andalso member (op=) qs Then)
    6.51 +        then "ultimately " ^ of_show_have qs
    6.52 +      else if nr=1 orelse member (op=) qs Then
    6.53 +        then of_thus_hence qs
    6.54 +        else of_show_have qs
    6.55 +    fun add_term term (s, ctxt)=
    6.56 +      (s ^ (annotate_types ctxt term
    6.57 +            |> with_vanilla_print_mode (Syntax.string_of_term ctxt)
    6.58 +            |> simplify_spaces
    6.59 +            |> maybe_quote),
    6.60 +       ctxt |> Variable.auto_fixes term)
    6.61      val reconstr = Metis (type_enc, lam_trans)
    6.62      fun of_metis ind options (ls, ss) =
    6.63        "\n" ^ of_indent (ind + 1) ^ options ^
    6.64        reconstructor_command reconstr 1 1 [] 0
    6.65            (ls |> sort_distinct (prod_ord string_ord int_ord),
    6.66             ss |> sort_distinct string_ord)
    6.67 -    and of_step ind (Fix xs) = of_indent ind ^ "fix " ^ of_frees xs ^ "\n"
    6.68 -      | of_step ind (Let (t1, t2)) =
    6.69 -        of_indent ind ^ "let " ^ of_term t1 ^ " = " ^ of_term t2 ^ "\n"
    6.70 -      | of_step ind (Assume (l, t)) =
    6.71 -        of_indent ind ^ "assume " ^ of_label l ^ of_term t ^ "\n"
    6.72 -      | of_step ind (Obtain (qs, xs, l, t, By_Metis (subproofs, facts))) =      (* FIXME *)
    6.73 -        maybe_moreover ind qs (length subproofs) ^
    6.74 -        of_subproofs ind subproofs ^
    6.75 -        of_indent ind ^ of_obtain qs xs ^ " " ^
    6.76 -        of_label l ^ of_term t ^
    6.77 -        (* The new skolemizer puts the arguments in the same order as the ATPs
    6.78 -           (E and Vampire -- but see also "atp_proof_reconstruct.ML" regarding
    6.79 -           Vampire). *)
    6.80 -        of_metis ind "using [[metis_new_skolem]] " facts ^ "\n"
    6.81 -      | of_step ind (Prove (qs, l, t, By_Metis (subproofs, facts))) =
    6.82 -        maybe_moreover ind qs (length subproofs) ^
    6.83 -        of_subproofs ind subproofs ^
    6.84 -        of_prove ind qs (length subproofs) l t facts
    6.85 -    and of_steps prefix suffix ind steps =
    6.86 -      let val s = implode (map (of_step ind) steps) in
    6.87 +    fun of_free (s, T) =
    6.88 +      maybe_quote s ^ " :: " ^
    6.89 +      maybe_quote (simplify_spaces (with_vanilla_print_mode
    6.90 +        (Syntax.string_of_typ ctxt) T))
    6.91 +    fun add_frees xs (s, ctxt) =
    6.92 +      (s ^ space_implode " and " (map of_free xs), ctxt |> register_fixes xs)
    6.93 +    fun add_fix _ [] = I
    6.94 +      | add_fix ind xs = add_suffix (of_indent ind ^ "fix ")
    6.95 +                        #> add_frees xs
    6.96 +                        #> add_suffix "\n"
    6.97 +    fun add_assm ind (l, t) =
    6.98 +      add_suffix (of_indent ind ^ "assume " ^ of_label l)
    6.99 +      #> add_term t
   6.100 +      #> add_suffix "\n"
   6.101 +    fun add_assms ind assms = fold (add_assm ind) assms
   6.102 +    fun add_step_post ind l t facts options =
   6.103 +      add_suffix (of_label l)
   6.104 +      #> add_term t
   6.105 +      #> add_suffix (of_metis ind options facts ^ "\n")
   6.106 +    fun of_subproof ind ctxt proof =
   6.107 +      let
   6.108 +        val ind = ind + 1
   6.109 +        val s = of_proof ind ctxt proof
   6.110 +        val prefix = "{ "
   6.111 +        val suffix = " }"
   6.112 +      in
   6.113          replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
   6.114          String.extract (s, ind * indent_size,
   6.115                          SOME (size s - ind * indent_size - 1)) ^
   6.116          suffix ^ "\n"
   6.117        end
   6.118 -    and of_block ind proof = of_steps "{ " " }" (ind + 1) proof
   6.119 -    and of_subproofs ind subproofs =
   6.120 -        subproofs
   6.121 -          |> map (of_block ind)
   6.122 -          |> space_implode (of_indent ind ^ "moreover\n")
   6.123 -    and of_prove ind qs nr_subproofs l t facts =
   6.124 -      of_indent ind ^ of_have qs nr_subproofs ^ " " ^ of_label l ^ of_term t ^
   6.125 -      of_metis ind "" facts ^ "\n"
   6.126 +    and of_subproofs _ _ _ [] = ""
   6.127 +      | of_subproofs ind ctxt qs subproofs =
   6.128 +        (if member (op=) qs Then then of_moreover ind else "") ^
   6.129 +        space_implode (of_moreover ind) (map (of_subproof ind ctxt) subproofs)
   6.130 +    and add_step_pre ind qs subproofs (s, ctxt) =
   6.131 +      (s ^ of_subproofs ind ctxt qs subproofs ^ of_indent ind, ctxt)
   6.132 +    and add_step ind (Let (t1, t2)) =
   6.133 +        add_suffix (of_indent ind ^ "let ")
   6.134 +        #> add_term t1
   6.135 +        #> add_suffix " = "
   6.136 +        #> add_term t2
   6.137 +        #> add_suffix "\n"
   6.138 +      | add_step ind (Prove (qs, l, t, By_Metis (subproofs, facts))) =
   6.139 +        add_step_pre ind qs subproofs
   6.140 +        #> add_suffix (of_prove qs (length subproofs) ^ " ")
   6.141 +        #> add_step_post ind l t facts ""
   6.142 +      | add_step ind (Obtain (qs, Fix xs, l, t,
   6.143 +                      By_Metis (subproofs, facts))) =
   6.144 +        add_step_pre ind qs subproofs
   6.145 +        #> add_suffix (of_obtain qs (length subproofs) ^ " ")
   6.146 +        #> add_frees xs
   6.147 +        #> add_suffix " where "
   6.148 +        (* The new skolemizer puts the arguments in the same order as the ATPs
   6.149 +         (E and Vampire -- but see also "atp_proof_reconstruct.ML" regarding
   6.150 +         Vampire). *)
   6.151 +        #> add_step_post ind l t facts "using [[metis_new_skolem]] "
   6.152 +    and add_steps ind steps =
   6.153 +      fold (add_step ind) steps
   6.154 +    and of_proof ind ctxt (Proof (Fix xs, Assume assms, steps)) =
   6.155 +      ("", ctxt)
   6.156 +      |> add_fix ind xs
   6.157 +      |> add_assms ind assms
   6.158 +      |> add_steps ind steps
   6.159 +      |> fst
   6.160 +  in
   6.161      (* One-step proofs are pointless; better use the Metis one-liner
   6.162         directly. *)
   6.163 -    and of_proof [Prove (_, _, _, By_Metis ([], _))] = ""
   6.164 -      | of_proof proof =
   6.165 -        (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
   6.166 -        of_indent 0 ^ "proof -\n" ^ of_steps "" "" 1 proof ^ of_indent 0 ^
   6.167 -        (if n <> 1 then "next" else "qed")
   6.168 -  in of_proof end
   6.169 +    case proof of
   6.170 +      Proof (Fix [], Assume [], [Prove (_, _, _, By_Metis ([], _))]) => ""
   6.171 +    | _ => (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
   6.172 +            of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
   6.173 +            of_indent 0 ^ (if n <> 1 then "next" else "qed")
   6.174 +  end
   6.175  
   6.176 -fun add_labels_of_step (Obtain (_, _, _, _, By_Metis (subproofs, (ls, _)))) =
   6.177 -      union (op =) (add_labels_of_proofs subproofs ls)
   6.178 -  | add_labels_of_step (Prove (_, _, _, By_Metis (subproofs, (ls, _)))) =
   6.179 -      union (op =) (add_labels_of_proofs subproofs ls)
   6.180 -  | add_labels_of_step _ = I
   6.181 -and add_labels_of_proof proof = fold add_labels_of_step proof
   6.182 +fun add_labels_of_step step =
   6.183 +  (case byline_of_step step of
   6.184 +     NONE => I
   6.185 +  |  SOME (By_Metis (subproofs, (ls, _))) =>
   6.186 +      union (op =) (add_labels_of_proofs subproofs ls))
   6.187 +and add_labels_of_proof proof = fold add_labels_of_step (steps_of_proof proof)
   6.188  and add_labels_of_proofs proofs = fold add_labels_of_proof proofs
   6.189  
   6.190  fun kill_useless_labels_in_proof proof =
   6.191    let
   6.192      val used_ls = add_labels_of_proof proof []
   6.193      fun do_label l = if member (op =) used_ls l then l else no_label
   6.194 -    fun do_step (Assume (l, t)) = Assume (do_label l, t)
   6.195 -      | do_step (Obtain (qs, xs, l, t, By_Metis (subproofs, facts))) =
   6.196 +    fun do_assms (Assume assms) = Assume (map (apfst do_label) assms)
   6.197 +    fun do_step (Obtain (qs, xs, l, t, By_Metis (subproofs, facts))) =
   6.198            Obtain (qs, xs, do_label l, t, By_Metis (map do_proof subproofs, facts))
   6.199        | do_step (Prove (qs, l, t, By_Metis (subproofs, facts))) =
   6.200            Prove (qs, do_label l, t, By_Metis (map do_proof subproofs, facts))
   6.201        | do_step step = step
   6.202 -    and do_proof proof = map do_step proof
   6.203 +    and do_proof (Proof (fix, assms, steps)) =
   6.204 +          Proof (fix, do_assms assms, map do_step steps)
   6.205    in do_proof proof end
   6.206  
   6.207  fun prefix_for_depth n = replicate_string (n + 1)
   6.208  
   6.209  val relabel_proof =
   6.210    let
   6.211 -    fun fresh_label depth (old as (l, subst, next_have)) =
   6.212 +    fun fresh_label depth prefix (old as (l, subst, next)) =
   6.213        if l = no_label then
   6.214          old
   6.215        else
   6.216 -        let val l' = (prefix_for_depth depth have_prefix, next_have) in
   6.217 -          (l', (l, l') :: subst, next_have + 1)
   6.218 +        let val l' = (prefix_for_depth depth prefix, next) in
   6.219 +          (l', (l, l') :: subst, next + 1)
   6.220          end
   6.221      fun do_facts subst =
   6.222        apfst (maps (the_list o AList.lookup (op =) subst))
   6.223 -    fun do_byline subst depth nexts (By_Metis (subproofs, facts)) =
   6.224 -      By_Metis
   6.225 -        (map (do_proof subst (depth + 1) (1, 1)) subproofs, do_facts subst facts)
   6.226 -    and do_proof _ _ _ [] = []
   6.227 -      | do_proof subst depth (next_assum, next_have) (Assume (l, t) :: proof) =
   6.228 -        if l = no_label then
   6.229 -          Assume (l, t) :: do_proof subst depth (next_assum, next_have) proof
   6.230 -        else
   6.231 -          let val l' = (prefix_for_depth depth assume_prefix, next_assum) in
   6.232 -            Assume (l', t) ::
   6.233 -            do_proof ((l, l') :: subst) depth (next_assum + 1, next_have) proof
   6.234 -          end
   6.235 -      | do_proof subst depth (nexts as (next_assum, next_have))
   6.236 -            (Obtain (qs, xs, l, t, by) :: proof) =
   6.237 +    fun do_assm depth (l, t) (subst, next) =
   6.238 +      let
   6.239 +        val (l, subst, next) =
   6.240 +          (l, subst, next) |> fresh_label depth assume_prefix
   6.241 +      in
   6.242 +        ((l, t), (subst, next))
   6.243 +      end
   6.244 +    fun do_assms subst depth (Assume assms) =
   6.245 +      fold_map (do_assm depth) assms (subst, 1)
   6.246 +      |> apfst Assume
   6.247 +      |> apsnd fst
   6.248 +    fun do_steps _ _ _ [] = []
   6.249 +      | do_steps subst depth next (Obtain (qs, xs, l, t, by) :: steps) =
   6.250          let
   6.251 -          val (l, subst, next_have) = (l, subst, next_have) |> fresh_label depth
   6.252 -          val by = by |> do_byline subst depth nexts
   6.253 +          val (l, subst, next) =
   6.254 +            (l, subst, next) |> fresh_label depth have_prefix
   6.255 +          val by = by |> do_byline subst depth
   6.256          in
   6.257 -          Obtain (qs, xs, l, t, by) ::
   6.258 -          do_proof subst depth (next_assum, next_have) proof
   6.259 +          Obtain (qs, xs, l, t, by) :: do_steps subst depth next steps
   6.260          end
   6.261 -      | do_proof subst depth (nexts as (next_assum, next_have))
   6.262 -            (Prove (qs, l, t, by) :: proof) =
   6.263 +      | do_steps subst depth next (Prove (qs, l, t, by) :: steps) =
   6.264          let
   6.265 -          val (l, subst, next_have) = (l, subst, next_have) |> fresh_label depth
   6.266 -          val by = by |> do_byline subst depth nexts
   6.267 +          val (l, subst, next) =
   6.268 +            (l, subst, next) |> fresh_label depth have_prefix
   6.269 +          val by = by |> do_byline subst depth
   6.270          in
   6.271 -          Prove (qs, l, t, by) ::
   6.272 -          do_proof subst depth (next_assum, next_have) proof
   6.273 +          Prove (qs, l, t, by) :: do_steps subst depth next steps
   6.274          end
   6.275 -      | do_proof subst depth nexts (step :: proof) =
   6.276 -        step :: do_proof subst depth nexts proof
   6.277 -  in do_proof [] 0 (1, 1) end
   6.278 +      | do_steps subst depth next (step :: steps) =
   6.279 +        step :: do_steps subst depth next steps
   6.280 +    and do_proof subst depth (Proof (fix, assms, steps)) =
   6.281 +      let val (assms, subst) = do_assms subst depth assms in
   6.282 +        Proof (fix, assms, do_steps subst depth 1 steps)
   6.283 +      end
   6.284 +    and do_byline subst depth (By_Metis (subproofs, facts)) =
   6.285 +      By_Metis (do_proofs subst depth subproofs, do_facts subst facts)
   6.286 +    and do_proofs subst depth = map (do_proof subst (depth + 1))
   6.287 +  in do_proof [] 0 end
   6.288  
   6.289  val chain_direct_proof =
   6.290    let
   6.291 -    fun label_of (Assume (l, _)) = SOME l
   6.292 -      | label_of (Obtain (_, _, l, _, _)) = SOME l
   6.293 -      | label_of (Prove (_, l, _, _)) = SOME l
   6.294 -      | label_of _ = NONE
   6.295      fun do_qs_lfs NONE lfs = ([], lfs)
   6.296        | do_qs_lfs (SOME l0) lfs =
   6.297          if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0)
   6.298 @@ -621,16 +653,18 @@
   6.299          end
   6.300        | chain_step lbl (Prove (qs, l, t, By_Metis (subproofs, (lfs, gfs)))) =
   6.301          let val (qs', lfs) = do_qs_lfs lbl lfs in
   6.302 -          Prove (qs' @ qs, l, t,
   6.303 -            By_Metis (chain_proofs subproofs, (lfs, gfs)))
   6.304 +          Prove (qs' @ qs, l, t, By_Metis (chain_proofs subproofs, (lfs, gfs)))
   6.305          end
   6.306        | chain_step _ step = step
   6.307 -    and chain_proof _ [] = []
   6.308 -      | chain_proof (prev as SOME _) (i :: is) =
   6.309 -        chain_step prev i :: chain_proof (label_of i) is
   6.310 -      | chain_proof _ (i :: is) = i :: chain_proof (label_of i) is
   6.311 -    and chain_proofs proofs = map (chain_proof NONE) proofs
   6.312 -  in chain_proof NONE end
   6.313 +    and chain_steps _ [] = []
   6.314 +      | chain_steps (prev as SOME _) (i :: is) =
   6.315 +        chain_step prev i :: chain_steps (label_of_step i) is
   6.316 +      | chain_steps _ (i :: is) = i :: chain_steps (label_of_step i) is
   6.317 +    and chain_proof (Proof (fix, Assume assms, steps)) =
   6.318 +      Proof (fix, Assume assms,
   6.319 +             chain_steps (try (List.last #> fst) assms) steps)
   6.320 +    and chain_proofs proofs = map (chain_proof) proofs
   6.321 +  in chain_proof end
   6.322  
   6.323  type isar_params =
   6.324    bool * bool * Time.time option * real * string Symtab.table
   6.325 @@ -676,7 +710,7 @@
   6.326                  (case resolve_conjecture ss of
   6.327                     [j] =>
   6.328                     if j = length hyp_ts then NONE
   6.329 -                   else SOME (Assume (raw_label_for_name name, nth hyp_ts j))
   6.330 +                   else SOME (raw_label_for_name name, nth hyp_ts j)
   6.331                   | _ => NONE)
   6.332                | _ => NONE)
   6.333          fun dep_of_step (Definition_Step _) = NONE
   6.334 @@ -691,7 +725,7 @@
   6.335          val steps =
   6.336            Symtab.empty
   6.337            |> fold (fn Definition_Step _ => I (* FIXME *)
   6.338 -                    | Inference_Step (name as (s, ss), role, t, rule, _) =>
   6.339 +                    | Inference_Step (name as (s, _), role, t, rule, _) =>
   6.340                        Symtab.update_new (s, (rule,
   6.341                          t |> (if is_clause_tainted [name] then
   6.342                                  s_maybe_not role
   6.343 @@ -705,7 +739,7 @@
   6.344            | is_clause_skolemize_rule _ = false
   6.345          (* The assumptions and conjecture are "prop"s; the other formulas are
   6.346             "bool"s. *)
   6.347 -        fun prop_of_clause [name as (s, ss)] =
   6.348 +        fun prop_of_clause [(s, ss)] =
   6.349              (case resolve_conjecture ss of
   6.350                 [j] => if j = length hyp_ts then concl_t else nth hyp_ts j
   6.351               | _ => the_default ("", @{term False}) (Symtab.lookup steps s)
   6.352 @@ -722,22 +756,16 @@
   6.353                | _ => fold (curry s_disj) lits @{term False}
   6.354              end
   6.355              |> HOLogic.mk_Trueprop |> close_form
   6.356 -        fun isar_proof_of_direct_proof outer predecessor accum [] =
   6.357 -            rev accum |> outer ? (append assms
   6.358 -                                  #> not (null params) ? cons (Fix params))
   6.359 -          | isar_proof_of_direct_proof outer predecessor accum (inf :: infs) =
   6.360 -            let
   6.361 -              fun maybe_show outer c =
   6.362 -                (outer andalso length c = 1 andalso subset (op =) (c, conjs))
   6.363 -                ? cons Show
   6.364 -              fun do_rest lbl step =
   6.365 -                isar_proof_of_direct_proof outer lbl (step :: accum) infs
   6.366 -              val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
   6.367 -              fun skolems_of t =
   6.368 -                Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
   6.369 -            in
   6.370 -              case inf of
   6.371 -                Have (gamma, c) =>
   6.372 +        fun isar_proof_of_direct_proof infs =
   6.373 +          let
   6.374 +            fun maybe_show outer c =
   6.375 +              (outer andalso length c = 1 andalso subset (op =) (c, conjs))
   6.376 +              ? cons Show
   6.377 +            val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
   6.378 +            fun skolems_of t =
   6.379 +              Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
   6.380 +            fun do_steps _ _ accum [] = rev accum
   6.381 +              | do_steps outer _ accum (Have (gamma, c) :: infs) =
   6.382                  let
   6.383                    val l = label_of_clause c
   6.384                    val t = prop_of_clause c
   6.385 @@ -745,7 +773,9 @@
   6.386                      By_Metis ([],
   6.387                        (fold (add_fact_from_dependencies fact_names)
   6.388                              gamma no_facts))
   6.389 -                  fun prove outer = Prove (maybe_show outer c [], l, t, by)
   6.390 +                  fun prove by = Prove (maybe_show outer c [], l, t, by)
   6.391 +                  fun do_rest lbl step =
   6.392 +                    do_steps outer (SOME lbl) (step :: accum) infs
   6.393                  in
   6.394                    if is_clause_tainted c then
   6.395                      case gamma of
   6.396 @@ -754,36 +784,40 @@
   6.397                           is_clause_tainted g then
   6.398                          let
   6.399                            val subproof =
   6.400 -                            Fix (skolems_of (prop_of_clause g)) :: rev accum
   6.401 +                            Proof (Fix (skolems_of (prop_of_clause g)),
   6.402 +                                   Assume [], rev accum)
   6.403                          in
   6.404 -                          isar_proof_of_direct_proof outer l
   6.405 -                              [Prove (maybe_show outer c [],
   6.406 -                                      label_of_clause c, prop_of_clause c,
   6.407 -                                      By_Metis ([subproof], no_facts))] []
   6.408 +                          do_steps outer (SOME l)
   6.409 +                              [prove (By_Metis ([subproof], no_facts))] []
   6.410                          end
   6.411                        else
   6.412 -                        do_rest l (prove outer)
   6.413 -                    | _ => do_rest l (prove outer)
   6.414 +                        do_rest l (prove by)
   6.415 +                    | _ => do_rest l (prove by)
   6.416                    else
   6.417                      if is_clause_skolemize_rule c then
   6.418 -                      do_rest l (Obtain ([], skolems_of t, l, t, by))
   6.419 +                      do_rest l (Obtain ([], Fix (skolems_of t), l, t, by))
   6.420                      else
   6.421 -                      do_rest l (prove outer)
   6.422 +                      do_rest l (prove by)
   6.423                  end
   6.424 -              | Cases cases =>
   6.425 +              | do_steps outer predecessor accum (Cases cases :: infs) =
   6.426                  let
   6.427                    fun do_case (c, infs) =
   6.428 -                    Assume (label_of_clause c, prop_of_clause c) ::
   6.429 -                    isar_proof_of_direct_proof false no_label [] infs
   6.430 +                    do_proof false [] [(label_of_clause c, prop_of_clause c)] infs
   6.431                    val c = succedent_of_cases cases
   6.432                    val l = label_of_clause c
   6.433 +                  val t = prop_of_clause c
   6.434 +                  val step =
   6.435 +                    (Prove (maybe_show outer c [], l, t, By_Metis
   6.436 +                      (map do_case cases, (the_list predecessor, []))))
   6.437                  in
   6.438 -                  do_rest l
   6.439 -                    (Prove (maybe_show outer c [],
   6.440 -                            l, prop_of_clause c,
   6.441 -                            By_Metis (map do_case cases, ([predecessor], []))))
   6.442 +                  do_steps outer (SOME l) (step :: accum) infs
   6.443                  end
   6.444 -            end
   6.445 +            and do_proof outer fix assms infs =
   6.446 +              Proof (Fix fix, Assume assms, do_steps outer NONE [] infs)
   6.447 +          in
   6.448 +            do_proof true params assms infs
   6.449 +          end
   6.450 +
   6.451          val cleanup_labels_in_proof =
   6.452            chain_direct_proof
   6.453            #> kill_useless_labels_in_proof
   6.454 @@ -791,7 +825,7 @@
   6.455          val (isar_proof, (preplay_fail, preplay_time)) =
   6.456            refute_graph
   6.457            |> redirect_graph axioms tainted bot
   6.458 -          |> isar_proof_of_direct_proof true no_label []
   6.459 +          |> isar_proof_of_direct_proof
   6.460            |> (if not preplay andalso isar_compress <= 1.0 then
   6.461                  rpair (false, (true, seconds 0.0))
   6.462                else
   6.463 @@ -818,9 +852,11 @@
   6.464                 else
   6.465                   []) @
   6.466                (if verbose then
   6.467 -                 let val num_steps = metis_steps_total isar_proof in
   6.468 -                   [string_of_int num_steps ^ " step" ^ plural_s num_steps]
   6.469 -                 end
   6.470 +                let
   6.471 +                  val num_steps = add_metis_steps (steps_of_proof isar_proof) 0
   6.472 +                in
   6.473 +                  [string_of_int num_steps ^ " step" ^ plural_s num_steps]
   6.474 +                end
   6.475                 else
   6.476                   [])
   6.477            in