src/HOL/SMT/Examples/cert/z3_nat_arith_07.proof

added proof reconstructon for Z3,
added certificates for simpler re-checking of proofs (no need to invoke external solvers),
added examples and certificates for all examples,
removed Unsynchronized.ref (in smt_normalize.ML)

#2 := false
#9 := 0::int
decl uf_2 :: (-> T1 int)
decl uf_1 :: (-> int T1)
decl uf_5 :: T1
#36 := uf_5
#37 := (uf_2 uf_5)
#35 := 4::int
#38 := (* 4::int #37)
#39 := (uf_1 #38)
#40 := (uf_2 #39)
#549 := (= #40 0::int)
#963 := (not #549)
#537 := (<= #40 0::int)
#958 := (not #537)
#22 := 1::int
#186 := (+ 1::int #40)
#189 := (uf_1 #186)
#524 := (uf_2 #189)
#452 := (<= #524 1::int)
#874 := (not #452)
decl up_4 :: (-> T1 T1 bool)
#4 := (:var 0 T1)
#456 := (up_4 #4 #189)
#440 := (pattern #456)
#446 := (not #456)
#455 := (= #4 #189)
#26 := (uf_1 1::int)
#27 := (= #4 #26)
#434 := (or #27 #455 #446)
#416 := (forall (vars (?x5 T1)) (:pat #440) #434)
#417 := (not #416)
#409 := (or #417 #452)
#400 := (not #409)
decl up_3 :: (-> T1 bool)
#192 := (up_3 #189)
#429 := (not #192)
#405 := (or #429 #400)
#389 := (not #405)
decl ?x5!0 :: (-> T1 T1)
#478 := (?x5!0 #189)
#479 := (= #26 #478)
#468 := (= #189 #478)
#445 := (up_4 #478 #189)
#447 := (not #445)
#396 := (or #447 #468 #479)
#391 := (not #396)
#386 := (or #192 #391 #452)
#377 := (not #386)
#843 := (or #377 #389)
#848 := (not #843)
#5 := (uf_2 #4)
#788 := (pattern #5)
#21 := (up_3 #4)
#836 := (pattern #21)
#210 := (?x5!0 #4)
#274 := (= #4 #210)
#271 := (= #26 #210)
#232 := (up_4 #210 #4)
#233 := (not #232)
#277 := (or #233 #271 #274)
#280 := (not #277)
#163 := (<= #5 1::int)
#289 := (or #21 #163 #280)
#304 := (not #289)
#24 := (:var 1 T1)
#25 := (up_4 #4 #24)
#809 := (pattern #25)
#28 := (= #4 #24)
#147 := (not #25)
#167 := (or #147 #27 #28)
#810 := (forall (vars (?x5 T1)) (:pat #809) #167)
#815 := (not #810)
#818 := (or #163 #815)
#821 := (not #818)
#253 := (not #21)
#824 := (or #253 #821)
#827 := (not #824)
#830 := (or #827 #304)
#833 := (not #830)
#837 := (forall (vars (?x4 T1)) (:pat #836 #788) #833)
#170 := (forall (vars (?x5 T1)) #167)
#236 := (not #170)
#239 := (or #163 #236)
#240 := (not #239)
#215 := (or #253 #240)
#303 := (not #215)
#305 := (or #303 #304)
#306 := (not #305)
#311 := (forall (vars (?x4 T1)) #306)
#838 := (iff #311 #837)
#834 := (iff #306 #833)
#831 := (iff #305 #830)
#828 := (iff #303 #827)
#825 := (iff #215 #824)
#822 := (iff #240 #821)
#819 := (iff #239 #818)
#816 := (iff #236 #815)
#813 := (iff #170 #810)
#811 := (iff #167 #167)
#812 := [refl]: #811
#814 := [quant-intro #812]: #813
#817 := [monotonicity #814]: #816
#820 := [monotonicity #817]: #819
#823 := [monotonicity #820]: #822
#826 := [monotonicity #823]: #825
#829 := [monotonicity #826]: #828
#832 := [monotonicity #829]: #831
#835 := [monotonicity #832]: #834
#839 := [quant-intro #835]: #838
#164 := (not #163)
#173 := (and #164 #170)
#259 := (or #253 #173)
#294 := (and #259 #289)
#297 := (forall (vars (?x4 T1)) #294)
#312 := (iff #297 #311)
#309 := (iff #294 #306)
#214 := (and #215 #289)
#307 := (iff #214 #306)
#308 := [rewrite]: #307
#301 := (iff #294 #214)
#216 := (iff #259 #215)
#268 := (iff #173 #240)
#300 := [rewrite]: #268
#213 := [monotonicity #300]: #216
#302 := [monotonicity #213]: #301
#310 := [trans #302 #308]: #309
#313 := [quant-intro #310]: #312
#230 := (= #210 #4)
#231 := (= #210 #26)
#234 := (or #233 #231 #230)
#235 := (not #234)
#228 := (not #164)
#241 := (or #228 #235)
#258 := (or #21 #241)
#260 := (and #259 #258)
#263 := (forall (vars (?x4 T1)) #260)
#298 := (iff #263 #297)
#295 := (iff #260 #294)
#292 := (iff #258 #289)
#283 := (or #163 #280)
#286 := (or #21 #283)
#290 := (iff #286 #289)
#291 := [rewrite]: #290
#287 := (iff #258 #286)
#284 := (iff #241 #283)
#281 := (iff #235 #280)
#278 := (iff #234 #277)
#275 := (iff #230 #274)
#276 := [rewrite]: #275
#272 := (iff #231 #271)
#273 := [rewrite]: #272
#279 := [monotonicity #273 #276]: #278
#282 := [monotonicity #279]: #281
#269 := (iff #228 #163)
#270 := [rewrite]: #269
#285 := [monotonicity #270 #282]: #284
#288 := [monotonicity #285]: #287
#293 := [trans #288 #291]: #292
#296 := [monotonicity #293]: #295
#299 := [quant-intro #296]: #298
#176 := (iff #21 #173)
#179 := (forall (vars (?x4 T1)) #176)
#264 := (~ #179 #263)
#261 := (~ #176 #260)
#251 := (~ #173 #173)
#249 := (~ #170 #170)
#247 := (~ #167 #167)
#248 := [refl]: #247
#250 := [nnf-pos #248]: #249
#245 := (~ #164 #164)
#246 := [refl]: #245
#252 := [monotonicity #246 #250]: #251
#242 := (not #173)
#243 := (~ #242 #241)
#237 := (~ #236 #235)
#238 := [sk]: #237
#229 := (~ #228 #228)
#209 := [refl]: #229
#244 := [nnf-neg #209 #238]: #243
#256 := (~ #21 #21)
#257 := [refl]: #256
#254 := (~ #253 #253)
#255 := [refl]: #254
#262 := [nnf-pos #255 #257 #244 #252]: #261
#265 := [nnf-pos #262]: #264
#29 := (or #27 #28)
#30 := (implies #25 #29)
#31 := (forall (vars (?x5 T1)) #30)
#23 := (< 1::int #5)
#32 := (and #23 #31)
#33 := (iff #21 #32)
#34 := (forall (vars (?x4 T1)) #33)
#182 := (iff #34 #179)
#148 := (or #147 #29)
#151 := (forall (vars (?x5 T1)) #148)
#154 := (and #23 #151)
#157 := (iff #21 #154)
#160 := (forall (vars (?x4 T1)) #157)
#180 := (iff #160 #179)
#177 := (iff #157 #176)
#174 := (iff #154 #173)
#171 := (iff #151 #170)
#168 := (iff #148 #167)
#169 := [rewrite]: #168
#172 := [quant-intro #169]: #171
#165 := (iff #23 #164)
#166 := [rewrite]: #165
#175 := [monotonicity #166 #172]: #174
#178 := [monotonicity #175]: #177
#181 := [quant-intro #178]: #180
#161 := (iff #34 #160)
#158 := (iff #33 #157)
#155 := (iff #32 #154)
#152 := (iff #31 #151)
#149 := (iff #30 #148)
#150 := [rewrite]: #149
#153 := [quant-intro #150]: #152
#156 := [monotonicity #153]: #155
#159 := [monotonicity #156]: #158
#162 := [quant-intro #159]: #161
#183 := [trans #162 #181]: #182
#146 := [asserted]: #34
#184 := [mp #146 #183]: #179
#266 := [mp~ #184 #265]: #263
#267 := [mp #266 #299]: #297
#314 := [mp #267 #313]: #311
#840 := [mp #314 #839]: #837
#754 := (not #837)
#851 := (or #754 #848)
#448 := (or #447 #479 #468)
#439 := (not #448)
#453 := (or #192 #452 #439)
#454 := (not #453)
#457 := (or #446 #27 #455)
#442 := (forall (vars (?x5 T1)) (:pat #440) #457)
#443 := (not #442)
#422 := (or #452 #443)
#424 := (not #422)
#430 := (or #429 #424)
#431 := (not #430)
#432 := (or #431 #454)
#433 := (not #432)
#852 := (or #754 #433)
#854 := (iff #852 #851)
#856 := (iff #851 #851)
#857 := [rewrite]: #856
#849 := (iff #433 #848)
#846 := (iff #432 #843)
#379 := (or #389 #377)
#844 := (iff #379 #843)
#845 := [rewrite]: #844
#841 := (iff #432 #379)
#378 := (iff #454 #377)
#388 := (iff #453 #386)
#381 := (or #192 #452 #391)
#387 := (iff #381 #386)
#383 := [rewrite]: #387
#382 := (iff #453 #381)
#399 := (iff #439 #391)
#397 := (iff #448 #396)
#398 := [rewrite]: #397
#384 := [monotonicity #398]: #399
#385 := [monotonicity #384]: #382
#375 := [trans #385 #383]: #388
#376 := [monotonicity #375]: #378
#392 := (iff #431 #389)
#401 := (iff #430 #405)
#402 := (iff #424 #400)
#394 := (iff #422 #409)
#410 := (or #452 #417)
#415 := (iff #410 #409)
#390 := [rewrite]: #415
#411 := (iff #422 #410)
#420 := (iff #443 #417)
#418 := (iff #442 #416)
#423 := (iff #457 #434)
#435 := [rewrite]: #423
#419 := [quant-intro #435]: #418
#408 := [monotonicity #419]: #420
#414 := [monotonicity #408]: #411
#395 := [trans #414 #390]: #394
#403 := [monotonicity #395]: #402
#406 := [monotonicity #403]: #401
#393 := [monotonicity #406]: #392
#842 := [monotonicity #393 #376]: #841
#847 := [trans #842 #845]: #846
#850 := [monotonicity #847]: #849
#855 := [monotonicity #850]: #854
#858 := [trans #855 #857]: #854
#853 := [quant-inst]: #852
#859 := [mp #853 #858]: #851
#934 := [unit-resolution #859 #840]: #848
#893 := (or #843 #405)
#894 := [def-axiom]: #893
#935 := [unit-resolution #894 #934]: #405
#938 := (or #389 #400)
#41 := (+ #40 1::int)
#42 := (uf_1 #41)
#43 := (up_3 #42)
#193 := (iff #43 #192)
#190 := (= #42 #189)
#187 := (= #41 #186)
#188 := [rewrite]: #187
#191 := [monotonicity #188]: #190
#194 := [monotonicity #191]: #193
#185 := [asserted]: #43
#197 := [mp #185 #194]: #192
#889 := (or #389 #429 #400)
#890 := [def-axiom]: #889
#939 := [unit-resolution #890 #197]: #938
#940 := [unit-resolution #939 #935]: #400
#881 := (or #409 #874)
#882 := [def-axiom]: #881
#941 := [unit-resolution #882 #940]: #874
#555 := -1::int
#525 := (* -1::int #524)
#528 := (+ #40 #525)
#494 := (>= #528 -1::int)
#510 := (= #528 -1::int)
#514 := (>= #40 -1::int)
#495 := (= #524 0::int)
#946 := (not #495)
#467 := (<= #524 0::int)
#942 := (not #467)
#943 := (or #942 #452)
#944 := [th-lemma]: #943
#945 := [unit-resolution #944 #941]: #942
#947 := (or #946 #467)
#948 := [th-lemma]: #947
#949 := [unit-resolution #948 #945]: #946
#498 := (or #495 #514)
#10 := (:var 0 int)
#12 := (uf_1 #10)
#796 := (pattern #12)
#87 := (>= #10 0::int)
#13 := (uf_2 #12)
#18 := (= #13 0::int)
#135 := (or #18 #87)
#803 := (forall (vars (?x3 int)) (:pat #796) #135)
#140 := (forall (vars (?x3 int)) #135)
#806 := (iff #140 #803)
#804 := (iff #135 #135)
#805 := [refl]: #804
#807 := [quant-intro #805]: #806
#207 := (~ #140 #140)
#225 := (~ #135 #135)
#226 := [refl]: #225
#208 := [nnf-pos #226]: #207
#17 := (< #10 0::int)
#19 := (implies #17 #18)
#20 := (forall (vars (?x3 int)) #19)
#143 := (iff #20 #140)
#106 := (= 0::int #13)
#112 := (not #17)
#113 := (or #112 #106)
#118 := (forall (vars (?x3 int)) #113)
#141 := (iff #118 #140)
#138 := (iff #113 #135)
#132 := (or #87 #18)
#136 := (iff #132 #135)
#137 := [rewrite]: #136
#133 := (iff #113 #132)
#130 := (iff #106 #18)
#131 := [rewrite]: #130
#128 := (iff #112 #87)
#88 := (not #87)
#123 := (not #88)
#126 := (iff #123 #87)
#127 := [rewrite]: #126
#124 := (iff #112 #123)
#121 := (iff #17 #88)
#122 := [rewrite]: #121
#125 := [monotonicity #122]: #124
#129 := [trans #125 #127]: #128
#134 := [monotonicity #129 #131]: #133
#139 := [trans #134 #137]: #138
#142 := [quant-intro #139]: #141
#119 := (iff #20 #118)
#116 := (iff #19 #113)
#109 := (implies #17 #106)
#114 := (iff #109 #113)
#115 := [rewrite]: #114
#110 := (iff #19 #109)
#107 := (iff #18 #106)
#108 := [rewrite]: #107
#111 := [monotonicity #108]: #110
#117 := [trans #111 #115]: #116
#120 := [quant-intro #117]: #119
#144 := [trans #120 #142]: #143
#105 := [asserted]: #20
#145 := [mp #105 #144]: #140
#227 := [mp~ #145 #208]: #140
#808 := [mp #227 #807]: #803
#532 := (not #803)
#488 := (or #532 #495 #514)
#529 := (>= #186 0::int)
#496 := (or #495 #529)
#489 := (or #532 #496)
#474 := (iff #489 #488)
#482 := (or #532 #498)
#483 := (iff #482 #488)
#493 := [rewrite]: #483
#491 := (iff #489 #482)
#497 := (iff #496 #498)
#515 := (iff #529 #514)
#516 := [rewrite]: #515
#499 := [monotonicity #516]: #497
#492 := [monotonicity #499]: #491
#475 := [trans #492 #493]: #474
#490 := [quant-inst]: #489
#476 := [mp #490 #475]: #488
#950 := [unit-resolution #476 #808]: #498
#951 := [unit-resolution #950 #949]: #514
#517 := (not #514)
#520 := (or #510 #517)
#69 := (= #10 #13)
#94 := (or #69 #88)
#797 := (forall (vars (?x2 int)) (:pat #796) #94)
#99 := (forall (vars (?x2 int)) #94)
#800 := (iff #99 #797)
#798 := (iff #94 #94)
#799 := [refl]: #798
#801 := [quant-intro #799]: #800
#206 := (~ #99 #99)
#222 := (~ #94 #94)
#223 := [refl]: #222
#196 := [nnf-pos #223]: #206
#14 := (= #13 #10)
#11 := (<= 0::int #10)
#15 := (implies #11 #14)
#16 := (forall (vars (?x2 int)) #15)
#102 := (iff #16 #99)
#76 := (not #11)
#77 := (or #76 #69)
#82 := (forall (vars (?x2 int)) #77)
#100 := (iff #82 #99)
#97 := (iff #77 #94)
#91 := (or #88 #69)
#95 := (iff #91 #94)
#96 := [rewrite]: #95
#92 := (iff #77 #91)
#89 := (iff #76 #88)
#85 := (iff #11 #87)
#86 := [rewrite]: #85
#90 := [monotonicity #86]: #89
#93 := [monotonicity #90]: #92
#98 := [trans #93 #96]: #97
#101 := [quant-intro #98]: #100
#83 := (iff #16 #82)
#80 := (iff #15 #77)
#73 := (implies #11 #69)
#78 := (iff #73 #77)
#79 := [rewrite]: #78
#74 := (iff #15 #73)
#71 := (iff #14 #69)
#72 := [rewrite]: #71
#75 := [monotonicity #72]: #74
#81 := [trans #75 #79]: #80
#84 := [quant-intro #81]: #83
#103 := [trans #84 #101]: #102
#68 := [asserted]: #16
#104 := [mp #68 #103]: #99
#224 := [mp~ #104 #196]: #99
#802 := [mp #224 #801]: #797
#559 := (not #797)
#511 := (or #559 #510 #517)
#531 := (not #529)
#526 := (= #186 #524)
#527 := (or #526 #531)
#523 := (or #559 #527)
#507 := (iff #523 #511)
#502 := (or #559 #520)
#505 := (iff #502 #511)
#506 := [rewrite]: #505
#503 := (iff #523 #502)
#521 := (iff #527 #520)
#518 := (iff #531 #517)
#519 := [monotonicity #516]: #518
#512 := (iff #526 #510)
#513 := [rewrite]: #512
#522 := [monotonicity #513 #519]: #521
#504 := [monotonicity #522]: #503
#508 := [trans #504 #506]: #507
#500 := [quant-inst]: #523
#501 := [mp #500 #508]: #511
#952 := [unit-resolution #501 #802]: #520
#953 := [unit-resolution #952 #951]: #510
#954 := (not #510)
#955 := (or #954 #494)
#956 := [th-lemma]: #955
#957 := [unit-resolution #956 #953]: #494
#959 := (not #494)
#960 := (or #958 #452 #959)
#961 := [th-lemma]: #960
#962 := [unit-resolution #961 #957 #941]: #958
#964 := (or #963 #537)
#965 := [th-lemma]: #964
#966 := [unit-resolution #965 #962]: #963
#583 := (>= #38 0::int)
#584 := (not #583)
#556 := (* -1::int #40)
#557 := (+ #38 #556)
#558 := (= #557 0::int)
#971 := (not #558)
#544 := (>= #557 0::int)
#967 := (not #544)
#201 := (>= #37 1::int)
#202 := (not #201)
#44 := (<= 1::int #37)
#45 := (not #44)
#203 := (iff #45 #202)
#199 := (iff #44 #201)
#200 := [rewrite]: #199
#204 := [monotonicity #200]: #203
#195 := [asserted]: #45
#205 := [mp #195 #204]: #202
#968 := (or #967 #201 #452 #959)
#969 := [th-lemma]: #968
#970 := [unit-resolution #969 #205 #957 #941]: #967
#972 := (or #971 #544)
#973 := [th-lemma]: #972
#974 := [unit-resolution #973 #970]: #971
#562 := (or #558 #584)
#564 := (or #559 #558 #584)
#567 := (= #38 #40)
#585 := (or #567 #584)
#543 := (or #559 #585)
#542 := (iff #543 #564)
#550 := (or #559 #562)
#551 := (iff #550 #564)
#554 := [rewrite]: #551
#552 := (iff #543 #550)
#404 := (iff #585 #562)
#560 := (iff #567 #558)
#561 := [rewrite]: #560
#563 := [monotonicity #561]: #404
#553 := [monotonicity #563]: #552
#545 := [trans #553 #554]: #542
#546 := [quant-inst]: #543
#547 := [mp #546 #545]: #564
#975 := [unit-resolution #547 #802]: #562
#976 := [unit-resolution #975 #974]: #584
#539 := (or #549 #583)
#535 := (or #532 #549 #583)
#536 := (or #532 #539)
#533 := (iff #536 #535)
#541 := [rewrite]: #533
#540 := [quant-inst]: #536
#534 := [mp #540 #541]: #535
#977 := [unit-resolution #534 #808]: #539
[unit-resolution #977 #976 #966]: false
unsat