author smolkas Wed, 09 Jan 2013 14:36:24 +0100 changeset 50780 4174abe2c5fd parent 50779 6f571f6797bd child 50783 8f42d300748f
consider merging obtain steps
```--- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Wed Jan 09 14:35:46 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Wed Jan 09 14:36:24 2013 +0100
@@ -105,11 +105,12 @@

(* candidates for elimination, use table as priority queue (greedy
algorithm) *)
-      (* TODO: consider adding "Obtain" cases *)
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)
+              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 =
@@ -147,7 +148,7 @@

val thesis = Term.Free ("thesis", HOLogic.boolT)
val prop =
-                    HOLogic.mk_imp (HOLogic.dest_Trueprop t, thesis)
+                    HOLogic.mk_imp (HOLogic.dest_Trueprop t, thesis)
|> fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) xs
|> rpair thesis
|> HOLogic.mk_imp
@@ -200,12 +201,17 @@

(* Merging *)
(* TODO: consider adding "Obtain" cases *)
-      fun merge (Prove (_, label1, _, By_Metis (lfs1, gfs1)))
-                (Prove (qs2, label2, t, By_Metis (lfs2, gfs2))) =
+      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) )
val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1
val gfs = union (op =) gfs1 gfs2
-          in Prove (qs2, label2, t, By_Metis (lfs, gfs)) end
+          in step_constructor (By_Metis (lfs, gfs)) end
| merge _ _ = error "Internal error: Unmergeable Isar steps"

fun try_merge metis_time (s1, i) (s2, j) =```