discontinued special support for README.html (which was hardly ever used in the past 2 decades);
--- a/NEWS Fri Aug 19 21:43:06 2022 +0200
+++ b/NEWS Fri Aug 19 23:58:44 2022 +0200
@@ -194,6 +194,10 @@
*** System ***
+* HTML presentation no longer supports README.html, which was meant as
+add-on to the index.html of a session. Rare INCOMPATIBILITY, consider
+using a separate theory "README" with Isabelle document markup/markdown.
+
* Isabelle/Scala is now based on Scala 3. This is a completely different
compiler ("dotty") and a quite different source language (we are using
the classic Java-style syntax, not the new Python-style syntax).
--- a/src/HOL/Algebra/README.html Fri Aug 19 21:43:06 2022 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,85 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-
-<HTML>
-
-<HEAD>
- <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
- <TITLE>HOL/Algebra/README.html</TITLE>
-</HEAD>
-
-<BODY>
-
-<H1>Algebra --- Classical Algebra, using Explicit Structures and Locales</H1>
-
-This directory contains proofs in classical algebra. It is intended
-as a base for any algebraic development in Isabelle. Emphasis is on
-reusability. This is achieved by modelling algebraic structures
-as first-class citizens of the logic (not axiomatic type classes, say).
-The library is expected to grow in future releases of Isabelle.
-Contributions are welcome.
-
-<H2>GroupTheory, including Sylow's Theorem</H2>
-
-<P>These proofs are mainly by Florian Kammüller. (Later, Larry
-Paulson simplified some of the proofs.) These theories were indeed
-the original motivation for locales.
-
-Here is an outline of the directory's contents: <UL> <LI>Theory <A
-HREF="Group.html"><CODE>Group</CODE></A> defines semigroups, monoids,
-groups, commutative monoids, commutative groups, homomorphisms and the
-subgroup relation. It also defines the product of two groups
-(This theory was reimplemented by Clemens Ballarin).
-
-<LI>Theory <A HREF="FiniteProduct.html"><CODE>FiniteProduct</CODE></A> extends
-commutative groups by a product operator for finite sets (provided by
-Clemens Ballarin).
-
-<LI>Theory <A HREF="Coset.html"><CODE>Coset</CODE></A> defines
-the factorization of a group and shows that the factorization a normal
-subgroup is a group.
-
-<LI>Theory <A HREF="Bij.html"><CODE>Bij</CODE></A>
-defines bijections over sets and operations on them and shows that they
-are a group. It shows that automorphisms form a group.
-
-<LI>Theory <A HREF="Exponent.html"><CODE>Exponent</CODE></A> the
- combinatorial argument underlying Sylow's first theorem.
-
-<LI>Theory <A HREF="Sylow.html"><CODE>Sylow</CODE></A>
-contains a proof of the first Sylow theorem.
-</UL>
-
-<H2>Rings and Polynomials</H2>
-
-<UL><LI>Theory <A HREF="Ring.html"><CODE>CRing</CODE></A>
-defines Abelian monoids and groups. The difference to commutative
- structures is merely notational: the binary operation is
- addition rather than multiplication. Commutative rings are
- obtained by inheriting properties from Abelian groups and
- commutative monoids. Further structures in the algebraic
- hierarchy of rings: integral domain.
-
-<LI>Theory <A HREF="Module.html"><CODE>Module</CODE></A>
-introduces the notion of a R-left-module over an Abelian group, where
- R is a ring.
-
-<LI>Theory <A HREF="UnivPoly.html"><CODE>UnivPoly</CODE></A>
-constructs univariate polynomials over rings and integral domains.
- Degree function. Universal Property.
-</UL>
-
-<H2>Development of Polynomials using Type Classes</H2>
-
-<P>A development of univariate polynomials for HOL's ring classes
-is available at <CODE>HOL/Library/Polynomial</CODE>.
-
-<P>[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985.
-
-<P>[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving,
- Author's PhD thesis, 1999. Also University of Cambridge, Computer Laboratory Technical Report number 473.
-
-<ADDRESS>
-<P><A HREF="http://www21.in.tum.de/~ballarin">Clemens Ballarin</A>.
-</ADDRESS>
-</BODY>
-</HTML>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Algebra/README.thy Fri Aug 19 23:58:44 2022 +0200
@@ -0,0 +1,74 @@
+theory README imports Main
+begin
+
+section \<open>Algebra --- Classical Algebra, using Explicit Structures and Locales\<close>
+
+text \<open>
+ This directory contains proofs in classical algebra. It is intended as a
+ base for any algebraic development in Isabelle. Emphasis is on reusability.
+ This is achieved by modelling algebraic structures as first-class citizens
+ of the logic (not axiomatic type classes, say). The library is expected to
+ grow in future releases of Isabelle. Contributions are welcome.
+\<close>
+
+subsection \<open>GroupTheory, including Sylow's Theorem\<close>
+
+text \<open>
+ These proofs are mainly by Florian Kammüller. (Later, Larry Paulson
+ simplified some of the proofs.) These theories were indeed the original
+ motivation for locales.
+
+ Here is an outline of the directory's contents:
+
+ \<^item> Theory \<^file>\<open>Group.thy\<close> defines semigroups, monoids, groups, commutative
+ monoids, commutative groups, homomorphisms and the subgroup relation. It
+ also defines the product of two groups (This theory was reimplemented by
+ Clemens Ballarin).
+
+ \<^item> Theory \<^file>\<open>FiniteProduct.thy\<close> extends commutative groups by a product
+ operator for finite sets (provided by Clemens Ballarin).
+
+ \<^item> Theory \<^file>\<open>Coset.thy\<close> defines the factorization of a group and shows that
+ the factorization a normal subgroup is a group.
+
+ \<^item> Theory \<^file>\<open>Bij.thy\<close> defines bijections over sets and operations on them and
+ shows that they are a group. It shows that automorphisms form a group.
+
+ \<^item> Theory \<^file>\<open>Exponent.thy\<close> the combinatorial argument underlying Sylow's
+ first theorem.
+
+ \<^item> Theory \<^file>\<open>Sylow.thy\<close> contains a proof of the first Sylow theorem.
+\<close>
+
+
+subsection \<open>Rings and Polynomials\<close>
+
+text \<open>
+ \<^item> Theory \<^file>\<open>Ring.thy\<close> defines Abelian monoids and groups. The difference to
+ commutative structures is merely notational: the binary operation is
+ addition rather than multiplication. Commutative rings are obtained by
+ inheriting properties from Abelian groups and commutative monoids. Further
+ structures in the algebraic hierarchy of rings: integral domain.
+
+ \<^item> Theory \<^file>\<open>Module.thy\<close> introduces the notion of a R-left-module over an
+ Abelian group, where R is a ring.
+
+ \<^item> Theory \<^file>\<open>UnivPoly.thy\<close> constructs univariate polynomials over rings and
+ integral domains. Degree function. Universal Property.
+\<close>
+
+
+subsection \<open>Development of Polynomials using Type Classes\<close>
+
+text \<open>
+ A development of univariate polynomials for HOL's ring classes is available
+ at \<^file>\<open>~~/src/HOL/Computational_Algebra/Polynomial.thy\<close>.
+
+ [Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985.
+
+ [Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving,
+ Author's PhD thesis, 1999. Also University of Cambridge, Computer Laboratory
+ Technical Report number 473.
+\<close>
+
+end
--- a/src/HOL/Auth/Guard/README.html Fri Aug 19 21:43:06 2022 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,68 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-
-<HTML>
-
-<HEAD>
- <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
- <TITLE>HOL/Auth/Guard/README.html</TITLE>
-</HEAD>
-
-<BODY>
-
-<H1>Protocol-Independent Secrecy Results</H1>
-
-date: april 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage:
-
-<P>The current development is built above the HOL (Higher-Order Logic)
-Isabelle theory and the formalization of protocols introduced by <A
-HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>. More details are
-in his paper <A
-HREF="http://www.cl.cam.ac.uk/users/lcp/papers/Auth/jcs.pdf">
-The Inductive approach
-to verifying cryptographic protocols</A> (J. Computer Security 6, pages
-85-128, 1998).
-
-<P>
-This directory contains a number of files:
-
-<UL>
-<LI>Extensions.thy contains extensions of Larry Paulson's files with many useful
-lemmas.
-
-<LI>Analz contains an important theorem about the decomposition of analz
-between pparts (pairs) and kparts (messages that are not pairs).
-
-<LI>Guard contains the protocol-independent secrecy theorem for nonces.
-<LI>GuardK is the same for keys.
-<LI>Guard_Public extends Guard and GuardK for public-key protocols.
-<LI>Guard_Shared extends Guard and GuardK for symmetric-key protocols.
-
-<LI>List_Msg contains definitions on lists (inside messages).
-
-<LI>P1 contains the definition of the protocol P1 and the proof of its
-properties (strong forward integrity, insertion resilience, truncation
-resilience, data confidentiality and non-repudiability)
-
-<LI>P2 is the same for the protocol P2
-
-<LI>NS_Public is for Needham-Schroeder-Lowe
-<LI>OtwayRees is for Otway-Rees
-<LI>Yahalom is for Yahalom
-
-<LI>Proto contains a more precise formalization of protocols with rules
-and a protocol-independent theorem for proving guardness from a preservation
-property. It also contains the proofs for Needham-Schroeder as an example.
-</UL>
-
-<HR>
-<P>Last modified 20 August 2002
-
-<ADDRESS>
-<A HREF="http://www.lri.fr/~blanqui/">Frederic Blanqui</A>,
-<A HREF="mailto:blanqui@lri.fr">blanqui@lri.fr</A>
-</ADDRESS>
-</BODY>
-</HTML>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/Guard/README_Guard.thy Fri Aug 19 23:58:44 2022 +0200
@@ -0,0 +1,57 @@
+theory README_Guard imports Main
+begin
+
+section \<open>Protocol-Independent Secrecy Results\<close>
+
+text \<open>
+ \<^item> date: April 2002
+ \<^item> author: Frederic Blanqui
+ \<^item> email: blanqui@lri.fr
+
+ The current development is built above the HOL (Higher-Order Logic) Isabelle
+ theory and the formalization of protocols introduced by Larry Paulson. More
+ details are in his paper
+ \<^url>\<open>https://www.cl.cam.ac.uk/users/lcp/papers/Auth/jcs.pdf\<close>: \<^emph>\<open>The Inductive
+ approach to verifying cryptographic protocols\<close> (J. Computer Security 6,
+ pages 85-128, 1998).
+
+ This directory contains a number of files:
+
+ \<^item> \<^file>\<open>Extensions.thy\<close> contains extensions of Larry Paulson's files with
+ many useful lemmas.
+
+ \<^item> \<^file>\<open>Analz.thy\<close> contains an important theorem about the decomposition of
+ analz between pparts (pairs) and kparts (messages that are not pairs).
+
+ \<^item> \<^file>\<open>Guard.thy\<close> contains the protocol-independent secrecy theorem for
+ nonces.
+
+ \<^item> \<^file>\<open>GuardK.thy\<close> is the same for keys.
+
+ \<^item> \<^file>\<open>Guard_Public.thy\<close> extends \<^file>\<open>Guard.thy\<close> and \<^file>\<open>GuardK.thy\<close> for
+ public-key protocols.
+
+ \<^item> \<^file>\<open>Guard_Shared.thy\<close> extends \<^file>\<open>Guard.thy\<close> and \<^file>\<open>GuardK.thy\<close> for
+ symmetric-key protocols.
+
+ \<^item> \<^file>\<open>List_Msg.thy\<close> contains definitions on lists (inside messages).
+
+ \<^item> \<^file>\<open>P1.thy\<close> contains the definition of the protocol P1 and the proof of
+ its properties (strong forward integrity, insertion resilience,
+ truncation resilience, data confidentiality and non-repudiability).
+
+ \<^item> \<^file>\<open>P2.thy\<close> is the same for the protocol P2
+
+ \<^item> \<^file>\<open>Guard_NS_Public.thy\<close> is for Needham-Schroeder-Lowe
+
+ \<^item> \<^file>\<open>Guard_OtwayRees.thy\<close> is for Otway-Rees
+
+ \<^item> \<^file>\<open>Guard_Yahalom.thy\<close> is for Yahalom
+
+ \<^item> \<^file>\<open>Proto.thy\<close> contains a more precise formalization of protocols with
+ rules and a protocol-independent theorem for proving guardness from a
+ preservation property. It also contains the proofs for Needham-Schroeder
+ as an example.
+\<close>
+
+end
--- a/src/HOL/Auth/README.html Fri Aug 19 21:43:06 2022 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-
-<HTML>
-
-<HEAD>
- <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
- <TITLE>HOL/Auth/README</TITLE>
-</HEAD>
-
-<BODY>
-
-<H1>Auth--The Inductive Approach to Verifying Security Protocols</H1>
-
-<P>Cryptographic protocols are of major importance, especially with the
-growing use of the Internet. This directory demonstrates the ``inductive
-method'' of protocol verification, which is described in <A
-HREF="http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html">various
-papers</A>. The operational semantics of protocol participants is defined
-inductively.
-
-<P>This directory contains proofs concerning
-
-<UL>
-<LI>three versions of the Otway-Rees protocol
-
-<LI>the Needham-Schroeder shared-key protocol
-
-<LI>the Needham-Schroeder public-key protocol (original and with Lowe's
-modification)
-
-<LI>two versions of Kerberos: the simplified form published in the BAN paper
- and also the full protocol (Kerberos IV)
-
-<LI>three versions of the Yahalom protocol, including a bad one that
- illustrates the purpose of the Oops rule
-
-<LI>a novel recursive authentication protocol
-
-<LI>the Internet protocol TLS
-
-<LI>The certified e-mail protocol of Abadi et al.
-</UL>
-
-<P>Frederic Blanqui has contributed a theory of guardedness, which is
-demonstrated by proofs of some roving agent protocols.
-
-<ADDRESS>
-<A
-HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>,
-<A HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
-</ADDRESS>
-</BODY>
-</HTML>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/README.thy Fri Aug 19 23:58:44 2022 +0200
@@ -0,0 +1,38 @@
+theory README imports Main
+begin
+
+section \<open>Auth--The Inductive Approach to Verifying Security Protocols\<close>
+
+text \<open>
+ Cryptographic protocols are of major importance, especially with the growing
+ use of the Internet. This directory demonstrates the ``inductive method'' of
+ protocol verification, which is described in papers:
+ \<^url>\<open>http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html\<close>. The operational
+ semantics of protocol participants is defined inductively.
+
+ This directory contains proofs concerning:
+
+ \<^item> three versions of the Otway-Rees protocol
+
+ \<^item> the Needham-Schroeder shared-key protocol
+
+ \<^item> the Needham-Schroeder public-key protocol (original and with Lowe's
+ modification)
+
+ \<^item> two versions of Kerberos: the simplified form published in the BAN paper
+ and also the full protocol (Kerberos IV)
+
+ \<^item> three versions of the Yahalom protocol, including a bad one that
+ illustrates the purpose of the Oops rule
+
+ \<^item> a novel recursive authentication protocol
+
+ \<^item> the Internet protocol TLS
+
+ \<^item> The certified e-mail protocol of Abadi et al.
+
+ Frederic Blanqui has contributed a theory of guardedness, which is
+ demonstrated by proofs of some roving agent protocols.
+\<close>
+
+end
--- a/src/HOL/HOLCF/README.html Fri Aug 19 21:43:06 2022 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,54 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-
-<html>
-
-<head>
- <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
- <title>HOLCF/README</title>
-</head>
-
-<body>
-
-<h3>HOLCF: A higher-order version of LCF based on Isabelle/HOL</h3>
-
-HOLCF is the definitional extension of Church's Higher-Order Logic with
-Scott's Logic for Computable Functions that has been implemented in the
-theorem prover Isabelle. This results in a flexible setup for reasoning
-about functional programs. HOLCF supports standard domain theory (in particular
-fixpoint reasoning and recursive domain equations) but also coinductive
-arguments about lazy datatypes.
-
-<p>
-
-The most recent description of HOLCF is found here:
-
-<ul>
- <li><a href="http://web.cecs.pdx.edu/~brianh/phdthesis.html">HOLCF '11: A Definitional Domain Theory for Verifying Functional Programs</a>, <br>
- Brian Huffman.<br>
- Ph.D. thesis, Portland State University.<br>
- Year: 2012.
-</ul>
-
-Descriptions of earlier versions can also be found online:
-
-<ul>
- <li><a href="/~nipkow/pubs/jfp99.html">HOLCF = HOL+LCF</a>
-</ul>
-
-A detailed description (in German) of the entire development can be found in:
-
-<ul>
- <li><a href="http://www4.informatik.tu-muenchen.de/publ/papers/Diss_Regensbu.pdf">HOLCF: eine konservative Erweiterung von HOL um LCF</a>, <br>
- Franz Regensburger.<br>
- Dissertation Technische Universität München.<br>
- Year: 1994.
-</ul>
-
-A short survey is available in:
-<ul>
- <li><a href="http://www4.informatik.tu-muenchen.de/publ/papers/Regensburger_HOLT1995.pdf">HOLCF: Higher Order Logic of Computable Functions</a><br>
-</ul>
-
-</body>
-
-</html>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOLCF/README.thy Fri Aug 19 23:58:44 2022 +0200
@@ -0,0 +1,37 @@
+theory README imports Main
+begin
+
+section \<open>HOLCF: A higher-order version of LCF based on Isabelle/HOL\<close>
+
+text \<open>
+ HOLCF is the definitional extension of Church's Higher-Order Logic with
+ Scott's Logic for Computable Functions that has been implemented in the
+ theorem prover Isabelle. This results in a flexible setup for reasoning
+ about functional programs. HOLCF supports standard domain theory (in
+ particular fixpoint reasoning and recursive domain equations) but also
+ coinductive arguments about lazy datatypes.
+
+ The most recent description of HOLCF is found here:
+
+ \<^item> \<^emph>\<open>HOLCF '11: A Definitional Domain Theory for Verifying Functional
+ Programs\<close> \<^url>\<open>http://web.cecs.pdx.edu/~brianh/phdthesis.html\<close>, Brian
+ Huffman. Ph.D. thesis, Portland State University. 2012.
+
+ Descriptions of earlier versions can also be found online:
+
+ \<^item> \<^emph>\<open>HOLCF = HOL+LCF\<close> \<^url>\<open>https://www21.in.tum.de/~nipkow/pubs/jfp99.html\<close>
+
+ A detailed description (in German) of the entire development can be found
+ in:
+
+ \<^item> \<^emph>\<open>HOLCF: eine konservative Erweiterung von HOL um LCF\<close>
+ \<^url>\<open>http://www4.informatik.tu-muenchen.de/publ/papers/Diss_Regensbu.pdf\<close>,
+ Franz Regensburger. Dissertation Technische Universität München. 1994.
+
+ A short survey is available in:
+
+ \<^item> \<^emph>\<open>HOLCF: Higher Order Logic of Computable Functions\<close>
+ \<^url>\<open>http://www4.informatik.tu-muenchen.de/publ/papers/Regensburger_HOLT1995.pdf\<close>
+\<close>
+
+end
--- a/src/HOL/Hoare/README.html Fri Aug 19 21:43:06 2022 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,119 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-
-<HTML>
-
-<HEAD>
- <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
- <TITLE>HOL/Hoare/ReadMe</TITLE>
-</HEAD>
-
-<BODY>
-
-<H2>Hoare Logic for a Simple WHILE Language</H2>
-
-<H3>Language and logic</H3>
-
-This directory contains an implementation of Hoare logic for a simple WHILE
-language. The constructs are
-<UL>
-<LI> <kbd>SKIP</kbd>
-<LI> <kbd>_ := _</kbd>
-<LI> <kbd>_ ; _</kbd>
-<LI> <kbd>IF _ THEN _ ELSE _ FI</kbd>
-<LI> <kbd>WHILE _ INV {_} DO _ OD</kbd>
-</UL>
-Note that each WHILE-loop must be annotated with an invariant.
-<P>
-
-After loading theory Hoare, you can state goals of the form
-<PRE>
-VARS x y ... {P} prog {Q}
-</PRE>
-where <kbd>prog</kbd> is a program in the above language, <kbd>P</kbd> is the
-precondition, <kbd>Q</kbd> the postcondition, and <kbd>x y ...</kbd> is the
-list of all <i>program variables</i> in <kbd>prog</kbd>. The latter list must
-be nonempty and it must include all variables that occur on the left-hand
-side of an assignment in <kbd>prog</kbd>. Example:
-<PRE>
-VARS x {x = a} x := x+1 {x = a+1}
-</PRE>
-The (normal) variable <kbd>a</kbd> is merely used to record the initial
-value of <kbd>x</kbd> and is not a program variable. Pre/post conditions
-can be arbitrary HOL formulae mentioning both program variables and normal
-variables.
-<P>
-
-The implementation hides reasoning in Hoare logic completely and provides a
-method <kbd>vcg</kbd> for transforming a goal in Hoare logic into an
-equivalent list of verification conditions in HOL:
-<PRE>
-apply vcg
-</PRE>
-If you want to simplify the resulting verification conditions at the same
-time:
-<PRE>
-apply vcg_simp
-</PRE>
-which, given the example goal above, solves it completely. For further
-examples see <a href="Examples.html">Examples</a>.
-<P>
-
-IMPORTANT:
-This is a logic of partial correctness. You can only prove that your program
-does the right thing <i>if</i> it terminates, but not <i>that</i> it
-terminates.
-A logic of total correctness is also provided and described below.
-
-<H3>Total correctness</H3>
-
-To prove termination, each WHILE-loop must be annotated with a variant:
-<UL>
-<LI> <kbd>WHILE _ INV {_} VAR {_} DO _ OD</kbd>
-</UL>
-A variant is an expression with type <kbd>nat</kbd>, which may use program
-variables and normal variables.
-<P>
-
-A total-correctness goal has the form
-<PRE>
-VARS x y ... [P] prog [Q]
-</PRE>
-enclosing the pre- and postcondition in square brackets.
-<P>
-
-Methods <kbd>vcg_tc</kbd> and <kbd>vcg_tc_simp</kbd> can be used to derive
-verification conditions.
-<P>
-
-From a total-correctness proof, a function can be extracted which
-for every input satisfying the precondition returns an output
-satisfying the postcondition.
-
-<H3>Notes on the implementation</H3>
-
-The implementation loosely follows
-<P>
-Mike Gordon.
-<cite>Mechanizing Programming Logics in Higher Order Logic.</cite><BR>
-University of Cambridge, Computer Laboratory, TR 145, 1988.
-<P>
-published as
-<P>
-Mike Gordon.
-<cite>Mechanizing Programming Logics in Higher Order Logic.</cite><BR>
-In
-<cite>Current Trends in Hardware Verification and Automated Theorem Proving
-</cite>,<BR>
-edited by G. Birtwistle and P.A. Subrahmanyam, Springer-Verlag, 1989.
-<P>
-
-The main differences: the state is modelled as a tuple as suggested in
-<P>
-J. von Wright and J. Hekanaho and P. Luostarinen and T. Langbacka.
-<cite>Mechanizing Some Advanced Refinement Concepts</cite>.
-Formal Methods in System Design, 3, 1993, 49-81.
-<P>
-and the embeding is deep, i.e. there is a concrete datatype of programs. The
-latter is not really necessary.
-</BODY>
-</HTML>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare/README.thy Fri Aug 19 23:58:44 2022 +0200
@@ -0,0 +1,93 @@
+theory README imports Main
+begin
+
+section \<open>Hoare Logic for a Simple WHILE Language\<close>
+
+subsection \<open>Language and logic\<close>
+
+text \<open>
+ This directory contains an implementation of Hoare logic for a simple WHILE
+ language. The constructs are
+
+ \<^item> \<^verbatim>\<open>SKIP\<close>
+ \<^item> \<^verbatim>\<open>_ := _\<close>
+ \<^item> \<^verbatim>\<open>_ ; _\<close>
+ \<^item> \<^verbatim>\<open>IF _ THEN _ ELSE _ FI\<close>
+ \<^item> \<^verbatim>\<open>WHILE _ INV {_} DO _ OD\<close>
+
+ Note that each WHILE-loop must be annotated with an invariant.
+
+ Within the context of theory \<^verbatim>\<open>Hoare\<close>, you can state goals of the form
+ @{verbatim [display] \<open>VARS x y ... {P} prog {Q}\<close>}
+ where \<^verbatim>\<open>prog\<close> is a program in the above language, \<^verbatim>\<open>P\<close> is the precondition,
+ \<^verbatim>\<open>Q\<close> the postcondition, and \<^verbatim>\<open>x y ...\<close> is the list of all \<^emph>\<open>program
+ variables\<close> in \<^verbatim>\<open>prog\<close>. The latter list must be nonempty and it must include
+ all variables that occur on the left-hand side of an assignment in \<^verbatim>\<open>prog\<close>.
+ Example:
+ @{verbatim [display] \<open>VARS x {x = a} x := x+1 {x = a+1}\<close>}
+ The (normal) variable \<^verbatim>\<open>a\<close> is merely used to record the initial value of
+ \<^verbatim>\<open>x\<close> and is not a program variable. Pre/post conditions can be arbitrary HOL
+ formulae mentioning both program variables and normal variables.
+
+ The implementation hides reasoning in Hoare logic completely and provides a
+ method \<^verbatim>\<open>vcg\<close> for transforming a goal in Hoare logic into an equivalent list
+ of verification conditions in HOL: \<^theory_text>\<open>apply vcg\<close>
+
+ If you want to simplify the resulting verification conditions at the same
+ time: \<^theory_text>\<open>apply vcg_simp\<close> which, given the example goal above, solves it
+ completely. For further examples see \<^file>\<open>Examples.thy\<close>.
+
+ \<^bold>\<open>IMPORTANT:\<close>
+ This is a logic of partial correctness. You can only prove that your program
+ does the right thing \<^emph>\<open>if\<close> it terminates, but not \<^emph>\<open>that\<close> it terminates. A
+ logic of total correctness is also provided and described below.
+\<close>
+
+
+subsection \<open>Total correctness\<close>
+
+text \<open>
+ To prove termination, each WHILE-loop must be annotated with a variant:
+
+ \<^item> \<^verbatim>\<open>WHILE _ INV {_} VAR {_} DO _ OD\<close>
+
+ A variant is an expression with type \<^verbatim>\<open>nat\<close>, which may use program variables
+ and normal variables.
+
+ A total-correctness goal has the form \<^verbatim>\<open>VARS x y ... [P] prog [Q]\<close> enclosing
+ the pre- and postcondition in square brackets.
+
+ Methods \<^verbatim>\<open>vcg_tc\<close> and \<^verbatim>\<open>vcg_tc_simp\<close> can be used to derive verification
+ conditions.
+
+ From a total-correctness proof, a function can be extracted which for every
+ input satisfying the precondition returns an output satisfying the
+ postcondition.
+\<close>
+
+
+subsection \<open>Notes on the implementation\<close>
+
+text \<open>
+ The implementation loosely follows
+
+ Mike Gordon. \<^emph>\<open>Mechanizing Programming Logics in Higher Order Logic\<close>.
+ University of Cambridge, Computer Laboratory, TR 145, 1988.
+
+ published as
+
+ Mike Gordon. \<^emph>\<open>Mechanizing Programming Logics in Higher Order Logic\<close>. In
+ \<^emph>\<open>Current Trends in Hardware Verification and Automated Theorem Proving\<close>,
+ edited by G. Birtwistle and P.A. Subrahmanyam, Springer-Verlag, 1989.
+
+ The main differences: the state is modelled as a tuple as suggested in
+
+ J. von Wright and J. Hekanaho and P. Luostarinen and T. Langbacka.
+ \<^emph>\<open>Mechanizing Some Advanced Refinement Concepts\<close>. Formal Methods in System
+ Design, 3, 1993, 49-81.
+
+ and the embeding is deep, i.e. there is a concrete datatype of programs. The
+ latter is not really necessary.
+\<close>
+
+end
--- a/src/HOL/Library/README.html Fri Aug 19 21:43:06 2022 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,72 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-
-<html>
-
-<head>
- <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
- <title>HOL-Library/README</title>
-</head>
-
-<body>
-
-<h1>HOL-Library: supplemental theories for main Isabelle/HOL</h1>
-
-This is a collection of generic theories that may be used together
-with main Isabelle/HOL.
-
-<p>
-
-Addition of new theories should be done with some care, as the
-``module system'' of Isabelle is rather simplistic. The following
-guidelines may be helpful to achieve maximum re-usability and minimum
-clashes with existing developments.
-
-<dl>
-
-<dt><strong>Examples</strong>
-
-<dd>Theories should be as ``generic'' as is sensible. Unused (or
-rather unusable?) theories should be avoided; common applications
-should actually refer to the present theory. Small example uses may
-be included in the library as well, but should be put in a separate
-theory, such as <tt>Foobar</tt> accompanied by
-<tt>Foobar_Examples</tt>.
-
-<dt><strong>Theory names</strong>
-
-<dd>The theory loader name space is <em>flat</em>, so use sufficiently
-long and descriptive names to reduce the danger of clashes with the
-user's own theories. The convention for theory names is as follows:
-<tt>Foobar_Doobar</tt> (this looks best in LaTeX output).
-
-<dt><strong>Names of logical items</strong>
-
-<dd>There are separate hierarchically structured name spaces for
-types, constants, theorems etc. Nevertheless, some care should be
-taken, as the name spaces are always ``open''. Use adequate names;
-avoid unreadable abbreviations. The general naming convention is to
-separate word constituents by underscores, as in <tt>foo_bar</tt> or
-<tt>Foo_Bar</tt> (this looks best in LaTeX output).
-
-<dt><strong>Global context declarations</strong>
-
-<dd>Only items introduced in the present theory should be declared
-globally (e.g. as Simplifier rules). Note that adding and deleting
-rules from parent theories may result in strange behavior later,
-depending on the user's arrangement of import lists.
-
-<dt><strong>Spacing</strong>
-
-<dd>Isabelle is able to produce a high-quality LaTeX document from the
-theory sources, provided some minor issues are taken care of. In
-particular, spacing and line breaks are directly taken from source
-text. Incidentally, output looks very good if common type-setting
-conventions are observed: put a single space <em>after</em> each
-punctuation character ("<tt>,</tt>", "<tt>.</tt>", etc.), but none
-before it; do not extra spaces inside of parentheses; do not attempt
-to simulate table markup with spaces, avoid ``hanging'' indentations.
-
-</dl>
-
-</body>
-</html>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/README.thy Fri Aug 19 23:58:44 2022 +0200
@@ -0,0 +1,43 @@
+theory README imports Main
+begin
+
+section \<open>HOL-Library: supplemental theories for main Isabelle/HOL\<close>
+
+text \<open>
+ This is a collection of generic theories that may be used together with main
+ Isabelle/HOL.
+
+ Addition of new theories should be done with some care, as the ``module
+ system'' of Isabelle is rather simplistic. The following guidelines may be
+ helpful to achieve maximum re-usability and minimum clashes with existing
+ developments.
+
+ \<^descr>[Examples] Theories should be as ``generic'' as is sensible. Unused (or
+ rather unusable?) theories should be avoided; common applications should
+ actually refer to the present theory. Small example uses may be included in
+ the library as well, but should be put in a separate theory, such as
+ \<^verbatim>\<open>Foobar.thy\<close> accompanied by \<^verbatim>\<open>Foobar_Examples.thy\<close>.
+
+ \<^descr>[Names of logical items] There are separate hierarchically structured name
+ spaces for types, constants, theorems etc. Nevertheless, some care should be
+ taken, as the name spaces are always ``open''. Use adequate names; avoid
+ unreadable abbreviations. The general naming convention is to separate word
+ constituents by underscores, as in \<^verbatim>\<open>foo_bar\<close> or \<^verbatim>\<open>Foo_Bar\<close> (this looks best
+ in LaTeX output).
+
+ \<^descr>[Global context declarations] Only items introduced in the present theory
+ should be declared globally (e.g. as Simplifier rules). Note that adding and
+ deleting rules from parent theories may result in strange behavior later,
+ depending on the user's arrangement of import lists.
+
+ \<^descr>[Spacing] Isabelle is able to produce a high-quality LaTeX document from
+ the theory sources, provided some minor issues are taken care of. In
+ particular, spacing and line breaks are directly taken from source text.
+ Incidentally, output looks very good if common type-setting conventions are
+ observed: put a single space \<^emph>\<open>after\<close> each punctuation character ("\<^verbatim>\<open>,\<close>",
+ "\<^verbatim>\<open>.\<close>", etc.), but none before it; do not extra spaces inside of
+ parentheses; do not attempt to simulate table markup with spaces, avoid
+ ``hanging'' indentations.
+\<close>
+
+end
--- a/src/HOL/ROOT Fri Aug 19 21:43:06 2022 +0200
+++ b/src/HOL/ROOT Fri Aug 19 23:58:44 2022 +0200
@@ -58,6 +58,8 @@
description "
Classical Higher-order Logic -- batteries included.
"
+ theories [document = false]
+ README
theories
Library
(*conflicting type class instantiations and dependent applications*)
@@ -326,6 +328,8 @@
Verification of imperative programs (verification conditions are generated
automatically from pre/post conditions and loop invariants).
"
+ theories [document = false]
+ README
theories
Examples
ExamplesAbort
@@ -406,6 +410,8 @@
sessions
"HOL-Cardinals"
"HOL-Combinatorics"
+ theories [document = false]
+ README
theories
(* Orders and Lattices *)
Galois_Connection (* Knaster-Tarski theorem and Galois connections *)
@@ -429,10 +435,15 @@
"
sessions "HOL-Library"
directories "Smartcard" "Guard"
+ theories [document = false]
+ README
theories
Auth_Shared
Auth_Public
"Smartcard/Auth_Smartcard"
+ theories [document = false]
+ "Guard/README_Guard"
+ theories
"Guard/Auth_Guard_Shared"
"Guard/Auth_Guard_Public"
document_files "root.tex"
@@ -445,10 +456,15 @@
Verifying security protocols using Chandy and Misra's UNITY formalism.
"
directories "Simple" "Comp"
+ theories [document = false]
+ README
theories
(*Basic meta-theory*)
UNITY_Main
+ theories [document = false]
+ "Simple/README_Simple"
+ theories
(*Simple examples: no composition*)
"Simple/Deadlock"
"Simple/Common"
@@ -463,6 +479,9 @@
(*Verifying security protocols using UNITY*)
"Simple/NSP_Bad"
+ theories [document = false]
+ "Comp/README_Comp"
+ theories
(*Example of composition*)
"Comp/Handshake"
@@ -783,7 +802,9 @@
description "
Lamport's Temporal Logic of Actions.
"
- theories TLA
+ theories
+ README
+ TLA
session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +
theories Inc
@@ -1083,6 +1104,8 @@
"
sessions
"HOL-Library"
+ theories [document = false]
+ README
theories
HOLCF (global)
document_files "root.tex"
--- a/src/HOL/TLA/README.html Fri Aug 19 21:43:06 2022 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,68 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-
-<HTML>
-
-<HEAD>
- <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
- <TITLE>HOL/TLA</TITLE>
-</HEAD>
-
-<BODY>
-
-<H2>TLA: Lamport's Temporal Logic of Actions</H2>
-
-<A HREF="http://www.research.digital.com/SRC/personal/Leslie_Lamport/tla/tla.html">TLA</A>
-is a linear-time temporal logic introduced by Leslie Lamport in
-<EM>The Temporal Logic of Actions</EM> (ACM TOPLAS 16(3), 1994,
-872-923). Unlike other temporal logics, both systems and properties
-are represented as logical formulas, and logical connectives such as
-implication, conjunction, and existential quantification represent
-structural relations such as refinement, parallel composition, and
-hiding. TLA has been applied to numerous case studies.
-
-<P>This directory formalizes TLA in Isabelle/HOL, as follows:
-<UL>
-<LI>Theory <A HREF="Intensional.html">Intensional</A> prepares the
- ground by introducing basic syntax for "lifted", possibl-world based
- logics.
-<LI>Theories <A HREF="Stfun.html">Stfun</A> and
- <A HREF="Action.html">Action</A> represent the state and transition
- level formulas of TLA, evaluated over single states and pairs of
- states.
-<LI>Theory <A HREF="Init.html">Init</A> introduces temporal logic
- and defines conversion functions from nontemporal to temporal
- formulas.
-<LI>Theory <A HREF="TLA.html">TLA</A> axiomatizes proper temporal
- logic.
-</UL>
-
-Please consult the
-<A HREF="http://www.pst.informatik.uni-muenchen.de/~merz/isabelle/IsaTLADesign.ps">design notes</A>
-for further information regarding the setup and use of this encoding
-of TLA.
-
-<P>
-The theories are accompanied by a small number of examples:
-<UL>
-<LI><A HREF="Inc/index.html">Inc</A>: Lamport's <EM>increment</EM>
- example, a standard TLA benchmark, illustrates an elementary TLA
- proof.
-<LI><A HREF="Buffer/index.html">Buffer</A>: a proof that two buffers
- in a row implement a single buffer, uses a simple refinement
- mapping.
-<LI><A HREF="Memory/index.html">Memory</A>: a verification of (the
- untimed part of) Broy and Lamport's <em>RPC-Memory</em> case study,
- more fully explained in LNCS 1169 (the
- <A HREF="http://www.pst.informatik.uni-muenchen.de/~merz/papers/RPCMemory.html">TLA
- solution</A> is available separately).
-</UL>
-
-<HR>
-
-<ADDRESS>
-<A HREF="mailto:merz@informatik.uni-muenchen.de">Stephan Merz</A>
-</ADDRESS>
-<!-- hhmts start -->
-Last modified: Sat Mar 5 00:54:49 CET 2005
-<!-- hhmts end -->
-</BODY></HTML>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TLA/README.thy Fri Aug 19 23:58:44 2022 +0200
@@ -0,0 +1,48 @@
+theory README imports Main
+begin
+
+section \<open>TLA: Lamport's Temporal Logic of Actions\<close>
+
+text \<open>
+ TLA \<^url>\<open>http://www.research.digital.com/SRC/personal/Leslie_Lamport/tla/tla.html\<close>
+ is a linear-time temporal logic introduced by Leslie Lamport in \<^emph>\<open>The
+ Temporal Logic of Actions\<close> (ACM TOPLAS 16(3), 1994, 872-923). Unlike other
+ temporal logics, both systems and properties are represented as logical
+ formulas, and logical connectives such as implication, conjunction, and
+ existential quantification represent structural relations such as
+ refinement, parallel composition, and hiding. TLA has been applied to
+ numerous case studies.
+
+ This directory formalizes TLA in Isabelle/HOL, as follows:
+
+ \<^item> \<^file>\<open>Intensional.thy\<close> prepares the ground by introducing basic syntax for
+ "lifted", possible-world based logics.
+
+ \<^item> \<^file>\<open>Stfun.thy\<close> and \<^file>\<open>Action.thy\<close> represent the state and transition
+ level formulas of TLA, evaluated over single states and pairs of states.
+
+ \<^item> \<^file>\<open>Init.thy\<close> introduces temporal logic and defines conversion functions
+ from nontemporal to temporal formulas.
+
+ \<^item> \<^file>\<open>TLA.thy\<close> axiomatizes proper temporal logic.
+
+
+ Please consult the \<^emph>\<open>design notes\<close>
+ \<^url>\<open>http://www.pst.informatik.uni-muenchen.de/~merz/isabelle/IsaTLADesign.ps\<close>
+ for further information regarding the setup and use of this encoding of TLA.
+
+ The theories are accompanied by a small number of examples:
+
+ \<^item> \<^dir>\<open>Inc\<close>: Lamport's \<^emph>\<open>increment\<close> example, a standard TLA benchmark,
+ illustrates an elementary TLA proof.
+
+ \<^item> \<^dir>\<open>Buffer\<close>: a proof that two buffers in a row implement a single buffer,
+ uses a simple refinement mapping.
+
+ \<^item> \<^dir>\<open>Memory\<close>: a verification of (the untimed part of) Broy and Lamport's
+ \<^emph>\<open>RPC-Memory\<close> case study, more fully explained in LNCS 1169 (the \<^emph>\<open>TLA
+ solution\<close> is available separately from
+ \<^url>\<open>http://www.pst.informatik.uni-muenchen.de/~merz/papers/RPCMemory.html\<close>).
+\<close>
+
+end
--- a/src/HOL/UNITY/Comp/README.html Fri Aug 19 21:43:06 2022 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-
-<HTML>
-
-<HEAD>
- <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
- <TITLE>HOL/UNITY/README</TITLE>
-</HEAD>
-
-<BODY>
-
-<H2>UNITY: Examples Involving Program Composition</H2>
-
-<P>
-The directory presents verification examples involving program composition.
-They are mostly taken from the works of Chandy, Charpentier and Chandy.
-
-<UL>
-<LI>examples of <em>universal properties</em>:
-the counter (<A HREF="Counter.thy"><CODE>Counter.thy</CODE></A>)
-and priority system (<A HREF="Priority.thy"><CODE>Priority.thy</CODE></A>)
-
-<LI>the allocation system (<A HREF="Alloc.thy"><CODE>Alloc.thy</CODE></A>)
-
-<LI>client implementation (<A HREF="Client.thy"><CODE>Client.thy</CODE></A>)
-
-<LI>allocator implementation (<A HREF="AllocImpl.thy"><CODE>AllocImpl.thy</CODE></A>)
-
-<LI>the handshake protocol
-(<A HREF="Handshake.thy"><CODE>Handshake.thy</CODE></A>)
-
-<LI>the timer array (demonstrates arrays of processes)
-(<A HREF="TimerArray.thy"><CODE>TimerArray.thy</CODE></A>)
-</UL>
-
-<P> Safety proofs (invariants) are often proved automatically. Progress
-proofs involving ENSURES can sometimes be proved automatically. The
-level of automation appears to be about the same as in HOL-UNITY by Flemming
-Andersen et al.
-
-<ADDRESS>
-<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
-</ADDRESS>
-</BODY>
-</HTML>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Comp/README_Comp.thy Fri Aug 19 23:58:44 2022 +0200
@@ -0,0 +1,24 @@
+theory README_Comp imports Main
+begin
+
+section \<open>UNITY: Examples Involving Program Composition\<close>
+
+text \<open>
+ The directory presents verification examples involving program composition.
+ They are mostly taken from the works of Chandy, Charpentier and Chandy.
+
+ \<^item> examples of \<^emph>\<open>universal properties\<close>: the counter (\<^file>\<open>Counter.thy\<close>) and
+ priority system (\<^file>\<open>Priority.thy\<close>)
+ \<^item> the allocation system (\<^file>\<open>Alloc.thy\<close>)
+ \<^item> client implementation (\<^file>\<open>Client.thy\<close>)
+ \<^item> allocator implementation (\<^file>\<open>AllocImpl.thy\<close>)
+ \<^item> the handshake protocol (\<^file>\<open>Handshake.thy\<close>)
+ \<^item> the timer array (demonstrates arrays of processes) (\<^file>\<open>TimerArray.thy\<close>)
+
+ Safety proofs (invariants) are often proved automatically. Progress proofs
+ involving ENSURES can sometimes be proved automatically. The level of
+ automation appears to be about the same as in HOL-UNITY by Flemming Andersen
+ et al.
+\<close>
+
+end
--- a/src/HOL/UNITY/README.html Fri Aug 19 21:43:06 2022 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,49 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-
-<HTML>
-
-<HEAD>
- <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
- <TITLE>HOL/UNITY/README</TITLE>
-</HEAD>
-
-<BODY>
-
-<H2>UNITY--Chandy and Misra's UNITY formalism</H2>
-
-<P>The book <EM>Parallel Program Design: A Foundation</EM> by Chandy and Misra
-(Addison-Wesley, 1988) presents the UNITY formalism. UNITY consists of an
-abstract programming language of guarded assignments and a calculus for
-reasoning about such programs. Misra's 1994 paper "A Logic for Concurrent
-Programming" presents New UNITY, giving more elegant foundations for a more
-general class of languages. In recent work, Chandy and Sanders have proposed
-new methods for reasoning about systems composed of many components.
-
-<P>This directory formalizes these new ideas for UNITY. The Isabelle examples
-may seem strange to UNITY traditionalists. Hand UNITY proofs tend to be
-written in the forwards direction, as in informal mathematics, while Isabelle
-works best in a backwards (goal-directed) style. Programs are expressed as
-sets of commands, where each command is a relation on states. Quantification
-over commands using [] is easily expressed. At present, there are no examples
-of quantification using ||.
-
-<P>A UNITY assertion denotes the set of programs satisfying it, as
-in the propositions-as-types paradigm. The resulting style is readable if
-unconventional.
-
-<P> Safety proofs (invariants) are often proved automatically. Progress
-proofs involving ENSURES can sometimes be proved automatically. The
-level of automation appears to be about the same as in HOL-UNITY by Flemming
-Andersen et al.
-
-<P>
-The directory <A HREF="Simple/"><CODE>Simple</CODE></A>
-presents a few examples, mostly taken from Misra's 1994
-paper, involving single programs.
-The directory <A HREF="Comp/"><CODE>Comp</CODE></A>
-presents examples of proofs involving program composition.
-
-<ADDRESS>
-<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
-</ADDRESS>
-</BODY></HTML>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/README.thy Fri Aug 19 23:58:44 2022 +0200
@@ -0,0 +1,37 @@
+theory README imports Main
+begin
+
+section \<open>UNITY--Chandy and Misra's UNITY formalism\<close>
+
+text \<open>
+ The book \<^emph>\<open>Parallel Program Design: A Foundation\<close> by Chandy and Misra
+ (Addison-Wesley, 1988) presents the UNITY formalism. UNITY consists of an
+ abstract programming language of guarded assignments and a calculus for
+ reasoning about such programs. Misra's 1994 paper "A Logic for Concurrent
+ Programming" presents New UNITY, giving more elegant foundations for a more
+ general class of languages. In recent work, Chandy and Sanders have proposed
+ new methods for reasoning about systems composed of many components.
+
+ This directory formalizes these new ideas for UNITY. The Isabelle examples
+ may seem strange to UNITY traditionalists. Hand UNITY proofs tend to be
+ written in the forwards direction, as in informal mathematics, while
+ Isabelle works best in a backwards (goal-directed) style. Programs are
+ expressed as sets of commands, where each command is a relation on states.
+ Quantification over commands using \<^verbatim>\<open>[]\<close> is easily expressed. At present,
+ there are no examples of quantification using \<^verbatim>\<open>||\<close>.
+
+ A UNITY assertion denotes the set of programs satisfying it, as in the
+ propositions-as-types paradigm. The resulting style is readable if
+ unconventional.
+
+ Safety proofs (invariants) are often proved automatically. Progress proofs
+ involving ENSURES can sometimes be proved automatically. The level of
+ automation appears to be about the same as in HOL-UNITY by Flemming Andersen
+ et al.
+
+ The directory \<^dir>\<open>Simple\<close> presents a few examples, mostly taken from Misra's
+ 1994 paper, involving single programs. The directory \<^dir>\<open>Comp\<close> presents
+ examples of proofs involving program composition.
+\<close>
+
+end
--- a/src/HOL/UNITY/Simple/README.html Fri Aug 19 21:43:06 2022 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-
-<HTML>
-
-<HEAD>
- <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
- <TITLE>HOL/UNITY/README</TITLE>
-</HEAD>
-
-<BODY>
-
-<H2>UNITY: Examples Involving Single Programs</H2>
-
-<P> The directory presents verification examples that do not involve program
-composition. They are mostly taken from Misra's 1994 papers on ``New UNITY'':
-<UL>
-<LI>common meeting time (<A HREF="Common.thy"><CODE>Common.thy</CODE></A>)
-
-<LI>the token ring (<A HREF="Token.thy"><CODE>Token.thy</CODE></A>)
-
-<LI>the communication network
-(<A HREF="Network.thy"><CODE>Network.thy</CODE></A>)
-
-<LI>the lift controller (a standard benchmark) (<A HREF="Lift.thy"><CODE>Lift.thy</CODE></A>)
-
-<LI>a mutual exclusion algorithm (<A HREF="Mutex.thy"><CODE>Mutex.thy</CODE></A>)
-
-<LI><EM>n</EM>-process deadlock
-(<A HREF="Deadlock.thy"><CODE>Deadlock.thy</CODE></A>)
-
-<LI>unordered channel (<A HREF="Channel.thy"><CODE>Channel.thy</CODE></A>)
-
-<LI>reachability in directed graphs (section 6.4 of the book) (<A
-HREF="Reach.thy"><CODE>Reach.thy</CODE></A> and
-<A HREF="Reachability.thy"><CODE>Reachability.thy</CODE></A>)
-</UL>
-
-<ADDRESS>
-<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
-</ADDRESS>
-</BODY>
-</HTML>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Simple/README_Simple.thy Fri Aug 19 23:58:44 2022 +0200
@@ -0,0 +1,22 @@
+theory README_Simple imports Main
+begin
+
+section \<open>UNITY: Examples Involving Single Programs\<close>
+
+text \<open>
+ The directory presents verification examples that do not involve program
+ composition. They are mostly taken from Misra's 1994 papers on ``New
+ UNITY'':
+
+ \<^item> common meeting time (\<^file>\<open>Common.thy\<close>)
+ \<^item> the token ring (\<^file>\<open>Token.thy\<close>)
+ \<^item> the communication network (\<^file>\<open>Network.thy\<close>)
+ \<^item> the lift controller (a standard benchmark) (\<^file>\<open>Lift.thy\<close>)
+ \<^item> a mutual exclusion algorithm (\<^file>\<open>Mutex.thy\<close>)
+ \<^item> \<open>n\<close>-process deadlock (\<^file>\<open>Deadlock.thy\<close>)
+ \<^item> unordered channel (\<^file>\<open>Channel.thy\<close>)
+ \<^item> reachability in directed graphs (section 6.4 of the book)
+ (\<^file>\<open>Reach.thy\<close> and \<^file>\<open>Reachability.thy\<close>>
+\<close>
+
+end
--- a/src/Pure/Thy/presentation.scala Fri Aug 19 21:43:06 2022 +0200
+++ b/src/Pure/Thy/presentation.scala Fri Aug 19 23:58:44 2022 +0200
@@ -433,7 +433,6 @@
/* present session */
val session_graph_path: Path = Path.explode("session_graph.pdf")
- val readme_path: Path = Path.explode("README.html")
def session_html(
html_context: HTML_Context,
@@ -473,19 +472,11 @@
val deps_link =
HTML.link(session_graph_path, HTML.text("theory dependencies"))
- val readme_links =
- if ((session_info.dir + readme_path).is_file) {
- Isabelle_System.copy_file(session_info.dir + readme_path, session_dir + readme_path)
- List(HTML.link(readme_path, HTML.text("README")))
- }
- else Nil
-
val document_links =
documents.map(doc => HTML.link(doc.path.pdf, HTML.text(doc.name)))
Library.separate(HTML.break ::: HTML.nl,
- (deps_link :: readme_links ::: document_links).
- map(link => HTML.text("View ") ::: List(link))).flatten
+ (deps_link :: document_links).map(link => HTML.text("View ") ::: List(link))).flatten
}
def present_theory(theory_name: String): Option[XML.Body] = {
--- a/src/Pure/Thy/sessions.scala Fri Aug 19 21:43:06 2022 +0200
+++ b/src/Pure/Thy/sessions.scala Fri Aug 19 23:58:44 2022 +0200
@@ -34,7 +34,7 @@
def exclude_session(name: String): Boolean = name == "" || name == DRAFT
def exclude_theory(name: String): Boolean =
- name == root_name || name == "README" || name == "index" || name == "bib"
+ name == root_name || name == "index" || name == "bib"
/* ROOTS file format */