src/HOL/SMT/Examples/cert/z3_pair_01.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_6 :: T2
#23 := uf_6
decl uf_4 :: T2
#19 := uf_4
#25 := (= uf_4 uf_6)
decl uf_2 :: (-> T1 T2)
decl uf_1 :: (-> T2 T3 T1)
decl uf_5 :: T3
#20 := uf_5
#21 := (uf_1 uf_4 uf_5)
#22 := (uf_2 #21)
#24 := (= #22 uf_6)
#65 := [asserted]: #24
#143 := (= uf_4 #22)
#11 := (:var 0 T3)
#10 := (:var 1 T2)
#12 := (uf_1 #10 #11)
#567 := (pattern #12)
#16 := (uf_2 #12)
#58 := (= #10 #16)
#574 := (forall (vars (?x4 T2) (?x5 T3)) (:pat #567) #58)
#62 := (forall (vars (?x4 T2) (?x5 T3)) #58)
#577 := (iff #62 #574)
#575 := (iff #58 #58)
#576 := [refl]: #575
#578 := [quant-intro #576]: #577
#71 := (~ #62 #62)
#87 := (~ #58 #58)
#88 := [refl]: #87
#72 := [nnf-pos #88]: #71
#17 := (= #16 #10)
#18 := (forall (vars (?x4 T2) (?x5 T3)) #17)
#63 := (iff #18 #62)
#60 := (iff #17 #58)
#61 := [rewrite]: #60
#64 := [quant-intro #61]: #63
#57 := [asserted]: #18
#67 := [mp #57 #64]: #62
#89 := [mp~ #67 #72]: #62
#579 := [mp #89 #578]: #574
#214 := (not #574)
#551 := (or #214 #143)
#553 := [quant-inst]: #551
#233 := [unit-resolution #553 #579]: #143
#235 := [trans #233 #65]: #25
#26 := (not #25)
#66 := [asserted]: #26
[unit-resolution #66 #235]: false
unsat