
wenzelm@11648: %
wenzelm@11648: \begin{isabellebody}%
wenzelm@11648: \def\isabellecontext{Documents}%
wenzelm@11866: \isamarkupfalse%
wenzelm@12627: %
wenzelm@12647: \isamarkupsection{Concrete Syntax \label{sec:concrete-syntax}%
wenzelm@12627: }
wenzelm@12627: \isamarkuptrue%
wenzelm@12627: %
wenzelm@12627: \begin{isamarkuptext}%
wenzelm@12767: The core concept of Isabelle's framework for concrete syntax is that
wenzelm@12767:   of \bfindex{mixfix annotations}.  Associated with any kind of
wenzelm@12767:   constant declaration, mixfixes affect both the grammar productions
wenzelm@12767:   for the parser and output templates for the pretty printer.
wenzelm@12627: 
wenzelm@12743:   In full generality, parser and pretty printer configuration is a
wenzelm@12767:   subtle affair \cite{isabelle-ref}.  Your syntax specifications need
wenzelm@12767:   to interact properly with the existing setup of Isabelle/Pure and
wenzelm@12767:   Isabelle/HOL\@.  To avoid creating ambiguities with existing
wenzelm@12767:   elements, it is particularly important to give new syntactic
paulson@12764:   constructs the right precedence.
wenzelm@12627: 
wenzelm@12671:   \medskip Subsequently we introduce a few simple syntax declaration
wenzelm@12743:   forms that already cover many common situations fairly well.%
wenzelm@12627: \end{isamarkuptext}%
wenzelm@12627: \isamarkuptrue%
wenzelm@12627: %
wenzelm@12647: \isamarkupsubsection{Infix Annotations%
wenzelm@12627: }
wenzelm@12627: \isamarkuptrue%
wenzelm@12627: %
wenzelm@12627: \begin{isamarkuptext}%
paulson@12764: Syntax annotations may be included wherever constants are declared,
wenzelm@12767:   such as \isacommand{consts} and \isacommand{constdefs} --- and also
wenzelm@12767:   \isacommand{datatype}, which declares constructor operations.
wenzelm@12767:   Type-constructors may be annotated as well, although this is less
wenzelm@12767:   frequently encountered in practice (the infix type \isa{{\isasymtimes}} comes
wenzelm@12767:   to mind).
wenzelm@12627: 
wenzelm@12644:   Infix declarations\index{infix annotations} provide a useful special
wenzelm@12767:   case of mixfixes.  The following example of the exclusive-or
wenzelm@12767:   operation on boolean values illustrates typical infix declarations.%
wenzelm@12627: \end{isamarkuptext}%
wenzelm@12627: \isamarkuptrue%
wenzelm@12627: \isacommand{constdefs}\isanewline
wenzelm@12627: \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
wenzelm@12627: \ \ {\isachardoublequote}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
wenzelm@12627: %
wenzelm@12627: \begin{isamarkuptext}%
wenzelm@12652: \noindent Now \isa{xor\ A\ B} and \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} refer to the
wenzelm@12652:   same expression internally.  Any curried function with at least two
wenzelm@12767:   arguments may be given infix syntax.  For partial applications with
wenzelm@12767:   fewer than two operands, there is a notation using the prefix~\isa{op}.  For instance, \isa{xor} without arguments is represented as
wenzelm@12767:   \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}}; together with ordinary function application, this
wenzelm@12652:   turns \isa{xor\ A} into \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ A}.
wenzelm@12627: 
wenzelm@12747:   \medskip The keyword \isakeyword{infixl} seen above specifies an
wenzelm@12747:   infix operator that is nested to the \emph{left}: in iterated
wenzelm@12747:   applications the more complex expression appears on the left-hand
wenzelm@12767:   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
wenzelm@12767:   \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}
wenzelm@12767:   would render \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} illegal, but demand explicit
wenzelm@12767:   parentheses to indicate the intended grouping.
wenzelm@12743: 
wenzelm@12747:   The string \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}} in our annotation refers to the
wenzelm@12747:   concrete syntax to represent the operator (a literal token), while
paulson@12764:   the number \isa{{\isadigit{6}}{\isadigit{0}}} determines the precedence of the construct:
wenzelm@12767:   the syntactic priorities of the arguments and result.  Isabelle/HOL
wenzelm@12767:   already uses up many popular combinations of ASCII symbols for its
wenzelm@12767:   own use, including both \isa{{\isacharplus}} and \isa{{\isacharplus}{\isacharplus}}.  Longer
wenzelm@12767:   character combinations are more likely to be still available for
wenzelm@12767:   user extensions, such as our~\isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}}.
wenzelm@12627: 
wenzelm@12767:   Operator precedences have a range of 0--1000.  Very low or high
wenzelm@12767:   priorities are reserved for the meta-logic.  HOL syntax mainly uses
wenzelm@12767:   the range of 10--100: the equality infix \isa{{\isacharequal}} is centered at
wenzelm@12767:   50; logical connectives (like \isa{{\isasymor}} and \isa{{\isasymand}}) are
wenzelm@12767:   below 50; algebraic ones (like \isa{{\isacharplus}} and \isa{{\isacharasterisk}}) are
wenzelm@12767:   above 50.  User syntax should strive to coexist with common HOL
wenzelm@12767:   forms, or use the mostly unused range 100--900.%
wenzelm@12627: \end{isamarkuptext}%
wenzelm@12627: \isamarkuptrue%
wenzelm@12635: %
wenzelm@12658: \isamarkupsubsection{Mathematical Symbols \label{sec:syntax-symbols}%
wenzelm@12635: }
wenzelm@12627: \isamarkuptrue%
wenzelm@12635: %
wenzelm@12635: \begin{isamarkuptext}%
wenzelm@12767: Concrete syntax based on ASCII characters has inherent limitations.
wenzelm@12767:   Mathematical notation demands a larger repertoire of glyphs.
wenzelm@12767:   Several standards of extended character sets have been proposed over
wenzelm@12767:   decades, but none has become universally available so far.  Isabelle
wenzelm@12767:   has its own notion of \bfindex{symbols} as the smallest entities of
wenzelm@12767:   source text, without referring to internal encodings.  There are
wenzelm@12767:   three kinds of such ``generalized characters'':
wenzelm@12635: 
wenzelm@12635:   \begin{enumerate}
wenzelm@12635: 
wenzelm@12652:   \item 7-bit ASCII characters
wenzelm@12635: 
wenzelm@12652:   \item named symbols: \verb,\,\verb,<,$ident$\verb,>,
wenzelm@12635: 
wenzelm@12652:   \item named control symbols: \verb,\,\verb,<^,$ident$\verb,>,
wenzelm@12635: 
wenzelm@12635:   \end{enumerate}
wenzelm@12635: 
wenzelm@12635:   Here $ident$ may be any identifier according to the usual Isabelle
wenzelm@12635:   conventions.  This results in an infinite store of symbols, whose
wenzelm@12767:   interpretation is left to further front-end tools.  For example, the
wenzelm@12767:   user-interface of Proof~General + X-Symbol and the Isabelle document
wenzelm@12767:   processor (see \S\ref{sec:document-preparation}) display the
wenzelm@12767:   \verb,\,\verb,<forall>, symbol as~\isa{{\isasymforall}}.
wenzelm@12635: 
wenzelm@12635:   A list of standard Isabelle symbols is given in
wenzelm@12767:   \cite[appendix~A]{isabelle-sys}.  You may introduce your own
wenzelm@12635:   interpretation of further symbols by configuring the appropriate
wenzelm@12652:   front-end tool accordingly, e.g.\ by defining certain {\LaTeX}
wenzelm@12652:   macros (see also \S\ref{sec:doc-prep-symbols}).  There are also a
wenzelm@12652:   few predefined control symbols, such as \verb,\,\verb,<^sub>, and
wenzelm@12635:   \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent
paulson@12764:   printable symbol, respectively.  For example, \verb,A\<^sup>\<star>, is
wenzelm@12671:   output as \isa{A\isactrlsup {\isasymstar}}.
wenzelm@12635: 
wenzelm@12767:   \medskip Replacing our definition of \isa{xor} by the following
nipkow@13439:   specifies an Isabelle symbol for the new operator:%
wenzelm@12635: \end{isamarkuptext}%
wenzelm@12627: \isamarkuptrue%
wenzelm@12627: \isamarkupfalse%
wenzelm@12627: \isamarkupfalse%
wenzelm@12635: \isacommand{constdefs}\isanewline
wenzelm@12635: \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
nipkow@13791: \ \ {\isachardoublequote}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
wenzelm@12627: \isamarkupfalse%
wenzelm@12635: %
wenzelm@12635: \begin{isamarkuptext}%
wenzelm@12652: \noindent The X-Symbol package within Proof~General provides several
wenzelm@12652:   input methods to enter \isa{{\isasymoplus}} in the text.  If all fails one may
wenzelm@12767:   just type a named entity \verb,\,\verb,<oplus>, by hand; the
wenzelm@12767:   corresponding symbol will be displayed after further input.
wenzelm@12635: 
wenzelm@12767:   \medskip More flexible is to provide alternative syntax forms
wenzelm@12767:   through the \bfindex{print mode} concept~\cite{isabelle-ref}.  By
wenzelm@12767:   convention, the mode of ``$xsymbols$'' is enabled whenever
wenzelm@12767:   Proof~General's X-Symbol mode or {\LaTeX} output is active.  Now
wenzelm@12767:   consider the following hybrid declaration of \isa{xor}:%
wenzelm@12635: \end{isamarkuptext}%
wenzelm@12627: \isamarkuptrue%
wenzelm@12627: \isamarkupfalse%
wenzelm@12635: \isamarkupfalse%
wenzelm@12635: \isacommand{constdefs}\isanewline
wenzelm@12635: \ \ 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
wenzelm@12635: \ \ {\isachardoublequote}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline
wenzelm@12635: \isanewline
wenzelm@12635: \isamarkupfalse%
wenzelm@12635: \isacommand{syntax}\ {\isacharparenleft}xsymbols{\isacharparenright}\isanewline
nipkow@13791: \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
wenzelm@12635: \isamarkupfalse%
wenzelm@12635: %
wenzelm@12635: \begin{isamarkuptext}%
wenzelm@12652: The \commdx{syntax} command introduced here acts like
wenzelm@12743:   \isakeyword{consts}, but without declaring a logical constant.  The
wenzelm@12747:   print mode specification of \isakeyword{syntax}, here \isa{{\isacharparenleft}xsymbols{\isacharparenright}}, is optional.  Also note that its type merely serves
wenzelm@12747:   for syntactic purposes, and is \emph{not} checked for consistency
wenzelm@12747:   with the real constant.
wenzelm@12635: 
wenzelm@12672:   \medskip We may now write \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} or \isa{A\ {\isasymoplus}\ B} in
wenzelm@12767:   input, while output uses the nicer syntax of $xsymbols$ whenever
wenzelm@12672:   that print mode is active.  Such an arrangement is particularly
wenzelm@12767:   useful for interactive development, where users may type ASCII text
wenzelm@12767:   and see mathematical symbols displayed during proofs.%
wenzelm@12635: \end{isamarkuptext}%
wenzelm@12627: \isamarkuptrue%
wenzelm@12635: %
wenzelm@12647: \isamarkupsubsection{Prefix Annotations%
wenzelm@12635: }
wenzelm@12627: \isamarkuptrue%
wenzelm@12635: %
wenzelm@12635: \begin{isamarkuptext}%
wenzelm@12767: Prefix syntax annotations\index{prefix annotation} are another form
wenzelm@12767:   of mixfixes \cite{isabelle-ref}, without any template arguments or
wenzelm@12767:   priorities --- just some literal syntax.  The following example
wenzelm@12767:   associates common symbols with the constructors of a datatype.%
wenzelm@12635: \end{isamarkuptext}%
wenzelm@12627: \isamarkuptrue%
wenzelm@12635: \isacommand{datatype}\ currency\ {\isacharequal}\isanewline
wenzelm@12635: \ \ \ \ Euro\ nat\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymeuro}{\isachardoublequote}{\isacharparenright}\isanewline
wenzelm@12635: \ \ {\isacharbar}\ Pounds\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isasympounds}{\isachardoublequote}{\isacharparenright}\isanewline
wenzelm@12635: \ \ {\isacharbar}\ Yen\ nat\ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymyen}{\isachardoublequote}{\isacharparenright}\isanewline
wenzelm@12635: \ \ {\isacharbar}\ Dollar\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isachardollar}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
wenzelm@12635: %
wenzelm@12635: \begin{isamarkuptext}%
wenzelm@12652: \noindent Here the mixfix annotations on the rightmost column happen
wenzelm@12652:   to consist of a single Isabelle symbol each: \verb,\,\verb,<euro>,,
wenzelm@12652:   \verb,\,\verb,<pounds>,, \verb,\,\verb,<yen>,, and \verb,$,.  Recall
wenzelm@12747:   that a constructor like \isa{Euro} actually is a function \isa{nat\ {\isasymRightarrow}\ currency}.  The expression \isa{Euro\ {\isadigit{1}}{\isadigit{0}}} will be
wenzelm@12652:   printed as \isa{{\isasymeuro}\ {\isadigit{1}}{\isadigit{0}}}; only the head of the application is
wenzelm@12743:   subject to our concrete syntax.  This rather simple form already
wenzelm@12743:   achieves conformance with notational standards of the European
wenzelm@12743:   Commission.
wenzelm@12635: 
wenzelm@12767:   Prefix syntax works the same way for \isakeyword{consts} or
paulson@12764:   \isakeyword{constdefs}.%
wenzelm@12649: \end{isamarkuptext}%
wenzelm@12649: \isamarkuptrue%
wenzelm@12649: %
wenzelm@12649: \isamarkupsubsection{Syntax Translations \label{sec:syntax-translations}%
wenzelm@12635: }
wenzelm@12627: \isamarkuptrue%
wenzelm@12635: %
wenzelm@12635: \begin{isamarkuptext}%
wenzelm@12767: Mixfix syntax annotations merely decorate particular constant
wenzelm@12767:   application forms with concrete syntax, for instance replacing \
wenzelm@12767:   \isa{xor\ A\ B} by \isa{A\ {\isasymoplus}\ B}.  Occasionally, the
wenzelm@12767:   relationship between some piece of notation and its internal form is
wenzelm@12767:   more complicated.  Here we need \bfindex{syntax translations}.
wenzelm@12635: 
paulson@12764:   Using the \isakeyword{syntax}\index{syntax (command)}, command we
paulson@12764:   introduce uninterpreted notational elements.  Then
paulson@12764:   \commdx{translations} relate input forms to complex logical
wenzelm@12767:   expressions.  This provides a simple mechanism for syntactic macros;
wenzelm@12767:   even heavier transformations may be written in ML
wenzelm@12671:   \cite{isabelle-ref}.
wenzelm@12649: 
paulson@12764:   \medskip A typical use of syntax translations is to introduce
wenzelm@12767:   relational notation for membership in a set of pair, replacing \
wenzelm@12767:   \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} by \isa{x\ {\isasymapprox}\ y}.%
wenzelm@12635: \end{isamarkuptext}%
wenzelm@12627: \isamarkuptrue%
wenzelm@12649: \isacommand{consts}\isanewline
wenzelm@12649: \ \ sim\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set{\isachardoublequote}\isanewline
wenzelm@12649: \isanewline
wenzelm@12649: \isamarkupfalse%
wenzelm@12649: \isacommand{syntax}\isanewline
wenzelm@12649: \ \ {\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
wenzelm@12649: \isamarkupfalse%
wenzelm@12649: \isacommand{translations}\isanewline
wenzelm@12649: \ \ {\isachardoublequote}x\ {\isasymapprox}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim{\isachardoublequote}\isamarkupfalse%
wenzelm@12635: %
wenzelm@12635: \begin{isamarkuptext}%
wenzelm@12649: \noindent Here the name of the dummy constant \isa{{\isacharunderscore}sim} does
wenzelm@12767:   not matter, as long as it is not used elsewhere.  Prefixing an
wenzelm@12767:   underscore is a common convention.  The \isakeyword{translations}
wenzelm@12649:   declaration already uses concrete syntax on the left-hand side;
wenzelm@12649:   internally we relate a raw application \isa{{\isacharunderscore}sim\ x\ y} with
wenzelm@12649:   \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim}.
wenzelm@12635: 
wenzelm@12652:   \medskip Another common application of syntax translations is to
wenzelm@12649:   provide variant versions of fundamental relational expressions, such
wenzelm@12649:   as \isa{{\isasymnoteq}} for negated equalities.  The following declaration
wenzelm@12649:   stems from Isabelle/HOL itself:%
wenzelm@12649: \end{isamarkuptext}%
wenzelm@12649: \isamarkuptrue%
wenzelm@12649: \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
wenzelm@12649: \isamarkupfalse%
wenzelm@12649: \isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}{\isasymignore}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
wenzelm@12649: %
wenzelm@12649: \begin{isamarkuptext}%
wenzelm@12649: \noindent Normally one would introduce derived concepts like this
wenzelm@12652:   within the logic, using \isakeyword{consts} + \isakeyword{defs}
wenzelm@12652:   instead of \isakeyword{syntax} + \isakeyword{translations}.  The
wenzelm@12649:   present formulation has the virtue that expressions are immediately
wenzelm@12666:   replaced by the ``definition'' upon parsing; the effect is reversed
wenzelm@12666:   upon printing.
wenzelm@12649: 
wenzelm@12767:   This sort of translation is appropriate when the defined concept is
wenzelm@12767:   a trivial variation on an existing one.  On the other hand, syntax
wenzelm@12767:   translations do not scale up well to large hierarchies of concepts.
wenzelm@12767:   Translations do not replace definitions!%
wenzelm@12635: \end{isamarkuptext}%
wenzelm@12627: \isamarkuptrue%
wenzelm@12635: %
wenzelm@12652: \isamarkupsection{Document Preparation \label{sec:document-preparation}%
wenzelm@12635: }
wenzelm@12627: \isamarkuptrue%
wenzelm@12635: %
wenzelm@12644: \begin{isamarkuptext}%
wenzelm@12652: Isabelle/Isar is centered around the concept of \bfindex{formal
wenzelm@12767:   proof documents}\index{documents|bold}.  The outcome of a formal
wenzelm@12767:   development effort is meant to be a human-readable record, presented
wenzelm@12767:   as browsable PDF file or printed on paper.  The overall document
wenzelm@12767:   structure follows traditional mathematical articles, with sections,
wenzelm@12767:   intermediate explanations, definitions, theorems and proofs.
wenzelm@12644: 
wenzelm@12644:   \medskip The Isabelle document preparation system essentially acts
wenzelm@12671:   as a front-end to {\LaTeX}.  After checking specifications and
wenzelm@12671:   proofs formally, the theory sources are turned into typesetting
wenzelm@12767:   instructions in a schematic manner.  This lets you write authentic
wenzelm@12767:   reports on theory developments with little effort: many technical
wenzelm@12767:   consistency checks are handled by the system.
wenzelm@12745: 
wenzelm@12745:   Here is an example to illustrate the idea of Isabelle document
wenzelm@12747:   preparation.%
wenzelm@12747: \end{isamarkuptext}%
wenzelm@12747: \isamarkuptrue%
wenzelm@12747: %
wenzelm@12747: \begin{quotation}
wenzelm@12747: %
wenzelm@12747: \begin{isamarkuptext}%
wenzelm@12747: The following datatype definition of \isa{{\isacharprime}a\ bintree} models
wenzelm@12747:   binary trees with nodes being decorated by elements of type \isa{{\isacharprime}a}.%
wenzelm@12745: \end{isamarkuptext}%
wenzelm@12745: \isamarkuptrue%
wenzelm@12745: \isacommand{datatype}\ {\isacharprime}a\ bintree\ {\isacharequal}\isanewline
wenzelm@12747: \ \ \ \ \ Leaf\ {\isacharbar}\ Branch\ {\isacharprime}a\ \ {\isachardoublequote}{\isacharprime}a\ bintree{\isachardoublequote}\ \ {\isachardoublequote}{\isacharprime}a\ bintree{\isachardoublequote}\isamarkupfalse%
wenzelm@12745: %
wenzelm@12745: \begin{isamarkuptext}%
wenzelm@12745: \noindent The datatype induction rule generated here is of the form
wenzelm@12745:   \begin{isabelle}%
wenzelm@12749: \ {\isasymlbrakk}P\ Leaf{\isacharsemicolon}\isanewline
paulson@14379: \isaindent{\ \ }{\isasymAnd}a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isachardot}\isanewline
paulson@14379: \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
wenzelm@12749: \isaindent{\ }{\isasymLongrightarrow}\ P\ bintree%
wenzelm@12747: \end{isabelle}%
wenzelm@12747: \end{isamarkuptext}%
wenzelm@12747: \isamarkuptrue%
wenzelm@12747: %
wenzelm@12747: \end{quotation}
wenzelm@12747: %
wenzelm@12747: \begin{isamarkuptext}%
wenzelm@12767: \noindent The above document output has been produced as follows:
wenzelm@12745: 
wenzelm@12745:   \begin{ttbox}
wenzelm@12745:   text {\ttlbrace}*
wenzelm@12745:     The following datatype definition of {\at}{\ttlbrace}text "'a bintree"{\ttrbrace}
wenzelm@12745:     models binary trees with nodes being decorated by elements
wenzelm@12745:     of type {\at}{\ttlbrace}typ 'a{\ttrbrace}.
wenzelm@12745:   *{\ttrbrace}
wenzelm@12745: 
wenzelm@12745:   datatype 'a bintree =
wenzelm@12745:     Leaf | Branch 'a  "'a bintree"  "'a bintree"
wenzelm@12767:   \end{ttbox}
wenzelm@12767:   \begin{ttbox}
wenzelm@12745:   text {\ttlbrace}*
wenzelm@12745:     {\ttback}noindent The datatype induction rule generated here is
wenzelm@12745:     of the form {\at}{\ttlbrace}thm [display] bintree.induct [no_vars]{\ttrbrace}
wenzelm@12745:   *{\ttrbrace}
wenzelm@12767:   \end{ttbox}\vspace{-\medskipamount}
wenzelm@12745: 
wenzelm@12747:   \noindent Here we have augmented the theory by formal comments
wenzelm@12767:   (using \isakeyword{text} blocks), the informal parts may again refer
wenzelm@12767:   to formal entities by means of ``antiquotations'' (such as
wenzelm@12745:   \texttt{\at}\verb,{text "'a bintree"}, or
wenzelm@12747:   \texttt{\at}\verb,{typ 'a},), see also \S\ref{sec:doc-prep-text}.%
wenzelm@12644: \end{isamarkuptext}%
wenzelm@12635: \isamarkuptrue%
wenzelm@12635: %
wenzelm@12647: \isamarkupsubsection{Isabelle Sessions%
wenzelm@12635: }
wenzelm@12635: \isamarkuptrue%
wenzelm@12635: %
wenzelm@12635: \begin{isamarkuptext}%
wenzelm@12652: In contrast to the highly interactive mode of Isabelle/Isar theory
wenzelm@12652:   development, the document preparation stage essentially works in
wenzelm@12671:   batch-mode.  An Isabelle \bfindex{session} consists of a collection
wenzelm@12767:   of source files that may contribute to an output document.  Each
wenzelm@12767:   session is derived from a single parent, usually an object-logic
wenzelm@12767:   image like \texttt{HOL}.  This results in an overall tree structure,
wenzelm@12767:   which is reflected by the output location in the file system
wenzelm@12767:   (usually rooted at \verb,~/isabelle/browser_info,).
wenzelm@12644: 
wenzelm@12684:   \medskip The easiest way to manage Isabelle sessions is via
wenzelm@12686:   \texttt{isatool mkdir} (generates an initial session source setup)
wenzelm@12686:   and \texttt{isatool make} (run sessions controlled by
wenzelm@12684:   \texttt{IsaMakefile}).  For example, a new session
wenzelm@12684:   \texttt{MySession} derived from \texttt{HOL} may be produced as
wenzelm@12684:   follows:
wenzelm@12684: 
wenzelm@12684: \begin{verbatim}
wenzelm@12684:   isatool mkdir HOL MySession
wenzelm@12684:   isatool make
wenzelm@12684: \end{verbatim}
wenzelm@12684: 
wenzelm@12686:   The \texttt{isatool make} job also informs about the file-system
wenzelm@12686:   location of the ultimate results.  The above dry run should be able
wenzelm@12686:   to produce some \texttt{document.pdf} (with dummy title, empty table
wenzelm@12743:   of contents etc.).  Any failure at this stage usually indicates
wenzelm@12686:   technical problems of the {\LaTeX} installation.\footnote{Especially
wenzelm@12767:   make sure that \texttt{pdflatex} is present; if in doubt one may
wenzelm@12686:   fall back on DVI output by changing \texttt{usedir} options in
wenzelm@12686:   \texttt{IsaMakefile} \cite{isabelle-sys}.}
wenzelm@12684: 
wenzelm@12684:   \medskip The detailed arrangement of the session sources is as
wenzelm@12747:   follows.
wenzelm@12644: 
wenzelm@12644:   \begin{itemize}
wenzelm@12644: 
wenzelm@12671:   \item Directory \texttt{MySession} holds the required theory files
wenzelm@12671:   $T@1$\texttt{.thy}, \dots, $T@n$\texttt{.thy}.
wenzelm@12644: 
wenzelm@12644:   \item File \texttt{MySession/ROOT.ML} holds appropriate ML commands
wenzelm@12644:   for loading all wanted theories, usually just
wenzelm@12666:   ``\texttt{use_thy"$T@i$";}'' for any $T@i$ in leaf position of the
wenzelm@12671:   dependency graph.
wenzelm@12644: 
wenzelm@12644:   \item Directory \texttt{MySession/document} contains everything
wenzelm@12652:   required for the {\LaTeX} stage; only \texttt{root.tex} needs to be
wenzelm@12652:   provided initially.
wenzelm@12644: 
wenzelm@12652:   The latter file holds appropriate {\LaTeX} code to commence a
wenzelm@12652:   document (\verb,\documentclass, etc.), and to include the generated
wenzelm@12743:   files $T@i$\texttt{.tex} for each theory.  Isabelle will generate a
wenzelm@12743:   file \texttt{session.tex} holding {\LaTeX} commands to include all
wenzelm@12747:   generated theory output files in topologically sorted order, so
wenzelm@12747:   \verb,\input{session}, in the body of \texttt{root.tex} does the job
wenzelm@12747:   in most situations.
wenzelm@12652: 
wenzelm@12682:   \item \texttt{IsaMakefile} holds appropriate dependencies and
wenzelm@12682:   invocations of Isabelle tools to control the batch job.  In fact,
wenzelm@12747:   several sessions may be managed by the same \texttt{IsaMakefile}.
paulson@12764:   See the \emph{Isabelle System Manual} \cite{isabelle-sys} 
paulson@12764:   for further details, especially on
wenzelm@12652:   \texttt{isatool usedir} and \texttt{isatool make}.
wenzelm@12644: 
wenzelm@12644:   \end{itemize}
wenzelm@12644: 
wenzelm@12686:   One may now start to populate the directory \texttt{MySession}, and
wenzelm@12767:   the file \texttt{MySession/ROOT.ML} accordingly.  The file
wenzelm@12767:   \texttt{MySession/document/root.tex} should also be adapted at some
wenzelm@12686:   point; the default version is mostly self-explanatory.  Note that
wenzelm@12686:   \verb,\isabellestyle, enables fine-tuning of the general appearance
wenzelm@12686:   of characters and mathematical symbols (see also
wenzelm@12686:   \S\ref{sec:doc-prep-symbols}).
wenzelm@12644: 
wenzelm@12686:   Especially observe the included {\LaTeX} packages \texttt{isabelle}
wenzelm@12686:   (mandatory), \texttt{isabellesym} (required for mathematical
wenzelm@12743:   symbols), and the final \texttt{pdfsetup} (provides sane defaults
paulson@12764:   for \texttt{hyperref}, including URL markup).  All three are
wenzelm@12743:   distributed with Isabelle. Further packages may be required in
paulson@12764:   particular applications, say for unusual mathematical symbols.
wenzelm@12644: 
wenzelm@12747:   \medskip Any additional files for the {\LaTeX} stage go into the
wenzelm@12747:   \texttt{MySession/document} directory as well.  In particular,
wenzelm@12767:   adding a file named \texttt{root.bib} causes an automatic run of
wenzelm@12767:   \texttt{bibtex} to process a bibliographic database; see also
wenzelm@12767:   \texttt{isatool document} \cite{isabelle-sys}.
wenzelm@12652: 
wenzelm@12652:   \medskip Any failure of the document preparation phase in an
wenzelm@12671:   Isabelle batch session leaves the generated sources in their target
wenzelm@12767:   location, identified by the accompanying error message.  This lets
wenzelm@12767:   you trace {\LaTeX} problems with the generated files at hand.%
wenzelm@12644: \end{isamarkuptext}%
wenzelm@12644: \isamarkuptrue%
wenzelm@12644: %
wenzelm@12647: \isamarkupsubsection{Structure Markup%
wenzelm@12644: }
wenzelm@12644: \isamarkuptrue%
wenzelm@12644: %
wenzelm@12644: \begin{isamarkuptext}%
wenzelm@12652: The large-scale structure of Isabelle documents follows existing
wenzelm@12652:   {\LaTeX} conventions, with chapters, sections, subsubsections etc.
wenzelm@12652:   The Isar language includes separate \bfindex{markup commands}, which
wenzelm@12682:   do not affect the formal meaning of a theory (or proof), but result
wenzelm@12666:   in corresponding {\LaTeX} elements.
wenzelm@12644: 
wenzelm@12666:   There are separate markup commands depending on the textual context:
wenzelm@12666:   in header position (just before \isakeyword{theory}), within the
wenzelm@12666:   theory body, or within a proof.  The header needs to be treated
wenzelm@12666:   specially here, since ordinary theory and proof commands may only
wenzelm@12666:   occur \emph{after} the initial \isakeyword{theory} specification.
wenzelm@12644: 
wenzelm@12666:   \medskip
wenzelm@12644: 
wenzelm@12644:   \begin{tabular}{llll}
wenzelm@12644:   header & theory & proof & default meaning \\\hline
wenzelm@12644:     & \commdx{chapter} & & \verb,\chapter, \\
wenzelm@12644:   \commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\
wenzelm@12644:     & \commdx{subsection} & \commdx{subsect} & \verb,\subsection, \\
wenzelm@12644:     & \commdx{subsubsection} & \commdx{subsubsect} & \verb,\subsubsection, \\
wenzelm@12644:   \end{tabular}
wenzelm@12644: 
wenzelm@12644:   \medskip
wenzelm@12644: 
wenzelm@12644:   From the Isabelle perspective, each markup command takes a single
wenzelm@12747:   $text$ argument (delimited by \verb,",~\isa{{\isasymdots}}~\verb,", or
wenzelm@12747:   \verb,{,\verb,*,~\isa{{\isasymdots}}~\verb,*,\verb,},).  After stripping any
wenzelm@12644:   surrounding white space, the argument is passed to a {\LaTeX} macro
wenzelm@12767:   \verb,\isamarkupXYZ, for command \isakeyword{XYZ}.  These macros are
wenzelm@12767:   defined in \verb,isabelle.sty, according to the meaning given in the
wenzelm@12767:   rightmost column above.
wenzelm@12644: 
wenzelm@12644:   \medskip The following source fragment illustrates structure markup
wenzelm@12652:   of a theory.  Note that {\LaTeX} labels may be included inside of
wenzelm@12652:   section headings as well.
wenzelm@12644: 
wenzelm@12644:   \begin{ttbox}
wenzelm@12644:   header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
wenzelm@12644: 
wenzelm@12644:   theory Foo_Bar = Main:
wenzelm@12644: 
wenzelm@12644:   subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
wenzelm@12644: 
wenzelm@12644:   consts
wenzelm@12644:     foo :: \dots
wenzelm@12644:     bar :: \dots
wenzelm@12647: 
wenzelm@12644:   defs \dots
wenzelm@12647: 
wenzelm@12644:   subsection {\ttlbrace}* Derived rules *{\ttrbrace}
wenzelm@12644: 
wenzelm@12644:   lemma fooI: \dots
wenzelm@12644:   lemma fooE: \dots
wenzelm@12644: 
wenzelm@12647:   subsection {\ttlbrace}* Main theorem {\ttback}label{\ttlbrace}sec:main-theorem{\ttrbrace} *{\ttrbrace}
wenzelm@12644: 
wenzelm@12644:   theorem main: \dots
wenzelm@12644: 
wenzelm@12644:   end
wenzelm@12767:   \end{ttbox}\vspace{-\medskipamount}
wenzelm@12644: 
wenzelm@12767:   You may occasionally want to change the meaning of markup commands,
wenzelm@12767:   say via \verb,\renewcommand, in \texttt{root.tex}.  For example,
wenzelm@12767:   \verb,\isamarkupheader, is a good candidate for some tuning.  We
wenzelm@12767:   could move it up in the hierarchy to become \verb,\chapter,.
wenzelm@12644: 
wenzelm@12644: \begin{verbatim}
wenzelm@12644:   \renewcommand{\isamarkupheader}[1]{\chapter{#1}}
wenzelm@12644: \end{verbatim}
wenzelm@12644: 
wenzelm@12767:   \noindent Now we must change the document class given in
wenzelm@12767:   \texttt{root.tex} to something that supports chapters.  A suitable
wenzelm@12767:   command is \verb,\documentclass{report},.
wenzelm@12644: 
wenzelm@12647:   \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to
wenzelm@12647:   hold the name of the current theory context.  This is particularly
wenzelm@12652:   useful for document headings:
wenzelm@12644: 
wenzelm@12644: \begin{verbatim}
wenzelm@12652:   \renewcommand{\isamarkupheader}[1]
wenzelm@12644:   {\chapter{#1}\markright{THEORY~\isabellecontext}}
wenzelm@12644: \end{verbatim}
wenzelm@12644: 
wenzelm@12644:   \noindent Make sure to include something like
wenzelm@12647:   \verb,\pagestyle{headings}, in \texttt{root.tex}; the document
paulson@12764:   should have more than two pages to show the effect.%
wenzelm@12644: \end{isamarkuptext}%
wenzelm@12644: \isamarkuptrue%
wenzelm@12644: %
wenzelm@12745: \isamarkupsubsection{Formal Comments and Antiquotations \label{sec:doc-prep-text}%
wenzelm@12644: }
wenzelm@12644: \isamarkuptrue%
wenzelm@12644: %
wenzelm@12644: \begin{isamarkuptext}%
wenzelm@12745: Isabelle \bfindex{source comments}, which are of the form
wenzelm@12747:   \verb,(,\verb,*,~\isa{{\isasymdots}}~\verb,*,\verb,),, essentially act like
wenzelm@12747:   white space and do not really contribute to the content.  They
wenzelm@12747:   mainly serve technical purposes to mark certain oddities in the raw
wenzelm@12747:   input text.  In contrast, \bfindex{formal comments} are portions of
wenzelm@12747:   text that are associated with formal Isabelle/Isar commands
wenzelm@12682:   (\bfindex{marginal comments}), or as standalone paragraphs within a
wenzelm@12666:   theory or proof context (\bfindex{text blocks}).
wenzelm@12658: 
wenzelm@12658:   \medskip Marginal comments are part of each command's concrete
wenzelm@12671:   syntax \cite{isabelle-ref}; the common form is ``\verb,--,~$text$''
wenzelm@12747:   where $text$ is delimited by \verb,",\isa{{\isasymdots}}\verb,", or
wenzelm@12747:   \verb,{,\verb,*,~\isa{{\isasymdots}}~\verb,*,\verb,}, as before.  Multiple
wenzelm@12671:   marginal comments may be given at the same time.  Here is a simple
wenzelm@12671:   example:%
wenzelm@12666: \end{isamarkuptext}%
wenzelm@12666: \isamarkuptrue%
wenzelm@12666: \isacommand{lemma}\ {\isachardoublequote}A\ {\isacharminus}{\isacharminus}{\isachargreater}\ A{\isachardoublequote}\isanewline
wenzelm@12666: \ \ %
wenzelm@12666: \isamarkupcmt{a triviality of propositional logic%
wenzelm@12666: }
wenzelm@12666: \isanewline
wenzelm@12666: \ \ %
wenzelm@12666: \isamarkupcmt{(should not really bother)%
wenzelm@12666: }
wenzelm@12666: \isanewline
wenzelm@12666: \ \ \isamarkupfalse%
wenzelm@12666: \isacommand{by}\ {\isacharparenleft}rule\ impI{\isacharparenright}\ %
wenzelm@12666: \isamarkupcmt{implicit assumption step involved here%
wenzelm@12666: }
wenzelm@12666: \isamarkupfalse%
wenzelm@12666: %
wenzelm@12666: \begin{isamarkuptext}%
wenzelm@12666: \noindent The above output has been produced as follows:
wenzelm@12658: 
wenzelm@12658: \begin{verbatim}
wenzelm@12658:   lemma "A --> A"
wenzelm@12658:     -- "a triviality of propositional logic"
wenzelm@12658:     -- "(should not really bother)"
wenzelm@12658:     by (rule impI) -- "implicit assumption step involved here"
wenzelm@12658: \end{verbatim}
wenzelm@12658: 
wenzelm@12671:   From the {\LaTeX} viewpoint, ``\verb,--,'' acts like a markup
wenzelm@12671:   command, associated with the macro \verb,\isamarkupcmt, (taking a
wenzelm@12671:   single argument).
wenzelm@12658: 
wenzelm@12666:   \medskip Text blocks are introduced by the commands \bfindex{text}
wenzelm@12666:   and \bfindex{txt}, for theory and proof contexts, respectively.
wenzelm@12666:   Each takes again a single $text$ argument, which is interpreted as a
wenzelm@12666:   free-form paragraph in {\LaTeX} (surrounded by some additional
wenzelm@12671:   vertical space).  This behavior may be changed by redefining the
wenzelm@12671:   {\LaTeX} environments of \verb,isamarkuptext, or
wenzelm@12671:   \verb,isamarkuptxt,, respectively (via \verb,\renewenvironment,) The
wenzelm@12671:   text style of the body is determined by \verb,\isastyletext, and
wenzelm@12671:   \verb,\isastyletxt,; the default setup uses a smaller font within
wenzelm@12747:   proofs.  This may be changed as follows:
wenzelm@12747: 
wenzelm@12747: \begin{verbatim}
wenzelm@12747:   \renewcommand{\isastyletxt}{\isastyletext}
wenzelm@12747: \end{verbatim}
wenzelm@12658: 
wenzelm@12767:   \medskip The $text$ part of Isabelle markup commands essentially
wenzelm@12767:   inserts \emph{quoted material} into a formal text, mainly for
wenzelm@12767:   instruction of the reader.  An \bfindex{antiquotation} is again a
wenzelm@12767:   formal object embedded into such an informal portion.  The
wenzelm@12767:   interpretation of antiquotations is limited to some well-formedness
wenzelm@12767:   checks, with the result being pretty printed to the resulting
wenzelm@12767:   document.  Quoted text blocks together with antiquotations provide
wenzelm@12767:   an attractive means of referring to formal entities, with good
wenzelm@12767:   confidence in getting the technical details right (especially syntax
wenzelm@12767:   and types).
wenzelm@12658: 
wenzelm@12666:   The general syntax of antiquotations is as follows:
wenzelm@12658:   \texttt{{\at}{\ttlbrace}$name$ $arguments${\ttrbrace}}, or
wenzelm@12658:   \texttt{{\at}{\ttlbrace}$name$ [$options$] $arguments${\ttrbrace}}
wenzelm@12666:   for a comma-separated list of options consisting of a $name$ or
wenzelm@12767:   \texttt{$name$=$value$} each.  The syntax of $arguments$ depends on
wenzelm@12767:   the kind of antiquotation, it generally follows the same conventions
wenzelm@12767:   for types, terms, or theorems as in the formal part of a theory.
wenzelm@12658: 
wenzelm@12767:   \medskip This sentence demonstrates quotations and antiquotations:
wenzelm@12767:   \isa{{\isasymlambda}x\ y{\isachardot}\ x} is a well-typed term.
wenzelm@12658: 
paulson@12764:   \medskip\noindent The output above was produced as follows:
wenzelm@12658:   \begin{ttbox}
wenzelm@12658: text {\ttlbrace}*
paulson@12764:   This sentence demonstrates quotations and antiquotations:
wenzelm@12658:   {\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term.
wenzelm@12658: *{\ttrbrace}
wenzelm@12767:   \end{ttbox}\vspace{-\medskipamount}
wenzelm@12658: 
paulson@12764:   The notational change from the ASCII character~\verb,%, to the
wenzelm@12767:   symbol~\isa{{\isasymlambda}} reveals that Isabelle printed this term, after
wenzelm@12767:   parsing and type-checking.  Document preparation enables symbolic
wenzelm@12767:   output by default.
wenzelm@12658: 
paulson@12764:   \medskip The next example includes an option to modify Isabelle's
paulson@12764:   \verb,show_types, flag.  The antiquotation
wenzelm@12767:   \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces the
wenzelm@12767:   output \isa{{\isasymlambda}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ y{\isasymColon}{\isacharprime}b{\isachardot}\ x}.  Type inference has figured
wenzelm@12767:   out the most general typings in the present theory context.  Terms
wenzelm@12767:   may acquire different typings due to constraints imposed by their
wenzelm@12767:   environment; within a proof, for example, variables are given the
wenzelm@12767:   same types as they have in the main goal statement.
wenzelm@12658: 
paulson@12764:   \medskip Several further kinds of antiquotations and options are
wenzelm@12666:   available \cite{isabelle-sys}.  Here are a few commonly used
wenzelm@12671:   combinations:
wenzelm@12658: 
wenzelm@12658:   \medskip
wenzelm@12658: 
wenzelm@12658:   \begin{tabular}{ll}
wenzelm@12658:   \texttt{\at}\verb,{typ,~$\tau$\verb,}, & print type $\tau$ \\
wenzelm@12658:   \texttt{\at}\verb,{term,~$t$\verb,}, & print term $t$ \\
wenzelm@12658:   \texttt{\at}\verb,{prop,~$\phi$\verb,}, & print proposition $\phi$ \\
wenzelm@12666:   \texttt{\at}\verb,{prop [display],~$\phi$\verb,}, & print large proposition $\phi$ (with linebreaks) \\
wenzelm@12658:   \texttt{\at}\verb,{prop [source],~$\phi$\verb,}, & check proposition $\phi$, print its input \\
wenzelm@12658:   \texttt{\at}\verb,{thm,~$a$\verb,}, & print fact $a$ \\
wenzelm@12658:   \texttt{\at}\verb,{thm,~$a$~\verb,[no_vars]}, & print fact $a$, fixing schematic variables \\
wenzelm@12747:   \texttt{\at}\verb,{thm [source],~$a$\verb,}, & check availability of fact $a$, print its name \\
wenzelm@12658:   \texttt{\at}\verb,{text,~$s$\verb,}, & print uninterpreted text $s$ \\
wenzelm@12658:   \end{tabular}
wenzelm@12658: 
wenzelm@12658:   \medskip
wenzelm@12658: 
wenzelm@12666:   Note that \attrdx{no_vars} given above is \emph{not} an
wenzelm@12666:   antiquotation option, but an attribute of the theorem argument given
wenzelm@12666:   here.  This might be useful with a diagnostic command like
wenzelm@12666:   \isakeyword{thm}, too.
wenzelm@12658: 
wenzelm@12666:   \medskip The \texttt{\at}\verb,{text, $s$\verb,}, antiquotation is
wenzelm@12658:   particularly interesting.  Embedding uninterpreted text within an
wenzelm@12666:   informal body might appear useless at first sight.  Here the key
wenzelm@12666:   virtue is that the string $s$ is processed as Isabelle output,
wenzelm@12666:   interpreting Isabelle symbols appropriately.
wenzelm@12658: 
wenzelm@12666:   For example, \texttt{\at}\verb,{text "\<forall>\<exists>"}, produces \isa{{\isasymforall}{\isasymexists}}, according to the standard interpretation of these symbol
wenzelm@12666:   (cf.\ \S\ref{sec:doc-prep-symbols}).  Thus we achieve consistent
wenzelm@12658:   mathematical notation in both the formal and informal parts of the
wenzelm@12767:   document very easily, independently of the term language of
wenzelm@12767:   Isabelle.  Manual {\LaTeX} code would leave more control over the
wenzelm@12767:   typesetting, but is also slightly more tedious.%
wenzelm@12644: \end{isamarkuptext}%
wenzelm@12644: \isamarkuptrue%
wenzelm@12644: %
wenzelm@12674: \isamarkupsubsection{Interpretation of Symbols \label{sec:doc-prep-symbols}%
wenzelm@12644: }
wenzelm@12644: \isamarkuptrue%
wenzelm@12644: %
wenzelm@12644: \begin{isamarkuptext}%
wenzelm@12666: As has been pointed out before (\S\ref{sec:syntax-symbols}),
wenzelm@12671:   Isabelle symbols are the smallest syntactic entities --- a
wenzelm@12682:   straightforward generalization of ASCII characters.  While Isabelle
wenzelm@12666:   does not impose any interpretation of the infinite collection of
paulson@12764:   named symbols, {\LaTeX} documents use canonical glyphs for certain
wenzelm@12671:   standard symbols \cite[appendix~A]{isabelle-sys}.
wenzelm@12658: 
wenzelm@12767:   The {\LaTeX} code produced from Isabelle text follows a simple
wenzelm@12767:   scheme.  You can tune the final appearance by redefining certain
wenzelm@12767:   macros, say in \texttt{root.tex} of the document.
wenzelm@12658: 
wenzelm@12671:   \begin{enumerate}
wenzelm@12671: 
wenzelm@12671:   \item 7-bit ASCII characters: letters \texttt{A\dots Z} and
wenzelm@12747:   \texttt{a\dots z} are output directly, digits are passed as an
wenzelm@12671:   argument to the \verb,\isadigit, macro, other characters are
wenzelm@12671:   replaced by specifically named macros of the form
wenzelm@12666:   \verb,\isacharXYZ,.
wenzelm@12658: 
wenzelm@12767:   \item Named symbols: \verb,\,\verb,<XYZ>, is turned into
wenzelm@12767:   \verb,{\isasymXYZ},; note the additional braces.
wenzelm@12658: 
wenzelm@12767:   \item Named control symbols: \verb,\,\verb,<^XYZ>, is turned into
wenzelm@12767:   \verb,\isactrlXYZ,; subsequent symbols may act as arguments if the
wenzelm@12767:   control macro is defined accordingly.
wenzelm@12671: 
wenzelm@12666:   \end{enumerate}
wenzelm@12666: 
paulson@12764:   You may occasionally wish to give new {\LaTeX} interpretations of
paulson@12764:   named symbols.  This merely requires an appropriate definition of
wenzelm@12767:   \verb,\isasymXYZ,, for \verb,\,\verb,<XYZ>, (see
wenzelm@12747:   \texttt{isabelle.sty} for working examples).  Control symbols are
wenzelm@12747:   slightly more difficult to get right, though.
wenzelm@12666: 
wenzelm@12666:   \medskip The \verb,\isabellestyle, macro provides a high-level
wenzelm@12666:   interface to tune the general appearance of individual symbols.  For
wenzelm@12671:   example, \verb,\isabellestyle{it}, uses the italics text style to
wenzelm@12671:   mimic the general appearance of the {\LaTeX} math mode; double
wenzelm@12743:   quotes are not printed at all.  The resulting quality of typesetting
wenzelm@12743:   is quite good, so this should be the default style for work that
wenzelm@12743:   gets distributed to a broader audience.%
wenzelm@12644: \end{isamarkuptext}%
wenzelm@12644: \isamarkuptrue%
wenzelm@12644: %
wenzelm@12652: \isamarkupsubsection{Suppressing Output \label{sec:doc-prep-suppress}%
wenzelm@12644: }
wenzelm@12644: \isamarkuptrue%
wenzelm@12644: %
wenzelm@12644: \begin{isamarkuptext}%
wenzelm@12749: By default, Isabelle's document system generates a {\LaTeX} file for
wenzelm@12749:   each theory that gets loaded while running the session.  The
wenzelm@12749:   generated \texttt{session.tex} will include all of these in order of
wenzelm@12749:   appearance, which in turn gets included by the standard
wenzelm@12743:   \texttt{root.tex}.  Certainly one may change the order or suppress
wenzelm@12747:   unwanted theories by ignoring \texttt{session.tex} and load
wenzelm@12747:   individual files directly in \texttt{root.tex}.  On the other hand,
wenzelm@12747:   such an arrangement requires additional maintenance whenever the
wenzelm@12747:   collection of theories changes.
wenzelm@12644: 
wenzelm@12647:   Alternatively, one may tune the theory loading process in
wenzelm@12652:   \texttt{ROOT.ML} itself: traversal of the theory dependency graph
wenzelm@12671:   may be fine-tuned by adding \verb,use_thy, invocations, although
wenzelm@12671:   topological sorting still has to be observed.  Moreover, the ML
wenzelm@12671:   operator \verb,no_document, temporarily disables document generation
wenzelm@12767:   while executing a theory loader command.  Its usage is like this:
wenzelm@12647: 
wenzelm@12647: \begin{verbatim}
wenzelm@12666:   no_document use_thy "T";
wenzelm@12647: \end{verbatim}
wenzelm@12647: 
wenzelm@12767:   \medskip Theory output may be suppressed more selectively.  Research
wenzelm@12767:   articles and slides usually do not include the formal content in
wenzelm@12767:   full.  Delimiting \bfindex{ignored material} by the special source
wenzelm@12767:   comments \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
wenzelm@12767:   \verb,(,\verb,*,\verb,>,\verb,*,\verb,), tells the document
wenzelm@12767:   preparation system to suppress these parts; the formal checking of
wenzelm@12771:   the theory is unchanged, of course.
wenzelm@12647: 
wenzelm@12767:   In this example, we hide a theory's \isakeyword{theory} and
wenzelm@12767:   \isakeyword{end} brackets:
wenzelm@12647: 
wenzelm@12647:   \medskip
wenzelm@12647: 
wenzelm@12647:   \begin{tabular}{l}
wenzelm@12647:   \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
wenzelm@12666:   \texttt{theory T = Main:} \\
wenzelm@12647:   \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
wenzelm@12647:   ~~$\vdots$ \\
wenzelm@12647:   \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
wenzelm@12647:   \texttt{end} \\
wenzelm@12647:   \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
wenzelm@12647:   \end{tabular}
wenzelm@12647: 
wenzelm@12647:   \medskip
wenzelm@12647: 
paulson@12764:   Text may be suppressed in a fine-grained manner.  We may even hide
wenzelm@12747:   vital parts of a proof, pretending that things have been simpler
wenzelm@12767:   than they really were.  For example, this ``fully automatic'' proof
wenzelm@12767:   is actually a fake:%
wenzelm@12649: \end{isamarkuptext}%
wenzelm@12649: \isamarkuptrue%
wenzelm@12649: \isacommand{lemma}\ {\isachardoublequote}x\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isacharless}\ x\ {\isacharasterisk}\ x{\isachardoublequote}\isanewline
wenzelm@12649: \ \ \isamarkupfalse%
wenzelm@12649: \isacommand{by}\ {\isacharparenleft}auto{\isacharparenright}\isamarkupfalse%
wenzelm@12649: %
wenzelm@12649: \begin{isamarkuptext}%
wenzelm@12649: \noindent Here the real source of the proof has been as follows:
wenzelm@12649: 
wenzelm@12649: \begin{verbatim}
paulson@14353:   by (auto(*<*)simp add: zero_less_mult_iff(*>*))
wenzelm@12658: \end{verbatim}
wenzelm@12658: %(*
wenzelm@12649: 
wenzelm@12767:   \medskip Suppressing portions of printed text demands care.  You
wenzelm@12767:   should not misrepresent the underlying theory development.  It is
wenzelm@12767:   easy to invalidate the visible text by hiding references to
wenzelm@12767:   questionable axioms.
wenzelm@12652: 
wenzelm@12747:   Authentic reports of Isabelle/Isar theories, say as part of a
wenzelm@12767:   library, should suppress nothing.  Other users may need the full
wenzelm@12767:   information for their own derivative work.  If a particular
wenzelm@12767:   formalization appears inadequate for general public coverage, it is
wenzelm@12767:   often more appropriate to think of a better way in the first place.
wenzelm@12671: 
wenzelm@12671:   \medskip Some technical subtleties of the
wenzelm@12666:   \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),
paulson@12764:   elements need to be kept in mind, too --- the system performs few
wenzelm@12671:   sanity checks here.  Arguments of markup commands and formal
wenzelm@12649:   comments must not be hidden, otherwise presentation fails.  Open and
wenzelm@12751:   close parentheses need to be inserted carefully; it is easy to hide
wenzelm@12751:   the wrong parts, especially after rearranging the theory text.%
wenzelm@12635: \end{isamarkuptext}%
wenzelm@12627: \isamarkuptrue%
wenzelm@11866: \isamarkupfalse%
wenzelm@11648: \end{isabellebody}%
wenzelm@11648: %%% Local Variables:
wenzelm@11648: %%% mode: latex
wenzelm@11648: %%% TeX-master: "root"
wenzelm@11648: %%% End:




