src/HOL/SMT/Examples/cert/z3_arith_quant_10.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
#4 := 2::int
decl ?x1!1 :: int
#85 := ?x1!1
decl ?x2!0 :: int
#84 := ?x2!0
#101 := (+ ?x2!0 ?x1!1)
#107 := (>= #101 2::int)
#113 := (<= #101 2::int)
#116 := (not #113)
#110 := (not #107)
#104 := (= #101 2::int)
#119 := (or #104 #110 #116)
#122 := (not #119)
#86 := (+ ?x1!1 ?x2!0)
#87 := (<= #86 2::int)
#88 := (not #87)
#89 := (>= #86 2::int)
#90 := (not #89)
#91 := (= #86 2::int)
#92 := (or #91 #90 #88)
#93 := (not #92)
#123 := (iff #93 #122)
#120 := (iff #92 #119)
#117 := (iff #88 #116)
#114 := (iff #87 #113)
#102 := (= #86 #101)
#103 := [rewrite]: #102
#115 := [monotonicity #103]: #114
#118 := [monotonicity #115]: #117
#111 := (iff #90 #110)
#108 := (iff #89 #107)
#109 := [monotonicity #103]: #108
#112 := [monotonicity #109]: #111
#105 := (iff #91 #104)
#106 := [monotonicity #103]: #105
#121 := [monotonicity #106 #112 #118]: #120
#124 := [monotonicity #121]: #123
#6 := (:var 0 int)
#5 := (:var 1 int)
#7 := (+ #5 #6)
#56 := (<= #7 2::int)
#58 := (not #56)
#54 := (>= #7 2::int)
#51 := (not #54)
#9 := (= #7 2::int)
#67 := (or #9 #51 #58)
#72 := (forall (vars (?x1 int) (?x2 int)) #67)
#75 := (not #72)
#94 := (~ #75 #93)
#95 := [sk]: #94
#10 := (< #7 2::int)
#11 := (or #9 #10)
#8 := (< 2::int #7)
#12 := (or #8 #11)
#13 := (forall (vars (?x1 int) (?x2 int)) #12)
#14 := (not #13)
#78 := (iff #14 #75)
#31 := (= 2::int #7)
#37 := (or #10 #31)
#42 := (or #8 #37)
#45 := (forall (vars (?x1 int) (?x2 int)) #42)
#48 := (not #45)
#76 := (iff #48 #75)
#73 := (iff #45 #72)
#70 := (iff #42 #67)
#61 := (or #51 #9)
#64 := (or #58 #61)
#68 := (iff #64 #67)
#69 := [rewrite]: #68
#65 := (iff #42 #64)
#62 := (iff #37 #61)
#55 := (iff #31 #9)
#57 := [rewrite]: #55
#53 := (iff #10 #51)
#52 := [rewrite]: #53
#63 := [monotonicity #52 #57]: #62
#59 := (iff #8 #58)
#60 := [rewrite]: #59
#66 := [monotonicity #60 #63]: #65
#71 := [trans #66 #69]: #70
#74 := [quant-intro #71]: #73
#77 := [monotonicity #74]: #76
#49 := (iff #14 #48)
#46 := (iff #13 #45)
#43 := (iff #12 #42)
#40 := (iff #11 #37)
#34 := (or #31 #10)
#38 := (iff #34 #37)
#39 := [rewrite]: #38
#35 := (iff #11 #34)
#32 := (iff #9 #31)
#33 := [rewrite]: #32
#36 := [monotonicity #33]: #35
#41 := [trans #36 #39]: #40
#44 := [monotonicity #41]: #43
#47 := [quant-intro #44]: #46
#50 := [monotonicity #47]: #49
#79 := [trans #50 #77]: #78
#30 := [asserted]: #14
#80 := [mp #30 #79]: #75
#98 := [mp~ #80 #95]: #93
#99 := [mp #98 #124]: #122
#126 := [not-or-elim #99]: #107
#100 := (not #104)
#125 := [not-or-elim #99]: #100
#127 := [not-or-elim #99]: #113
#183 := (or #104 #116 #110)
#184 := [th-lemma]: #183
[unit-resolution #184 #127 #125 #126]: false
unsat