doc-src/TutorialI/Documents/document/Documents.tex

stylistic changes

%
\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} specifies nesting to the
  \emph{right}, reading \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} as \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}.  In contrast, a \emph{non-oriented} declaration via
  \isakeyword{infix} would render \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} illegal, but
  demand explicit parentheses to indicate the intended grouping.

  The string \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}} in 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 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}.  You 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 Replacing our definition of \isa{xor} by the following 
  specifies a 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 immediately be displayed.

  \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$, provided
  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 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}.  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 also works 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}%
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}

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

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

  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 these 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$}.  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}

  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.  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$\verb,>, is turned into
  \verb,{\isasym,$XYZ$\verb,},; note the additional braces.

  \item Named control symbols: \verb,\,\verb,<^,$XYZ$\verb,>, is
  turned into \verb,\isactrl,$XYZ$; subsequent symbols may act as
  arguments if the corresponding macro is defined accordingly.

  \end{enumerate}

  You may occasionally wish to give new {\LaTeX} interpretations of
  named symbols.  This merely requires an appropriate definition of
  \verb,\isasym,$XYZ$\verb,, for \verb,\,\verb,<,$XYZ$\verb,>, (see
  \texttt{isabelle.sty} for working examples).  Control symbols are
  slightly more difficult to get right, though.

  \medskip The \verb,\isabellestyle, macro provides a high-level
  interface to tune the general appearance of individual symbols.  For
  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.  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 document preparation is affected; the formal
  checking of the theory is unchanged.

  In this example, we suppress  a theory's uninteresting
  \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: int_less_le(*>*))
\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: