renamed sledgehammer_shrink to sledgehammer_compress
authorsmolkas
Thu, 14 Feb 2013 22:49:22 +0100
changeset 51130 76d68444cd59
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
--- a/src/Doc/Sledgehammer/document/root.tex	Thu Feb 14 22:49:22 2013 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Thu Feb 14 22:49:22 2013 +0100
@@ -369,7 +369,7 @@
 \item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies
 that Isar proofs should be generated, instead of one-liner \textit{metis} or
 \textit{smt} proofs. The length of the Isar proofs can be controlled by setting
-\textit{isar\_shrink} (\S\ref{output-format}).
+\textit{isar\_compress} (\S\ref{output-format}).
 
 \item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the
 provers' time limit. It is set to 30 seconds, but since Sledgehammer runs
@@ -508,7 +508,7 @@
 is highly experimental. Work on a new implementation has begun. There is a large body of
 research into transforming resolution proofs into natural deduction proofs (such
 as Isar proofs), which we hope to leverage. In the meantime, a workaround is to
-set the \textit{isar\_shrink} option (\S\ref{output-format}) to a larger
+set the \textit{isar\_compress} option (\S\ref{output-format}) to a larger
 value or to try several provers and keep the nicest-looking proof.
 
 \point{How can I tell whether a suggested proof is sound?}
@@ -1302,7 +1302,7 @@
 fails; however, they are usually faster and sometimes more robust than
 \textit{metis} proofs.
 
-\opdefault{isar\_shrink}{int}{\upshape 10}
+\opdefault{isar\_compress}{int}{\upshape 10}
 Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs}
 is enabled. A value of $n$ indicates that each Isar proof step should correspond
 to a group of up to $n$ consecutive proof steps in the ATP proof.
--- a/src/HOL/Metis_Examples/Big_O.thy	Thu Feb 14 22:49:22 2013 +0100
+++ b/src/HOL/Metis_Examples/Big_O.thy	Thu Feb 14 22:49:22 2013 +0100
@@ -29,7 +29,7 @@
 
 (*** Now various verions with an increasing shrink factor ***)
 
-sledgehammer_params [isar_proofs, isar_shrink = 1]
+sledgehammer_params [isar_proofs, isar_compress = 1]
 
 lemma
   "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -60,7 +60,7 @@
   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F4)
 qed
 
-sledgehammer_params [isar_proofs, isar_shrink = 2]
+sledgehammer_params [isar_proofs, isar_compress = 2]
 
 lemma
   "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -83,7 +83,7 @@
   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F2)
 qed
 
-sledgehammer_params [isar_proofs, isar_shrink = 3]
+sledgehammer_params [isar_proofs, isar_compress = 3]
 
 lemma
   "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -103,7 +103,7 @@
   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_ge_zero)
 qed
 
-sledgehammer_params [isar_proofs, isar_shrink = 4]
+sledgehammer_params [isar_proofs, isar_compress = 4]
 
 lemma
   "(\<exists>c\<Colon>'a\<Colon>linordered_idom.
@@ -123,7 +123,7 @@
   thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis abs_mult)
 qed
 
-sledgehammer_params [isar_proofs, isar_shrink = 1]
+sledgehammer_params [isar_proofs, isar_compress = 1]
 
 lemma bigo_alt_def: "O(f) = {h. \<exists>c. (0 < c \<and> (\<forall>x. abs (h x) <= c * abs (f x)))}"
 by (auto simp add: bigo_def bigo_pos_const)
--- a/src/HOL/Metis_Examples/Sets.thy	Thu Feb 14 22:49:22 2013 +0100
+++ b/src/HOL/Metis_Examples/Sets.thy	Thu Feb 14 22:49:22 2013 +0100
@@ -21,7 +21,7 @@
 lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
 by metis
 
-sledgehammer_params [isar_proofs, isar_shrink = 1]
+sledgehammer_params [isar_proofs, isar_compress = 1]
 
 (*multiple versions of this example*)
 lemma (*equal_union: *)
@@ -70,7 +70,7 @@
   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
 qed
 
-sledgehammer_params [isar_proofs, isar_shrink = 2]
+sledgehammer_params [isar_proofs, isar_compress = 2]
 
 lemma (*equal_union: *)
    "(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))"
@@ -107,7 +107,7 @@
   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
 qed
 
-sledgehammer_params [isar_proofs, isar_shrink = 3]
+sledgehammer_params [isar_proofs, isar_compress = 3]
 
 lemma (*equal_union: *)
    "(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))"
