src/HOL/SMT/Examples/cert/z3_linarith_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_3 :: (-> T1 T2)
decl uf_2 :: T1
#7 := uf_2
#16 := (uf_3 uf_2)
decl uf_1 :: (-> int int T1)
#13 := 3::int
#12 := 2::int
#14 := (uf_1 2::int 3::int)
#15 := (uf_3 #14)
#17 := (= #15 #16)
#516 := (= #16 #15)
#194 := (= uf_2 #14)
#5 := (:var 0 int)
#4 := (:var 1 int)
#6 := (uf_1 #4 #5)
#530 := (pattern #6)
#39 := 0::int
#37 := -1::int
#41 := (* -1::int #5)
#42 := (+ #4 #41)
#40 := (>= #42 0::int)
#38 := (not #40)
#8 := (= #6 uf_2)
#45 := (iff #8 #38)
#531 := (forall (vars (?x1 int) (?x2 int)) (:pat #530) #45)
#48 := (forall (vars (?x1 int) (?x2 int)) #45)
#534 := (iff #48 #531)
#532 := (iff #45 #45)
#533 := [refl]: #532
#535 := [quant-intro #533]: #534
#58 := (~ #48 #48)
#56 := (~ #45 #45)
#57 := [refl]: #56
#59 := [nnf-pos #57]: #58
#9 := (< #4 #5)
#10 := (iff #8 #9)
#11 := (forall (vars (?x1 int) (?x2 int)) #10)
#49 := (iff #11 #48)
#46 := (iff #10 #45)
#43 := (iff #9 #38)
#44 := [rewrite]: #43
#47 := [monotonicity #44]: #46
#50 := [quant-intro #47]: #49
#34 := [asserted]: #11
#51 := [mp #34 #50]: #48
#60 := [mp~ #51 #59]: #48
#536 := [mp #60 #535]: #531
#508 := (not #531)
#509 := (or #508 #194)
#201 := (* -1::int 3::int)
#115 := (+ 2::int #201)
#202 := (>= #115 0::int)
#116 := (not #202)
#114 := (= #14 uf_2)
#203 := (iff #114 #116)
#510 := (or #508 #203)
#506 := (iff #510 #509)
#150 := (iff #509 #509)
#513 := [rewrite]: #150
#171 := (iff #203 #194)
#1 := true
#164 := (iff #194 true)
#169 := (iff #164 #194)
#170 := [rewrite]: #169
#505 := (iff #203 #164)
#180 := (iff #116 true)
#529 := (not false)
#184 := (iff #529 true)
#520 := [rewrite]: #184
#519 := (iff #116 #529)
#528 := (iff #202 false)
#192 := (>= -1::int 0::int)
#526 := (iff #192 false)
#527 := [rewrite]: #526
#193 := (iff #202 #192)
#311 := (= #115 -1::int)
#134 := -3::int
#208 := (+ 2::int -3::int)
#524 := (= #208 -1::int)
#181 := [rewrite]: #524
#187 := (= #115 #208)
#207 := (= #201 -3::int)
#204 := [rewrite]: #207
#522 := [monotonicity #204]: #187
#518 := [trans #522 #181]: #311
#525 := [monotonicity #518]: #193
#523 := [trans #525 #527]: #528
#179 := [monotonicity #523]: #519
#521 := [trans #179 #520]: #180
#205 := (iff #114 #194)
#206 := [rewrite]: #205
#168 := [monotonicity #206 #521]: #505
#507 := [trans #168 #170]: #171
#512 := [monotonicity #507]: #506
#515 := [trans #512 #513]: #506
#511 := [quant-inst]: #510
#155 := [mp #511 #515]: #509
#156 := [unit-resolution #155 #536]: #194
#514 := [monotonicity #156]: #516
#517 := [symm #514]: #17
#18 := (not #17)
#35 := [asserted]: #18
[unit-resolution #35 #517]: false
unsat