+
+end
diff -r 95d7459e5bc0 -r b6589c8ccadd src/HOL/Hoare/README.html
--- 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 @@
-
-
-
-
-
-
- HOL/Hoare/ReadMe
-
-
-
-
-Hoare Logic for a Simple WHILE Language
-
-Language and logic
-
-This directory contains an implementation of Hoare logic for a simple WHILE
-language. The constructs are
-
-- SKIP
-
- _ := _
-
- _ ; _
-
- IF _ THEN _ ELSE _ FI
-
- WHILE _ INV {_} DO _ OD
-
-Note that each WHILE-loop must be annotated with an invariant.
-
-
-After loading theory Hoare, you can state goals of the form
-
-VARS x y ... {P} prog {Q}
-
-where prog is a program in the above language, P is the
-precondition, Q the postcondition, and x y ... is the
-list of all program variables in prog. The latter list must
-be nonempty and it must include all variables that occur on the left-hand
-side of an assignment in prog. Example:
-
-VARS x {x = a} x := x+1 {x = a+1}
-
-The (normal) variable a is merely used to record the initial
-value of x 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 vcg for transforming a goal in Hoare logic into an
-equivalent list of verification conditions in HOL:
-
-apply vcg
-
-If you want to simplify the resulting verification conditions at the same
-time:
-
-apply vcg_simp
-
-which, given the example goal above, solves it completely. For further
-examples see Examples.
-
-
-IMPORTANT:
-This is a logic of partial correctness. You can only prove that your program
-does the right thing if it terminates, but not that it
-terminates.
-A logic of total correctness is also provided and described below.
-
-
Total correctness
-
-To prove termination, each WHILE-loop must be annotated with a variant:
-
-- WHILE _ INV {_} VAR {_} DO _ OD
-
-A variant is an expression with type nat, which may use program
-variables and normal variables.
-
-
-A total-correctness goal has the form
-
-VARS x y ... [P] prog [Q]
-
-enclosing the pre- and postcondition in square brackets.
-
-
-Methods vcg_tc and vcg_tc_simp 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.
-
-
Notes on the implementation
-
-The implementation loosely follows
-
-Mike Gordon.
-Mechanizing Programming Logics in Higher Order Logic.
-University of Cambridge, Computer Laboratory, TR 145, 1988.
-
-published as
-
-Mike Gordon.
-Mechanizing Programming Logics in Higher Order Logic.
-In
-Current Trends in Hardware Verification and Automated Theorem Proving
-,
-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.
-Mechanizing Some Advanced Refinement Concepts.
-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.
-
-
diff -r 95d7459e5bc0 -r b6589c8ccadd src/HOL/Hoare/README.thy
--- /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 \Hoare Logic for a Simple WHILE Language\
+
+subsection \Language and logic\
+
+text \
+ This directory contains an implementation of Hoare logic for a simple WHILE
+ language. The constructs are
+
+ \<^item> \<^verbatim>\SKIP\
+ \<^item> \<^verbatim>\_ := _\
+ \<^item> \<^verbatim>\_ ; _\
+ \<^item> \<^verbatim>\IF _ THEN _ ELSE _ FI\
+ \<^item> \<^verbatim>\WHILE _ INV {_} DO _ OD\
+
+ Note that each WHILE-loop must be annotated with an invariant.
+
+ Within the context of theory \<^verbatim>\Hoare\, you can state goals of the form
+ @{verbatim [display] \VARS x y ... {P} prog {Q}\}
+ where \<^verbatim>\prog\ is a program in the above language, \<^verbatim>\P\ is the precondition,
+ \<^verbatim>\Q\ the postcondition, and \<^verbatim>\x y ...\ is the list of all \<^emph>\program
+ variables\ in \<^verbatim>\prog\. The latter list must be nonempty and it must include
+ all variables that occur on the left-hand side of an assignment in \<^verbatim>\prog\.
+ Example:
+ @{verbatim [display] \VARS x {x = a} x := x+1 {x = a+1}\}
+ The (normal) variable \<^verbatim>\a\ is merely used to record the initial value of
+ \<^verbatim>\x\ 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>\vcg\ for transforming a goal in Hoare logic into an equivalent list
+ of verification conditions in HOL: \<^theory_text>\apply vcg\
+
+ If you want to simplify the resulting verification conditions at the same
+ time: \<^theory_text>\apply vcg_simp\ which, given the example goal above, solves it
+ completely. For further examples see \<^file>\Examples.thy\.
+
+ \<^bold>\IMPORTANT:\
+ This is a logic of partial correctness. You can only prove that your program
+ does the right thing \<^emph>\if\ it terminates, but not \<^emph>\that\ it terminates. A
+ logic of total correctness is also provided and described below.
+\
+
+
+subsection \Total correctness\
+
+text \
+ To prove termination, each WHILE-loop must be annotated with a variant:
+
+ \<^item> \<^verbatim>\WHILE _ INV {_} VAR {_} DO _ OD\
+
+ A variant is an expression with type \<^verbatim>\nat\, which may use program variables
+ and normal variables.
+
+ A total-correctness goal has the form \<^verbatim>\VARS x y ... [P] prog [Q]\ enclosing
+ the pre- and postcondition in square brackets.
+
+ Methods \<^verbatim>\vcg_tc\ and \<^verbatim>\vcg_tc_simp\ 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.
+\
+
+
+subsection \Notes on the implementation\
+
+text \
+ The implementation loosely follows
+
+ Mike Gordon. \<^emph>\Mechanizing Programming Logics in Higher Order Logic\.
+ University of Cambridge, Computer Laboratory, TR 145, 1988.
+
+ published as
+
+ Mike Gordon. \<^emph>\Mechanizing Programming Logics in Higher Order Logic\. In
+ \<^emph>\Current Trends in Hardware Verification and Automated Theorem Proving\,
+ 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>\Mechanizing Some Advanced Refinement Concepts\. 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.
+\
+
+end
diff -r 95d7459e5bc0 -r b6589c8ccadd src/HOL/Library/README.html
--- 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 @@
-
-
-
-
-
-
- HOL-Library/README
-
-
-
-
-HOL-Library: supplemental theories for main Isabelle/HOL
-
-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.
-
-
-
-- 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 Foobar accompanied by
-Foobar_Examples.
-
-
- Theory names
-
-
- The theory loader name space is flat, 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:
-Foobar_Doobar (this looks best in LaTeX output).
-
-
- 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 foo_bar or
-Foo_Bar (this looks best in LaTeX output).
-
-
- 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.
-
-
- 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 after each
-punctuation character (",", ".", etc.), but none
-before it; do not extra spaces inside of parentheses; do not attempt
-to simulate table markup with spaces, avoid ``hanging'' indentations.
-
-
-
-
-
diff -r 95d7459e5bc0 -r b6589c8ccadd src/HOL/Library/README.thy
--- /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 \HOL-Library: supplemental theories for main Isabelle/HOL\
+
+text \
+ 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>\Foobar.thy\ accompanied by \<^verbatim>\Foobar_Examples.thy\.
+
+ \<^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>\foo_bar\ or \<^verbatim>\Foo_Bar\ (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>\after\ each punctuation character ("\<^verbatim>\,\",
+ "\<^verbatim>\.\", etc.), but none before it; do not extra spaces inside of
+ parentheses; do not attempt to simulate table markup with spaces, avoid
+ ``hanging'' indentations.
+\
+
+end
diff -r 95d7459e5bc0 -r b6589c8ccadd src/HOL/ROOT
--- 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"
diff -r 95d7459e5bc0 -r b6589c8ccadd src/HOL/TLA/README.html
--- 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 @@
-
-
-
-
-
-
- HOL/TLA
-
-
-
-
-TLA: Lamport's Temporal Logic of Actions
-
-TLA
-is a linear-time temporal logic introduced by Leslie Lamport in
-The Temporal Logic of Actions (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:
-
-- Theory Intensional prepares the
- ground by introducing basic syntax for "lifted", possibl-world based
- logics.
-
- Theories Stfun and
- Action represent the state and transition
- level formulas of TLA, evaluated over single states and pairs of
- states.
-
- Theory Init introduces temporal logic
- and defines conversion functions from nontemporal to temporal
- formulas.
-
- Theory TLA axiomatizes proper temporal
- logic.
-
-
-Please consult the
-design notes
-for further information regarding the setup and use of this encoding
-of TLA.
-
-
-The theories are accompanied by a small number of examples:
-
-- Inc: Lamport's increment
- example, a standard TLA benchmark, illustrates an elementary TLA
- proof.
-
- Buffer: a proof that two buffers
- in a row implement a single buffer, uses a simple refinement
- mapping.
-
- Memory: a verification of (the
- untimed part of) Broy and Lamport's RPC-Memory case study,
- more fully explained in LNCS 1169 (the
- TLA
- solution is available separately).
-
-
-
-
-
-Stephan Merz
-
-
-Last modified: Sat Mar 5 00:54:49 CET 2005
-
-
diff -r 95d7459e5bc0 -r b6589c8ccadd src/HOL/TLA/README.thy
--- /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 \TLA: Lamport's Temporal Logic of Actions\
+
+text \
+ TLA \<^url>\http://www.research.digital.com/SRC/personal/Leslie_Lamport/tla/tla.html\
+ is a linear-time temporal logic introduced by Leslie Lamport in \<^emph>\The
+ Temporal Logic of Actions\ (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>\Intensional.thy\ prepares the ground by introducing basic syntax for
+ "lifted", possible-world based logics.
+
+ \<^item> \<^file>\Stfun.thy\ and \<^file>\Action.thy\ represent the state and transition
+ level formulas of TLA, evaluated over single states and pairs of states.
+
+ \<^item> \<^file>\Init.thy\ introduces temporal logic and defines conversion functions
+ from nontemporal to temporal formulas.
+
+ \<^item> \<^file>\TLA.thy\ axiomatizes proper temporal logic.
+
+
+ Please consult the \<^emph>\design notes\
+ \<^url>\http://www.pst.informatik.uni-muenchen.de/~merz/isabelle/IsaTLADesign.ps\
+ 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>\Inc\: Lamport's \<^emph>\increment\ example, a standard TLA benchmark,
+ illustrates an elementary TLA proof.
+
+ \<^item> \<^dir>\Buffer\: a proof that two buffers in a row implement a single buffer,
+ uses a simple refinement mapping.
+
+ \<^item> \<^dir>\Memory\: a verification of (the untimed part of) Broy and Lamport's
+ \<^emph>\RPC-Memory\ case study, more fully explained in LNCS 1169 (the \<^emph>\TLA
+ solution\ is available separately from
+ \<^url>\http://www.pst.informatik.uni-muenchen.de/~merz/papers/RPCMemory.html\).
+\
+
+end
diff -r 95d7459e5bc0 -r b6589c8ccadd src/HOL/UNITY/Comp/README.html
--- 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 @@
-
-
-
-
-
-
- HOL/UNITY/README
-
-
-
-
-UNITY: Examples Involving Program Composition
-
-
-The directory presents verification examples involving program composition.
-They are mostly taken from the works of Chandy, Charpentier and Chandy.
-
-
-
- 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.
-
-
-lcp@cl.cam.ac.uk
-
-
-
diff -r 95d7459e5bc0 -r b6589c8ccadd src/HOL/UNITY/Comp/README_Comp.thy
--- /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 \UNITY: Examples Involving Program Composition\
+
+text \
+ The directory presents verification examples involving program composition.
+ They are mostly taken from the works of Chandy, Charpentier and Chandy.
+
+ \<^item> examples of \<^emph>\universal properties\: the counter (\<^file>\Counter.thy\) and
+ priority system (\<^file>\Priority.thy\)
+ \<^item> the allocation system (\<^file>\Alloc.thy\)
+ \<^item> client implementation (\<^file>\Client.thy\)
+ \<^item> allocator implementation (\<^file>\AllocImpl.thy\)
+ \<^item> the handshake protocol (\<^file>\