summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/ZF/README.html

changeset 1341 | 69fec018854c |

child 3279 | 815ef5848324 |

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/README.html Fri Nov 17 13:22:50 1995 +0100 @@ -0,0 +1,89 @@ +<HTML><HEAD><TITLE>ZF/ReadMe</TITLE></HEAD><BODY> + +<H2>ZF: Zermelo-Fraenkel Set Theory</H2> + +This directory contains the Standard ML sources of the Isabelle system for +ZF Set Theory. It is loaded upon FOL, not Pure Isabelle. Important files +include + +<DL> +<DT>Makefile +<DD>compiles the files under Poly/ML or SML of New Jersey. Can also +run all the tests described below.<P> + +<DT>ROOT.ML +<DD>loads all source files. Enter an ML image containing FOL and +type: use "ROOT.ML"; +</DL> + +There are also several subdirectories of examples. To execute the examples on +some directory <Dir>, enter an ML image containing ZF and type +<TT>use "<Dir>/ROOT.ML";</TT> + +<DL> +<DT>AC +<DD>subdirectory containing proofs from the book "Equivalents of the Axiom +of Choice, II" by H. Rubin and J.E. Rubin, 1985. Thanks to Krzysztof +Gr`abczewski.<P> + +<DT>Coind +<DD>subdirectory containing a large example of proof by co-induction. It +is by Jacob Frost following a paper by Robin Milner and Mads Tofte.<P> + +<DT>IMP +<DD>subdirectory containing a semantics equivalence proof between +operational and denotational definitions of a simple programming language. +Thanks to Heiko Loetzbeyer & Robert Sandner.<P> + +<DT>Resid +<DD>subdirectory containing a proof of the Church-Rosser Theorem. It is +by Ole Rasmussen, following the Coq proof by Gérard Huet.<P> + +<DT>ex +<DD>subdirectory containing various examples. +</DL> + +Isabelle/ZF formalizes the greater part of elementary set theory, +including relations, functions, injections, surjections, ordinals and +cardinals. Results proved include Cantor's Theorem, the Recursion +Theorem, the Schroeder-Bernstein Theorem, and (assuming AC) the +Wellordering Theorem.<P> + +Isabelle/ZF also provides theories of lists, trees, etc., for +formalizing computational notions. It supports inductive definitions +of infinite-branching trees for any cardinality of branching.<P> + +Useful references for Isabelle/ZF: + +<UL> +<LI> Lawrence C. Paulson,<BR> + Set theory for verification: I. From foundations to functions.<BR> + J. Automated Reasoning 11 (1993), 353-389. + +<LI> Lawrence C. Paulson,<BR> + Set theory for verification: II. Induction and recursion.<BR> + Report 312, Computer Lab (1993).<BR> + +<LI> Lawrence C. Paulson,<BR> + A fixedpoint approach to implementing (co)inductive definitions. <BR> + In: A. Bundy (editor),<BR> + CADE-12: 12th International Conference on Automated Deduction,<BR> + (Springer LNAI 814, 1994), 148-161. +</UL> + +Useful references on ZF set theory: + +<UL> +<LI> Paul R. Halmos, Naive Set Theory (Van Nostrand, 1960) + +<LI> Patrick Suppes, Axiomatic Set Theory (Dover, 1972) + +<LI> Keith J. Devlin,<BR> + Fundamentals of Contemporary Set Theory (Springer, 1979) + +<LI> Kenneth Kunen<BR> + Set Theory: An Introduction to Independence Proofs<BR> + (North-Holland, 1980) +</UL> + +</BODY></HTML>