src/HOL/SMT/Examples/cert/z3_hol_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
decl uf_1 :: (-> int T1)
#37 := 6::int
#38 := (uf_1 6::int)
decl uf_3 :: (-> T1 T1)
decl uf_2 :: (-> T1 int)
#30 := 4::int
#31 := (uf_1 4::int)
#32 := (uf_3 #31)
#33 := (uf_2 #32)
#34 := (* 4::int #33)
#35 := (uf_1 #34)
#36 := (uf_3 #35)
#39 := (= #36 #38)
#548 := (uf_3 #38)
#394 := (= #548 #38)
#549 := (= #38 #548)
#523 := (uf_2 #38)
#142 := -10::int
#513 := (+ -10::int #523)
#537 := (uf_1 #513)
#538 := (uf_3 #537)
#514 := (= #538 #548)
#22 := 10::int
#539 := (>= #523 10::int)
#506 := (ite #539 #514 #549)
#4 := (:var 0 T1)
#21 := (uf_3 #4)
#708 := (pattern #21)
#5 := (uf_2 #4)
#687 := (pattern #5)
#209 := (= #4 #21)
#143 := (+ -10::int #5)
#146 := (uf_1 #143)
#149 := (uf_3 #146)
#208 := (= #21 #149)
#163 := (>= #5 10::int)
#190 := (ite #163 #208 #209)
#709 := (forall (vars (?x4 T1)) (:pat #687 #708) #190)
#193 := (forall (vars (?x4 T1)) #190)
#712 := (iff #193 #709)
#710 := (iff #190 #190)
#711 := [refl]: #710
#713 := [quant-intro #711]: #712
#168 := (ite #163 #149 #4)
#173 := (= #21 #168)
#176 := (forall (vars (?x4 T1)) #173)
#210 := (iff #176 #193)
#191 := (iff #173 #190)
#192 := [rewrite]: #191
#211 := [quant-intro #192]: #210
#188 := (~ #176 #176)
#205 := (~ #173 #173)
#206 := [refl]: #205
#189 := [nnf-pos #206]: #188
#24 := (- #5 10::int)
#25 := (uf_1 #24)
#26 := (uf_3 #25)
#23 := (< #5 10::int)
#27 := (ite #23 #4 #26)
#28 := (= #21 #27)
#29 := (forall (vars (?x4 T1)) #28)
#179 := (iff #29 #176)
#152 := (ite #23 #4 #149)
#155 := (= #21 #152)
#158 := (forall (vars (?x4 T1)) #155)
#177 := (iff #158 #176)
#174 := (iff #155 #173)
#171 := (= #152 #168)
#161 := (not #163)
#165 := (ite #161 #4 #149)
#169 := (= #165 #168)
#170 := [rewrite]: #169
#166 := (= #152 #165)
#162 := (iff #23 #161)
#164 := [rewrite]: #162
#167 := [monotonicity #164]: #166
#172 := [trans #167 #170]: #171
#175 := [monotonicity #172]: #174
#178 := [quant-intro #175]: #177
#159 := (iff #29 #158)
#156 := (iff #28 #155)
#153 := (= #27 #152)
#150 := (= #26 #149)
#147 := (= #25 #146)
#144 := (= #24 #143)
#145 := [rewrite]: #144
#148 := [monotonicity #145]: #147
#151 := [monotonicity #148]: #150
#154 := [monotonicity #151]: #153
#157 := [monotonicity #154]: #156
#160 := [quant-intro #157]: #159
#180 := [trans #160 #178]: #179
#141 := [asserted]: #29
#181 := [mp #141 #180]: #176
#207 := [mp~ #181 #189]: #176
#212 := [mp #207 #211]: #193
#714 := [mp #212 #713]: #709
#681 := (not #709)
#517 := (or #681 #506)
#533 := (= #548 #538)
#507 := (ite #539 #533 #549)
#518 := (or #681 #507)
#529 := (iff #518 #517)
#530 := (iff #517 #517)
#485 := [rewrite]: #530
#508 := (iff #507 #506)
#473 := (iff #533 #514)
#504 := [rewrite]: #473
#515 := [monotonicity #504]: #508
#509 := [monotonicity #515]: #529
#486 := [trans #509 #485]: #529
#519 := [quant-inst]: #518
#491 := [mp #519 #486]: #517
#484 := [unit-resolution #491 #714]: #506
#493 := (not #539)
#465 := (<= #523 6::int)
#526 := (= #523 6::int)
#10 := (:var 0 int)
#12 := (uf_1 #10)
#695 := (pattern #12)
#9 := 0::int
#82 := (>= #10 0::int)
#83 := (not #82)
#13 := (uf_2 #12)
#64 := (= #10 #13)
#89 := (or #64 #83)
#696 := (forall (vars (?x2 int)) (:pat #695) #89)
#94 := (forall (vars (?x2 int)) #89)
#699 := (iff #94 #696)
#697 := (iff #89 #89)
#698 := [refl]: #697
#700 := [quant-intro #698]: #699
#185 := (~ #94 #94)
#199 := (~ #89 #89)
#200 := [refl]: #199
#183 := [nnf-pos #200]: #185
#14 := (= #13 #10)
#11 := (<= 0::int #10)
#15 := (implies #11 #14)
#16 := (forall (vars (?x2 int)) #15)
#97 := (iff #16 #94)
#71 := (not #11)
#72 := (or #71 #64)
#77 := (forall (vars (?x2 int)) #72)
#95 := (iff #77 #94)
#92 := (iff #72 #89)
#86 := (or #83 #64)
#90 := (iff #86 #89)
#91 := [rewrite]: #90
#87 := (iff #72 #86)
#84 := (iff #71 #83)
#80 := (iff #11 #82)
#81 := [rewrite]: #80
#85 := [monotonicity #81]: #84
#88 := [monotonicity #85]: #87
#93 := [trans #88 #91]: #92
#96 := [quant-intro #93]: #95
#78 := (iff #16 #77)
#75 := (iff #15 #72)
#68 := (implies #11 #64)
#73 := (iff #68 #72)
#74 := [rewrite]: #73
#69 := (iff #15 #68)
#66 := (iff #14 #64)
#67 := [rewrite]: #66
#70 := [monotonicity #67]: #69
#76 := [trans #70 #74]: #75
#79 := [quant-intro #76]: #78
#98 := [trans #79 #96]: #97
#63 := [asserted]: #16
#99 := [mp #63 #98]: #94
#201 := [mp~ #99 #183]: #94
#701 := [mp #201 #700]: #696
#671 := (not #696)
#615 := (or #671 #526)
#520 := (>= 6::int 0::int)
#522 := (not #520)
#516 := (= 6::int #523)
#524 := (or #516 #522)
#604 := (or #671 #524)
#606 := (iff #604 #615)
#601 := (iff #615 #615)
#608 := [rewrite]: #601
#614 := (iff #524 #526)
#603 := (or #526 false)
#612 := (iff #603 #526)
#613 := [rewrite]: #612
#600 := (iff #524 #603)
#609 := (iff #522 false)
#1 := true
#327 := (not true)
#666 := (iff #327 false)
#667 := [rewrite]: #666
#618 := (iff #522 #327)
#528 := (iff #520 true)
#621 := [rewrite]: #528
#622 := [monotonicity #621]: #618
#611 := [trans #622 #667]: #609
#525 := (iff #516 #526)
#527 := [rewrite]: #525
#602 := [monotonicity #527 #611]: #600
#610 := [trans #602 #613]: #614
#607 := [monotonicity #610]: #606
#592 := [trans #607 #608]: #606
#605 := [quant-inst]: #604
#593 := [mp #605 #592]: #615
#454 := [unit-resolution #593 #701]: #526
#303 := (not #526)
#462 := (or #303 #465)
#458 := [th-lemma]: #462
#463 := [unit-resolution #458 #454]: #465
#442 := (not #465)
#445 := (or #442 #493)
#449 := [th-lemma]: #445
#451 := [unit-resolution #449 #463]: #493
#492 := (not #506)
#496 := (or #492 #539 #549)
#497 := [def-axiom]: #496
#452 := [unit-resolution #497 #451 #484]: #549
#395 := [symm #452]: #394
#397 := (= #36 #548)
#372 := (uf_2 #35)
#576 := (+ -10::int #372)
#568 := (uf_1 #576)
#569 := (uf_3 #568)
#408 := (= #569 #548)
#401 := (= #568 #38)
#422 := (= #576 6::int)
#677 := (uf_2 #31)
#365 := -1::int
#478 := (* -1::int #677)
#479 := (+ #33 #478)
#480 := (<= #479 0::int)
#476 := (= #33 #677)
#431 := (= #32 #31)
#589 := (= #31 #32)
#590 := (+ -10::int #677)
#587 := (uf_1 #590)
#591 := (uf_3 #587)
#571 := (= #32 #591)
#572 := (>= #677 10::int)
#574 := (ite #572 #571 #589)
#577 := (or #681 #574)
#578 := [quant-inst]: #577
#450 := [unit-resolution #578 #714]: #574
#580 := (not #572)
#552 := (<= #677 4::int)
#324 := (= #677 4::int)
#674 := (or #671 #324)
#343 := (>= 4::int 0::int)
#679 := (not #343)
#336 := (= 4::int #677)
#678 := (or #336 #679)
#660 := (or #671 #678)
#368 := (iff #660 #674)
#384 := (iff #674 #674)
#385 := [rewrite]: #384
#312 := (iff #678 #324)
#669 := (or #324 false)
#672 := (iff #669 #324)
#311 := [rewrite]: #672
#306 := (iff #678 #669)
#668 := (iff #679 false)
#664 := (iff #679 #327)
#325 := (iff #343 true)
#326 := [rewrite]: #325
#665 := [monotonicity #326]: #664
#663 := [trans #665 #667]: #668
#320 := (iff #336 #324)
#662 := [rewrite]: #320
#670 := [monotonicity #662 #663]: #306
#673 := [trans #670 #311]: #312
#383 := [monotonicity #673]: #368
#386 := [trans #383 #385]: #368
#661 := [quant-inst]: #660
#278 := [mp #661 #386]: #674
#453 := [unit-resolution #278 #701]: #324
#441 := (not #324)
#444 := (or #441 #552)
#446 := [th-lemma]: #444
#447 := [unit-resolution #446 #453]: #552
#443 := (not #552)
#448 := (or #443 #580)
#438 := [th-lemma]: #448
#428 := [unit-resolution #438 #447]: #580
#579 := (not #574)
#583 := (or #579 #572 #589)
#573 := [def-axiom]: #583
#430 := [unit-resolution #573 #428 #450]: #589
#434 := [symm #430]: #431
#435 := [monotonicity #434]: #476
#439 := (not #476)
#432 := (or #439 #480)
#440 := [th-lemma]: #432
#433 := [unit-resolution #440 #435]: #480
#481 := (>= #479 0::int)
#436 := (or #439 #481)
#437 := [th-lemma]: #436
#423 := [unit-resolution #437 #435]: #481
#553 := (>= #677 4::int)
#425 := (or #441 #553)
#426 := [th-lemma]: #425
#424 := [unit-resolution #426 #453]: #553
#648 := (* -1::int #372)
#652 := (+ #34 #648)
#631 := (<= #652 0::int)
#649 := (= #652 0::int)
#370 := (>= #34 0::int)
#409 := (not #481)
#427 := (not #553)
#411 := (or #370 #427 #409)
#412 := [th-lemma]: #411
#413 := [unit-resolution #412 #424 #423]: #370
#371 := (not #370)
#640 := (or #371 #649)
#488 := (or #671 #371 #649)
#650 := (= #34 #372)
#651 := (or #650 #371)
#489 := (or #671 #651)
#630 := (iff #489 #488)
#632 := (or #671 #640)
#635 := (iff #632 #488)
#629 := [rewrite]: #635
#633 := (iff #489 #632)
#641 := (iff #651 #640)
#643 := (or #649 #371)
#645 := (iff #643 #640)
#646 := [rewrite]: #645
#644 := (iff #651 #643)
#653 := (iff #650 #649)
#642 := [rewrite]: #653
#639 := [monotonicity #642]: #644
#647 := [trans #639 #646]: #641
#634 := [monotonicity #647]: #633
#636 := [trans #634 #629]: #630
#490 := [quant-inst]: #489
#637 := [mp #490 #636]: #488
#414 := [unit-resolution #637 #701]: #640
#415 := [unit-resolution #414 #413]: #649
#416 := (not #649)
#417 := (or #416 #631)
#418 := [th-lemma]: #417
#419 := [unit-resolution #418 #415]: #631
#638 := (>= #652 0::int)
#420 := (or #416 #638)
#421 := [th-lemma]: #420
#410 := [unit-resolution #421 #415]: #638
#399 := [th-lemma #410 #419 #424 #447 #423 #433]: #422
#402 := [monotonicity #399]: #401
#393 := [monotonicity #402]: #408
#564 := (= #36 #569)
#575 := (= #35 #36)
#570 := (>= #372 10::int)
#556 := (ite #570 #564 #575)
#554 := (or #681 #556)
#557 := [quant-inst]: #554
#403 := [unit-resolution #557 #714]: #556
#404 := (not #631)
#405 := (or #570 #404 #427 #409)
#406 := [th-lemma]: #405
#407 := [unit-resolution #406 #419 #424 #423]: #570
#559 := (not #570)
#558 := (not #556)
#560 := (or #558 #559 #564)
#555 := [def-axiom]: #560
#400 := [unit-resolution #555 #407 #403]: #564
#396 := [trans #400 #393]: #397
#398 := [trans #396 #395]: #39
#40 := (not #39)
#182 := [asserted]: #40
[unit-resolution #182 #398]: false
unsat