Isabelle/FOL sessions

CCL

    Author:     Martin Coen, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

    Classical Computational Logic based on First-Order Logic.

    A computational logic for an untyped functional language with
    evaluation to weak head-normal form.
FOL

    First-Order Logic with Natural Deduction (constructive and classical
    versions). For a classical sequent calculus, see Isabelle/LK.

    Useful references on First-Order Logic:

    Simon Thompson, Type Theory and Functional Programming (Addison-Wesley,
    1991) (The first chapter is an excellent introduction to natural deduction
    in general.)

    Antony Galton, Logic for Information Technology (Wiley, 1990)

    Michael Dummett, Elements of Intuitionism (Oxford, 1977)
FOL-ex

    Examples for First-Order Logic.
FOLP

    Author:     Martin Coen, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

    Modifed version of FOL that contains proof terms.

    Presence of unknown proof term means that matching does not behave as expected.
FOLP-ex

    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1992  University of Cambridge

    Examples for First-Order Logic.
LCF

    Author:     Tobias Nipkow
    Copyright   1992  University of Cambridge

    Logic for Computable Functions.

    Useful references on LCF: Lawrence C. Paulson,
    Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)
ZF

    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)
  
ZF-AC

    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.
ZF-Coind

    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
ZF-Constructible

    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
ZF-IMP

    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.
ZF-Induct

    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   2001  University of Cambridge

    Inductive definitions.
ZF-Resid

    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
ZF-UNITY

    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

    ZF/UNITY proofs.
ZF-ex

    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.