# HG changeset patch # User wenzelm # Date 1363121988 -3600 # Node ID 2ff3a5589b055bfc13d3584503c1b787e4afb62f # Parent b05cd411d3d3d833b486a7e4dd3cee8dde2fa81d refurbished some old README.html files as session descriptions, which show up in chapter index; diff -r b05cd411d3d3 -r 2ff3a5589b05 src/CTT/README.html --- a/src/CTT/README.html Tue Mar 12 20:03:04 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ - - - - - - - CTT/README - - - - -

CTT: Constructive Type Theory

- -This is a version of Constructive Type Theory (extensional equality, no universes).

- -Useful references on Constructive Type Theory: - -

- - - diff -r b05cd411d3d3 -r 2ff3a5589b05 src/CTT/ROOT --- a/src/CTT/ROOT Tue Mar 12 20:03:04 2013 +0100 +++ b/src/CTT/ROOT Tue Mar 12 21:59:48 2013 +0100 @@ -4,6 +4,17 @@ description {* Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge + + This is a version of Constructive Type Theory (extensional equality, + no universes). + + Useful references on Constructive Type Theory: + + B. Nordström, K. Petersson and J. M. Smith, Programming in Martin-Löf's + Type Theory (Oxford University Press, 1990) + + Simon Thompson, Type Theory and Functional Programming (Addison-Wesley, + 1991) *} options [document = false] theories Main diff -r b05cd411d3d3 -r 2ff3a5589b05 src/Cube/README.html --- a/src/Cube/README.html Tue Mar 12 20:03:04 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,30 +0,0 @@ - - - - - - - Cube/README - - - - -

Cube: Barendregt's Lambda-Cube

- -This directory contains the theory sources for the Lambda-Cube in -Isabelle/Pure.

- -The ex subdirectory contains some examples.

- -NB: the formalization is not completely sound! It does not enforce -distinctness of variable names in contexts!

- -For more information about the Lambda-Cube, see - -

- - diff -r b05cd411d3d3 -r 2ff3a5589b05 src/Cube/ROOT --- a/src/Cube/ROOT Tue Mar 12 20:03:04 2013 +0100 +++ b/src/Cube/ROOT Tue Mar 12 21:59:48 2013 +0100 @@ -5,7 +5,13 @@ Author: Tobias Nipkow Copyright 1992 University of Cambridge - The Lambda-Cube a la Barendregt. + Barendregt's Lambda-Cube. + + NB: the formalization is not completely sound! It does not enforce + distinctness of variable names in contexts! + + For more information about the Lambda-Cube, see H. Barendregt, Introduction + to Generalised Type Systems, J. Functional Programming. *} options [document = false] theories Example diff -r b05cd411d3d3 -r 2ff3a5589b05 src/FOL/README.html --- a/src/FOL/README.html Tue Mar 12 20:03:04 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,30 +0,0 @@ - - - - - - - FOL/README - - - - -

FOL: First-Order Logic with Natural Deduction

- -This directory contains the ML sources of the Isabelle system for -First-Order Logic (constructive and classical versions). For a -classical sequent calculus, see LK.

- -The ex subdirectory contains some examples.

- -Useful references on First-Order Logic: - -

- - diff -r b05cd411d3d3 -r 2ff3a5589b05 src/FOL/ROOT --- a/src/FOL/ROOT Tue Mar 12 20:03:04 2013 +0100 +++ b/src/FOL/ROOT Tue Mar 12 21:59:48 2013 +0100 @@ -1,12 +1,28 @@ chapter FOL session FOL = Pure + - description "First-Order Logic with Natural Deduction" + description {* + 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) + *} options [proofs = 2] theories FOL files "document/root.tex" session "FOL-ex" in ex = FOL + + description {* + Examples for First-Order Logic. + *} theories First_Order_Logic Natural_Numbers diff -r b05cd411d3d3 -r 2ff3a5589b05 src/HOL/HOLCF/FOCUS/README.html --- a/src/HOL/HOLCF/FOCUS/README.html Tue Mar 12 20:03:04 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,22 +0,0 @@ - - - - - - - HOLCF/README - - - - -

FOCUS: a theory of stream-processing functions Isabelle/HOLCF

