src/ZF/ROOT

more explicit errors in pathological cases

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
    Main
    Main_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*)