avoid old 'smt' method in examples
authorblanchet
Tue Aug 19 09:36:37 2014 +0200 (2014-08-19)
changeset 5799468b283f9f826
parent 57993 c52255a71114
child 57995 08aa1e2cbec0
avoid old 'smt' method in examples
src/HOL/ROOT
src/HOL/SMT_Examples/SMT_Examples.certs
src/HOL/SMT_Examples/SMT_Examples.thy
src/HOL/SMT_Examples/SMT_Tests.thy
     1.1 --- a/src/HOL/ROOT	Tue Aug 19 09:34:57 2014 +0200
     1.2 +++ b/src/HOL/ROOT	Tue Aug 19 09:36:37 2014 +0200
     1.3 @@ -782,7 +782,6 @@
     1.4    files
     1.5      "Boogie_Dijkstra.certs2"
     1.6      "Boogie_Max.certs2"
     1.7 -    "SMT_Examples.certs"
     1.8      "SMT_Examples.certs2"
     1.9      "SMT_Word_Examples.certs2"
    1.10      "VCC_Max.certs2"
     2.1 --- a/src/HOL/SMT_Examples/SMT_Examples.certs	Tue Aug 19 09:34:57 2014 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,38 +0,0 @@
     2.4 -43550507f510d81bc4fb9ef8c1fd14424eaa9070 37 0
     2.5 -#2 := false
     2.6 -#10 := 0::Int
     2.7 -decl f3 :: Int
     2.8 -#7 := f3
     2.9 -#12 := (<= f3 0::Int)
    2.10 -#54 := (not #12)
    2.11 -decl f4 :: Int
    2.12 -#8 := f4
    2.13 -#13 := (<= f4 0::Int)
    2.14 -#9 := (* f3 f4)
    2.15 -#11 := (<= #9 0::Int)
    2.16 -#37 := (not #11)
    2.17 -#44 := (or #37 #12 #13)
    2.18 -#47 := (not #44)
    2.19 -#14 := (or #12 #13)
    2.20 -#15 := (implies #11 #14)
    2.21 -#16 := (not #15)
    2.22 -#50 := (iff #16 #47)
    2.23 -#38 := (or #37 #14)
    2.24 -#41 := (not #38)
    2.25 -#48 := (iff #41 #47)
    2.26 -#45 := (iff #38 #44)
    2.27 -#46 := [rewrite]: #45
    2.28 -#49 := [monotonicity #46]: #48
    2.29 -#42 := (iff #16 #41)
    2.30 -#39 := (iff #15 #38)
    2.31 -#40 := [rewrite]: #39
    2.32 -#43 := [monotonicity #40]: #42
    2.33 -#51 := [trans #43 #49]: #50
    2.34 -#36 := [asserted]: #16
    2.35 -#52 := [mp #36 #51]: #47
    2.36 -#55 := [not-or-elim #52]: #54
    2.37 -#56 := (not #13)
    2.38 -#57 := [not-or-elim #52]: #56
    2.39 -#53 := [not-or-elim #52]: #11
    2.40 -[th-lemma arith farkas 1 1 1 #53 #57 #55]: false
    2.41 -unsat
     3.1 --- a/src/HOL/SMT_Examples/SMT_Examples.thy	Tue Aug 19 09:34:57 2014 +0200
     3.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Tue Aug 19 09:36:37 2014 +0200
     3.3 @@ -8,9 +8,6 @@
     3.4  imports Complex_Main
     3.5  begin
     3.6  
     3.7 -declare [[smt_certificates = "SMT_Examples.certs"]]
     3.8 -declare [[smt_read_only_certificates = true]]
     3.9 -
    3.10  declare [[smt2_certificates = "SMT_Examples.certs2"]]
    3.11  declare [[smt2_read_only_certificates = true]]
    3.12  
    3.13 @@ -382,16 +379,12 @@
    3.14     U + (2 * (1 + p) * (b + e) + (1 + p) * d + d * p) - (1 + p) * (b + d + e)"
    3.15    using [[z3_new_extensions]] by smt2
    3.16  
    3.17 -lemma [z3_rule, z3_new_rule]:
    3.18 +lemma [z3_new_rule]:
    3.19    fixes x :: "int"
    3.20    assumes "x * y \<le> 0" and "\<not> y \<le> 0" and "\<not> x \<le> 0"
    3.21    shows False
    3.22    using assms by (metis mult_le_0_iff)
    3.23  
    3.24 -lemma "x * y \<le> (0 :: int) \<Longrightarrow> x \<le> 0 \<or> y \<le> 0"
    3.25 -  using [[z3_with_extensions]] [[z3_new_extensions]]
    3.26 -  by smt (* smt2 FIXME: "th-lemma" tactic fails *)
    3.27 -
    3.28  
    3.29  section {* Pairs *}
    3.30  
     4.1 --- a/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Aug 19 09:34:57 2014 +0200
     4.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Aug 19 09:36:37 2014 +0200
     4.3 @@ -8,7 +8,6 @@
     4.4  imports Complex_Main
     4.5  begin
     4.6  
     4.7 -smt_status
     4.8  smt2_status
     4.9  
    4.10  text {* Most examples are taken from various Isabelle theories and from HOL4. *}
    4.11 @@ -588,7 +587,7 @@
    4.12    "p = \<lparr> cx = 3, cy = 4, black = True \<rparr> \<longrightarrow>
    4.13       p \<lparr> black := True \<rparr> \<lparr> cx := 3 \<rparr> \<lparr> cy := 4 \<rparr> = p"
    4.14    using point.simps bw_point.simps
    4.15 -  by smt+ (* smt2 FIXME: bad Z3 4.3.x proof *)
    4.16 +  sorry (* smt2 FIXME: bad Z3 4.3.x proof *)
    4.17  
    4.18  lemma
    4.19    "\<lparr> cx = 3, cy = 4, black = b \<rparr> \<lparr> black := w \<rparr> = \<lparr> cx = 3, cy = 4, black = w \<rparr>"