3279

1 
<HTML><HEAD><TITLE>ZF/README</TITLE></HEAD><BODY>

1341

2 


3 
<H2>ZF: ZermeloFraenkel Set Theory</H2>


4 

3279

5 
This directory contains the ML sources of the Isabelle system for


6 
ZF Set Theory, based on FOL.<p>

1341

7 

3279

8 
There are several subdirectories of examples:

1341

9 
<DL>


10 
<DT>AC


11 
<DD>subdirectory containing proofs from the book "Equivalents of the Axiom


12 
of Choice, II" by H. Rubin and J.E. Rubin, 1985. Thanks to Krzysztof


13 
Gr`abczewski.<P>


14 


15 
<DT>Coind


16 
<DD>subdirectory containing a large example of proof by coinduction. It


17 
is by Jacob Frost following a paper by Robin Milner and Mads Tofte.<P>


18 


19 
<DT>IMP


20 
<DD>subdirectory containing a semantics equivalence proof between


21 
operational and denotational definitions of a simple programming language.


22 
Thanks to Heiko Loetzbeyer & Robert Sandner.<P>


23 


24 
<DT>Resid


25 
<DD>subdirectory containing a proof of the ChurchRosser Theorem. It is


26 
by Ole Rasmussen, following the Coq proof by Gérard Huet.<P>


27 


28 
<DT>ex


29 
<DD>subdirectory containing various examples.


30 
</DL>


31 


32 
Isabelle/ZF formalizes the greater part of elementary set theory,


33 
including relations, functions, injections, surjections, ordinals and


34 
cardinals. Results proved include Cantor's Theorem, the Recursion


35 
Theorem, the SchroederBernstein Theorem, and (assuming AC) the


36 
Wellordering Theorem.<P>


37 


38 
Isabelle/ZF also provides theories of lists, trees, etc., for


39 
formalizing computational notions. It supports inductive definitions


40 
of infinitebranching trees for any cardinality of branching.<P>


41 


42 
Useful references for Isabelle/ZF:


43 


44 
<UL>


45 
<LI> Lawrence C. Paulson,<BR>


46 
Set theory for verification: I. From foundations to functions.<BR>


47 
J. Automated Reasoning 11 (1993), 353389.


48 


49 
<LI> Lawrence C. Paulson,<BR>


50 
Set theory for verification: II. Induction and recursion.<BR>


51 
Report 312, Computer Lab (1993).<BR>


52 


53 
<LI> Lawrence C. Paulson,<BR>


54 
A fixedpoint approach to implementing (co)inductive definitions. <BR>


55 
In: A. Bundy (editor),<BR>


56 
CADE12: 12th International Conference on Automated Deduction,<BR>


57 
(Springer LNAI 814, 1994), 148161.


58 
</UL>


59 


60 
Useful references on ZF set theory:


61 


62 
<UL>


63 
<LI> Paul R. Halmos, Naive Set Theory (Van Nostrand, 1960)


64 


65 
<LI> Patrick Suppes, Axiomatic Set Theory (Dover, 1972)


66 


67 
<LI> Keith J. Devlin,<BR>


68 
Fundamentals of Contemporary Set Theory (Springer, 1979)


69 


70 
<LI> Kenneth Kunen<BR>


71 
Set Theory: An Introduction to Independence Proofs<BR>


72 
(NorthHolland, 1980)


73 
</UL>


74 


75 
</BODY></HTML>
