src/ZF/README
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 1062 c79fb313bf89
permissions -rw-r--r--
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
		ZF: Zermelo-Fraenkel Set Theory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
This directory contains the Standard ML sources of the Isabelle system for
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
ZF Set Theory.  It is loaded upon FOL, not Pure Isabelle.  Important files
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
include
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
958
f2c225386348 Now mentions Coind
lcp
parents: 488
diff changeset
     7
Makefile -- compiles the files under Poly/ML or SML of New Jersey.  Can also
f2c225386348 Now mentions Coind
lcp
parents: 488
diff changeset
     8
run all the tests described below.
f2c225386348 Now mentions Coind
lcp
parents: 488
diff changeset
     9
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
ROOT.ML -- loads all source files.  Enter an ML image containing FOL and
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
type: use "ROOT.ML";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
1062
c79fb313bf89 New examples directories Resid and AC
lcp
parents: 958
diff changeset
    13
There are also several subdirectories of examples.  To execute the examples on
c79fb313bf89 New examples directories Resid and AC
lcp
parents: 958
diff changeset
    14
some directory <Dir>, enter an ML image containing ZF and type
c79fb313bf89 New examples directories Resid and AC
lcp
parents: 958
diff changeset
    15
	use "<Dir>/ROOT.ML";
c79fb313bf89 New examples directories Resid and AC
lcp
parents: 958
diff changeset
    16
c79fb313bf89 New examples directories Resid and AC
lcp
parents: 958
diff changeset
    17
AC -- subdirectory containing proofs from the book "Equivalents of the Axiom
c79fb313bf89 New examples directories Resid and AC
lcp
parents: 958
diff changeset
    18
of Choice, II" by H. Rubin and J.E. Rubin, 1985.  Thanks to Krzysztof
c79fb313bf89 New examples directories Resid and AC
lcp
parents: 958
diff changeset
    19
Gr`abczewski. 
c79fb313bf89 New examples directories Resid and AC
lcp
parents: 958
diff changeset
    20
c79fb313bf89 New examples directories Resid and AC
lcp
parents: 958
diff changeset
    21
Coind -- subdirectory containing a large example of proof by co-induction.  It
c79fb313bf89 New examples directories Resid and AC
lcp
parents: 958
diff changeset
    22
is by Jacob Frost following a paper by Robin Milner and Mads Tofte.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    24
IMP -- subdirectory containing a semantics equivalence proof between
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    25
operational and denotational definitions of a simple programming language.
1062
c79fb313bf89 New examples directories Resid and AC
lcp
parents: 958
diff changeset
    26
Thanks to Heiko Loetzbeyer & Robert Sandner.
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    27
1062
c79fb313bf89 New examples directories Resid and AC
lcp
parents: 958
diff changeset
    28
Resid -- subdirectory containing a proof of the Church-Rosser Theorem.  It is
c79fb313bf89 New examples directories Resid and AC
lcp
parents: 958
diff changeset
    29
by Ole Rasmussen, following the Coq proof by Gérard Huet.
c79fb313bf89 New examples directories Resid and AC
lcp
parents: 958
diff changeset
    30
c79fb313bf89 New examples directories Resid and AC
lcp
parents: 958
diff changeset
    31
ex -- subdirectory containing various examples.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    33
Isabelle/ZF formalizes the greater part of elementary set theory, including
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    34
relations, functions, injections, surjections, ordinals and cardinals.
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    35
Results proved include Cantor's Theorem, the Recursion Theorem, the
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    36
Schroeder-Bernstein Theorem, and (assuming AC) the Wellordering Theorem.
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    37
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    38
Isabelle/ZF also provides theories of lists, trees, etc., for formalizing
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    39
computational notions.  It supports inductive definitions of
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    40
infinite-branching trees for any cardinality of branching.
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    41
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    42
Useful references for Isabelle/ZF:
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    43
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    44
	Lawrence C. Paulson,
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    45
	Set theory for verification: I. From foundations to functions.
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    46
	J. Automated Reasoning 11 (1993), 353-389.
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    47
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    48
	Lawrence C. Paulson,
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    49
	Set theory for verification: II. Induction and recursion.
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    50
	Report 312, Computer Lab (1993).
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    51
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    52
	Lawrence C. Paulson,
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    53
	A fixedpoint approach to implementing (co)inductive definitions.  
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    54
	In: A. Bundy (editor),
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    55
	CADE-12: 12th International Conference on Automated Deduction,
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    56
	(Springer LNAI 814, 1994), 148-161.
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    57
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
Useful references on ZF set theory:
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
	Paul R. Halmos, Naive Set Theory (Van Nostrand, 1960)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
	Patrick Suppes, Axiomatic Set Theory (Dover, 1972)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
	Keith J. Devlin,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
	Fundamentals of Contemporary Set Theory (Springer, 1979)
488
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    66
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    67
	Kenneth Kunen
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    68
	Set Theory: An Introduction to Independence Proofs
52f7447d4f1b Addition of infinite branching datatypes
lcp
parents: 0
diff changeset
    69
	(North-Holland, 1980)
958
f2c225386348 Now mentions Coind
lcp
parents: 488
diff changeset
    70
f2c225386348 Now mentions Coind
lcp
parents: 488
diff changeset
    71
$Id$