renamed sledgehammer_shrink to sledgehammer_compress
authorsmolkas
Thu Feb 14 22:49:22 2013 +0100 (2013-02-14)
changeset 5113076d68444cd59
parent 51129 1edc2cc25f19
child 51131 7de262be1e95
renamed sledgehammer_shrink to sledgehammer_compress
src/Doc/Sledgehammer/document/root.tex
src/HOL/Metis_Examples/Big_O.thy
src/HOL/Metis_Examples/Sets.thy
src/HOL/Metis_Examples/Trans_Closure.thy
src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML
     1.1 --- a/src/Doc/Sledgehammer/document/root.tex	Thu Feb 14 22:49:22 2013 +0100
     1.2 +++ b/src/Doc/Sledgehammer/document/root.tex	Thu Feb 14 22:49:22 2013 +0100
     1.3 @@ -369,7 +369,7 @@
     1.4  \item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies
     1.5  that Isar proofs should be generated, instead of one-liner \textit{metis} or
     1.6  \textit{smt} proofs. The length of the Isar proofs can be controlled by setting
     1.7 -\textit{isar\_shrink} (\S\ref{output-format}).
     1.8 +\textit{isar\_compress} (\S\ref{output-format}).
     1.9  
    1.10  \item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the
    1.11  provers' time limit. It is set to 30 seconds, but since Sledgehammer runs
    1.12 @@ -508,7 +508,7 @@
    1.13  is highly experimental. Work on a new implementation has begun. There is a large body of
    1.14  research into transforming resolution proofs into natural deduction proofs (such
    1.15  as Isar proofs), which we hope to leverage. In the meantime, a workaround is to
    1.16 -set the \textit{isar\_shrink} option (\S\ref{output-format}) to a larger
    1.17 +set the \textit{isar\_compress} option (\S\ref{output-format}) to a larger
    1.18  value or to try several provers and keep the nicest-looking proof.
    1.19  
    1.20  \point{How can I tell whether a suggested proof is sound?}
    1.21 @@ -1302,7 +1302,7 @@
    1.22  fails; however, they are usually faster and sometimes more robust than
    1.23  \textit{metis} proofs.
    1.24  
    1.25 -\opdefault{isar\_shrink}{int}{\upshape 10}
    1.26 +\opdefault{isar\_compress}{int}{\upshape 10}
    1.27  Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs}
    1.28  is enabled. A value of $n$ indicates that each Isar proof step should correspond
    1.29  to a group of up to $n$ consecutive proof steps in the ATP proof.
     2.1 --- a/src/HOL/Metis_Examples/Big_O.thy	Thu Feb 14 22:49:22 2013 +0100
     2.2 +++ b/src/HOL/Metis_Examples/Big_O.thy	Thu Feb 14 22:49:22 2013 +0100
     2.3 @@ -29,7 +29,7 @@
     2.4  
     2.5  (*** Now various verions with an increasing shrink factor ***)
     2.6  
     2.7 -sledgehammer_params [isar_proofs, isar_shrink = 1]
     2.8 +sledgehammer_params [isar_proofs, isar_compress = 1]
     2.9  
    2.10  lemma
    2.11    "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
    2.12 @@ -60,7 +60,7 @@
    2.13    thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F4)
    2.14  qed
    2.15  
    2.16 -sledgehammer_params [isar_proofs, isar_shrink = 2]
    2.17 +sledgehammer_params [isar_proofs, isar_compress = 2]
    2.18  
    2.19  lemma
    2.20    "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
    2.21 @@ -83,7 +83,7 @@
    2.22    thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F2)
    2.23  qed
    2.24  
    2.25 -sledgehammer_params [isar_proofs, isar_shrink = 3]
    2.26 +sledgehammer_params [isar_proofs, isar_compress = 3]
    2.27  
    2.28  lemma
    2.29    "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
    2.30 @@ -103,7 +103,7 @@
    2.31    thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_ge_zero)
    2.32  qed
    2.33  
    2.34 -sledgehammer_params [isar_proofs, isar_shrink = 4]
    2.35 +sledgehammer_params [isar_proofs, isar_compress = 4]
    2.36  
    2.37  lemma
    2.38    "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
    2.39 @@ -123,7 +123,7 @@
    2.40    thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis abs_mult)
    2.41  qed
    2.42  
    2.43 -sledgehammer_params [isar_proofs, isar_shrink = 1]
    2.44 +sledgehammer_params [isar_proofs, isar_compress = 1]
    2.45  
    2.46  lemma bigo_alt_def: "O(f) = {h. \<exists>c. (0 < c \<and> (\<forall>x. abs (h x) <= c * abs (f x)))}"
    2.47  by (auto simp add: bigo_def bigo_pos_const)
     3.1 --- a/src/HOL/Metis_Examples/Sets.thy	Thu Feb 14 22:49:22 2013 +0100
     3.2 +++ b/src/HOL/Metis_Examples/Sets.thy	Thu Feb 14 22:49:22 2013 +0100
     3.3 @@ -21,7 +21,7 @@
     3.4  lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
     3.5  by metis
     3.6  
     3.7 -sledgehammer_params [isar_proofs, isar_shrink = 1]
     3.8 +sledgehammer_params [isar_proofs, isar_compress = 1]
     3.9  
    3.10  (*multiple versions of this example*)
    3.11  lemma (*equal_union: *)
    3.12 @@ -70,7 +70,7 @@
    3.13    ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis
    3.14  qed
    3.15  
    3.16 -sledgehammer_params [isar_proofs, isar_shrink = 2]
    3.17 +sledgehammer_params [isar_proofs, isar_compress = 2]
    3.18  
    3.19  lemma (*equal_union: *)
    3.20     "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
    3.21 @@ -107,7 +107,7 @@
    3.22    ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis
    3.23  qed
    3.24  
    3.25 -sledgehammer_params [isar_proofs, isar_shrink = 3]
    3.26 +sledgehammer_params [isar_proofs, isar_compress = 3]
    3.27  
    3.28  lemma (*equal_union: *)
    3.29     "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
    3.30 @@ -124,7 +124,7 @@
    3.31    ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2)
    3.32  qed
    3.33  
    3.34 -sledgehammer_params [isar_proofs, isar_shrink = 4]
    3.35 +sledgehammer_params [isar_proofs, isar_compress = 4]
    3.36  
    3.37  lemma (*equal_union: *)
    3.38     "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
    3.39 @@ -140,7 +140,7 @@
    3.40    ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a set. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_subset_iff Un_upper2)
    3.41  qed
    3.42  
    3.43 -sledgehammer_params [isar_proofs, isar_shrink = 1]
    3.44 +sledgehammer_params [isar_proofs, isar_compress = 1]
    3.45  
    3.46  lemma (*equal_union: *)
    3.47     "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
     4.1 --- a/src/HOL/Metis_Examples/Trans_Closure.thy	Thu Feb 14 22:49:22 2013 +0100
     4.2 +++ b/src/HOL/Metis_Examples/Trans_Closure.thy	Thu Feb 14 22:49:22 2013 +0100
     4.3 @@ -44,7 +44,7 @@
     4.4  
     4.5  lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b,c) \<in> R\<^sup>*\<rbrakk>
     4.6         \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
     4.7 -(* sledgehammer [isar_proofs, isar_shrink = 2] *)
     4.8 +(* sledgehammer [isar_proofs, isar_compress = 2] *)
     4.9  proof -
    4.10    assume A1: "f c = Intg x"
    4.11    assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
     5.1 --- a/src/HOL/Sledgehammer.thy	Thu Feb 14 22:49:22 2013 +0100
     5.2 +++ b/src/HOL/Sledgehammer.thy	Thu Feb 14 22:49:22 2013 +0100
     5.3 @@ -17,7 +17,7 @@
     5.4  ML_file "Tools/Sledgehammer/sledgehammer_proof.ML"
     5.5  ML_file "Tools/Sledgehammer/sledgehammer_annotate.ML"
     5.6  ML_file "Tools/Sledgehammer/sledgehammer_preplay.ML"
     5.7 -ML_file "Tools/Sledgehammer/sledgehammer_shrink.ML"
     5.8 +ML_file "Tools/Sledgehammer/sledgehammer_compress.ML"
     5.9  ML_file "Tools/Sledgehammer/sledgehammer_reconstruct.ML" 
    5.10  ML_file "Tools/Sledgehammer/sledgehammer_provers.ML"
    5.11  ML_file "Tools/Sledgehammer/sledgehammer_minimize.ML"
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Thu Feb 14 22:49:22 2013 +0100
     6.3 @@ -0,0 +1,252 @@
     6.4 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_compress.ML
     6.5 +    Author:     Jasmin Blanchette, TU Muenchen
     6.6 +    Author:     Steffen Juilf Smolka, TU Muenchen
     6.7 +
     6.8 +Compression of reconstructed isar proofs.
     6.9 +*)
    6.10 +
    6.11 +signature SLEDGEHAMMER_COMPRESS =
    6.12 +sig
    6.13 +  type isar_step = Sledgehammer_Proof.isar_step
    6.14 +  type preplay_time = Sledgehammer_Preplay.preplay_time
    6.15 +  val compress_proof :
    6.16 +    bool -> Proof.context -> string -> string -> bool -> Time.time option
    6.17 +    -> real -> isar_step list -> isar_step list * (bool * preplay_time)
    6.18 +end
    6.19 +
    6.20 +structure Sledgehammer_Compress : SLEDGEHAMMER_COMPRESS =
    6.21 +struct
    6.22 +
    6.23 +open Sledgehammer_Util
    6.24 +open Sledgehammer_Proof
    6.25 +open Sledgehammer_Preplay
    6.26 +
    6.27 +(* Parameters *)
    6.28 +val merge_timeout_slack = 1.2
    6.29 +
    6.30 +(* Data structures, orders *)
    6.31 +val label_ord = prod_ord int_ord fast_string_ord o pairself swap
    6.32 +structure Label_Table = Table(
    6.33 +  type key = label
    6.34 +  val ord = label_ord)
    6.35 +
    6.36 +(* clean vector interface *)
    6.37 +fun get i v = Vector.sub (v, i)
    6.38 +fun replace x i v = Vector.update (v, i, x)
    6.39 +fun update f i v = replace (get i v |> f) i v
    6.40 +fun v_map_index f v = Vector.foldr (op::) nil v |> map_index f |> Vector.fromList
    6.41 +fun v_fold_index f v s =
    6.42 +  Vector.foldl (fn (x, (i, s)) => (i+1, f (i, x) s)) (0, s) v |> snd
    6.43 +
    6.44 +(* Queue interface to table *)
    6.45 +fun pop tab key =
    6.46 +  let val v = hd (Inttab.lookup_list tab key) in
    6.47 +    (v, Inttab.remove_list (op =) (key, v) tab)
    6.48 +  end
    6.49 +fun pop_max tab = pop tab (the (Inttab.max_key tab))
    6.50 +fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab
    6.51 +
    6.52 +(* Main function for compresing proofs *)
    6.53 +fun compress_proof debug ctxt type_enc lam_trans preplay preplay_timeout
    6.54 +                   isar_compress proof =
    6.55 +  let
    6.56 +    (* 60 seconds seems like a good interpreation of "no timeout" *)
    6.57 +    val preplay_timeout = preplay_timeout |> the_default (seconds 60.0)
    6.58 +
    6.59 +    (* handle metis preplay fail *)
    6.60 +    local
    6.61 +      open Unsynchronized
    6.62 +      val metis_fail = ref false
    6.63 +    in
    6.64 +      fun handle_metis_fail try_metis () =
    6.65 +        try_metis () handle exn =>
    6.66 +          (if Exn.is_interrupt exn orelse debug then reraise exn
    6.67 +           else metis_fail := true; some_preplay_time)
    6.68 +      fun get_time lazy_time =
    6.69 +        if !metis_fail andalso not (Lazy.is_finished lazy_time)
    6.70 +          then some_preplay_time
    6.71 +          else Lazy.force lazy_time
    6.72 +      val metis_fail = fn () => !metis_fail
    6.73 +    end
    6.74 +
    6.75 +    (* compress proof on top level - do not compress case splits *)
    6.76 +    fun compress_top_level on_top_level ctxt proof =
    6.77 +    let
    6.78 +      (* proof vector *)
    6.79 +      val proof_vect = proof |> map SOME |> Vector.fromList
    6.80 +      val n = Vector.length proof_vect
    6.81 +      val n_metis = metis_steps_top_level proof
    6.82 +      val target_n_metis = Real.fromInt n_metis / isar_compress |> Real.round
    6.83 +
    6.84 +      (* table for mapping from (top-level-)label to proof position *)
    6.85 +      fun update_table (i, Assume (l, _)) = Label_Table.update_new (l, i)
    6.86 +        | update_table (i, Obtain (_, _, l, _, _)) = Label_Table.update_new (l, i)
    6.87 +        | update_table (i, Prove (_, l, _, _)) = Label_Table.update_new (l, i)
    6.88 +        | update_table _ = I
    6.89 +      val label_index_table = fold_index update_table proof Label_Table.empty
    6.90 +      val lookup_indices = map_filter (Label_Table.lookup label_index_table)
    6.91 +
    6.92 +      (* proof references *)
    6.93 +      fun refs (Obtain (_, _, _, _, By_Metis (lfs, _))) = lookup_indices lfs
    6.94 +        | refs (Prove (_, _, _, By_Metis (lfs, _))) = lookup_indices lfs
    6.95 +        | refs (Prove (_, _, _, Case_Split (cases, (lfs, _)))) =
    6.96 +          lookup_indices lfs @ maps (maps refs) cases
    6.97 +        | refs (Prove (_, _, _, Subblock proof)) = maps refs proof
    6.98 +        | refs _ = []
    6.99 +      val refed_by_vect =
   6.100 +        Vector.tabulate (n, (fn _ => []))
   6.101 +        |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) proof
   6.102 +        |> Vector.map rev (* after rev, indices are sorted in ascending order *)
   6.103 +
   6.104 +      (* candidates for elimination, use table as priority queue (greedy
   6.105 +         algorithm) *)
   6.106 +      fun add_if_cand proof_vect (i, [j]) =
   6.107 +          (case (the (get i proof_vect), the (get j proof_vect)) of
   6.108 +            (Prove (_, _, t, By_Metis _), Prove (_, _, _, By_Metis _)) =>
   6.109 +              cons (Term.size_of_term t, i)
   6.110 +          | (Prove (_, _, t, By_Metis _), Obtain (_, _, _, _, By_Metis _)) =>
   6.111 +              cons (Term.size_of_term t, i)
   6.112 +          | _ => I)
   6.113 +        | add_if_cand _ _ = I
   6.114 +      val cand_tab =
   6.115 +        v_fold_index (add_if_cand proof_vect) refed_by_vect []
   6.116 +        |> Inttab.make_list
   6.117 +
   6.118 +      (* cache metis preplay times in lazy time vector *)
   6.119 +      val metis_time =
   6.120 +        v_map_index
   6.121 +          (if not preplay then K (zero_preplay_time) #> Lazy.value
   6.122 +           else
   6.123 +             apsnd the (* step *)
   6.124 +             #> apfst (fn i => try (get (i-1) #> the) proof_vect) (* succedent *)
   6.125 +             #> try_metis debug type_enc lam_trans ctxt preplay_timeout
   6.126 +             #> handle_metis_fail
   6.127 +             #> Lazy.lazy)
   6.128 +          proof_vect
   6.129 +
   6.130 +      fun sum_up_time lazy_time_vector =
   6.131 +        Vector.foldl
   6.132 +          (apfst get_time #> uncurry add_preplay_time)
   6.133 +          zero_preplay_time lazy_time_vector
   6.134 +
   6.135 +      (* Merging *)
   6.136 +      fun merge (Prove (_, label1, _, By_Metis (lfs1, gfs1))) step2 =
   6.137 +          let
   6.138 +            val (step_constructor, lfs2, gfs2) =
   6.139 +              (case step2 of
   6.140 +                (Prove (qs2, label2, t, By_Metis (lfs2, gfs2))) =>
   6.141 +                  (fn by => Prove (qs2, label2, t, by), lfs2, gfs2)
   6.142 +              | (Obtain (qs2, xs, label2, t, By_Metis (lfs2, gfs2))) =>
   6.143 +                  (fn by => Obtain (qs2, xs, label2, t, by), lfs2, gfs2)
   6.144 +              | _ => error "sledgehammer_compress: unmergeable Isar steps" )
   6.145 +            val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1
   6.146 +            val gfs = union (op =) gfs1 gfs2
   6.147 +          in step_constructor (By_Metis (lfs, gfs)) end
   6.148 +        | merge _ _ = error "sledgehammer_compress: unmergeable Isar steps"
   6.149 +
   6.150 +      fun try_merge metis_time (s1, i) (s2, j) =
   6.151 +        if not preplay then (merge s1 s2 |> SOME, metis_time)
   6.152 +        else
   6.153 +          (case get i metis_time |> Lazy.force of
   6.154 +            (true, _) => (NONE, metis_time)
   6.155 +          | (_, t1) =>
   6.156 +            (case get j metis_time |> Lazy.force of
   6.157 +              (true, _) => (NONE, metis_time)
   6.158 +            | (_, t2) =>
   6.159 +              let
   6.160 +                val s12 = merge s1 s2
   6.161 +                val timeout = time_mult merge_timeout_slack (Time.+(t1, t2))
   6.162 +              in
   6.163 +                case try_metis_quietly debug type_enc lam_trans ctxt timeout
   6.164 +                (NONE, s12) () of
   6.165 +                  (true, _) => (NONE, metis_time)
   6.166 +                | exact_time =>
   6.167 +                  (SOME s12, metis_time
   6.168 +                             |> replace (zero_preplay_time |> Lazy.value) i
   6.169 +                             |> replace (Lazy.value exact_time) j)
   6.170 +
   6.171 +              end))
   6.172 +
   6.173 +      fun merge_steps metis_time proof_vect refed_by cand_tab n' n_metis' =
   6.174 +        if Inttab.is_empty cand_tab
   6.175 +          orelse n_metis' <= target_n_metis
   6.176 +          orelse (on_top_level andalso n'<3)
   6.177 +        then
   6.178 +          (Vector.foldr
   6.179 +             (fn (NONE, proof) => proof | (SOME s, proof) => s :: proof)
   6.180 +             [] proof_vect,
   6.181 +           sum_up_time metis_time)
   6.182 +        else
   6.183 +          let
   6.184 +            val (i, cand_tab) = pop_max cand_tab
   6.185 +            val j = get i refed_by |> the_single
   6.186 +            val s1 = get i proof_vect |> the
   6.187 +            val s2 = get j proof_vect |> the
   6.188 +          in
   6.189 +            case try_merge metis_time (s1, i) (s2, j) of
   6.190 +              (NONE, metis_time) =>
   6.191 +              merge_steps metis_time proof_vect refed_by cand_tab n' n_metis'
   6.192 +            | (s, metis_time) =>
   6.193 +            let
   6.194 +              val refs = refs s1
   6.195 +              val refed_by = refed_by |> fold
   6.196 +                (update (Ord_List.remove int_ord i #> Ord_List.insert int_ord j)) refs
   6.197 +              val new_candidates =
   6.198 +                fold (add_if_cand proof_vect)
   6.199 +                  (map (fn i => (i, get i refed_by)) refs) []
   6.200 +              val cand_tab = add_list cand_tab new_candidates
   6.201 +              val proof_vect = proof_vect |> replace NONE i |> replace s j
   6.202 +            in
   6.203 +              merge_steps metis_time proof_vect refed_by cand_tab (n' - 1)
   6.204 +                          (n_metis' - 1)
   6.205 +            end
   6.206 +          end
   6.207 +    in
   6.208 +      merge_steps metis_time proof_vect refed_by_vect cand_tab n n_metis
   6.209 +    end
   6.210 +
   6.211 +    fun do_proof on_top_level ctxt proof =
   6.212 +      let
   6.213 +        (* Enrich context with top-level facts *)
   6.214 +        val thy = Proof_Context.theory_of ctxt
   6.215 +        (* TODO: add Skolem variables to context? *)
   6.216 +        fun enrich_with_fact l t =
   6.217 +          Proof_Context.put_thms false
   6.218 +            (string_for_label l, SOME [Skip_Proof.make_thm thy t])
   6.219 +        fun enrich_with_step (Assume (l, t)) = enrich_with_fact l t
   6.220 +          | enrich_with_step (Obtain (_, _, l, t, _)) = enrich_with_fact l t
   6.221 +          | enrich_with_step (Prove (_, l, t, _)) = enrich_with_fact l t
   6.222 +          | enrich_with_step _ = I
   6.223 +        val rich_ctxt = fold enrich_with_step proof ctxt
   6.224 +
   6.225 +        (* compress subproofs (case_splits and subblocks) and top-levl *)
   6.226 +        val ((proof, top_level_time), lower_level_time) =
   6.227 +          proof |> do_subproof rich_ctxt
   6.228 +                |>> compress_top_level on_top_level rich_ctxt
   6.229 +      in
   6.230 +        (proof, add_preplay_time lower_level_time top_level_time)
   6.231 +      end
   6.232 +
   6.233 +    and do_subproof ctxt proof =
   6.234 +      let
   6.235 +        fun compress_each_and_collect_time compress candidates =
   6.236 +          let fun f_m cand time = compress cand ||> add_preplay_time time
   6.237 +          in fold_map f_m candidates zero_preplay_time end
   6.238 +        val compress_subproof =
   6.239 +          compress_each_and_collect_time (do_proof false ctxt)
   6.240 +        fun compress (Prove (qs, l, t, Case_Split (cases, facts))) =
   6.241 +            let val (cases, time) = compress_subproof cases
   6.242 +            in (Prove (qs, l, t, Case_Split (cases, facts)), time) end
   6.243 +          | compress (Prove (qs, l, t, Subblock proof)) =
   6.244 +            let val ([proof], time) = compress_subproof [proof]
   6.245 +            in (Prove (qs, l, t, Subblock proof), time) end
   6.246 +          | compress step = (step, zero_preplay_time)
   6.247 +      in
   6.248 +        compress_each_and_collect_time compress proof
   6.249 +      end
   6.250 +  in
   6.251 +    do_proof true ctxt proof
   6.252 +    |> apsnd (pair (metis_fail ()))
   6.253 +  end
   6.254 +
   6.255 +end
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Feb 14 22:49:22 2013 +0100
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Feb 14 22:49:22 2013 +0100
     7.3 @@ -95,7 +95,7 @@
     7.4     ("max_mono_iters", "smart"),
     7.5     ("max_new_mono_instances", "smart"),
     7.6     ("isar_proofs", "false"),
     7.7 -   ("isar_shrink", "10"),
     7.8 +   ("isar_compress", "10"),
     7.9     ("slice", "true"),
    7.10     ("minimize", "smart"),
    7.11     ("preplay_timeout", "3")]
    7.12 @@ -119,7 +119,7 @@
    7.13  val params_for_minimize =
    7.14    ["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans",
    7.15     "uncurried_aliases", "max_mono_iters", "max_new_mono_instances",
    7.16 -   "learn", "isar_proofs", "isar_shrink", "timeout", "preplay_timeout"]
    7.17 +   "learn", "isar_proofs", "isar_compress", "timeout", "preplay_timeout"]
    7.18  
    7.19  val property_dependent_params = ["provers", "timeout"]
    7.20  
    7.21 @@ -314,7 +314,7 @@
    7.22      val max_new_mono_instances =
    7.23        lookup_option lookup_int "max_new_mono_instances"
    7.24      val isar_proofs = lookup_bool "isar_proofs"
    7.25 -    val isar_shrink = Real.max (1.0, lookup_real "isar_shrink")
    7.26 +    val isar_compress = Real.max (1.0, lookup_real "isar_compress")
    7.27      val slice = mode <> Auto_Try andalso lookup_bool "slice"
    7.28      val minimize =
    7.29        if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
    7.30 @@ -330,7 +330,7 @@
    7.31       learn = learn, fact_filter = fact_filter, max_facts = max_facts,
    7.32       fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
    7.33       max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
    7.34 -     isar_shrink = isar_shrink, slice = slice, minimize = minimize,
    7.35 +     isar_compress = isar_compress, slice = slice, minimize = minimize,
    7.36       timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
    7.37    end
    7.38  
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Feb 14 22:49:22 2013 +0100
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Feb 14 22:49:22 2013 +0100
     8.3 @@ -54,7 +54,7 @@
     8.4  
     8.5  fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
     8.6                   max_new_mono_instances, type_enc, strict, lam_trans,
     8.7 -                 uncurried_aliases, isar_proofs, isar_shrink,
     8.8 +                 uncurried_aliases, isar_proofs, isar_compress,
     8.9                   preplay_timeout, ...} : params)
    8.10                 silent (prover : prover) timeout i n state facts =
    8.11    let
    8.12 @@ -76,7 +76,7 @@
    8.13         learn = false, fact_filter = NONE, max_facts = SOME (length facts),
    8.14         fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters,
    8.15         max_new_mono_instances = max_new_mono_instances,
    8.16 -       isar_proofs = isar_proofs, isar_shrink = isar_shrink,
    8.17 +       isar_proofs = isar_proofs, isar_compress = isar_compress,
    8.18         slice = false, minimize = SOME false, timeout = timeout,
    8.19         preplay_timeout = preplay_timeout, expect = ""}
    8.20      val problem =
    8.21 @@ -243,7 +243,7 @@
    8.22          ({debug, verbose, overlord, blocking, provers, type_enc, strict,
    8.23           lam_trans, uncurried_aliases, learn, fact_filter, max_facts,
    8.24           fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proofs,
    8.25 -         isar_shrink, slice, minimize, timeout, preplay_timeout, expect}
    8.26 +         isar_compress, slice, minimize, timeout, preplay_timeout, expect}
    8.27           : params) =
    8.28    let
    8.29      fun lookup_override name default_value =
    8.30 @@ -261,7 +261,7 @@
    8.31       learn = learn, fact_filter = fact_filter, max_facts = max_facts,
    8.32       fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
    8.33       max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
    8.34 -     isar_shrink = isar_shrink, slice = slice, minimize = minimize,
    8.35 +     isar_compress = isar_compress, slice = slice, minimize = minimize,
    8.36       timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
    8.37    end
    8.38  
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Thu Feb 14 22:49:22 2013 +0100
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Thu Feb 14 22:49:22 2013 +0100
     9.3 @@ -1,4 +1,4 @@
     9.4 -(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_shrink.ML
     9.5 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
     9.6      Author:     Jasmin Blanchette, TU Muenchen
     9.7      Author:     Steffen Juilf Smolka, TU Muenchen
     9.8  
    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Feb 14 22:49:22 2013 +0100
    10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Feb 14 22:49:22 2013 +0100
    10.3 @@ -35,7 +35,7 @@
    10.4       max_mono_iters : int option,
    10.5       max_new_mono_instances : int option,
    10.6       isar_proofs : bool,
    10.7 -     isar_shrink : real,
    10.8 +     isar_compress : real,
    10.9       slice : bool,
   10.10       minimize : bool option,
   10.11       timeout : Time.time option,
   10.12 @@ -322,7 +322,7 @@
   10.13     max_mono_iters : int option,
   10.14     max_new_mono_instances : int option,
   10.15     isar_proofs : bool,
   10.16 -   isar_shrink : real,
   10.17 +   isar_compress : real,
   10.18     slice : bool,
   10.19     minimize : bool option,
   10.20     timeout : Time.time option,
   10.21 @@ -635,7 +635,7 @@
   10.22            best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config)
   10.23          (params as {debug, verbose, overlord, type_enc, strict, lam_trans,
   10.24                      uncurried_aliases, fact_filter, max_facts, max_mono_iters,
   10.25 -                    max_new_mono_instances, isar_proofs, isar_shrink,
   10.26 +                    max_new_mono_instances, isar_proofs, isar_compress,
   10.27                      slice, timeout, preplay_timeout, ...})
   10.28          minimize_command
   10.29          ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   10.30 @@ -898,7 +898,7 @@
   10.31                    else
   10.32                      ()
   10.33                  val isar_params =
   10.34 -                  (debug, verbose, preplay_timeout, isar_shrink,
   10.35 +                  (debug, verbose, preplay_timeout, isar_compress,
   10.36                     pool, fact_names, sym_tab, atp_proof, goal)
   10.37                  val one_line_params =
   10.38                    (preplay, proof_banner mode name, used_facts,
    11.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Feb 14 22:49:22 2013 +0100
    11.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Feb 14 22:49:22 2013 +0100
    11.3 @@ -54,7 +54,7 @@
    11.4  open Sledgehammer_Util
    11.5  open Sledgehammer_Proof
    11.6  open Sledgehammer_Annotate
    11.7 -open Sledgehammer_Shrink
    11.8 +open Sledgehammer_Compress
    11.9  
   11.10  structure String_Redirect = ATP_Proof_Redirect(
   11.11    type key = step_name
   11.12 @@ -639,7 +639,7 @@
   11.13    * (string * stature) list vector * int Symtab.table * string proof * thm
   11.14  
   11.15  fun isar_proof_text ctxt isar_proofs
   11.16 -    (debug, verbose, preplay_timeout, isar_shrink, pool, fact_names, sym_tab,
   11.17 +    (debug, verbose, preplay_timeout, isar_compress, pool, fact_names, sym_tab,
   11.18       atp_proof, goal)
   11.19      (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
   11.20    let
   11.21 @@ -757,12 +757,12 @@
   11.22            |> redirect_graph axioms tainted bot
   11.23            |> map (isar_step_of_direct_inf true)
   11.24            |> append assms
   11.25 -          |> (if not preplay andalso isar_shrink <= 1.0 then
   11.26 +          |> (if not preplay andalso isar_compress <= 1.0 then
   11.27                  rpair (false, (true, seconds 0.0))
   11.28                else
   11.29 -                shrink_proof debug ctxt type_enc lam_trans preplay
   11.30 +                compress_proof debug ctxt type_enc lam_trans preplay
   11.31                    preplay_timeout
   11.32 -                  (if isar_proofs then isar_shrink else 1000.0))
   11.33 +                  (if isar_proofs then isar_compress else 1000.0))
   11.34         (* |>> reorder_proof_to_minimize_jumps (* ? *) *)
   11.35            |>> chain_direct_proof
   11.36            |>> kill_useless_labels_in_proof
    12.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Thu Feb 14 22:49:22 2013 +0100
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,252 +0,0 @@
    12.4 -(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_shrink.ML
    12.5 -    Author:     Jasmin Blanchette, TU Muenchen
    12.6 -    Author:     Steffen Juilf Smolka, TU Muenchen
    12.7 -
    12.8 -Shrinking of reconstructed isar proofs.
    12.9 -*)
   12.10 -
   12.11 -signature SLEDGEHAMMER_SHRINK =
   12.12 -sig
   12.13 -  type isar_step = Sledgehammer_Proof.isar_step
   12.14 -  type preplay_time = Sledgehammer_Preplay.preplay_time
   12.15 -  val shrink_proof :
   12.16 -    bool -> Proof.context -> string -> string -> bool -> Time.time option
   12.17 -    -> real -> isar_step list -> isar_step list * (bool * preplay_time)
   12.18 -end
   12.19 -
   12.20 -structure Sledgehammer_Shrink : SLEDGEHAMMER_SHRINK =
   12.21 -struct
   12.22 -
   12.23 -open Sledgehammer_Util
   12.24 -open Sledgehammer_Proof
   12.25 -open Sledgehammer_Preplay
   12.26 -
   12.27 -(* Parameters *)
   12.28 -val merge_timeout_slack = 1.2
   12.29 -
   12.30 -(* Data structures, orders *)
   12.31 -val label_ord = prod_ord int_ord fast_string_ord o pairself swap
   12.32 -structure Label_Table = Table(
   12.33 -  type key = label
   12.34 -  val ord = label_ord)
   12.35 -
   12.36 -(* clean vector interface *)
   12.37 -fun get i v = Vector.sub (v, i)
   12.38 -fun replace x i v = Vector.update (v, i, x)
   12.39 -fun update f i v = replace (get i v |> f) i v
   12.40 -fun v_map_index f v = Vector.foldr (op::) nil v |> map_index f |> Vector.fromList
   12.41 -fun v_fold_index f v s =
   12.42 -  Vector.foldl (fn (x, (i, s)) => (i+1, f (i, x) s)) (0, s) v |> snd
   12.43 -
   12.44 -(* Queue interface to table *)
   12.45 -fun pop tab key =
   12.46 -  let val v = hd (Inttab.lookup_list tab key) in
   12.47 -    (v, Inttab.remove_list (op =) (key, v) tab)
   12.48 -  end
   12.49 -fun pop_max tab = pop tab (the (Inttab.max_key tab))
   12.50 -fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab
   12.51 -
   12.52 -(* Main function for shrinking proofs *)
   12.53 -fun shrink_proof debug ctxt type_enc lam_trans preplay preplay_timeout
   12.54 -                 isar_shrink proof =
   12.55 -  let
   12.56 -    (* 60 seconds seems like a good interpreation of "no timeout" *)
   12.57 -    val preplay_timeout = preplay_timeout |> the_default (seconds 60.0)
   12.58 -
   12.59 -    (* handle metis preplay fail *)
   12.60 -    local
   12.61 -      open Unsynchronized
   12.62 -      val metis_fail = ref false
   12.63 -    in
   12.64 -      fun handle_metis_fail try_metis () =
   12.65 -        try_metis () handle exn =>
   12.66 -          (if Exn.is_interrupt exn orelse debug then reraise exn
   12.67 -           else metis_fail := true; some_preplay_time)
   12.68 -      fun get_time lazy_time =
   12.69 -        if !metis_fail andalso not (Lazy.is_finished lazy_time)
   12.70 -          then some_preplay_time
   12.71 -          else Lazy.force lazy_time
   12.72 -      val metis_fail = fn () => !metis_fail
   12.73 -    end
   12.74 -
   12.75 -    (* Shrink proof on top level - do not shrink case splits *)
   12.76 -    fun shrink_top_level on_top_level ctxt proof =
   12.77 -    let
   12.78 -      (* proof vector *)
   12.79 -      val proof_vect = proof |> map SOME |> Vector.fromList
   12.80 -      val n = Vector.length proof_vect
   12.81 -      val n_metis = metis_steps_top_level proof
   12.82 -      val target_n_metis = Real.fromInt n_metis / isar_shrink |> Real.round
   12.83 -
   12.84 -      (* table for mapping from (top-level-)label to proof position *)
   12.85 -      fun update_table (i, Assume (l, _)) = Label_Table.update_new (l, i)
   12.86 -        | update_table (i, Obtain (_, _, l, _, _)) = Label_Table.update_new (l, i)
   12.87 -        | update_table (i, Prove (_, l, _, _)) = Label_Table.update_new (l, i)
   12.88 -        | update_table _ = I
   12.89 -      val label_index_table = fold_index update_table proof Label_Table.empty
   12.90 -      val lookup_indices = map_filter (Label_Table.lookup label_index_table)
   12.91 -
   12.92 -      (* proof references *)
   12.93 -      fun refs (Obtain (_, _, _, _, By_Metis (lfs, _))) = lookup_indices lfs
   12.94 -        | refs (Prove (_, _, _, By_Metis (lfs, _))) = lookup_indices lfs
   12.95 -        | refs (Prove (_, _, _, Case_Split (cases, (lfs, _)))) =
   12.96 -          lookup_indices lfs @ maps (maps refs) cases
   12.97 -        | refs (Prove (_, _, _, Subblock proof)) = maps refs proof
   12.98 -        | refs _ = []
   12.99 -      val refed_by_vect =
  12.100 -        Vector.tabulate (n, (fn _ => []))
  12.101 -        |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) proof
  12.102 -        |> Vector.map rev (* after rev, indices are sorted in ascending order *)
  12.103 -
  12.104 -      (* candidates for elimination, use table as priority queue (greedy
  12.105 -         algorithm) *)
  12.106 -      fun add_if_cand proof_vect (i, [j]) =
  12.107 -          (case (the (get i proof_vect), the (get j proof_vect)) of
  12.108 -            (Prove (_, _, t, By_Metis _), Prove (_, _, _, By_Metis _)) =>
  12.109 -              cons (Term.size_of_term t, i)
  12.110 -          | (Prove (_, _, t, By_Metis _), Obtain (_, _, _, _, By_Metis _)) =>
  12.111 -              cons (Term.size_of_term t, i)
  12.112 -          | _ => I)
  12.113 -        | add_if_cand _ _ = I
  12.114 -      val cand_tab =
  12.115 -        v_fold_index (add_if_cand proof_vect) refed_by_vect []
  12.116 -        |> Inttab.make_list
  12.117 -
  12.118 -      (* cache metis preplay times in lazy time vector *)
  12.119 -      val metis_time =
  12.120 -        v_map_index
  12.121 -          (if not preplay then K (zero_preplay_time) #> Lazy.value
  12.122 -           else
  12.123 -             apsnd the (* step *)
  12.124 -             #> apfst (fn i => try (get (i-1) #> the) proof_vect) (* succedent *)
  12.125 -             #> try_metis debug type_enc lam_trans ctxt preplay_timeout
  12.126 -             #> handle_metis_fail
  12.127 -             #> Lazy.lazy)
  12.128 -          proof_vect
  12.129 -
  12.130 -      fun sum_up_time lazy_time_vector =
  12.131 -        Vector.foldl
  12.132 -          (apfst get_time #> uncurry add_preplay_time)
  12.133 -          zero_preplay_time lazy_time_vector
  12.134 -
  12.135 -      (* Merging *)
  12.136 -      fun merge (Prove (_, label1, _, By_Metis (lfs1, gfs1))) step2 =
  12.137 -          let
  12.138 -            val (step_constructor, lfs2, gfs2) =
  12.139 -              (case step2 of
  12.140 -                (Prove (qs2, label2, t, By_Metis (lfs2, gfs2))) =>
  12.141 -                  (fn by => Prove (qs2, label2, t, by), lfs2, gfs2)
  12.142 -              | (Obtain (qs2, xs, label2, t, By_Metis (lfs2, gfs2))) =>
  12.143 -                  (fn by => Obtain (qs2, xs, label2, t, by), lfs2, gfs2)
  12.144 -              | _ => error "sledgehammer_shrink: unmergeable Isar steps" )
  12.145 -            val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1
  12.146 -            val gfs = union (op =) gfs1 gfs2
  12.147 -          in step_constructor (By_Metis (lfs, gfs)) end
  12.148 -        | merge _ _ = error "sledgehammer_shrink: unmergeable Isar steps"
  12.149 -
  12.150 -      fun try_merge metis_time (s1, i) (s2, j) =
  12.151 -        if not preplay then (merge s1 s2 |> SOME, metis_time)
  12.152 -        else
  12.153 -          (case get i metis_time |> Lazy.force of
  12.154 -            (true, _) => (NONE, metis_time)
  12.155 -          | (_, t1) =>
  12.156 -            (case get j metis_time |> Lazy.force of
  12.157 -              (true, _) => (NONE, metis_time)
  12.158 -            | (_, t2) =>
  12.159 -              let
  12.160 -                val s12 = merge s1 s2
  12.161 -                val timeout = time_mult merge_timeout_slack (Time.+(t1, t2))
  12.162 -              in
  12.163 -                case try_metis_quietly debug type_enc lam_trans ctxt timeout
  12.164 -                (NONE, s12) () of
  12.165 -                  (true, _) => (NONE, metis_time)
  12.166 -                | exact_time =>
  12.167 -                  (SOME s12, metis_time
  12.168 -                             |> replace (zero_preplay_time |> Lazy.value) i
  12.169 -                             |> replace (Lazy.value exact_time) j)
  12.170 -
  12.171 -              end))
  12.172 -
  12.173 -      fun merge_steps metis_time proof_vect refed_by cand_tab n' n_metis' =
  12.174 -        if Inttab.is_empty cand_tab
  12.175 -          orelse n_metis' <= target_n_metis
  12.176 -          orelse (on_top_level andalso n'<3)
  12.177 -        then
  12.178 -          (Vector.foldr
  12.179 -             (fn (NONE, proof) => proof | (SOME s, proof) => s :: proof)
  12.180 -             [] proof_vect,
  12.181 -           sum_up_time metis_time)
  12.182 -        else
  12.183 -          let
  12.184 -            val (i, cand_tab) = pop_max cand_tab
  12.185 -            val j = get i refed_by |> the_single
  12.186 -            val s1 = get i proof_vect |> the
  12.187 -            val s2 = get j proof_vect |> the
  12.188 -          in
  12.189 -            case try_merge metis_time (s1, i) (s2, j) of
  12.190 -              (NONE, metis_time) =>
  12.191 -              merge_steps metis_time proof_vect refed_by cand_tab n' n_metis'
  12.192 -            | (s, metis_time) =>
  12.193 -            let
  12.194 -              val refs = refs s1
  12.195 -              val refed_by = refed_by |> fold
  12.196 -                (update (Ord_List.remove int_ord i #> Ord_List.insert int_ord j)) refs
  12.197 -              val new_candidates =
  12.198 -                fold (add_if_cand proof_vect)
  12.199 -                  (map (fn i => (i, get i refed_by)) refs) []
  12.200 -              val cand_tab = add_list cand_tab new_candidates
  12.201 -              val proof_vect = proof_vect |> replace NONE i |> replace s j
  12.202 -            in
  12.203 -              merge_steps metis_time proof_vect refed_by cand_tab (n' - 1)
  12.204 -                          (n_metis' - 1)
  12.205 -            end
  12.206 -          end
  12.207 -    in
  12.208 -      merge_steps metis_time proof_vect refed_by_vect cand_tab n n_metis
  12.209 -    end
  12.210 -
  12.211 -    fun do_proof on_top_level ctxt proof =
  12.212 -      let
  12.213 -        (* Enrich context with top-level facts *)
  12.214 -        val thy = Proof_Context.theory_of ctxt
  12.215 -        (* TODO: add Skolem variables to context? *)
  12.216 -        fun enrich_with_fact l t =
  12.217 -          Proof_Context.put_thms false
  12.218 -            (string_for_label l, SOME [Skip_Proof.make_thm thy t])
  12.219 -        fun enrich_with_step (Assume (l, t)) = enrich_with_fact l t
  12.220 -          | enrich_with_step (Obtain (_, _, l, t, _)) = enrich_with_fact l t
  12.221 -          | enrich_with_step (Prove (_, l, t, _)) = enrich_with_fact l t
  12.222 -          | enrich_with_step _ = I
  12.223 -        val rich_ctxt = fold enrich_with_step proof ctxt
  12.224 -
  12.225 -        (* Shrink subproofs (case_splits and subblocks) and top-levl *)
  12.226 -        val ((proof, top_level_time), lower_level_time) =
  12.227 -          proof |> do_subproof rich_ctxt
  12.228 -                |>> shrink_top_level on_top_level rich_ctxt
  12.229 -      in
  12.230 -        (proof, add_preplay_time lower_level_time top_level_time)
  12.231 -      end
  12.232 -
  12.233 -    and do_subproof ctxt proof =
  12.234 -      let
  12.235 -        fun shrink_each_and_collect_time shrink candidates =
  12.236 -          let fun f_m cand time = shrink cand ||> add_preplay_time time
  12.237 -          in fold_map f_m candidates zero_preplay_time end
  12.238 -        val shrink_subproof =
  12.239 -          shrink_each_and_collect_time (do_proof false ctxt)
  12.240 -        fun shrink (Prove (qs, l, t, Case_Split (cases, facts))) =
  12.241 -            let val (cases, time) = shrink_subproof cases
  12.242 -            in (Prove (qs, l, t, Case_Split (cases, facts)), time) end
  12.243 -          | shrink (Prove (qs, l, t, Subblock proof)) =
  12.244 -            let val ([proof], time) = shrink_subproof [proof]
  12.245 -            in (Prove (qs, l, t, Subblock proof), time) end
  12.246 -          | shrink step = (step, zero_preplay_time)
  12.247 -      in
  12.248 -        shrink_each_and_collect_time shrink proof
  12.249 -      end
  12.250 -  in
  12.251 -    do_proof true ctxt proof
  12.252 -    |> apsnd (pair (metis_fail ()))
  12.253 -  end
  12.254 -
  12.255 -end