--- a/doc-src/TutorialI/Documents/document/Documents.tex Sun Jan 06 16:51:48 2002 +0100
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Mon Jan 07 18:30:31 2002 +0100
@@ -8,18 +8,18 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Concerning Isabelle's ``inner'' language of simply-typed \isa{{\isasymlambda}}-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.
+Concerning Isabelle's ``inner'' language of simply-typed \isa{{\isasymlambda}}-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
@@ -43,7 +43,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.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{constdefs}\isanewline
@@ -51,18 +51,19 @@
\ \ {\isachardoublequote}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
%
\begin{isamarkuptext}%
-Any curried function with at least two arguments may be associated
- with infix syntax: \isa{xor\ A\ B} and \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} refer to
- the same expression internally. In partial applications with less
- than two operands there is a special notation with \isa{op} prefix:
- \isa{xor} without arguments is represented as \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}};
- combined with plain prefix application this turns \isa{xor\ A}
- into \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ A}.
+\noindent Now \isa{xor\ A\ B} and \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ 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: \isa{xor} without arguments is represented
+ 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 string \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}} in the above declaration
+ \medskip The string \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}} in the above annotation
refers to the bit of concrete syntax to represent the operator,
- while the number \isa{{\isadigit{6}}{\isadigit{0}}} determines the precedence of the whole
- construct.
+ 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 spends many popular combinations
of ASCII symbols for its own use, including both \isa{{\isacharplus}} and
@@ -81,30 +82,11 @@
\medskip The keyword \isakeyword{infixl} specifies an 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} refers 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
- 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.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\ xor{\isacharunderscore}assoc{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B{\isacharparenright}\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C\ {\isacharequal}\ A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}{\isachardoublequote}\isanewline
-\ \ \isamarkupfalse%
-\isacommand{by}\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
-%
-\begin{isamarkuptext}%
-Such rules may be used in simplification to regroup nested
- expressions as required. Note that the system would actually print
- the above statement as \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C\ {\isacharequal}\ A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}
- (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 \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 have rendered \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} illegal, but demand
+ explicit parentheses about the intended grouping.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -117,40 +99,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,<forall>, 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,<forall>, 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>\<star>, is
+ shown as ``\isa{A\isactrlsup {\isasymstar}}''.
\medskip The following version of our \isa{xor} definition uses a
standard Isabelle symbol to achieve typographically pleasing output.%
@@ -164,16 +144,16 @@
\isamarkupfalse%
%
\begin{isamarkuptext}%
-The X-Symbol package within Proof~General provides several input
- methods to enter \isa{{\isasymoplus}} in the text. If all fails one may just
- type \verb,\,\verb,<oplus>, 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 \isa{{\isasymoplus}} in the text. If all fails one may
+ just type \verb,\,\verb,<oplus>, 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 \isa{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 \isa{xor}.%
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
@@ -188,31 +168,32 @@
\isamarkupfalse%
%
\begin{isamarkuptext}%
-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 \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}} or \isa{{\isasymoplus}} in
+ \medskip We may now write either \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}} or \isa{{\isasymoplus}} 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 \isa{{\isasymoplus}}
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.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{syntax}\ {\isacharparenleft}xsymbols\ \isakeyword{output}{\isacharparenright}\isanewline
@@ -223,13 +204,11 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-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.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{datatype}\ currency\ {\isacharequal}\isanewline
@@ -239,14 +218,11 @@
\ \ {\isacharbar}\ Dollar\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isachardollar}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
%
\begin{isamarkuptext}%
-\noindent Here the degenerate mixfix annotations on the rightmost
- column happen to consist of a single Isabelle symbol each:
- \verb,\,\verb,<euro>,, \verb,\,\verb,<pounds>,,
- \verb,\,\verb,<yen>,, 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 printed as \isa{{\isasymeuro}\ {\isadigit{1}}{\isadigit{0}}}; 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,<euro>,,
+ \verb,\,\verb,<pounds>,, \verb,\,\verb,<yen>,, 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
+ printed as \isa{{\isasymeuro}\ {\isadigit{1}}{\isadigit{0}}}; 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.
@@ -261,7 +237,7 @@
%
\begin{isamarkuptext}%
\noindent Here \isa{type} refers to the builtin syntactic category
- of Isabelle types. We could now write down funny things like \isa{{\isasymeuro}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ {\isasymcurrency}}, for example.%
+ of Isabelle types. We may now write down funny things like \isa{{\isasymeuro}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ {\isasymcurrency}}, for example.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -270,23 +246,22 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-Mixfix syntax annotations work well for those situations, where a
- constant application forms needs to be decorated by concrete syntax.
- Just reconsider \isa{xor\ A\ B} versus \isa{A\ {\isasymoplus}\ 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 \isa{xor\ A\ B} versus \isa{A\ {\isasymoplus}\ 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 \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} versus \isa{x\ {\isasymapprox}\ y}.%
+ \medskip A typical example of syntax translations is to decorate
+ relational expressions (set membership of tuples) with nice symbolic
+ notation, such as \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} versus \isa{x\ {\isasymapprox}\ y}.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{consts}\isanewline
@@ -301,13 +276,13 @@
%
\begin{isamarkuptext}%
\noindent Here the name of the dummy constant \isa{{\isacharunderscore}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 \isa{{\isacharunderscore}sim\ x\ y} with
\isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ 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 \isa{{\isasymnoteq}} for negated equalities. The following declaration
stems from Isabelle/HOL itself:%
@@ -319,49 +294,49 @@
%
\begin{isamarkuptext}%
\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, \isa{{\isasymnoteq}} 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.%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Document Preparation \label{sec:document-prep}%
+\isamarkupsection{Document Preparation \label{sec:document-preparation}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
-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.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -370,89 +345,100 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-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.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -460,23 +446,18 @@
}
\isamarkuptrue%
%
-\isamarkupsubsubsection{Sections%
-}
-\isamarkuptrue%
-%
\begin{isamarkuptext}%
-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.
+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.
- 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
@@ -493,15 +474,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}
@@ -528,27 +509,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}
@@ -569,7 +549,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Symbols and Characters%
+\isamarkupsubsection{Symbols and Characters \label{sec:doc-prep-symbols}%
}
\isamarkuptrue%
%
@@ -578,46 +558,44 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Suppressing Output%
+\isamarkupsubsection{Suppressing Output \label{sec:doc-prep-suppress}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
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
@@ -633,10 +611,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:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\ {\isachardoublequote}x\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isacharless}\ x\ {\isacharasterisk}\ x{\isachardoublequote}\isanewline
@@ -650,28 +628,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.%
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
--- a/doc-src/TutorialI/tutorial.ind Sun Jan 06 16:51:48 2002 +0100
+++ b/doc-src/TutorialI/tutorial.ind Mon Jan 07 18:30:31 2002 +0100
@@ -21,9 +21,6 @@
\item \verb$^$\texttt{*}, \bold{207}
\item \isasymAnd, \bold{12}, \bold{207}
\item \ttAnd, \bold{207}
- \item \isasymrightleftharpoons, 57
- \item \isasymrightharpoonup, 57
- \item \isasymleftharpoondown, 57
\item \emph {$\Rightarrow $}, \bold{5}
\item \ttlbr, \bold{207}
\item \ttrbr, \bold{207}
@@ -107,7 +104,7 @@
\item case splits, \bold{31}
\item \isa {case_tac} (method), 19, 99, 155
\item \isa {cases} (method), 160
- \item \isacommand {chapter} (command), 59
+ \item \isacommand {chapter} (command), 60
\item \isa {clarify} (method), 89, 90
\item \isa {clarsimp} (method), 89, 90
\item \isa {classical} (theorem), \bold{71}
@@ -244,7 +241,7 @@
\indexspace
\item \isa {hd} (constant), 17, 37
- \item \isacommand {header} (command), 59
+ \item \isacommand {header} (command), 60
\item Hilbert's $\varepsilon$-operator, 84
\item HOLCF, 43
\item Hopcroft, J. E., 143
@@ -265,7 +262,7 @@
\item \isa {iff} (attribute), 88, 100, 128
\item \isa {iffD1} (theorem), \bold{92}
\item \isa {iffD2} (theorem), \bold{92}
- \item ignored material, \bold{61}
+ \item ignored material, \bold{62}
\item image
\subitem under a function, \bold{109}
\subitem under a relation, \bold{110}
@@ -359,7 +356,7 @@
\item \isa {Main} (theory), 4
\item major premise, \bold{73}
\item \isa {make} (constant), 161
- \item markup commands, \bold{59}
+ \item markup commands, \bold{60}
\item \isa {max} (constant), 23, 24
\item measure functions, 47, 112
\item \isa {measure_def} (theorem), \bold{113}
@@ -500,8 +497,8 @@
\item \isa {safe} (method), 89, 90
\item safe rules, \bold{88}
- \item \isacommand {sect} (command), 59
- \item \isacommand {section} (command), 59
+ \item \isacommand {sect} (command), 60
+ \item \isacommand {section} (command), 60
\item selector
\subitem record, 157
\item session, \bold{58}
@@ -550,23 +547,24 @@
\item subgoal numbering, 46
\item \isa {subgoal_tac} (method), 96
\item subgoals, 12
- \item \isacommand {subsect} (command), 59
- \item \isacommand {subsection} (command), 59
+ \item \isacommand {subsect} (command), 60
+ \item \isacommand {subsection} (command), 60
\item subset relation, \bold{104}
\item \isa {subsetD} (theorem), \bold{104}
\item \isa {subsetI} (theorem), \bold{104}
\item \isa {subst} (method), 75
\item substitution, 75--77
- \item \isacommand {subsubsect} (command), 59
- \item \isacommand {subsubsection} (command), 59
+ \item \isacommand {subsubsect} (command), 60
+ \item \isacommand {subsubsection} (command), 60
\item \isa {Suc} (constant), 22
\item \isa {surj_def} (theorem), \bold{108}
\item surjections, 108
\item \isa {sym} (theorem), \bold{92}
- \item symbols, \bold{55}
+ \item symbols, \bold{54}
\item syntax, 6, 11
- \item \isacommand {syntax} (command), 56
- \item syntax translations, 57
+ \item \isacommand {syntax} (command), 55
+ \item syntax (command), 57
+ \item syntax translations, \bold{57}
\indexspace
@@ -620,7 +618,7 @@
\item \isa {Un_subset_iff} (theorem), \bold{104}
\item \isacommand {undo} (command), 16
\item \isa {unfold} (method), \bold{31}
- \item Unicode, 55
+ \item Unicode, 54
\item unification, 74--77
\item \isa {UNION} (constant), 107
\item \texttt {Union}, \bold{207}