# HG changeset patch
# User blanchet
# Date 1272361441 -7200
# Node ID fe9b37503db33aa6cb25c5b46c76009941d0a33f
# Parent  8a5c99a1c965f65b9549abf1bf1646b8d7deb66d
honor "shrink_proof" Sledgehammer option

diff -r 8a5c99a1c965 -r fe9b37503db3 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Apr 27 11:24:47 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Apr 27 11:44:01 2010 +0200
@@ -405,12 +405,13 @@
 fun bad_free (Free (a,_)) = String.isPrefix skolem_prefix a
   | bad_free _ = false;
 
-fun add_desired_line ctxt (num, t, []) (j, lines) =
+fun add_desired_line ctxt _ (num, t, []) (j, lines) =
     (j, (num, t, []) :: lines)  (* conjecture clauses must be kept *)
-  | add_desired_line ctxt (num, t, deps) (j, lines) =
+  | add_desired_line ctxt shrink_factor (num, t, deps) (j, lines) =
     (j + 1,
      if eq_types t orelse not (null (Term.add_tvars t [])) orelse
-        exists_subterm bad_free t orelse length deps < 2 then
+        exists_subterm bad_free t orelse
+        (length deps < 2 orelse j mod shrink_factor <> 0) then
        map (replace_deps (num, deps)) lines  (* delete line *)
      else
        (num, t, deps) :: lines)
@@ -540,7 +541,7 @@
       str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
 val strip_spaces = strip_spaces_in_list o String.explode
 
-fun proof_from_atp_proof pool ctxt atp_proof thm_names frees =
+fun proof_from_atp_proof pool ctxt shrink_factor atp_proof thm_names frees =
   let
     val tuples =
       atp_proof |> split_lines |> map strip_spaces
@@ -549,7 +550,8 @@
                 |> decode_lines ctxt
     val tuples = fold_rev (add_line thm_names) tuples []
     val tuples = fold_rev add_nonnull_line tuples []
-    val tuples = fold_rev (add_desired_line ctxt) tuples (0, []) |> snd
+    val tuples = fold_rev (add_desired_line ctxt shrink_factor) tuples (0, [])
+                 |> snd
   in
     (if null frees then [] else [Fix frees]) @
     map2 step_for_tuple (length tuples downto 1) tuples
@@ -714,9 +716,6 @@
     and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
   in do_proof end
 
-(* FIXME: implement *)
-fun shrink_proof shrink_factor proof = proof
-
 val then_chain_proof =
   let
     fun aux _ [] = []
@@ -845,10 +844,10 @@
     val (one_line_proof, lemma_names) =
       metis_proof_text (minimize_command, atp_proof, thm_names, goal, i)
     fun isar_proof_for () =
-      case proof_from_atp_proof pool ctxt atp_proof thm_names frees
+      case proof_from_atp_proof pool ctxt shrink_factor atp_proof thm_names
+                                frees
            |> direct_proof thy conjecture_shape hyp_ts concl_t
            |> kill_duplicate_assumptions_in_proof
-           |> shrink_proof shrink_factor
            |> then_chain_proof
            |> kill_useless_labels_in_proof
            |> relabel_proof