Manual/Guide/guide.tex

2 % HOL Manual LaTeX Source: notes for authors of reference manual
39    \setlength{\unitlength}{1mm}           % unit of length = 1mm
59 This note describes the organization of the \HOL\ documentation and the
61 reference manual and how to write documentation for libraries.  All authors of
63 carefully before starting to write.  General users of the system may find the
64 beginning sections of this note useful when they wish to typeset the \HOL\
67 \section{Structure of the HOL documentation}
69 The \HOL\ system documentation consists of three volumes:
74 system. This is intended to be the first item read by new users of \HOL\ and
75 provides a self-study introduction to the structure and use of the system.
78 and description of the \HOL\ system, and as an advanced guide for users with
79 some prior experience of the system.
81 \item \REFERENCE, which provides full reference documentation in the form of
88 speaking, part of the \HOL\ manual set, but which is also described in this
93 \item \LIBRARIES. This consists of stand-alone documentation for each of the
99 contributors of the coresponding \HOL\ system libraries.
101 \section{Structure of the documentation directories}
103 Most of the \LaTeX\ sources for \HOL\ system documentation reside in the
104 subdirectory {\tt Manual} of the main \HOL\ distribution directory.  Certain
106 reason for this and for the organization of these files is described later in
107 this document.  For similar reasons, also explained later, much of the
115 of the documentation.
118 of the documentation.
121 of the documentation.
124 of the documentation.
127 for all volumes of the manual.
138 \noindent Each of these subdirectories contains a {\tt READ-ME} file explaining
139 its contents.  Authors working on parts of the \HOL\ documentation in these
144 Each volume of the \HOL\ documentation is typeset using \LaTeX.  More
146 2.09 of 7 Dec 1989, based on \TeX, the C version 3.0. Building the
156 The following sections describe how to obtain typeset versions of each of the
157 four volumes of the \HOL\ system documentation.
159 \subsection{Choice of paper size}
165 Before typesetting any part of the documentation, the choice of paper size must
167 of this file there is the declaration of a \LaTeX\ boolean flag `{\tt Afour}'
176 volumes of the \HOL\ documentation with a single command. When working in the
178 versions of the documentation from scratch.  Note that the desired paper size
197 versions of the cover pages for the manual volumes.  All these documents are
199 that some of them are rather long, and therefore not lightly to be printed.
204 \TUTORIAL\ volume of the \HOL\ documentation.  Working in the {\tt Tutorial}
209 \item Type `{\tt make clean}' to remove all traces of previous executions of
216 scratch, running it through \latex\ twice to ensure consistency of the
222 guarantee that various forms of reference (i.e.\ citataions, page references,
223 entries in the table of contents and so on) are consistent.  The command `{\tt
233 \DESCRIPTION\ volume of the \HOL\ documentation.  Working in the {\tt
239 \item Type `{\tt make clean}' to remove all traces of previous executions of
251 scratch, running it through \latex\ twice to ensure consistency of the
257 various forms of reference are consistent.  The command `{\tt make
270 individual steps required in this process.  For a full description of the {\tt
280 to ensure consistency of the references and the index.
291 {\tt Manual} subdirectory {\it of the relevant library directory} and typing
293 one of the main \HOL\ manuals.
315 \item {\small DVI2PS}: name of the {\small DVI} to PostScript converter.
325 \item Type `{\tt make clean}' to remove all traces of previous executions of
336 be able to understand the \TeX\ psfig macros.  We supply a version of
340 \section{Structure of the reference manual}
347 and terms of the \HOL\ logic, for setting up theories, and for using the
349 tacticals.  The arrangement of this chapter is strictly alphabetical.
353 sections, based on the `subject matter' of the theorems.  The sections
354 describing groups of theorems more or less mirror the \HOL\ theories that
359 \section{Structure of the reference manual directory}
366 A specification of the format of \id\doc\ files and an explanation of how they
378 The source files for the manual are in the following subdirectories of the
394 further subdirectories.  These correspond to a classification of built-in
402    {\tt axioms}         & axioms of the \HOL\ logic \\
426 \section{Generation of the LaTeX source}
438 \latex\ source text of the documentation on the identifier \id\ in the file
441 to generate chapter 1 of the \REFERENCE\ manual.
464 guarantee that the index is consistent with the body of the text. Step \bnum{3}
465 may, of course, be omitted until a final typeset version, complete with index,
473 To facilitate the debugging of individual manual entries (\ie\ individual \doc\
501 mktex} itself.  Furthermore, {\tt mktex} makes use of the {\tt sed} script {\tt
503 subdirectory {\tt bin} of the directory in which {\tt mktex} is run.
505 Because of these pathname dependencies, it is intended that individual authors
506 working on the reference manual entries will create their own versions of {\tt
510 \section{The format of {\tt .doc} files}
516 conventions adopted for the form and content of reference manual entries in
528 respectively.  The format of \doc\ files for theorems is the simpler (and more
529 rigid) of the two, so it is explained first.
531 \subsection{The format of {\tt .doc} files for theorems}\label{thsec}
533 The format of \doc\ files for theorems is simple.  For each theorem, there is
537 The format of this \doc\ file is as shown below:
553 \item the two occurrences of \vsp\ are {\it required\/} single spaces,
555 \item \meta{thmname} is the name of the theorem (as discussed above),
557 \item \meta{thyname} is the name of the theory in which the theorem is stored,
560 {\small\verb!\ENDTHEOREM!} are the ascii representation of the theorem in
565 \noindent No indentation should be added to the text of the theorem as printed
576 \noindent The meaning of this theorem is clear only when it is known that
577 \ml{f} and \ml{g} are functions that yield values of type \ml{one}.  For
578 theorems of this kind, the documentation should contain the result of
595 \noindent That is, the string `{\small\verb!\none!}' takes the place of the
659 of them.  The two functions are
668 \noindent The first takes a list of string-theorem pairs and writes
670 does this for all of the axioms, theorems and definitions of the
673 \subsection{The format of {\tt .doc} files for other identifiers}
676 In this section, the format and content of \doc\ files for \ML\ identifiers
678 the names of built-in \ML\ functions.  For each identifier \meta{name}, there
683 The general format of a \doc\ file is shown in Figure~\ref{doc-fig}.  The file
684 has several fields, which must appear in the order shown below (though some of
702 The format and content of each of these fields is explained in detail in the
749 \item the three occurrences of \vsp\ are {\it required\/} single spaces,
751 \item \meta{type} is the type of the identifier being documented, usually
783 should be used in place of {\small\verb!\TYPE!}, and all other conventions
799 be misleading as to the nature of the \ML\ function in question.  For example,
800 the type of {\small\verb!AP_THM!} is shown by the system as
811   \item Appearance of {\small\verb!goal!} when a
815   \item Appearance of {\small\verb!conv!} when a {\small\verb!term -> thm!} is
817         naturally thought of as a conversion. {\small\verb!ASSUME!} at
827 typechecked, for example `{\tt *.doc}'. The following example shows the form of
849 consists of a line containing only the keyword `{\small\verb!\SYNOPSIS!}',
850 followed by a {\it brief\/} description of the \ML\ identifier being
851 documented. The text of this description should start on the line immediately
853 exactly one blank line between the text of the synopsis (which is indicated by
854 three dots in Figure~\ref{doc-fig}) and the keyword of the field that
857 The synopsis should consist of at most one or two short sentences (or phrases)
858 which provide a concise but accurate indication of the purpose or function of
859 the \ML\ identifier being documented.  The aim of the synopsis is not to give
864 person singular present tense, for example ``Solves any goal of the form
866 corresponding to \ldots''. Consistency in this regard makes reading a lot of
883 This field is optional. It is intended simply to provide a list of relevant
885 when you cannot remember the name, but do know the kind of thing you are
903 followed by a single space and the name of the library. For example:
911 The {\small\verb!\DESCRIBE!} field consists of a line containing only the
912 keyword `{\small\verb!\DESCRIBE!}', followed by a full description of the
916 {\small\verb!\SYNOPSIS!} field.  The text of the description should start on
919 the text of the description (which is indicated by three dots in
920 Figure~\ref{doc-fig}) and the keyword of the field that follows.
922 The aim of the {\small\verb!\DESCRIBE!} field is to give a complete and
923 accurate specification of what the \ML\ function\footnote{\dots or other \ML\
924 data object, but the vast majority of manual entries are for functions.} being
929 question (this belongs under {\small\verb!\USES!}).  Comments of a general
934 {\small\verb!REPEAT!} and {\small\verb!ORELSE!}).  But a description of
935 failure due to incorrect use of the function (e.g.\ applying
947 conclusion is alpha-convertible to the conclusion of {th}.
952 \noindent The use of the braces `{\small\verb!{!}' and  `{\small\verb!}!}' in
957 The {\small\verb!\FAILURE!} field consists of a line containing only the
959 specification of the conditions under which evaluation can fail when the \ML\
961 required, even when the function being described cannot fail.  The text of the
964 between the text of this specification (which is indicated by three dots in
965 Figure~\ref{doc-fig}) and the keyword of the field that follows.
971 of the form returned by the built-in function
974 however, a feature of the way {\small\verb!INDUCT_THEN!} is implemented that
976 theorems whose form is not precisely that of a theorem proved by
980 of the correct form, but `may' fail on other theorems. When the function being
991 conclusion of the supplied theorem {th}.
996 \noindent The use of the braces `{\small\verb!{!}' and  `{\small\verb!}!}' in
1001 The {\small\verb!\EXAMPLE!} field consists of a line containing only the
1003 examples of the use of the \ML\ identifier being documented.  The text of the
1006 text of this specification (which is indicated by three dots in
1007 Figure~\ref{doc-fig}) and the keyword of the field that follows.
1019 description of what is going on. An example is given below:
1039 The {\small\verb!\USES!} field consists of a line containing only the keyword
1040 `{\small\verb!\USES!}', followed by a statement of common or typical uses of
1041 the \ML\ identifier being documented.  The text of the example should start on
1043 There must be exactly one blank line between the text of this specification
1044 (which is indicated by three dots in Figure~\ref{doc-fig}) and the keyword of
1050 needs to be said about the uses of a function.  A {\small\verb!\USES!} field
1060 Specializes the leading universally-quantified variable of a theorem to a
1085 Obtaining specific instances of already proved theorems; implementing
1091 \noindent But, in the case of {\small\verb!SPEC!}, no {\small\verb!\USES!}
1093 still a paraphrase of the function of {\small\verb!SPEC!}; the second
1095 part of this kind of activity).
1099 The {\small\verb!\COMMENTS!} field consists of a line containing only the
1102 elsewhere.  The text of the example should start on the line immediately
1104 exactly one blank line between the text of this specification (which is
1105 indicated by three dots in Figure~\ref{doc-fig}) and the keyword of the field
1109 remarks about implementation matters, promises of future reimplementation,
1114 composition of validity checking steps simply follows the composition of the
1120 The {\small\verb!\SEEALSO!} field consists of a line containing only the
1121 keyword `{\small\verb!\SEEALSO!}', followed by list of manual entries
1122 relevant to the \ML\ identifier being documented.  The list of related entries
1124 `{\small\verb!\EXAMPLE!}'.  The list itself should consist of a sequence of
1128 keyword of the field that follows.
1150 The {\small\verb!\ENDDOC!} line, which consists of a single line containing
1151 only the keyword `{\small\verb!\ENDDOC!}', signals the end of a manual entry.
1158 {\small\verb!\COMMENTS!} fields of a \doc\ file all consist of a keyword line
1159 followed by general text.  Within this text, only two kinds of typesetting
1160 command are allowed: `{\small\verb%\noindent%}\vsp' at the beginning of a line,
1165 \item  `{\small\verb%\noindent%}\vsp' at the beginning of a line prevents
1166 indentation of that line.
1174 \item A sequence of lines of the following form, where `{\small\verb|{|}' and
1175 `{\small\verb|}|}' occur at the beginning of otherwise empty lines:
1190 of text and the open bracket `{\small\verb|{|}' and no blank line between the
1191 closing bracket `{\small\verb|}|}' and the following line of text (even if
1192 otherwise required by virtue of being the last line in a field).  Here is an
1193 example of the correct use of the displayed verbatim format:
1203 solve the current goal.  This kind of tactic is very useful when dealing with
1208 \noindent Here, there are three spaces manually inserted at the beginning of
1212 The following exception may made to the general rule of indenting displayed
1232 by a commentary of ordinary text.
1237 the text of the various fields in a reference manual entry, the following
1247 The preferred terms for the parts of theorems, goals, implications
1256 \noindent It is permissible to use {\em hypotheses} instead of {\em
1258 The overloading of the word {\em conclusion} is unfortunate, but no viable
1263 Substitution of term {\tt u} for a variable {\tt x} in term {\tt t} should be
1268 t[u1,...,un/t1,...,tn]}. The use of {\tt t[u1/t1,...,un/tn]} should be avoided
1269 because of the scope for ambiguity.
1286 \noindent Assumption lists of goals should be shown, even when they do not play
1293 Alpha-convertibility of terms should not, except in obvious special cases like
1296 classes of terms. If important, these issues can be mentioned in the
1299 The union (of assumption lists) should be written as an infix lowercase {\tt
1302 consideration, it can be discussed separately.  The addition or subtraction of
1308 The following formats should be followed for rule-style specifications of
1326 \item Use a line consisting of minus-signs for inference rules, and a line
1327 consisting of equal-signs for tactics.
1329 \item The line should overlap by exactly one space on either side of the wider
1330 of the lines of text above and below.
1332 \item The other line of text should be centred within the rule bar as closely
1335 \item Above the line put the theorem(s) or goal prior to application of the
1336 rule or tactic (may be empty in the case of theorems).
1339 application of the rule or theorem. In the case of a tactic which completely
1343 \item To the right of the line, after 2 spaces, write the name of the rule or
1348 in the top line of the rule. Sometimes this convention does not make manifest
1349 the required order of the arguments; in this case the arguments which appear in
1350 the rule line should be restated (see the example of {\small\verb!AP_THM!}
1357 Some examples of rule notation as described above are:
1384 \subsection{Format of a {\tt .doc} file}
1419 \caption{Format of a \doc\ file.\label{doc-fig}}
1424 \subsection{Example of a {\tt .doc} file}
1441 conclusion is alpha-convertible to the conclusion of {th}.
1445 conclusion of the supplied theorem {th}.
1471 \subsection{Example of a typeset {\tt .doc} file}
1485 conclusion is alpha-convertible to the conclusion of {\small\verb%th%}.
1489 conclusion of the supplied theorem {\small\verb%th%}.
1548 \item The name of the library
1549 \item A brief description of what the library does (not more than a few lines)
1556 \item{\tt help} A help directory, containing one or both of the following
1567 giving the name of the relevant library.
1585 version of the library documentation. It should include at least the following
1591 files produced by a run of \latex.
1607 usage, probably mentioning some of the \ML\ functions and/or theorems provided,
1611 the reference section of \ML\ functions. Apart from the library name, this can
1615 the reference section of theorems. Apart from the library name, this can again
1618 \item{\tt references.tex}: a standard \latex\ list of any references made in the