@@ -124,7 +124,7 @@
   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)
 qed
 
-sledgehammer_params [isar_proofs, isar_shrink = 4]
+sledgehammer_params [isar_proofs, isar_compress = 4]
 
 lemma (*equal_union: *)
    "(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))"
@@ -140,7 +140,7 @@
   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)
 qed
 
-sledgehammer_params [isar_proofs, isar_shrink = 1]
+sledgehammer_params [isar_proofs, isar_compress = 1]
 
 lemma (*equal_union: *)
    "(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))"
--- a/src/HOL/Metis_Examples/Trans_Closure.thy	Thu Feb 14 22:49:22 2013 +0100
+++ b/src/HOL/Metis_Examples/Trans_Closure.thy	Thu Feb 14 22:49:22 2013 +0100
@@ -44,7 +44,7 @@
 
 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>
        \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
-(* sledgehammer [isar_proofs, isar_shrink = 2] *)
+(* sledgehammer [isar_proofs, isar_compress = 2] *)
 proof -
   assume A1: "f c = Intg x"
   assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x"
--- a/src/HOL/Sledgehammer.thy	Thu Feb 14 22:49:22 2013 +0100
+++ b/src/HOL/Sledgehammer.thy	Thu Feb 14 22:49:22 2013 +0100
@@ -17,7 +17,7 @@
 ML_file "Tools/Sledgehammer/sledgehammer_proof.ML"
 ML_file "Tools/Sledgehammer/sledgehammer_annotate.ML"
 ML_file "Tools/Sledgehammer/sledgehammer_preplay.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_shrink.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_compress.ML"
 ML_file "Tools/Sledgehammer/sledgehammer_reconstruct.ML" 
 ML_file "Tools/Sledgehammer/sledgehammer_provers.ML"
 ML_file "Tools/Sledgehammer/sledgehammer_minimize.ML"
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Thu Feb 14 22:49:22 2013 +0100
@@ -0,0 +1,252 @@
+(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_compress.ML
+    Author:     Jasmin Blanchette, TU Muenchen
+    Author:     Steffen Juilf Smolka, TU Muenchen
+
+Compression of reconstructed isar proofs.
+*)
+
+signature SLEDGEHAMMER_COMPRESS =
+sig
+  type isar_step = Sledgehammer_Proof.isar_step
+  type preplay_time = Sledgehammer_Preplay.preplay_time
+  val compress_proof :
+    bool -> Proof.context -> string -> string -> bool -> Time.time option
+    -> real -> isar_step list -> isar_step list * (bool * preplay_time)
+end
+
+structure Sledgehammer_Compress : SLEDGEHAMMER_COMPRESS =
+struct
+
+open Sledgehammer_Util
+open Sledgehammer_Proof
+open Sledgehammer_Preplay
+
+(* Parameters *)
+val merge_timeout_slack = 1.2
+
+(* Data structures, orders *)
+val label_ord = prod_ord int_ord fast_string_ord o pairself swap
+structure Label_Table = Table(
+  type key = label
+  val ord = label_ord)
+
+(* clean vector interface *)
+fun get i v = Vector.sub (v, i)
+fun replace x i v = Vector.update (v, i, x)
+fun update f i v = replace (get i v |> f) i v
+fun v_map_index f v = Vector.foldr (op::) nil v |> map_index f |> Vector.fromList
+fun v_fold_index f v s =
+  Vector.foldl (fn (x, (i, s)) => (i+1, f (i, x) s)) (0, s) v |> snd
+
+(* Queue interface to table *)
+fun pop tab key =
+  let val v = hd (Inttab.lookup_list tab key) in
+    (v, Inttab.remove_list (op =) (key, v) tab)
+  end
+fun pop_max tab = pop tab (the (Inttab.max_key tab))
+fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab
+
+(* Main function for compresing proofs *)
+fun compress_proof debug ctxt type_enc lam_trans preplay preplay_timeout
+                   isar_compress proof =
+  let
+    (* 60 seconds seems like a good interpreation of "no timeout" *)
+    val preplay_timeout = preplay_timeout |> the_default (seconds 60.0)
+
+    (* handle metis preplay fail *)
+    local
+      open Unsynchronized
+      val metis_fail = ref false
+    in
+      fun handle_metis_fail try_metis () =
+        try_metis () handle exn =>
+          (if Exn.is_interrupt exn orelse debug then reraise exn
+           else metis_fail := true; some_preplay_time)
+      fun get_time lazy_time =
+        if !metis_fail andalso not (Lazy.is_finished lazy_time)
+          then some_preplay_time
+          else Lazy.force lazy_time
+      val metis_fail = fn () => !metis_fail
+    end
+
+    (* compress proof on top level - do not compress case splits *)
+    fun compress_top_level on_top_level ctxt proof =
+    let
+      (* proof vector *)
+      val proof_vect = proof |> map SOME |> Vector.fromList
+      val n = Vector.length proof_vect
+      val n_metis = metis_steps_top_level proof
+      val target_n_metis = Real.fromInt n_metis / isar_compress |> Real.round
+
+      (* table for mapping from (top-level-)label to proof position *)
+      fun update_table (i, Assume (l, _)) = Label_Table.update_new (l, i)
+        | update_table (i, Obtain (_, _, l, _, _)) = Label_Table.update_new (l, i)
+        | update_table (i, Prove (_, l, _, _)) = Label_Table.update_new (l, i)
+        | update_table _ = I
+      val label_index_table = fold_index update_table proof Label_Table.empty
+      val lookup_indices = map_filter (Label_Table.lookup label_index_table)
+
+      (* proof references *)
+      fun refs (Obtain (_, _, _, _, By_Metis (lfs, _))) = lookup_indices lfs
+        | refs (Prove (_, _, _, By_Metis (lfs, _))) = lookup_indices lfs
+        | refs (Prove (_, _, _, Case_Split (cases, (lfs, _)))) =
+          lookup_indices lfs @ maps (maps refs) cases
+        | refs (Prove (_, _, _, Subblock proof)) = maps refs proof
+        | refs _ = []
+      val refed_by_vect =
+        Vector.tabulate (n, (fn _ => []))
+        |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) proof
+        |> Vector.map rev (* after rev, indices are sorted in ascending order *)
+
+      (* candidates for elimination, use table as priority queue (greedy
+         algorithm) *)
+      fun add_if_cand proof_vect (i, [j]) =
+          (case (the (get i proof_vect), the (get j proof_vect)) of
+            (Prove (_, _, t, By_Metis _), Prove (_, _, _, By_Metis _)) =>
+              cons (Term.size_of_term t, i)
+          | (Prove (_, _, t, By_Metis _), Obtain (_, _, _, _, By_Metis _)) =>
+              cons (Term.size_of_term t, i)
+          | _ => I)
+        | add_if_cand _ _ = I
+      val cand_tab =
+        v_fold_index (add_if_cand proof_vect) refed_by_vect []
+        |> Inttab.make_list
+
+      (* cache metis preplay times in lazy time vector *)
+      val metis_time =
+        v_map_index
+          (if not preplay then K (zero_preplay_time) #> Lazy.value
+           else
+             apsnd the (* step *)
+             #> apfst (fn i => try (get (i-1) #> the) proof_vect) (* succedent *)
+             #> try_metis debug type_enc lam_trans ctxt preplay_timeout
+             #> handle_metis_fail
+             #> Lazy.lazy)
+          proof_vect
+
+      fun sum_up_time lazy_time_vector =
+        Vector.foldl
+          (apfst get_time #> uncurry add_preplay_time)
+          zero_preplay_time lazy_time_vector
+
+      (* Merging *)
+      fun merge (Prove (_, label1, _, By_Metis (lfs1, gfs1))) step2 =
+          let
+            val (step_constructor, lfs2, gfs2) =
+              (case step2 of
+                (Prove (qs2, label2, t, By_Metis (lfs2, gfs2))) =>
+                  (fn by => Prove (qs2, label2, t, by), lfs2, gfs2)
+              | (Obtain (qs2, xs, label2, t, By_Metis (lfs2, gfs2))) =>
+                  (fn by => Obtain (qs2, xs, label2, t, by), lfs2, gfs2)
+              | _ => error "sledgehammer_compress: unmergeable Isar steps" )
+            val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1
+            val gfs = union (op =) gfs1 gfs2
+          in step_constructor (By_Metis (lfs, gfs)) end
+        | merge _ _ = error "sledgehammer_compress: unmergeable Isar steps"
+
+      fun try_merge metis_time (s1, i) (s2, j) =
+        if not preplay then (merge s1 s2 |> SOME, metis_time)
+        else
+          (case get i metis_time |> Lazy.force of
+            (true, _) => (NONE, metis_time)
+          | (_, t1) =>
+            (case get j metis_time |> Lazy.force of
+              (true, _) => (NONE, metis_time)
+            | (_, t2) =>
+              let
+                val s12 = merge s1 s2
+                val timeout = time_mult merge_timeout_slack (Time.+(t1, t2))
+              in
+                case try_metis_quietly debug type_enc lam_trans ctxt timeout
+                (NONE, s12) () of
+                  (true, _) => (NONE, metis_time)
+                | exact_time =>
+                  (SOME s12, metis_time
+                             |> replace (zero_preplay_time |> Lazy.value) i
+                             |> replace (Lazy.value exact_time) j)
+
+              end))
+
+      fun merge_steps metis_time proof_vect refed_by cand_tab n' n_metis' =
+        if Inttab.is_empty cand_tab
+          orelse n_metis' <= target_n_metis
+          orelse (on_top_level andalso n'<3)
+        then
+          (Vector.foldr
+             (fn (NONE, proof) => proof | (SOME s, proof) => s :: proof)
+             [] proof_vect,
+           sum_up_time metis_time)
+        else
+          let
+            val (i, cand_tab) = pop_max cand_tab
+            val j = get i refed_by |> the_single
+            val s1 = get i proof_vect |> the
+            val s2 = get j proof_vect |> the
+          in
+            case try_merge metis_time (s1, i) (s2, j) of
+              (NONE, metis_time) =>
+              merge_steps metis_time proof_vect refed_by cand_tab n' n_metis'
+            | (s, metis_time) =>
+            let
+              val refs = refs s1
+              val refed_by = refed_by |> fold
+                (update (Ord_List.remove int_ord i #> Ord_List.insert int_ord j)) refs
+              val new_candidates =
+                fold (add_if_cand proof_vect)
+                  (map (fn i => (i, get i refed_by)) refs) []
+              val cand_tab = add_list cand_tab new_candidates
+              val proof_vect = proof_vect |> replace NONE i |> replace s j
+            in
+              merge_steps metis_time proof_vect refed_by cand_tab (n' - 1)
+                          (n_metis' - 1)
+            end
+          end
+    in
+      merge_steps metis_time proof_vect refed_by_vect cand_tab n n_metis
+    end
+
+    fun do_proof on_top_level ctxt proof =
+      let
+        (* Enrich context with top-level facts *)
+        val thy = Proof_Context.theory_of ctxt
+        (* TODO: add Skolem variables to context? *)
+        fun enrich_with_fact l t =
+          Proof_Context.put_thms false
+            (string_for_label l, SOME [Skip_Proof.make_thm thy t])
+        fun enrich_with_step (Assume (l, t)) = enrich_with_fact l t
+          | enrich_with_step (Obtain (_, _, l, t, _)) = enrich_with_fact l t
+          | enrich_with_step (Prove (_, l, t, _)) = enrich_with_fact l t
+          | enrich_with_step _ = I
+        val rich_ctxt = fold enrich_with_step proof ctxt
+
+        (* compress subproofs (case_splits and subblocks) and top-levl *)
+        val ((proof, top_level_time), lower_level_time) =
+          proof |> do_subproof rich_ctxt
+                |>> compress_top_level on_top_level rich_ctxt
+      in
+        (proof, add_preplay_time lower_level_time top_level_time)
+      end
+
+    and do_subproof ctxt proof =
+      let
+        fun compress_each_and_collect_time compress candidates =
+          let fun f_m cand time = compress cand ||> add_preplay_time time
+          in fold_map f_m candidates zero_preplay_time end
+        val compress_subproof =
+          compress_each_and_collect_time (do_proof false ctxt)
+        fun compress (Prove (qs, l, t, Case_Split (cases, facts))) =
+            let val (cases, time) = compress_subproof cases
+            in (Prove (qs, l, t, Case_Split (cases, facts)), time) end
+          | compress (Prove (qs, l, t, Subblock proof)) =
+            let val ([proof], time) = compress_subproof [proof]
+            in (Prove (qs, l, t, Subblock proof), time) end
+          | compress step = (step, zero_preplay_time)
+      in
+        compress_each_and_collect_time compress proof
+      end
+  in
+    do_proof true ctxt proof
+    |> apsnd (pair (metis_fail ()))
+  end
+
+end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Feb 14 22:49:22 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Feb 14 22:49:22 2013 +0100
@@ -95,7 +95,7 @@
    ("max_mono_iters", "smart"),
    ("max_new_mono_instances", "smart"),
    ("isar_proofs", "false"),
-   ("isar_shrink", "10"),
+   ("isar_compress", "10"),
    ("slice", "true"),
    ("minimize", "smart"),
    ("preplay_timeout", "3")]
@@ -119,7 +119,7 @@
 val params_for_minimize =
   ["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans",
    "uncurried_aliases", "max_mono_iters", "max_new_mono_instances",
-   "learn", "isar_proofs", "isar_shrink", "timeout", "preplay_timeout"]
+   "learn", "isar_proofs", "isar_compress", "timeout", "preplay_timeout"]
 
 val property_dependent_params = ["provers", "timeout"]
 
@@ -314,7 +314,7 @@
     val max_new_mono_instances =
       lookup_option lookup_int "max_new_mono_instances"
     val isar_proofs = lookup_bool "isar_proofs"
-    val isar_shrink = Real.max (1.0, lookup_real "isar_shrink")
+    val isar_compress = Real.max (1.0, lookup_real "isar_compress")
     val slice = mode <> Auto_Try andalso lookup_bool "slice"
     val minimize =
       if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
@@ -330,7 +330,7 @@
      learn = learn, fact_filter = fact_filter, max_facts = max_facts,
      fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
-     isar_shrink = isar_shrink, slice = slice, minimize = minimize,
+     isar_compress = isar_compress, slice = slice, minimize = minimize,
      timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
   end
 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Feb 14 22:49:22 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Feb 14 22:49:22 2013 +0100
@@ -54,7 +54,7 @@
 
 fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
                  max_new_mono_instances, type_enc, strict, lam_trans,
-                 uncurried_aliases, isar_proofs, isar_shrink,
+                 uncurried_aliases, isar_proofs, isar_compress,
                  preplay_timeout, ...} : params)
                silent (prover : prover) timeout i n state facts =
   let
@@ -76,7 +76,7 @@
        learn = false, fact_filter = NONE, max_facts = SOME (length facts),
        fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters,
        max_new_mono_instances = max_new_mono_instances,
-       isar_proofs = isar_proofs, isar_shrink = isar_shrink,
+       isar_proofs = isar_proofs, isar_compress = isar_compress,
        slice = false, minimize = SOME false, timeout = timeout,
        preplay_timeout = preplay_timeout, expect = ""}
     val problem =
@@ -243,7 +243,7 @@
         ({debug, verbose, overlord, blocking, provers, type_enc, strict,
          lam_trans, uncurried_aliases, learn, fact_filter, max_facts,
          fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proofs,
-         isar_shrink, slice, minimize, timeout, preplay_timeout, expect}
+         isar_compress, slice, minimize, timeout, preplay_timeout, expect}
          : params) =
   let
     fun lookup_override name default_value =
@@ -261,7 +261,7 @@
      learn = learn, fact_filter = fact_filter, max_facts = max_facts,
      fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
-     isar_shrink = isar_shrink, slice = slice, minimize = minimize,
+     isar_compress = isar_compress, slice = slice, minimize = minimize,
      timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
   end
 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Thu Feb 14 22:49:22 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Thu Feb 14 22:49:22 2013 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_shrink.ML
+(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
     Author:     Jasmin Blanchette, TU Muenchen
     Author:     Steffen Juilf Smolka, TU Muenchen
 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Feb 14 22:49:22 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Feb 14 22:49:22 2013 +0100
@@ -35,7 +35,7 @@
      max_mono_iters : int option,
      max_new_mono_instances : int option,
      isar_proofs : bool,
-     isar_shrink : real,
+     isar_compress : real,
      slice : bool,
      minimize : bool option,
      timeout : Time.time option,
@@ -322,7 +322,7 @@
    max_mono_iters : int option,
    max_new_mono_instances : int option,
    isar_proofs : bool,
-   isar_shrink : real,
+   isar_compress : real,
    slice : bool,
    minimize : bool option,
    timeout : Time.time option,
@@ -635,7 +635,7 @@
           best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config)
         (params as {debug, verbose, overlord, type_enc, strict, lam_trans,
                     uncurried_aliases, fact_filter, max_facts, max_mono_iters,
-                    max_new_mono_instances, isar_proofs, isar_shrink,
+                    max_new_mono_instances, isar_proofs, isar_compress,
                     slice, timeout, preplay_timeout, ...})
         minimize_command
         ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
@@ -898,7 +898,7 @@
                   else
                     ()
                 val isar_params =
-                  (debug, verbose, preplay_timeout, isar_shrink,
+                  (debug, verbose, preplay_timeout, isar_compress,
                    pool, fact_names, sym_tab, atp_proof, goal)
                 val one_line_params =
                   (preplay, proof_banner mode name, used_facts,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Feb 14 22:49:22 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Feb 14 22:49:22 2013 +0100
@@ -54,7 +54,7 @@
 open Sledgehammer_Util
 open Sledgehammer_Proof
 open Sledgehammer_Annotate
-open Sledgehammer_Shrink
+open Sledgehammer_Compress
 
 structure String_Redirect = ATP_Proof_Redirect(
   type key = step_name
@@ -639,7 +639,7 @@
   * (string * stature) list vector * int Symtab.table * string proof * thm
 
 fun isar_proof_text ctxt isar_proofs
-    (debug, verbose, preplay_timeout, isar_shrink, pool, fact_names, sym_tab,
+    (debug, verbose, preplay_timeout, isar_compress, pool, fact_names, sym_tab,
      atp_proof, goal)
     (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
   let
@@ -757,12 +757,12 @@
           |> redirect_graph axioms tainted bot
           |> map (isar_step_of_direct_inf true)
           |> append assms
-          |> (if not preplay andalso isar_shrink <= 1.0 then
+          |> (if not preplay andalso isar_compress <= 1.0 then
                 rpair (false, (true, seconds 0.0))
               else
-                shrink_proof debug ctxt type_enc lam_trans preplay
+                compress_proof debug ctxt type_enc lam_trans preplay
                   preplay_timeout
-                  (if isar_proofs then isar_shrink else 1000.0))
+                  (if isar_proofs then isar_compress else 1000.0))
        (* |>> reorder_proof_to_minimize_jumps (* ? *) *)
           |>> chain_direct_proof
           |>> kill_useless_labels_in_proof
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Thu Feb 14 22:49:22 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,252 +0,0 @@
-(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_shrink.ML
-    Author:     Jasmin Blanchette, TU Muenchen
-    Author:     Steffen Juilf Smolka, TU Muenchen
-
-Shrinking of reconstructed isar proofs.
-*)
-
-signature SLEDGEHAMMER_SHRINK =
-sig
-  type isar_step = Sledgehammer_Proof.isar_step
-  type preplay_time = Sledgehammer_Preplay.preplay_time
-  val shrink_proof :
-    bool -> Proof.context -> string -> string -> bool -> Time.time option
-    -> real -> isar_step list -> isar_step list * (bool * preplay_time)
-end
-
-structure Sledgehammer_Shrink : SLEDGEHAMMER_SHRINK =
-struct
-
-open Sledgehammer_Util
-open Sledgehammer_Proof
-open Sledgehammer_Preplay
-
-(* Parameters *)
-val merge_timeout_slack = 1.2
-
-(* Data structures, orders *)
-val label_ord = prod_ord int_ord fast_string_ord o pairself swap
-structure Label_Table = Table(
-  type key = label
-  val ord = label_ord)
-
-(* clean vector interface *)
-fun get i v = Vector.sub (v, i)
-fun replace x i v = Vector.update (v, i, x)
-fun update f i v = replace (get i v |> f) i v
-fun v_map_index f v = Vector.foldr (op::) nil v |> map_index f |> Vector.fromList
-fun v_fold_index f v s =
-  Vector.foldl (fn (x, (i, s)) => (i+1, f (i, x) s)) (0, s) v |> snd
-
-(* Queue interface to table *)
-fun pop tab key =
-  let val v = hd (Inttab.lookup_list tab key) in
-    (v, Inttab.remove_list (op =) (key, v) tab)
-  end
-fun pop_max tab = pop tab (the (Inttab.max_key tab))
-fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab
-
-(* Main function for shrinking proofs *)
-fun shrink_proof debug ctxt type_enc lam_trans preplay preplay_timeout
-                 isar_shrink proof =
-  let
-    (* 60 seconds seems like a good interpreation of "no timeout" *)
-    val preplay_timeout = preplay_timeout |> the_default (seconds 60.0)
-
-    (* handle metis preplay fail *)
-    local
-      open Unsynchronized
-      val metis_fail = ref false
-    in
-      fun handle_metis_fail try_metis () =
-        try_metis () handle exn =>
-          (if Exn.is_interrupt exn orelse debug then reraise exn
-           else metis_fail := true; some_preplay_time)
-      fun get_time lazy_time =
-        if !metis_fail andalso not (Lazy.is_finished lazy_time)
-          then some_preplay_time
-          else Lazy.force lazy_time
-      val metis_fail = fn () => !metis_fail
-    end
-
-    (* Shrink proof on top level - do not shrink case splits *)
-    fun shrink_top_level on_top_level ctxt proof =
-    let
-      (* proof vector *)
-      val proof_vect = proof |> map SOME |> Vector.fromList
-      val n = Vector.length proof_vect
-      val n_metis = metis_steps_top_level proof
-      val target_n_metis = Real.fromInt n_metis / isar_shrink |> Real.round
-
-      (* table for mapping from (top-level-)label to proof position *)
-      fun update_table (i, Assume (l, _)) = Label_Table.update_new (l, i)
-        | update_table (i, Obtain (_, _, l, _, _)) = Label_Table.update_new (l, i)
-        | update_table (i, Prove (_, l, _, _)) = Label_Table.update_new (l, i)
-        | update_table _ = I
-      val label_index_table = fold_index update_table proof Label_Table.empty
-      val lookup_indices = map_filter (Label_Table.lookup label_index_table)
-
-      (* proof references *)
-      fun refs (Obtain (_, _, _, _, By_Metis (lfs, _))) = lookup_indices lfs
-        | refs (Prove (_, _, _, By_Metis (lfs, _))) = lookup_indices lfs
-        | refs (Prove (_, _, _, Case_Split (cases, (lfs, _)))) =
-          lookup_indices lfs @ maps (maps refs) cases
-        | refs (Prove (_, _, _, Subblock proof)) = maps refs proof
-        | refs _ = []
-      val refed_by_vect =
-        Vector.tabulate (n, (fn _ => []))
-        |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) proof
-        |> Vector.map rev (* after rev, indices are sorted in ascending order *)
-
-      (* candidates for elimination, use table as priority queue (greedy
-         algorithm) *)
-      fun add_if_cand proof_vect (i, [j]) =
-          (case (the (get i proof_vect), the (get j proof_vect)) of
-            (Prove (_, _, t, By_Metis _), Prove (_, _, _, By_Metis _)) =>
-              cons (Term.size_of_term t, i)
-          | (Prove (_, _, t, By_Metis _), Obtain (_, _, _, _, By_Metis _)) =>
-              cons (Term.size_of_term t, i)
-          | _ => I)
-        | add_if_cand _ _ = I
-      val cand_tab =
-        v_fold_index (add_if_cand proof_vect) refed_by_vect []
-        |> Inttab.make_list
-
-      (* cache metis preplay times in lazy time vector *)
-      val metis_time =
-        v_map_index
-          (if not preplay then K (zero_preplay_time) #> Lazy.value
-           else
-             apsnd the (* step *)
-             #> apfst (fn i => try (get (i-1) #> the) proof_vect) (* succedent *)
-             #> try_metis debug type_enc lam_trans ctxt preplay_timeout
-             #> handle_metis_fail
-             #> Lazy.lazy)
-          proof_vect
-
-      fun sum_up_time lazy_time_vector =
-        Vector.foldl
-          (apfst get_time #> uncurry add_preplay_time)
-          zero_preplay_time lazy_time_vector
-
-      (* Merging *)
-      fun merge (Prove (_, label1, _, By_Metis (lfs1, gfs1))) step2 =
-          let
-            val (step_constructor, lfs2, gfs2) =
-              (case step2 of
-                (Prove (qs2, label2, t, By_Metis (lfs2, gfs2))) =>
-                  (fn by => Prove (qs2, label2, t, by), lfs2, gfs2)
-              | (Obtain (qs2, xs, label2, t, By_Metis (lfs2, gfs2))) =>
-                  (fn by => Obtain (qs2, xs, label2, t, by), lfs2, gfs2)
-              | _ => error "sledgehammer_shrink: unmergeable Isar steps" )
-            val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1
-            val gfs = union (op =) gfs1 gfs2
-          in step_constructor (By_Metis (lfs, gfs)) end
-        | merge _ _ = error "sledgehammer_shrink: unmergeable Isar steps"
-
-      fun try_merge metis_time (s1, i) (s2, j) =
-        if not preplay then (merge s1 s2 |> SOME, metis_time)
-        else
-          (case get i metis_time |> Lazy.force of
-            (true, _) => (NONE, metis_time)
-          | (_, t1) =>
-            (case get j metis_time |> Lazy.force of
-              (true, _) => (NONE, metis_time)
-            | (_, t2) =>
-              let
-                val s12 = merge s1 s2
-                val timeout = time_mult merge_timeout_slack (Time.+(t1, t2))
-              in
-                case try_metis_quietly debug type_enc lam_trans ctxt timeout
-                (NONE, s12) () of
-                  (true, _) => (NONE, metis_time)
-                | exact_time =>
-                  (SOME s12, metis_time
-                             |> replace (zero_preplay_time |> Lazy.value) i
-                             |> replace (Lazy.value exact_time) j)
-
-              end))
-
-      fun merge_steps metis_time proof_vect refed_by cand_tab n' n_metis' =
-        if Inttab.is_empty cand_tab
-          orelse n_metis' <= target_n_metis
-          orelse (on_top_level andalso n'<3)
-        then
-          (Vector.foldr
-             (fn (NONE, proof) => proof | (SOME s, proof) => s :: proof)
-             [] proof_vect,
-           sum_up_time metis_time)
-        else
-          let
-            val (i, cand_tab) = pop_max cand_tab
-            val j = get i refed_by |> the_single
-            val s1 = get i proof_vect |> the
-            val s2 = get j proof_vect |> the
-          in
-            case try_merge metis_time (s1, i) (s2, j) of
-              (NONE, metis_time) =>
-              merge_steps metis_time proof_vect refed_by cand_tab n' n_metis'
-            | (s, metis_time) =>
-            let
-              val refs = refs s1
-              val refed_by = refed_by |> fold
-                (update (Ord_List.remove int_ord i #> Ord_List.insert int_ord j)) refs
-              val new_candidates =
-                fold (add_if_cand proof_vect)
-                  (map (fn i => (i, get i refed_by)) refs) []
-              val cand_tab = add_list cand_tab new_candidates
-              val proof_vect = proof_vect |> replace NONE i |> replace s j
-            in
-              merge_steps metis_time proof_vect refed_by cand_tab (n' - 1)
-                          (n_metis' - 1)
-            end
-          end
-    in
-      merge_steps metis_time proof_vect refed_by_vect cand_tab n n_metis
-    end
-
-    fun do_proof on_top_level ctxt proof =
-      let
-        (* Enrich context with top-level facts *)
-        val thy = Proof_Context.theory_of ctxt
-        (* TODO: add Skolem variables to context? *)
-        fun enrich_with_fact l t =
-          Proof_Context.put_thms false
-            (string_for_label l, SOME [Skip_Proof.make_thm thy t])
-        fun enrich_with_step (Assume (l, t)) = enrich_with_fact l t
-          | enrich_with_step (Obtain (_, _, l, t, _)) = enrich_with_fact l t
-          | enrich_with_step (Prove (_, l, t, _)) = enrich_with_fact l t
-          | enrich_with_step _ = I
-        val rich_ctxt = fold enrich_with_step proof ctxt
-
-        (* Shrink subproofs (case_splits and subblocks) and top-levl *)
-        val ((proof, top_level_time), lower_level_time) =
-          proof |> do_subproof rich_ctxt
-                |>> shrink_top_level on_top_level rich_ctxt
-      in
-        (proof, add_preplay_time lower_level_time top_level_time)
-      end
-
-    and do_subproof ctxt proof =
-      let
-        fun shrink_each_and_collect_time shrink candidates =
-          let fun f_m cand time = shrink cand ||> add_preplay_time time
-          in fold_map f_m candidates zero_preplay_time end
-        val shrink_subproof =
-          shrink_each_and_collect_time (do_proof false ctxt)
-        fun shrink (Prove (qs, l, t, Case_Split (cases, facts))) =
-            let val (cases, time) = shrink_subproof cases
-            in (Prove (qs, l, t, Case_Split (cases, facts)), time) end
-          | shrink (Prove (qs, l, t, Subblock proof)) =
-            let val ([proof], time) = shrink_subproof [proof]
-            in (Prove (qs, l, t, Subblock proof), time) end
-          | shrink step = (step, zero_preplay_time)
-      in
-        shrink_each_and_collect_time shrink proof
-      end
-  in
-    do_proof true ctxt proof
-    |> apsnd (pair (metis_fail ()))
-  end
-
-end