# HG changeset patch
# User boehmes
# Date 1301665759 -7200
# Node ID 9893b2913a44083e0fbd122107197697df777ff7
# Parent  1e7b62c93f5d5f55a70f2a543b8c446a4acc814a
save reflexivity steps in discharging Z3 Skolemization hypotheses

diff -r 1e7b62c93f5d -r 9893b2913a44 src/HOL/Tools/SMT/z3_proof_reconstruction.ML
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Apr 01 13:49:38 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Apr 01 15:49:19 2011 +0200
@@ -596,8 +596,7 @@
 end
 
 
-(* c = SOME x. P x |- (EX x. P x) = P c
-   c = SOME x. ~ P x |- ~(ALL x. P x) = ~ P c *)
+(* |- (EX x. P x) = P c     |- ~(ALL x. P x) = ~ P c *)
 local
   val forall =
     SMT_Utils.mk_const_pat @{theory} @{const_name all}
@@ -619,8 +618,7 @@
     in (Thm.instantiate ([], vars_of (Thm.prop_of thm) ~~ vs) thm, ctxt') end
 
   val sk_rules = @{lemma
-    "a = (SOME x. P x) ==> (EX x. P x) = P a"
-    "a = (SOME x. ~P x) ==> (~(ALL x. P x)) = (~P a)"
+    "(EX x. P x) = P (SOME x. P x)"   "(~(ALL x. P x)) = (~P (SOME x. ~P x))"
     by (metis someI_ex)+}
 in
 
@@ -628,10 +626,9 @@
   apfst Thm oo close vars (yield_singleton Assumption.add_assumes)
 
 fun discharge_sk_tac i st = (
-  Tactic.rtac @{thm trans} i
-  THEN Tactic.resolve_tac sk_rules i
-  THEN (Tactic.rtac @{thm refl} ORELSE' discharge_sk_tac) (i+1)
-  THEN Tactic.rtac @{thm refl} i) st
+  Tactic.rtac @{thm trans}
+  THEN' Tactic.resolve_tac sk_rules
+  THEN' (Tactic.rtac @{thm refl} ORELSE' discharge_sk_tac)) i st
 
 end