chapter ZF
session ZF (main ZF) = Pure +
description {*
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)
*}
theories
Main
Main_ZFC
document_files "root.tex"
session "ZF-AC" (ZF) in AC = ZF +
description {*
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.
*}
theories
WO6_WO1
WO1_WO7
AC7_AC9
WO1_AC
AC15_WO6
WO2_AC16
AC16_WO4
AC17_AC1
AC18_AC19
DC
document_files "root.tex" "root.bib"
session "ZF-Coind" (ZF) in Coind = ZF +
description {*
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
*}
options [document = false]
theories ECR
session "ZF-Constructible" (ZF) in Constructible = ZF +
description {*
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
*}
theories
DPow_absolute
AC_in_L
Rank_Separation
document_files "root.tex" "root.bib"
session "ZF-IMP" (ZF) in IMP = ZF +
description {*
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.
*}
options [document = false]
theories Equiv
document_files "root.tex" "root.bib"
session "ZF-Induct" (ZF) in Induct = ZF +
description {*
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 2001 University of Cambridge
Inductive definitions.
*}
theories
(** Datatypes **)
Datatypes (*sample datatypes*)
Binary_Trees (*binary trees*)
Term (*recursion over the list functor*)
Ntree (*variable-branching trees; function demo*)
Tree_Forest (*mutual recursion*)
Brouwer (*Infinite-branching trees*)
Mutil (*mutilated chess board*)
(*by Sidi Ehmety: Multisets. A parent is FoldSet, the "fold" function for
finite sets*)
Multiset
Rmap (*mapping a relation over a list*)
PropLog (*completeness of propositional logic*)
(*two Coq examples by Christine Paulin-Mohring*)
ListN
Acc
Comb (*Combinatory Logic example*)
Primrec (*Primitive recursive functions*)
document_files
"root.bib"
"root.tex"
session "ZF-Resid" (ZF) in Resid = ZF +
description {*
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
*}
options [document = false]
theories Confluence
session "ZF-UNITY" (ZF) in UNITY = ZF +
description {*
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
ZF/UNITY proofs.
*}
options [document = false]
theories
(*Simple examples: no composition*)
Mutex
(*Basic meta-theory*)
Guar
(*Prefix relation; the Allocator example*)
Distributor Merge ClientImpl AllocImpl
session "ZF-ex" (ZF) in ex = ZF +
description {*
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.
*}
options [document = false]
theories
misc
Ring (*abstract algebra*)
Commutation (*abstract Church-Rosser theory*)
Primes (*GCD theory*)
NatSum (*Summing integers, squares, cubes, etc.*)
Ramsey (*Simple form of Ramsey's theorem*)
Limit (*Inverse limit construction of domains*)
BinEx (*Binary integer arithmetic*)
LList CoUnit (*CoDatatypes*)