# HG changeset patch
# User boehmes
# Date 1302282248 -7200
# Node ID 0fd33b6b22cf56188cce1c1b96f251e8d1760298
# Parent  c2b5dbb76b7ee6b39473142eacdb7e8ab847ee57
corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables

diff -r c2b5dbb76b7e -r 0fd33b6b22cf src/HOL/SMT_Examples/SMT_Examples.certs
--- a/src/HOL/SMT_Examples/SMT_Examples.certs	Fri Apr 08 17:13:49 2011 +0200
+++ b/src/HOL/SMT_Examples/SMT_Examples.certs	Fri Apr 08 19:04:08 2011 +0200
@@ -15018,3 +15018,64 @@
 #36 := [asserted]: #16
 [mp #36 #70]: false
 unsat
+1953a39a3cc38daf2fde4846aa1d5cbc2ff95785 60 0
+#2 := false
+#8 := 0::Int
+decl ?v1!0 :: Int
+#67 := ?v1!0
+#70 := (<= ?v1!0 0::Int)
+#63 := (not #70)
+#11 := 1::Int
+#68 := (>= ?v1!0 1::Int)
+#69 := (not #68)
+#79 := (or #69 #63)
+#82 := (not #79)
+#64 := (or #63 #69)
+#71 := (not #64)
+#83 := (iff #71 #82)
+#80 := (iff #64 #79)
+#81 := [rewrite]: #80
+#84 := [monotonicity #81]: #83
+#9 := (:var 0 Int)
+#48 := (>= #9 1::Int)
+#46 := (not #48)
+#42 := (<= #9 0::Int)
+#43 := (not #42)
+#50 := (or #43 #46)
+#53 := (forall (vars (?v1 Int)) #50)
+#56 := (not #53)
+#72 := (~ #56 #71)
+#73 := [sk]: #72
+#12 := (< #9 1::Int)
+#10 := (< 0::Int #9)
+#13 := (or #10 #12)
+#14 := (forall (vars (?v0 Int) (?v1 Int)) #13)
+#15 := (not #14)
+#59 := (iff #15 #56)
+#36 := (forall (vars (?v1 Int)) #13)
+#39 := (not #36)
+#57 := (iff #39 #56)
+#54 := (iff #36 #53)
+#51 := (iff #13 #50)
+#47 := (iff #12 #46)
+#49 := [rewrite]: #47
+#44 := (iff #10 #43)
+#45 := [rewrite]: #44
+#52 := [monotonicity #45 #49]: #51
+#55 := [quant-intro #52]: #54
+#58 := [monotonicity #55]: #57
+#40 := (iff #15 #39)
+#37 := (iff #14 #36)
+#38 := [elim-unused]: #37
+#41 := [monotonicity #38]: #40
+#60 := [trans #41 #58]: #59
+#35 := [asserted]: #15
+#61 := [mp #35 #60]: #56
+#76 := [mp~ #61 #73]: #71
+#77 := [mp #76 #84]: #82
+#85 := [not-or-elim #77]: #70
+#78 := [not-or-elim #77]: #68
+#141 := [th-lemma arith farkas 1 1]: #64
+#142 := [unit-resolution #141 #78]: #63
+[unit-resolution #142 #85]: false
+unsat
diff -r c2b5dbb76b7e -r 0fd33b6b22cf src/HOL/SMT_Examples/SMT_Examples.thy
--- a/src/HOL/SMT_Examples/SMT_Examples.thy	Fri Apr 08 17:13:49 2011 +0200
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Fri Apr 08 19:04:08 2011 +0200
@@ -390,11 +390,12 @@
 
 lemma "\<exists>u::int. \<forall>(x::int) y::real. 0 < x \<and> 0 < y \<longrightarrow> -1 < x" by smt
 
-
 lemma "\<exists>x::int. (\<forall>y. y \<ge> x \<longrightarrow> y > 0) \<longrightarrow> x > 0" by smt
 
 lemma "\<forall>x::int. SMT.trigger [[SMT.pat x]] (x < a \<longrightarrow> 2 * x < 2 * a)" by smt
 
+lemma "\<forall>(a::int) b::int. 0 < b \<or> b < 1" by smt
+
 
 subsection {* Non-linear arithmetic over integers and reals *}
 
diff -r c2b5dbb76b7e -r 0fd33b6b22cf src/HOL/Tools/SMT/z3_proof_reconstruction.ML
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Apr 08 17:13:49 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Apr 08 19:04:08 2011 +0200
@@ -564,19 +564,19 @@
 
 (* |- (ALL x1 ... xn y1 ... yn. P x1 ... xn) = (ALL x1 ... xn. P x1 ... xn) *)
 local
-  val elim_all = @{lemma "(ALL x. P) == P" by simp}
-  val elim_ex = @{lemma "(EX x. P) == P" by simp}
-
-  fun elim_unused_conv ctxt =
-    Conv.params_conv ~1 (K (Conv.arg_conv (Conv.arg1_conv
-      (Conv.rewrs_conv [elim_all, elim_ex])))) ctxt
+  val elim_all = @{lemma "P = Q ==> (ALL x. P) = Q" by fast}
+  val elim_ex = @{lemma "P = Q ==> (EX x. P) = Q" by fast}
 
-  fun elim_unused_tac ctxt =
-    REPEAT_ALL_NEW (
-      Tactic.match_tac [@{thm refl}, @{thm iff_allI}, @{thm iff_exI}]
-      ORELSE' CONVERSION (elim_unused_conv ctxt))
+  fun elim_unused_tac i st = (
+    Tactic.match_tac [@{thm refl}]
+    ORELSE' (Tactic.match_tac [elim_all, elim_ex] THEN' elim_unused_tac)
+    ORELSE' (
+      Tactic.match_tac [@{thm iff_allI}, @{thm iff_exI}]
+      THEN' elim_unused_tac)) i st
 in
-fun elim_unused_vars ctxt = Thm o Z3_Proof_Tools.by_tac (elim_unused_tac ctxt)
+
+val elim_unused_vars = Thm o Z3_Proof_Tools.by_tac elim_unused_tac
+
 end
 
 
@@ -781,7 +781,7 @@
     | (Z3_Proof_Parser.Quant_Intro, [(p, _)]) => (quant_intro vars p ct, cxp)
     | (Z3_Proof_Parser.Pull_Quant, _) => (pull_quant cx ct, cxp)
     | (Z3_Proof_Parser.Push_Quant, _) => (push_quant cx ct, cxp)
-    | (Z3_Proof_Parser.Elim_Unused_Vars, _) => (elim_unused_vars cx ct, cxp)
+    | (Z3_Proof_Parser.Elim_Unused_Vars, _) => (elim_unused_vars ct, cxp)
     | (Z3_Proof_Parser.Dest_Eq_Res, _) => (dest_eq_res cx ct, cxp)
     | (Z3_Proof_Parser.Quant_Inst, _) => (quant_inst ct, cxp)
     | (Z3_Proof_Parser.Skolemize, _) => skolemize vars ct cx ||> rpair ptab