merge
authorblanchet
Fri Dec 21 13:33:54 2012 +0100 (2012-12-21)
changeset 506091d8dae3257f0
parent 50608 5977de2993ac
parent 50602 b1b9119503b8
child 50610 d9c4fbbb0c11
child 50613 168befd6cfa6
merge
     1.1 --- a/src/HOL/SMT_Examples/SMT_Tests.certs	Thu Dec 20 15:51:27 2012 +0100
     1.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.certs	Fri Dec 21 13:33:54 2012 +0100
     1.3 @@ -56557,3 +56557,1404 @@
     1.4  #78 := [asserted]: #52
     1.5  [mp #78 #87]: false
     1.6  unsat
     1.7 +f797db065a8c5b2969ce205bd43175da50729663 62 0
     1.8 +#2 := false
     1.9 +#22 := 0::Int
    1.10 +decl f3 :: (-> S2 S3 Int)
    1.11 +decl f6 :: S3
    1.12 +#10 := f6
    1.13 +decl f4 :: S2
    1.14 +#7 := f4
    1.15 +#11 := (f3 f4 f6)
    1.16 +decl f5 :: S3
    1.17 +#8 := f5
    1.18 +#9 := (f3 f4 f5)
    1.19 +#56 := -1::Int
    1.20 +#57 := (* -1::Int #11)
    1.21 +#58 := (+ #9 #57)
    1.22 +#59 := (<= #58 0::Int)
    1.23 +#62 := (if #59 #9 #11)
    1.24 +#70 := (* -1::Int #62)
    1.25 +#253 := (+ #11 #70)
    1.26 +#602 := (>= #253 0::Int)
    1.27 +#290 := (= #11 #62)
    1.28 +#206 := (not #59)
    1.29 +#205 := (= #9 #62)
    1.30 +#598 := (not #205)
    1.31 +#71 := (+ #9 #70)
    1.32 +#69 := (>= #71 0::Int)
    1.33 +#75 := (not #69)
    1.34 +#12 := (<= #9 #11)
    1.35 +#13 := (if #12 #9 #11)
    1.36 +#14 := (<= #13 #9)
    1.37 +#15 := (not #14)
    1.38 +#76 := (iff #15 #75)
    1.39 +#73 := (iff #14 #69)
    1.40 +#65 := (<= #62 #9)
    1.41 +#68 := (iff #65 #69)
    1.42 +#72 := [rewrite]: #68
    1.43 +#66 := (iff #14 #65)
    1.44 +#63 := (= #13 #62)
    1.45 +#60 := (iff #12 #59)
    1.46 +#61 := [rewrite]: #60
    1.47 +#64 := [monotonicity #61]: #63
    1.48 +#67 := [monotonicity #64]: #66
    1.49 +#74 := [trans #67 #72]: #73
    1.50 +#77 := [monotonicity #74]: #76
    1.51 +#53 := [asserted]: #15
    1.52 +#78 := [mp #53 #77]: #75
    1.53 +#594 := [hypothesis]: #205
    1.54 +#599 := (or #598 #69)
    1.55 +#600 := [th-lemma arith triangle-eq]: #599
    1.56 +#595 := [unit-resolution #600 #594 #78]: false
    1.57 +#601 := [lemma #595]: #598
    1.58 +#291 := (or #206 #205)
    1.59 +#292 := [def-axiom]: #291
    1.60 +#604 := [unit-resolution #292 #601]: #206
    1.61 +#283 := (or #59 #290)
    1.62 +#294 := [def-axiom]: #283
    1.63 +#244 := [unit-resolution #294 #604]: #290
    1.64 +#245 := (not #290)
    1.65 +#605 := (or #245 #602)
    1.66 +#603 := [th-lemma arith triangle-eq]: #605
    1.67 +#606 := [unit-resolution #603 #244]: #602
    1.68 +[th-lemma arith farkas 1 1 1 #78 #604 #606]: false
    1.69 +unsat
    1.70 +31e82c3a0418f1a5035c07306f1bcb632442caaa 62 0
    1.71 +#2 := false
    1.72 +#22 := 0::Int
    1.73 +decl f3 :: (-> S2 S3 Int)
    1.74 +decl f6 :: S3
    1.75 +#10 := f6
    1.76 +decl f4 :: S2
    1.77 +#7 := f4
    1.78 +#11 := (f3 f4 f6)
    1.79 +decl f5 :: S3
    1.80 +#8 := f5
    1.81 +#9 := (f3 f4 f5)
    1.82 +#56 := -1::Int
    1.83 +#57 := (* -1::Int #11)
    1.84 +#58 := (+ #9 #57)
    1.85 +#59 := (<= #58 0::Int)
    1.86 +#62 := (if #59 #9 #11)
    1.87 +#69 := (* -1::Int #62)
    1.88 +#70 := (+ #11 #69)
    1.89 +#68 := (>= #70 0::Int)
    1.90 +#75 := (not #68)
    1.91 +#12 := (<= #9 #11)
    1.92 +#13 := (if #12 #9 #11)
    1.93 +#14 := (<= #13 #11)
    1.94 +#15 := (not #14)
    1.95 +#76 := (iff #15 #75)
    1.96 +#73 := (iff #14 #68)
    1.97 +#65 := (<= #62 #11)
    1.98 +#71 := (iff #65 #68)
    1.99 +#72 := [rewrite]: #71
   1.100 +#66 := (iff #14 #65)
   1.101 +#63 := (= #13 #62)
   1.102 +#60 := (iff #12 #59)
   1.103 +#61 := [rewrite]: #60
   1.104 +#64 := [monotonicity #61]: #63
   1.105 +#67 := [monotonicity #64]: #66
   1.106 +#74 := [trans #67 #72]: #73
   1.107 +#77 := [monotonicity #74]: #76
   1.108 +#53 := [asserted]: #15
   1.109 +#78 := [mp #53 #77]: #75
   1.110 +#290 := (= #11 #62)
   1.111 +#206 := (not #59)
   1.112 +#599 := [hypothesis]: #59
   1.113 +#253 := (+ #9 #69)
   1.114 +#598 := (>= #253 0::Int)
   1.115 +#205 := (= #9 #62)
   1.116 +#291 := (or #206 #205)
   1.117 +#292 := [def-axiom]: #291
   1.118 +#600 := [unit-resolution #292 #599]: #205
   1.119 +#595 := (not #205)
   1.120 +#601 := (or #595 #598)
   1.121 +#239 := [th-lemma arith triangle-eq]: #601
   1.122 +#602 := [unit-resolution #239 #600]: #598
   1.123 +#604 := [th-lemma arith farkas -1 1 1 #602 #78 #599]: false
   1.124 +#244 := [lemma #604]: #206
   1.125 +#283 := (or #59 #290)
   1.126 +#294 := [def-axiom]: #283
   1.127 +#245 := [unit-resolution #294 #244]: #290
   1.128 +#605 := (not #290)
   1.129 +#603 := (or #605 #68)
   1.130 +#606 := [th-lemma arith triangle-eq]: #603
   1.131 +[unit-resolution #606 #245 #78]: false
   1.132 +unsat
   1.133 +255fa9c9d454506807f3975ef67899ee95170888 238 0
   1.134 +#2 := false
   1.135 +#23 := 0::Int
   1.136 +decl f3 :: (-> S2 S3 Int)
   1.137 +decl f6 :: S3
   1.138 +#10 := f6
   1.139 +decl f4 :: S2
   1.140 +#7 := f4
   1.141 +#11 := (f3 f4 f6)
   1.142 +decl f5 :: S3
   1.143 +#8 := f5
   1.144 +#9 := (f3 f4 f5)
   1.145 +#57 := -1::Int
   1.146 +#58 := (* -1::Int #11)
   1.147 +#59 := (+ #9 #58)
   1.148 +#60 := (<= #59 0::Int)
   1.149 +#63 := (if #60 #9 #11)
   1.150 +#72 := (* -1::Int #63)
   1.151 +#255 := (+ #9 #72)
   1.152 +#600 := (>= #255 0::Int)
   1.153 +#607 := (not #600)
   1.154 +#617 := (>= #11 0::Int)
   1.155 +#586 := (= #11 0::Int)
   1.156 +decl f7 :: (-> S4 Int S3)
   1.157 +decl f8 :: S4
   1.158 +#17 := f8
   1.159 +#295 := (f7 f8 #11)
   1.160 +#618 := (f3 f4 #295)
   1.161 +#271 := (= #618 0::Int)
   1.162 +#592 := (not #617)
   1.163 +#439 := [hypothesis]: #592
   1.164 +#612 := (or #617 #271)
   1.165 +#24 := (:var 0 Int)
   1.166 +#26 := (f7 f8 #24)
   1.167 +#628 := (pattern #26)
   1.168 +#27 := (f3 f4 #26)
   1.169 +#32 := (= #27 0::Int)
   1.170 +#89 := (>= #24 0::Int)
   1.171 +#120 := (or #89 #32)
   1.172 +#635 := (forall (vars (?v0 Int)) (:pat #628) #120)
   1.173 +#123 := (forall (vars (?v0 Int)) #120)
   1.174 +#638 := (iff #123 #635)
   1.175 +#636 := (iff #120 #120)
   1.176 +#637 := [refl]: #636
   1.177 +#639 := [quant-intro #637]: #638
   1.178 +#136 := (~ #123 #123)
   1.179 +#144 := (~ #120 #120)
   1.180 +#145 := [refl]: #144
   1.181 +#137 := [nnf-pos #145]: #136
   1.182 +#31 := (< #24 0::Int)
   1.183 +#33 := (implies #31 #32)
   1.184 +#34 := (forall (vars (?v0 Int)) #33)
   1.185 +#126 := (iff #34 #123)
   1.186 +#104 := (not #31)
   1.187 +#105 := (or #104 #32)
   1.188 +#108 := (forall (vars (?v0 Int)) #105)
   1.189 +#124 := (iff #108 #123)
   1.190 +#121 := (iff #105 #120)
   1.191 +#118 := (iff #104 #89)
   1.192 +#91 := (not #89)
   1.193 +#113 := (not #91)
   1.194 +#116 := (iff #113 #89)
   1.195 +#117 := [rewrite]: #116
   1.196 +#114 := (iff #104 #113)
   1.197 +#111 := (iff #31 #91)
   1.198 +#112 := [rewrite]: #111
   1.199 +#115 := [monotonicity #112]: #114
   1.200 +#119 := [trans #115 #117]: #118
   1.201 +#122 := [monotonicity #119]: #121
   1.202 +#125 := [quant-intro #122]: #124
   1.203 +#109 := (iff #34 #108)
   1.204 +#106 := (iff #33 #105)
   1.205 +#107 := [rewrite]: #106
   1.206 +#110 := [quant-intro #107]: #109
   1.207 +#127 := [trans #110 #125]: #126
   1.208 +#103 := [asserted]: #34
   1.209 +#128 := [mp #103 #127]: #123
   1.210 +#146 := [mp~ #128 #137]: #123
   1.211 +#640 := [mp #146 #639]: #635
   1.212 +#619 := (not #635)
   1.213 +#259 := (or #619 #617 #271)
   1.214 +#260 := (or #619 #612)
   1.215 +#262 := (iff #260 #259)
   1.216 +#598 := [rewrite]: #262
   1.217 +#261 := [quant-inst #11]: #260
   1.218 +#599 := [mp #261 #598]: #259
   1.219 +#304 := [unit-resolution #599 #640]: #612
   1.220 +#454 := [unit-resolution #304 #439]: #271
   1.221 +#300 := (= #11 #618)
   1.222 +#584 := (= f6 #295)
   1.223 +#299 := (= #295 f6)
   1.224 +#18 := (:var 0 S3)
   1.225 +#19 := (f3 f4 #18)
   1.226 +#621 := (pattern #19)
   1.227 +#20 := (f7 f8 #19)
   1.228 +#21 := (= #20 #18)
   1.229 +#622 := (forall (vars (?v0 S3)) (:pat #621) #21)
   1.230 +#22 := (forall (vars (?v0 S3)) #21)
   1.231 +#625 := (iff #22 #622)
   1.232 +#623 := (iff #21 #21)
   1.233 +#624 := [refl]: #623
   1.234 +#626 := [quant-intro #624]: #625
   1.235 +#142 := (~ #22 #22)
   1.236 +#140 := (~ #21 #21)
   1.237 +#141 := [refl]: #140
   1.238 +#143 := [nnf-pos #141]: #142
   1.239 +#55 := [asserted]: #22
   1.240 +#132 := [mp~ #55 #143]: #22
   1.241 +#627 := [mp #132 #626]: #622
   1.242 +#278 := (not #622)
   1.243 +#609 := (or #278 #299)
   1.244 +#283 := [quant-inst #10]: #609
   1.245 +#306 := [unit-resolution #283 #627]: #299
   1.246 +#585 := [symm #306]: #584
   1.247 +#582 := [monotonicity #585]: #300
   1.248 +#456 := [trans #582 #454]: #586
   1.249 +#457 := (not #586)
   1.250 +#450 := (or #457 #617)
   1.251 +#458 := [th-lemma arith triangle-eq]: #450
   1.252 +#459 := [unit-resolution #458 #439 #456]: false
   1.253 +#460 := [lemma #459]: #617
   1.254 +#555 := (or #592 #607)
   1.255 +#73 := (+ #11 #72)
   1.256 +#74 := (+ #9 #73)
   1.257 +#70 := (>= #74 0::Int)
   1.258 +#77 := (not #70)
   1.259 +#14 := (+ #9 #11)
   1.260 +#12 := (<= #9 #11)
   1.261 +#13 := (if #12 #9 #11)
   1.262 +#15 := (<= #13 #14)
   1.263 +#16 := (not #15)
   1.264 +#78 := (iff #16 #77)
   1.265 +#75 := (iff #15 #70)
   1.266 +#66 := (<= #63 #14)
   1.267 +#69 := (iff #66 #70)
   1.268 +#71 := [rewrite]: #69
   1.269 +#67 := (iff #15 #66)
   1.270 +#64 := (= #13 #63)
   1.271 +#61 := (iff #12 #60)
   1.272 +#62 := [rewrite]: #61
   1.273 +#65 := [monotonicity #62]: #64
   1.274 +#68 := [monotonicity #65]: #67
   1.275 +#76 := [trans #68 #71]: #75
   1.276 +#79 := [monotonicity #76]: #78
   1.277 +#54 := [asserted]: #16
   1.278 +#80 := [mp #54 #79]: #77
   1.279 +#589 := (or #592 #607 #70)
   1.280 +#593 := [th-lemma arith assign-bounds 1 -1]: #589
   1.281 +#552 := [unit-resolution #593 #80]: #555
   1.282 +#556 := [unit-resolution #552 #460]: #607
   1.283 +#207 := (= #9 #63)
   1.284 +#297 := (f7 f8 #9)
   1.285 +#402 := (f3 f4 #297)
   1.286 +#284 := (= #402 0::Int)
   1.287 +#405 := (iff #284 #207)
   1.288 +#445 := (iff #207 #284)
   1.289 +#562 := (= #63 0::Int)
   1.290 +#424 := (>= #73 0::Int)
   1.291 +#292 := (= #11 #63)
   1.292 +#580 := (iff #284 #292)
   1.293 +#574 := (iff #292 #284)
   1.294 +#587 := (= 0::Int #402)
   1.295 +#578 := (iff #587 #284)
   1.296 +#573 := [commutativity]: #578
   1.297 +#576 := (iff #292 #587)
   1.298 +#314 := (= #63 #402)
   1.299 +#591 := (= #9 #402)
   1.300 +#319 := (= f5 #297)
   1.301 +#298 := (= #297 f5)
   1.302 +#613 := (or #278 #298)
   1.303 +#615 := [quant-inst #8]: #613
   1.304 +#318 := [unit-resolution #615 #627]: #298
   1.305 +#320 := [symm #318]: #319
   1.306 +#313 := [monotonicity #320]: #591
   1.307 +#214 := (= #63 #9)
   1.308 +#601 := (not #292)
   1.309 +#602 := [hypothesis]: #601
   1.310 +#285 := (or #60 #292)
   1.311 +#296 := [def-axiom]: #285
   1.312 +#597 := [unit-resolution #296 #602]: #60
   1.313 +#208 := (not #60)
   1.314 +#293 := (or #208 #207)
   1.315 +#294 := [def-axiom]: #293
   1.316 +#603 := [unit-resolution #294 #597]: #207
   1.317 +#590 := [symm #603]: #214
   1.318 +#588 := [trans #590 #313]: #314
   1.319 +#241 := (not #207)
   1.320 +#604 := (or #241 #600)
   1.321 +#606 := [th-lemma arith triangle-eq]: #604
   1.322 +#246 := [unit-resolution #606 #603]: #600
   1.323 +#303 := [unit-resolution #593 #246 #80]: #592
   1.324 +#305 := [unit-resolution #304 #303]: #271
   1.325 +#583 := [trans #582 #305]: #586
   1.326 +#577 := [monotonicity #583 #588]: #576
   1.327 +#579 := [trans #577 #573]: #574
   1.328 +#575 := [symm #579]: #580
   1.329 +#272 := (>= #9 0::Int)
   1.330 +#247 := (not #272)
   1.331 +#605 := (or #247 #208 #607 #70)
   1.332 +#608 := [th-lemma arith assign-bounds -1 1 -1]: #605
   1.333 +#594 := [unit-resolution #608 #597 #80 #246]: #247
   1.334 +#616 := (or #272 #284)
   1.335 +#614 := (or #619 #272 #284)
   1.336 +#620 := (or #619 #616)
   1.337 +#270 := (iff #620 #614)
   1.338 +#275 := [rewrite]: #270
   1.339 +#610 := [quant-inst #9]: #620
   1.340 +#611 := [mp #610 #275]: #614
   1.341 +#595 := [unit-resolution #611 #640]: #616
   1.342 +#317 := [unit-resolution #595 #594]: #284
   1.343 +#581 := [mp #317 #575]: #292
   1.344 +#422 := [unit-resolution #602 #581]: false
   1.345 +#423 := [lemma #422]: #292
   1.346 +#567 := (or #601 #424)
   1.347 +#568 := [th-lemma arith triangle-eq]: #567
   1.348 +#569 := [unit-resolution #568 #423]: #424
   1.349 +#566 := [hypothesis]: #241
   1.350 +#572 := [unit-resolution #294 #566]: #208
   1.351 +#563 := (not #424)
   1.352 +#401 := (or #592 #563 #60 #70)
   1.353 +#403 := [th-lemma arith assign-bounds 1 1 1]: #401
   1.354 +#404 := [unit-resolution #403 #572 #80 #569]: #592
   1.355 +#557 := [unit-resolution #304 #404]: #271
   1.356 +#561 := (= #63 #618)
   1.357 +#558 := (= #63 #11)
   1.358 +#560 := [symm #423]: #558
   1.359 +#559 := [trans #560 #582]: #561
   1.360 +#444 := [trans #559 #557]: #562
   1.361 +#446 := [monotonicity #313 #444]: #445
   1.362 +#553 := [symm #446]: #405
   1.363 +#564 := (or #247 #563 #70)
   1.364 +#570 := [th-lemma arith assign-bounds 1 -1]: #564
   1.365 +#571 := [unit-resolution #570 #569 #80]: #247
   1.366 +#565 := [unit-resolution #595 #571]: #284
   1.367 +#455 := [mp #565 #553]: #207
   1.368 +#550 := [unit-resolution #566 #455]: false
   1.369 +#551 := [lemma #550]: #207
   1.370 +[unit-resolution #606 #551 #556]: false
   1.371 +unsat
   1.372 +045d7d8d25dac55517e319701f444d30bf2a94d9 109 0
   1.373 +#2 := false
   1.374 +#28 := 0::Int
   1.375 +decl f3 :: (-> S2 S3 Int)
   1.376 +decl f7 :: S3
   1.377 +#13 := f7
   1.378 +decl f4 :: S2
   1.379 +#7 := f4
   1.380 +#14 := (f3 f4 f7)
   1.381 +decl f6 :: S3
   1.382 +#10 := f6
   1.383 +#11 := (f3 f4 f6)
   1.384 +#67 := -1::Int
   1.385 +#76 := (* -1::Int #14)
   1.386 +#86 := (+ #11 #76)
   1.387 +#87 := (<= #86 0::Int)
   1.388 +#90 := (if #87 #11 #14)
   1.389 +#98 := (* -1::Int #90)
   1.390 +decl f5 :: S3
   1.391 +#8 := f5
   1.392 +#9 := (f3 f4 f5)
   1.393 +#99 := (+ #9 #98)
   1.394 +#97 := (>= #99 0::Int)
   1.395 +#96 := (not #97)
   1.396 +#77 := (+ #9 #76)
   1.397 +#75 := (>= #77 0::Int)
   1.398 +#74 := (not #75)
   1.399 +#70 := (* -1::Int #11)
   1.400 +#71 := (+ #9 #70)
   1.401 +#69 := (>= #71 0::Int)
   1.402 +#68 := (not #69)
   1.403 +#80 := (and #68 #74)
   1.404 +#83 := (not #80)
   1.405 +#104 := (or #83 #96)
   1.406 +#107 := (not #104)
   1.407 +#17 := (<= #11 #14)
   1.408 +#18 := (if #17 #11 #14)
   1.409 +#19 := (< #9 #18)
   1.410 +#15 := (< #9 #14)
   1.411 +#12 := (< #9 #11)
   1.412 +#16 := (and #12 #15)
   1.413 +#20 := (implies #16 #19)
   1.414 +#21 := (not #20)
   1.415 +#110 := (iff #21 #107)
   1.416 +#60 := (not #16)
   1.417 +#61 := (or #60 #19)
   1.418 +#64 := (not #61)
   1.419 +#108 := (iff #64 #107)
   1.420 +#105 := (iff #61 #104)
   1.421 +#102 := (iff #19 #96)
   1.422 +#93 := (< #9 #90)
   1.423 +#100 := (iff #93 #96)
   1.424 +#101 := [rewrite]: #100
   1.425 +#94 := (iff #19 #93)
   1.426 +#91 := (= #18 #90)
   1.427 +#88 := (iff #17 #87)
   1.428 +#89 := [rewrite]: #88
   1.429 +#92 := [monotonicity #89]: #91
   1.430 +#95 := [monotonicity #92]: #94
   1.431 +#103 := [trans #95 #101]: #102
   1.432 +#84 := (iff #60 #83)
   1.433 +#81 := (iff #16 #80)
   1.434 +#78 := (iff #15 #74)
   1.435 +#79 := [rewrite]: #78
   1.436 +#72 := (iff #12 #68)
   1.437 +#73 := [rewrite]: #72
   1.438 +#82 := [monotonicity #73 #79]: #81
   1.439 +#85 := [monotonicity #82]: #84
   1.440 +#106 := [monotonicity #85 #103]: #105
   1.441 +#109 := [monotonicity #106]: #108
   1.442 +#65 := (iff #21 #64)
   1.443 +#62 := (iff #20 #61)
   1.444 +#63 := [rewrite]: #62
   1.445 +#66 := [monotonicity #63]: #65
   1.446 +#111 := [trans #66 #109]: #110
   1.447 +#59 := [asserted]: #21
   1.448 +#112 := [mp #59 #111]: #107
   1.449 +#116 := [not-or-elim #112]: #97
   1.450 +#113 := [not-or-elim #112]: #80
   1.451 +#115 := [and-elim #113]: #74
   1.452 +#633 := (+ #14 #98)
   1.453 +#630 := (<= #633 0::Int)
   1.454 +#330 := (= #14 #90)
   1.455 +#246 := (not #87)
   1.456 +#245 := (= #11 #90)
   1.457 +#628 := (not #245)
   1.458 +#642 := (+ #11 #98)
   1.459 +#644 := (<= #642 0::Int)
   1.460 +#357 := (not #644)
   1.461 +#114 := [and-elim #113]: #68
   1.462 +#355 := [hypothesis]: #644
   1.463 +#356 := [th-lemma arith farkas -1 -1 1 #355 #114 #116]: false
   1.464 +#358 := [lemma #356]: #357
   1.465 +#252 := [hypothesis]: #245
   1.466 +#629 := (or #628 #644)
   1.467 +#351 := [th-lemma arith triangle-eq]: #629
   1.468 +#352 := [unit-resolution #351 #252 #358]: false
   1.469 +#626 := [lemma #352]: #628
   1.470 +#331 := (or #246 #245)
   1.471 +#332 := [def-axiom]: #331
   1.472 +#631 := [unit-resolution #332 #626]: #246
   1.473 +#323 := (or #87 #330)
   1.474 +#334 := [def-axiom]: #323
   1.475 +#341 := [unit-resolution #334 #631]: #330
   1.476 +#342 := (not #330)
   1.477 +#343 := (or #342 #630)
   1.478 +#344 := [th-lemma arith triangle-eq]: #343
   1.479 +#622 := [unit-resolution #344 #341]: #630
   1.480 +[th-lemma arith farkas -1 -1 1 #622 #115 #116]: false
   1.481 +unsat
   1.482 +1962433f8497846ba06e564f4ca48d7e020eb6e0 141 0
   1.483 +#2 := false
   1.484 +#10 := 0::Int
   1.485 +decl f3 :: (-> S2 S3 Int)
   1.486 +decl f6 :: (-> S4 Int S3)
   1.487 +decl f5 :: S3
   1.488 +#8 := f5
   1.489 +decl f4 :: S2
   1.490 +#7 := f4
   1.491 +#9 := (f3 f4 f5)
   1.492 +decl f7 :: S4
   1.493 +#12 := f7
   1.494 +#272 := (f6 f7 #9)
   1.495 +#570 := (f3 f4 #272)
   1.496 +#277 := (= #570 0::Int)
   1.497 +#543 := (= #9 0::Int)
   1.498 +#11 := (<= #9 0::Int)
   1.499 +#13 := (f6 f7 0::Int)
   1.500 +#14 := (if #11 f5 #13)
   1.501 +#266 := (= #13 #14)
   1.502 +#567 := (not #266)
   1.503 +#15 := (= #14 #13)
   1.504 +#16 := (not #15)
   1.505 +#564 := (iff #16 #567)
   1.506 +#293 := (iff #15 #266)
   1.507 +#294 := [commutativity]: #293
   1.508 +#568 := [monotonicity #294]: #564
   1.509 +#52 := [asserted]: #16
   1.510 +#278 := [mp #52 #568]: #567
   1.511 +#259 := (or #11 #266)
   1.512 +#270 := [def-axiom]: #259
   1.513 +#279 := [unit-resolution #270 #278]: #11
   1.514 +#569 := (>= #9 0::Int)
   1.515 +#541 := (not #277)
   1.516 +#181 := (= f5 #14)
   1.517 +#182 := (not #11)
   1.518 +#267 := (or #182 #181)
   1.519 +#268 := [def-axiom]: #267
   1.520 +#280 := [unit-resolution #268 #279]: #181
   1.521 +#556 := (= #13 f5)
   1.522 +#269 := (= #272 f5)
   1.523 +#17 := (:var 0 S3)
   1.524 +#18 := (f3 f4 #17)
   1.525 +#596 := (pattern #18)
   1.526 +#19 := (f6 f7 #18)
   1.527 +#20 := (= #19 #17)
   1.528 +#597 := (forall (vars (?v0 S3)) (:pat #596) #20)
   1.529 +#21 := (forall (vars (?v0 S3)) #20)
   1.530 +#600 := (iff #21 #597)
   1.531 +#598 := (iff #20 #20)
   1.532 +#599 := [refl]: #598
   1.533 +#601 := [quant-intro #599]: #600
   1.534 +#116 := (~ #21 #21)
   1.535 +#114 := (~ #20 #20)
   1.536 +#115 := [refl]: #114
   1.537 +#117 := [nnf-pos #115]: #116
   1.538 +#53 := [asserted]: #21
   1.539 +#106 := [mp~ #53 #117]: #21
   1.540 +#602 := [mp #106 #601]: #597
   1.541 +#588 := (not #597)
   1.542 +#590 := (or #588 #269)
   1.543 +#246 := [quant-inst #8]: #590
   1.544 +#281 := [unit-resolution #246 #602]: #269
   1.545 +#549 := (= #13 #272)
   1.546 +#553 := (= 0::Int #9)
   1.547 +#551 := (= #570 #9)
   1.548 +#557 := (= #9 #570)
   1.549 +#560 := (= f5 #272)
   1.550 +#274 := [symm #281]: #560
   1.551 +#561 := [monotonicity #274]: #557
   1.552 +#552 := [symm #561]: #551
   1.553 +#558 := (= 0::Int #570)
   1.554 +#559 := [hypothesis]: #277
   1.555 +#562 := [symm #559]: #558
   1.556 +#548 := [trans #562 #552]: #553
   1.557 +#554 := [monotonicity #548]: #549
   1.558 +#397 := [trans #554 #281]: #556
   1.559 +#398 := [trans #397 #280]: #266
   1.560 +#399 := [unit-resolution #278 #398]: false
   1.561 +#542 := [lemma #399]: #541
   1.562 +#292 := (or #569 #277)
   1.563 +#22 := (:var 0 Int)
   1.564 +#24 := (f6 f7 #22)
   1.565 +#603 := (pattern #24)
   1.566 +#25 := (f3 f4 #24)
   1.567 +#30 := (= #25 0::Int)
   1.568 +#64 := (>= #22 0::Int)
   1.569 +#94 := (or #64 #30)
   1.570 +#610 := (forall (vars (?v0 Int)) (:pat #603) #94)
   1.571 +#97 := (forall (vars (?v0 Int)) #94)
   1.572 +#613 := (iff #97 #610)
   1.573 +#611 := (iff #94 #94)
   1.574 +#612 := [refl]: #611
   1.575 +#614 := [quant-intro #612]: #613
   1.576 +#110 := (~ #97 #97)
   1.577 +#118 := (~ #94 #94)
   1.578 +#119 := [refl]: #118
   1.579 +#111 := [nnf-pos #119]: #110
   1.580 +#29 := (< #22 0::Int)
   1.581 +#31 := (implies #29 #30)
   1.582 +#32 := (forall (vars (?v0 Int)) #31)
   1.583 +#100 := (iff #32 #97)
   1.584 +#78 := (not #29)
   1.585 +#79 := (or #78 #30)
   1.586 +#82 := (forall (vars (?v0 Int)) #79)
   1.587 +#98 := (iff #82 #97)
   1.588 +#95 := (iff #79 #94)
   1.589 +#92 := (iff #78 #64)
   1.590 +#65 := (not #64)
   1.591 +#87 := (not #65)
   1.592 +#90 := (iff #87 #64)
   1.593 +#91 := [rewrite]: #90
   1.594 +#88 := (iff #78 #87)
   1.595 +#85 := (iff #29 #65)
   1.596 +#86 := [rewrite]: #85
   1.597 +#89 := [monotonicity #86]: #88
   1.598 +#93 := [trans #89 #91]: #92
   1.599 +#96 := [monotonicity #93]: #95
   1.600 +#99 := [quant-intro #96]: #98
   1.601 +#83 := (iff #32 #82)
   1.602 +#80 := (iff #31 #79)
   1.603 +#81 := [rewrite]: #80
   1.604 +#84 := [quant-intro #81]: #83
   1.605 +#101 := [trans #84 #99]: #100
   1.606 +#77 := [asserted]: #32
   1.607 +#102 := [mp #77 #101]: #97
   1.608 +#120 := [mp~ #102 #111]: #97
   1.609 +#615 := [mp #120 #614]: #610
   1.610 +#295 := (not #610)
   1.611 +#188 := (or #295 #569 #277)
   1.612 +#565 := (or #295 #292)
   1.613 +#288 := (iff #565 #188)
   1.614 +#289 := [rewrite]: #288
   1.615 +#566 := [quant-inst #9]: #565
   1.616 +#563 := [mp #566 #289]: #188
   1.617 +#555 := [unit-resolution #563 #615]: #292
   1.618 +#550 := [unit-resolution #555 #542]: #569
   1.619 +#544 := [th-lemma arith eq-propagate 0 0 #550 #279]: #543
   1.620 +#538 := [monotonicity #281]: #551
   1.621 +#539 := [trans #538 #544]: #277
   1.622 +[unit-resolution #542 #539]: false
   1.623 +unsat
   1.624 +f80dc9916afc1b74e708843f9de068b19b70dd30 62 0
   1.625 +#2 := false
   1.626 +#22 := 0::Int
   1.627 +decl f3 :: (-> S2 S3 Int)
   1.628 +decl f5 :: S3
   1.629 +#8 := f5
   1.630 +decl f4 :: S2
   1.631 +#7 := f4
   1.632 +#9 := (f3 f4 f5)
   1.633 +decl f6 :: S3
   1.634 +#10 := f6
   1.635 +#11 := (f3 f4 f6)
   1.636 +#56 := -1::Int
   1.637 +#57 := (* -1::Int #11)
   1.638 +#58 := (+ #9 #57)
   1.639 +#59 := (<= #58 0::Int)
   1.640 +#62 := (if #59 #11 #9)
   1.641 +#68 := (* -1::Int #62)
   1.642 +#69 := (+ #9 #68)
   1.643 +#70 := (<= #69 0::Int)
   1.644 +#75 := (not #70)
   1.645 +#12 := (<= #9 #11)
   1.646 +#13 := (if #12 #11 #9)
   1.647 +#14 := (<= #9 #13)
   1.648 +#15 := (not #14)
   1.649 +#76 := (iff #15 #75)
   1.650 +#73 := (iff #14 #70)
   1.651 +#65 := (<= #9 #62)
   1.652 +#71 := (iff #65 #70)
   1.653 +#72 := [rewrite]: #71
   1.654 +#66 := (iff #14 #65)
   1.655 +#63 := (= #13 #62)
   1.656 +#60 := (iff #12 #59)
   1.657 +#61 := [rewrite]: #60
   1.658 +#64 := [monotonicity #61]: #63
   1.659 +#67 := [monotonicity #64]: #66
   1.660 +#74 := [trans #67 #72]: #73
   1.661 +#77 := [monotonicity #74]: #76
   1.662 +#53 := [asserted]: #15
   1.663 +#78 := [mp #53 #77]: #75
   1.664 +#290 := (= #9 #62)
   1.665 +#206 := (not #59)
   1.666 +#599 := [hypothesis]: #59
   1.667 +#253 := (+ #11 #68)
   1.668 +#594 := (<= #253 0::Int)
   1.669 +#205 := (= #11 #62)
   1.670 +#291 := (or #206 #205)
   1.671 +#292 := [def-axiom]: #291
   1.672 +#600 := [unit-resolution #292 #599]: #205
   1.673 +#595 := (not #205)
   1.674 +#601 := (or #595 #594)
   1.675 +#239 := [th-lemma arith triangle-eq]: #601
   1.676 +#602 := [unit-resolution #239 #600]: #594
   1.677 +#604 := [th-lemma arith farkas 1 -1 1 #602 #78 #599]: false
   1.678 +#244 := [lemma #604]: #206
   1.679 +#283 := (or #59 #290)
   1.680 +#294 := [def-axiom]: #283
   1.681 +#245 := [unit-resolution #294 #244]: #290
   1.682 +#605 := (not #290)
   1.683 +#603 := (or #605 #70)
   1.684 +#606 := [th-lemma arith triangle-eq]: #603
   1.685 +[unit-resolution #606 #245 #78]: false
   1.686 +unsat
   1.687 +863d026b871fd01ad877b22fe75d3d9947adc4c3 62 0
   1.688 +#2 := false
   1.689 +#22 := 0::Int
   1.690 +decl f3 :: (-> S2 S3 Int)
   1.691 +decl f6 :: S3
   1.692 +#10 := f6
   1.693 +decl f4 :: S2
   1.694 +#7 := f4
   1.695 +#11 := (f3 f4 f6)
   1.696 +decl f5 :: S3
   1.697 +#8 := f5
   1.698 +#9 := (f3 f4 f5)
   1.699 +#56 := -1::Int
   1.700 +#59 := (* -1::Int #11)
   1.701 +#60 := (+ #9 #59)
   1.702 +#58 := (>= #60 0::Int)
   1.703 +#62 := (if #58 #9 #11)
   1.704 +#68 := (* -1::Int #62)
   1.705 +#253 := (+ #11 #68)
   1.706 +#239 := (<= #253 0::Int)
   1.707 +#290 := (= #11 #62)
   1.708 +#206 := (not #58)
   1.709 +#205 := (= #9 #62)
   1.710 +#598 := (not #205)
   1.711 +#69 := (+ #9 #68)
   1.712 +#70 := (<= #69 0::Int)
   1.713 +#75 := (not #70)
   1.714 +#12 := (<= #11 #9)
   1.715 +#13 := (if #12 #9 #11)
   1.716 +#14 := (<= #9 #13)
   1.717 +#15 := (not #14)
   1.718 +#76 := (iff #15 #75)
   1.719 +#73 := (iff #14 #70)
   1.720 +#65 := (<= #9 #62)
   1.721 +#71 := (iff #65 #70)
   1.722 +#72 := [rewrite]: #71
   1.723 +#66 := (iff #14 #65)
   1.724 +#63 := (= #13 #62)
   1.725 +#57 := (iff #12 #58)
   1.726 +#61 := [rewrite]: #57
   1.727 +#64 := [monotonicity #61]: #63
   1.728 +#67 := [monotonicity #64]: #66
   1.729 +#74 := [trans #67 #72]: #73
   1.730 +#77 := [monotonicity #74]: #76
   1.731 +#53 := [asserted]: #15
   1.732 +#78 := [mp #53 #77]: #75
   1.733 +#594 := [hypothesis]: #205
   1.734 +#599 := (or #598 #70)
   1.735 +#600 := [th-lemma arith triangle-eq]: #599
   1.736 +#595 := [unit-resolution #600 #594 #78]: false
   1.737 +#601 := [lemma #595]: #598
   1.738 +#291 := (or #206 #205)
   1.739 +#292 := [def-axiom]: #291
   1.740 +#604 := [unit-resolution #292 #601]: #206
   1.741 +#283 := (or #58 #290)
   1.742 +#294 := [def-axiom]: #283
   1.743 +#244 := [unit-resolution #294 #604]: #290
   1.744 +#245 := (not #290)
   1.745 +#605 := (or #245 #239)
   1.746 +#603 := [th-lemma arith triangle-eq]: #605
   1.747 +#606 := [unit-resolution #603 #244]: #239
   1.748 +[th-lemma arith farkas 1 1 1 #78 #604 #606]: false
   1.749 +unsat
   1.750 +54dc3056c3d64c5f00f83943070ff19ad35f8f48 409 0
   1.751 +#2 := false
   1.752 +#29 := 0::Int
   1.753 +decl f3 :: (-> S2 S3 Int)
   1.754 +decl f5 :: (-> S4 Int S3)
   1.755 +decl f8 :: S3
   1.756 +#11 := f8
   1.757 +decl f4 :: S2
   1.758 +#7 := f4
   1.759 +#12 := (f3 f4 f8)
   1.760 +decl f7 :: S3
   1.761 +#9 := f7
   1.762 +#10 := (f3 f4 f7)
   1.763 +#61 := -1::Int
   1.764 +#72 := (* -1::Int #10)
   1.765 +#73 := (+ #72 #12)
   1.766 +decl f6 :: S4
   1.767 +#8 := f6
   1.768 +#76 := (f5 f6 #73)
   1.769 +#79 := (f3 f4 #76)
   1.770 +#62 := (* -1::Int #12)
   1.771 +#341 := (+ #62 #79)
   1.772 +#619 := (+ #10 #341)
   1.773 +#459 := (<= #619 0::Int)
   1.774 +#620 := (= #619 0::Int)
   1.775 +#63 := (+ #10 #62)
   1.776 +#91 := (<= #63 0::Int)
   1.777 +#94 := (if #91 #12 #10)
   1.778 +#100 := (* -1::Int #94)
   1.779 +#564 := (+ #10 #100)
   1.780 +#540 := (<= #564 0::Int)
   1.781 +#521 := (not #540)
   1.782 +#594 := (<= #79 0::Int)
   1.783 +#602 := (= #79 0::Int)
   1.784 +#243 := (not #91)
   1.785 +#487 := [hypothesis]: #243
   1.786 +#604 := (or #91 #602)
   1.787 +#30 := (:var 0 Int)
   1.788 +#32 := (f5 f6 #30)
   1.789 +#663 := (pattern #32)
   1.790 +#33 := (f3 f4 #32)
   1.791 +#38 := (= #33 0::Int)
   1.792 +#124 := (>= #30 0::Int)
   1.793 +#155 := (or #124 #38)
   1.794 +#670 := (forall (vars (?v0 Int)) (:pat #663) #155)
   1.795 +#158 := (forall (vars (?v0 Int)) #155)
   1.796 +#673 := (iff #158 #670)
   1.797 +#671 := (iff #155 #155)
   1.798 +#672 := [refl]: #671
   1.799 +#674 := [quant-intro #672]: #673
   1.800 +#171 := (~ #158 #158)
   1.801 +#179 := (~ #155 #155)
   1.802 +#180 := [refl]: #179
   1.803 +#172 := [nnf-pos #180]: #171
   1.804 +#37 := (< #30 0::Int)
   1.805 +#39 := (implies #37 #38)
   1.806 +#40 := (forall (vars (?v0 Int)) #39)
   1.807 +#161 := (iff #40 #158)
   1.808 +#139 := (not #37)
   1.809 +#140 := (or #139 #38)
   1.810 +#143 := (forall (vars (?v0 Int)) #140)
   1.811 +#159 := (iff #143 #158)
   1.812 +#156 := (iff #140 #155)
   1.813 +#153 := (iff #139 #124)
   1.814 +#126 := (not #124)
   1.815 +#148 := (not #126)
   1.816 +#151 := (iff #148 #124)
   1.817 +#152 := [rewrite]: #151
   1.818 +#149 := (iff #139 #148)
   1.819 +#146 := (iff #37 #126)
   1.820 +#147 := [rewrite]: #146
   1.821 +#150 := [monotonicity #147]: #149
   1.822 +#154 := [trans #150 #152]: #153
   1.823 +#157 := [monotonicity #154]: #156
   1.824 +#160 := [quant-intro #157]: #159
   1.825 +#144 := (iff #40 #143)
   1.826 +#141 := (iff #39 #140)
   1.827 +#142 := [rewrite]: #141
   1.828 +#145 := [quant-intro #142]: #144
   1.829 +#162 := [trans #145 #160]: #161
   1.830 +#138 := [asserted]: #40
   1.831 +#163 := [mp #138 #162]: #158
   1.832 +#181 := [mp~ #163 #172]: #158
   1.833 +#675 := [mp #181 #674]: #670
   1.834 +#353 := (not #670)
   1.835 +#605 := (or #353 #91 #602)
   1.836 +#630 := (>= #73 0::Int)
   1.837 +#603 := (or #630 #602)
   1.838 +#606 := (or #353 #603)
   1.839 +#593 := (iff #606 #605)
   1.840 +#607 := (or #353 #604)
   1.841 +#439 := (iff #607 #605)
   1.842 +#592 := [rewrite]: #439
   1.843 +#436 := (iff #606 #607)
   1.844 +#598 := (iff #603 #604)
   1.845 +#628 := (iff #630 #91)
   1.846 +#338 := [rewrite]: #628
   1.847 +#599 := [monotonicity #338]: #598
   1.848 +#438 := [monotonicity #599]: #436
   1.849 +#595 := [trans #438 #592]: #593
   1.850 +#600 := [quant-inst #73]: #606
   1.851 +#596 := [mp #600 #595]: #605
   1.852 +#488 := [unit-resolution #596 #675]: #604
   1.853 +#498 := [unit-resolution #488 #487]: #602
   1.854 +#478 := (not #602)
   1.855 +#499 := (or #478 #594)
   1.856 +#454 := [th-lemma arith triangle-eq]: #499
   1.857 +#455 := [unit-resolution #454 #498]: #594
   1.858 +#539 := (not #594)
   1.859 +#466 := (or #539 #521)
   1.860 +#66 := (f5 f6 #63)
   1.861 +#69 := (f3 f4 #66)
   1.862 +#647 := (* -1::Int #69)
   1.863 +#290 := (+ #62 #647)
   1.864 +#631 := (+ #10 #290)
   1.865 +#640 := (>= #631 0::Int)
   1.866 +#646 := (= #631 0::Int)
   1.867 +#654 := (>= #63 0::Int)
   1.868 +#573 := (+ #12 #100)
   1.869 +#574 := (<= #573 0::Int)
   1.870 +#558 := (not #574)
   1.871 +#349 := (<= #69 0::Int)
   1.872 +#643 := (= #69 0::Int)
   1.873 +#649 := (not #654)
   1.874 +#527 := [hypothesis]: #649
   1.875 +#629 := (or #654 #643)
   1.876 +#354 := (or #353 #654 #643)
   1.877 +#355 := (or #353 #629)
   1.878 +#625 := (iff #355 #354)
   1.879 +#626 := [rewrite]: #625
   1.880 +#249 := [quant-inst #63]: #355
   1.881 +#348 := [mp #249 #626]: #354
   1.882 +#514 := [unit-resolution #348 #675]: #629
   1.883 +#517 := [unit-resolution #514 #527]: #643
   1.884 +#518 := (not #643)
   1.885 +#519 := (or #518 #349)
   1.886 +#515 := [th-lemma arith triangle-eq]: #519
   1.887 +#520 := [unit-resolution #515 #517]: #349
   1.888 +#479 := (>= #10 0::Int)
   1.889 +#560 := (= #10 0::Int)
   1.890 +#332 := (f5 f6 #10)
   1.891 +#480 := (f3 f4 #332)
   1.892 +#481 := (= #480 0::Int)
   1.893 +#554 := (not #479)
   1.894 +#541 := [hypothesis]: #554
   1.895 +#440 := (or #479 #481)
   1.896 +#585 := (or #353 #479 #481)
   1.897 +#586 := (or #353 #440)
   1.898 +#474 := (iff #586 #585)
   1.899 +#489 := [rewrite]: #474
   1.900 +#589 := [quant-inst #10]: #586
   1.901 +#491 := [mp #589 #489]: #585
   1.902 +#543 := [unit-resolution #491 #675]: #440
   1.903 +#544 := [unit-resolution #543 #541]: #481
   1.904 +#548 := (= #10 #480)
   1.905 +#546 := (= f7 #332)
   1.906 +#333 := (= #332 f7)
   1.907 +#24 := (:var 0 S3)
   1.908 +#25 := (f3 f4 #24)
   1.909 +#656 := (pattern #25)
   1.910 +#26 := (f5 f6 #25)
   1.911 +#27 := (= #26 #24)
   1.912 +#657 := (forall (vars (?v0 S3)) (:pat #656) #27)
   1.913 +#28 := (forall (vars (?v0 S3)) #27)
   1.914 +#660 := (iff #28 #657)
   1.915 +#658 := (iff #27 #27)
   1.916 +#659 := [refl]: #658
   1.917 +#661 := [quant-intro #659]: #660
   1.918 +#177 := (~ #28 #28)
   1.919 +#175 := (~ #27 #27)
   1.920 +#176 := [refl]: #175
   1.921 +#178 := [nnf-pos #176]: #177
   1.922 +#114 := [asserted]: #28
   1.923 +#167 := [mp~ #114 #178]: #28
   1.924 +#662 := [mp #167 #661]: #657
   1.925 +#313 := (not #657)
   1.926 +#648 := (or #313 #333)
   1.927 +#650 := [quant-inst #9]: #648
   1.928 +#545 := [unit-resolution #650 #662]: #333
   1.929 +#547 := [symm #545]: #546
   1.930 +#549 := [monotonicity #547]: #548
   1.931 +#550 := [trans #549 #544]: #560
   1.932 +#551 := (not #560)
   1.933 +#552 := (or #551 #479)
   1.934 +#542 := [th-lemma arith triangle-eq]: #552
   1.935 +#553 := [unit-resolution #542 #541 #550]: false
   1.936 +#531 := [lemma #553]: #479
   1.937 +#500 := (or #654 #91)
   1.938 +#446 := [th-lemma arith farkas 1 1]: #500
   1.939 +#501 := [unit-resolution #446 #527]: #91
   1.940 +#621 := (or #243 #620)
   1.941 +#34 := (= #33 #30)
   1.942 +#129 := (or #126 #34)
   1.943 +#664 := (forall (vars (?v0 Int)) (:pat #663) #129)
   1.944 +#132 := (forall (vars (?v0 Int)) #129)
   1.945 +#667 := (iff #132 #664)
   1.946 +#665 := (iff #129 #129)
   1.947 +#666 := [refl]: #665
   1.948 +#668 := [quant-intro #666]: #667
   1.949 +#169 := (~ #132 #132)
   1.950 +#168 := (~ #129 #129)
   1.951 +#165 := [refl]: #168
   1.952 +#170 := [nnf-pos #165]: #169
   1.953 +#31 := (<= 0::Int #30)
   1.954 +#35 := (implies #31 #34)
   1.955 +#36 := (forall (vars (?v0 Int)) #35)
   1.956 +#135 := (iff #36 #132)
   1.957 +#116 := (not #31)
   1.958 +#117 := (or #116 #34)
   1.959 +#120 := (forall (vars (?v0 Int)) #117)
   1.960 +#133 := (iff #120 #132)
   1.961 +#130 := (iff #117 #129)
   1.962 +#127 := (iff #116 #126)
   1.963 +#123 := (iff #31 #124)
   1.964 +#125 := [rewrite]: #123
   1.965 +#128 := [monotonicity #125]: #127
   1.966 +#131 := [monotonicity #128]: #130
   1.967 +#134 := [quant-intro #131]: #133
   1.968 +#121 := (iff #36 #120)
   1.969 +#118 := (iff #35 #117)
   1.970 +#119 := [rewrite]: #118
   1.971 +#122 := [quant-intro #119]: #121
   1.972 +#136 := [trans #122 #134]: #135
   1.973 +#115 := [asserted]: #36
   1.974 +#137 := [mp #115 #136]: #132
   1.975 +#166 := [mp~ #137 #170]: #132
   1.976 +#669 := [mp #166 #668]: #664
   1.977 +#633 := (not #664)
   1.978 +#611 := (or #633 #243 #620)
   1.979 +#627 := (= #79 #73)
   1.980 +#352 := (not #630)
   1.981 +#624 := (or #352 #627)
   1.982 +#612 := (or #633 #624)
   1.983 +#616 := (iff #612 #611)
   1.984 +#608 := (or #633 #621)
   1.985 +#615 := (iff #608 #611)
   1.986 +#610 := [rewrite]: #615
   1.987 +#609 := (iff #612 #608)
   1.988 +#618 := (iff #624 #621)
   1.989 +#335 := (iff #627 #620)
   1.990 +#617 := [rewrite]: #335
   1.991 +#339 := (iff #352 #243)
   1.992 +#340 := [monotonicity #338]: #339
   1.993 +#622 := [monotonicity #340 #617]: #618
   1.994 +#614 := [monotonicity #622]: #609
   1.995 +#457 := [trans #614 #610]: #616
   1.996 +#613 := [quant-inst #73]: #612
   1.997 +#458 := [mp #613 #457]: #611
   1.998 +#482 := [unit-resolution #458 #669]: #621
   1.999 +#506 := [unit-resolution #482 #501]: #620
  1.1000 +#507 := (not #620)
  1.1001 +#502 := (or #507 #459)
  1.1002 +#508 := [th-lemma arith triangle-eq]: #502
  1.1003 +#476 := [unit-resolution #508 #506]: #459
  1.1004 +#557 := (not #459)
  1.1005 +#555 := (not #349)
  1.1006 +#559 := (or #554 #555 #557 #558)
  1.1007 +#565 := [hypothesis]: #574
  1.1008 +#566 := [hypothesis]: #479
  1.1009 +#567 := [hypothesis]: #459
  1.1010 +#101 := (+ #79 #100)
  1.1011 +#102 := (+ #69 #101)
  1.1012 +#103 := (<= #102 0::Int)
  1.1013 +#108 := (not #103)
  1.1014 +#20 := (<= #10 #12)
  1.1015 +#21 := (if #20 #12 #10)
  1.1016 +#16 := (- #12 #10)
  1.1017 +#17 := (f5 f6 #16)
  1.1018 +#18 := (f3 f4 #17)
  1.1019 +#13 := (- #10 #12)
  1.1020 +#14 := (f5 f6 #13)
  1.1021 +#15 := (f3 f4 #14)
  1.1022 +#19 := (+ #15 #18)
  1.1023 +#22 := (<= #19 #21)
  1.1024 +#23 := (not #22)
  1.1025 +#111 := (iff #23 #108)
  1.1026 +#82 := (+ #69 #79)
  1.1027 +#85 := (<= #82 #21)
  1.1028 +#88 := (not #85)
  1.1029 +#109 := (iff #88 #108)
  1.1030 +#106 := (iff #85 #103)
  1.1031 +#97 := (<= #82 #94)
  1.1032 +#104 := (iff #97 #103)
  1.1033 +#105 := [rewrite]: #104
  1.1034 +#98 := (iff #85 #97)
  1.1035 +#95 := (= #21 #94)
  1.1036 +#92 := (iff #20 #91)
  1.1037 +#93 := [rewrite]: #92
  1.1038 +#96 := [monotonicity #93]: #95
  1.1039 +#99 := [monotonicity #96]: #98
  1.1040 +#107 := [trans #99 #105]: #106
  1.1041 +#110 := [monotonicity #107]: #109
  1.1042 +#89 := (iff #23 #88)
  1.1043 +#86 := (iff #22 #85)
  1.1044 +#83 := (= #19 #82)
  1.1045 +#80 := (= #18 #79)
  1.1046 +#77 := (= #17 #76)
  1.1047 +#74 := (= #16 #73)
  1.1048 +#75 := [rewrite]: #74
  1.1049 +#78 := [monotonicity #75]: #77
  1.1050 +#81 := [monotonicity #78]: #80
  1.1051 +#70 := (= #15 #69)
  1.1052 +#67 := (= #14 #66)
  1.1053 +#64 := (= #13 #63)
  1.1054 +#65 := [rewrite]: #64
  1.1055 +#68 := [monotonicity #65]: #67
  1.1056 +#71 := [monotonicity #68]: #70
  1.1057 +#84 := [monotonicity #71 #81]: #83
  1.1058 +#87 := [monotonicity #84]: #86
  1.1059 +#90 := [monotonicity #87]: #89
  1.1060 +#112 := [trans #90 #110]: #111
  1.1061 +#60 := [asserted]: #23
  1.1062 +#113 := [mp #60 #112]: #108
  1.1063 +#563 := [hypothesis]: #349
  1.1064 +#568 := [th-lemma arith farkas 1 -1 1 -1 1 #563 #113 #567 #566 #565]: false
  1.1065 +#556 := [lemma #568]: #559
  1.1066 +#483 := [unit-resolution #556 #476 #531 #520]: #558
  1.1067 +#242 := (= #12 #94)
  1.1068 +#328 := (or #243 #242)
  1.1069 +#329 := [def-axiom]: #328
  1.1070 +#442 := [unit-resolution #329 #501]: #242
  1.1071 +#473 := (not #242)
  1.1072 +#475 := (or #473 #574)
  1.1073 +#477 := [th-lemma arith triangle-eq]: #475
  1.1074 +#484 := [unit-resolution #477 #442 #483]: false
  1.1075 +#486 := [lemma #484]: #654
  1.1076 +#295 := (or #649 #646)
  1.1077 +#634 := (or #633 #649 #646)
  1.1078 +#305 := (= #69 #63)
  1.1079 +#310 := (or #649 #305)
  1.1080 +#635 := (or #633 #310)
  1.1081 +#641 := (iff #635 #634)
  1.1082 +#637 := (or #633 #295)
  1.1083 +#276 := (iff #637 #634)
  1.1084 +#639 := [rewrite]: #276
  1.1085 +#632 := (iff #635 #637)
  1.1086 +#296 := (iff #310 #295)
  1.1087 +#306 := (iff #305 #646)
  1.1088 +#294 := [rewrite]: #306
  1.1089 +#297 := [monotonicity #294]: #296
  1.1090 +#638 := [monotonicity #297]: #632
  1.1091 +#281 := [trans #638 #639]: #641
  1.1092 +#636 := [quant-inst #63]: #635
  1.1093 +#282 := [mp #636 #281]: #634
  1.1094 +#460 := [unit-resolution #282 #669]: #295
  1.1095 +#461 := [unit-resolution #460 #486]: #646
  1.1096 +#462 := (not #646)
  1.1097 +#463 := (or #462 #640)
  1.1098 +#464 := [th-lemma arith triangle-eq]: #463
  1.1099 +#465 := [unit-resolution #464 #461]: #640
  1.1100 +#588 := (>= #12 0::Int)
  1.1101 +#526 := (= #12 0::Int)
  1.1102 +#330 := (f5 f6 #12)
  1.1103 +#490 := (f3 f4 #330)
  1.1104 +#492 := (= #490 0::Int)
  1.1105 +#533 := (not #588)
  1.1106 +#528 := [hypothesis]: #533
  1.1107 +#485 := (or #588 #492)
  1.1108 +#495 := (or #353 #588 #492)
  1.1109 +#496 := (or #353 #485)
  1.1110 +#590 := (iff #496 #495)
  1.1111 +#587 := [rewrite]: #590
  1.1112 +#497 := [quant-inst #12]: #496
  1.1113 +#591 := [mp #497 #587]: #495
  1.1114 +#529 := [unit-resolution #591 #675]: #485
  1.1115 +#524 := [unit-resolution #529 #528]: #492
  1.1116 +#505 := (= #12 #490)
  1.1117 +#503 := (= f8 #330)
  1.1118 +#334 := (= #330 f8)
  1.1119 +#644 := (or #313 #334)
  1.1120 +#318 := [quant-inst #11]: #644
  1.1121 +#530 := [unit-resolution #318 #662]: #334
  1.1122 +#504 := [symm #530]: #503
  1.1123 +#398 := [monotonicity #504]: #505
  1.1124 +#509 := [trans #398 #524]: #526
  1.1125 +#510 := (not #526)
  1.1126 +#511 := (or #510 #588)
  1.1127 +#516 := [th-lemma arith triangle-eq]: #511
  1.1128 +#512 := [unit-resolution #516 #528 #509]: false
  1.1129 +#513 := [lemma #512]: #588
  1.1130 +#525 := (not #640)
  1.1131 +#522 := (or #533 #539 #525 #521)
  1.1132 +#534 := [hypothesis]: #540
  1.1133 +#535 := [hypothesis]: #588
  1.1134 +#536 := [hypothesis]: #640
  1.1135 +#537 := [hypothesis]: #594
  1.1136 +#538 := [th-lemma arith farkas -1 1 -1 -1 1 #113 #537 #536 #535 #534]: false
  1.1137 +#523 := [lemma #538]: #522
  1.1138 +#467 := [unit-resolution #523 #513 #465]: #466
  1.1139 +#468 := [unit-resolution #467 #455]: #521
  1.1140 +#327 := (= #10 #94)
  1.1141 +#320 := (or #91 #327)
  1.1142 +#331 := [def-axiom]: #320
  1.1143 +#469 := [unit-resolution #331 #487]: #327
  1.1144 +#470 := (not #327)
  1.1145 +#471 := (or #470 #540)
  1.1146 +#456 := [th-lemma arith triangle-eq]: #471
  1.1147 +#472 := [unit-resolution #456 #469 #468]: false
  1.1148 +#433 := [lemma #472]: #91
  1.1149 +#434 := [unit-resolution #482 #433]: #620
  1.1150 +#441 := [unit-resolution #508 #434]: #459
  1.1151 +#443 := [unit-resolution #329 #433]: #242
  1.1152 +#444 := [unit-resolution #477 #443]: #574
  1.1153 +#445 := (or #349 #525 #243)
  1.1154 +#447 := [th-lemma arith assign-bounds 1 -1]: #445
  1.1155 +#448 := [unit-resolution #447 #465 #433]: #349
  1.1156 +#449 := (or #555 #557 #558)
  1.1157 +#450 := [unit-resolution #556 #531]: #449
  1.1158 +[unit-resolution #450 #448 #444 #441]: false
  1.1159 +unsat
  1.1160 +a792a04eb456fe8e05c404760a48764de177c4d7 109 0
  1.1161 +#2 := false
  1.1162 +#28 := 0::Int
  1.1163 +decl f3 :: (-> S2 S3 Int)
  1.1164 +decl f5 :: S3
  1.1165 +#8 := f5
  1.1166 +decl f4 :: S2
  1.1167 +#7 := f4
  1.1168 +#9 := (f3 f4 f5)
  1.1169 +decl f7 :: S3
  1.1170 +#13 := f7
  1.1171 +#14 := (f3 f4 f7)
  1.1172 +#67 := -1::Int
  1.1173 +#74 := (* -1::Int #14)
  1.1174 +#86 := (+ #9 #74)
  1.1175 +#87 := (<= #86 0::Int)
  1.1176 +#90 := (if #87 #14 #9)
  1.1177 +#96 := (* -1::Int #90)
  1.1178 +decl f6 :: S3
  1.1179 +#10 := f6
  1.1180 +#11 := (f3 f4 f6)
  1.1181 +#97 := (+ #11 #96)
  1.1182 +#98 := (<= #97 0::Int)
  1.1183 +#99 := (not #98)
  1.1184 +#75 := (+ #11 #74)
  1.1185 +#76 := (<= #75 0::Int)
  1.1186 +#77 := (not #76)
  1.1187 +#70 := (* -1::Int #11)
  1.1188 +#71 := (+ #9 #70)
  1.1189 +#69 := (>= #71 0::Int)
  1.1190 +#68 := (not #69)
  1.1191 +#80 := (and #68 #77)
  1.1192 +#83 := (not #80)
  1.1193 +#104 := (or #83 #99)
  1.1194 +#107 := (not #104)
  1.1195 +#17 := (<= #9 #14)
  1.1196 +#18 := (if #17 #14 #9)
  1.1197 +#19 := (< #18 #11)
  1.1198 +#15 := (< #14 #11)
  1.1199 +#12 := (< #9 #11)
  1.1200 +#16 := (and #12 #15)
  1.1201 +#20 := (implies #16 #19)
  1.1202 +#21 := (not #20)
  1.1203 +#110 := (iff #21 #107)
  1.1204 +#60 := (not #16)
  1.1205 +#61 := (or #60 #19)
  1.1206 +#64 := (not #61)
  1.1207 +#108 := (iff #64 #107)
  1.1208 +#105 := (iff #61 #104)
  1.1209 +#102 := (iff #19 #99)
  1.1210 +#93 := (< #90 #11)
  1.1211 +#100 := (iff #93 #99)
  1.1212 +#101 := [rewrite]: #100
  1.1213 +#94 := (iff #19 #93)
  1.1214 +#91 := (= #18 #90)
  1.1215 +#88 := (iff #17 #87)
  1.1216 +#89 := [rewrite]: #88
  1.1217 +#92 := [monotonicity #89]: #91
  1.1218 +#95 := [monotonicity #92]: #94
  1.1219 +#103 := [trans #95 #101]: #102
  1.1220 +#84 := (iff #60 #83)
  1.1221 +#81 := (iff #16 #80)
  1.1222 +#78 := (iff #15 #77)
  1.1223 +#79 := [rewrite]: #78
  1.1224 +#72 := (iff #12 #68)
  1.1225 +#73 := [rewrite]: #72
  1.1226 +#82 := [monotonicity #73 #79]: #81
  1.1227 +#85 := [monotonicity #82]: #84
  1.1228 +#106 := [monotonicity #85 #103]: #105
  1.1229 +#109 := [monotonicity #106]: #108
  1.1230 +#65 := (iff #21 #64)
  1.1231 +#62 := (iff #20 #61)
  1.1232 +#63 := [rewrite]: #62
  1.1233 +#66 := [monotonicity #63]: #65
  1.1234 +#111 := [trans #66 #109]: #110
  1.1235 +#59 := [asserted]: #21
  1.1236 +#112 := [mp #59 #111]: #107
  1.1237 +#116 := [not-or-elim #112]: #98
  1.1238 +#113 := [not-or-elim #112]: #80
  1.1239 +#114 := [and-elim #113]: #68
  1.1240 +#644 := (+ #9 #96)
  1.1241 +#627 := (>= #644 0::Int)
  1.1242 +#330 := (= #9 #90)
  1.1243 +#246 := (not #87)
  1.1244 +#245 := (= #14 #90)
  1.1245 +#628 := (not #245)
  1.1246 +#642 := (+ #14 #96)
  1.1247 +#633 := (>= #642 0::Int)
  1.1248 +#357 := (not #633)
  1.1249 +#115 := [and-elim #113]: #77
  1.1250 +#355 := [hypothesis]: #633
  1.1251 +#356 := [th-lemma arith farkas -1 -1 1 #355 #115 #116]: false
  1.1252 +#358 := [lemma #356]: #357
  1.1253 +#252 := [hypothesis]: #245
  1.1254 +#629 := (or #628 #633)
  1.1255 +#351 := [th-lemma arith triangle-eq]: #629
  1.1256 +#352 := [unit-resolution #351 #252 #358]: false
  1.1257 +#626 := [lemma #352]: #628
  1.1258 +#331 := (or #246 #245)
  1.1259 +#332 := [def-axiom]: #331
  1.1260 +#631 := [unit-resolution #332 #626]: #246
  1.1261 +#323 := (or #87 #330)
  1.1262 +#334 := [def-axiom]: #323
  1.1263 +#341 := [unit-resolution #334 #631]: #330
  1.1264 +#342 := (not #330)
  1.1265 +#343 := (or #342 #627)
  1.1266 +#344 := [th-lemma arith triangle-eq]: #343
  1.1267 +#622 := [unit-resolution #344 #341]: #627
  1.1268 +[th-lemma arith farkas -1 1 1 #622 #114 #116]: false
  1.1269 +unsat
  1.1270 +06ea32eecccdf6605c3b038ea8337a1d74e482b8 137 0
  1.1271 +#2 := false
  1.1272 +decl f5 :: S3
  1.1273 +#8 := f5
  1.1274 +decl f6 :: (-> S4 Int S3)
  1.1275 +#10 := 0::Int
  1.1276 +decl f7 :: S4
  1.1277 +#12 := f7
  1.1278 +#13 := (f6 f7 0::Int)
  1.1279 +decl f3 :: (-> S2 S3 Int)
  1.1280 +decl f4 :: S2
  1.1281 +#7 := f4
  1.1282 +#9 := (f3 f4 f5)
  1.1283 +#11 := (<= #9 0::Int)
  1.1284 +#14 := (if #11 #13 f5)
  1.1285 +#266 := (= f5 #14)
  1.1286 +#181 := (= #13 #14)
  1.1287 +#568 := (not #266)
  1.1288 +#15 := (= #14 f5)
  1.1289 +#16 := (not #15)
  1.1290 +#278 := (iff #16 #568)
  1.1291 +#567 := (iff #15 #266)
  1.1292 +#564 := [commutativity]: #567
  1.1293 +#279 := [monotonicity #564]: #278
  1.1294 +#52 := [asserted]: #16
  1.1295 +#280 := [mp #52 #279]: #568
  1.1296 +#259 := (or #11 #266)
  1.1297 +#270 := [def-axiom]: #259
  1.1298 +#281 := [unit-resolution #270 #280]: #11
  1.1299 +#182 := (not #11)
  1.1300 +#267 := (or #182 #181)
  1.1301 +#268 := [def-axiom]: #267
  1.1302 +#548 := [unit-resolution #268 #281]: #181
  1.1303 +#399 := (= f5 #13)
  1.1304 +#272 := (f6 f7 #9)
  1.1305 +#397 := (= #272 #13)
  1.1306 +#274 := (= #9 0::Int)
  1.1307 +#252 := (f3 f4 #272)
  1.1308 +#377 := (= #252 0::Int)
  1.1309 +#273 := (>= #9 0::Int)
  1.1310 +#289 := (not #377)
  1.1311 +#563 := [hypothesis]: #289
  1.1312 +#584 := (or #273 #377)
  1.1313 +#22 := (:var 0 Int)
  1.1314 +#24 := (f6 f7 #22)
  1.1315 +#603 := (pattern #24)
  1.1316 +#25 := (f3 f4 #24)
  1.1317 +#30 := (= #25 0::Int)
  1.1318 +#64 := (>= #22 0::Int)
  1.1319 +#94 := (or #64 #30)
  1.1320 +#610 := (forall (vars (?v0 Int)) (:pat #603) #94)
  1.1321 +#97 := (forall (vars (?v0 Int)) #94)
  1.1322 +#613 := (iff #97 #610)
  1.1323 +#611 := (iff #94 #94)
  1.1324 +#612 := [refl]: #611
  1.1325 +#614 := [quant-intro #612]: #613
  1.1326 +#110 := (~ #97 #97)
  1.1327 +#118 := (~ #94 #94)
  1.1328 +#119 := [refl]: #118
  1.1329 +#111 := [nnf-pos #119]: #110
  1.1330 +#29 := (< #22 0::Int)
  1.1331 +#31 := (implies #29 #30)
  1.1332 +#32 := (forall (vars (?v0 Int)) #31)
  1.1333 +#100 := (iff #32 #97)
  1.1334 +#78 := (not #29)
  1.1335 +#79 := (or #78 #30)
  1.1336 +#82 := (forall (vars (?v0 Int)) #79)
  1.1337 +#98 := (iff #82 #97)
  1.1338 +#95 := (iff #79 #94)
  1.1339 +#92 := (iff #78 #64)
  1.1340 +#65 := (not #64)
  1.1341 +#87 := (not #65)
  1.1342 +#90 := (iff #87 #64)
  1.1343 +#91 := [rewrite]: #90
  1.1344 +#88 := (iff #78 #87)
  1.1345 +#85 := (iff #29 #65)
  1.1346 +#86 := [rewrite]: #85
  1.1347 +#89 := [monotonicity #86]: #88
  1.1348 +#93 := [trans #89 #91]: #92
  1.1349 +#96 := [monotonicity #93]: #95
  1.1350 +#99 := [quant-intro #96]: #98
  1.1351 +#83 := (iff #32 #82)
  1.1352 +#80 := (iff #31 #79)
  1.1353 +#81 := [rewrite]: #80
  1.1354 +#84 := [quant-intro #81]: #83
  1.1355 +#101 := [trans #84 #99]: #100
  1.1356 +#77 := [asserted]: #32
  1.1357 +#102 := [mp #77 #101]: #97
  1.1358 +#120 := [mp~ #102 #111]: #97
  1.1359 +#615 := [mp #120 #614]: #610
  1.1360 +#591 := (not #610)
  1.1361 +#592 := (or #591 #273 #377)
  1.1362 +#593 := (or #591 #584)
  1.1363 +#589 := (iff #593 #592)
  1.1364 +#595 := [rewrite]: #589
  1.1365 +#594 := [quant-inst #9]: #593
  1.1366 +#585 := [mp #594 #595]: #592
  1.1367 +#559 := [unit-resolution #585 #615]: #584
  1.1368 +#560 := [unit-resolution #559 #563]: #273
  1.1369 +#557 := [th-lemma arith eq-propagate 0 0 #560 #281]: #274
  1.1370 +#558 := (= #252 #9)
  1.1371 +#269 := (= #272 f5)
  1.1372 +#17 := (:var 0 S3)
  1.1373 +#18 := (f3 f4 #17)
  1.1374 +#596 := (pattern #18)
  1.1375 +#19 := (f6 f7 #18)
  1.1376 +#20 := (= #19 #17)
  1.1377 +#597 := (forall (vars (?v0 S3)) (:pat #596) #20)
  1.1378 +#21 := (forall (vars (?v0 S3)) #20)
  1.1379 +#600 := (iff #21 #597)
  1.1380 +#598 := (iff #20 #20)
  1.1381 +#599 := [refl]: #598
  1.1382 +#601 := [quant-intro #599]: #600
  1.1383 +#116 := (~ #21 #21)
  1.1384 +#114 := (~ #20 #20)
  1.1385 +#115 := [refl]: #114
  1.1386 +#117 := [nnf-pos #115]: #116
  1.1387 +#53 := [asserted]: #21
  1.1388 +#106 := [mp~ #53 #117]: #21
  1.1389 +#602 := [mp #106 #601]: #597
  1.1390 +#588 := (not #597)
  1.1391 +#590 := (or #588 #269)
  1.1392 +#246 := [quant-inst #8]: #590
  1.1393 +#561 := [unit-resolution #246 #602]: #269
  1.1394 +#562 := [monotonicity #561]: #558
  1.1395 +#551 := [trans #562 #557]: #377
  1.1396 +#552 := [unit-resolution #563 #551]: false
  1.1397 +#553 := [lemma #552]: #377
  1.1398 +#555 := (= #9 #252)
  1.1399 +#549 := (= f5 #272)
  1.1400 +#554 := [symm #561]: #549
  1.1401 +#550 := [monotonicity #554]: #555
  1.1402 +#556 := [trans #550 #553]: #274
  1.1403 +#398 := [monotonicity #556]: #397
  1.1404 +#541 := [trans #554 #398]: #399
  1.1405 +#542 := [trans #541 #548]: #266
  1.1406 +[unit-resolution #280 #542]: false
  1.1407 +unsat
     2.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Thu Dec 20 15:51:27 2012 +0100
     2.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Fri Dec 21 13:33:54 2012 +0100
     2.3 @@ -346,6 +346,14 @@
     2.4  
     2.5  (* unfolding of definitions and theory-specific rewritings *)
     2.6  
     2.7 +fun expand_head_conv cv ct =
     2.8 +  (case Thm.term_of ct of
     2.9 +    _ $ _ =>
    2.10 +      Conv.fun_conv (expand_head_conv cv) then_conv
    2.11 +      Conv.try_conv (Thm.beta_conversion false)
    2.12 +  | _ => cv) ct
    2.13 +
    2.14 +
    2.15  (** rewrite bool case expressions as if expressions **)
    2.16  
    2.17  local
    2.18 @@ -355,7 +363,9 @@
    2.19    val thm = mk_meta_eq @{lemma
    2.20      "bool_case = (%x y P. if P then x else y)" by (rule ext)+ simp}
    2.21  
    2.22 -  fun unfold_conv _ = SMT_Utils.if_true_conv is_bool_case (Conv.rewr_conv thm)
    2.23 +  fun unfold_conv _ =
    2.24 +    SMT_Utils.if_true_conv (is_bool_case o Term.head_of)
    2.25 +      (expand_head_conv (Conv.rewr_conv thm))
    2.26  in
    2.27  
    2.28  fun rewrite_bool_case_conv ctxt =
    2.29 @@ -393,8 +403,8 @@
    2.30      | abs_min_max _ _ = NONE
    2.31  
    2.32    fun unfold_amm_conv ctxt ct =
    2.33 -    (case abs_min_max ctxt (Thm.term_of ct) of
    2.34 -      SOME thm => Conv.rewr_conv thm
    2.35 +    (case abs_min_max ctxt (Term.head_of (Thm.term_of ct)) of
    2.36 +      SOME thm => expand_head_conv (Conv.rewr_conv thm)
    2.37      | NONE => Conv.all_conv) ct
    2.38  in
    2.39  
    2.40 @@ -460,8 +470,11 @@
    2.41      "int (n * m) = int n * int m"
    2.42      "int (n div m) = int n div int m"
    2.43      "int (n mod m) = int n mod int m"
    2.44 +    by (auto simp add: int_mult zdiv_int zmod_int)}
    2.45 +
    2.46 +  val int_if = mk_meta_eq @{lemma
    2.47      "int (if P then n else m) = (if P then int n else int m)"
    2.48 -    by (auto simp add: int_mult zdiv_int zmod_int)}
    2.49 +    by simp}
    2.50  
    2.51    fun mk_number_eq ctxt i lhs =
    2.52      let
    2.53 @@ -471,12 +484,8 @@
    2.54        fun tac _ = Simplifier.simp_tac (Simplifier.context ctxt ss) 1       
    2.55      in Goal.norm_result (Goal.prove_internal [] eq tac) end
    2.56  
    2.57 -  fun expand_head_conv cv ct =
    2.58 -    (case Thm.term_of ct of
    2.59 -      _ $ _ =>
    2.60 -        Conv.fun_conv (expand_head_conv cv) then_conv
    2.61 -        Thm.beta_conversion false
    2.62 -    | _ => cv) ct
    2.63 +  fun ite_conv cv1 cv2 =
    2.64 +    Conv.combination_conv (Conv.combination_conv (Conv.arg_conv cv1) cv2) cv2
    2.65  
    2.66    fun int_conv ctxt ct =
    2.67      (case Thm.term_of ct of
    2.68 @@ -484,7 +493,9 @@
    2.69          Conv.rewr_conv (mk_number_eq ctxt (snd (HOLogic.dest_number n)) ct)
    2.70      | @{const of_nat (int)} $ _ =>
    2.71          (Conv.rewrs_conv ints then_conv Conv.sub_conv ints_conv ctxt) else_conv
    2.72 -        Conv.sub_conv (Conv.top_sweep_conv nat_conv) ctxt        
    2.73 +        (Conv.rewr_conv int_if then_conv
    2.74 +          ite_conv (nat_conv ctxt) (int_conv ctxt)) else_conv
    2.75 +        Conv.sub_conv (Conv.top_sweep_conv nat_conv) ctxt
    2.76      | _ => Conv.no_conv) ct
    2.77  
    2.78    and ints_conv ctxt = Conv.top_sweep_conv int_conv ctxt