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:

Useful references on ZF set theory: