src/ZF/ROOT
author wenzelm
Mon Oct 30 20:04:10 2017 +0100 (20 months ago)
changeset 66946 3d8fd98c7c86
parent 66778 cf0187ca3a57
child 69272 15e9ed5b28fb
permissions -rw-r--r--
ROOT cleanup: empty 'document_files' means there is no document;
     1 chapter ZF
     2 
     3 session ZF (main timing) = Pure +
     4   description {*
     5     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6     Copyright   1995  University of Cambridge
     7 
     8     Zermelo-Fraenkel Set Theory. This theory is the work of Martin Coen,
     9     Philippe Noel and Lawrence Paulson.
    10 
    11     Isabelle/ZF formalizes the greater part of elementary set theory, including
    12     relations, functions, injections, surjections, ordinals and cardinals.
    13     Results proved include Cantor's Theorem, the Recursion Theorem, the
    14     Schroeder-Bernstein Theorem, and (assuming AC) the Wellordering Theorem.
    15 
    16     Isabelle/ZF also provides theories of lists, trees, etc., for formalizing
    17     computational notions. It supports inductive definitions of
    18     infinite-branching trees for any cardinality of branching.
    19 
    20 
    21     Useful references for Isabelle/ZF:
    22 
    23     Lawrence C. Paulson, Set theory for verification: I. From foundations to
    24     functions. J. Automated Reasoning 11 (1993), 353-389.
    25 
    26     Lawrence C. Paulson, Set theory for verification: II. Induction and
    27     recursion. Report 312, Computer Lab (1993).
    28 
    29     Lawrence C. Paulson, A fixedpoint approach to implementing (co)inductive
    30     definitions. In: A. Bundy (editor), CADE-12: 12th International
    31     Conference on Automated Deduction, (Springer LNAI 814, 1994), 148-161.
    32 
    33 
    34     Useful references on ZF set theory:
    35 
    36     Paul R. Halmos, Naive Set Theory (Van Nostrand, 1960)
    37 
    38     Patrick Suppes, Axiomatic Set Theory (Dover, 1972)
    39 
    40     Keith J. Devlin, Fundamentals of Contemporary Set Theory (Springer, 1979)
    41 
    42     Kenneth Kunen, Set Theory: An Introduction to Independence Proofs,
    43     (North-Holland, 1980)
    44   *}
    45   sessions
    46     FOL
    47   theories
    48     ZF (global)
    49     ZFC (global)
    50   document_files "root.tex"
    51 
    52 session "ZF-AC" in AC = ZF +
    53   description {*
    54     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    55     Copyright   1995  University of Cambridge
    56 
    57     Proofs of AC-equivalences, due to Krzysztof Grabczewski.
    58 
    59     See also the book "Equivalents of the Axiom of Choice, II" by H. Rubin and
    60     J.E. Rubin, 1985.
    61 
    62     The report
    63     http://www.cl.cam.ac.uk/Research/Reports/TR377-lcp-mechanising-set-theory.ps.gz
    64     "Mechanizing Set Theory", by Paulson and Grabczewski, describes both this
    65     development and ZF's theories of cardinals.
    66   *}
    67   theories
    68     WO6_WO1
    69     WO1_WO7
    70     AC7_AC9
    71     WO1_AC
    72     AC15_WO6
    73     WO2_AC16
    74     AC16_WO4
    75     AC17_AC1
    76     AC18_AC19
    77     DC
    78   document_files "root.tex" "root.bib"
    79 
    80 session "ZF-Coind" in Coind = ZF +
    81   description {*
    82     Author:     Jacob Frost, Cambridge University Computer Laboratory
    83     Copyright   1995  University of Cambridge
    84 
    85     Coind -- A Coinduction Example.
    86 
    87     It involves proving the consistency of the dynamic and static semantics for
    88     a small functional language. A codatatype definition specifies values and
    89     value environments in mutual recursion: non-well-founded values represent
    90     recursive functions; value environments are variant functions from
    91     variables into values.
    92 
    93     Based upon the article
    94         Robin Milner and Mads Tofte,
    95         Co-induction in Relational Semantics,
    96         Theoretical Computer Science 87 (1991), pages 209-220.
    97 
    98     Written up as
    99         Jacob Frost, A Case Study of Co_induction in Isabelle
   100         Report, Computer Lab, University of Cambridge (1995).
   101         http://www.cl.cam.ac.uk/Research/Reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz
   102   *}
   103   theories ECR
   104 
   105 session "ZF-Constructible" in Constructible = ZF +
   106   description {*
   107     Relative Consistency of the Axiom of Choice:
   108     Inner Models, Absoluteness and Consistency Proofs.
   109 
   110     Gödel's proof of the relative consistency of the axiom of choice is
   111     mechanized using Isabelle/ZF. The proof builds upon a previous
   112     mechanization of the reflection theorem (see
   113     http://www.cl.cam.ac.uk/users/lcp/papers/Sets/reflection.pdf). The heavy
   114     reliance on metatheory in the original proof makes the formalization
   115     unusually long, and not entirely satisfactory: two parts of the proof do
   116     not fit together. It seems impossible to solve these problems without
   117     formalizing the metatheory. However, the present development follows a
   118     standard textbook, Kunen's Set Theory, and could support the formalization
   119     of further material from that book. It also serves as an example of what to
   120     expect when deep mathematics is formalized.
   121 
   122     A paper describing this development is
   123     http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-551.pdf
   124   *}
   125   theories
   126     DPow_absolute
   127     AC_in_L
   128     Rank_Separation
   129   document_files "root.tex" "root.bib"
   130 
   131 session "ZF-IMP" in IMP = ZF +
   132   description {*
   133     Author:     Heiko Loetzbeyer & Robert Sandner, TUM
   134     Copyright   1994 TUM
   135 
   136     Formalization of the denotational and operational semantics of a
   137     simple while-language, including an equivalence proof.
   138 
   139     The whole development essentially formalizes/transcribes
   140     chapters 2 and 5 of
   141 
   142     Glynn Winskel. The Formal Semantics of Programming Languages.
   143     MIT Press, 1993.
   144   *}
   145   theories Equiv
   146   document_files
   147     "root.tex"
   148     "root.bib"
   149 
   150 session "ZF-Induct" in Induct = ZF +
   151   description {*
   152     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   153     Copyright   2001  University of Cambridge
   154 
   155     Inductive definitions.
   156   *}
   157   theories
   158     (** Datatypes **)
   159     Datatypes       (*sample datatypes*)
   160     Binary_Trees    (*binary trees*)
   161     Term            (*recursion over the list functor*)
   162     Ntree           (*variable-branching trees; function demo*)
   163     Tree_Forest     (*mutual recursion*)
   164     Brouwer         (*Infinite-branching trees*)
   165     Mutil           (*mutilated chess board*)
   166 
   167     (*by Sidi Ehmety: Multisets.  A parent is FoldSet, the "fold" function for
   168     finite sets*)
   169     Multiset
   170     Rmap            (*mapping a relation over a list*)
   171     PropLog         (*completeness of propositional logic*)
   172 
   173     (*two Coq examples by Christine Paulin-Mohring*)
   174     ListN
   175     Acc
   176 
   177     Comb            (*Combinatory Logic example*)
   178     Primrec         (*Primitive recursive functions*)
   179   document_files
   180     "root.bib"
   181     "root.tex"
   182 
   183 session "ZF-Resid" in Resid = ZF +
   184   description {*
   185     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   186     Copyright   1995  University of Cambridge
   187 
   188     Residuals -- a proof of the Church-Rosser Theorem for the
   189     untyped lambda-calculus.
   190 
   191     By Ole Rasmussen, following the Coq proof given in
   192 
   193     Gerard Huet.  Residual Theory in Lambda-Calculus: A Formal Development.
   194     J. Functional Programming 4(3) 1994, 371-394.
   195 
   196     See Rasmussen's report: The Church-Rosser Theorem in Isabelle: A Proof
   197     Porting Experiment.
   198     http://www.cl.cam.ac.uk/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz
   199   *}
   200   theories Confluence
   201 
   202 session "ZF-UNITY" (timing) in UNITY = "ZF-Induct" +
   203   description {*
   204     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   205     Copyright   1998  University of Cambridge
   206 
   207     ZF/UNITY proofs.
   208   *}
   209   theories
   210     (*Simple examples: no composition*)
   211     Mutex
   212 
   213     (*Basic meta-theory*)
   214     Guar
   215 
   216     (*Prefix relation; the Allocator example*)
   217     Distributor Merge ClientImpl AllocImpl
   218 
   219 session "ZF-ex" in ex = ZF +
   220   description {*
   221     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   222     Copyright   1993  University of Cambridge
   223 
   224     Miscellaneous examples for Zermelo-Fraenkel Set Theory.
   225 
   226     Includes a simple form of Ramsey's theorem. A report is available:
   227     http://www.cl.cam.ac.uk/Research/Reports/TR271-lcp-set-theory.dvi.Z
   228 
   229     Several (co)inductive and (co)datatype definitions are presented. The
   230     report http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz
   231     describes the theoretical foundations of datatypes while
   232     href="http://www.cl.cam.ac.uk/Research/Reports/TR320-lcp-isabelle-ind-defs.dvi.gz
   233     describes the package that automates their declaration.
   234   *}
   235   theories
   236     misc
   237     Ring             (*abstract algebra*)
   238     Commutation      (*abstract Church-Rosser theory*)
   239     Primes           (*GCD theory*)
   240     NatSum           (*Summing integers, squares, cubes, etc.*)
   241     Ramsey           (*Simple form of Ramsey's theorem*)
   242     Limit            (*Inverse limit construction of domains*)
   243     BinEx            (*Binary integer arithmetic*)
   244     LList CoUnit     (*CoDatatypes*)