# HG changeset patch # User wenzelm # Date 1010424643 -3600 # Node ID a55c066624eba4d51a12f309e084a6a4670e7cde # Parent 2d136f05e1641a53fcef490d74a8fd014eba8566 tuned; diff -r 2d136f05e164 -r a55c066624eb doc-src/TutorialI/Documents/Documents.thy --- a/doc-src/TutorialI/Documents/Documents.thy Mon Jan 07 18:30:31 2002 +0100 +++ b/doc-src/TutorialI/Documents/Documents.thy Mon Jan 07 18:30:43 2002 +0100 @@ -2,22 +2,24 @@ theory Documents = Main: (*>*) +(* FIXME exercises? *) + section {* Concrete Syntax \label{sec:concrete-syntax} *} text {* Concerning Isabelle's ``inner'' language of simply-typed @{text - \}-calculus, the core concept of Isabelle's elaborate infrastructure - for concrete syntax is that of general \bfindex{mixfix annotations}. - Associated with any kind of name and type declaration, mixfixes give - rise both to grammar productions for the parser and output templates - for the pretty printer. + \}-calculus, the core concept of Isabelle's elaborate + infrastructure for concrete syntax is that of general + \bfindex{mixfix annotations}. Associated with any kind of constant + declaration, mixfixes affect both the grammar productions for the + parser and output templates for the pretty printer. In full generality, the whole affair of parser and pretty printer - configuration is rather subtle. Any syntax specifications given by - end-users need to interact properly with the existing setup of - Isabelle/Pure and Isabelle/HOL; see \cite{isabelle-ref} for further - details. It is particularly important to get the precedence of new - syntactic constructs right, avoiding ambiguities with existing + configuration is rather subtle, see \cite{isabelle-ref} for further + details. Any syntax specifications given by end-users need to + interact properly with the existing setup of Isabelle/Pure and + Isabelle/HOL. It is particularly important to get the precedence of + new syntactic constructs right, avoiding ambiguities with existing elements. \medskip Subsequently we introduce a few simple declaration forms @@ -39,7 +41,7 @@ case of mixfixes, where users need not care about the full details of priorities, nesting, spacing, etc. The subsequent example of the exclusive-or operation on boolean values illustrates typical infix - declarations. + declarations arising in practice. *} constdefs @@ -47,18 +49,19 @@ "A [+] B \ (A \ \ B) \ (\ A \ B)" text {* - Any curried function with at least two arguments may be associated - with infix syntax: @{text "xor A B"} and @{text "A [+] B"} refer to - the same expression internally. In partial applications with less - than two operands there is a special notation with \isa{op} prefix: - @{text xor} without arguments is represented as @{text "op [+]"}; - combined with plain prefix application this turns @{text "xor A"} - into @{text "op [+] A"}. + \noindent Now @{text "xor A B"} and @{text "A [+] B"} refer to the + same expression internally. Any curried function with at least two + arguments may be associated with infix syntax. For partial + applications with less than two operands there is a special notation + with \isa{op} prefix: @{text xor} without arguments is represented + as @{text "op [+]"}; together with plain prefix application this + turns @{text "xor A"} into @{text "op [+] A"}. - \medskip The string @{text [source] "[+]"} in the above declaration + \medskip The string @{text [source] "[+]"} in the above annotation refers to the bit of concrete syntax to represent the operator, - while the number @{text 60} determines the precedence of the whole - construct. + while the number @{text 60} determines the precedence of the + construct (i.e.\ the syntactic priorities of the arguments and + result). As it happens, Isabelle/HOL already spends many popular combinations of ASCII symbols for its own use, including both @{text "+"} and @@ -80,29 +83,11 @@ is nested to the \emph{left}: in iterated applications the more complex expression appears on the left-hand side: @{term "A [+] B [+] C"} stands for @{text "(A [+] B) [+] C"}. Similarly, - \isakeyword{infixr} refers to nesting to the \emph{right}, reading - @{term "A [+] B [+] C"} as @{text "A [+] (B [+] C)"}. In contrast, - a \emph{non-oriented} declaration via \isakeyword{infix} would - always demand explicit parentheses. - - Many binary operations observe the associative law, so the exact - grouping does not matter. Nevertheless, formal statements need be - given in a particular format, associativity needs to be treated - explicitly within the logic. Exclusive-or is happens to be - associative, as shown below. -*} - -lemma xor_assoc: "(A [+] B) [+] C = A [+] (B [+] C)" - by (auto simp add: xor_def) - -text {* - Such rules may be used in simplification to regroup nested - expressions as required. Note that the system would actually print - the above statement as @{term "A [+] B [+] C = A [+] (B [+] C)"} - (due to nesting to the left). We have preferred to give the fully - parenthesized form in the text for clarity. Only in rare situations - one may consider to force parentheses by use of non-oriented infix - syntax; equality would probably be a typical candidate. + \isakeyword{infixr} specifies to nesting to the \emph{right}, + reading @{term "A [+] B [+] C"} as @{text "A [+] (B [+] C)"}. In + contrast, a \emph{non-oriented} declaration via \isakeyword{infix} + would have rendered @{term "A [+] B [+] C"} illegal, but demand + explicit parentheses about the intended grouping. *} @@ -113,40 +98,38 @@ limitations. Rich mathematical notation demands a larger repertoire of symbols. Several standards of extended character sets have been proposed over decades, but none has become universally available so - far, not even Unicode\index{Unicode}. + far, not even Unicode\index{Unicode}. Isabelle supports a generic + notion of \bfindex{symbols} as the smallest entities of source text, + without referring to internal encodings. - Isabelle supports a generic notion of \bfindex{symbols} as the - smallest entities of source text, without referring to internal - encodings. Such ``generalized characters'' may be of one of the - following three kinds: + There are three kinds of such ``generalized characters'' available: \begin{enumerate} - \item Traditional 7-bit ASCII characters. + \item 7-bit ASCII characters - \item Named symbols: \verb,\,\verb,<,$ident$\verb,>, (or - \verb,\\,\verb,<,$ident$\verb,>,). + \item named symbols: \verb,\,\verb,<,$ident$\verb,>, - \item Named control symbols: \verb,\,\verb,<^,$ident$\verb,>, (or - \verb,\\,\verb,<^,$ident$\verb,>,). + \item named control symbols: \verb,\,\verb,<^,$ident$\verb,>, \end{enumerate} Here $ident$ may be any identifier according to the usual Isabelle conventions. This results in an infinite store of symbols, whose - interpretation is left to further front-end tools. For example, the - \verb,\,\verb,, symbol of Isabelle is really displayed as - $\forall$ --- both by the user-interface of Proof~General + X-Symbol - and the Isabelle document processor (see \S\ref{sec:document-prep}). + interpretation is left to further front-end tools. For example, + both by the user-interface of Proof~General + X-Symbol and the + Isabelle document processor (see \S\ref{sec:document-preparation}) + display the \verb,\,\verb,, symbol really as ``$\forall$''. A list of standard Isabelle symbols is given in \cite[appendix~A]{isabelle-sys}. Users may introduce their own interpretation of further symbols by configuring the appropriate - front-end tool accordingly, e.g.\ defining appropriate {\LaTeX} - macros for document preparation. There are also a few predefined - control symbols, such as \verb,\,\verb,<^sub>, and + front-end tool accordingly, e.g.\ by defining certain {\LaTeX} + macros (see also \S\ref{sec:doc-prep-symbols}). There are also a + few predefined control symbols, such as \verb,\,\verb,<^sub>, and \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent - (printable) symbol, respectively. + (printable) symbol, respectively. For example, \verb,A\<^sup>\, is + shown as ``@{text "A\<^sup>\"}''. \medskip The following version of our @{text xor} definition uses a standard Isabelle symbol to achieve typographically pleasing output. @@ -164,16 +147,17 @@ (*>*) text {* - The X-Symbol package within Proof~General provides several input - methods to enter @{text \} in the text. If all fails one may just - type \verb,\,\verb,, by hand; the display is adapted - immediately after continuing further input. + \noindent The X-Symbol package within Proof~General provides several + input methods to enter @{text \} in the text. If all fails one may + just type \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 ``$xsymbols$'' is - enabled whenever X-Symbol is active. Consider the following hybrid - declaration of @{text xor}. + \cite{isabelle-ref}). By convention, the mode of ``$xsymbols$'' is + enabled whenever Proof~General's X-Symbol mode (or {\LaTeX} output) + is active. Consider the following hybrid declaration of @{text + xor}. *} (*<*) @@ -191,31 +175,32 @@ (*>*) text {* - Here the \commdx{syntax} command acts like \isakeyword{consts}, but - without declaring a logical constant, and with an optional print - mode specification. Note that the type declaration given here - merely serves for syntactic purposes, and is not checked for - consistency with the real constant. + The \commdx{syntax} command introduced here acts like + \isakeyword{consts}, but without declaring a logical constant; an + optional print mode specification may be given, too. Note that the + type declaration given here merely serves for syntactic purposes, + and is not checked for consistency with the real constant. - \medskip Now we may write either @{text "[+]"} or @{text "\"} in + \medskip We may now write either @{text "[+]"} or @{text "\"} in input, while output uses the nicer syntax of $xsymbols$, provided - that print mode is presently active. This scheme is particularly - useful for interactive development, with the user typing plain ASCII - text, but gaining improved visual feedback from the system (say in - current goal output). + that print mode is presently active. Such an arrangement is + particularly useful for interactive development, where users may + type plain ASCII text, but gain improved visual feedback from the + system (say in current goal output). \begin{warn} - Using alternative syntax declarations easily results in varying - versions of input sources. Isabelle provides no systematic way to - convert alternative expressions back and forth. Print modes only - affect situations where formal entities are pretty printed by the - Isabelle process (e.g.\ output of terms and types), but not the - original theory text. + Alternative syntax declarations are apt to result in varying + occurrences of concrete syntax in the input sources. Isabelle + provides no systematic way to convert alternative syntax expressions + back and forth; print modes only affect situations where formal + entities are pretty printed by the Isabelle process (e.g.\ output of + terms and types), but not the original theory text. \end{warn} \medskip The following variant makes the alternative @{text \} notation only available for output. Thus we may enforce input - sources to refer to plain ASCII only. + sources to refer to plain ASCII only, but effectively disable + cut-and-paste from output as well. *} syntax (xsymbols output) @@ -225,13 +210,11 @@ subsection {* Prefix Annotations *} text {* - Prefix syntax annotations\index{prefix annotation} are just a very - degenerate of the general mixfix form \cite{isabelle-ref}, without - any template arguments or priorities --- just some piece of literal - syntax. - - The following example illustrates this idea idea by associating - common symbols with the constructors of a currency datatype. + Prefix syntax annotations\index{prefix annotation} are just another + degenerate form of general mixfixes \cite{isabelle-ref}, without any + template arguments or priorities --- just some bits of literal + syntax. The following example illustrates this idea idea by + associating common symbols with the constructors of a datatype. *} datatype currency = @@ -241,14 +224,12 @@ | Dollar nat ("$") text {* - \noindent Here the degenerate 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 @{text Euro} actually is a function - @{typ "nat \ currency"}. An expression like @{text "Euro 10"} will - be printed as @{term "\ 10"}; only the head of the application is + \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 @{text Euro} actually is a function @{typ + "nat \ currency"}. An expression like @{text "Euro 10"} will be + printed as @{term "\ 10"}; only the head of the application is subject to our concrete syntax. This simple form already achieves conformance with notational standards of the European Commission. @@ -264,7 +245,7 @@ text {* \noindent Here @{typ type} refers to the builtin syntactic category - of Isabelle types. We could now write down funny things like @{text + of Isabelle types. We may now write down funny things like @{text "\ :: nat \ \"}, for example. *} @@ -272,24 +253,23 @@ subsection {* Syntax Translations \label{sec:syntax-translations} *} text{* - Mixfix syntax annotations work well for those situations, where a - constant application forms needs to be decorated by concrete syntax. - Just reconsider @{text "xor A B"} versus @{text "A \ B"} covered - before. Occasionally, the relationship between some piece of - notation and its internal form is slightly more involved. + Mixfix syntax annotations work well for those situations where a + particular constant application forms need to be decorated by + concrete syntax; just reconsider @{text "xor A B"} versus @{text "A + \ B"} covered before. Occasionally, the relationship between some + piece of notation and its internal form is slightly more involved. + Here the concept of \bfindex{syntax translations} enters the scene. - Here the concept of \bfindex{syntax translations} enters the scene. Using the raw \isakeyword{syntax}\index{syntax (command)} command we - introduce uninterpreted notational elements, while - \commdx{translations} relates the input forms with certain logical - expressions. This essentially provides a simple mechanism for for - syntactic macros; even heavier transformations may be programmed in - ML \cite{isabelle-ref}. + may introduce uninterpreted notational elements, while + \commdx{translations} relates the input forms with more complex + logical expressions. This essentially provides a simple mechanism + for for syntactic macros; even heavier transformations may be + programmed in ML \cite{isabelle-ref}. - \medskip A typical example of syntax translations is to decorate an - relational expression (i.e.\ set membership of tuples) with nice - symbolic notation, such as @{text "(x, y) \ sim"} versus @{text "x \ - y"}. + \medskip A typical example of syntax translations is to decorate + relational expressions (set membership of tuples) with nice symbolic + notation, such as @{text "(x, y) \ sim"} versus @{text "x \ y"}. *} consts @@ -302,13 +282,13 @@ text {* \noindent Here the name of the dummy constant @{text "_sim"} does - not really matter, as long as it is not used otherwise. Prefixing + not really matter, as long as it is not used elsewhere. Prefixing an underscore is a common convention. The \isakeyword{translations} declaration already uses concrete syntax on the left-hand side; internally we relate a raw application @{text "_sim x y"} with @{text "(x, y) \ sim"}. - \medskip Another useful application of syntax translations is to + \medskip Another common application of syntax translations is to provide variant versions of fundamental relational expressions, such as @{text \} for negated equalities. The following declaration stems from Isabelle/HOL itself: @@ -319,156 +299,164 @@ text {* \noindent Normally one would introduce derived concepts like this - within the logic, using \isakeyword{consts} and \isakeyword{defs} - instead of \isakeyword{syntax} and \isakeyword{translations}. The + within the logic, using \isakeyword{consts} + \isakeyword{defs} + instead of \isakeyword{syntax} + \isakeyword{translations}. The present formulation has the virtue that expressions are immediately replaced by its ``definition'' upon parsing; the effect is reversed upon printing. Internally, @{text"\"} never appears. Simulating definitions via translations is adequate for very basic - variations of fundamental logical concepts, when the new - representation is a trivial variation on an existing one. On the - other hand, syntax translations do not scale up well to large - hierarchies of concepts built on each other. + logical concepts, where a new representation is a trivial variation + on an existing one. On the other hand, syntax translations do not + scale up well to large hierarchies of concepts built on each other. *} -section {* Document Preparation \label{sec:document-prep} *} +section {* Document Preparation \label{sec:document-preparation} *} text {* - Isabelle/Isar is centered around a certain notion of \bfindex{formal - proof documents}\index{documents|bold}: ultimately the result of the - user's theory development efforts is a human-readable record --- as - a browsable PDF file or printed on paper. The overall document - structure follows traditional mathematical articles, with - sectioning, explanations, definitions, theorem statements, and - proofs. + Isabelle/Isar is centered around the concept of \bfindex{formal + proof documents}\index{documents|bold}. Ultimately the result of + the user's theory development efforts is meant to be a + human-readable record, presented as a browsable PDF file or printed + on paper. The overall document structure follows traditional + mathematical articles, with sectioning, intermediate explanations, + definitions, theorem statements and proofs. The Isar proof language \cite{Wenzel-PhD}, which is not covered in this book, admits to write formal proof texts that are acceptable both to the machine and human readers at the same time. Thus - marginal comments and explanations may be kept at a minimum. - Nevertheless, Isabelle document output is still useful without - actual Isar proof texts; formal specifications usually deserve their - own coverage in the text, while unstructured proof scripts may be - just ignore by readers (or intentionally suppressed from the text). + marginal comments and explanations may be kept at a minimum. Even + without proper coverage of human-readable proofs, Isabelle document + is very useful to produce formally derived texts (elaborating on the + specifications etc.). Unstructured proof scripts given here may be + just ignored by readers, or intentionally suppressed from the text + by the writer (see also \S\ref{sec:doc-prep-suppress}). \medskip The Isabelle document preparation system essentially acts - like a formal front-end for {\LaTeX}. After checking definitions - and proofs the theory sources are turned into typesetting - instructions, so the final document is known to observe quite strong - ``soundness'' properties. This enables users to write authentic - reports on formal theory developments with little additional effort, - the most tedious consistency checks are handled by the system. + like a formal front-end to {\LaTeX}. After checking specifications + and proofs, the theory sources are turned into typesetting + instructions in a well-defined manner. This enables users to write + authentic reports on formal theory developments with little + additional effort, the most tedious consistency checks are handled + by the system. *} subsection {* Isabelle Sessions *} text {* - In contrast to the highly interactive mode of the formal parts of - Isabelle/Isar theory development, the document preparation stage - essentially works in batch-mode. This revolves around the concept - of a \bfindex{session}, which essentially consists of a collection - of theory source files that contribute to a single output document. - Each session is derived from a parent one (usually an object-logic - image such as \texttt{HOL}); this results in an overall tree - structure of Isabelle sessions. + In contrast to the highly interactive mode of Isabelle/Isar theory + development, the document preparation stage essentially works in + batch-mode. An Isabelle \bfindex{session} essentially consists of a + collection of theory source files that contribute to a single output + document eventually. Session is derived from a single parent each + (usually an object-logic image like \texttt{HOL}), resulting in an + overall tree structure that is reflected in the output location + within the file system (usually rooted at + \verb,~/isabelle/browser_info,). - The canonical arrangement of source files of a session called - \texttt{MySession} is as follows: + Here is the canonical arrangement of sources of a session called + \texttt{MySession}: \begin{itemize} \item Directory \texttt{MySession} contains the required theory - files, say $A@1$\texttt{.thy}, \dots, $A@n$\texttt{.thy}. + files ($A@1$\texttt{.thy}, \dots, $A@n$\texttt{.thy}). \item File \texttt{MySession/ROOT.ML} holds appropriate ML commands for loading all wanted theories, usually just - \texttt{use_thy~"$A@i$"} for any $A@i$ in leaf position of the + ``\texttt{use_thy~"$A@i$";}'' for any $A@i$ in leaf position of the theory dependency graph. \item Directory \texttt{MySession/document} contains everything - required for the {\LaTeX} stage, but only \texttt{root.tex} needs to - be provided initially. The latter file holds appropriate {\LaTeX} - code to commence a document (\verb,\documentclass, etc.), and to - include the generated files $A@i$\texttt{.tex} for each theory. The - generated file \texttt{session.tex} holds {\LaTeX} commands to - include \emph{all} theory output files in topologically sorted - order. + required for the {\LaTeX} stage; only \texttt{root.tex} needs to be + provided initially. - \item In addition an \texttt{IsaMakefile} outside of directory + The latter file holds appropriate {\LaTeX} code to commence a + document (\verb,\documentclass, etc.), and to include the generated + files $A@i$\texttt{.tex} for each theory. The generated + \texttt{session.tex} will hold {\LaTeX} commands to include all + theory output files in topologically sorted order, so + \verb,\input{session}, in \texttt{root.tex} will do it in most + situations. + + \item In addition, \texttt{IsaMakefile} outside of the directory \texttt{MySession} holds appropriate dependencies and invocations of - Isabelle tools to control the batch job. The details are covered in - \cite{isabelle-sys}; \texttt{isatool usedir} is the most important - entry point. + Isabelle tools to control the batch job. In fact, several sessions + may be controlled by the same \texttt{IsaMakefile}. See also + \cite{isabelle-sys} for further details, especially on + \texttt{isatool usedir} and \texttt{isatool make}. \end{itemize} With everything put in its proper place, \texttt{isatool make} should be sufficient to process the Isabelle session completely, - with the generated document appearing in its proper place (within - \verb,~/isabelle/browser_info,). + with the generated document appearing in its proper place. - In practice, users may want to have \texttt{isatool mkdir} generate - an initial working setup without further ado. For example, an empty - session \texttt{MySession} derived from \texttt{HOL} may be produced - as follows: + \medskip In practice, users may want to have \texttt{isatool mkdir} + generate an initial working setup without further ado. For example, + an empty session \texttt{MySession} derived from \texttt{HOL} may be + produced as follows: \begin{verbatim} isatool mkdir HOL MySession isatool make \end{verbatim} - This runs the session with sensible default options, including - verbose mode to tell the user where the result will appear. The - above dry run should produce should produce a single page of output - (with a dummy title, empty table of contents etc.). Any failure at - that stage is likely to indicate some technical problems with your - {\LaTeX} installation.\footnote{Especially make sure that - \texttt{pdflatex} is present.} + This processes the session with sensible default options, including + verbose mode to tell the user where the ultimate results will + appear. The above dry run should produce should already be able to + produce a single page of output (with a dummy title, empty table of + contents etc.). Any failure at that stage is likely to indicate + technical problems with the user's {\LaTeX} + installation.\footnote{Especially make sure that \texttt{pdflatex} + is present; if all fails one may fall back on DVI output by changing + \texttt{usedir} options \cite{isabelle-sys}.} - \medskip Users may now start to populate the directory + \medskip One may now start to populate the directory \texttt{MySession}, and the file \texttt{MySession/ROOT.ML} accordingly. \texttt{MySession/document/root.tex} should be also - adapted at some point; the generated version is mostly - self-explanatory. The default versions includes the - \texttt{isabelle} (mandatory) and \texttt{isabellesym} (required for - mathematical symbols); further packages may required, e.g.\ for - unusual Isabelle symbols. + adapted at some point; the default version is mostly + self-explanatory. + + Especially note the standard inclusion of {\LaTeX} packages + \texttt{isabelle} (mandatory), and \texttt{isabellesym} (required + for mathematical symbols), and the final \texttt{pdfsetup} (provides + handsome defaults for \texttt{hyperref}, including URL markup). + Further {\LaTeX} packages further packages may required in + particular applications, e.g.\ for unusual Isabelle symbols. - Realistic applications may demand additional files in - \texttt{MySession/document} for the {\LaTeX} stage, such as - \texttt{root.bib} for the bibliographic database.\footnote{Using - that particular name of \texttt{root.bib}, the Isabelle document - processor (actually \texttt{isatool document} \cite{isabelle-sys}) - will be smart enough to invoke \texttt{bibtex} accordingly.} + \medskip Further auxiliary files for the {\LaTeX} stage should be + included in the \texttt{MySession/document} directory, e.g.\ + additional {\TeX} sources or graphics. In particular, adding + \texttt{root.bib} here (with that specific name) causes an automatic + run of \texttt{bibtex} to process a bibliographic database; see for + further commodities \texttt{isatool document} covered in + \cite{isabelle-sys}. - \medskip Failure of the document preparation phase in an Isabelle - batch session leaves the generated sources in there target location - (as pointed out by the accompanied error message). In case of - {\LaTeX} errors, users may trace error messages at the file position - of the generated text. + \medskip Any failure of the document preparation phase in an + Isabelle batch session leaves the generated sources in there target + location (as pointed out by the accompanied error message). In case + of {\LaTeX} errors, users may trace error messages at the file + position of the generated text. *} subsection {* Structure Markup *} -subsubsection {* Sections *} +text {* + The large-scale structure of Isabelle documents follows existing + {\LaTeX} conventions, with chapters, sections, subsubsections etc. + The Isar language includes separate \bfindex{markup commands}, which + do not effect the formal content of a theory (or proof), but result + in corresponding {\LaTeX} elements issued to the output. -text {* - The large-scale structure of Isabelle documents closely follows - {\LaTeX} convention, with chapters, sections, subsubsections etc. - The formal Isar language includes separate structure \bfindex{markup - commands}, which do not effect the formal content of a theory (or - proof), but results in corresponding {\LaTeX} elements issued to the - output. - - There are different markup commands for different formal contexts: - in header position (just before a \isakeyword{theory} command), - within the theory body, or within a proof. Note that the header - needs to be treated specially, since ordinary theory and proof - commands may only occur \emph{after} the initial \isakeyword{theory} + There are separate markup commands for different formal contexts: in + header position (just before a \isakeyword{theory} command), within + the theory body, or within a proof. Note that the header needs to + be treated specially, since ordinary theory and proof commands may + only occur \emph{after} the initial \isakeyword{theory} specification. \smallskip @@ -485,15 +473,15 @@ 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 + \verb,{,\verb,*,~\dots~\verb,*,\verb,},). After stripping any surrounding white space, the argument is passed to a {\LaTeX} macro - \verb,\isamarkupXXX, for any command \isakeyword{XXX}. The latter - are defined in \verb,isabelle.sty, according to the rightmost column - above. + \verb,\isamarkupXYZ, for any command \isakeyword{XYZ}. These macros + are defined in \verb,isabelle.sty, according to the meaning given in + the rightmost column above. \medskip The following source fragment illustrates structure markup - of a theory. Note that {\LaTeX} labels may well be included inside - of section headings as well. + of a theory. Note that {\LaTeX} labels may be included inside of + section headings as well. \begin{ttbox} header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace} @@ -520,27 +508,26 @@ end \end{ttbox} - Users may occasionally want to change the meaning of some markup - commands, typically via appropriate use of \verb,\renewcommand, in - \texttt{root.tex}. The \verb,\isamarkupheader, is a good candidate - for some adaption, e.g.\ moving it up in the hierarchy to become - \verb,\chapter,. + Users may occasionally want to change the meaning of markup + commands, say via \verb,\renewcommand, in \texttt{root.tex}. The + \verb,\isamarkupheader, is a good candidate for some adaption, e.g.\ + moving it up in the hierarchy to become \verb,\chapter,. \begin{verbatim} \renewcommand{\isamarkupheader}[1]{\chapter{#1}} \end{verbatim} - Certainly, this requires to change the default + \noindent Certainly, this requires to change the default \verb,\documentclass{article}, in \texttt{root.tex} to something that supports the notion of chapters in the first place, e.g.\ \verb,\documentclass{report},. \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to hold the name of the current theory context. This is particularly - useful for document headings or footings, e.g.\ like this: + useful for document headings: \begin{verbatim} - \renewcommand{\isamarkupheader}[1]% + \renewcommand{\isamarkupheader}[1] {\chapter{#1}\markright{THEORY~\isabellecontext}} \end{verbatim} @@ -560,51 +547,49 @@ *} -subsection {* Symbols and Characters *} +subsection {* Symbols and Characters \label{sec:doc-prep-symbols} *} text {* FIXME \verb,\isabellestyle, *} -subsection {* Suppressing Output *} +subsection {* Suppressing Output \label{sec:doc-prep-suppress} *} text {* By default Isabelle's document system generates a {\LaTeX} source file for each theory that happens to get loaded during the session. - The generated \texttt{session.tex} file will include all of these in + 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} file. Certainly one may change the order of - appearance 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 efforts for maintenance. + \texttt{root.tex}. Certainly one may change the order of appearance + 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. Alternatively, one may tune the theory loading process in - \texttt{ROOT.ML}: traversal of the theory dependency graph may be - fine-tuned by adding further \verb,use_thy, invocations, although - topological sorting needs to be preserved. Moreover, the ML - operator \verb,no_document, temporarily disables document generation - while executing a theory loader command; the usage is like this: + \texttt{ROOT.ML} itself: traversal of the theory dependency graph + may be fine-tuned by adding further \verb,use_thy, invocations, + although topological sorting still has to be observed. Moreover, + the ML operator \verb,no_document, temporarily disables document + generation while executing a theory loader command; its usage is + like this: \begin{verbatim} - no_document use_thy "Aux"; + no_document use_thy "A"; \end{verbatim} - Theory output may be also suppressed \emph{partially} as well. - Typical applications include research papers or slides based on - formal developments --- these usually do not show the full formal - content. The special source comments + \medskip Theory output may be also suppressed in smaller portions as + well. For example, research papers or slides usually do not include + the formal content in full. In order to delimit \bfindex{ignored + material} special source comments \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and - \verb,(,\verb,*,\verb,>,\verb,*,\verb,), are interpreted by the - document generator as open and close parenthesis for - \bfindex{ignored material}. Any text inside of (potentially nested) - \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\dots~\verb,(,\verb,*,\verb,>,\verb,*,\verb,), - parentheses is just ignored from the output --- after correct formal - checking. + \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 as before. In the following example we suppress the slightly formalistic - \isakeyword{theory} and \isakeyword{end} part of a theory text. + \isakeyword{theory} + \isakeyword{end} surroundings a theory. \medskip @@ -620,10 +605,10 @@ \medskip - Text may be suppressed at a very fine grain; thus we may even drop - vital parts of the formal text, preventing that things have been - simpler than in reality. For example, the following ``fully - automatic'' proof is actually a fake: + Text may be suppressed in a fine grained manner. For example, 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: *} lemma "x \ (0::int) \ 0 < x * x" @@ -636,28 +621,27 @@ by (auto(*<*)simp add: int_less_le(*>*)) \end{verbatim} %(* - \medskip Ignoring portions of printed text generally demands some - care by the user. First of all, the writer is responsible not to - obfuscate the underlying formal development in an unduly manner. It - is fairly easy to scramble the remaining visible text by referring - to questionable formal items (strange definitions, arbitrary axioms - etc.) that have been hidden from sight. + \medskip Ignoring portions of printed does demand some care by the + user. 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. Some minor technical subtleties of the - \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,), - elements need to be observed as well, as the system performs little - sanity checks here. Arguments of markup commands and formal + \verb,(,\verb,*,\verb,<,\verb,*,\verb,),-\verb,(,\verb,*,\verb,>,\verb,*,\verb,), + elements need to be kept in mind as well, since the system performs + little sanity checks here. Arguments of markup commands and formal comments must not be hidden, otherwise presentation fails. Open and close parentheses need to be inserted carefully; it is fairly easy - to hide just the wrong parts, especially after rearranging the - sources. + to hide the wrong parts, especially after rearranging the sources. \medskip Authentic reports of formal theories, say as part of a - library, should usually refrain from suppressing parts of the text + library, usually 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 works out as too - ugly for general public coverage, it is often better to think of a - better way in the first place. + 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. *} (*<*) diff -r 2d136f05e164 -r a55c066624eb doc-src/TutorialI/Documents/documents.tex --- a/doc-src/TutorialI/Documents/documents.tex Mon Jan 07 18:30:31 2002 +0100 +++ b/doc-src/TutorialI/Documents/documents.tex Mon Jan 07 18:30:43 2002 +0100 @@ -2,18 +2,13 @@ \chapter{Presenting theories} \label{ch:thy-present} -Now that the reader has become sufficiently acquainted with basic formal -theory development in Isabelle/HOL, the subsequent interlude covers the -``marginal'' issue of presenting theories in a typographically pleasing -manner. Isabelle provides a rich infrastructure for concrete syntax (input -and output of the $\lambda$-calculus term language), as well as document -preparation of theory texts using existing PDF-{\LaTeX} technology. - -The measure of theory beautification depends on the kind of application one -has in mind, and the intended audience of the final results. In any case, -users may already benefit themselves from handsome notation available in -interactive development. Only minimal provisions in theory specifications may -already change the general appearance of formal entities in a significant way. +By virtue of the previous chapters the reader has become sufficiently +acquainted with basic formal theory development in Isabelle/HOL. The +subsequent interlude covers the ``marginal'' issue of presenting theories in a +typographically pleasing manner. Isabelle provides a rich infrastructure for +concrete syntax (input and output of the $\lambda$-calculus language), as well +as document preparation of theory texts based on existing PDF-{\LaTeX} +technology. As has been pointed out by Leibniz\index{Leibniz, Gottfried Wilhelm} more than 300 years ago, \emph{notions} are in principle more important than