- -For introductions to FOCUSs, see - -For slides on Buffer.thy, see Coinduction beats induction on streams. - - diff -r b05cd411d3d3 -r 2ff3a5589b05 src/HOL/HOLCF/IMP/README.html --- a/src/HOL/HOLCF/IMP/README.html Tue Mar 12 20:03:04 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,18 +0,0 @@ - - - - - - - HOLCF/IMP/README - - - - -

IMP -- A WHILE-language and its Semantics

- -This is the HOLCF-based denotational semantics of a simple -WHILE-language. For a full description see HOL/IMP. - - diff -r b05cd411d3d3 -r 2ff3a5589b05 src/HOL/HOLCF/IOA/README.html --- a/src/HOL/HOLCF/IOA/README.html Tue Mar 12 20:03:04 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,24 +0,0 @@ - - - - - - - HOLCF/IOA/README - - - - -

IOA: A formalization of I/O automata in HOLCF

- -Author: Olaf Müller
-Copyright 1997 Technische Universität München

- -The distribution contains simulation relations, temporal logic, and an abstraction theory. -Everything is based upon a domain-theoretic model of finite and infinite sequences. -

-For details see the IOA project. - - - - diff -r b05cd411d3d3 -r 2ff3a5589b05 src/HOL/Hahn_Banach/README.html --- a/src/HOL/Hahn_Banach/README.html Tue Mar 12 20:03:04 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,36 +0,0 @@ - - - - - - - HOL/Hahn_Banach/README - - - - -

The Hahn-Banach Theorem for Real Vector Spaces (Isabelle/Isar)

- -Author: Gertrud Bauer, Technische Universität München

- -This directory contains the proof of the Hahn-Banach theorem for real vectorspaces, -following H. Heuser, Funktionalanalysis, p. 228 -232. -The Hahn-Banach theorem is one of the fundamental theorems of functioal analysis. -It is a conclusion of Zorn's lemma.

- -Two different formaulations of the theorem are presented, one for general real vectorspaces -and its application to normed vectorspaces.

- -The theorem says, that every continous linearform, defined on arbitrary subspaces -(not only one-dimensional subspaces), can be extended to a continous linearform on -the whole vectorspace. - - -

- -
-bauerg@in.tum.de -
- - - diff -r b05cd411d3d3 -r 2ff3a5589b05 src/HOL/IMPP/README.html --- a/src/HOL/IMPP/README.html Tue Mar 12 20:03:04 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,21 +0,0 @@ - - - - - - - - - HOL/IMPP/README - - - - -

IMPP--An imperative language with procedures

- -This is an extension of IMP with local variables -and mutually recursive procedures. For documentation see - -Hoare Logic for Mutual Recursion and Local Variables. - - diff -r b05cd411d3d3 -r 2ff3a5589b05 src/HOL/IOA/README.html --- a/src/HOL/IOA/README.html Tue Mar 12 20:03:04 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,25 +0,0 @@ - - - - - - - HOLCF/IOA/README - - - - -

IOA: A basic formalization of I/O automata in HOL

- -Author: Konrad Slind, Tobias Nipkow and Olaf Müller
-Copyright 1995,1996 Technische Universität München - -

- -This directory contains a formalization of the meta theory of I/O automata in HOL. -This formalization has been significantly changed and extended. The new version -is available in the subdirectory HOLCF/IOA. There are also the proofs of two -communication protocols which formerly have been here. - - - diff -r b05cd411d3d3 -r 2ff3a5589b05 src/HOL/Induct/README.html --- a/src/HOL/Induct/README.html Tue Mar 12 20:03:04 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,42 +0,0 @@ - - - - - - - HOL/Induct/README - - - - -

Induct--Examples of (Co)Inductive Definitions

- -

This directory is a collection of small examples to demonstrate -Isabelle/HOL's (co)inductive definitions package. Large examples appear on -many other directories, such as Auth, IMP and Lambda. - -

- -
- -
-lcp@cl.cam.ac.uk -
- diff -r b05cd411d3d3 -r 2ff3a5589b05 src/HOL/Isar_Examples/README.html --- a/src/HOL/Isar_Examples/README.html Tue Mar 12 20:03:04 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,19 +0,0 @@ - - - - - - - HOL/Isar_Examples - - - -

HOL/Isar_Examples

