%
\begin{isabellebody}%
\def\isabellecontext{Documents}%
\isamarkupfalse%
%
\isamarkupsection{Concrete Syntax \label{sec:concrete-syntax}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
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, parser and pretty printer configuration is a
rather subtle affair, see \cite{isabelle-ref} for details. 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 syntax declaration
forms that already cover many common situations fairly well.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Infix Annotations%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Syntax annotations may be included wherever constants are declared
directly or indirectly, including \isacommand{consts},
\isacommand{constdefs}, or \isacommand{datatype} (for the
constructor operations). Type-constructors may be annotated as
well, although this is less frequently encountered in practice (the
infix type \isa{{\isasymtimes}} comes to mind).
Infix declarations\index{infix annotations} provide a useful special
case of mixfixes, where users need not care about the full details
of priorities, nesting, spacing, etc. The following example of the
exclusive-or operation on boolean values illustrates typical infix
declarations arising in practice.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{constdefs}\isanewline
\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
\ \ {\isachardoublequote}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
%
\begin{isamarkuptext}%
\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 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.
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.
Operator precedence also needs some special considerations. The
admissible range is 0--1000. Very low or high priorities are
basically reserved for the meta-logic. Syntax of Isabelle/HOL
mainly uses the range of 10--100: the equality infix \isa{{\isacharequal}} is
centered at 50, logical connectives (like \isa{{\isasymor}} and \isa{{\isasymand}}) are below 50, and algebraic ones (like \isa{{\isacharplus}} and \isa{{\isacharasterisk}}) above 50. User syntax should strive to coexist with common
HOL forms, or use the mostly unused range 100--900.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Mathematical Symbols \label{sec:syntax-symbols}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Concrete syntax based on plain ASCII characters has its inherent
limitations. Rich mathematical notation demands a larger repertoire
of glyphs. Several standards of extended character sets have been
proposed over decades, but none has become universally available so
far. Isabelle supports a generic notion of \bfindex{symbols} as the
smallest entities of source text, without referring to internal
encodings. There are three kinds of such ``generalized
characters'':
\begin{enumerate}
\item 7-bit ASCII characters
\item named symbols: \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,
both 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 as \isa{{\isasymforall}}.
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.\ 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. For example, \verb,A\<^sup>\<star>, is
output as \isa{A\isactrlsup {\isasymstar}}.
\medskip The following version of our \isa{xor} definition uses a
standard Isabelle symbol to achieve typographically more pleasing
output than before.%
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
\isamarkupfalse%
\isacommand{constdefs}\isanewline
\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
\ \ {\isachardoublequote}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
\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 a named entity \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 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%
\isamarkupfalse%
\isacommand{constdefs}\isanewline
\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
\ \ {\isachardoublequote}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline
\isanewline
\isamarkupfalse%
\isacommand{syntax}\ {\isacharparenleft}xsymbols{\isacharparenright}\isanewline
\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
\isamarkupfalse%
%
\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.
\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
that print mode is 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.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Prefix Annotations%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Prefix syntax annotations\index{prefix annotation} are another
degenerate form of 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
\ \ \ \ Euro\ nat\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymeuro}{\isachardoublequote}{\isacharparenright}\isanewline
\ \ {\isacharbar}\ Pounds\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isasympounds}{\isachardoublequote}{\isacharparenright}\isanewline
\ \ {\isacharbar}\ Yen\ nat\ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymyen}{\isachardoublequote}{\isacharparenright}\isanewline
\ \ {\isacharbar}\ Dollar\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isachardollar}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
%
\begin{isamarkuptext}%
\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 rather simple form already
achieves conformance with notational standards of the European
Commission.
Prefix syntax also works for plain \isakeyword{consts} or
\isakeyword{constdefs}, of course.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Syntax Translations \label{sec:syntax-translations}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Mixfix syntax annotations work well in those situations where
particular constant application forms need to be decorated by
concrete syntax; e.g.\ \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.
Using the raw \isakeyword{syntax}\index{syntax (command)} command we
may introduce uninterpreted notational elements, while
\commdx{translations} relate input forms with more complex logical
expressions. This essentially provides a simple mechanism for
syntactic macros; even heavier transformations may be written in ML
\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}.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{consts}\isanewline
\ \ sim\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set{\isachardoublequote}\isanewline
\isanewline
\isamarkupfalse%
\isacommand{syntax}\isanewline
\ \ {\isachardoublequote}{\isacharunderscore}sim{\isachardoublequote}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infix}\ {\isachardoublequote}{\isasymapprox}{\isachardoublequote}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline
\isamarkupfalse%
\isacommand{translations}\isanewline
\ \ {\isachardoublequote}x\ {\isasymapprox}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim{\isachardoublequote}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent Here the name of the dummy constant \isa{{\isacharunderscore}sim} does
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 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:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{syntax}\ {\isachardoublequote}{\isacharunderscore}not{\isacharunderscore}equal{\isachardoublequote}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymnoteq}{\isasymignore}{\isachardoublequote}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline
\isamarkupfalse%
\isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}{\isasymignore}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent Normally one would introduce derived concepts like this
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 the ``definition'' upon parsing; the effect is reversed
upon printing.
Simulating definitions via translations is adequate for very basic
principles, 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-preparation}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Isabelle/Isar is centered around the concept of \bfindex{formal
proof documents}\index{documents|bold}. The ultimate result of a
formal development effort is meant to be a human-readable record,
presented as browsable PDF file or printed on paper. The overall
document structure follows traditional mathematical articles, with
sections, intermediate explanations, definitions, theorems and
proofs.
\medskip The Isabelle document preparation system essentially acts
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.
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}.%
\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%
%
\begin{isamarkuptext}%
\noindent The datatype induction rule generated here is of the form
\begin{isabelle}%
{\isasymlbrakk}P\ Leaf{\isacharsemicolon}\isanewline
\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:
\begin{ttbox}
text {\ttlbrace}*
The following datatype definition of {\at}{\ttlbrace}text "'a bintree"{\ttrbrace}
models binary trees with nodes being decorated by elements
of type {\at}{\ttlbrace}typ 'a{\ttrbrace}.
*{\ttrbrace}
datatype 'a bintree =
Leaf | Branch 'a "'a bintree" "'a bintree"
text {\ttlbrace}*
{\ttback}noindent The datatype induction rule generated here is
of the form {\at}{\ttlbrace}thm [display] bintree.induct [no_vars]{\ttrbrace}
*{\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
\texttt{\at}\verb,{text "'a bintree"}, or
\texttt{\at}\verb,{typ 'a},; see also \S\ref{sec:doc-prep-text}.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Isabelle Sessions%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
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} consists of a collection
of source files that may contribute to an output document
eventually. Each session is derived from a single parent, usually
an object-logic image like \texttt{HOL}. This results in an overall
tree structure, which is reflected by the output location in the
file system (usually rooted at \verb,~/isabelle/browser_info,).
\medskip The easiest way to manage Isabelle sessions is via
\texttt{isatool mkdir} (generates an initial session source setup)
and \texttt{isatool make} (run sessions controlled by
\texttt{IsaMakefile}). For example, a new session
\texttt{MySession} derived from \texttt{HOL} may be produced as
follows:
\begin{verbatim}
isatool mkdir HOL MySession
isatool make
\end{verbatim}
The \texttt{isatool make} job also informs about the file-system
location of the ultimate results. The above dry run should be able
to produce some \texttt{document.pdf} (with dummy title, empty table
of contents etc.). Any failure at this stage usually indicates
technical problems of the {\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 in
\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.
\begin{itemize}
\item Directory \texttt{MySession} holds the required theory files
$T@1$\texttt{.thy}, \dots, $T@n$\texttt{.thy}.
\item File \texttt{MySession/ROOT.ML} holds appropriate ML commands
for loading all wanted theories, usually just
``\texttt{use_thy"$T@i$";}'' for any $T@i$ in leaf position of the
dependency graph.
\item Directory \texttt{MySession/document} contains everything
required for the {\LaTeX} stage; 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 $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.
\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}.
See also \cite{isabelle-sys} for further details, especially on
\texttt{isatool usedir} and \texttt{isatool make}.
\end{itemize}
One may now start to populate the directory \texttt{MySession}, and
the file \texttt{MySession/ROOT.ML} accordingly.
\texttt{MySession/document/root.tex} should also be adapted at some
point; the default version is mostly self-explanatory. Note that
\verb,\isabellestyle, enables fine-tuning of the general appearance
of characters and mathematical symbols (see also
\S\ref{sec:doc-prep-symbols}).
Especially observe the included {\LaTeX} packages \texttt{isabelle}
(mandatory), \texttt{isabellesym} (required for mathematical
symbols), and the final \texttt{pdfsetup} (provides sane defaults
for \texttt{hyperref}, including URL markup) --- all three are
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 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
hand.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Structure Markup%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
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 affect the formal meaning of a theory (or proof), but result
in corresponding {\LaTeX} elements.
There are separate markup commands depending on the textual context:
in header position (just before \isakeyword{theory}), within the
theory body, or within a proof. The header needs to be treated
specially here, since ordinary theory and proof commands may only
occur \emph{after} the initial \isakeyword{theory} specification.
\medskip
\begin{tabular}{llll}
header & theory & proof & default meaning \\\hline
& \commdx{chapter} & & \verb,\chapter, \\
\commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\
& \commdx{subsection} & \commdx{subsect} & \verb,\subsection, \\
& \commdx{subsubsection} & \commdx{subsubsect} & \verb,\subsubsection, \\
\end{tabular}
\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
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
the rightmost column above.
\medskip The following source fragment illustrates structure markup
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}
theory Foo_Bar = Main:
subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
consts
foo :: \dots
bar :: \dots
defs \dots
subsection {\ttlbrace}* Derived rules *{\ttrbrace}
lemma fooI: \dots
lemma fooE: \dots
subsection {\ttlbrace}* Main theorem {\ttback}label{\ttlbrace}sec:main-theorem{\ttrbrace} *{\ttrbrace}
theorem main: \dots
end
\end{ttbox}
Users may occasionally want to change the meaning of markup
commands, say via \verb,\renewcommand, in \texttt{root.tex};
\verb,\isamarkupheader, is a good candidate for some tuning, e.g.\
moving it up in the hierarchy to become \verb,\chapter,.
\begin{verbatim}
\renewcommand{\isamarkupheader}[1]{\chapter{#1}}
\end{verbatim}
\noindent That particular modification requires change to the
document class given in \texttt{root.tex} to something that supports
the notion of chapters in the first place, such as
\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:
\begin{verbatim}
\renewcommand{\isamarkupheader}[1]
{\chapter{#1}\markright{THEORY~\isabellecontext}}
\end{verbatim}
\noindent Make sure to include something like
\verb,\pagestyle{headings}, in \texttt{root.tex}; the document
should have more than 2 pages to show the effect.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Formal Comments and Antiquotations \label{sec:doc-prep-text}%
}
\isamarkuptrue%
%
\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
(\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
marginal comments may be given at the same time. Here is a simple
example:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\ {\isachardoublequote}A\ {\isacharminus}{\isacharminus}{\isachargreater}\ A{\isachardoublequote}\isanewline
\ \ %
\isamarkupcmt{a triviality of propositional logic%
}
\isanewline
\ \ %
\isamarkupcmt{(should not really bother)%
}
\isanewline
\ \ \isamarkupfalse%
\isacommand{by}\ {\isacharparenleft}rule\ impI{\isacharparenright}\ %
\isamarkupcmt{implicit assumption step involved here%
}
\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent The above output has been produced as follows:
\begin{verbatim}
lemma "A --> A"
-- "a triviality of propositional logic"
-- "(should not really bother)"
by (rule impI) -- "implicit assumption step involved here"
\end{verbatim}
From the {\LaTeX} viewpoint, ``\verb,--,'' acts like a markup
command, associated with the macro \verb,\isamarkupcmt, (taking a
single argument).
\medskip Text blocks are introduced by the commands \bfindex{text}
and \bfindex{txt}, for theory and proof contexts, respectively.
Each takes again a single $text$ argument, which is interpreted as a
free-form paragraph in {\LaTeX} (surrounded by some additional
vertical space). This behavior may be changed by redefining the
{\LaTeX} environments of \verb,isamarkuptext, or
\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.
\medskip The $text$ part of each of the various markup commands
considered so far essentially inserts \emph{quoted material} into a
formal text, mainly for instruction of the reader. An
\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).
The general syntax of antiquotations is as follows:
\texttt{{\at}{\ttlbrace}$name$ $arguments${\ttrbrace}}, or
\texttt{{\at}{\ttlbrace}$name$ [$options$] $arguments${\ttrbrace}}
for a comma-separated list of options consisting of a $name$ or
\texttt{$name$=$value$}. The syntax of $arguments$ depends on the
kind of antiquotation, it generally follows the same conventions for
types, terms, or theorems as in the formal part of a theory.
\medskip Here is an example of the quotation-antiquotation
technique: \isa{{\isasymlambda}x\ y{\isachardot}\ x} is a well-typed term.
\medskip\noindent The above output has been produced as follows:
\begin{ttbox}
text {\ttlbrace}*
Here is an example of the quotation-antiquotation technique:
{\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term.
*{\ttrbrace}
\end{ttbox}
From the notational change of the ASCII character \verb,%, to the
symbol \isa{{\isasymlambda}} we see that the term really got printed by the
system (after parsing and type-checking) --- document preparation
enables symbolic output by default.
\medskip The next example includes an option to modify the
\verb,show_types, flag of Isabelle:
\texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces \isa{{\isasymlambda}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ y{\isasymColon}{\isacharprime}b{\isachardot}\ x}. Type-inference has figured out the most
general typings in the present (theory) context. Note that term
fragments may acquire different typings due to constraints imposed
by previous text (say within a proof), e.g.\ due to the main goal
statement given beforehand.
\medskip Several further kinds of antiquotations (and options) are
available \cite{isabelle-sys}. Here are a few commonly used
combinations:
\medskip
\begin{tabular}{ll}
\texttt{\at}\verb,{typ,~$\tau$\verb,}, & print type $\tau$ \\
\texttt{\at}\verb,{term,~$t$\verb,}, & print term $t$ \\
\texttt{\at}\verb,{prop,~$\phi$\verb,}, & print proposition $\phi$ \\
\texttt{\at}\verb,{prop [display],~$\phi$\verb,}, & print large proposition $\phi$ (with linebreaks) \\
\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,{text,~$s$\verb,}, & print uninterpreted text $s$ \\
\end{tabular}
\medskip
Note that \attrdx{no_vars} given above is \emph{not} an
antiquotation option, but an attribute of the theorem argument given
here. This might be useful with a diagnostic command like
\isakeyword{thm}, too.
\medskip The \texttt{\at}\verb,{text, $s$\verb,}, antiquotation is
particularly interesting. Embedding uninterpreted text within an
informal body might appear useless at first sight. Here the key
virtue is that the string $s$ is processed as Isabelle output,
interpreting Isabelle symbols appropriately.
For example, \texttt{\at}\verb,{text "\<forall>\<exists>"}, produces \isa{{\isasymforall}{\isasymexists}}, according to the standard interpretation of these symbol
(cf.\ \S\ref{sec:doc-prep-symbols}). Thus we achieve consistent
mathematical notation in both the formal and informal parts of the
document very easily. Manual {\LaTeX} code would leave more control
over the typesetting, but is also slightly more tedious.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsection{Interpretation of Symbols \label{sec:doc-prep-symbols}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
As has been pointed out before (\S\ref{sec:syntax-symbols}),
Isabelle symbols are the smallest syntactic entities --- a
straightforward generalization of ASCII characters. While Isabelle
does not impose any interpretation of the infinite collection of
named symbols, {\LaTeX} documents show canonical glyphs for certain
standard symbols \cite[appendix~A]{isabelle-sys}.
The {\LaTeX} code produced from Isabelle text follows a relatively
simple scheme. Users may wish to tune the final appearance by
redefining certain macros, say in \texttt{root.tex} of the document.
\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
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 control symbols: \verb,{\isasym,$XYZ$\verb,}, become
\verb,\isactrl,$XYZ$ each; 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.
\medskip The \verb,\isabellestyle, macro provides a high-level
interface to tune the general appearance of individual symbols. For
example, \verb,\isabellestyle{it}, uses the italics text style to
mimic the general appearance of the {\LaTeX} math mode; double
quotes are not printed at all. The resulting quality of typesetting
is quite good, so this should be the default style for work that
gets distributed to a broader audience.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\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 gets loaded while running the session.
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.
Alternatively, one may tune the theory loading process in
\texttt{ROOT.ML} itself: traversal of the theory dependency graph
may be fine-tuned by adding \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 "T";
\end{verbatim}
\medskip Theory output may also be suppressed in smaller portions.
For example, research articles, 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,), may be included in the
text. Only the document preparation system is affected, the formal
checking the theory is performed unchanged.
In the following example we suppress the slightly formalistic
\isakeyword{theory} + \isakeyword{end} surroundings a theory.
\medskip
\begin{tabular}{l}
\verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
\texttt{theory T = Main:} \\
\verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
~~$\vdots$ \\
\verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
\texttt{end} \\
\verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
\end{tabular}
\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:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\ {\isachardoublequote}x\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isacharless}\ x\ {\isacharasterisk}\ x{\isachardoublequote}\isanewline
\ \ \isamarkupfalse%
\isacommand{by}\ {\isacharparenleft}auto{\isacharparenright}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent Here the real source of the proof has been as follows:
\begin{verbatim}
by (auto(*<*)simp add: int_less_le(*>*))
\end{verbatim}
%(*
\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.
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.
\medskip Some technical subtleties of the
\verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),
elements need to be kept in mind, too --- 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 the wrong parts, especially after rearranging the sources.%
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: