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

src/ZF/README

author | paulson |

Fri, 16 Feb 1996 18:00:47 +0100 | |

changeset 1512 | ce37c64244c0 |

parent 1062 | c79fb313bf89 |

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

Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.

ZF: Zermelo-Fraenkel Set Theory 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 Makefile -- compiles the files under Poly/ML or SML of New Jersey. Can also run all the tests described below. ROOT.ML -- loads all source files. Enter an ML image containing FOL and type: use "ROOT.ML"; There are also several subdirectories of examples. To execute the examples on some directory <Dir>, enter an ML image containing ZF and type use "<Dir>/ROOT.ML"; AC -- 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. Coind -- subdirectory containing a large example of proof by co-induction. It is by Jacob Frost following a paper by Robin Milner and Mads Tofte. IMP -- subdirectory containing a semantics equivalence proof between operational and denotational definitions of a simple programming language. Thanks to Heiko Loetzbeyer & Robert Sandner. Resid -- subdirectory containing a proof of the Church-Rosser Theorem. It is by Ole Rasmussen, following the Coq proof by Gérard Huet. ex -- subdirectory containing various examples. 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. 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. Useful references for Isabelle/ZF: Lawrence C. Paulson, Set theory for verification: I. From foundations to functions. J. Automated Reasoning 11 (1993), 353-389. Lawrence C. Paulson, Set theory for verification: II. Induction and recursion. Report 312, Computer Lab (1993). Lawrence C. Paulson, A fixedpoint approach to implementing (co)inductive definitions. In: A. Bundy (editor), CADE-12: 12th International Conference on Automated Deduction, (Springer LNAI 814, 1994), 148-161. Useful references on ZF set theory: Paul R. Halmos, Naive Set Theory (Van Nostrand, 1960) Patrick Suppes, Axiomatic Set Theory (Dover, 1972) Keith J. Devlin, Fundamentals of Contemporary Set Theory (Springer, 1979) Kenneth Kunen Set Theory: An Introduction to Independence Proofs (North-Holland, 1980) $Id$