- -Isar offers a new high-level proof (and theory) language interface to -Isabelle. This directory contains some example Isar documents. See -also the included document, or the Isabelle/Isar page for more -information. - - diff -r b05cd411d3d3 -r 2ff3a5589b05 src/HOL/Prolog/README.html --- a/src/HOL/Prolog/README.html Tue Mar 12 20:03:04 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,20 +0,0 @@ - - - - - - - - - HOL/Prolog/README - - - -

Prolog -- A bare-bones implementation of Lambda-Prolog

- -This is a simple exploratory implementation of -Lambda-Prolog in HOL, -including some minimal examples (in Test.thy) and a more typical example -of a little functional language and its type system. - - diff -r b05cd411d3d3 -r 2ff3a5589b05 src/HOL/Proofs/Lambda/README.html --- a/src/HOL/Proofs/Lambda/README.html Tue Mar 12 20:03:04 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,29 +0,0 @@ - - - - - - - HOL/Lambda - - - - -

Lambda Calculus in de Bruijn's Notation

- -This theory defines lambda-calculus terms with de Bruijn indixes and proves -confluence of beta, eta and beta+eta. -

- - -The paper - -More Church-Rosser Proofs (in Isabelle/HOL) -describes the whole theory. - -

- -

Last modified 20.5.2000 - - - diff -r b05cd411d3d3 -r 2ff3a5589b05 src/HOL/README.html --- a/src/HOL/README.html Tue Mar 12 20:03:04 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,121 +0,0 @@ - - - - - - - HOL/README - - - - -

HOL: Higher-Order Logic

- -These are the main sources of the Isabelle system for Higher-Order Logic. - -

- -There are also several example sessions: -

