%

\begin{isabellebody}%

\def\isabellecontext{Documents}%

\isamarkupfalse%

%

\isamarkupsection{Concrete Syntax \label{sec:concrete-syntax}%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

The core concept of Isabelle's framework for concrete syntax is that

  of \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

  subtle affair \cite{isabelle-ref}.  Your syntax specifications need

  to interact properly with the existing setup of Isabelle/Pure and

  Isabelle/HOL\@.  To avoid creating ambiguities with existing

  elements, it is particularly important to give new syntactic

  constructs the right precedence.

  \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,

  such as \isacommand{consts} and \isacommand{constdefs} --- and also

  \isacommand{datatype}, which declares 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.  The following example of the exclusive-or

  operation on boolean values illustrates typical infix declarations.%

\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 given infix syntax.  For partial applications with

  fewer than two operands, there is a notation using the prefix~\isa{op}.  For instance, \isa{xor} without arguments is represented as

  \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}}; together with ordinary function application, this

  turns \isa{xor\ A} into \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ A}.

  \medskip The keyword \isakeyword{infixl} seen above specifies an

  infix operator that is nested to the \emph{left}: in iterated

  applications the more complex expression appears on the left-hand

  side, and \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} means 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}}.  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 our annotation refers to the

  concrete syntax to represent the operator (a literal token), while

  the number \isa{{\isadigit{6}}{\isadigit{0}}} determines the precedence of the construct:

  the syntactic priorities of the arguments and result.  Isabelle/HOL

  already uses up many popular combinations of ASCII symbols for its

  own use, including both \isa{{\isacharplus}} and \isa{{\isacharplus}{\isacharplus}}.  Longer

  character combinations are more likely to be still available for

  user extensions, such as our~\isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}}.

  Operator precedences have a range of 0--1000.  Very low or high

  priorities are reserved for the meta-logic.  HOL syntax 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; algebraic ones (like \isa{{\isacharplus}} and \isa{{\isacharasterisk}}) are

  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 ASCII characters has inherent limitations.

  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

  has its own 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, 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}.  You may introduce your 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 Replacing our definition of \isa{xor} by the following

  specifies an Isabelle symbol for the new operator:%

\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

  corresponding symbol will be displayed after further input.

  \medskip More flexible is to provide alternative syntax forms

  through the \bfindex{print mode} concept~\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 of \isakeyword{syntax}, here \isa{{\isacharparenleft}xsymbols{\isacharparenright}}, is optional.  Also note that its type merely serves

  for syntactic purposes, and is \emph{not} checked for consistency

  with the real constant.

  \medskip We may now write \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} or \isa{A\ {\isasymoplus}\ B} in

  input, while output uses the nicer syntax of $xsymbols$ whenever

  that print mode is active.  Such an arrangement is particularly

  useful for interactive development, where users may type ASCII text

  and see mathematical symbols displayed during proofs.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{Prefix Annotations%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

Prefix syntax annotations\index{prefix annotation} are another form

  of mixfixes \cite{isabelle-ref}, without any template arguments or

  priorities --- just some literal syntax.  The following example

  associates 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}.  The expression \isa{Euro\ {\isadigit{1}}{\isadigit{0}}} will be

  printed as \isa{{\isasymeuro}\ {\isadigit{1}}{\isadigit{0}}}; only the head of the application is

  subject to our concrete syntax.  This rather simple form already

  achieves conformance with notational standards of the European

  Commission.

  Prefix syntax works the same way for \isakeyword{consts} or

  \isakeyword{constdefs}.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\isamarkupsubsection{Syntax Translations \label{sec:syntax-translations}%

}

\isamarkuptrue%

%

\begin{isamarkuptext}%

Mixfix syntax annotations merely decorate particular constant

  application forms with concrete syntax, for instance replacing \

  \isa{xor\ A\ B} by \isa{A\ {\isasymoplus}\ B}.  Occasionally, the

  relationship between some piece of notation and its internal form is

  more complicated.  Here we need \bfindex{syntax translations}.

  Using the \isakeyword{syntax}\index{syntax (command)}, command we

  introduce uninterpreted notational elements.  Then

  \commdx{translations} relate input forms to complex logical

  expressions.  This provides a simple mechanism for syntactic macros;

  even heavier transformations may be written in ML

  \cite{isabelle-ref}.

  \medskip A typical use of syntax translations is to introduce

  relational notation for membership in a set of pair, replacing \

  \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} by \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 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.

  This sort of translation is appropriate when the defined concept is

  a trivial variation on an existing one.  On the other hand, syntax

  translations do not scale up well to large hierarchies of concepts.

  Translations do not replace definitions!%

