Index of /ports/math/isabelle/work/Isabelle2005/src/ZF
Name Last modified Size Description
![[DIR]](/icons/back.gif)
Parent Directory 09-Aug-2008 06:09 -
![[ ]](/icons/unknown.gif)
AC.thy 17-Jun-2005 07:15 2k
![[TXT]](/icons/text.gif)
AC.thy.html 09-Aug-2008 06:10 0k
![[DIR]](/icons/folder.gif)
AC/ 09-Aug-2008 06:10 -
Arith.thy 17-Jun-2005 07:15 19k
Arith.thy.html 09-Aug-2008 06:10 0k
ArithSimp.thy 17-Jun-2005 07:15 21k
ArithSimp.thy.html 09-Aug-2008 06:10 0k
Bool.thy 17-Jun-2005 07:15 5k
Bool.thy.html 09-Aug-2008 06:10 0k
Cardinal.thy 17-Jun-2005 07:15 38k
Cardinal.thy.html 09-Aug-2008 06:10 0k
CardinalArith.thy 17-Jun-2005 07:15 35k
CardinalArith.thy.html 09-Aug-2008 06:10 0k
Cardinal_AC.thy 17-Jun-2005 07:15 7k
Cardinal_AC.thy.html 09-Aug-2008 06:10 0k
Coind/ 09-Aug-2008 06:10 -
Constructible/ 09-Aug-2008 06:10 -
Datatype.ML 15-Sep-2005 08:17 3k
Datatype.ML.html 09-Aug-2008 06:10 0k
Datatype.thy 17-Jun-2005 07:15 1k
Datatype.thy.html 09-Aug-2008 06:10 0k
Epsilon.thy 17-Jun-2005 07:15 14k
Epsilon.thy.html 09-Aug-2008 06:10 0k
Finite.thy 17-Jun-2005 07:15 7k
Finite.thy.html 09-Aug-2008 06:10 0k
Fixedpt.thy 17-Jun-2005 07:15 10k
Fixedpt.thy.html 09-Aug-2008 06:10 0k
IMP/ 09-Aug-2008 06:10 -
Induct/ 09-Aug-2008 06:10 -
Inductive.ML 09-Nov-2001 13:53 3k
Inductive.ML.html 09-Aug-2008 06:10 0k
Inductive.thy 17-Jun-2005 07:15 1k
Inductive.thy.html 09-Aug-2008 06:10 0k
InfDatatype.thy 17-Jun-2005 07:15 4k
InfDatatype.thy.html 09-Aug-2008 06:10 0k
Integ/ 09-Aug-2008 06:10 -
IsaMakefile 28-Mar-2005 06:19 5k
IsaMakefile.html 09-Aug-2008 06:10 9k
List.thy 17-Jun-2005 07:15 42k
List.thy.html 09-Aug-2008 06:10 0k
Main.ML 12-Jan-2002 07:38 1k
Main.ML.html 09-Aug-2008 06:10 0k
Main.thy 17-Jun-2005 07:15 2k
Main.thy.html 09-Aug-2008 06:10 0k
Main_ZFC.ML 10-May-2002 13:53 3k
Main_ZFC.ML.html 09-Aug-2008 06:10 0k
Main_ZFC.thy 17-Jun-2005 07:15 1k
Main_ZFC.thy.html 09-Aug-2008 06:10 0k
Nat.thy 17-Jun-2005 07:15 9k
Nat.thy.html 09-Aug-2008 06:10 0k
OrdQuant.thy 02-Aug-2005 10:47 12k
OrdQuant.thy.html 09-Aug-2008 06:10 0k
Order.thy 17-Jun-2005 07:15 24k
Order.thy.html 09-Aug-2008 06:10 0k
OrderArith.thy 17-Jun-2005 07:15 20k
OrderArith.thy.html 09-Aug-2008 06:10 0k
OrderType.thy 17-Jun-2005 07:15 39k
OrderType.thy.html 09-Aug-2008 06:10 0k
Ordinal.thy 17-Jun-2005 07:15 25k
Ordinal.thy.html 09-Aug-2008 06:10 0k
Perm.thy 17-Jun-2005 07:15 19k
Perm.thy.html 09-Aug-2008 06:10 0k
QPair.thy 17-Jun-2005 07:15 10k
QPair.thy.html 09-Aug-2008 06:10 0k
QUniv.thy 17-Jun-2005 07:15 8k
QUniv.thy.html 09-Aug-2008 06:10 0k
ROOT.ML 20-Jun-2005 13:13 1k
ROOT.ML.html 09-Aug-2008 06:10 0k
Resid/ 09-Aug-2008 06:10 -
Sum.thy 17-Jun-2005 07:15 6k
Sum.thy.html 09-Aug-2008 06:10 0k
Tools/ 09-Aug-2008 06:10 -
Trancl.thy 17-Jun-2005 07:15 13k
Trancl.thy.html 09-Aug-2008 06:10 0k
UNITY/ 09-Aug-2008 06:10 -
Univ.thy 17-Jun-2005 07:15 28k
Univ.thy.html 09-Aug-2008 06:10 0k
WF.thy 17-Jun-2005 07:15 13k
WF.thy.html 09-Aug-2008 06:10 0k
ZF.thy 17-Jun-2005 07:15 25k
ZF.thy.html 09-Aug-2008 06:10 0k
Zorn.thy 17-Jun-2005 07:15 14k
Zorn.thy.html 09-Aug-2008 06:10 0k
arith_data.ML 01-Aug-2005 10:20 9k
arith_data.ML.html 09-Aug-2008 06:10 0k
document/ 09-Aug-2008 06:10 -
equalities.thy 17-Jun-2005 07:15 36k
equalities.thy.html 09-Aug-2008 06:10 0k
ex/ 09-Aug-2008 06:10 -
func.thy 17-Jun-2005 07:15 21k
func.thy.html 09-Aug-2008 06:10 0k
ind_syntax.ML 15-Jul-2005 06:44 6k
ind_syntax.ML.html 09-Aug-2008 06:10 0k
pair.thy 02-Aug-2005 10:47 5k
pair.thy.html 09-Aug-2008 06:10 0k
simpdata.ML 12-Sep-2005 09:21 2k
simpdata.ML.html 09-Aug-2008 06:10 0k
thy_syntax.ML 03-Mar-2005 03:44 6k
thy_syntax.ML.html 09-Aug-2008 06:10 0k
upair.thy 17-Jun-2005 07:15 17k
upair.thy.html 09-Aug-2008 06:10 0k
ZF/README
ZF: Zermelo-Fraenkel Set Theory
This directory contains the ML sources of the Isabelle system for
ZF Set Theory, based on FOL.
There are several subdirectories of examples:
- 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�ard 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)