src/ZF/README.html
author wenzelm
Thu Sep 02 00:48:07 2010 +0200 (2010-09-02)
changeset 38980 af73cf0dc31f
parent 36862 952b2b102a0a
permissions -rw-r--r--
turned show_question_marks into proper configuration option;
show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;
tuned;
webertj@15283
     1
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
webertj@15283
     2
webertj@15582
     3
<HTML>
webertj@15582
     4
webertj@15582
     5
<HEAD>
webertj@15582
     6
  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
webertj@15582
     7
  <TITLE>ZF/README</TITLE>
webertj@15582
     8
</HEAD>
webertj@15582
     9
webertj@15582
    10
<BODY>
clasohm@1341
    11
clasohm@1341
    12
<H2>ZF: Zermelo-Fraenkel Set Theory</H2>
clasohm@1341
    13
wenzelm@3279
    14
This directory contains the ML sources of the Isabelle system for
wenzelm@3279
    15
ZF Set Theory, based on FOL.<p>
clasohm@1341
    16
wenzelm@3279
    17
There are several subdirectories of examples:
clasohm@1341
    18
<DL>
clasohm@1341
    19
<DT>AC
clasohm@1341
    20
<DD>subdirectory containing proofs from the book "Equivalents of the Axiom
clasohm@1341
    21
of Choice, II" by H. Rubin and J.E. Rubin, 1985.  Thanks to Krzysztof
clasohm@1341
    22
Gr`abczewski.<P>
clasohm@1341
    23
clasohm@1341
    24
<DT>Coind
clasohm@1341
    25
<DD>subdirectory containing a large example of proof by co-induction.  It
clasohm@1341
    26
is by Jacob Frost following a paper by Robin Milner and Mads Tofte.<P>
clasohm@1341
    27
clasohm@1341
    28
<DT>IMP
clasohm@1341
    29
<DD>subdirectory containing a semantics equivalence proof between
clasohm@1341
    30
operational and denotational definitions of a simple programming language.
clasohm@1341
    31
Thanks to Heiko Loetzbeyer & Robert Sandner.<P>
clasohm@1341
    32
clasohm@1341
    33
<DT>Resid
clasohm@1341
    34
<DD>subdirectory containing a proof of the Church-Rosser Theorem.  It is
webertj@15283
    35
by Ole Rasmussen, following the Coq proof by G´┐Żard Huet.<P>
clasohm@1341
    36
clasohm@1341
    37
<DT>ex
clasohm@1341
    38
<DD>subdirectory containing various examples.
clasohm@1341
    39
</DL>
clasohm@1341
    40
clasohm@1341
    41
Isabelle/ZF formalizes the greater part of elementary set theory,
clasohm@1341
    42
including relations, functions, injections, surjections, ordinals and
clasohm@1341
    43
cardinals.  Results proved include Cantor's Theorem, the Recursion
clasohm@1341
    44
Theorem, the Schroeder-Bernstein Theorem, and (assuming AC) the
clasohm@1341
    45
Wellordering Theorem.<P>
clasohm@1341
    46
clasohm@1341
    47
Isabelle/ZF also provides theories of lists, trees, etc., for
clasohm@1341
    48
formalizing computational notions.  It supports inductive definitions
clasohm@1341
    49
of infinite-branching trees for any cardinality of branching.<P>
clasohm@1341
    50
clasohm@1341
    51
Useful references for Isabelle/ZF:
clasohm@1341
    52
clasohm@1341
    53
<UL>
clasohm@1341
    54
<LI>	Lawrence C. Paulson,<BR>
clasohm@1341
    55
	Set theory for verification: I. From foundations to functions.<BR>
clasohm@1341
    56
	J. Automated Reasoning 11 (1993), 353-389.
clasohm@1341
    57
clasohm@1341
    58
<LI>	Lawrence C. Paulson,<BR>
clasohm@1341
    59
	Set theory for verification: II. Induction and recursion.<BR>
clasohm@1341
    60
	Report 312, Computer Lab (1993).<BR>
clasohm@1341
    61
clasohm@1341
    62
<LI>	Lawrence C. Paulson,<BR>
clasohm@1341
    63
	A fixedpoint approach to implementing (co)inductive definitions. <BR> 
clasohm@1341
    64
	In: A. Bundy (editor),<BR>
clasohm@1341
    65
	CADE-12: 12th International Conference on Automated Deduction,<BR>
clasohm@1341
    66
	(Springer LNAI 814, 1994), 148-161.
clasohm@1341
    67
</UL>
clasohm@1341
    68
clasohm@1341
    69
Useful references on ZF set theory:
clasohm@1341
    70
clasohm@1341
    71
<UL>
clasohm@1341
    72
<LI>	Paul R. Halmos, Naive Set Theory (Van Nostrand, 1960)
clasohm@1341
    73
clasohm@1341
    74
<LI>	Patrick Suppes, Axiomatic Set Theory (Dover, 1972)
clasohm@1341
    75
clasohm@1341
    76
<LI>	Keith J. Devlin,<BR>
clasohm@1341
    77
	Fundamentals of Contemporary Set Theory (Springer, 1979)
clasohm@1341
    78
clasohm@1341
    79
<LI>	Kenneth Kunen<BR>
clasohm@1341
    80
	Set Theory: An Introduction to Independence Proofs<BR>
clasohm@1341
    81
	(North-Holland, 1980)
clasohm@1341
    82
</UL>
clasohm@1341
    83
clasohm@1341
    84
</BODY></HTML>