# 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:
-
-
-- 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)
-
-
-
-
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
-
-
-- H. Barendregt
- Introduction to Generalised Type Systems
- J. Functional Programming
-
-
-
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:
-
-
-- 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)
-
-
-
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.
-
-
-
-- Comb proves the Church-Rosser theorem for combinators (paper
-available).
-
-
- Mutil is the famous Mutilated Chess Board problem (paper
-available).
-
-
- PropLog proves the completeness of a formalization of
-propositional logic (paper
-available).
-
-
- Exp demonstrates the use of iterated inductive definitions to
-reason about mutually recursive relations.
-
-
-
-
-
-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:
-
-
-- Lawrence C. Paulson,
- Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)
-
-
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:
-
-
-- 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)
-
-
-
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:
-
-
-- 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)
-
-
-
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.
-
-
-