src/ZF/README

Simplification of definition of synth

		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$