src/HOL/SMT/Examples/cert/z3_linarith_13.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_3 :: (-> int int T1)
#18 := 3::int
decl uf_4 :: int
#17 := uf_4
#19 := (uf_3 uf_4 3::int)
decl uf_2 :: T1
#7 := uf_2
#221 := (= uf_2 #19)
decl uf_1 :: (-> int int T1)
#20 := (uf_1 3::int uf_4)
#256 := (= uf_2 #20)
#531 := (iff #256 #221)
#529 := (iff #221 #256)
#87 := (= #19 #20)
#21 := (distinct #19 #20)
#22 := (not #21)
#96 := (iff #22 #87)
#88 := (not #87)
#91 := (not #88)
#94 := (iff #91 #87)
#95 := [rewrite]: #94
#92 := (iff #22 #91)
#89 := (iff #21 #88)
#90 := [rewrite]: #89
#93 := [monotonicity #90]: #92
#97 := [trans #93 #95]: #96
#86 := [asserted]: #22
#100 := [mp #86 #97]: #87
#530 := [monotonicity #100]: #529
#525 := [symm #530]: #531
#548 := (not #221)
#232 := (not #256)
#526 := (iff #232 #548)
#532 := [monotonicity #525]: #526
#536 := [hypothesis]: #232
#533 := [mp #536 #532]: #548
#259 := (>= uf_4 3::int)
#576 := (not #259)
#542 := (or #256 #576)
#257 := (iff #256 #259)
#5 := (:var 0 int)
#4 := (:var 1 int)
#6 := (uf_1 #4 #5)
#583 := (pattern #6)
#44 := 0::int
#41 := -1::int
#42 := (* -1::int #5)
#43 := (+ #4 #42)
#45 := (<= #43 0::int)
#8 := (= #6 uf_2)
#48 := (iff #8 #45)
#584 := (forall (vars (?x1 int) (?x2 int)) (:pat #583) #48)
#51 := (forall (vars (?x1 int) (?x2 int)) #48)
#587 := (iff #51 #584)
#585 := (iff #48 #48)
#586 := [refl]: #585
#588 := [quant-intro #586]: #587
#108 := (~ #51 #51)
#106 := (~ #48 #48)
#107 := [refl]: #106
#109 := [nnf-pos #107]: #108
#9 := (<= #4 #5)
#10 := (iff #8 #9)
#11 := (forall (vars (?x1 int) (?x2 int)) #10)
#52 := (iff #11 #51)
#49 := (iff #10 #48)
#46 := (iff #9 #45)
#47 := [rewrite]: #46
#50 := [monotonicity #47]: #49
#53 := [quant-intro #50]: #52
#38 := [asserted]: #11
#54 := [mp #38 #53]: #51
#110 := [mp~ #54 #109]: #51
#589 := [mp #110 #588]: #584
#575 := (not #584)
#577 := (or #575 #257)
#167 := (* -1::int uf_4)
#254 := (+ 3::int #167)
#168 := (<= #254 0::int)
#255 := (= #20 uf_2)
#169 := (iff #255 #168)
#234 := (or #575 #169)
#571 := (iff #234 #577)
#246 := (iff #577 #577)
#578 := [rewrite]: #246
#261 := (iff #169 #257)
#187 := (iff #168 #259)
#260 := [rewrite]: #187
#247 := (iff #255 #256)
#258 := [rewrite]: #247
#240 := [monotonicity #258 #260]: #261
#245 := [monotonicity #240]: #571
#579 := [trans #245 #578]: #571
#364 := [quant-inst]: #234
#580 := [mp #364 #579]: #577
#541 := [unit-resolution #580 #589]: #257
#581 := (not #257)
#582 := (or #581 #256 #576)
#572 := [def-axiom]: #582
#537 := [unit-resolution #572 #541]: #542
#543 := [unit-resolution #537 #536]: #576
#385 := (or #221 #259)
#552 := (iff #221 #576)
#12 := (uf_3 #4 #5)
#590 := (pattern #12)
#69 := (>= #43 0::int)
#68 := (not #69)
#40 := (= uf_2 #12)
#75 := (iff #40 #68)
#591 := (forall (vars (?x3 int) (?x4 int)) (:pat #590) #75)
#80 := (forall (vars (?x3 int) (?x4 int)) #75)
#594 := (iff #80 #591)
#592 := (iff #75 #75)
#593 := [refl]: #592
#595 := [quant-intro #593]: #594
#101 := (~ #80 #80)
#111 := (~ #75 #75)
#112 := [refl]: #111
#98 := [nnf-pos #112]: #101
#14 := (< #4 #5)
#13 := (= #12 uf_2)
#15 := (iff #13 #14)
#16 := (forall (vars (?x3 int) (?x4 int)) #15)
#83 := (iff #16 #80)
#60 := (iff #14 #40)
#65 := (forall (vars (?x3 int) (?x4 int)) #60)
#81 := (iff #65 #80)
#78 := (iff #60 #75)
#72 := (iff #68 #40)
#76 := (iff #72 #75)
#77 := [rewrite]: #76
#73 := (iff #60 #72)
#70 := (iff #14 #68)
#71 := [rewrite]: #70
#74 := [monotonicity #71]: #73
#79 := [trans #74 #77]: #78
#82 := [quant-intro #79]: #81
#66 := (iff #16 #65)
#63 := (iff #15 #60)
#57 := (iff #40 #14)
#61 := (iff #57 #60)
#62 := [rewrite]: #61
#58 := (iff #15 #57)
#55 := (iff #13 #40)
#56 := [rewrite]: #55
#59 := [monotonicity #56]: #58
#64 := [trans #59 #62]: #63
#67 := [quant-intro #64]: #66
#84 := [trans #67 #82]: #83
#39 := [asserted]: #16
#85 := [mp #39 #84]: #80
#113 := [mp~ #85 #98]: #80
#596 := [mp #113 #595]: #591
#276 := (not #591)
#550 := (or #276 #552)
#222 := (* -1::int 3::int)
#223 := (+ uf_4 #222)
#224 := (>= #223 0::int)
#560 := (not #224)
#561 := (iff #221 #560)
#554 := (or #276 #561)
#555 := (iff #554 #550)
#266 := (iff #550 #550)
#267 := [rewrite]: #266
#553 := (iff #561 #552)
#282 := (iff #560 #576)
#280 := (iff #224 #259)
#562 := -3::int
#566 := (+ -3::int uf_4)
#567 := (>= #566 0::int)
#557 := (iff #567 #259)
#279 := [rewrite]: #557
#570 := (iff #224 #567)
#209 := (= #223 #566)
#559 := (+ uf_4 -3::int)
#568 := (= #559 #566)
#208 := [rewrite]: #568
#565 := (= #223 #559)
#563 := (= #222 -3::int)
#564 := [rewrite]: #563
#203 := [monotonicity #564]: #565
#569 := [trans #203 #208]: #209
#556 := [monotonicity #569]: #570
#281 := [trans #556 #279]: #280
#175 := [monotonicity #281]: #282
#275 := [monotonicity #175]: #553
#265 := [monotonicity #275]: #555
#268 := [trans #265 #267]: #555
#551 := [quant-inst]: #554
#546 := [mp #551 #268]: #550
#384 := [unit-resolution #546 #596]: #552
#547 := (not #552)
#262 := (or #547 #221 #259)
#544 := [def-axiom]: #262
#386 := [unit-resolution #544 #384]: #385
#528 := [unit-resolution #386 #543]: #221
#527 := [unit-resolution #528 #533]: false
#534 := [lemma #527]: #256
#523 := [mp #534 #525]: #221
#363 := (or #232 #259)
#237 := (or #581 #232 #259)
#573 := [def-axiom]: #237
#365 := [unit-resolution #573 #541]: #363
#366 := [unit-resolution #365 #534]: #259
#519 := (or #548 #576)
#545 := (or #547 #548 #576)
#549 := [def-axiom]: #545
#520 := [unit-resolution #549 #384]: #519
#522 := [unit-resolution #520 #366]: #548
[unit-resolution #522 #523]: false
unsat