src/ZF/ROOT

tuned

+
−chapter ZF
+
−
+
−session ZF (main timing ZF) = Pure +
+
−  description {*
+
−    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+
−    Copyright   1995  University of Cambridge
+
−
+
−    Zermelo-Fraenkel Set Theory. This theory is the work of Martin Coen,
+
−    Philippe Noel and Lawrence Paulson.
+
−
+
−    Isabelle/ZF formalizes the greater part of elementary set theory, including
+
−    relations, functions, injections, surjections, ordinals and cardinals.
+
−    Results proved include Cantor's Theorem, the Recursion Theorem, the
+
−    Schroeder-Bernstein Theorem, and (assuming AC) the Wellordering Theorem.
+
−
+
−    Isabelle/ZF also provides theories of lists, trees, etc., for formalizing
+
−    computational notions. It supports inductive definitions of
+
−    infinite-branching trees for any cardinality of branching.
+
−
+
−
+
−    Useful references for Isabelle/ZF:
+
−
+
−    Lawrence C. Paulson, Set theory for verification: I. From foundations to
+
−    functions. J. Automated Reasoning 11 (1993), 353-389.
+
−
+
−    Lawrence C. Paulson, Set theory for verification: II. Induction and
+
−    recursion. Report 312, Computer Lab (1993).
+
−
+
−    Lawrence C. Paulson, A fixedpoint approach to implementing (co)inductive
+
−    definitions. In: A. Bundy (editor), CADE-12: 12th International
+
−    Conference on Automated Deduction, (Springer LNAI 814, 1994), 148-161.
+
−
+
−
+
−    Useful references on ZF set theory:
+
−
+
−    Paul R. Halmos, Naive Set Theory (Van Nostrand, 1960)
+
−
+
−    Patrick Suppes, Axiomatic Set Theory (Dover, 1972)
+
−
+
−    Keith J. Devlin, Fundamentals of Contemporary Set Theory (Springer, 1979)
+
−
+
−    Kenneth Kunen, Set Theory: An Introduction to Independence Proofs,
+
−    (North-Holland, 1980)
+
−  *}
+
−  theories
+
−    ZFC
+
−  document_files "root.tex"
+
−
+
−session "ZF-AC" (ZF) in AC = ZF +
+
−  description {*
+
−    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+
−    Copyright   1995  University of Cambridge
+
−
+
−    Proofs of AC-equivalences, due to Krzysztof Grabczewski.
+
−
+
−    See also the book "Equivalents of the Axiom of Choice, II" by H. Rubin and
+
−    J.E. Rubin, 1985.
+
−
+
−    The report
+
−    http://www.cl.cam.ac.uk/Research/Reports/TR377-lcp-mechanising-set-theory.ps.gz
+
−    "Mechanizing Set Theory", by Paulson and Grabczewski, describes both this
+
−    development and ZF's theories of cardinals.
+
−  *}
+
−  theories
+
−    WO6_WO1
+
−    WO1_WO7
+
−    AC7_AC9
+
−    WO1_AC
+
−    AC15_WO6
+
−    WO2_AC16
+
−    AC16_WO4
+
−    AC17_AC1
+
−    AC18_AC19
+
−    DC
+
−  document_files "root.tex" "root.bib"
+
−
+
−session "ZF-Coind" (ZF) in Coind = ZF +
+
−  description {*
+
−    Author:     Jacob Frost, Cambridge University Computer Laboratory
+
−    Copyright   1995  University of Cambridge
+
−
+
−    Coind -- A Coinduction Example.
+
−
+
−    It involves proving the consistency of the dynamic and static semantics for
+
−    a small functional language. A codatatype definition specifies values and
+
−    value environments in mutual recursion: non-well-founded values represent
+
−    recursive functions; value environments are variant functions from
+
−    variables into values.
+
−
+
−    Based upon the article
+
−        Robin Milner and Mads Tofte,
+
−        Co-induction in Relational Semantics,
+
−        Theoretical Computer Science 87 (1991), pages 209-220.
+
−
+
−    Written up as
+
−        Jacob Frost, A Case Study of Co_induction in Isabelle
+
−        Report, Computer Lab, University of Cambridge (1995).
+
−        http://www.cl.cam.ac.uk/Research/Reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz
+
−  *}
+
−  options [document = false]
+
−  theories ECR
+
−
+
−session "ZF-Constructible" (ZF) in Constructible = ZF +
+
−  description {*
+
−    Relative Consistency of the Axiom of Choice:
+
−    Inner Models, Absoluteness and Consistency Proofs.
+
−
+
−    Gödel's proof of the relative consistency of the axiom of choice is
+
−    mechanized using Isabelle/ZF. The proof builds upon a previous
+
−    mechanization of the reflection theorem (see
+
−    http://www.cl.cam.ac.uk/users/lcp/papers/Sets/reflection.pdf). The heavy
+
−    reliance on metatheory in the original proof makes the formalization
+
−    unusually long, and not entirely satisfactory: two parts of the proof do
+
−    not fit together. It seems impossible to solve these problems without
+
−    formalizing the metatheory. However, the present development follows a
+
−    standard textbook, Kunen's Set Theory, and could support the formalization
+
−    of further material from that book. It also serves as an example of what to
+
−    expect when deep mathematics is formalized.
+
−
+
−    A paper describing this development is
+
−    http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-551.pdf
+
−  *}
+
−  theories
+
−    DPow_absolute
+
−    AC_in_L
+
−    Rank_Separation
+
−  document_files "root.tex" "root.bib"
+
−
+
−session "ZF-IMP" (ZF) in IMP = ZF +
+
−  description {*
+
−    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
+
−    Copyright   1994 TUM
+
−
+
−    Formalization of the denotational and operational semantics of a
+
−    simple while-language, including an equivalence proof.
+
−
+
−    The whole development essentially formalizes/transcribes
+
−    chapters 2 and 5 of
+
−
+
−    Glynn Winskel. The Formal Semantics of Programming Languages.
+
−    MIT Press, 1993.
+
−  *}
+
−  options [document = false]
+
−  theories Equiv
+
−  document_files "root.tex" "root.bib"
+
−
+
−session "ZF-Induct" (ZF) in Induct = ZF +
+
−  description {*
+
−    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+
−    Copyright   2001  University of Cambridge
+
−
+
−    Inductive definitions.
+
−  *}
+
−  theories
+
−    (** Datatypes **)
+
−    Datatypes       (*sample datatypes*)
+
−    Binary_Trees    (*binary trees*)
+
−    Term            (*recursion over the list functor*)
+
−    Ntree           (*variable-branching trees; function demo*)
+
−    Tree_Forest     (*mutual recursion*)
+
−    Brouwer         (*Infinite-branching trees*)
+
−    Mutil           (*mutilated chess board*)
+
−
+
−    (*by Sidi Ehmety: Multisets.  A parent is FoldSet, the "fold" function for
+
−    finite sets*)
+
−    Multiset
+
−    Rmap            (*mapping a relation over a list*)
+
−    PropLog         (*completeness of propositional logic*)
+
−
+
−    (*two Coq examples by Christine Paulin-Mohring*)
+
−    ListN
+
−    Acc
+
−
+
−    Comb            (*Combinatory Logic example*)
+
−    Primrec         (*Primitive recursive functions*)
+
−  document_files
+
−    "root.bib"
+
−    "root.tex"
+
−
+
−session "ZF-Resid" (ZF) in Resid = ZF +
+
−  description {*
+
−    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+
−    Copyright   1995  University of Cambridge
+
−
+
−    Residuals -- a proof of the Church-Rosser Theorem for the
+
−    untyped lambda-calculus.
+
−
+
−    By Ole Rasmussen, following the Coq proof given in
+
−
+
−    Gerard Huet.  Residual Theory in Lambda-Calculus: A Formal Development.
+
−    J. Functional Programming 4(3) 1994, 371-394.
+
−
+
−    See Rasmussen's report: The Church-Rosser Theorem in Isabelle: A Proof
+
−    Porting Experiment.
+
−    http://www.cl.cam.ac.uk/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz
+
−  *}
+
−  options [document = false]
+
−  theories Confluence
+
−
+
−session "ZF-UNITY" (timing ZF) in UNITY = ZF +
+
−  description {*
+
−    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+
−    Copyright   1998  University of Cambridge
+
−
+
−    ZF/UNITY proofs.
+
−  *}
+
−  options [document = false]
+
−  theories
+
−    (*Simple examples: no composition*)
+
−    Mutex
+
−
+
−    (*Basic meta-theory*)
+
−    Guar
+
−
+
−    (*Prefix relation; the Allocator example*)
+
−    Distributor Merge ClientImpl AllocImpl
+
−
+
−session "ZF-ex" (ZF) in ex = ZF +
+
−  description {*
+
−    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+
−    Copyright   1993  University of Cambridge
+
−
+
−    Miscellaneous examples for Zermelo-Fraenkel Set Theory.
+
−
+
−    Includes a simple form of Ramsey's theorem. A report is available:
+
−    http://www.cl.cam.ac.uk/Research/Reports/TR271-lcp-set-theory.dvi.Z
+
−
+
−    Several (co)inductive and (co)datatype definitions are presented. The
+
−    report http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz
+
−    describes the theoretical foundations of datatypes while
+
−    href="http://www.cl.cam.ac.uk/Research/Reports/TR320-lcp-isabelle-ind-defs.dvi.gz
+
−    describes the package that automates their declaration.
+
−  *}
+
−  options [document = false]
+
−  theories
+
−    misc
+
−    Ring             (*abstract algebra*)
+
−    Commutation      (*abstract Church-Rosser theory*)
+
−    Primes           (*GCD theory*)
+
−    NatSum           (*Summing integers, squares, cubes, etc.*)
+
−    Ramsey           (*Simple form of Ramsey's theorem*)
+
−    Limit            (*Inverse limit construction of domains*)
+
−    BinEx            (*Binary integer arithmetic*)
+
−    LList CoUnit     (*CoDatatypes*)