isabelle: src/ZF/README.html@855ca2dcc03d


<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">

<!-- $Id$ -->

<HTML>

<HEAD>
  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
  <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�ard 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>
author	wenzelm
	Fri, 03 Oct 2008 17:07:39 +0200
changeset 28478	855ca2dcc03d
parent 15582	7219facb3fd0
child 36862	952b2b102a0a
permissions	-rw-r--r--