|
1341
|
1 |
<HTML><HEAD><TITLE>ZF/ReadMe</TITLE></HEAD><BODY>
|
|
|
2 |
|
|
|
3 |
<H2>ZF: Zermelo-Fraenkel 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 co-induction. 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 Church-Rosser 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 Schroeder-Bernstein 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 infinite-branching 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), 353-389.
|
|
|
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 |
CADE-12: 12th International Conference on Automated Deduction,<BR>
|
|
|
71 |
(Springer LNAI 814, 1994), 148-161.
|
|
|
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 |
(North-Holland, 1980)
|
|
|
87 |
</UL>
|
|
|
88 |
|
|
|
89 |
</BODY></HTML>
|