1341

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


2 


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


4 


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


6 
ZF Set Theory. It is loaded upon FOL, not Pure Isabelle. Important files


7 
include


8 


9 
<DL>


10 
<DT>Makefile


11 
<DD>compiles the files under Poly/ML or SML of New Jersey. Can also


12 
run all the tests described below.<P>


13 


14 
<DT>ROOT.ML


15 
<DD>loads all source files. Enter an ML image containing FOL and


16 
type: use "ROOT.ML";


17 
</DL>


18 


19 
There are also several subdirectories of examples. To execute the examples on


20 
some directory <Dir>, enter an ML image containing ZF and type


21 
<TT>use "<Dir>/ROOT.ML";</TT>


22 


23 
<DL>


24 
<DT>AC


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


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


27 
Gr`abczewski.<P>


28 


29 
<DT>Coind


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


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


32 


33 
<DT>IMP


34 
<DD>subdirectory containing a semantics equivalence proof between


35 
operational and denotational definitions of a simple programming language.


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


37 


38 
<DT>Resid


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


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


41 


42 
<DT>ex


43 
<DD>subdirectory containing various examples.


44 
</DL>


45 


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


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


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


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


50 
Wellordering Theorem.<P>


51 


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


53 
formalizing computational notions. It supports inductive definitions


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


55 


56 
Useful references for Isabelle/ZF:


57 


58 
<UL>


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


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


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


62 


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


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


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


66 


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


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


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


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


71 
(Springer LNAI 814, 1994), 148161.


72 
</UL>


73 


74 
Useful references on ZF set theory:


75 


76 
<UL>


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


78 


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


80 


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


82 
Fundamentals of Contemporary Set Theory (Springer, 1979)


83 


84 
<LI> Kenneth Kunen<BR>


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


86 
(NorthHolland, 1980)


87 
</UL>


88 


89 
</BODY></HTML>
