src/HOL/SMT/Examples/cert/z3_fol_02.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 T2 bool)
#5 := (:var 0 T2)
decl uf_3 :: T1
#11 := uf_3
#12 := (up_1 uf_3 #5)
#560 := (pattern #12)
#57 := (not #12)
#561 := (forall (vars (?x3 T2)) (:pat #560) #57)
decl uf_4 :: T2
#14 := uf_4
#15 := (up_1 uf_3 uf_4)
decl uf_2 :: T1
#7 := uf_2
#136 := (= uf_2 uf_3)
#543 := (iff #15 #136)
#4 := (:var 1 T1)
#6 := (up_1 #4 #5)
#553 := (pattern #6)
#8 := (= #4 uf_2)
#9 := (iff #6 #8)
#554 := (forall (vars (?x1 T1) (?x2 T2)) (:pat #553) #9)
#10 := (forall (vars (?x1 T1) (?x2 T2)) #9)
#557 := (iff #10 #554)
#555 := (iff #9 #9)
#556 := [refl]: #555
#558 := [quant-intro #556]: #557
#47 := (~ #10 #10)
#45 := (~ #9 #9)
#46 := [refl]: #45
#48 := [nnf-pos #46]: #47
#33 := [asserted]: #10
#49 := [mp~ #33 #48]: #10
#559 := [mp #49 #558]: #554
#227 := (not #554)
#185 := (or #227 #543)
#135 := (= uf_3 uf_2)
#205 := (iff #15 #135)
#528 := (or #227 #205)
#190 := (iff #528 #185)
#192 := (iff #185 #185)
#530 := [rewrite]: #192
#201 := (iff #205 #543)
#223 := (iff #135 #136)
#137 := [rewrite]: #223
#544 := [monotonicity #137]: #201
#191 := [monotonicity #544]: #190
#531 := [trans #191 #530]: #190
#189 := [quant-inst]: #528
#532 := [mp #189 #531]: #185
#539 := [unit-resolution #532 #559]: #543
decl ?x3!0 :: T2
#50 := ?x3!0
#51 := (up_1 uf_3 ?x3!0)
#224 := (iff #51 #136)
#155 := (or #227 #224)
#222 := (iff #51 #135)
#228 := (or #227 #222)
#229 := (iff #228 #155)
#545 := (iff #155 #155)
#547 := [rewrite]: #545
#215 := (iff #222 #224)
#226 := [monotonicity #137]: #215
#208 := [monotonicity #226]: #229
#202 := [trans #208 #547]: #229
#225 := [quant-inst]: #228
#334 := [mp #225 #202]: #155
#537 := [unit-resolution #334 #559]: #224
#541 := (not #224)
#527 := (or #541 #136)
#63 := (not #15)
#540 := [hypothesis]: #63
#68 := (or #15 #51)
#60 := (forall (vars (?x3 T2)) #57)
#69 := (or #63 #60)
#76 := (and #68 #69)
#70 := (and #69 #68)
#77 := (iff #70 #76)
#78 := [rewrite]: #77
#13 := (exists (vars (?x3 T2)) #12)
#35 := (not #13)
#36 := (iff #15 #35)
#71 := (~ #36 #70)
#61 := (~ #35 #60)
#58 := (~ #57 #57)
#59 := [refl]: #58
#62 := [nnf-neg #59]: #61
#54 := (not #35)
#55 := (~ #54 #51)
#42 := (~ #13 #51)
#39 := [sk]: #42
#56 := [nnf-neg #39]: #55
#66 := (~ #15 #15)
#67 := [refl]: #66
#64 := (~ #63 #63)
#65 := [refl]: #64
#72 := [nnf-pos #65 #67 #56 #62]: #71
#16 := (iff #13 #15)
#17 := (not #16)
#37 := (iff #17 #36)
#38 := [rewrite]: #37
#34 := [asserted]: #17
#41 := [mp #34 #38]: #36
#73 := [mp~ #41 #72]: #70
#74 := [mp #73 #78]: #76
#75 := [and-elim #74]: #68
#526 := [unit-resolution #75 #540]: #51
#549 := (not #51)
#550 := (or #541 #549 #136)
#551 := [def-axiom]: #550
#233 := [unit-resolution #551 #526]: #527
#249 := [unit-resolution #233 #537]: #136
#213 := (not #136)
#533 := (not #543)
#250 := (or #533 #213)
#534 := (or #533 #15 #213)
#529 := [def-axiom]: #534
#251 := [unit-resolution #529 #540]: #250
#237 := [unit-resolution #251 #249 #539]: false
#252 := [lemma #237]: #15
#566 := (or #63 #561)
#567 := (iff #69 #566)
#564 := (iff #60 #561)
#562 := (iff #57 #57)
#563 := [refl]: #562
#565 := [quant-intro #563]: #564
#568 := [monotonicity #565]: #567
#79 := [and-elim #74]: #69
#569 := [mp #79 #568]: #566
#535 := [unit-resolution #569 #252]: #561
#536 := (not #561)
#538 := (or #536 #63)
#176 := [quant-inst]: #538
[unit-resolution #176 #252 #535]: false
unsat