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