1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> |
|
2 |
|
3 <HTML> |
|
4 |
|
5 <HEAD> |
|
6 <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"> |
|
7 <TITLE>ZF/README</TITLE> |
|
8 </HEAD> |
|
9 |
|
10 <BODY> |
|
11 |
|
12 <H2>ZF: Zermelo-Fraenkel Set Theory</H2> |
|
13 |
|
14 This directory contains the ML sources of the Isabelle system for |
|
15 ZF Set Theory, based on FOL.<p> |
|
16 |
|
17 There are several subdirectories of examples: |
|
18 <DL> |
|
19 <DT>AC |
|
20 <DD>subdirectory containing proofs from the book "Equivalents of the Axiom |
|
21 of Choice, II" by H. Rubin and J.E. Rubin, 1985. Thanks to Krzysztof |
|
22 Gr`abczewski.<P> |
|
23 |
|
24 <DT>Coind |
|
25 <DD>subdirectory containing a large example of proof by co-induction. It |
|
26 is by Jacob Frost following a paper by Robin Milner and Mads Tofte.<P> |
|
27 |
|
28 <DT>IMP |
|
29 <DD>subdirectory containing a semantics equivalence proof between |
|
30 operational and denotational definitions of a simple programming language. |
|
31 Thanks to Heiko Loetzbeyer & Robert Sandner.<P> |
|
32 |
|
33 <DT>Resid |
|
34 <DD>subdirectory containing a proof of the Church-Rosser Theorem. It is |
|
35 by Ole Rasmussen, following the Coq proof by G�ard Huet.<P> |
|
36 |
|
37 <DT>ex |
|
38 <DD>subdirectory containing various examples. |
|
39 </DL> |
|
40 |
|
41 Isabelle/ZF formalizes the greater part of elementary set theory, |
|
42 including relations, functions, injections, surjections, ordinals and |
|
43 cardinals. Results proved include Cantor's Theorem, the Recursion |
|
44 Theorem, the Schroeder-Bernstein Theorem, and (assuming AC) the |
|
45 Wellordering Theorem.<P> |
|
46 |
|
47 Isabelle/ZF also provides theories of lists, trees, etc., for |
|
48 formalizing computational notions. It supports inductive definitions |
|
49 of infinite-branching trees for any cardinality of branching.<P> |
|
50 |
|
51 Useful references for Isabelle/ZF: |
|
52 |
|
53 <UL> |
|
54 <LI> Lawrence C. Paulson,<BR> |
|
55 Set theory for verification: I. From foundations to functions.<BR> |
|
56 J. Automated Reasoning 11 (1993), 353-389. |
|
57 |
|
58 <LI> Lawrence C. Paulson,<BR> |
|
59 Set theory for verification: II. Induction and recursion.<BR> |
|
60 Report 312, Computer Lab (1993).<BR> |
|
61 |
|
62 <LI> Lawrence C. Paulson,<BR> |
|
63 A fixedpoint approach to implementing (co)inductive definitions. <BR> |
|
64 In: A. Bundy (editor),<BR> |
|
65 CADE-12: 12th International Conference on Automated Deduction,<BR> |
|
66 (Springer LNAI 814, 1994), 148-161. |
|
67 </UL> |
|
68 |
|
69 Useful references on ZF set theory: |
|
70 |
|
71 <UL> |
|
72 <LI> Paul R. Halmos, Naive Set Theory (Van Nostrand, 1960) |
|
73 |
|
74 <LI> Patrick Suppes, Axiomatic Set Theory (Dover, 1972) |
|
75 |
|
76 <LI> Keith J. Devlin,<BR> |
|
77 Fundamentals of Contemporary Set Theory (Springer, 1979) |
|
78 |
|
79 <LI> Kenneth Kunen<BR> |
|
80 Set Theory: An Introduction to Independence Proofs<BR> |
|
81 (North-Holland, 1980) |
|
82 </UL> |
|
83 |
|
84 </BODY></HTML> |
|