src/HOL/SMT/Examples/cert/z3_nat_arith_02.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
#23 := 3::int
decl uf_2 :: (-> T1 int)
decl uf_3 :: T1
#21 := uf_3
#22 := (uf_2 uf_3)
#137 := (>= #22 3::int)
#135 := (not #137)
#24 := (< #22 3::int)
#136 := (iff #24 #135)
#138 := [rewrite]: #136
#132 := [asserted]: #24
#139 := [mp #132 #138]: #135
#9 := 0::int
decl uf_1 :: (-> int T1)
#25 := 2::int
#26 := (* 2::int #22)
#27 := (uf_1 #26)
#28 := (uf_2 #27)
#297 := -1::int
#633 := (* -1::int #28)
#635 := (+ #26 #633)
#278 := (>= #635 0::int)
#291 := (= #635 0::int)
#315 := (>= #26 0::int)
#279 := (= #28 0::int)
#627 := (not #279)
#624 := (<= #28 0::int)
#281 := (not #624)
#29 := 7::int
#143 := (>= #28 7::int)
#30 := (< #28 7::int)
#31 := (not #30)
#150 := (iff #31 #143)
#141 := (not #143)
#145 := (not #141)
#148 := (iff #145 #143)
#149 := [rewrite]: #148
#146 := (iff #31 #145)
#142 := (iff #30 #141)
#144 := [rewrite]: #142
#147 := [monotonicity #144]: #146
#151 := [trans #147 #149]: #150
#133 := [asserted]: #31
#152 := [mp #133 #151]: #143
#618 := (or #281 #141)
#265 := [th-lemma]: #618
#266 := [unit-resolution #265 #152]: #281
#625 := (or #627 #624)
#628 := [th-lemma]: #625
#614 := [unit-resolution #628 #266]: #627
#10 := (:var 0 int)
#12 := (uf_1 #10)
#649 := (pattern #12)
#73 := (>= #10 0::int)
#13 := (uf_2 #12)
#18 := (= #13 0::int)
#121 := (or #18 #73)
#656 := (forall (vars (?x3 int)) (:pat #649) #121)
#126 := (forall (vars (?x3 int)) #121)
#659 := (iff #126 #656)
#657 := (iff #121 #121)
#658 := [refl]: #657
#660 := [quant-intro #658]: #659
#154 := (~ #126 #126)
#170 := (~ #121 #121)
#171 := [refl]: #170
#155 := [nnf-pos #171]: #154
#17 := (< #10 0::int)
#19 := (implies #17 #18)
#20 := (forall (vars (?x3 int)) #19)
#129 := (iff #20 #126)
#92 := (= 0::int #13)
#98 := (not #17)
#99 := (or #98 #92)
#104 := (forall (vars (?x3 int)) #99)
#127 := (iff #104 #126)
#124 := (iff #99 #121)
#118 := (or #73 #18)
#122 := (iff #118 #121)
#123 := [rewrite]: #122
#119 := (iff #99 #118)
#116 := (iff #92 #18)
#117 := [rewrite]: #116
#114 := (iff #98 #73)
#74 := (not #73)
#109 := (not #74)
#112 := (iff #109 #73)
#113 := [rewrite]: #112
#110 := (iff #98 #109)
#107 := (iff #17 #74)
#108 := [rewrite]: #107
#111 := [monotonicity #108]: #110
#115 := [trans #111 #113]: #114
#120 := [monotonicity #115 #117]: #119
#125 := [trans #120 #123]: #124
#128 := [quant-intro #125]: #127
#105 := (iff #20 #104)
#102 := (iff #19 #99)
#95 := (implies #17 #92)
#100 := (iff #95 #99)
#101 := [rewrite]: #100
#96 := (iff #19 #95)
#93 := (iff #18 #92)
#94 := [rewrite]: #93
#97 := [monotonicity #94]: #96
#103 := [trans #97 #101]: #102
#106 := [quant-intro #103]: #105
#130 := [trans #106 #128]: #129
#91 := [asserted]: #20
#131 := [mp #91 #130]: #126
#172 := [mp~ #131 #155]: #126
#661 := [mp #172 #660]: #656
#619 := (not #656)
#620 := (or #619 #279 #315)
#280 := (or #279 #315)
#621 := (or #619 #280)
#617 := (iff #621 #620)
#623 := [rewrite]: #617
#622 := [quant-inst]: #621
#260 := [mp #622 #623]: #620
#615 := [unit-resolution #260 #661 #614]: #315
#316 := (not #315)
#302 := (or #291 #316)
#55 := (= #10 #13)
#80 := (or #55 #74)
#650 := (forall (vars (?x2 int)) (:pat #649) #80)
#85 := (forall (vars (?x2 int)) #80)
#653 := (iff #85 #650)
#651 := (iff #80 #80)
#652 := [refl]: #651
#654 := [quant-intro #652]: #653
#153 := (~ #85 #85)
#167 := (~ #80 #80)
#168 := [refl]: #167
#134 := [nnf-pos #168]: #153
#14 := (= #13 #10)
#11 := (<= 0::int #10)
#15 := (implies #11 #14)
#16 := (forall (vars (?x2 int)) #15)
#88 := (iff #16 #85)
#62 := (not #11)
#63 := (or #62 #55)
#68 := (forall (vars (?x2 int)) #63)
#86 := (iff #68 #85)
#83 := (iff #63 #80)
#77 := (or #74 #55)
#81 := (iff #77 #80)
#82 := [rewrite]: #81
#78 := (iff #63 #77)
#75 := (iff #62 #74)
#71 := (iff #11 #73)
#72 := [rewrite]: #71
#76 := [monotonicity #72]: #75
#79 := [monotonicity #76]: #78
#84 := [trans #79 #82]: #83
#87 := [quant-intro #84]: #86
#69 := (iff #16 #68)
#66 := (iff #15 #63)
#59 := (implies #11 #55)
#64 := (iff #59 #63)
#65 := [rewrite]: #64
#60 := (iff #15 #59)
#57 := (iff #14 #55)
#58 := [rewrite]: #57
#61 := [monotonicity #58]: #60
#67 := [trans #61 #65]: #66
#70 := [quant-intro #67]: #69
#89 := [trans #70 #87]: #88
#54 := [asserted]: #16
#90 := [mp #54 #89]: #85
#169 := [mp~ #90 #134]: #85
#655 := [mp #169 #654]: #650
#637 := (not #650)
#638 := (or #637 #291 #316)
#314 := (= #26 #28)
#318 := (or #314 #316)
#639 := (or #637 #318)
#290 := (iff #639 #638)
#640 := (or #637 #302)
#294 := (iff #640 #638)
#631 := [rewrite]: #294
#630 := (iff #639 #640)
#303 := (iff #318 #302)
#422 := (iff #314 #291)
#629 := [rewrite]: #422
#636 := [monotonicity #629]: #303
#289 := [monotonicity #636]: #630
#632 := [trans #289 #631]: #290
#634 := [quant-inst]: #639
#274 := [mp #634 #632]: #638
#322 := [unit-resolution #274 #655]: #302
#337 := [unit-resolution #322 #615]: #291
#338 := (not #291)
#339 := (or #338 #278)
#340 := [th-lemma]: #339
#232 := [unit-resolution #340 #337]: #278
[th-lemma #152 #232 #139]: false
unsat