src/HOL/SMT/Examples/cert/z3_arith_quant_17.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
#144 := (not false)
#7 := 0::int
#5 := (:var 0 int)
#52 := (<= #5 0::int)
#53 := (not #52)
#147 := (or #53 #144)
#150 := (not #147)
#153 := (forall (vars (?x1 int)) #150)
#180 := (iff #153 false)
#175 := (forall (vars (?x1 int)) false)
#178 := (iff #175 false)
#179 := [elim-unused]: #178
#176 := (iff #153 #175)
#173 := (iff #150 false)
#1 := true
#168 := (not true)
#171 := (iff #168 false)
#172 := [rewrite]: #171
#169 := (iff #150 #168)
#166 := (iff #147 true)
#161 := (or #53 true)
#164 := (iff #161 true)
#165 := [rewrite]: #164
#162 := (iff #147 #161)
#159 := (iff #144 true)
#160 := [rewrite]: #159
#163 := [monotonicity #160]: #162
#167 := [trans #163 #165]: #166
#170 := [monotonicity #167]: #169
#174 := [trans #170 #172]: #173
#177 := [quant-intro #174]: #176
#181 := [trans #177 #179]: #180
#56 := -1::int
#57 := (* -1::int #5)
#4 := (:var 1 int)
#58 := (+ #4 #57)
#59 := (<= #58 0::int)
#62 := (not #59)
#68 := (or #53 #62)
#73 := (forall (vars (?x2 int)) #68)
#76 := (not #73)
#79 := (or #53 #76)
#105 := (not #79)
#123 := (forall (vars (?x1 int)) #105)
#156 := (iff #123 #153)
#127 := (forall (vars (?x2 int)) #53)
#130 := (not #127)
#133 := (or #53 #130)
#136 := (not #133)
#139 := (forall (vars (?x1 int)) #136)
#154 := (iff #139 #153)
#155 := [rewrite]: #154
#140 := (iff #123 #139)
#141 := [rewrite]: #140
#157 := [trans #141 #155]: #156
#116 := (and #52 #73)
#119 := (forall (vars (?x1 int)) #116)
#124 := (iff #119 #123)
#113 := (iff #116 #105)
#122 := [rewrite]: #113
#125 := [quant-intro #122]: #124
#94 := (not #53)
#104 := (and #94 #73)
#108 := (forall (vars (?x1 int)) #104)
#120 := (iff #108 #119)
#117 := (iff #104 #116)
#114 := (iff #94 #52)
#115 := [rewrite]: #114
#118 := [monotonicity #115]: #117
#121 := [quant-intro #118]: #120
#82 := (exists (vars (?x1 int)) #79)
#85 := (not #82)
#109 := (~ #85 #108)
#106 := (~ #105 #104)
#101 := (not #76)
#102 := (~ #101 #73)
#99 := (~ #73 #73)
#97 := (~ #68 #68)
#98 := [refl]: #97
#100 := [nnf-pos #98]: #99
#103 := [nnf-neg #100]: #102
#95 := (~ #94 #94)
#96 := [refl]: #95
#107 := [nnf-neg #96 #103]: #106
#110 := [nnf-neg #107]: #109
#8 := (< 0::int #5)
#6 := (<= #4 #5)
#9 := (implies #6 #8)
#10 := (forall (vars (?x2 int)) #9)
#11 := (implies #10 #8)
#12 := (exists (vars (?x1 int)) #11)
#13 := (not #12)
#88 := (iff #13 #85)
#30 := (not #6)
#31 := (or #30 #8)
#34 := (forall (vars (?x2 int)) #31)
#40 := (not #34)
#41 := (or #8 #40)
#46 := (exists (vars (?x1 int)) #41)
#49 := (not #46)
#86 := (iff #49 #85)
#83 := (iff #46 #82)
#80 := (iff #41 #79)
#77 := (iff #40 #76)
#74 := (iff #34 #73)
#71 := (iff #31 #68)
#65 := (or #62 #53)
#69 := (iff #65 #68)
#70 := [rewrite]: #69
#66 := (iff #31 #65)
#54 := (iff #8 #53)
#55 := [rewrite]: #54
#63 := (iff #30 #62)
#60 := (iff #6 #59)
#61 := [rewrite]: #60
#64 := [monotonicity #61]: #63
#67 := [monotonicity #64 #55]: #66
#72 := [trans #67 #70]: #71
#75 := [quant-intro #72]: #74
#78 := [monotonicity #75]: #77
#81 := [monotonicity #55 #78]: #80
#84 := [quant-intro #81]: #83
#87 := [monotonicity #84]: #86
#50 := (iff #13 #49)
#47 := (iff #12 #46)
#44 := (iff #11 #41)
#37 := (implies #34 #8)
#42 := (iff #37 #41)
#43 := [rewrite]: #42
#38 := (iff #11 #37)
#35 := (iff #10 #34)
#32 := (iff #9 #31)
#33 := [rewrite]: #32
#36 := [quant-intro #33]: #35
#39 := [monotonicity #36]: #38
#45 := [trans #39 #43]: #44
#48 := [quant-intro #45]: #47
#51 := [monotonicity #48]: #50
#89 := [trans #51 #87]: #88
#29 := [asserted]: #13
#90 := [mp #29 #89]: #85
#111 := [mp~ #90 #110]: #108
#112 := [mp #111 #121]: #119
#126 := [mp #112 #125]: #123
#158 := [mp #126 #157]: #153
[mp #158 #181]: false
unsat