src/HOL/SMT/Examples/cert/z3_fol_04.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 up_1 :: (-> T1 bool)
decl uf_2 :: T1
#4 := uf_2
#5 := (up_1 uf_2)
decl uf_3 :: T1
#13 := uf_3
#14 := (up_1 uf_3)
#34 := (not #5)
#35 := (or #34 #14)
#38 := (not #35)
#15 := (implies #5 #14)
#16 := (not #15)
#39 := (iff #16 #38)
#36 := (iff #15 #35)
#37 := [rewrite]: #36
#40 := [monotonicity #37]: #39
#33 := [asserted]: #16
#43 := [mp #33 #40]: #38
#41 := [not-or-elim #43]: #5
#6 := (:var 0 T1)
#7 := (up_1 #6)
#536 := (pattern #7)
#10 := (not #7)
#537 := (forall (vars (?x2 T1)) (:pat #536) #10)
#11 := (forall (vars (?x2 T1)) #10)
#540 := (iff #11 #537)
#538 := (iff #10 #10)
#539 := [refl]: #538
#541 := [quant-intro #539]: #540
#8 := (exists (vars (?x1 T1)) #7)
#9 := (not #8)
#45 := (~ #9 #11)
#50 := (~ #10 #10)
#51 := [refl]: #50
#59 := [nnf-neg #51]: #45
#12 := (ite #5 #9 #11)
#57 := (iff #12 #9)
#1 := true
#52 := (ite true #9 #11)
#55 := (iff #52 #9)
#56 := [rewrite]: #55
#53 := (iff #12 #52)
#48 := (iff #5 true)
#49 := [iff-true #41]: #48
#54 := [monotonicity #49]: #53
#58 := [trans #54 #56]: #57
#32 := [asserted]: #12
#47 := [mp #32 #58]: #9
#60 := [mp~ #47 #59]: #11
#542 := [mp #60 #541]: #537
#119 := (not #537)
#206 := (or #119 #34)
#120 := [quant-inst]: #206
[unit-resolution #120 #542 #41]: false
unsat