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