- -
Algebra -
rings and univariate polynomials - -
Auth -
a new approach to verifying authentication protocols - -
AxClasses -
a few basic examples of using axiomatic type classes - -
Complex -
a development of the complex numbers, the reals, and the hyper-reals, -which are used in non-standard analysis (builds the image HOL-Complex) - -
Hoare -
verification of imperative programs (verification conditions are -generated automatically from pre/post conditions and loop invariants) - -
HoareParallel -
verification of shared-variable imperative programs a la Owicki-Gries. -(verification conditions are generated automatically) - -
Hyperreal -
Nonstandard analysis. Builds on Real and is part of Complex. - -
IMP -
mechanization of a large part of a semantics text by Glynn Winskel - -
IMPP -
extension of IMP with local variables and mutually recursive -procedures - -
Import -
theories imported from other (HOL) theorem provers. - -
Induct -
examples of (co)inductive definitions - -
IOA -
a simple theory of Input/Output Automata - -
Isar_Examples -
several introductory examples using Isabelle/Isar - -
Lambda -
fundamental properties of lambda-calculus (Church-Rosser and termination) - -
Lattice -
lattices and order structures (in Isabelle/Isar) - -
Library -
A collection of generic theories - -
Matrix -
two-dimensional matrices - -
MicroJava -
formalization of a fragment of Java, together with a corresponding -virtual machine and a specification of its bytecode verifier and a -lightweight bytecode verifier, including proofs of type-safety - -
Modelcheck -
basic setup for integration of some model checkers in Isabelle/HOL - -
NanoJava -
Haore Logic for a tiny fragment of Java - -
NumberTheory -
fundamental Theorem of Arithmetic, Chinese Remainder Theorem, -Fermat/Euler Theorem, Wilson's Theorem, Quadratic Reciprocity - -
Prolog -
a (bare-bones) implementation of Lambda-Prolog - -
Real -
the real numbers, part of Complex - -
Hahn_Banach -
the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar) - -
SET_Protocol -
verification of the SET Protocol - -
Subst -
a theory of substitution and unification. - -
TLA -
Lamport's Temporal Logic of Actions (with separate example sessions) - -
UNITY -
Chandy and Misra's UNITY formalism - -
W0 -
a precursor of MiniML, without let-expressions - -
ex -
miscellaneous examples - -
- - - diff -r b05cd411d3d3 -r 2ff3a5589b05 src/HOL/ROOT --- a/src/HOL/ROOT Tue Mar 12 20:03:04 2013 +0100 +++ b/src/HOL/ROOT Tue Mar 12 21:59:48 2013 +0100 @@ -50,12 +50,40 @@ Author: Gertrud Bauer, TU Munich The Hahn-Banach theorem for real vector spaces. + + This is the proof of the Hahn-Banach theorem for real vectorspaces, + following H. Heuser, Funktionalanalysis, p. 228 -232. The Hahn-Banach + theorem is one of the fundamental theorems of functioal analysis. It is a + conclusion of Zorn's lemma. + + Two different formaulations of the theorem are presented, one for general + real vectorspaces and its application to normed vectorspaces. + + The theorem says, that every continous linearform, defined on arbitrary + subspaces (not only one-dimensional subspaces), can be extended to a + continous linearform on the whole vectorspace. *} options [document_graph] theories Hahn_Banach files "document/root.bib" "document/root.tex" session "HOL-Induct" in Induct = HOL + + description {* + Examples of (Co)Inductive Definitions. + + Comb proves the Church-Rosser theorem for combinators (see + http://www.cl.cam.ac.uk/ftp/papers/reports/TR396-lcp-generic-automatic-proof-tools.ps.gz). + + Mutil is the famous Mutilated Chess Board problem (see + http://www.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.dvi.gz). + + PropLog proves the completeness of a formalization of propositional logic + (see + HREF="http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz). + + Exp demonstrates the use of iterated inductive definitions to reason about + mutually recursive relations. + *} theories [quick_and_dirty] Common_Patterns theories @@ -117,6 +145,12 @@ description {* Author: David von Oheimb Copyright 1999 TUM + + IMPP -- An imperative language with procedures. + + This is an extension of IMP with local variables and mutually recursive + procedures. For documentation see "Hoare Logic for Mutual Recursion and + Local Variables" (http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html). *} options [document = false] theories EvenOdd @@ -131,6 +165,10 @@ theories Number_Theory session "HOL-Old_Number_Theory" in Old_Number_Theory = HOL + + description {* + Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler + Theorem, Wilson's Theorem, Quadratic Reciprocity. + *} options [document_graph] theories [document = false] "~~/src/HOL/Library/Infinite_Set" @@ -147,10 +185,19 @@ files "document/root.tex" session "HOL-Hoare" in Hoare = HOL + + description {* + Verification of imperative programs (verification conditions are generated + automatically from pre/post conditions and loop invariants). + *} + theories Hoare files "document/root.bib" "document/root.tex" session "HOL-Hoare_Parallel" in Hoare_Parallel = HOL + + description {* + Verification of shared-variable imperative programs a la Owicki-Gries. + (verification conditions are generated automatically). + *} options [document_graph] theories Hoare_Parallel files "document/root.bib" "document/root.tex" @@ -217,6 +264,7 @@ files "document/root.bib" "document/root.tex" session "HOL-Auth" in Auth = HOL + + description {* A new approach to verifying authentication protocols. *} options [document_graph] theories Auth_Shared @@ -231,7 +279,7 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge - Verifying security protocols using UNITY. + Verifying security protocols using Chandy and Misra's UNITY formalism. *} options [document_graph] theories @@ -315,6 +363,15 @@ files "document/root.bib" "document/root.tex" session "HOL-Proofs-Lambda" in "Proofs/Lambda" = "HOL-Proofs" + + description {* + Lambda Calculus in de Bruijn's Notation. + + This session defines lambda-calculus terms with de Bruijn indixes and + proves confluence of beta, eta and beta+eta. + + The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole + theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html). + *} options [document_graph, print_mode = "no_brackets", proofs = 2, parallel_proofs = 0] theories [document = false] "~~/src/HOL/Library/Code_Target_Int" @@ -328,11 +385,22 @@ session "HOL-Prolog" in Prolog = HOL + description {* Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) + + A bare-bones implementation of Lambda-Prolog. + + This is a simple exploratory implementation of Lambda-Prolog in HOL, + including some minimal examples (in Test.thy) and a more typical example of + a little functional language and its type system. *} options [document = false] theories Test Type session "HOL-MicroJava" in MicroJava = HOL + + description {* + Formalization of a fragment of Java, together with a corresponding virtual + machine and a specification of its bytecode verifier and a lightweight + bytecode verifier, including proofs of type-safety. + *} options [document_graph] theories [document = false] "~~/src/HOL/Library/While_Combinator" theories MicroJava @@ -346,6 +414,9 @@ theories MicroJava session "HOL-NanoJava" in NanoJava = HOL + + description {* + Hoare Logic for a tiny fragment of Java. + *} options [document_graph] theories Example files "document/root.bib" "document/root.tex" @@ -361,10 +432,12 @@ session "HOL-IOA" in IOA = HOL + description {* - Author: Tobias Nipkow & Konrad Slind - Copyright 1994 TU Muenchen + Author: Tobias Nipkow and Konrad Slind and Olaf Müller + Copyright 1994--1996 TU Muenchen - The meta theory of I/O-Automata. + The meta theory of I/O-Automata in HOL. This formalization has been + significantly changed and extended, see HOLCF/IOA. There are also the + proofs of two communication protocols which formerly have been here. @inproceedings{Nipkow-Slind-IOA, author={Tobias Nipkow and Konrad Slind}, @@ -485,7 +558,9 @@ files "document/root.bib" "document/root.tex" session "HOL-Isar_Examples" in Isar_Examples = HOL + - description {* Miscellaneous Isabelle/Isar examples for Higher-Order Logic. *} + description {* + Miscellaneous Isabelle/Isar examples for Higher-Order Logic. + *} theories [document = false] "~~/src/HOL/Library/Lattice_Syntax" "../Number_Theory/Primes" @@ -511,18 +586,26 @@ "document/style.tex" session "HOL-SET_Protocol" in SET_Protocol = HOL + + description {* + Verification of the SET Protocol. + *} options [document_graph] theories [document = false] "~~/src/HOL/Library/Nat_Bijection" theories SET_Protocol files "document/root.tex" session "HOL-Matrix_LP" in Matrix_LP = HOL + + description {* + Two-dimensional matrices and linear programming. + *} options [document_graph] theories Cplex files "document/root.tex" session "HOL-TLA" in TLA = HOL + - description {* The Temporal Logic of Actions *} + description {* + Lamport's Temporal Logic of Actions. + *} options [document = false] theories TLA @@ -637,6 +720,7 @@ files "document/root.tex" session "HOL-NSA" in NSA = HOL + + description {* Nonstandard analysis. *} options [document_graph] theories Hypercomplex files "document/root.tex" @@ -864,6 +948,11 @@ theories HOLCF_Library session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF + + description {* + IMP -- A WHILE-language and its Semantics. + + This is the HOLCF-based denotational semantics of a simple WHILE-language. + *} options [document = false] theories HoareEx files "document/root.tex" @@ -885,6 +974,20 @@ Pattern_Match session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF + + description {* + FOCUS: a theory of stream-processing functions Isabelle/HOLCF. + + For introductions to FOCUS, see + + "The Design of Distributed Systems - An Introduction to FOCUS" + http://www4.in.tum.de/publ/html.php?e=2 + + "Specification and Refinement of a Buffer of Length One" + http://www4.in.tum.de/publ/html.php?e=15 + + "Specification and Development of Interactive Systems: Focus on Streams, + Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321 + *} options [document = false] theories Fstreams @@ -894,8 +997,13 @@ session IOA in "HOLCF/IOA" = HOLCF + description {* Author: Olaf Mueller + Copyright 1997 TU München - Formalization of a semantic model of I/O-Automata. + A formalization of I/O automata in HOLCF. + + The distribution contains simulation relations, temporal logic, and an + abstraction theory. Everything is based upon a domain-theoretic model of + finite and infinite sequences. *} options [document = false] theories "meta_theory/Abstraction" diff -r b05cd411d3d3 -r 2ff3a5589b05 src/LCF/README.html --- a/src/LCF/README.html Tue Mar 12 20:03:04 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,25 +0,0 @@ - - - - - - - LCF/README - - - - -

LCF: Logic for Computable Functions

- -This directory contains the ML sources of the Isabelle system for -LCF, based on FOL.

- -The ex subdirectory contains some examples.

- -Useful references on LCF: - -

- diff -r b05cd411d3d3 -r 2ff3a5589b05 src/LCF/ROOT --- a/src/LCF/ROOT Tue Mar 12 20:03:04 2013 +0100 +++ b/src/LCF/ROOT Tue Mar 12 21:59:48 2013 +0100 @@ -4,6 +4,11 @@ description {* 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) *} options [document = false] theories LCF diff -r b05cd411d3d3 -r 2ff3a5589b05 src/Sequents/README.html --- a/src/Sequents/README.html Tue Mar 12 20:03:04 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,53 +0,0 @@ - - - - - - - Sequents/README - - - - -

Sequents: Various Sequent Calculi

- -This directory contains the ML sources of the Isabelle system for -various Sequent, Linear, and Modal Logic.

- -The subdirectories ex, ex/LK, ex/ILL, -ex/Modal contain some examples.

- -Much of the work in Modal logic was done by Martin Coen. Thanks to -Rajeev Gore' for supplying the inference system for S43. Sara Kalvala -reorganized the files and supplied Linear Logic. Jacob Frost provided -some improvements to the syntax of sequents. - -

Useful references on sequent calculi: - -

- -Useful references on Modal Logics: - - -Useful references on Linear Logic: - - - diff -r b05cd411d3d3 -r 2ff3a5589b05 src/Sequents/ROOT --- a/src/Sequents/ROOT Tue Mar 12 20:03:04 2013 +0100 +++ b/src/Sequents/ROOT Tue Mar 12 21:59:48 2013 +0100 @@ -5,7 +5,37 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge - Classical Sequent Calculus based on Pure Isabelle. + Various Sequent Calculi for Classical, Linear, and Modal Logic. + + Much of the work in Modal logic was done by Martin Coen. Thanks to Rajeev + Gore' for supplying the inference system for S43. Sara Kalvala reorganized + the files and supplied Linear Logic. Jacob Frost provided some improvements + to the syntax of sequents. + + + Useful references on sequent calculi: + + Steve Reeves and Michael Clarke, Logic for Computer Science + (Addison-Wesley, 1990) + + G. Takeuti, Proof Theory (North Holland, 1987) + + + Useful references on Modal Logics: + + Melvin C Fitting, Proof Methods for Modal and Intuitionistic Logics + (Reidel, 1983) + + Lincoln A. Wallen, Automated Deduction in Nonclassical Logics (MIT Press, + 1990) + + + Useful references on Linear Logic: + + A. S. Troelstra, Lectures on Linear Logic (CSLI, 1992) + + S. Kalvala and V. de Paiva, Linear Logic in Isabelle (in TR 379, University + of Cambridge Computer Lab, 1995, ed L. Paulson) *} options [document = false] theories diff -r b05cd411d3d3 -r 2ff3a5589b05 src/ZF/AC/README.html --- a/src/ZF/AC/README.html Tue Mar 12 20:03:04 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,32 +0,0 @@ - - - - - - - ZF/AC/README - - - - -

AC -- Equivalents of the Axiom of Choice

- -Krzysztof Grabczewski has mechanized the first two chapters of the book - -

-

-@book{rubin&rubin,
-  author	= "Herman Rubin and Jean E. Rubin",
-  title		= "Equivalents of the Axiom of Choice, {II}",
-  publisher	= "North-Holland",
-  year		= 1985}
-
- -

-The report -Mechanizing Set Theory, -by Paulson and Grabczewski, describes both this development and ZF's theories -of cardinals. - - - diff -r b05cd411d3d3 -r 2ff3a5589b05 src/ZF/Coind/README.html --- a/src/ZF/Coind/README.html Tue Mar 12 20:03:04 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,39 +0,0 @@ - - - - - - - ZF/Coind/README - - - - -

Coind -- A Coinduction Example

- -Jacob Frost has mechanized the proofs from the article - -

-

-@Article{milner-coind,
-  author	= "Robin Milner and Mads Tofte",
-  title		= "Co-induction in Relational Semantics",
-  journal	= TCS,
-  year		= 1991,
-  volume	= 87,
-  pages		= "209--220"}
-
- -

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

-Frost's -report describes this development. - - - diff -r b05cd411d3d3 -r 2ff3a5589b05 src/ZF/Constructible/README.html --- a/src/ZF/Constructible/README.html Tue Mar 12 20:03:04 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,39 +0,0 @@ - - - - - - - ZF/Constructible/README - - - -

Constructible--Relative Consistency of the Axiom of Choice

- -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. 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 -available. - -
- -

- -Last modified $Date$ - -

-Larry Paulson, -lcp@cl.cam.ac.uk -
- - diff -r b05cd411d3d3 -r 2ff3a5589b05 src/ZF/IMP/README.html --- a/src/ZF/IMP/README.html Tue Mar 12 20:03:04 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,32 +0,0 @@ - - - - - - - ZF/IMP/README - - - - -

IMP -- A while-language and two semantics

- -The formalization of the denotational and operational semantics of a simple -while-language together with an equivalence proof between the two semantics. -The whole development essentially formalizes/transcribes chapters 2 and 5 of -

-

-@book{Winskel,
- author = {Glynn Winskel},
- title = {The Formal Semantics of Programming Languages},
- publisher = {MIT Press},
- year = 1993}.
-
-

-There is a -report -by Lötzbeyer and Sandner. -

-A much extended version of this development is found in -HOL/IMP. - diff -r b05cd411d3d3 -r 2ff3a5589b05 src/ZF/README.html --- a/src/ZF/README.html Tue Mar 12 20:03:04 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,84 +0,0 @@ - - - - - - - ZF/README - - - - -

ZF: Zermelo-Fraenkel Set Theory

- -This directory contains the ML sources of the Isabelle system for -ZF Set Theory, based on FOL.

- -There are several subdirectories of examples: -

-
AC -
subdirectory containing proofs from the book "Equivalents of the Axiom -of Choice, II" by H. Rubin and J.E. Rubin, 1985. Thanks to Krzysztof -Gr`abczewski.

- -

Coind -
subdirectory containing a large example of proof by co-induction. It -is by Jacob Frost following a paper by Robin Milner and Mads Tofte.

- -

IMP -
subdirectory containing a semantics equivalence proof between -operational and denotational definitions of a simple programming language. -Thanks to Heiko Loetzbeyer & Robert Sandner.

- -

Resid -
subdirectory containing a proof of the Church-Rosser Theorem. It is -by Ole Rasmussen, following the Coq proof by G�ard Huet.

- -

ex -
subdirectory containing various examples. -
- -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: - -

- -Useful references on ZF set theory: - - - - diff -r b05cd411d3d3 -r 2ff3a5589b05 src/ZF/ROOT --- a/src/ZF/ROOT Tue Mar 12 20:03:04 2013 +0100 +++ b/src/ZF/ROOT Tue Mar 12 21:59:48 2013 +0100 @@ -5,9 +5,42 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1995 University of Cambridge - Zermelo-Fraenkel Set Theory on top of classical First-Order Logic. + 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. - This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson. + 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) *} options [document_graph] theories @@ -21,6 +54,14 @@ 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. *} options [document_graph] theories @@ -43,6 +84,12 @@ 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, @@ -51,12 +98,31 @@ 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" in Constructible = ZF + - description {* Inner Models, Absoluteness and Consistency Proofs. *} + 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 + *} options [document_graph] theories DPow_absolute AC_in_L Rank_Separation files "document/root.tex" "document/root.bib" @@ -122,6 +188,10 @@ 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 @@ -150,6 +220,15 @@ 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 diff -r b05cd411d3d3 -r 2ff3a5589b05 src/ZF/Resid/README.html --- a/src/ZF/Resid/README.html Tue Mar 12 20:03:04 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,34 +0,0 @@ - - - - - - - ZF/Resid/README - - - - -

Resid -- A theory of residuals

- -Ole Rasmussen has ported to Isabelle/ZF the Coq proofs described in the -article - -

- -

-@Article{huet-residual,
-  author  = "{G\'erard} Huet",
-  title   = "Residual Theory in $\lambda$-Calculus: A Formal Development",
-  journal = JFP,
-  year    = 1994,
-  volume  = 4,
-  number  = 3,
-  pages   = "371--394"}
-
- -See Rasmussen's report The Church-Rosser Theorem in Isabelle: A Proof Porting Experiment. - - - diff -r b05cd411d3d3 -r 2ff3a5589b05 src/ZF/ex/README.html --- a/src/ZF/ex/README.html Tue Mar 12 20:03:04 2013 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,21 +0,0 @@ - - - - - - - ZF/ex/README - - - - -

ZF general examples

- -Examples on this directory include a simple form of Ramsey's theorem. A report is available. - -

- -Several (co)inductive and (co)datatype definitions are presented. One report describes the theoretical foundations of datatypes while another describes the package that automates their declaration. - - -