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

tuned;

%
\begin{isabellebody}%
\def\isabellecontext{Documents}%
\isamarkupfalse%
%
\isamarkupsection{Concrete Syntax \label{sec:concrete-syntax}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Concerning Isabelle's ``inner'' language of simply-typed \isa{{\isasymlambda}}-calculus, the core concept of Isabelle's elaborate
  infrastructure for concrete syntax is that of general
  \bfindex{mixfix annotations}.  Associated with any kind of constant
  declaration, mixfixes affect both the grammar productions for the
  parser and output templates for the pretty printer.

  In full generality, the whole affair of parser and pretty printer
  configuration is rather subtle, see also \cite{isabelle-ref}.  Any
  syntax specifications given by end-users need to interact properly
  with the existing setup of Isabelle/Pure and Isabelle/HOL.  It is
  particularly important to get the precedence of new syntactic
  constructs right, avoiding ambiguities with existing elements.

  \medskip Subsequently we introduce a few simple declaration forms
  that already cover the most 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
  (\isa{{\isacharasterisk}} and \isa{{\isacharplus}} types may come 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 string \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}} in the above annotation
  refers to the bit of concrete syntax to represent the operator,
  while the number \isa{{\isadigit{6}}{\isadigit{0}}} determines the precedence of the
  construct (i.e.\ the syntactic priorities of the arguments and
  result).

  As it happens, Isabelle/HOL already spends many popular combinations
  of ASCII symbols for its own use, including both \isa{{\isacharplus}} and
  \isa{{\isacharplus}{\isacharplus}}.  Slightly more awkward combinations like the present
  \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}} tend to be available for user extensions.  The current
  arrangement of inner syntax may be inspected via
  \commdx{print\protect\_syntax}, albeit its output is enormous.

  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.

  The keyword \isakeyword{infixl} specifies an operator that is nested
  to the \emph{left}: in iterated applications the more complex
  expression appears on the left-hand side: \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C}
  stands for \isa{{\isacharparenleft}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B{\isacharparenright}\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C}.  Similarly,
  \isakeyword{infixr} specifies to nesting to the \emph{right},
  reading \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} as \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}.  In
  contrast, a \emph{non-oriented} declaration via \isakeyword{infix}
  would have rendered \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} illegal, but demand
  explicit parentheses about the intended grouping.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\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 symbols.  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 by the user-interface of Proof~General + X-Symbol and the
  Isabelle document processor (see \S\ref{sec:document-preparation})
  display the \verb,\,\verb,<forall>, symbol really as \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
  shown as \isa{A\isactrlsup {\isasymstar}}.

  \medskip The following version of our \isa{xor} definition uses a
  standard Isabelle symbol to achieve typographically pleasing output.%