\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 outcome 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 lets you write authentic

  reports on theory developments with little effort: many technical

  consistency checks are handled by the system.

  Here is an example to illustrate the idea of Isabelle document

  preparation.%

\end{isamarkuptext}%

\isamarkuptrue%

%

\begin{quotation}

%

\begin{isamarkuptext}%

The following datatype definition of \isa{{\isacharprime}a\ bintree} models

  binary trees with nodes being decorated by elements of type \isa{{\isacharprime}a}.%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{datatype}\ {\isacharprime}a\ bintree\ {\isacharequal}\isanewline

\ \ \ \ \ Leaf\ {\isacharbar}\ Branch\ {\isacharprime}a\ \ {\isachardoublequote}{\isacharprime}a\ bintree{\isachardoublequote}\ \ {\isachardoublequote}{\isacharprime}a\ bintree{\isachardoublequote}\isamarkupfalse%

%

\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

\isaindent{\ }{\isasymLongrightarrow}\ P\ bintree%

\end{isabelle}%

\end{isamarkuptext}%

\isamarkuptrue%

%

\end{quotation}

%

\begin{isamarkuptext}%

\noindent The above document output has been produced as follows:

  \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"

  \end{ttbox}

  \begin{ttbox}

  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}\vspace{-\medskipamount}

  \noindent Here we have augmented the theory by formal comments

  (using \isakeyword{text} blocks), the informal parts may again refer

  to formal entities by means of ``antiquotations'' (such as

  \texttt{\at}\verb,{text "'a bintree"}, or

  \texttt{\at}\verb,{typ 'a},), see also \S\ref{sec:doc-prep-text}.%

\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.  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 in doubt 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.

  \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 the body of \texttt{root.tex} does the job

  in most situations.

  \item \texttt{IsaMakefile} holds appropriate dependencies and

  invocations of Isabelle tools to control the batch job.  In fact,

  several sessions may be managed by the same \texttt{IsaMakefile}.

  See the \emph{Isabelle System Manual} \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.  The file

  \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, say for unusual mathematical symbols.

  \medskip Any additional files for the {\LaTeX} stage go into the

  \texttt{MySession/document} directory as well.  In particular,

  adding a file named \texttt{root.bib} causes an automatic run of

  \texttt{bibtex} to process a bibliographic database; see also

  \texttt{isatool document} \cite{isabelle-sys}.

  \medskip Any failure of the document preparation phase in an

  Isabelle batch session leaves the generated sources in their target

  location, identified by the accompanying error message.  This lets

  you trace {\LaTeX} problems with the generated 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,",~\isa{{\isasymdots}}~\verb,", or

  \verb,{,\verb,*,~\isa{{\isasymdots}}~\verb,*,\verb,},).  After stripping any

  surrounding white space, the argument is passed to a {\LaTeX} macro

  \verb,\isamarkupXYZ, for 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}\vspace{-\medskipamount}

  You may occasionally want to change the meaning of markup commands,

  say via \verb,\renewcommand, in \texttt{root.tex}.  For example,

  \verb,\isamarkupheader, is a good candidate for some tuning.  We

  could move it up in the hierarchy to become \verb,\chapter,.

