# HG changeset patch
# User blanchet
# Date 1386660257 -28800
# Node ID cbebe2cf77f135b886b0aa48d246dfc318fdbe67
# Parent  15a642b9ffacc0226e76234f40f3b12e6472fde1
more work on Z3 Isar proofs

diff -r 15a642b9ffac -r cbebe2cf77f1 src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Mon Dec 09 23:22:44 2013 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Tue Dec 10 15:24:17 2013 +0800
@@ -3,10 +3,7 @@
     Author:     Steffen Juilf Smolka, TU Muenchen
 
 Compression of isar proofs by merging steps.
-Only proof steps using the MetisM proof_method are merged.
-
-PRE CONDITION: the proof must be labeled canocially, see
-Slegehammer_Proof.relabel_proof_canonically
+Only proof steps using the same proof method are merged.
 *)
 
 signature SLEDGEHAMMER_COMPRESS =
@@ -24,35 +21,26 @@
 open Sledgehammer_Proof
 open Sledgehammer_Preplay
 
-
-(*** util ***)
-
 (* traverses steps in post-order and collects the steps with the given labels *)
 fun collect_successors steps lbls =
   let
     fun do_steps _ ([], accu) = ([], accu)
-      | do_steps [] (lbls, accu) = (lbls, accu)
-      | do_steps (step::steps) (lbls, accu) =
-          do_steps steps (do_step step (lbls, accu))
-
+      | do_steps [] accum = accum
+      | do_steps (step :: steps) accum = do_steps steps (do_step step accum)
     and do_step (Let _) x = x
       | do_step (step as Prove (_, _, l, _, subproofs, _)) x =
         (case do_subproofs subproofs x of
           ([], accu) => ([], accu)
-        | (lbls as l'::lbls', accu) =>
-            if l=l'
-              then (lbls', step::accu)
-              else (lbls, accu))
-
+        | accum as (l' :: lbls', accu) => if l = l' then (lbls', step :: accu) else accum)
     and do_subproofs [] x = x
-      | do_subproofs (proof::subproofs) x =
-          (case do_steps (steps_of_proof proof) x of
-            ([], accu) => ([], accu)
-          | x => do_subproofs subproofs x)
+      | do_subproofs (proof :: subproofs) x =
+        (case do_steps (steps_of_proof proof) x of
+          accum as ([], _) => accum
+        | accum => do_subproofs subproofs accum)
   in
-    case do_steps steps (lbls, []) of
+    (case do_steps steps (lbls, []) of
       ([], succs) => rev succs
-    | _ => raise Fail "Sledgehammer_Compress: collect_successors"
+    | _ => raise Fail "Sledgehammer_Compress: collect_successors")
   end
 
 (* traverses steps in reverse post-order and inserts the given updates *)
@@ -60,130 +48,104 @@
   let
     fun do_steps [] updates = ([], updates)
       | do_steps steps [] = (steps, [])
-      | do_steps (step::steps) updates =
-          do_step step (do_steps steps updates)
-
-    and do_step step (steps, []) = (step::steps, [])
-      | do_step (step as Let _) (steps, updates) = (step::steps, updates)
+      | do_steps (step :: steps) updates = do_step step (do_steps steps updates)
+    and do_step step (steps, []) = (step :: steps, [])
+      | do_step (step as Let _) (steps, updates) = (step :: steps, updates)
       | do_step (Prove (qs, xs, l, t, subproofs, by))
-          (steps, updates as
-           Prove(qs', xs', l', t', subproofs', by') :: updates') =
-          let
-            val (subproofs, updates) =
-              if l=l'
-                then do_subproofs subproofs' updates'
-                else do_subproofs subproofs updates
-          in
-            if l=l'
-              then (Prove (qs', xs', l', t', subproofs, by') :: steps,
-                    updates)
-              else (Prove (qs, xs, l, t, subproofs, by) :: steps,
-                    updates)
-          end
-      | do_step _ _ =
-          raise Fail "Sledgehammer_Compress: update_steps (invalid update)"
-
+          (steps, updates as Prove (qs', xs', l', t', subproofs', by') :: updates') =
+        let
+          val (subproofs, updates) =
+            if l = l' then do_subproofs subproofs' updates' else do_subproofs subproofs updates
+        in
+          if l = l' then (Prove (qs', xs', l', t', subproofs, by') :: steps, updates)
+          else (Prove (qs, xs, l, t, subproofs, by) :: steps, updates)
+        end
+      | do_step _ _ = raise Fail "Sledgehammer_Compress: update_steps (invalid update)"
     and do_subproofs [] updates = ([], updates)
       | do_subproofs steps [] = (steps, [])
-      | do_subproofs (proof::subproofs) updates =
-          do_proof proof (do_subproofs subproofs updates)
-
+      | do_subproofs (proof :: subproofs) updates =
+        do_proof proof (do_subproofs subproofs updates)
     and do_proof proof (proofs, []) = (proof :: proofs, [])
       | do_proof (Proof (fix, assms, steps)) (proofs, updates) =
-          let val (steps, updates) = do_steps steps updates in
-            (Proof (fix, assms, steps) :: proofs, updates)
-          end
+        let val (steps, updates) = do_steps steps updates in
+          (Proof (fix, assms, steps) :: proofs, updates)
+        end
   in
-    case do_steps steps (rev updates) of
+    (case do_steps steps (rev updates) of
       (steps, []) => steps
-    | _ => raise Fail "Sledgehammer_Compress: update_steps"
+    | _ => raise Fail "Sledgehammer_Compress: update_steps")
   end
 
 (* tries merging the first step into the second step *)
-fun try_merge
-  (Prove (_, [], lbl1, _, [], ((lfs1, gfs1), MetisM)))
-  (Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), MetisM))) =
+fun try_merge (Prove (_, [], lbl1, _, [], ((lfs1, gfs1), meth1)))
+      (Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), meth2))) =
+    if meth1 = meth2 then
       let
         val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1
         val gfs = union (op =) gfs1 gfs2
       in
-        SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), MetisM)))
+        SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), meth1)))
       end
+    else
+      NONE
   | try_merge _ _ = NONE
 
-
-
-(*** main function ***)
-
 val compress_degree = 2
 val merge_timeout_slack = 1.2
 
-(* PRE CONDITION: the proof must be labeled canocially, see
-   Slegehammer_Proof.relabel_proof_canonically *)
+(* Precondition: The proof must be labeled canonically
+   (cf. "Slegehammer_Proof.relabel_proof_canonically"). *)
 fun compress_proof isar_compress
-        ({get_preplay_time, set_preplay_time, preplay_quietly, ...}
-         : preplay_interface)
-  proof =
+    ({get_preplay_time, set_preplay_time, preplay_quietly, ...} : preplay_interface) proof =
   if isar_compress <= 1.0 then
     proof
   else
-  let
-    val (compress_further : unit -> bool,
-         decrement_step_count : unit -> unit) =
-      let
-        val number_of_steps = add_proof_steps (steps_of_proof proof) 0
-        val target_number_of_steps =
-          Real.fromInt number_of_steps / isar_compress
-          |> Real.round
-          |> curry Int.max 2 (* don't produce one-step isar proofs *)
-        val delta =
-          number_of_steps - target_number_of_steps |> Unsynchronized.ref
-      in
-        (fn () => !delta > 0,
-         fn () => delta := !delta - 1)
-      end
+    let
+      val (compress_further, decrement_step_count) =
+        let
+          val number_of_steps = add_proof_steps (steps_of_proof proof) 0
+          val target_number_of_steps = Real.round (Real.fromInt number_of_steps / isar_compress)
+          val delta = Unsynchronized.ref (number_of_steps - target_number_of_steps)
+        in
+          (fn () => !delta > 0, fn () => delta := !delta - 1)
+        end
 
-
-    val (get_successors : label -> label list,
-         replace_successor: label -> label list -> label -> unit) =
-      let
-        fun add_refs (Let _) tab = tab
-          | add_refs (Prove (_, _, v, _, _, ((lfs, _), _))) tab =
-              fold (fn key => Canonical_Lbl_Tab.cons_list (key, v)) lfs tab
+      val (get_successors, replace_successor) =
+        let
+          fun add_refs (Let _) = I
+            | add_refs (Prove (_, _, v, _, _, ((lfs, _), _))) =
+              fold (fn key => Canonical_Lbl_Tab.cons_list (key, v)) lfs
 
-        val tab =
-          Canonical_Lbl_Tab.empty
-          |> fold_isar_steps add_refs (steps_of_proof proof)
-          (* rev should have the same effect as sort canonical_label_ord *)
-          |> Canonical_Lbl_Tab.map (K rev)
-          |> Unsynchronized.ref
-
-        fun get_successors l = Canonical_Lbl_Tab.lookup_list (!tab) l
-        fun set_successors l refs =
-          tab := Canonical_Lbl_Tab.update (l, refs) (!tab)
-        fun replace_successor old new dest =
-          set_successors dest
-            (get_successors dest |> Ord_List.remove canonical_label_ord old
-                                |> Ord_List.union canonical_label_ord new)
+          val tab =
+            Canonical_Lbl_Tab.empty
+            |> fold_isar_steps add_refs (steps_of_proof proof)
+            (* "rev" should have the same effect as "sort canonical_label_ord" *)
+            |> Canonical_Lbl_Tab.map (K rev)
+            |> Unsynchronized.ref
 
-      in
-         (get_successors, replace_successor)
-      end
-
-
-
-    (** elimination of trivial, one-step subproofs **)
+          fun get_successors l = Canonical_Lbl_Tab.lookup_list (!tab) l
+          fun set_successors l refs = tab := Canonical_Lbl_Tab.update (l, refs) (!tab)
+          fun replace_successor old new dest =
+            get_successors dest
+            |> Ord_List.remove canonical_label_ord old
+            |> Ord_List.union canonical_label_ord new
+            |> set_successors dest
+        in
+          (get_successors, replace_successor)
+        end
 
-    fun elim_subproofs' time qs fix l t lfs gfs subs nontriv_subs =
-      if null subs orelse not (compress_further ()) then
-        (set_preplay_time l (false, time);
-         Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), MetisM)))
-      else
-        case subs of
-          ((sub as Proof (_, assms, sub_steps)) :: subs) =>
+      (** elimination of trivial, one-step subproofs **)
+
+      fun elim_subproofs' time qs fix l t lfs gfs meth subs nontriv_subs =
+        if null subs orelse not (compress_further ()) then
+          (set_preplay_time l (false, time);
+           Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), meth)))
+        else
+          (case subs of
+            (sub as Proof (_, assms, sub_steps)) :: subs =>
             (let
               (* trivial subproofs have exactly one Prove step *)
-              val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), MetisM))) = try the_single sub_steps
+              val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), _))) = try the_single sub_steps
 
               (* only touch proofs that can be preplayed sucessfully *)
               val (false, time') = get_preplay_time l'
@@ -194,7 +156,7 @@
                 subtract (op =) (map fst assms) lfs'
                 |> union (op =) lfs
               val gfs'' = union (op =) gfs' gfs
-              val by = ((lfs'', gfs''), MetisM)
+              val by = ((lfs'', gfs''), meth)
               val step'' = Prove (qs, fix, l, t, subs'', by)
 
               (* check if the modified step can be preplayed fast enough *)
@@ -204,165 +166,135 @@
             in
               decrement_step_count (); (* l' successfully eliminated! *)
               map (replace_successor l' [l]) lfs';
-              elim_subproofs' time'' qs fix l t lfs'' gfs'' subs nontriv_subs
+              elim_subproofs' time'' qs fix l t lfs'' gfs'' meth subs nontriv_subs
             end
             handle Bind =>
-              elim_subproofs' time qs fix l t lfs gfs subs (sub::nontriv_subs))
-        | _ => raise Fail "Sledgehammer_Compress: elim_subproofs'"
-
+              elim_subproofs' time qs fix l t lfs gfs meth subs (sub :: nontriv_subs))
+          | _ => raise Fail "Sledgehammer_Compress: elim_subproofs'")
 
-    fun elim_subproofs (step as Let _) = step
-      | elim_subproofs
-        (step as Prove (qs, fix, l, t, subproofs, ((lfs, gfs), MetisM))) =
-          if subproofs = [] then step else
-            case get_preplay_time l of
-              (true, _) => step (* timeout or fail *)
-            | (false, time) =>
-                elim_subproofs' time qs fix l t lfs gfs subproofs []
-
-
+      fun elim_subproofs (step as Let _) = step
+        | elim_subproofs
+          (step as Prove (qs, fix, l, t, subproofs, ((lfs, gfs), meth))) =
+            if subproofs = [] then step else
+              case get_preplay_time l of
+                (true, _) => step (* timeout or fail *)
+              | (false, time) =>
+                  elim_subproofs' time qs fix l t lfs gfs meth subproofs []
 
-    (** top_level compression: eliminate steps by merging them into their
-        successors **)
-
-    fun compress_top_level steps =
-      let
+      (** top_level compression: eliminate steps by merging them into their
+          successors **)
 
-        (* #successors, (size_of_term t, position) *)
-        fun cand_key (i, l, t_size) =
-          (get_successors l |> length, (t_size, i))
+      fun compress_top_level steps =
+        let
+          (* (#successors, (size_of_term t, position)) *)
+          fun cand_key (i, l, t_size) = (get_successors l |> length, (t_size, i))
 
-        val compression_ord =
-          prod_ord int_ord (prod_ord (int_ord #> rev_order) int_ord)
-          #> rev_order
+          val compression_ord =
+            prod_ord int_ord (prod_ord (int_ord #> rev_order) int_ord)
+            #> rev_order
 
-        val cand_ord = pairself cand_key #> compression_ord
+          val cand_ord = pairself cand_key #> compression_ord
 
-        fun pop_next_cand candidates =
-          case max_list cand_ord candidates of
-            NONE => (NONE, [])
-          | cand as SOME (i, _, _) =>
-              (cand, filter_out (fn (j, _, _) => j=i) candidates)
+          fun pop_next_cand candidates =
+            (case max_list cand_ord candidates of
+              NONE => (NONE, [])
+            | cand as SOME (i, _, _) => (cand, filter_out (fn (j, _, _) => j = i) candidates))
 
-        val candidates =
-          let
-            fun add_cand (_, Let _) = I
-              | add_cand (i, Prove (_, _, l, t, _, _)) =
-                  cons (i, l, size_of_term t)
-          in
-            (steps
-            |> split_last |> fst (* last step must NOT be eliminated *)
-            |> fold_index add_cand) []
-          end
+          val candidates =
+            let
+              fun add_cand (_, Let _) = I
+                | add_cand (i, Prove (_, _, l, t, _, _)) = cons (i, l, size_of_term t)
+            in
+              (steps
+              |> split_last |> fst (* keep last step *)
+              |> fold_index add_cand) []
+            end
 
-        fun try_eliminate (i, l, _) succ_lbls steps =
-          let
-            (* only touch steps that can be preplayed successfully *)
-            val (false, time) = get_preplay_time l
-
-            val succ_times =
-              map (get_preplay_time #> (fn (false, t) => t)) succ_lbls
-
-            val timeslice =
-              time_mult (1.0 / (Real.fromInt (length succ_lbls))) time
+          fun try_eliminate (i, l, _) succ_lbls steps =
+            let
+              (* only touch steps that can be preplayed successfully *)
+              val (false, time) = get_preplay_time l
 
-            val timeouts =
-              map (curry Time.+ timeslice #> time_mult merge_timeout_slack)
-                succ_times
+              val succ_times = map (get_preplay_time #> (fn (false, t) => t)) succ_lbls
+              val timeslice = time_mult (1.0 / (Real.fromInt (length succ_lbls))) time
+              val timeouts =
+                map (curry Time.+ timeslice #> time_mult merge_timeout_slack) succ_times
 
-            val ((cand as Prove (_, _, l, _, _, ((lfs, _), MetisM))) :: steps') = drop i steps
+              val ((cand as Prove (_, _, l, _, _, ((lfs, _), _))) :: steps') = drop i steps
 
-            (* FIXME: debugging *)
-            val _ = (if (label_of_step cand |> the) <> l then
-                      raise Fail "Sledgehammer_Compress: try_eliminate"
-                    else ())
-
-            val succs = collect_successors steps' succ_lbls
-            val succs' = map (try_merge cand #> the) succs
+              (* FIXME: debugging *)
+              val _ =
+                if the (label_of_step cand) <> l then
+                  raise Fail "Sledgehammer_Compress: try_eliminate"
+                else
+                  ()
 
-            (* TODO: should be lazy: stop preplaying as soon as one step
-               fails/times out *)
-            val preplay_times =
-              map (uncurry preplay_quietly) (timeouts ~~ succs')
+              val succs = collect_successors steps' succ_lbls
+              val succs' = map (try_merge cand #> the) succs
 
-            (* ensure none of the modified successors timed out *)
-            val false = List.exists fst preplay_times
+              (* TODO: should be lazy: stop preplaying as soon as one step
+                 fails/times out *)
+              val preplay_times = map2 preplay_quietly timeouts succs'
 
-            val (steps1, _::steps2) = chop i steps
+              (* ensure none of the modified successors timed out *)
+              val false = List.exists fst preplay_times
 
-            (* replace successors with their modified versions *)
-            val steps2 = update_steps steps2 succs'
-
-          in
-            decrement_step_count (); (* candidate successfully eliminated *)
-            map (uncurry set_preplay_time) (succ_lbls ~~ preplay_times);
-            map (replace_successor l succ_lbls) lfs;
-            (* removing the step would mess up the indices
-               -> replace with dummy step instead *)
-            steps1 @ dummy_isar_step :: steps2
-          end
-          handle Bind => steps
-               | Match => steps
-               | Option.Option => steps
+              val (steps1, _ :: steps2) = chop i steps
+              (* replace successors with their modified versions *)
+              val steps2 = update_steps steps2 succs'
+            in
+              decrement_step_count (); (* candidate successfully eliminated *)
+              map2 set_preplay_time succ_lbls preplay_times;
+              map (replace_successor l succ_lbls) lfs;
+              (* removing the step would mess up the indices
+                 -> replace with dummy step instead *)
+              steps1 @ dummy_isar_step :: steps2
+            end
+            handle Bind => steps
+                 | Match => steps
+                 | Option.Option => steps
 
-        fun compression_loop candidates steps =
-          if not (compress_further ()) then
-            steps
-          else
-            case pop_next_cand candidates of
-              (NONE, _) => steps (* no more candidates for elimination *)
-            | (SOME (cand as (_, l, _)), candidates) =>
-              let
-                val successors = get_successors l
-              in
-                if length successors > compress_degree
-                  then steps
-                  else compression_loop candidates
-                         (try_eliminate cand successors steps)
-              end
-
-
-      in
-        compression_loop candidates steps
-        |> filter_out (fn step => step = dummy_isar_step)
-      end
-
-
+          fun compression_loop candidates steps =
+            if not (compress_further ()) then
+              steps
+            else
+              (case pop_next_cand candidates of
+                (NONE, _) => steps (* no more candidates for elimination *)
+              | (SOME (cand as (_, l, _)), candidates) =>
+                let val successors = get_successors l in
+                  if length successors > compress_degree then steps
+                  else compression_loop candidates (try_eliminate cand successors steps)
+                end)
+        in
+          compression_loop candidates steps
+          |> remove (op =) dummy_isar_step
+        end
 
-    (** recusion over the proof tree **)
-    (*
-       Proofs are compressed bottom-up, beginning with the innermost
-       subproofs.
-       On the innermost proof level, the proof steps have no subproofs.
-       In the best case, these steps can be merged into just one step,
-       resulting in a trivial subproof. Going one level up, trivial subproofs
-       can be eliminated. In the best case, this once again leads to a proof
-       whose proof steps do not have subproofs. Applying this approach
-       recursively will result in a flat proof in the best cast.
-    *)
-
-    infix 1 ?>
-    fun x ?> f = if compress_further () then f x else x
-
-    fun do_proof (proof as (Proof (fix, assms, steps))) =
-      if compress_further ()
-        then Proof (fix, assms, do_steps steps)
-        else proof
-
-    and do_steps steps =
-      (* bottom-up: compress innermost proofs first *)
-      steps |> map (fn step => step ?> do_sub_levels)
-            ?> compress_top_level
-
-    and do_sub_levels (Let x) = Let x
-      | do_sub_levels (Prove (qs, xs, l, t, subproofs, by)) =
+      (** recusion over the proof tree **)
+      (*
+         Proofs are compressed bottom-up, beginning with the innermost
+         subproofs.
+         On the innermost proof level, the proof steps have no subproofs.
+         In the best case, these steps can be merged into just one step,
+         resulting in a trivial subproof. Going one level up, trivial subproofs
+         can be eliminated. In the best case, this once again leads to a proof
+         whose proof steps do not have subproofs. Applying this approach
+         recursively will result in a flat proof in the best cast.
+      *)
+      fun do_proof (proof as (Proof (fix, assms, steps))) =
+        if compress_further () then Proof (fix, assms, do_steps steps) else proof
+      and do_steps steps =
+        (* bottom-up: compress innermost proofs first *)
+        steps |> map (fn step => step |> compress_further () ? do_sub_levels)
+              |> compress_further () ? compress_top_level
+      and do_sub_levels (Let x) = Let x
+        | do_sub_levels (Prove (qs, xs, l, t, subproofs, by)) =
           (* compress subproofs *)
           Prove (qs, xs, l, t, map do_proof subproofs, by)
-            (* eliminate trivial subproofs *)
-            ?> elim_subproofs
-
-  in
-    do_proof proof
-  end
+          (* eliminate trivial subproofs *)
+          |> compress_further () ? elim_subproofs
+    in
+      do_proof proof
+    end
 
 end;
diff -r 15a642b9ffac -r cbebe2cf77f1 src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML	Mon Dec 09 23:22:44 2013 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML	Tue Dec 10 15:24:17 2013 +0800
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML
+    Author:     Steffen Juilf Smolka, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
-    Author:     Steffen Juilf Smolka, TU Muenchen
 
 Minimize dependencies (used facts) of Isar proof steps.
 *)
@@ -8,9 +8,11 @@
 signature SLEDGEHAMMER_MINIMIZE_ISAR =
 sig
   type preplay_interface = Sledgehammer_Preplay.preplay_interface
+  type isar_step = Sledgehammer_Proof.isar_step
   type isar_proof = Sledgehammer_Proof.isar_proof
-  val minimize_dependencies_and_remove_unrefed_steps :
-    bool -> preplay_interface -> isar_proof -> isar_proof
+
+  val min_deps_of_step : preplay_interface -> isar_step -> isar_step
+  val postprocess_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
 end;
 
 structure Sledgehammer_Minimize_Isar : SLEDGEHAMMER_MINIMIZE_ISAR =
@@ -20,49 +22,39 @@
 open Sledgehammer_Proof
 open Sledgehammer_Preplay
 
-val slack = 1.3
+val slack = seconds 0.1
 
 fun min_deps_of_step (_ : preplay_interface) (step as Let _) = step
   | min_deps_of_step {get_preplay_time, set_preplay_time, preplay_quietly, ...}
-      (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), method))) =
-  (case get_preplay_time l of
-    (* don't touch steps that time out or fail; minimizing won't help *)
-    (true, _) => step
-  | (false, time) =>
-    let
-      fun mk_step_lfs_gfs lfs gfs =
-        Prove (qs, xs, l, t, subproofs, ((lfs, gfs), method))
-      val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs)
+      (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) =
+    (case get_preplay_time l of
+      (* don't touch steps that time out or fail; minimizing won't help (not true -- FIXME) *)
+      (true, _) => step
+    | (false, time) =>
+      let
+        fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))
+        val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs)
 
-      fun minimize_facts _ time min_facts [] = (time, min_facts)
-        | minimize_facts mk_step time min_facts (f :: facts) =
-          (case preplay_quietly (time_mult slack time)
-                  (mk_step (min_facts @ facts)) of
-            (true, _) => minimize_facts mk_step time (f :: min_facts) facts
-          | (false, time) => minimize_facts mk_step time min_facts facts)
-
-      val (time, min_lfs) = minimize_facts (mk_step_gfs_lfs gfs) time [] lfs
-      val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
+        fun minimize_facts _ time min_facts [] = (time, min_facts)
+          | minimize_facts mk_step time min_facts (f :: facts) =
+            (case preplay_quietly (Time.+ (time, slack)) (mk_step (min_facts @ facts)) of
+              (true, _) => minimize_facts mk_step time (f :: min_facts) facts
+            | (false, time) => minimize_facts mk_step time min_facts facts)
 
-    in
-      set_preplay_time l (false, time);
-      mk_step_lfs_gfs min_lfs min_gfs
-    end)
+        val (time, min_lfs) = minimize_facts (mk_step_gfs_lfs gfs) time [] lfs
+        val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
+      in
+        set_preplay_time l (false, time); mk_step_lfs_gfs min_lfs min_gfs
+      end)
 
-fun minimize_dependencies_and_remove_unrefed_steps isar_try0 preplay_interface
-        proof =
+fun postprocess_remove_unreferenced_steps postproc_step =
   let
-    fun cons_to xs x = x :: xs
-
     val add_lfs = fold (Ord_List.insert label_ord)
 
     fun do_proof (Proof (fix, assms, steps)) =
-      let
-        val (refed, steps) = do_steps steps
-      in
+      let val (refed, steps) = do_steps steps in
         (refed, Proof (fix, assms, steps))
       end
-
     and do_steps steps =
       let
         (* the last step is always implicitly referenced *)
@@ -72,7 +64,6 @@
       in
         fold_rev do_step steps (refed, [concl])
       end
-
     and do_step step (refed, accu) =
       case label_of_step step of
         NONE => (refed, step :: accu)
@@ -80,15 +71,10 @@
           if Ord_List.member label_ord refed l then
             do_refed_step step
             |>> Ord_List.union label_ord refed
-            ||> cons_to accu
+            ||> (fn x => x :: accu)
           else
             (refed, accu)
-
-    and do_refed_step step =
-      step
-      |> isar_try0 ? min_deps_of_step preplay_interface
-      |> do_refed_step'
-
+    and do_refed_step step = step |> postproc_step |> do_refed_step'
     and do_refed_step' (Let _) = raise Fail "Sledgehammer_Minimize_Isar"
       | do_refed_step' (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))) =
         let
@@ -102,7 +88,7 @@
           (refed, step)
         end
   in
-    snd (do_proof proof)
+    snd o do_proof
   end
 
 end;
diff -r 15a642b9ffac -r cbebe2cf77f1 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Mon Dec 09 23:22:44 2013 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Tue Dec 10 15:24:17 2013 +0800
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
+    Author:     Steffen Juilf Smolka, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
-    Author:     Steffen Juilf Smolka, TU Muenchen
 
 Preplaying of isar proofs.
 *)
@@ -235,7 +235,6 @@
       overall_preplay_stats = K (zero_preplay_time, false)}
   else
     let
-
       (* add local proof facts to context *)
       val ctxt = enrich_context proof ctxt
 
@@ -254,9 +253,9 @@
 
       (* preplay steps treating exceptions like timeouts *)
       fun preplay_quietly timeout step =
-        case preplay true timeout step of
+        (case preplay true timeout step of
           PplSucc preplay_time => preplay_time
-        | PplFail _ => (true, timeout)
+        | PplFail _ => (true, timeout))
 
       val preplay_tab =
         let
@@ -277,9 +276,8 @@
 
       fun get_preplay_result lbl =
         Canonical_Lbl_Tab.lookup (!preplay_tab) lbl |> the |> Lazy.force
-        handle
-          Option.Option =>
-            raise Fail "Sledgehammer_Preplay: preplay time table"
+        handle Option.Option =>
+          raise Fail "Sledgehammer_Preplay: preplay time table"
 
       fun set_preplay_result lbl result =
         preplay_tab :=
@@ -298,20 +296,20 @@
             try (label_of_step #> the #> get_preplay_result) step
             |> the_default (PplSucc zero_preplay_time)
           fun do_step step =
-            case result_of_step step of
+            (case result_of_step step of
               PplSucc preplay_time => apfst (add_preplay_time preplay_time)
-            | PplFail _ => apsnd (K true)
+            | PplFail _ => apsnd (K true))
         in
           fold_isar_steps do_step steps (zero_preplay_time, false)
         end
 
     in
-      { get_preplay_result = get_preplay_result,
-        set_preplay_result = set_preplay_result,
-        get_preplay_time = get_preplay_time,
-        set_preplay_time = set_preplay_time,
-        preplay_quietly = preplay_quietly,
-        overall_preplay_stats = overall_preplay_stats}
+      {get_preplay_result = get_preplay_result,
+       set_preplay_result = set_preplay_result,
+       get_preplay_time = get_preplay_time,
+       set_preplay_time = set_preplay_time,
+       preplay_quietly = preplay_quietly,
+       overall_preplay_stats = overall_preplay_stats}
     end
 
 end;
diff -r 15a642b9ffac -r cbebe2cf77f1 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Dec 09 23:22:44 2013 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Dec 10 15:24:17 2013 +0800
@@ -64,10 +64,8 @@
    clsarity). *)
 fun is_only_type_information t = t aconv @{term True}
 
-fun s_maybe_not role = role <> Conjecture ? s_not
-
 fun is_same_inference (role, t) (_, role', t', _, _) =
-  s_maybe_not role t aconv s_maybe_not role' t'
+  (t |> role = Conjecture ? s_not) aconv (t' |> role' = Conjecture ? s_not)
 
 (* Discard facts; consolidate adjacent lines that prove the same formula, since
    they differ only in type information.*)
@@ -86,11 +84,12 @@
     (* Type information will be deleted later; skip repetition test. *)
     if is_only_type_information t then
       line :: lines
-    (* Is there a repetition? If so, replace later line by earlier one. *)
-    else case take_prefix (not o is_same_inference (role, t)) lines of
-      (_, []) => line :: lines
-    | (pre, (name', _, _, _, _) :: post) =>
-      line :: pre @ map (replace_dependencies_in_line (name', [name])) post
+    else
+      (* Is there a repetition? If so, replace later line by earlier one. *)
+      (case take_prefix (not o is_same_inference (role, t)) lines of
+        (_, []) => line :: lines
+      | (pre, (name', _, _, _, _) :: post) =>
+        line :: pre @ map (replace_dependencies_in_line (name', [name])) post)
 
 (* Recursively delete empty lines (type information) from the proof. *)
 fun add_nontrivial_line (line as (name, _, t, _, [])) lines =
@@ -201,6 +200,7 @@
   in chain_proof end
 
 fun maybe_mk_Trueprop t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
+val maybe_dest_Trueprop = perhaps (try HOLogic.dest_Trueprop)
 
 type isar_params =
   bool * bool * string * string * Time.time option * real * bool * (term, string) atp_step list *
@@ -239,7 +239,7 @@
         val assms = map_filter (get_role (curry (op =) Hypothesis)) atp_proof
         val lems =
           map_filter (get_role (curry (op =) Lemma)) atp_proof
-          |> map (fn (l, t) => Prove ([], [], l, t, [], (([], []), ArithM)))
+          |> map (fn (l, t) => Prove ([], [], l, maybe_mk_Trueprop t, [], (([], []), ArithM)))
 
         val bot = atp_proof |> List.last |> #1
 
@@ -258,7 +258,7 @@
           |> fold (fn (name as (s, _), role, t, rule, _) =>
                       Symtab.update_new (s, (rule,
                         t |> (if is_clause_tainted [name] then
-                                s_maybe_not role
+                                role <> Conjecture ? (maybe_dest_Trueprop #> s_not)
                                 #> fold exists_of (map Var (Term.add_vars t []))
                               else
                                 I))))
@@ -268,12 +268,14 @@
             Option.map (is_skolemize_rule o fst) (Symtab.lookup steps s) = SOME true
           | is_clause_skolemize_rule _ = false
 
-        (* The assumptions and conjecture are "prop"s; the other formulas are "bool"s. *)
+        (* The assumptions and conjecture are "prop"s; the other formulas are "bool"s (for ATPs) or
+           "prop"s (for Z3). TODO: Always use "prop". *)
         fun prop_of_clause [(num, _)] =
             Symtab.lookup steps num |> the |> snd |> maybe_mk_Trueprop |> close_form
           | prop_of_clause names =
             let
-              val lits = map snd (map_filter (Symtab.lookup steps o fst) names)
+              val lits =
+                map (maybe_dest_Trueprop o snd) (map_filter (Symtab.lookup steps o fst) names)
             in
               case List.partition (can HOLogic.dest_not) lits of
                 (negs as _ :: _, pos as _ :: _) =>
@@ -305,7 +307,7 @@
               fun do_rest l step = isar_steps outer (SOME l) (step :: accum) infs
             in
               if is_clause_tainted c then
-                case gamma of
+                (case gamma of
                   [g] =>
                   if is_clause_skolemize_rule g andalso is_clause_tainted g then
                     let
@@ -315,7 +317,7 @@
                     end
                   else
                     do_rest l (prove [] by)
-                | _ => do_rest l (prove [] by)
+                | _ => do_rest l (prove [] by))
               else
                 if is_clause_skolemize_rule c then
                   do_rest l (Prove ([], skolems_of t, l, t, [], by))
@@ -350,13 +352,14 @@
         val (preplay_interface as {overall_preplay_stats, ...}, isar_proof) =
           refute_graph
 (*
-          |> tap (tracing o prefix "REFUTE: " o string_of_refute_graph)
+          |> tap (tracing o prefix "REFUTE GRAPH: " o string_of_refute_graph)
 *)
           |> redirect_graph axioms tainted bot
 (*
-          |> tap (tracing o prefix "DIRECT: " o string_of_direct_proof)
+          |> tap (tracing o prefix "DIRECT PROOF: " o string_of_direct_proof)
 *)
           |> isar_proof_of_direct_proof
+          |> postprocess_remove_unreferenced_steps I
           |> relabel_proof_canonically
           |> `(proof_preplay_interface debug ctxt metis_type_enc metis_lam_trans do_preplay
                preplay_timeout)
@@ -365,7 +368,7 @@
           |> compress_proof (if isar_proofs = SOME true then isar_compress else 1000.0)
                preplay_interface
           |> isar_try0 ? try0 preplay_timeout preplay_interface
-          |> minimize_dependencies_and_remove_unrefed_steps isar_try0 preplay_interface
+          |> postprocess_remove_unreferenced_steps (isar_try0 ? min_deps_of_step preplay_interface)
           |> `overall_preplay_stats
           ||> clean_up_labels_in_proof
         val isar_text =
diff -r 15a642b9ffac -r cbebe2cf77f1 src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML	Mon Dec 09 23:22:44 2013 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML	Tue Dec 10 15:24:17 2013 +0800
@@ -17,46 +17,40 @@
 structure Sledgehammer_Try0 : SLEDGEHAMMER_TRY0 =
 struct
 
+open Sledgehammer_Util
 open Sledgehammer_Proof
 open Sledgehammer_Preplay
 
-fun variants (Let _) = raise Fail "Sledgehammer_Try0: variants"
-  | variants (Prove (qs, xs, l, t, subproofs, (facts, _))) =
-      let
-        val methods = [SimpM, FastforceM, AutoM, ArithM, ForceM, BlastM]
-        fun step method = Prove (qs, xs, l, t, subproofs, (facts, method))
-        (*fun step_without_facts method =
-          Prove (qs, xs, l, t, subproofs, (no_facts, method))*)
-      in
-        (* FIXME *)
-        (* There seems to be a bias for methods earlier in the list, so we put
-           the variants using no facts first. *)
-        (*map step_without_facts methods @*) map step methods
-      end
+val variant_methods = [SimpM, AutoM, ArithM, FastforceM, BlastM, ForceM, MetisM]
+
+fun variants_of_step (Let _) = raise Fail "Sledgehammer_Try0: variants_of_step"
+  | variants_of_step (Prove (qs, xs, l, t, subproofs, (facts, meth))) =
+    variant_methods
+    |> remove (op =) meth
+    |> map (fn meth' => Prove (qs, xs, l, t, subproofs, (facts, meth')))
+
+val slack = seconds 0.05
 
 fun try0_step _ _ (step as Let _) = step
-  | try0_step preplay_timeout ({preplay_quietly, get_preplay_time,
-    set_preplay_time, ...} : preplay_interface)
-    (step as Prove (_, _, l, _, _, _)) =
-      let
-
-        val timeout =
-          case get_preplay_time l of
-            (true, _) => preplay_timeout
-          | (false, t) => t
+  | try0_step preplay_timeout
+      ({preplay_quietly, get_preplay_time, set_preplay_time, ...} : preplay_interface)
+      (step as Prove (_, _, l, _, _, _)) =
+    let
+      val timeout =
+        (case get_preplay_time l of
+          (true, _) => preplay_timeout
+        | (false, t) => Time.+ (t, slack))
 
-        fun try_variant variant =
-           case preplay_quietly timeout variant of
-             (true, _) => NONE
-           | time as (false, _) => SOME (variant, time)
+      fun try_variant variant =
+        (case preplay_quietly timeout variant of
+          (true, _) => NONE
+        | time as (false, _) => SOME (variant, time))
+    in
+      (case Par_List.get_some try_variant (variants_of_step step) of
+        SOME (step, time) => (set_preplay_time l time; step)
+      | NONE => step)
+    end
 
-      in
-        case Par_List.get_some try_variant (variants step) of
-          SOME (step, time) => (set_preplay_time l time; step)
-        | NONE => step
-      end
-
-fun try0 preplay_timeout preplay_interface proof =
-     map_isar_steps (try0_step preplay_timeout preplay_interface) proof
+val try0 = map_isar_steps oo try0_step
 
 end;