allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)

--- a/src/HOL/SMT_Examples/SMT_Examples.certs	Mon Jul 18 13:49:26 2011 +0200
+++ b/src/HOL/SMT_Examples/SMT_Examples.certs	Mon Jul 18 18:52:52 2011 +0200
@@ -15262,3 +15262,41 @@
 #271 := [asserted]: #124
 [unit-resolution #271 #651]: false
 unsat
+d578ad7e6589d737d5b50614f48a1b12ef69c636 37 0
+#2 := false
+#11 := 0::Int
+decl f3 :: Int
+#8 := f3
+#13 := (<= f3 0::Int)
+#55 := (not #13)
+decl f4 :: Int
+#9 := f4
+#14 := (<= f4 0::Int)
+#10 := (* f3 f4)
+#12 := (<= #10 0::Int)
+#38 := (not #12)
+#45 := (or #38 #13 #14)
+#48 := (not #45)
+#15 := (or #13 #14)
+#16 := (implies #12 #15)
+#17 := (not #16)
+#51 := (iff #17 #48)
+#39 := (or #38 #15)
+#42 := (not #39)
+#49 := (iff #42 #48)
+#46 := (iff #39 #45)
+#47 := [rewrite]: #46
+#50 := [monotonicity #47]: #49
+#43 := (iff #17 #42)
+#40 := (iff #16 #39)
+#41 := [rewrite]: #40
+#44 := [monotonicity #41]: #43
+#52 := [trans #44 #50]: #51
+#37 := [asserted]: #17
+#53 := [mp #37 #52]: #48
+#56 := [not-or-elim #53]: #55
+#57 := (not #14)
+#58 := [not-or-elim #53]: #57
+#54 := [not-or-elim #53]: #12
+[th-lemma arith farkas 1 1 1 #54 #58 #56]: false
+unsat

--- a/src/HOL/SMT_Examples/SMT_Examples.thy	Mon Jul 18 13:49:26 2011 +0200
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Mon Jul 18 18:52:52 2011 +0200
@@ -414,6 +414,15 @@
    U + (2 * (1 + p) * (b + e) + (1 + p) * d + d * p) - (1 + p) * (b + d + e)"
   by smt
 
+lemma [z3_rule]:
+  fixes x :: "int"
+  assumes "x * y \<le> 0" and "\<not> y \<le> 0" and "\<not> x \<le> 0"
+  shows False
+  using assms by (metis mult_le_0_iff)
+
+lemma "x * y \<le> (0 :: int) \<Longrightarrow> x \<le> 0 \<or> y \<le> 0" by smt
+
+
 
 subsection {* Linear arithmetic for natural numbers *}
 

--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Jul 18 13:49:26 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Jul 18 18:52:52 2011 +0200
@@ -91,7 +91,14 @@
             SOME thm => (SMT_Config.trace_msg ctxt I "Z3: succeeded"; thm)
           | NONE => apply provers ct)
 
-  in apply o cons (named ctxt "schematic rules" (by_schematic_rule ctxt)) end
+    fun schematic_label full = "schematic rules" |> full ? suffix " (full)"
+    fun schematic ctxt full ct =
+      ct
+      |> full ? fold_rev (curry Drule.mk_implies o Thm.cprop_of) thms
+      |> named ctxt (schematic_label full) (by_schematic_rule ctxt)
+      |> fold Thm.elim_implies thms
+
+  in apply o cons (schematic ctxt false) o cons (schematic ctxt true) end
 
 local
   val rewr_if =