--- a/src/HOL/ROOT Tue Aug 19 09:34:57 2014 +0200
+++ b/src/HOL/ROOT Tue Aug 19 09:36:37 2014 +0200
@@ -782,7 +782,6 @@
files
"Boogie_Dijkstra.certs2"
"Boogie_Max.certs2"
- "SMT_Examples.certs"
"SMT_Examples.certs2"
"SMT_Word_Examples.certs2"
"VCC_Max.certs2"
--- a/src/HOL/SMT_Examples/SMT_Examples.certs Tue Aug 19 09:34:57 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-43550507f510d81bc4fb9ef8c1fd14424eaa9070 37 0
-#2 := false
-#10 := 0::Int
-decl f3 :: Int
-#7 := f3
-#12 := (<= f3 0::Int)
-#54 := (not #12)
-decl f4 :: Int
-#8 := f4
-#13 := (<= f4 0::Int)
-#9 := (* f3 f4)
-#11 := (<= #9 0::Int)
-#37 := (not #11)
-#44 := (or #37 #12 #13)
-#47 := (not #44)
-#14 := (or #12 #13)
-#15 := (implies #11 #14)
-#16 := (not #15)
-#50 := (iff #16 #47)
-#38 := (or #37 #14)
-#41 := (not #38)
-#48 := (iff #41 #47)
-#45 := (iff #38 #44)
-#46 := [rewrite]: #45
-#49 := [monotonicity #46]: #48
-#42 := (iff #16 #41)
-#39 := (iff #15 #38)
-#40 := [rewrite]: #39
-#43 := [monotonicity #40]: #42
-#51 := [trans #43 #49]: #50
-#36 := [asserted]: #16
-#52 := [mp #36 #51]: #47
-#55 := [not-or-elim #52]: #54
-#56 := (not #13)
-#57 := [not-or-elim #52]: #56
-#53 := [not-or-elim #52]: #11
-[th-lemma arith farkas 1 1 1 #53 #57 #55]: false
-unsat
--- a/src/HOL/SMT_Examples/SMT_Examples.thy Tue Aug 19 09:34:57 2014 +0200
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy Tue Aug 19 09:36:37 2014 +0200
@@ -8,9 +8,6 @@
imports Complex_Main
begin
-declare [[smt_certificates = "SMT_Examples.certs"]]
-declare [[smt_read_only_certificates = true]]
-
declare [[smt2_certificates = "SMT_Examples.certs2"]]
declare [[smt2_read_only_certificates = true]]
@@ -382,16 +379,12 @@
U + (2 * (1 + p) * (b + e) + (1 + p) * d + d * p) - (1 + p) * (b + d + e)"
using [[z3_new_extensions]] by smt2
-lemma [z3_rule, z3_new_rule]:
+lemma [z3_new_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"
- using [[z3_with_extensions]] [[z3_new_extensions]]
- by smt (* smt2 FIXME: "th-lemma" tactic fails *)
-
section {* Pairs *}
--- a/src/HOL/SMT_Examples/SMT_Tests.thy Tue Aug 19 09:34:57 2014 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy Tue Aug 19 09:36:37 2014 +0200
@@ -8,7 +8,6 @@
imports Complex_Main
begin
-smt_status
smt2_status
text {* Most examples are taken from various Isabelle theories and from HOL4. *}
@@ -588,7 +587,7 @@
"p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
p \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p"
using point.simps bw_point.simps
- by smt+ (* smt2 FIXME: bad Z3 4.3.x proof *)
+ sorry (* smt2 FIXME: bad Z3 4.3.x proof *)
lemma
"\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> cx = 3, cy = 4, black = w \<rparr>"