\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 \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.  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; an
  optional print mode specification may be given, too.  Note that the
  type declaration given here merely serves for syntactic purposes,
  and is not checked for consistency with the real constant.

  \medskip We may now write either \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}} or \isa{{\isasymoplus}} in
  input, while output uses the nicer syntax of $xsymbols$, provided
  that print mode is presently active.  Such an arrangement is
  particularly useful for interactive development, where users may
  type plain ASCII text, but gain improved visual feedback from the
  system (say in current goal output).

  \begin{warn}
  Alternative syntax declarations are apt to result in varying
  occurrences of concrete syntax in the input sources.  Isabelle
  provides no systematic way to convert alternative syntax expressions
  back and forth; print modes only affect situations where formal
  entities are pretty printed by the Isabelle process (e.g.\ output of
  terms and types), but not the original theory text.
  \end{warn}

  \medskip The following variant makes the alternative \isa{{\isasymoplus}}
  notation only available for output.  Thus we may enforce input
  sources to refer to plain ASCII only, but effectively disable
  cut-and-paste from output as well.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{syntax}\ {\isacharparenleft}xsymbols\ \isakeyword{output}{\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%
%
\isamarkupsubsection{Prefix Annotations%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Prefix syntax annotations\index{prefix annotation} are just another
  degenerate form of general mixfixes \cite{isabelle-ref}, without any
  template arguments or priorities --- just some bits of literal
  syntax.  The following example illustrates this idea idea by
  associating common symbols with the constructors of a datatype.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{datatype}\ currency\ {\isacharequal}\isanewline
\ \ \ \ 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 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 for those situations where a
  particular constant application forms need to be decorated by
  concrete syntax; just reconsider \isa{xor\ A\ B} versus \isa{A\ {\isasymoplus}\ B} covered before.  Occasionally, the relationship between some
  piece of notation and its internal form is slightly more involved.
  Here the concept of \bfindex{syntax translations} enters the scene.

  Using the raw \isakeyword{syntax}\index{syntax (command)} command we
  may introduce uninterpreted notational elements, while
  \commdx{translations} relates the input forms with more complex
  logical expressions.  This essentially provides a simple mechanism
  for for syntactic macros; even heavier transformations may be
  written in ML \cite{isabelle-ref}.

  \medskip A typical example of syntax translations is to decorate
  relational expressions 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.

  The Isar proof language \cite{Wenzel-PhD}, which is not covered in
  this book, admits to write formal proof texts that are acceptable
  both to the machine and human readers at the same time.  Thus
  marginal comments and explanations may be kept at a minimum.  Even
  without proper coverage of human-readable proofs, Isabelle document
  is very useful to produce formally derived texts.  Unstructured
  proof scripts given here may be just ignored by readers, or
  intentionally suppressed from the text by the writer (see also
  \S\ref{sec:doc-prep-suppress}).

  \medskip The Isabelle document preparation system essentially acts
  like a formal front-end to {\LaTeX}.  After checking specifications
  and proofs, the theory sources are turned into typesetting
  instructions in a well-defined manner.  This enables users to write
  authentic reports on formal developments with little effort, most
  tedious consistency checks are handled by the system.%
\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} essentially consists of a
  collection of theory source files that contribute to a single output
  document eventually.  Session is derived from a single parent each
  (usually an object-logic image like \texttt{HOL}), resulting in an
  overall tree structure that is reflected in the output location
  within the file system (usually rooted at
  \verb,~/isabelle/browser_info,).

  Here is the canonical arrangement of sources of a session called
  \texttt{MySession}:

  \begin{itemize}

  \item Directory \texttt{MySession} contains 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
  theory 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.  The generated
  \texttt{session.tex} will hold {\LaTeX} commands to include all
  theory output files in topologically sorted order, so
  \verb,\input{session}, in \texttt{root.tex} will do it in most
  situations.

  \item \texttt{IsaMakefile} outside of the directory
  \texttt{MySession} 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}

  With everything put in its proper place, \texttt{isatool make}
  should be sufficient to process the Isabelle session completely,
  with the generated document appearing in its proper place.

  \medskip In reality, users may want to have \texttt{isatool mkdir}
  generate an initial working setup without further ado.  For example,
  an empty session \texttt{MySession} derived from \texttt{HOL} may be
  produced as follows:

\begin{verbatim}
  isatool mkdir HOL MySession
  isatool make
\end{verbatim}

  This processes the session with sensible default options, including
  verbose mode to tell the user where the ultimate results will
  appear.  The above dry run should produce should already be able to
  produce a single page of output (with a dummy title, empty table of
  contents etc.).  Any failure at that stage is likely to indicate
  technical problems with the user's {\LaTeX}
  installation.\footnote{Especially make sure that \texttt{pdflatex}
  is present; if all fails one may fall back on DVI output by changing
  \texttt{usedir} options \cite{isabelle-sys}.}

  \medskip One may now start to populate the directory
  \texttt{MySession}, and the file \texttt{MySession/ROOT.ML}
  accordingly.  \texttt{MySession/document/root.tex} should be also
  adapted at some point; the default version is mostly
  self-explanatory.  Note that the \verb,\isabellestyle, enables
  fine-tuning of the general appearance of characters and mathematical
  symbols (see also \S\ref{sec:doc-prep-symbols}).

  Especially note the standard inclusion of {\LaTeX} packages
  \texttt{isabelle} (mandatory), and \texttt{isabellesym} (required
  for mathematical symbols), and the final \texttt{pdfsetup} (provides
  handsome defaults for \texttt{hyperref}, including URL markup).
  Further {\LaTeX} packages further packages may required in
  particular applications, e.g.\ for unusual Isabelle symbols.

  \medskip Further auxiliary files for the {\LaTeX} stage should be
  included in the \texttt{MySession/document} directory, e.g.\
  additional {\TeX} sources or graphics.  In particular, adding
  \texttt{root.bib} here (with that specific name) causes an automatic
  run of \texttt{bibtex} to process a bibliographic database; see for
  further commodities \texttt{isatool document} covered in
  \cite{isabelle-sys}.

  \medskip Any failure of the document preparation phase in an
  Isabelle batch session leaves the generated sources in there target
  location (as pointed out by the accompanied error message).  In case
  of {\LaTeX} errors, users may trace error messages at the file
  position of the generated text.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\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 effect the formal content 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 adaption, e.g.\
  moving it up in the hierarchy to become \verb,\chapter,.

