# HG changeset patch # User wenzelm # Date 1363123441 -3600 # Node ID 2aea76fe9c7335e4b712274d87216c76c1c4ae4d # Parent f4c82c165f589fa309c17b105837150ed15dc9e0# Parent 90a598019aeb6ad397f4b0f69559d97b1666ca19 merged diff -r f4c82c165f58 -r 2aea76fe9c73 NEWS --- a/NEWS Tue Mar 12 19:55:17 2013 +0100 +++ b/NEWS Tue Mar 12 22:24:01 2013 +0100 @@ -61,6 +61,14 @@ isar_shrink ~> isar_compress +*** System *** + +* Discontinued "isabelle usedir" option -P (remote path) and -r (reset +session path). Note that usedir is legacy and superseded by "isabelle +build" since Isabelle2013. + + + New in Isabelle2013 (February 2013) ----------------------------------- diff -r f4c82c165f58 -r 2aea76fe9c73 src/CCL/ROOT --- a/src/CCL/ROOT Tue Mar 12 19:55:17 2013 +0100 +++ b/src/CCL/ROOT Tue Mar 12 22:24:01 2013 +0100 @@ -1,3 +1,5 @@ +chapter CCL + session CCL = Pure + description {* Author: Martin Coen, Cambridge University Computer Laboratory diff -r f4c82c165f58 -r 2aea76fe9c73 src/CTT/README.html --- a/src/CTT/README.html Tue Mar 12 19:55:17 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 f4c82c165f58 -r 2aea76fe9c73 src/CTT/ROOT --- a/src/CTT/ROOT Tue Mar 12 19:55:17 2013 +0100 +++ b/src/CTT/ROOT Tue Mar 12 22:24:01 2013 +0100 @@ -1,7 +1,20 @@ +chapter CTT + session CTT = Pure + 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 f4c82c165f58 -r 2aea76fe9c73 src/Cube/README.html --- a/src/Cube/README.html Tue Mar 12 19:55:17 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 f4c82c165f58 -r 2aea76fe9c73 src/Cube/ROOT --- a/src/Cube/ROOT Tue Mar 12 19:55:17 2013 +0100 +++ b/src/Cube/ROOT Tue Mar 12 22:24:01 2013 +0100 @@ -1,9 +1,17 @@ +chapter Cube + session Cube = Pure + description {* 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 f4c82c165f58 -r 2aea76fe9c73 src/Doc/ROOT --- a/src/Doc/ROOT Tue Mar 12 19:55:17 2013 +0100 +++ b/src/Doc/ROOT Tue Mar 12 22:24:01 2013 +0100 @@ -1,3 +1,5 @@ +chapter Doc + session Classes (doc) in "Classes" = HOL + options [document_variants = "classes"] theories [document = false] Setup diff -r f4c82c165f58 -r 2aea76fe9c73 src/FOL/README.html --- a/src/FOL/README.html Tue Mar 12 19:55:17 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 f4c82c165f58 -r 2aea76fe9c73 src/FOL/ROOT --- a/src/FOL/ROOT Tue Mar 12 19:55:17 2013 +0100 +++ b/src/FOL/ROOT Tue Mar 12 22:24:01 2013 +0100 @@ -1,10 +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 f4c82c165f58 -r 2aea76fe9c73 src/FOLP/ROOT --- a/src/FOLP/ROOT Tue Mar 12 19:55:17 2013 +0100 +++ b/src/FOLP/ROOT Tue Mar 12 22:24:01 2013 +0100 @@ -1,3 +1,5 @@ +chapter FOLP + session FOLP = Pure + description {* Author: Martin Coen, Cambridge University Computer Laboratory diff -r f4c82c165f58 -r 2aea76fe9c73 src/HOL/Algebra/README.html --- a/src/HOL/Algebra/README.html Tue Mar 12 19:55:17 2013 +0100 +++ b/src/HOL/Algebra/README.html Tue Mar 12 22:24:01 2013 +0100 @@ -110,9 +110,6 @@

