1.1 --- a/src/HOL/SMT_Examples/SMT_Examples.certs	Mon Jul 18 13:49:26 2011 +0200
     1.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.certs	Mon Jul 18 18:52:52 2011 +0200
     1.3 @@ -15262,3 +15262,41 @@
     1.4  #271 := [asserted]: #124
     1.5  [unit-resolution #271 #651]: false
     1.6  unsat
     1.7 +d578ad7e6589d737d5b50614f48a1b12ef69c636 37 0
     1.8 +#2 := false
     1.9 +#11 := 0::Int
    1.10 +decl f3 :: Int
    1.11 +#8 := f3
    1.12 +#13 := (<= f3 0::Int)
    1.13 +#55 := (not #13)
    1.14 +decl f4 :: Int
    1.15 +#9 := f4
    1.16 +#14 := (<= f4 0::Int)
    1.17 +#10 := (* f3 f4)
    1.18 +#12 := (<= #10 0::Int)
    1.19 +#38 := (not #12)
    1.20 +#45 := (or #38 #13 #14)
    1.21 +#48 := (not #45)
    1.22 +#15 := (or #13 #14)
    1.23 +#16 := (implies #12 #15)
    1.24 +#17 := (not #16)
    1.25 +#51 := (iff #17 #48)
    1.26 +#39 := (or #38 #15)
    1.27 +#42 := (not #39)
    1.28 +#49 := (iff #42 #48)
    1.29 +#46 := (iff #39 #45)
    1.30 +#47 := [rewrite]: #46
    1.31 +#50 := [monotonicity #47]: #49
    1.32 +#43 := (iff #17 #42)
    1.33 +#40 := (iff #16 #39)
    1.34 +#41 := [rewrite]: #40
    1.35 +#44 := [monotonicity #41]: #43
    1.36 +#52 := [trans #44 #50]: #51
    1.37 +#37 := [asserted]: #17
    1.38 +#53 := [mp #37 #52]: #48
    1.39 +#56 := [not-or-elim #53]: #55
    1.40 +#57 := (not #14)
    1.41 +#58 := [not-or-elim #53]: #57
    1.42 +#54 := [not-or-elim #53]: #12
    1.43 +[th-lemma arith farkas 1 1 1 #54 #58 #56]: false
    1.44 +unsat

     2.1 --- a/src/HOL/SMT_Examples/SMT_Examples.thy	Mon Jul 18 13:49:26 2011 +0200
     2.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Mon Jul 18 18:52:52 2011 +0200
     2.3 @@ -414,6 +414,15 @@
     2.4     U + (2 * (1 + p) * (b + e) + (1 + p) * d + d * p) - (1 + p) * (b + d + e)"
     2.5    by smt
     2.6  
     2.7 +lemma [z3_rule]:
     2.8 +  fixes x :: "int"
     2.9 +  assumes "x * y \<le> 0" and "\<not> y \<le> 0" and "\<not> x \<le> 0"
    2.10 +  shows False
    2.11 +  using assms by (metis mult_le_0_iff)
    2.12 +
    2.13 +lemma "x * y \<le> (0 :: int) \<Longrightarrow> x \<le> 0 \<or> y \<le> 0" by smt
    2.14 +
    2.15 +
    2.16  
    2.17  subsection {* Linear arithmetic for natural numbers *}
    2.18  

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