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

src/ZF/README.html

author | wenzelm |

Wed, 21 May 1997 17:13:00 +0200 | |

changeset 3279 | 815ef5848324 |

parent 1341 | 69fec018854c |

child 15283 | f21466450330 |

permissions | -rw-r--r-- |

tuned all READMEs;

<HTML><HEAD><TITLE>ZF/README</TITLE></HEAD><BODY> <H2>ZF: Zermelo-Fraenkel Set Theory</H2> This directory contains the ML sources of the Isabelle system for ZF Set Theory, based on FOL.<p> There are several subdirectories of examples: <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>