[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving, Author's PhD thesis, 1999. -


-

Last modified on $Date$ -

Clemens Ballarin.

diff -r f4c82c165f58 -r 2aea76fe9c73 src/HOL/Auth/Guard/README.html --- a/src/HOL/Auth/Guard/README.html Tue Mar 12 19:55:17 2013 +0100 +++ b/src/HOL/Auth/Guard/README.html Tue Mar 12 22:24:01 2013 +0100 @@ -1,7 +1,5 @@ - - diff -r f4c82c165f58 -r 2aea76fe9c73 src/HOL/Auth/README.html --- a/src/HOL/Auth/README.html Tue Mar 12 19:55:17 2013 +0100 +++ b/src/HOL/Auth/README.html Tue Mar 12 22:24:01 2013 +0100 @@ -1,7 +1,5 @@ - - @@ -46,9 +44,6 @@

Frederic Blanqui has contributed a theory of guardedness, which is demonstrated by proofs of some roving agent protocols. -


-

Last modified $Date$ -

Larry Paulson, diff -r f4c82c165f58 -r 2aea76fe9c73 src/HOL/HOLCF/FOCUS/README.html --- a/src/HOL/HOLCF/FOCUS/README.html Tue Mar 12 19:55:17 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 f4c82c165f58 -r 2aea76fe9c73 src/HOL/HOLCF/IMP/README.html --- a/src/HOL/HOLCF/IMP/README.html Tue Mar 12 19:55:17 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 f4c82c165f58 -r 2aea76fe9c73 src/HOL/HOLCF/IOA/README.html --- a/src/HOL/HOLCF/IOA/README.html Tue Mar 12 19:55:17 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 f4c82c165f58 -r 2aea76fe9c73 src/HOL/Hahn_Banach/README.html --- a/src/HOL/Hahn_Banach/README.html Tue Mar 12 19:55:17 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 f4c82c165f58 -r 2aea76fe9c73 src/HOL/IMPP/README.html --- a/src/HOL/IMPP/README.html Tue Mar 12 19:55:17 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 f4c82c165f58 -r 2aea76fe9c73 src/HOL/IOA/README.html --- a/src/HOL/IOA/README.html Tue Mar 12 19:55:17 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 f4c82c165f58 -r 2aea76fe9c73 src/HOL/Induct/README.html --- a/src/HOL/Induct/README.html Tue Mar 12 19:55:17 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 f4c82c165f58 -r 2aea76fe9c73 src/HOL/Isar_Examples/README.html --- a/src/HOL/Isar_Examples/README.html Tue Mar 12 19:55:17 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 f4c82c165f58 -r 2aea76fe9c73 src/HOL/Prolog/README.html --- a/src/HOL/Prolog/README.html Tue Mar 12 19:55:17 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 f4c82c165f58 -r 2aea76fe9c73 src/HOL/Proofs/Lambda/README.html --- a/src/HOL/Proofs/Lambda/README.html Tue Mar 12 19:55:17 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 f4c82c165f58 -r 2aea76fe9c73 src/HOL/README.html --- a/src/HOL/README.html Tue Mar 12 19:55:17 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 f4c82c165f58 -r 2aea76fe9c73 src/HOL/ROOT --- a/src/HOL/ROOT Tue Mar 12 19:55:17 2013 +0100 +++ b/src/HOL/ROOT Tue Mar 12 22:24:01 2013 +0100 @@ -1,3 +1,5 @@ +chapter HOL + session HOL (main) = Pure + description {* Classical Higher-order Logic *} options [document_graph] @@ -48,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 @@ -115,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 @@ -129,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" @@ -145,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" @@ -215,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 @@ -229,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 @@ -313,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" @@ -326,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 @@ -344,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" @@ -359,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}, @@ -483,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" @@ -509,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 @@ -635,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" @@ -862,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" @@ -883,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 @@ -892,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 f4c82c165f58 -r 2aea76fe9c73 src/HOL/TLA/README.html --- a/src/HOL/TLA/README.html Tue Mar 12 19:55:17 2013 +0100 +++ b/src/HOL/TLA/README.html Tue Mar 12 22:24:01 2013 +0100 @@ -1,7 +1,5 @@ - - diff -r f4c82c165f58 -r 2aea76fe9c73 src/HOL/UNITY/Comp/README.html --- a/src/HOL/UNITY/Comp/README.html Tue Mar 12 19:55:17 2013 +0100 +++ b/src/HOL/UNITY/Comp/README.html Tue Mar 12 22:24:01 2013 +0100 @@ -1,7 +1,5 @@ - - @@ -40,9 +38,6 @@ level of automation appears to be about the same as in HOL-UNITY by Flemming Andersen et al. -
-

Last modified on $Date$ -

lcp@cl.cam.ac.uk
diff -r f4c82c165f58 -r 2aea76fe9c73 src/HOL/UNITY/README.html --- a/src/HOL/UNITY/README.html Tue Mar 12 19:55:17 2013 +0100 +++ b/src/HOL/UNITY/README.html Tue Mar 12 22:24:01 2013 +0100 @@ -1,7 +1,5 @@ - - @@ -45,9 +43,6 @@ The directory Comp presents examples of proofs involving program composition. -
-

Last modified on $Date$ -

lcp@cl.cam.ac.uk
diff -r f4c82c165f58 -r 2aea76fe9c73 src/HOL/UNITY/Simple/README.html --- a/src/HOL/UNITY/Simple/README.html Tue Mar 12 19:55:17 2013 +0100 +++ b/src/HOL/UNITY/Simple/README.html Tue Mar 12 22:24:01 2013 +0100 @@ -1,7 +1,5 @@ - - @@ -37,9 +35,6 @@ Reachability.thy) -
-

Last modified on $Date$ -

lcp@cl.cam.ac.uk
diff -r f4c82c165f58 -r 2aea76fe9c73 src/LCF/README.html --- a/src/LCF/README.html Tue Mar 12 19:55:17 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 f4c82c165f58 -r 2aea76fe9c73 src/LCF/ROOT --- a/src/LCF/ROOT Tue Mar 12 19:55:17 2013 +0100 +++ b/src/LCF/ROOT Tue Mar 12 22:24:01 2013 +0100 @@ -1,7 +1,14 @@ +chapter LCF + session LCF = Pure + 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 f4c82c165f58 -r 2aea76fe9c73 src/Pure/ROOT --- a/src/Pure/ROOT Tue Mar 12 19:55:17 2013 +0100 +++ b/src/Pure/ROOT Tue Mar 12 22:24:01 2013 +0100 @@ -1,3 +1,5 @@ +chapter Pure + session RAW = theories files diff -r f4c82c165f58 -r 2aea76fe9c73 src/Pure/System/session.ML --- a/src/Pure/System/session.ML Tue Mar 12 19:55:17 2013 +0100 +++ b/src/Pure/System/session.ML Tue Mar 12 22:24:01 2013 +0100 @@ -1,18 +1,16 @@ (* Title: Pure/System/session.ML Author: Markus Wenzel, TU Muenchen -Session management -- maintain state of logic images. +Session management -- internal state of logic images. *) signature SESSION = sig - val id: unit -> string list val name: unit -> string - val path: unit -> string list val welcome: unit -> string + val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list -> + string -> string * string -> bool * string -> bool -> unit val finish: unit -> unit - val init: bool -> bool -> bool -> string -> string -> bool -> string -> (string * string) list -> - string -> string -> bool * string -> string -> bool -> unit val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b val use_dir: string -> string -> bool -> string list -> bool -> bool -> string -> string -> bool -> string list -> string -> string -> bool * string -> @@ -24,22 +22,10 @@ (* session state *) -val session = Unsynchronized.ref ([Context.PureN]: string list); +val session = Unsynchronized.ref {chapter = "Pure", name = "Pure"}; val session_finished = Unsynchronized.ref false; -fun id () = ! session; -fun name () = "Isabelle/" ^ List.last (! session); - - -(* access path *) - -val session_path = Unsynchronized.ref ([]: string list); -val remote_path = Unsynchronized.ref (NONE: Url.T option); - -fun path () = ! session_path; - - -(* welcome *) +fun name () = "Isabelle/" ^ #name (! session); fun welcome () = if Distribution.is_official then @@ -47,22 +33,21 @@ else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")"; -(* add_path *) +(* init *) -fun add_path reset s = - let val sess = ! session @ [s] in - (case duplicates (op =) sess of - [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s])) - | dups => error ("Duplicate session identifiers " ^ commas_quote dups)) - end; - - -(* init_name *) - -fun init_name reset parent name = - if not (member (op =) (! session) parent) orelse not (! session_finished) then +fun init build info info_path doc doc_graph doc_output doc_variants + parent (chapter, name) doc_dump verbose = + if #name (! session) <> parent orelse not (! session_finished) then error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name) - else (add_path reset name; session_finished := false); + else + let + val _ = session := {chapter = chapter, name = name}; + val _ = session_finished := false; + in + Present.init build info info_path (if doc = "false" then "" else doc) + doc_graph doc_output doc_variants (chapter, name) + doc_dump verbose (map Thy_Info.get_theory (Thy_Info.get_names ())) + end; (* finish *) @@ -78,7 +63,7 @@ session_finished := true); -(* use_dir *) +(* timing within ML *) fun with_timing name verbose f x = let @@ -100,29 +85,13 @@ else (); in y end; -fun get_rpath rpath = - (if rpath = "" then () else - if is_some (! remote_path) then - error "Path for remote theory browsing information may only be set once" - else - remote_path := SOME (Url.explode rpath); - (! remote_path, rpath <> "")); -fun init build reset info info_path doc doc_graph doc_output doc_variants - parent name doc_dump rpath verbose = - (init_name reset parent name; - Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_output - doc_variants (path ()) name doc_dump (get_rpath rpath) verbose - (map Thy_Info.get_theory (Thy_Info.get_names ()))); - -local +(* use_dir *) fun read_variants strs = rev (distinct (eq_fst (op =)) (rev (("document", "") :: map Present.read_variant strs))) |> filter_out (fn (_, s) => s = "-"); -in - fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent name doc_dump rpath level timing verbose max_threads trace_threads parallel_proofs parallel_proofs_threshold = @@ -132,8 +101,15 @@ Output.physical_stderr "### Legacy feature: old \"isabelle usedir\" -- use \"isabelle build\" instead!\n"; val _ = - init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name - doc_dump rpath verbose; + if not reset then () + else Output.physical_stderr "### Ignoring reset (historic usedir option -r)\n"; + val _ = + if rpath = "" then () + else Output.physical_stderr "### Ignoring remote path (historic usedir option -P)\n"; + + val _ = + init build info (Path.explode info_path) doc doc_graph "" (read_variants doc_variants) + parent ("Unsorted", name) doc_dump verbose; val res1 = (use |> with_timing item timing |> Exn.capture) root; val res2 = Exn.capture finish (); in ignore (Par_Exn.release_all [res1, res2]) end) @@ -148,5 +124,3 @@ handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1); end; - -end; diff -r f4c82c165f58 -r 2aea76fe9c73 src/Pure/Thy/html.ML --- a/src/Pure/Thy/html.ML Tue Mar 12 19:55:17 2013 +0100 +++ b/src/Pure/Thy/html.ML Tue Mar 12 22:24:01 2013 +0100 @@ -22,12 +22,11 @@ val verbatim: string -> text val begin_document: string -> text val end_document: text - val begin_index: Url.T * string -> Url.T * string -> (Url.T * string) list -> Url.T -> text + val begin_session_index: string -> (Url.T * string) list -> Url.T -> text val applet_pages: string -> Url.T * string -> (string * string) list val theory_entry: Url.T * string -> text - val session_entries: (Url.T * string) list -> text val theory_source: text -> text - val begin_theory: Url.T * string -> string -> (Url.T option * string) list -> + val begin_theory: string -> (Url.T option * string) list -> (Url.T * Url.T * bool) list -> text -> text val external_file: Url.T -> string -> text end; @@ -288,15 +287,11 @@ val end_document = "\n\n\n\n"; -fun gen_link how (path, name) = para (href_path path how ^ " to index of " ^ plain name); -val up_link = gen_link "Up"; -val back_link = gen_link "Back"; - (* session index *) -fun begin_index up (index_path, session) docs graph = - begin_document ("Index of " ^ session) ^ up_link up ^ +fun begin_session_index session docs graph = + begin_document ("Session " ^ plain session) ^ para ("View " ^ href_path graph "theory dependencies" ^ implode (map (fn (p, name) => "
\nView " ^ href_path p name) docs)) ^ "\n\n
\n

Theories

\n" - | session_entries es = - "\n
\n
\n\ - \

Sessions

\n"; +fun theory_entry (p, s) = "
  • " ^ href_path p (plain s) ^ "
  • \n"; (* theory *) @@ -350,9 +340,8 @@ fun file (href, path, loadit) = href_path href (if loadit then file_path path else enclose "(" ")" (file_path path)); - fun theory up A = - begin_document ("Theory " ^ A) ^ "\n" ^ up_link up ^ - command "theory" ^ " " ^ name A; + fun theory A = + begin_document ("Theory " ^ A) ^ "\n" ^ command "theory" ^ " " ^ name A; fun imports Bs = keyword "imports" ^ " " ^ space_implode " " (map (uncurry href_opt_path o apsnd name) Bs); @@ -360,8 +349,8 @@ fun uses Ps = keyword "uses" ^ " " ^ space_implode " " (map file Ps) ^ "
    \n"; in -fun begin_theory up A Bs Ps body = - theory up A ^ "
    \n" ^ +fun begin_theory A Bs Ps body = + theory A ^ "
    \n" ^ imports Bs ^ "
    \n" ^ (if null Ps then "" else uses Ps) ^ body; diff -r f4c82c165f58 -r 2aea76fe9c73 src/Pure/Thy/html.scala --- a/src/Pure/Thy/html.scala Tue Mar 12 19:55:17 2013 +0100 +++ b/src/Pure/Thy/html.scala Tue Mar 12 22:24:01 2013 +0100 @@ -11,7 +11,7 @@ object HTML { - // encode text + /* encode text */ def encode(text: String): String = { @@ -29,19 +29,45 @@ } - // common markup elements + /* document */ + + val end_document = "\n
    \n\n\n" - def session_entry(name: String): String = + def begin_document(title: String): String = + "\n" + + "\n" + + "\n" + + "\n" + + "\n" + + "" + encode(title) + "\n" + + "\n" + + "\n" + + "\n" + + "\n" + + "
    " + + "

    " + encode(title) + "

    \n" + + + /* common markup elements */ + + private def session_entry(entry: (String, String)): String = + { + val (name, description) = entry + val descr = + if (description == "") Nil + else List(XML.elem("br"), XML.elem("pre", List(XML.Text(description)))) XML.string_of_tree( XML.elem("li", List(XML.Elem(Markup("a", List(("href", name + "/index.html"))), - List(XML.Text(name)))))) + "\n" + List(XML.Text(name)))) ::: descr)) + "\n" + } - def session_entries(names: List[String]): String = - if (names.isEmpty) "" - else - "\n
    \n
    \n" + - "

    Sessions

    \n"; - - val end_document = "\n
    \n\n\n" + def chapter_index(chapter: String, sessions: List[(String, String)]): String = + { + begin_document("Isabelle/" + chapter + " sessions") + + (if (sessions.isEmpty) "" + else "
    ") + + end_document + } } diff -r f4c82c165f58 -r 2aea76fe9c73 src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Tue Mar 12 19:55:17 2013 +0100 +++ b/src/Pure/Thy/present.ML Tue Mar 12 22:24:01 2013 +0100 @@ -14,9 +14,8 @@ include BASIC_PRESENT val session_name: theory -> string val read_variant: string -> string * string - val init: bool -> bool -> string -> string -> bool -> string -> (string * string) list -> - string list -> string -> bool * string -> Url.T option * bool -> bool -> - theory list -> unit (*not thread-safe!*) + val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list -> + string * string -> bool * string -> bool -> theory list -> unit (*not thread-safe!*) val finish: unit -> unit (*not thread-safe!*) val init_theory: string -> unit val theory_source: string -> (unit -> HTML.text) -> unit @@ -45,15 +44,6 @@ val graph_pdf_path = Path.basic "session_graph.pdf"; val graph_eps_path = Path.basic "session_graph.eps"; -val session_path = Path.basic ".session"; -val session_entries_path = Path.explode ".session/entries"; -val pre_index_path = Path.explode ".session/pre-index"; - -fun mk_rel_path [] ys = Path.make ys - | mk_rel_path xs [] = Path.appends (replicate (length xs) Path.parent) - | mk_rel_path (ps as x :: xs) (qs as y :: ys) = if x = y then mk_rel_path xs ys else - Path.appends (replicate (length ps) Path.parent @ [Path.make qs]); - fun show_path path = Path.implode (Path.append (File.pwd ()) path); @@ -62,37 +52,48 @@ structure Browser_Info = Theory_Data ( - type T = {name: string, session: string list, is_local: bool}; - val empty = {name = "", session = [], is_local = false}: T; + type T = {chapter: string, name: string}; + val empty = {chapter = Context.PureN, name = Context.PureN}: T; fun extend _ = empty; fun merge _ = empty; ); -val put_info = Browser_Info.put; -val get_info = Browser_Info.get; -val session_name = #name o get_info; +val session_name = #name o Browser_Info.get; +val session_chapter_name = (fn {chapter, name} => [chapter, name]) o Browser_Info.get; (** graphs **) fun ID_of sess s = space_implode "/" (sess @ [s]); -fun ID_of_thy thy = ID_of (#session (get_info thy)) (Context.theory_name thy); +fun ID_of_thy thy = ID_of (session_chapter_name thy) (Context.theory_name thy); +fun theory_link (curr_chapter, curr_session) thy = + let + val {chapter, name = session} = Browser_Info.get thy; + val link = html_path (Context.theory_name thy); + in + if curr_session = session then SOME link + else if curr_chapter = chapter then + SOME (Path.appends [Path.parent, Path.basic session, link]) + else if chapter = Context.PureN then NONE + else SOME (Path.appends [Path.parent, Path.parent, Path.basic chapter, Path.basic session, link]) + end; (*retrieve graph data from initial collection of theories*) -fun init_graph remote_path curr_sess = rev o map (fn thy => +fun init_graph (curr_chapter, curr_session) = rev o map (fn thy => let - val name = Context.theory_name thy; - val {name = sess_name, session, is_local} = get_info thy; + val {chapter, name = session_name} = Browser_Info.get thy; + val thy_name = Context.theory_name thy; + val path = + (case theory_link (curr_chapter, curr_session) thy of + NONE => "" + | SOME p => Path.implode p); val entry = - {name = name, ID = ID_of session name, dir = sess_name, - path = - if null session then "" else - if is_some remote_path andalso not is_local then - Url.implode (Url.append (the remote_path) (Url.File - (Path.append (Path.make session) (html_path name)))) - else Path.implode (Path.append (mk_rel_path curr_sess session) (html_path name)), + {name = thy_name, + ID = ID_of [chapter, session_name] thy_name, + dir = session_name, + path = path, unfold = false, parents = map ID_of_thy (Theory.parents_of thy), content = []}; @@ -130,8 +131,8 @@ val empty_browser_info = make_browser_info (Symtab.empty, [], [], [], []); -fun init_browser_info remote_path curr_sess thys = make_browser_info - (Symtab.empty, [], [], [], init_graph remote_path curr_sess thys); +fun init_browser_info session thys = + make_browser_info (Symtab.empty, [], [], [], init_graph session thys); fun map_browser_info f {theories, files, tex_index, html_index, graph} = make_browser_info (f (theories, files, tex_index, html_index, graph)); @@ -189,54 +190,30 @@ (* session_info *) type session_info = - {name: string, parent: string, session: string, path: string list, html_prefix: Path.T, + {name: string, chapter: string, info_path: Path.T, info: bool, doc_format: string, doc_graph: bool, doc_output: Path.T option, - documents: (string * string) list, doc_dump: (bool * string), remote_path: Url.T option, - verbose: bool, readme: Path.T option}; + documents: (string * string) list, doc_dump: (bool * string), verbose: bool, + readme: Path.T option}; fun make_session_info - (name, parent, session, path, html_prefix, info, doc_format, doc_graph, doc_output, - documents, doc_dump, remote_path, verbose, readme) = - {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix, - info = info, doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output, - documents = documents, doc_dump = doc_dump, remote_path = remote_path, - verbose = verbose, readme = readme}: session_info; + (name, chapter, info_path, info, doc_format, doc_graph, doc_output, + documents, doc_dump, verbose, readme) = + {name = name, chapter = chapter, info_path = info_path, info = info, + doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output, + documents = documents, doc_dump = doc_dump, verbose = verbose, + readme = readme}: session_info; (* state *) val session_info = Unsynchronized.ref (NONE: session_info option); -fun session_default x f = (case ! session_info of NONE => x | SOME info => f info); +fun with_session_info x f = (case ! session_info of NONE => x | SOME info => f info); (** document preparation **) -(* maintain session index *) - -val session_entries = - HTML.session_entries o - map (fn name => (Url.File (Path.append (Path.basic name) index_path), name)); - -fun get_entries dir = - split_lines (File.read (Path.append dir session_entries_path)); - -fun put_entries entries dir = - File.write (Path.append dir session_entries_path) (cat_lines entries); - - -fun create_index dir = - File.read (Path.append dir pre_index_path) ^ - session_entries (get_entries dir) ^ HTML.end_document - |> File.write (Path.append dir index_path); - -fun update_index dir name = - (case try get_entries dir of - NONE => warning ("Browser info: cannot access session index of " ^ Path.print dir) - | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir)); - - (* document variants *) fun read_variant str = @@ -248,19 +225,14 @@ (* init session *) -fun name_of_session elems = space_implode "/" ("Isabelle" :: elems); - -fun init build info info_path doc doc_graph document_output doc_variants path name - (doc_dump as (_, dump_prefix)) (remote_path, first_time) verbose thys = +fun init build info info_path doc doc_graph document_output doc_variants + (chapter, name) (doc_dump as (_, dump_prefix)) verbose thys = if not build andalso not info andalso doc = "" andalso dump_prefix = "" then (browser_info := empty_browser_info; session_info := NONE) else let - val parent_name = name_of_session (take (length path - 1) path); - val session_name = name_of_session path; - val sess_prefix = Path.make path; - val html_prefix = Path.append (Path.expand (Path.explode info_path)) sess_prefix; - val doc_output = if document_output = "" then NONE else SOME (Path.explode document_output); + val doc_output = + if document_output = "" then NONE else SOME (Path.explode document_output); val documents = if doc = "" then [] @@ -269,11 +241,6 @@ else (); []) else doc_variants; - val parent_index_path = Path.append Path.parent index_path; - val index_up_lnk = - if first_time then - Url.append (the remote_path) (Url.File (Path.append sess_prefix parent_index_path)) - else Url.File parent_index_path; val readme = if File.exists readme_html_path then SOME readme_html_path else if File.exists readme_path then SOME readme_path @@ -282,14 +249,12 @@ val docs = (case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @ map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents; - val index_text = HTML.begin_index (index_up_lnk, parent_name) - (Url.File index_path, session_name) docs (Url.explode "medium.html"); in session_info := - SOME (make_session_info (name, parent_name, session_name, path, html_prefix, info, doc, - doc_graph, doc_output, documents, doc_dump, remote_path, verbose, readme)); - browser_info := init_browser_info remote_path path thys; - add_html_index (0, index_text) + SOME (make_session_info (name, chapter, info_path, info, doc, + doc_graph, doc_output, documents, doc_dump, verbose, readme)); + browser_info := init_browser_info (chapter, name) thys; + add_html_index (0, HTML.begin_session_index name docs (Url.explode "medium.html")) end; @@ -337,15 +302,18 @@ fun finish () = - session_default () (fn {name, info, html_prefix, doc_format, doc_graph, doc_output, - documents, doc_dump = (dump_copy, dump_prefix), path, verbose, readme, ...} => + with_session_info () (fn {name, chapter, info, info_path, doc_format, doc_graph, doc_output, + documents, doc_dump = (dump_copy, dump_prefix), verbose, readme, ...} => let val {theories, files, tex_index, html_index, graph} = ! browser_info; val thys = Symtab.dest theories; - val parent_html_prefix = Path.append html_prefix Path.parent; + + val chapter_prefix = Path.append info_path (Path.basic chapter); + val session_prefix = Path.append chapter_prefix (Path.basic name); fun finish_html (a, {html, ...}: theory_info) = - File.write_buffer (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_document html); + File.write_buffer (Path.append session_prefix (html_path a)) + (Buffer.add HTML.end_document html); val sorted_graph = sorted_index graph; val opt_graphs = @@ -355,21 +323,19 @@ val _ = if info then - (Isabelle_System.mkdirs (Path.append html_prefix session_path); - File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer html_index); - File.write (Path.append html_prefix session_entries_path) ""; - create_index html_prefix; - if length path > 1 then update_index parent_html_prefix name else (); - (case readme of NONE => () | SOME path => File.copy path html_prefix); - Graph_Display.write_graph_browser (Path.append html_prefix graph_path) sorted_graph; + (Isabelle_System.mkdirs session_prefix; + File.write_buffer (Path.append session_prefix index_path) + (index_buffer html_index |> Buffer.add HTML.end_document); + (case readme of NONE => () | SOME path => File.copy path session_prefix); + Graph_Display.write_graph_browser (Path.append session_prefix graph_path) sorted_graph; Isabelle_System.isabelle_tool "browser" "-b"; - File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix; - List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt) + File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") session_prefix; + List.app (fn (a, txt) => File.write (Path.append session_prefix (Path.basic a)) txt) (HTML.applet_pages name (Url.File index_path, name)); - File.copy (Path.explode "~~/etc/isabelle.css") html_prefix; + File.copy (Path.explode "~~/etc/isabelle.css") session_prefix; List.app finish_html thys; List.app (uncurry File.write) files; - if verbose then Output.physical_stderr ("Browser info at " ^ show_path html_prefix ^ "\n") + if verbose then Output.physical_stderr ("Browser info at " ^ show_path session_prefix ^ "\n") else ()) else (); @@ -415,7 +381,7 @@ val jobs = (if info orelse is_none doc_output then - map (document_job html_prefix true) documents + map (document_job session_prefix true) documents else []) @ (case doc_output of NONE => [] @@ -430,33 +396,23 @@ (* theory elements *) -fun init_theory name = session_default () (fn _ => init_theory_info name empty_theory_info); +fun init_theory name = with_session_info () (fn _ => init_theory_info name empty_theory_info); fun theory_source name mk_text = - session_default () (fn _ => add_html_source name (HTML.theory_source (mk_text ()))); + with_session_info () (fn _ => add_html_source name (HTML.theory_source (mk_text ()))); fun theory_output name s = - session_default () (fn _ => add_tex_source name (Latex.isabelle_file name s)); + with_session_info () (fn _ => add_tex_source name (Latex.isabelle_file name s)); -fun parent_link remote_path curr_session thy = - let - val {name = _, session, is_local} = get_info thy; - val name = Context.theory_name thy; - val link = - if null session then NONE - else SOME - (if is_some remote_path andalso not is_local then - Url.append (the remote_path) (Url.File (Path.append (Path.make session) (html_path name))) - else Url.File (Path.append (mk_rel_path curr_session session) (html_path name))); - in (link, name) end; - fun begin_theory update_time dir thy = - session_default thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} => + with_session_info thy (fn {name = session_name, chapter, info_path, ...} => let val name = Context.theory_name thy; val parents = Theory.parents_of thy; - val parent_specs = map (parent_link remote_path path) parents; + val parent_specs = parents |> map (fn parent => + (Option.map Url.File (theory_link (chapter, session_name) parent), + (Context.theory_name parent))); val files = []; (* FIXME *) val files_html = files |> map (fn (raw_path, loadit) => @@ -464,18 +420,22 @@ val path = File.check_file (File.full_path dir raw_path); val base = Path.base path; val base_html = html_ext base; - val _ = add_file (Path.append html_prefix base_html, - HTML.external_file (Url.File base) (File.read path)); + (* FIXME retain file path!? *) + val session_prefix = Path.appends [info_path, Path.basic chapter, Path.basic name]; + val _ = + add_file (Path.append session_prefix base_html, + HTML.external_file (Url.File base) (File.read path)); in (Url.File base_html, Url.File raw_path, loadit) end); fun prep_html_source (tex_source, html_source, html) = - let - val txt = HTML.begin_theory (Url.File index_path, session) - name parent_specs files_html (Buffer.content html_source) + let val txt = HTML.begin_theory name parent_specs files_html (Buffer.content html_source) in (tex_source, Buffer.empty, Buffer.add txt html) end; val entry = - {name = name, ID = ID_of path name, dir = sess_name, unfold = true, + {name = name, + ID = ID_of [chapter, session_name] name, + dir = session_name, + unfold = true, path = Path.implode (html_path name), parents = map ID_of_thy parents, content = []}; @@ -484,7 +444,7 @@ add_graph_entry (update_time, entry); add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name)); add_tex_index (update_time, Latex.theory_entry name); - put_info {name = sess_name, session = path, is_local = is_some remote_path} thy + Browser_Info.put {chapter = chapter, name = session_name} thy end); diff -r f4c82c165f58 -r 2aea76fe9c73 src/Pure/Thy/present.scala --- a/src/Pure/Thy/present.scala Tue Mar 12 19:55:17 2013 +0100 +++ b/src/Pure/Thy/present.scala Tue Mar 12 22:24:01 2013 +0100 @@ -7,35 +7,41 @@ package isabelle +import scala.collection.immutable.SortedMap + + object Present { - /* maintain session index -- NOT thread-safe */ + /* maintain chapter index -- NOT thread-safe */ private val index_path = Path.basic("index.html") - private val session_entries_path = Path.explode(".session/entries") - private val pre_index_path = Path.explode(".session/pre-index") + private val sessions_path = Path.basic(".sessions") - private def get_entries(dir: Path): List[String] = - split_lines(File.read(dir + session_entries_path)) + private def read_sessions(dir: Path): List[(String, String)] = + { + import XML.Decode._ + list(pair(string, string))(YXML.parse_body(File.read(dir + sessions_path))) + } - private def put_entries(entries: List[String], dir: Path): Unit = - File.write(dir + session_entries_path, cat_lines(entries)) + private def write_sessions(dir: Path, sessions: List[(String, String)]) + { + import XML.Encode._ + File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions))) + } - def create_index(dir: Path): Unit = - File.write(dir + index_path, - File.read(dir + pre_index_path) + - HTML.session_entries(get_entries(dir)) + - HTML.end_document) + def update_chapter_index(info_path: Path, chapter: String, new_sessions: List[(String, String)]) + { + val dir = info_path + Path.basic(chapter) + Isabelle_System.mkdirs(dir) - def update_index(dir: Path, names: List[String]): Unit = - try { - put_entries(get_entries(dir).filterNot(names.contains) ::: names, dir) - create_index(dir) - } - catch { - case ERROR(msg) => - java.lang.System.err.println( - "### " + msg + "\n### Browser info: failed to update session index of " + dir) - } + val sessions0 = + try { read_sessions(dir + sessions_path) } + catch { case ERROR(_) => Nil case _: XML.XML_Atom => Nil case _: XML.XML_Body => Nil } + + val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList + + write_sessions(dir, sessions) + File.write(dir + index_path, HTML.chapter_index(chapter, sessions)) + } } diff -r f4c82c165f58 -r 2aea76fe9c73 src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Tue Mar 12 19:55:17 2013 +0100 +++ b/src/Pure/Tools/build.ML Tue Mar 12 22:24:01 2013 +0100 @@ -109,11 +109,12 @@ fun build args_file = Command_Line.tool (fn () => let val (command_timings, (do_output, (options, (verbose, (browser_info, - (parent_name, (name, theories))))))) = + (parent_name, (chapter, (name, theories)))))))) = File.read (Path.explode args_file) |> YXML.parse_body |> let open XML.Decode in pair (list properties) (pair bool (pair Options.decode (pair bool (pair string - (pair string (pair string ((list (pair Options.decode (list string)))))))))) + (pair string (pair string (pair string + ((list (pair Options.decode (list string))))))))))) end; val document_variants = @@ -125,18 +126,15 @@ val _ = writeln ("\fSession.name = " ^ name); val _ = - (case Session.path () of - [] => () - | path => writeln ("\fSession.parent_path = " ^ space_implode "/" path)); - val _ = - Session.init do_output false - (Options.bool options "browser_info") browser_info + Session.init do_output + (Options.bool options "browser_info") + (Path.explode browser_info) (Options.string options "document") (Options.bool options "document_graph") (Options.string options "document_output") document_variants - parent_name name - (false, "") "" + parent_name (chapter, name) + (false, "") verbose; val last_timing = lookup_timings (fold update_timings command_timings empty_timings); diff -r f4c82c165f58 -r 2aea76fe9c73 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Tue Mar 12 19:55:17 2013 +0100 +++ b/src/Pure/Tools/build.scala Tue Mar 12 22:24:01 2013 +0100 @@ -14,6 +14,7 @@ import java.util.zip.GZIPInputStream import scala.collection.SortedSet +import scala.collection.mutable import scala.annotation.tailrec @@ -46,6 +47,8 @@ /** session information **/ // external version + abstract class Entry + sealed case class Chapter(name: String) extends Entry sealed case class Session_Entry( pos: Position.T, name: String, @@ -55,10 +58,11 @@ description: String, options: List[Options.Spec], theories: List[(List[Options.Spec], List[String])], - files: List[String]) + files: List[String]) extends Entry // internal version sealed case class Session_Info( + chapter: String, select: Boolean, pos: Position.T, groups: List[String], @@ -72,8 +76,8 @@ def is_pure(name: String): Boolean = name == "RAW" || name == "Pure" - def session_info(options: Options, select: Boolean, dir: Path, entry: Session_Entry) - : (String, Session_Info) = + def session_info(options: Options, select: Boolean, dir: Path, + chapter: String, entry: Session_Entry): (String, Session_Info) = try { val name = entry.name @@ -87,10 +91,11 @@ entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map(Path.explode(_))) }) val files = entry.files.map(Path.explode(_)) - val entry_digest = SHA1.digest((name, entry.parent, entry.options, entry.theories).toString) + val entry_digest = + SHA1.digest((chapter, name, entry.parent, entry.options, entry.theories).toString) val info = - Session_Info(select, entry.pos, entry.groups, dir + Path.explode(entry.path), + Session_Info(chapter, select, entry.pos, entry.groups, dir + Path.explode(entry.path), entry.parent, entry.description, session_options, theories, files, entry_digest) (name, info) @@ -180,6 +185,9 @@ /* parser */ + val chapter_default = "Unsorted" + + private val CHAPTER = "chapter" private val SESSION = "session" private val IN = "in" private val DESCRIPTION = "description" @@ -189,10 +197,20 @@ lazy val root_syntax = Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" + - (SESSION, Keyword.THY_DECL) + IN + DESCRIPTION + OPTIONS + THEORIES + FILES + (CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) + + IN + DESCRIPTION + OPTIONS + THEORIES + FILES private object Parser extends Parse.Parser { + def entry(pos: Position.T): Parser[Entry] = chapter(pos) | session_entry(pos) + + def chapter(pos: Position.T): Parser[Chapter] = + { + val chapter_name = atom("chapter name", _.is_name) + + command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter(a) } + } + def session_entry(pos: Position.T): Parser[Session_Entry] = { val session_name = atom("session name", _.is_name) @@ -219,11 +237,19 @@ Session_Entry(pos, a, b, c, d, e, f, g, h) } } - def parse_entries(root: Path): List[Session_Entry] = + def parse_entries(root: Path): List[(String, Session_Entry)] = { val toks = root_syntax.scan(File.read(root)) - parse_all(rep(session_entry(root.position)), Token.reader(toks, root.implode)) match { - case Success(result, _) => result + + parse_all(rep(entry(root.position)), Token.reader(toks, root.implode)) match { + case Success(result, _) => + var chapter = chapter_default + val entries = new mutable.ListBuffer[(String, Session_Entry)] + result.foreach { + case Chapter(name) => chapter = name + case session_entry: Session_Entry => entries += ((chapter, session_entry)) + } + entries.toList case bad => error(bad.toString) } } @@ -250,7 +276,8 @@ def find_root(select: Boolean, dir: Path): List[(String, Session_Info)] = { val root = dir + ROOT - if (root.is_file) Parser.parse_entries(root).map(session_info(options, select, dir, _)) + if (root.is_file) + Parser.parse_entries(root).map(p => session_info(options, select, dir, p._1, p._2)) else Nil } @@ -398,7 +425,7 @@ val groups = if (info.groups.isEmpty) "" else info.groups.mkString(" (", " ", ")") - progress.echo("Session " + name + groups) + progress.echo("Session " + info.chapter + "/" + name + groups) } val thy_deps = @@ -470,9 +497,10 @@ { import XML.Encode._ pair(list(properties), pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, - pair(string, pair(string, list(pair(Options.encode, list(Path.encode))))))))))( + pair(string, pair(string, pair(string, + list(pair(Options.encode, list(Path.encode)))))))))))( (command_timings, (do_output, (info.options, (verbose, (browser_info, - (parent, (name, info.theories)))))))) + (parent, (info.chapter, (name, info.theories))))))))) })) private val env = @@ -568,7 +596,6 @@ private def log_gz(name: String): Path = log(name).ext("gz") private val SESSION_NAME = "\fSession.name = " - private val SESSION_PARENT_PATH = "\fSession.parent_path = " sealed case class Log_Info( @@ -727,7 +754,7 @@ } // scheduler loop - case class Result(current: Boolean, parent_path: Option[String], heap: String, rc: Int) + case class Result(current: Boolean, heap: String, rc: Int) def sleep(): Unit = Thread.sleep(500) @@ -748,7 +775,7 @@ val res = job.join progress.echo(res.err) - val (parent_path, heap) = + val heap = if (res.rc == 0) { (output_dir + log(name)).file.delete @@ -757,13 +784,7 @@ File.write_gzip(output_dir + log_gz(name), sources + "\n" + parent_heap + "\n" + heap + "\n" + res.out) - val parent_path = - if (job.info.options.bool("browser_info")) - res.out_lines.find(_.startsWith(SESSION_PARENT_PATH)) - .map(_.substring(SESSION_PARENT_PATH.length)) - else None - - (parent_path, heap) + heap } else { (output_dir + Path.basic(name)).file.delete @@ -778,10 +799,10 @@ progress.echo("\n" + cat_lines(tail)) } - (None, no_heap) + no_heap } loop(pending - name, running - name, - results + (name -> Result(false, parent_path, heap, res.rc))) + results + (name -> Result(false, heap, res.rc))) //}}} case None if (running.size < (max_jobs max 1)) => //{{{ check/start next job @@ -789,7 +810,7 @@ case Some((name, info)) => val parent_result = info.parent match { - case None => Result(true, None, no_heap, 0) + case None => Result(true, no_heap, 0) case Some(parent) => results(parent) } val output = output_dir + Path.basic(name) @@ -812,10 +833,10 @@ val all_current = current && parent_result.current if (all_current) - loop(pending - name, running, results + (name -> Result(true, None, heap, 0))) + loop(pending - name, running, results + (name -> Result(true, heap, 0))) else if (no_build) { if (verbose) progress.echo("Skipping " + name + " ...") - loop(pending - name, running, results + (name -> Result(false, None, heap, 1))) + loop(pending - name, running, results + (name -> Result(false, heap, 1))) } else if (parent_result.rc == 0 && !progress.stopped) { progress.echo((if (do_output) "Building " else "Running ") + name + " ...") @@ -826,7 +847,7 @@ } else { progress.echo(name + " CANCELLED") - loop(pending - name, running, results + (name -> Result(false, None, heap, 1))) + loop(pending - name, running, results + (name -> Result(false, heap, 1))) } case None => sleep(); loop(pending, running, results) } @@ -847,11 +868,11 @@ else loop(queue, Map.empty, Map.empty) val session_entries = - (for ((name, res) <- results.iterator if res.parent_path.isDefined) - yield (res.parent_path.get, name)).toList.groupBy(_._1).map( - { case (p, es) => (p, es.map(_._2).sorted) }) - for ((p, names) <- session_entries) - Present.update_index(browser_info + Path.explode(p), names) + (for { (name, res) <- results.iterator; info = full_tree(name) } + yield (info.chapter, (name, info.description))).toList.groupBy(_._1).map( + { case (chapter, es) => (chapter, es.map(_._2)) }) + for ((chapter, entries) <- session_entries) + Present.update_chapter_index(browser_info, chapter, entries) val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc }) if (rc != 0 && (verbose || !no_build)) { diff -r f4c82c165f58 -r 2aea76fe9c73 src/Sequents/README.html --- a/src/Sequents/README.html Tue Mar 12 19:55:17 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 f4c82c165f58 -r 2aea76fe9c73 src/Sequents/ROOT --- a/src/Sequents/ROOT Tue Mar 12 19:55:17 2013 +0100 +++ b/src/Sequents/ROOT Tue Mar 12 22:24:01 2013 +0100 @@ -1,9 +1,41 @@ +chapter Sequents + session Sequents = Pure + description {* 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 f4c82c165f58 -r 2aea76fe9c73 src/ZF/AC/README.html --- a/src/ZF/AC/README.html Tue Mar 12 19:55:17 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 f4c82c165f58 -r 2aea76fe9c73 src/ZF/Coind/README.html --- a/src/ZF/Coind/README.html Tue Mar 12 19:55:17 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 f4c82c165f58 -r 2aea76fe9c73 src/ZF/Constructible/README.html --- a/src/ZF/Constructible/README.html Tue Mar 12 19:55:17 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 f4c82c165f58 -r 2aea76fe9c73 src/ZF/IMP/README.html --- a/src/ZF/IMP/README.html Tue Mar 12 19:55:17 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 f4c82c165f58 -r 2aea76fe9c73 src/ZF/README.html --- a/src/ZF/README.html Tue Mar 12 19:55:17 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 f4c82c165f58 -r 2aea76fe9c73 src/ZF/ROOT --- a/src/ZF/ROOT Tue Mar 12 19:55:17 2013 +0100 +++ b/src/ZF/ROOT Tue Mar 12 22:24:01 2013 +0100 @@ -1,11 +1,46 @@ +chapter ZF + session ZF (main) = Pure + description {* 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 @@ -19,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 @@ -41,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, @@ -49,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" @@ -120,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 @@ -148,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 f4c82c165f58 -r 2aea76fe9c73 src/ZF/Resid/README.html --- a/src/ZF/Resid/README.html Tue Mar 12 19:55:17 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 f4c82c165f58 -r 2aea76fe9c73 src/ZF/ex/README.html --- a/src/ZF/ex/README.html Tue Mar 12 19:55:17 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. - - -