\begin{verbatim}

  \renewcommand{\isamarkupheader}[1]{\chapter{#1}}

\end{verbatim}

  \noindent Now we must change the document class given in

  \texttt{root.tex} to something that supports chapters.  A suitable

  command is \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 two 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,*,~\isa{{\isasymdots}}~\verb,*,\verb,),, essentially act like

  white space and do not really contribute to the content.  They

  mainly serve technical purposes to mark certain oddities in the raw

  input text.  In contrast, \bfindex{formal comments} are portions of

  text that are associated with formal Isabelle/Isar commands

  (\bfindex{marginal comments}), or as standalone paragraphs within a

  theory or proof context (\bfindex{text blocks}).

  \medskip Marginal comments are part of each command's concrete

  syntax \cite{isabelle-ref}; the common form is ``\verb,--,~$text$''

  where $text$ is delimited by \verb,",\isa{{\isasymdots}}\verb,", or

  \verb,{,\verb,*,~\isa{{\isasymdots}}~\verb,*,\verb,}, as before.  Multiple

  marginal comments may be given at the same time.  Here is a simple

  example:%

\end{isamarkuptext}%

\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.  This may be changed as follows:

\begin{verbatim}

  \renewcommand{\isastyletxt}{\isastyletext}

\end{verbatim}

  \medskip The $text$ part of Isabelle markup commands 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.  Quoted text blocks together with antiquotations provide

  an attractive means of referring to 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$} each.  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 This sentence demonstrates quotations and antiquotations:

  \isa{{\isasymlambda}x\ y{\isachardot}\ x} is a well-typed term.

  \medskip\noindent The output above was produced as follows:

  \begin{ttbox}

text {\ttlbrace}*

  This sentence demonstrates quotations and antiquotations:

  {\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term.

*{\ttrbrace}

  \end{ttbox}\vspace{-\medskipamount}

  The notational change from the ASCII character~\verb,%, to the

  symbol~\isa{{\isasymlambda}} reveals that Isabelle printed this term, after

  parsing and type-checking.  Document preparation enables symbolic

  output by default.

  \medskip The next example includes an option to modify Isabelle's

  \verb,show_types, flag.  The antiquotation

  \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces the

  output \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.  Terms

  may acquire different typings due to constraints imposed by their

  environment; within a proof, for example, variables are given the

  same types as they have in the main goal statement.

  \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 $a$, print its name \\

  \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, independently of the term language of

  Isabelle.  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 use canonical glyphs for certain

  standard symbols \cite[appendix~A]{isabelle-sys}.

  The {\LaTeX} code produced from Isabelle text follows a simple

  scheme.  You can 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 directly, digits are passed as an

  argument to the \verb,\isadigit, macro, other characters are

  replaced by specifically named macros of the form

  \verb,\isacharXYZ,.

  \item Named symbols: \verb,\,\verb,<XYZ>, is turned into

  \verb,{\isasymXYZ},; note the additional braces.

  \item Named control symbols: \verb,\,\verb,<^XYZ>, is turned into

  \verb,\isactrlXYZ,; subsequent symbols may act as arguments if the

  control macro is defined accordingly.

  \end{enumerate}

  You may occasionally wish to give new {\LaTeX} interpretations of

  named symbols.  This merely requires an appropriate definition of

  \verb,\isasymXYZ,, for \verb,\,\verb,<XYZ>, (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} 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 load

  individual files directly in \texttt{root.tex}.  On the other hand,

  such an arrangement requires additional maintenance whenever the

  collection of theories changes.

  Alternatively, one may tune the theory loading process in

  \texttt{ROOT.ML} itself: traversal of the theory dependency graph

  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 be suppressed more selectively.  Research

  articles and slides usually do not include the formal content in

  full.  Delimiting \bfindex{ignored material} by the special source

  comments \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and

  \verb,(,\verb,*,\verb,>,\verb,*,\verb,), tells the document

  preparation system to suppress these parts; the formal checking of

  the theory is unchanged, of course.

  In this example, we hide a theory's \isakeyword{theory} and

  \isakeyword{end} brackets:

  \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 hide

  vital parts of a proof, pretending that things have been simpler

  than they really were.  For example, this ``fully automatic'' proof

  is actually a fake:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{lemma}\ {\isachardoublequote}x\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isacharless}\ x\ {\isacharasterisk}\ x{\isachardoublequote}\isanewline

\ \ \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: zero_less_mult_iff(*>*))

\end{verbatim}

%(*

  \medskip Suppressing portions of printed text demands care.  You

  should not misrepresent the underlying theory development.  It is

  easy to invalidate the visible text by hiding references to

  questionable axioms.

  Authentic reports of Isabelle/Isar theories, say as part of a

  library, should suppress nothing.  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 few

  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 easy to hide

  the wrong parts, especially after rearranging the theory text.%

\end{isamarkuptext}%

\isamarkuptrue%

\isamarkupfalse%

\end{isabellebody}%

%%% Local Variables:

%%% mode: latex

%%% TeX-master: "root"

%%% End: