1 ZF: Zermelo-Fraenkel 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 |
|
7 Makefile -- compiles the files under Poly/ML or SML of New Jersey. Can also |
|
8 run all the tests described below. |
|
9 |
|
10 ROOT.ML -- loads all source files. Enter an ML image containing FOL and |
|
11 type: use "ROOT.ML"; |
|
12 |
|
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 co-induction. It |
|
22 is by Jacob Frost following a paper by Robin Milner and Mads Tofte. |
|
23 |
|
24 IMP -- subdirectory containing a semantics equivalence proof between |
|
25 operational and denotational definitions of a simple programming language. |
|
26 Thanks to Heiko Loetzbeyer & Robert Sandner. |
|
27 |
|
28 Resid -- subdirectory containing a proof of the Church-Rosser Theorem. It is |
|
29 by Ole Rasmussen, following the Coq proof by Gérard Huet. |
|
30 |
|
31 ex -- subdirectory containing various examples. |
|
32 |
|
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 Schroeder-Bernstein 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 infinite-branching 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), 353-389. |
|
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 CADE-12: 12th International Conference on Automated Deduction, |
|
56 (Springer LNAI 814, 1994), 148-161. |
|
57 |
|
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) |
|
66 |
|
67 Kenneth Kunen |
|
68 Set Theory: An Introduction to Independence Proofs |
|
69 (North-Holland, 1980) |
|
70 |
|
71 $Id$ |
|