0

1 
ZF: ZermeloFraenkel Set Theory


2 


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


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


5 
include


6 

958

7 
Makefile  compiles the files under Poly/ML or SML of New Jersey. Can also


8 
run all the tests described below.


9 

0

10 
ROOT.ML  loads all source files. Enter an ML image containing FOL and


11 
type: use "ROOT.ML";


12 

1062

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


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


15 
use "<Dir>/ROOT.ML";


16 


17 
AC  subdirectory containing proofs from the book "Equivalents of the Axiom


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


19 
Gr`abczewski.


20 


21 
Coind  subdirectory containing a large example of proof by coinduction. It


22 
is by Jacob Frost following a paper by Robin Milner and Mads Tofte.

0

23 

488

24 
IMP  subdirectory containing a semantics equivalence proof between


25 
operational and denotational definitions of a simple programming language.

1062

26 
Thanks to Heiko Loetzbeyer & Robert Sandner.

488

27 

1062

28 
Resid  subdirectory containing a proof of the ChurchRosser Theorem. It is


29 
by Ole Rasmussen, following the Coq proof by Gérard Huet.


30 


31 
ex  subdirectory containing various examples.

0

32 

488

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


34 
relations, functions, injections, surjections, ordinals and cardinals.


35 
Results proved include Cantor's Theorem, the Recursion Theorem, the


36 
SchroederBernstein Theorem, and (assuming AC) the Wellordering Theorem.


37 


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


39 
computational notions. It supports inductive definitions of


40 
infinitebranching trees for any cardinality of branching.


41 


42 
Useful references for Isabelle/ZF:


43 


44 
Lawrence C. Paulson,


45 
Set theory for verification: I. From foundations to functions.


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


47 


48 
Lawrence C. Paulson,


49 
Set theory for verification: II. Induction and recursion.


50 
Report 312, Computer Lab (1993).


51 


52 
Lawrence C. Paulson,


53 
A fixedpoint approach to implementing (co)inductive definitions.


54 
In: A. Bundy (editor),


55 
CADE12: 12th International Conference on Automated Deduction,


56 
(Springer LNAI 814, 1994), 148161.


57 

0

58 
Useful references on ZF set theory:


59 


60 
Paul R. Halmos, Naive Set Theory (Van Nostrand, 1960)


61 


62 
Patrick Suppes, Axiomatic Set Theory (Dover, 1972)


63 


64 
Keith J. Devlin,


65 
Fundamentals of Contemporary Set Theory (Springer, 1979)

488

66 


67 
Kenneth Kunen


68 
Set Theory: An Introduction to Independence Proofs


69 
(NorthHolland, 1980)

958

70 


71 
$Id$
