# HG changeset patch # User wenzelm # Date 1011025420 -3600 # Node ID cc59ceb0bcb4cde477d47419548ecbbb1bb8b70d # Parent 892af6538f3d07e3d2a53c5d1cde03dd04f32ee1 updated; diff -r 892af6538f3d -r cc59ceb0bcb4 doc-src/TutorialI/Documents/document/Documents.tex --- a/doc-src/TutorialI/Documents/document/Documents.tex Mon Jan 14 17:23:35 2002 +0100 +++ b/doc-src/TutorialI/Documents/document/Documents.tex Mon Jan 14 17:23:40 2002 +0100 @@ -58,22 +58,23 @@ as \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}}; together with plain prefix application this turns \isa{xor\ A} into \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ A}. - \medskip The keyword \isakeyword{infixl} specifies an infix operator - that is nested to the \emph{left}: in iterated applications the more - complex expression appears on the left-hand side: \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} stands for \isa{{\isacharparenleft}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B{\isacharparenright}\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C}. Similarly, - \isakeyword{infixr} specifies to nesting to the \emph{right}, - reading \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} as \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}. In - contrast, a \emph{non-oriented} declaration via \isakeyword{infix} - would render \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} illegal, but demand explicit - parentheses to indicate the intended grouping. + \medskip The keyword \isakeyword{infixl} seen above specifies an + infix operator that is nested to the \emph{left}: in iterated + applications the more complex expression appears on the left-hand + side, \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} stands for \isa{{\isacharparenleft}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B{\isacharparenright}\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C}. + Similarly, \isakeyword{infixr} specifies nesting to the + \emph{right}, reading \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} as \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}. In contrast, a \emph{non-oriented} declaration via + \isakeyword{infix} would render \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} illegal, but + demand explicit parentheses to indicate the intended grouping. - The string \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}} in the above annotation refers to - the concrete syntax to represent the operator (a literal token), - while the number \isa{{\isadigit{6}}{\isadigit{0}}} determines the precedence of the - construct (i.e.\ the syntactic priorities of the arguments and - result). As it happens, Isabelle/HOL already uses up many popular - combinations of ASCII symbols for its own use, including both \isa{{\isacharplus}} and \isa{{\isacharplus}{\isacharplus}}. Slightly more awkward combinations like the - present \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}} tend to be available for user extensions. + The string \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}} in our annotation refers to the + concrete syntax to represent the operator (a literal token), while + the number \isa{{\isadigit{6}}{\isadigit{0}}} determines the precedence of the construct + (i.e.\ the syntactic priorities of the arguments and result). As it + happens, Isabelle/HOL already uses up many popular combinations of + ASCII symbols for its own use, including both \isa{{\isacharplus}} and \isa{{\isacharplus}{\isacharplus}}. As a rule of thumb, more awkward character combinations are + more likely to be still available for user extensions, just as our + present \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}}. Operator precedence also needs some special considerations. The admissible range is 0--1000. Very low or high priorities are @@ -143,11 +144,12 @@ just type a named entity \verb,\,\verb,, by hand; the display will be adapted immediately after continuing input. - \medskip A slightly more refined scheme is to provide alternative - syntax via the \bfindex{print mode} concept of Isabelle (see also - \cite{isabelle-ref}). By convention, the mode of ``$xsymbols$'' is - enabled whenever Proof~General's X-Symbol mode (or {\LaTeX} output) - is active. Now consider the following hybrid declaration of \isa{xor}.% + \medskip A slightly more refined scheme of providing alternative + syntax forms uses the \bfindex{print mode} concept of Isabelle (see + also \cite{isabelle-ref}). By convention, the mode of + ``$xsymbols$'' is enabled whenever Proof~General's X-Symbol mode or + {\LaTeX} output is active. Now consider the following hybrid + declaration of \isa{xor}:% \end{isamarkuptext}% \isamarkuptrue% \isamarkupfalse% @@ -164,12 +166,9 @@ \begin{isamarkuptext}% The \commdx{syntax} command introduced here acts like \isakeyword{consts}, but without declaring a logical constant. The - print mode specification (here \isa{{\isacharparenleft}xsymbols{\isacharparenright}}) limits the - effect of the syntax annotation concerning output; that alternative - production available for input invariably. Also note that the type - declaration in \isakeyword{syntax} merely serves for syntactic - purposes, and is \emph{not} checked for consistency with the real - constant. + print mode specification of \isakeyword{syntax}, here \isa{{\isacharparenleft}xsymbols{\isacharparenright}}, is optional. Also note that its type merely serves + for syntactic purposes, and is \emph{not} checked for consistency + with the real constant. \medskip We may now write \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} or \isa{A\ {\isasymoplus}\ B} in input, while output uses the nicer syntax of $xsymbols$, provided @@ -201,7 +200,7 @@ \noindent Here the mixfix annotations on the rightmost column happen to consist of a single Isabelle symbol each: \verb,\,\verb,,, \verb,\,\verb,,, \verb,\,\verb,,, and \verb,$,. Recall - that a constructor like \isa{Euro} actually is a function \isa{nat\ {\isasymRightarrow}\ currency}. An expression like \isa{Euro\ {\isadigit{1}}{\isadigit{0}}} will be + that a constructor like \isa{Euro} actually is a function \isa{nat\ {\isasymRightarrow}\ currency}. The expression \isa{Euro\ {\isadigit{1}}{\isadigit{0}}} will be printed as \isa{{\isasymeuro}\ {\isadigit{1}}{\isadigit{0}}}; only the head of the application is subject to our concrete syntax. This rather simple form already achieves conformance with notational standards of the European @@ -232,8 +231,8 @@ \cite{isabelle-ref}. \medskip A typical example of syntax translations is to decorate - relational expressions (i.e.\ set-membership of tuples) with nice - symbolic notation, such as \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} versus \isa{x\ {\isasymapprox}\ y}.% + relational expressions (set-membership of tuples) with symbolic + notation, e.g.\ \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} versus \isa{x\ {\isasymapprox}\ y}.% \end{isamarkuptext}% \isamarkuptrue% \isacommand{consts}\isanewline @@ -296,19 +295,23 @@ as a front-end to {\LaTeX}. After checking specifications and proofs formally, the theory sources are turned into typesetting instructions in a schematic manner. This enables users to write - authentic reports on theory developments with little effort, where - most consistency checks are handled by the system. + authentic reports on theory developments with little effort --- many + technical consistency checks are handled by the system. Here is an example to illustrate the idea of Isabelle document - preparation. - - \bigskip The following datatype definition of \isa{{\isacharprime}a\ bintree} - models binary trees with nodes being decorated by elements of type - \isa{{\isacharprime}a}.% + preparation.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\begin{quotation} +% +\begin{isamarkuptext}% +The following datatype definition of \isa{{\isacharprime}a\ bintree} models + binary trees with nodes being decorated by elements of type \isa{{\isacharprime}a}.% \end{isamarkuptext}% \isamarkuptrue% \isacommand{datatype}\ {\isacharprime}a\ bintree\ {\isacharequal}\isanewline -\ \ Leaf\ {\isacharbar}\ Branch\ {\isacharprime}a\ \ {\isachardoublequote}{\isacharprime}a\ bintree{\isachardoublequote}\ \ {\isachardoublequote}{\isacharprime}a\ bintree{\isachardoublequote}\isamarkupfalse% +\ \ \ \ \ Leaf\ {\isacharbar}\ Branch\ {\isacharprime}a\ \ {\isachardoublequote}{\isacharprime}a\ bintree{\isachardoublequote}\ \ {\isachardoublequote}{\isacharprime}a\ bintree{\isachardoublequote}\isamarkupfalse% % \begin{isamarkuptext}% \noindent The datatype induction rule generated here is of the form @@ -317,10 +320,15 @@ \isaindent{\ \ \ }{\isasymAnd}a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isachardot}\isanewline \isaindent{\ \ \ \ \ \ }{\isasymlbrakk}P\ bintree{\isadigit{1}}{\isacharsemicolon}\ P\ bintree{\isadigit{2}}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Branch\ a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isacharparenright}{\isasymrbrakk}\isanewline {\isasymLongrightarrow}\ P\ bintree% -\end{isabelle} - - \bigskip The above document output has been produced by the - following theory specification: +\end{isabelle}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\end{quotation} +% +\begin{isamarkuptext}% +The above document output has been produced by the following theory + specification: \begin{ttbox} text {\ttlbrace}* @@ -338,11 +346,11 @@ *{\ttrbrace} \end{ttbox} - Here we have augmented the theory by formal comments (via - \isakeyword{text} blocks). The informal parts may again refer to - formal entities by means of ``antiquotations'' (such as + \noindent Here we have augmented the theory by formal comments + (using \isakeyword{text} blocks). The informal parts may again + refer to formal entities by means of ``antiquotations'' (such as \texttt{\at}\verb,{text "'a bintree"}, or - \texttt{\at}\verb,{typ 'a},; see also \S\ref{sec:doc-prep-text}.% + \texttt{\at}\verb,{typ 'a},), see also \S\ref{sec:doc-prep-text}.% \end{isamarkuptext}% \isamarkuptrue% % @@ -382,8 +390,7 @@ \texttt{IsaMakefile} \cite{isabelle-sys}.} \medskip The detailed arrangement of the session sources is as - follows. This may be ignored in the beginning, but some of these - files need to be edited in realistic applications. + follows. \begin{itemize} @@ -403,13 +410,13 @@ document (\verb,\documentclass, etc.), and to include the generated files $T@i$\texttt{.tex} for each theory. Isabelle will generate a file \texttt{session.tex} holding {\LaTeX} commands to include all - generated theory output files in topologically sorted order. So - \verb,\input{session}, in \texttt{root.tex} does the job in most - situations. + generated theory output files in topologically sorted order, so + \verb,\input{session}, in the body of \texttt{root.tex} does the job + in most situations. \item \texttt{IsaMakefile} holds appropriate dependencies and invocations of Isabelle tools to control the batch job. In fact, - several sessions may be controlled by the same \texttt{IsaMakefile}. + several sessions may be managed by the same \texttt{IsaMakefile}. See also \cite{isabelle-sys} for further details, especially on \texttt{isatool usedir} and \texttt{isatool make}. @@ -430,16 +437,16 @@ distributed with Isabelle. Further packages may be required in particular applications, e.g.\ for unusual mathematical symbols. - \medskip Additional files for the {\LaTeX} stage may be put into the - \texttt{MySession/document} directory, too. In particular, adding - \texttt{root.bib} here (with that specific name) causes an automatic - run of \texttt{bibtex} to process a bibliographic database; see also - \texttt{isatool document} covered in \cite{isabelle-sys}. + \medskip Any additional files for the {\LaTeX} stage go into the + \texttt{MySession/document} directory as well. In particular, + adding \texttt{root.bib} (with that specific name) causes an + automatic run of \texttt{bibtex} to process a bibliographic + database; see also \texttt{isatool document} in \cite{isabelle-sys}. \medskip Any failure of the document preparation phase in an Isabelle batch session leaves the generated sources in their target location (as pointed out by the accompanied error message). This - enables users to trace {\LaTeX} problems with the target files at + enables users to trace {\LaTeX} problems with the generated files at hand.% \end{isamarkuptext}% \isamarkuptrue% @@ -474,8 +481,8 @@ \medskip From the Isabelle perspective, each markup command takes a single - $text$ argument (delimited by \verb,",\dots\verb,", or - \verb,{,\verb,*,~\dots~\verb,*,\verb,},). After stripping any + $text$ argument (delimited by \verb,",~\isa{{\isasymdots}}~\verb,", or + \verb,{,\verb,*,~\isa{{\isasymdots}}~\verb,*,\verb,},). After stripping any surrounding white space, the argument is passed to a {\LaTeX} macro \verb,\isamarkupXYZ, for any command \isakeyword{XYZ}. These macros are defined in \verb,isabelle.sty, according to the meaning given in @@ -545,18 +552,18 @@ % \begin{isamarkuptext}% Isabelle \bfindex{source comments}, which are of the form - \verb,(,\verb,*,~\dots~\verb,*,\verb,),, essentially act like white - space and do not really contribute to the content. They mainly - serve technical purposes to mark certain oddities in the raw input - text. In contrast, \bfindex{formal comments} are portions of text - that are associated with formal Isabelle/Isar commands + \verb,(,\verb,*,~\isa{{\isasymdots}}~\verb,*,\verb,),, essentially act like + white space and do not really contribute to the content. They + mainly serve technical purposes to mark certain oddities in the raw + input text. In contrast, \bfindex{formal comments} are portions of + text that are associated with formal Isabelle/Isar commands (\bfindex{marginal comments}), or as standalone paragraphs within a theory or proof context (\bfindex{text blocks}). \medskip Marginal comments are part of each command's concrete syntax \cite{isabelle-ref}; the common form is ``\verb,--,~$text$'' - where $text$ is delimited by \verb,",\dots\verb,", or - \verb,{,\verb,*,~\dots~\verb,*,\verb,}, as before. Multiple + where $text$ is delimited by \verb,",\isa{{\isasymdots}}\verb,", or + \verb,{,\verb,*,~\isa{{\isasymdots}}~\verb,*,\verb,}, as before. Multiple marginal comments may be given at the same time. Here is a simple example:% \end{isamarkuptext}% @@ -599,7 +606,11 @@ \verb,isamarkuptxt,, respectively (via \verb,\renewenvironment,) The text style of the body is determined by \verb,\isastyletext, and \verb,\isastyletxt,; the default setup uses a smaller font within - proofs. + proofs. This may be changed as follows: + +\begin{verbatim} + \renewcommand{\isastyletxt}{\isastyletext} +\end{verbatim} \medskip The $text$ part of each of the various markup commands considered so far essentially inserts \emph{quoted material} into a @@ -607,10 +618,10 @@ \bfindex{antiquotation} is again a formal object embedded into such an informal portion. The interpretation of antiquotations is limited to some well-formedness checks, with the result being pretty - printed to the resulting document. So quoted text blocks together - with antiquotations provide very useful means to reference formal - entities with good confidence in getting the technical details right - (especially syntax and types). + printed to the resulting document. Quoted text blocks together with + antiquotations provide very useful means to reference formal + entities, with good confidence in getting the technical details + right (especially syntax and types). The general syntax of antiquotations is as follows: \texttt{{\at}{\ttlbrace}$name$ $arguments${\ttrbrace}}, or @@ -658,7 +669,7 @@ \texttt{\at}\verb,{prop [source],~$\phi$\verb,}, & check proposition $\phi$, print its input \\ \texttt{\at}\verb,{thm,~$a$\verb,}, & print fact $a$ \\ \texttt{\at}\verb,{thm,~$a$~\verb,[no_vars]}, & print fact $a$, fixing schematic variables \\ - \texttt{\at}\verb,{thm [source],~$a$\verb,}, & check availability of fact, print name $a$ \\ + \texttt{\at}\verb,{thm [source],~$a$\verb,}, & check availability of fact $a$, print its name \\ \texttt{\at}\verb,{text,~$s$\verb,}, & print uninterpreted text $s$ \\ \end{tabular} @@ -702,25 +713,25 @@ \begin{enumerate} \item 7-bit ASCII characters: letters \texttt{A\dots Z} and - \texttt{a\dots z} are output verbatim, digits are passed as an + \texttt{a\dots z} are output directly, digits are passed as an argument to the \verb,\isadigit, macro, other characters are replaced by specifically named macros of the form \verb,\isacharXYZ,. - \item Named symbols: \verb,\,\verb,<,$XYZ$\verb,>, become - \verb,{\isasym,$XYZ$\verb,}, each (note the additional braces). + \item Named symbols: \verb,\,\verb,<,$XYZ$\verb,>, is turned into + \verb,{\isasym,$XYZ$\verb,},; note the additional braces. - \item Named control symbols: \verb,{\isasym,$XYZ$\verb,}, become - \verb,\isactrl,$XYZ$ each; subsequent symbols may act as arguments - if the corresponding macro is defined accordingly. + \item Named control symbols: \verb,\,\verb,<^,$XYZ$\verb,>, is + turned into \verb,\isactrl,$XYZ$; subsequent symbols may act as + arguments if the corresponding macro is defined accordingly. \end{enumerate} Users may occasionally wish to give new {\LaTeX} interpretations of named symbols; this merely requires an appropriate definition of - \verb,\,\verb,<,$XYZ$\verb,>, (see \texttt{isabelle.sty} for working - examples). Control symbols are slightly more difficult to get - right, though. + \verb,\isasym,$XYZ$\verb,, for \verb,\,\verb,<,$XYZ$\verb,>, (see + \texttt{isabelle.sty} for working examples). Control symbols are + slightly more difficult to get right, though. \medskip The \verb,\isabellestyle, macro provides a high-level interface to tune the general appearance of individual symbols. For @@ -742,10 +753,10 @@ The generated \texttt{session.tex} will include all of these in order of appearance, which in turn gets included by the standard \texttt{root.tex}. Certainly one may change the order or suppress - unwanted theories by ignoring \texttt{session.tex} and include - individual files in \texttt{root.tex} by hand. On the other hand, - such an arrangement requires additional maintenance chores whenever - the collection of theories changes. + unwanted theories by ignoring \texttt{session.tex} and load + individual files directly in \texttt{root.tex}. On the other hand, + such an arrangement requires additional maintenance whenever the + collection of theories changes. Alternatively, one may tune the theory loading process in \texttt{ROOT.ML} itself: traversal of the theory dependency graph @@ -765,9 +776,9 @@ \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and \verb,(,\verb,*,\verb,>,\verb,*,\verb,), may be included in the text. Only the document preparation system is affected, the formal - checking the theory is performed unchanged. + checking of the theory is performed unchanged. - In the following example we suppress the slightly formalistic + In the subsequent example we suppress the slightly formalistic \isakeyword{theory} + \isakeyword{end} surroundings a theory. \medskip @@ -785,9 +796,9 @@ \medskip Text may be suppressed in a fine-grained manner. We may even drop - vital parts of a formal proof, pretending that things have been - simpler than in reality. For example, the following ``fully - automatic'' proof is actually a fake:% + vital parts of a proof, pretending that things have been simpler + than in reality. For example, this ``fully automatic'' proof is + actually a fake:% \end{isamarkuptext}% \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}x\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isacharless}\ x\ {\isacharasterisk}\ x{\isachardoublequote}\isanewline @@ -803,18 +814,18 @@ %(* \medskip Ignoring portions of printed text does demand some care by - the writer. First of all, the writer is responsible not to - obfuscate the underlying formal development in an unduly manner. It - is fairly easy to invalidate the remaining visible text, e.g.\ by - referencing questionable formal items (strange definitions, - arbitrary axioms etc.) that have been hidden from sight beforehand. + the writer. First of all, the user is responsible not to obfuscate + the underlying theory development in an unduly manner. It is fairly + easy to invalidate the visible text, e.g.\ by referencing + questionable formal items (strange definitions, arbitrary axioms + etc.) that have been hidden from sight beforehand. - Authentic reports of formal theories, say as part of a library, - should refrain from suppressing parts of the text at all. Other - users may need the full information for their own derivative work. - If a particular formalization appears inadequate for general public - coverage, it is often more appropriate to think of a better way in - the first place. + Authentic reports of Isabelle/Isar theories, say as part of a + library, should refrain from suppressing parts of the text at all. + Other users may need the full information for their own derivative + work. If a particular formalization appears inadequate for general + public coverage, it is often more appropriate to think of a better + way in the first place. \medskip Some technical subtleties of the \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),