# HG changeset patch
# User blanchet
# Date 1408433797 -7200
# Node ID 68b283f9f8266d5031f0e329df565968f1d31f1b
# Parent  c52255a711149786fadb70c88febdd89a08e3153
avoid old 'smt' method in examples

diff -r c52255a71114 -r 68b283f9f826 src/HOL/ROOT
--- 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"
diff -r c52255a71114 -r 68b283f9f826 src/HOL/SMT_Examples/SMT_Examples.certs
--- 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
diff -r c52255a71114 -r 68b283f9f826 src/HOL/SMT_Examples/SMT_Examples.thy
--- 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 *}
 
diff -r c52255a71114 -r 68b283f9f826 src/HOL/SMT_Examples/SMT_Tests.thy
--- 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>"