\begin{verbatim}
  \renewcommand{\isamarkupheader}[1]{\chapter{#1}}
\end{verbatim}

  \noindent Certainly, this requires to change the default
  \verb,\documentclass{article}, in \texttt{root.tex} to something
  that supports the notion of chapters in the first place, e.g.\
  \verb,\documentclass{report},.

  \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to
  hold the name of the current theory context.  This is particularly
  useful for document headings:

\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%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
Isabelle 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 stanalone 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 usual.  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} view, ``\verb,--,'' acts like a markup command,
  the corresponding macro is \verb,\isamarkupcmt, (with 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).  The exact behavior may be changed by redefining
  the {\LaTeX} environments of \verb,isamarkuptext, or
  \verb,isamarkuptxt,, respectively.  The text style of the body is
  determined by the \verb,\isastyletext, and \verb,\isastyletxt,
  macros; the default uses a smaller font within proofs.

  \medskip The $text$ part of each of the various markup commands
  considered so far essentially inserts quoted material within a
  formal text, mainly for instruction of the reader (arbitrary
  {\LaTeX} macros may be also included).  An \bfindex{antiquotation}
  is again a formal object that has been 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 handsome means to reference formal
  entities with good confidence in technical details (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$} pair \cite{isabelle-isar-ref}.  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}.  Here type-inference has figured out the
  most general typings in the present (theory) context.  Note that
  term fragments may acquire a different typings due to constraints
  imposed by previous text (within a proof), say by the main goal
  statement given before hand.

  \medskip Several further kinds of antiquotations (and options) are
  available \cite{isabelle-sys}.  Here are a few commonly used
  combinations are as follows:

  \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 validity 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 type-setting, 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 the smallest syntactic entities, a
  straight-forward generalization of ASCII characters.  While Isabelle
  does not impose any interpretation of the infinite collection of
  symbols, the {\LaTeX} document output produces the canonical output
  for certain standard symbols \cite[appendix~A]{isabelle-sys}.

  The {\LaTeX} code produced from Isabelle text follows a relatively
  simple scheme (see below).  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).  See
  \cite[appendix~A]{isabelle-sys} and \texttt{isabellesym.sty} for the
  collection of predefined standard symbols.

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

  Users may occasionally wish to invent new named symbols; this merely
  requires an appropriate definition of \verb,\,\verb,<,$XYZ$\verb,>,
  as far as {\LaTeX} output is concerned.  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 italics fonts to mimic the
  general appearance of the {\LaTeX} math mode; double quotes are not
  printed at all.  The resulting quality of type-setting is quite
  good, so this should probably be the default style for real
  production 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 happens to get loaded during 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 of appearance
  or suppress unwanted theories by ignoring \texttt{session.tex} and
  include individual files in \texttt{root.tex} by hand.  On the other
  hand, such an arrangement requires additional maintenance chores
  whenever the collection of theories changes.

  Alternatively, one may tune the theory loading process in
  \texttt{ROOT.ML} itself: traversal of the theory dependency graph
  may be fine-tuned by adding further \verb,use_thy, invocations,
  although topological sorting still has to be observed.  Moreover,
  the ML operator \verb,no_document, temporarily disables document
  generation while executing a theory loader command; its usage is
  like this:

\begin{verbatim}
  no_document use_thy "T";
\end{verbatim}

  \medskip Theory output may be also suppressed in smaller portions as
  well.  For example, research papers or slides usually do not include
  the formal content in full.  In order to delimit \bfindex{ignored
  material} special source comments
  \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
  \verb,(,\verb,*,\verb,>,\verb,*,\verb,), may be included in the
  text.  Only the document preparation system is affected, the formal
  checking the theory is performed as before.

  In the following example we suppress the slightly formalistic
  \isakeyword{theory} + \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.  For example, we
  may even drop vital parts of a formal proof, pretending that things
  have been simpler than in reality.  For example, the following
  ``fully automatic'' proof is actually a fake:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\ {\isachardoublequote}x\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isacharless}\ x\ {\isacharasterisk}\ x{\isachardoublequote}\isanewline
\ \ \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 does demand some care by the
  user.  First of all, the writer is responsible not to obfuscate the
  underlying formal development in an unduly manner.  It is fairly
  easy to invalidate the remaining visible text, e.g.\ by referencing
  questionable formal items (strange definitions, arbitrary axioms
  etc.) that have been hidden from sight beforehand.

  Some minor technical subtleties of the
  \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),
  elements need to be kept in mind as well, since the system performs
  little sanity checks here.  Arguments of markup commands and formal
  comments must not be hidden, otherwise presentation fails.  Open and
  close parentheses need to be inserted carefully; it is fairly easy
  to hide the wrong parts, especially after rearranging the sources.

  \medskip Authentic reports of formal theories, say as part of a
  library, usually should refrain from suppressing parts of the text
  at all.  Other users may need the full information for their own
  derivative work.  If a particular formalization appears inadequate
  for general public coverage, it is often more appropriate to think
  of a better way in the first place.%
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: