- ZF
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
Zermelo-Fraenkel Set Theory. This theory is the work of Martin Coen,
Philippe Noel and Lawrence Paulson.
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)
- ZF-AC
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
Proofs of AC-equivalences, due to Krzysztof Grabczewski.
See also the book "Equivalents of the Axiom of Choice, II" by H. Rubin and
J.E. Rubin, 1985.
The report
http://www.cl.cam.ac.uk/Research/Reports/TR377-lcp-mechanising-set-theory.ps.gz
"Mechanizing Set Theory", by Paulson and Grabczewski, describes both this
development and ZF's theories of cardinals.
- ZF-Coind
Author: Jacob Frost, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
Coind -- A Coinduction Example.
It involves proving the consistency of the dynamic and static semantics for
a small functional language. A codatatype definition specifies values and
value environments in mutual recursion: non-well-founded values represent
recursive functions; value environments are variant functions from
variables into values.
Based upon the article
Robin Milner and Mads Tofte,
Co-induction in Relational Semantics,
Theoretical Computer Science 87 (1991), pages 209-220.
Written up as
Jacob Frost, A Case Study of Co_induction in Isabelle
Report, Computer Lab, University of Cambridge (1995).
http://www.cl.cam.ac.uk/Research/Reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz
- ZF-Constructible
Relative Consistency of the Axiom of Choice:
Inner Models, Absoluteness and Consistency Proofs.
Gödel's proof of the relative consistency of the axiom of choice is
mechanized using Isabelle/ZF. The proof builds upon a previous
mechanization of the reflection theorem (see
http://www.cl.cam.ac.uk/users/lcp/papers/Sets/reflection.pdf). The heavy
reliance on metatheory in the original proof makes the formalization
unusually long, and not entirely satisfactory: two parts of the proof do
not fit together. It seems impossible to solve these problems without
formalizing the metatheory. However, the present development follows a
standard textbook, Kunen's Set Theory, and could support the formalization
of further material from that book. It also serves as an example of what to
expect when deep mathematics is formalized.
A paper describing this development is
http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-551.pdf
- ZF-IMP
Author: Heiko Loetzbeyer & Robert Sandner, TUM
Copyright 1994 TUM
Formalization of the denotational and operational semantics of a
simple while-language, including an equivalence proof.
The whole development essentially formalizes/transcribes
chapters 2 and 5 of
Glynn Winskel. The Formal Semantics of Programming Languages.
MIT Press, 1993.
- ZF-Induct
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 2001 University of Cambridge
Inductive definitions.
- ZF-Resid
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
Residuals -- a proof of the Church-Rosser Theorem for the
untyped lambda-calculus.
By Ole Rasmussen, following the Coq proof given in
Gerard Huet. Residual Theory in Lambda-Calculus: A Formal Development.
J. Functional Programming 4(3) 1994, 371-394.
See Rasmussen's report: The Church-Rosser Theorem in Isabelle: A Proof
Porting Experiment.
http://www.cl.cam.ac.uk/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz
- ZF-UNITY
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
ZF/UNITY proofs.
- ZF-ex
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Miscellaneous examples for Zermelo-Fraenkel Set Theory.
Includes a simple form of Ramsey's theorem. A report is available:
http://www.cl.cam.ac.uk/Research/Reports/TR271-lcp-set-theory.dvi.Z
Several (co)inductive and (co)datatype definitions are presented. The
report http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz
describes the theoretical foundations of datatypes while
href="http://www.cl.cam.ac.uk/Research/Reports/TR320-lcp-isabelle-ind-defs.dvi.gz
describes the package that automates their declaration.