# HG changeset patch
# User boehmes
# Date 1258533293 -3600
# Node ID dd5513734567e2af8c4e418e3d12f2b4b2bc3aa0
# Parent  3aa6b991125203103f09c10cfe4d8b3641c9afb4
added arithmetic example using div and mod

diff -r 3aa6b9911252 -r dd5513734567 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Nov 17 23:47:57 2009 +0100
+++ b/src/HOL/IsaMakefile	Wed Nov 18 09:34:53 2009 +0100
@@ -1342,7 +1342,9 @@
   SMT/Examples/cert/z3_linarith_19					\
   SMT/Examples/cert/z3_linarith_19.proof				\
   SMT/Examples/cert/z3_linarith_20					\
-  SMT/Examples/cert/z3_linarith_20.proof SMT/Examples/cert/z3_mono_01	\
+  SMT/Examples/cert/z3_linarith_20.proof 				\
+  SMT/Examples/cert/z3_linarith_21					\
+  SMT/Examples/cert/z3_linarith_21.proof SMT/Examples/cert/z3_mono_01	\
   SMT/Examples/cert/z3_mono_01.proof SMT/Examples/cert/z3_mono_02	\
   SMT/Examples/cert/z3_mono_02.proof SMT/Examples/cert/z3_nat_arith_01	\
   SMT/Examples/cert/z3_nat_arith_01.proof				\
diff -r 3aa6b9911252 -r dd5513734567 src/HOL/SMT/Examples/SMT_Examples.thy
--- a/src/HOL/SMT/Examples/SMT_Examples.thy	Tue Nov 17 23:47:57 2009 +0100
+++ b/src/HOL/SMT/Examples/SMT_Examples.thy	Wed Nov 18 09:34:53 2009 +0100
@@ -409,6 +409,13 @@
   using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_linarith_20"]]
   by smt
 
+lemma                                                                         
+  assumes "(n + m) mod 2 = 0" and "n mod 4 = 3"                               
+  shows "n mod 2 = 1 & m mod 2 = (1::int)"      
+  using assms
+  using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_linarith_21"]]
+  by smt
+
 
 subsection {* Linear arithmetic with quantifiers *}
 
diff -r 3aa6b9911252 -r dd5513734567 src/HOL/SMT/Examples/cert/z3_linarith_21
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_linarith_21	Wed Nov 18 09:34:53 2009 +0100
@@ -0,0 +1,10 @@
+(benchmark Isabelle
+:extrafuns (
+  (uf_2 Int)
+  (uf_1 Int)
+ )
+:assumption (= (mod (+ uf_1 uf_2) 2) 0)
+:assumption (= (mod uf_1 4) 3)
+:assumption (not (and (= (mod uf_1 2) 1) (= (mod uf_2 2) 1)))
+:formula true
+)
diff -r 3aa6b9911252 -r dd5513734567 src/HOL/SMT/Examples/cert/z3_linarith_21.proof
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Examples/cert/z3_linarith_21.proof	Wed Nov 18 09:34:53 2009 +0100
@@ -0,0 +1,208 @@
+#2 := false
+#9 := 0::int
+#11 := 4::int
+decl uf_1 :: int
+#4 := uf_1
+#189 := (div uf_1 4::int)
+#210 := -4::int
+#211 := (* -4::int #189)
+#12 := (mod uf_1 4::int)
+#134 := -1::int
+#209 := (* -1::int #12)
+#212 := (+ #209 #211)
+#213 := (+ uf_1 #212)
+#214 := (<= #213 0::int)
+#215 := (not #214)
+#208 := (>= #213 0::int)
+#207 := (not #208)
+#216 := (or #207 #215)
+#217 := (not #216)
+#1 := true
+#36 := [true-axiom]: true
+#393 := (or false #217)
+#394 := [th-lemma]: #393
+#395 := [unit-resolution #394 #36]: #217
+#224 := (or #216 #214)
+#225 := [def-axiom]: #224
+#396 := [unit-resolution #225 #395]: #214
+#222 := (or #216 #208)
+#223 := [def-axiom]: #222
+#397 := [unit-resolution #223 #395]: #208
+#250 := (>= #12 4::int)
+#251 := (not #250)
+#398 := (or false #251)
+#399 := [th-lemma]: #398
+#400 := [unit-resolution #399 #36]: #251
+#13 := 3::int
+#90 := (>= #12 3::int)
+#92 := (not #90)
+#89 := (<= #12 3::int)
+#91 := (not #89)
+#93 := (or #91 #92)
+#94 := (not #93)
+#14 := (= #12 3::int)
+#95 := (iff #14 #94)
+#96 := [rewrite]: #95
+#38 := [asserted]: #14
+#97 := [mp #38 #96]: #94
+#99 := [not-or-elim #97]: #90
+#7 := 2::int
+#261 := (div uf_1 2::int)
+#140 := -2::int
+#276 := (* -2::int #261)
+#15 := (mod uf_1 2::int)
+#275 := (* -1::int #15)
+#277 := (+ #275 #276)
+#278 := (+ uf_1 #277)
+#279 := (<= #278 0::int)
+#280 := (not #279)
+#274 := (>= #278 0::int)
+#273 := (not #274)
+#281 := (or #273 #280)
+#282 := (not #281)
+#408 := (or false #282)
+#409 := [th-lemma]: #408
+#410 := [unit-resolution #409 #36]: #282
+#289 := (or #281 #279)
+#290 := [def-axiom]: #289
+#411 := [unit-resolution #290 #410]: #279
+#287 := (or #281 #274)
+#288 := [def-axiom]: #287
+#412 := [unit-resolution #288 #410]: #274
+#16 := 1::int
+#55 := (>= #15 1::int)
+#100 := (not #55)
+decl uf_2 :: int
+#5 := uf_2
+#18 := (mod uf_2 2::int)
+#61 := (<= #18 1::int)
+#102 := (not #61)
+#375 := [hypothesis]: #102
+#358 := (>= #18 2::int)
+#359 := (not #358)
+#403 := (or false #359)
+#404 := [th-lemma]: #403
+#405 := [unit-resolution #404 #36]: #359
+#406 := [th-lemma #405 #375]: false
+#407 := [lemma #406]: #61
+#413 := (or #100 #102)
+#62 := (>= #18 1::int)
+#315 := (div uf_2 2::int)
+#330 := (* -2::int #315)
+#329 := (* -1::int #18)
+#331 := (+ #329 #330)
+#332 := (+ uf_2 #331)
+#333 := (<= #332 0::int)
+#334 := (not #333)
+#328 := (>= #332 0::int)
+#327 := (not #328)
+#335 := (or #327 #334)
+#336 := (not #335)
+#376 := (or false #336)
+#377 := [th-lemma]: #376
+#378 := [unit-resolution #377 #36]: #336
+#343 := (or #335 #333)
+#344 := [def-axiom]: #343
+#379 := [unit-resolution #344 #378]: #333
+#341 := (or #335 #328)
+#342 := [def-axiom]: #341
+#380 := [unit-resolution #342 #378]: #328
+#103 := (not #62)
+#381 := [hypothesis]: #103
+#352 := (>= #18 0::int)
+#382 := (or false #352)
+#383 := [th-lemma]: #382
+#384 := [unit-resolution #383 #36]: #352
+#6 := (+ uf_1 uf_2)
+#116 := (div #6 2::int)
+#141 := (* -2::int #116)
+#8 := (mod #6 2::int)
+#139 := (* -1::int #8)
+#142 := (+ #139 #141)
+#143 := (+ uf_2 #142)
+#144 := (+ uf_1 #143)
+#138 := (<= #144 0::int)
+#136 := (not #138)
+#137 := (>= #144 0::int)
+#135 := (not #137)
+#145 := (or #135 #136)
+#146 := (not #145)
+#385 := (or false #146)
+#386 := [th-lemma]: #385
+#387 := [unit-resolution #386 #36]: #146
+#153 := (or #145 #138)
+#154 := [def-axiom]: #153
+#388 := [unit-resolution #154 #387]: #138
+#151 := (or #145 #137)
+#152 := [def-axiom]: #151
+#389 := [unit-resolution #152 #387]: #137
+#78 := (<= #8 0::int)
+#79 := (>= #8 0::int)
+#81 := (not #79)
+#80 := (not #78)
+#82 := (or #80 #81)
+#83 := (not #82)
+#10 := (= #8 0::int)
+#84 := (iff #10 #83)
+#85 := [rewrite]: #84
+#37 := [asserted]: #10
+#86 := [mp #37 #85]: #83
+#87 := [not-or-elim #86]: #78
+#390 := (or false #79)
+#391 := [th-lemma]: #390
+#392 := [unit-resolution #391 #36]: #79
+#401 := [th-lemma #99 #400 #397 #396 #392 #87 #389 #388 #384 #381 #380 #379]: false
+#402 := [lemma #401]: #62
+#57 := (<= #15 1::int)
+#101 := (not #57)
+#369 := [hypothesis]: #101
+#304 := (>= #15 2::int)
+#305 := (not #304)
+#370 := (or false #305)
+#371 := [th-lemma]: #370
+#372 := [unit-resolution #371 #36]: #305
+#373 := [th-lemma #372 #369]: false
+#374 := [lemma #373]: #57
+#104 := (or #100 #101 #102 #103)
+#69 := (and #55 #57 #61 #62)
+#74 := (not #69)
+#113 := (iff #74 #104)
+#105 := (not #104)
+#108 := (not #105)
+#111 := (iff #108 #104)
+#112 := [rewrite]: #111
+#109 := (iff #74 #108)
+#106 := (iff #69 #105)
+#107 := [rewrite]: #106
+#110 := [monotonicity #107]: #109
+#114 := [trans #110 #112]: #113
+#19 := (= #18 1::int)
+#17 := (= #15 1::int)
+#20 := (and #17 #19)
+#21 := (not #20)
+#75 := (iff #21 #74)
+#72 := (iff #20 #69)
+#63 := (and #61 #62)
+#58 := (and #55 #57)
+#66 := (and #58 #63)
+#70 := (iff #66 #69)
+#71 := [rewrite]: #70
+#67 := (iff #20 #66)
+#64 := (iff #19 #63)
+#65 := [rewrite]: #64
+#59 := (iff #17 #58)
+#60 := [rewrite]: #59
+#68 := [monotonicity #60 #65]: #67
+#73 := [trans #68 #71]: #72
+#76 := [monotonicity #73]: #75
+#39 := [asserted]: #21
+#77 := [mp #39 #76]: #74
+#115 := [mp #77 #114]: #104
+#414 := [unit-resolution #115 #374 #402]: #413
+#415 := [unit-resolution #414 #407]: #100
+#298 := (>= #15 0::int)
+#416 := (or false #298)
+#417 := [th-lemma]: #416
+#418 := [unit-resolution #417 #36]: #298
+[th-lemma #418 #415 #412 #411 #99 #400 #397 #396]: false
+unsat