# HG changeset patch
# User smolkas
# Date 1357738546 -3600
# Node ID 6f571f6797bd5c3607477ff68d596bbd8ef98c36
# Parent  15dc91cf47502d37c3e847d15ca7b455cbf7421f
preplay obtain steps

diff -r 15dc91cf4750 -r 6f571f6797bd src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Wed Jan 09 12:22:09 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Wed Jan 09 14:35:46 2013 +0100
@@ -68,13 +68,14 @@
       val metis_fail = ref false
     in
       fun handle_metis_fail try_metis () =
-        try_metis () handle _ => (metis_fail := true; SOME Time.zeroTime)
+        try_metis () handle exp =>
+          (if debug then raise exp else metis_fail := true; SOME Time.zeroTime)
       fun get_time lazy_time =
         if !metis_fail then SOME Time.zeroTime else Lazy.force lazy_time
       val metis_fail = fn () => !metis_fail
     end
 
-    (* Shrink top level proof - do not shrink case splits *)
+    (* Shrink proof on top level - do not shrink case splits *)
     fun shrink_top_level on_top_level ctxt proof =
     let
       (* proof vector *)
@@ -123,32 +124,64 @@
           |> maps (thms_of_name ctxt)
 
       (* TODO: add "Obtain" case *)
-      fun try_metis timeout (succedent, Prove (_, _, t, byline)) =
-        if not preplay then K (SOME Time.zeroTime) else
-        let
-          val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
-          val facts =
-            (case byline of
-              By_Metis fact_names => resolve_fact_names fact_names
-            | Case_Split (cases, fact_names) =>
-              resolve_fact_names fact_names
-                @ (case the succedent of
-                    Assume (_, t) => make_thm t
-                  | Obtain (_, _, _, t, _) => make_thm t
-                  | Prove (_, _, t, _) => make_thm t
-                  | _ => error "Internal error: unexpected succedent of case split")
-                :: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t)
-                                | _ => error "Internal error: malformed case split")
-                           #> make_thm)
-                     cases)
-          val goal =
-            Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t
-          fun tac {context = ctxt, prems = _} =
-            Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1
-        in
-          take_time timeout (fn () => goal tac)
-        end
-        | try_metis _ _  = K (SOME Time.zeroTime)
+      exception ZeroTime
+      fun try_metis timeout (succedent, step) =
+        (if not preplay then K (SOME Time.zeroTime) else
+          let
+            val (t, byline, obtain) =
+              (case step of
+                Prove (_, _, t, byline) => (t, byline, false)
+              | Obtain (_, xs, _, t, byline) =>
+                (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
+                   (see ~~/src/Pure/Isar/obtain.ML) *)
+                let
+                  (*val thesis = Term.Free ("thesis", HOLogic.boolT)
+                    |> HOLogic.mk_Trueprop
+                  val frees = map Term.Free xs
+
+                  (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
+                  val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis))
+
+                  (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *)
+                  val prop = Logic.all thesis (Logic.mk_implies (inner_prop, thesis))*)
+
+                  val thesis = Term.Free ("thesis", HOLogic.boolT)
+                  val prop =
+                    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
+                    |> (fn t => HOLogic.mk_all ("thesis", HOLogic.boolT, t))
+                    |> HOLogic.mk_Trueprop
+                in
+                  (prop, byline, true)
+                end
+              | _ => raise ZeroTime)
+            val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
+            val facts =
+              (case byline of
+                By_Metis fact_names => resolve_fact_names fact_names
+              | Case_Split (cases, fact_names) =>
+                resolve_fact_names fact_names
+                  @ (case the succedent of
+                      Assume (_, t) => make_thm t
+                    | Obtain (_, _, _, t, _) => make_thm t
+                    | Prove (_, _, t, _) => make_thm t
+                    | _ => error "Internal error: unexpected succedent of case split")
+                  :: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t)
+                                  | _ => error "Internal error: malformed case split")
+                             #> make_thm)
+                       cases)
+            val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug
+                            |> obtain ? Config.put Metis_Tactic.new_skolem true
+            val goal =
+              Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t
+            fun tac {context = ctxt, prems = _} =
+              Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1
+          in
+            take_time timeout (fn () => goal tac)
+          end)
+          handle ZeroTime => K (SOME Time.zeroTime)
 
       val try_metis_quietly = the_default NONE oo try oo try_metis