doc-src/TutorialI/Documents/document/Documents.tex
author wenzelm
Sun Oct 09 15:46:06 2011 +0200 (2011-10-09 ago)
changeset 45106 3498077f2012
parent 40406 313a24b66a8d
child 47822 34b44d28fc4b
permissions -rw-r--r--
updated ISABELLE_HOME_USER;
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Documents}%
     4 %
     5 \isadelimtheory
     6 %
     7 \endisadelimtheory
     8 %
     9 \isatagtheory
    10 %
    11 \endisatagtheory
    12 {\isafoldtheory}%
    13 %
    14 \isadelimtheory
    15 %
    16 \endisadelimtheory
    17 %
    18 \isamarkupsection{Concrete Syntax \label{sec:concrete-syntax}%
    19 }
    20 \isamarkuptrue%
    21 %
    22 \begin{isamarkuptext}%
    23 The core concept of Isabelle's framework for concrete syntax is that
    24   of \bfindex{mixfix annotations}.  Associated with any kind of
    25   constant declaration, mixfixes affect both the grammar productions
    26   for the parser and output templates for the pretty printer.
    27 
    28   In full generality, parser and pretty printer configuration is a
    29   subtle affair~\cite{isabelle-ref}.  Your syntax specifications need
    30   to interact properly with the existing setup of Isabelle/Pure and
    31   Isabelle/HOL\@.  To avoid creating ambiguities with existing
    32   elements, it is particularly important to give new syntactic
    33   constructs the right precedence.
    34 
    35   Below we introduce a few simple syntax declaration
    36   forms that already cover many common situations fairly well.%
    37 \end{isamarkuptext}%
    38 \isamarkuptrue%
    39 %
    40 \isamarkupsubsection{Infix Annotations%
    41 }
    42 \isamarkuptrue%
    43 %
    44 \begin{isamarkuptext}%
    45 Syntax annotations may be included wherever constants are declared,
    46   such as \isacommand{definition} and \isacommand{primrec} --- and also
    47   \isacommand{datatype}, which declares constructor operations.
    48   Type-constructors may be annotated as well, although this is less
    49   frequently encountered in practice (the infix type \isa{{\isaliteral{5C3C74696D65733E}{\isasymtimes}}} comes
    50   to mind).
    51 
    52   Infix declarations\index{infix annotations} provide a useful special
    53   case of mixfixes.  The following example of the exclusive-or
    54   operation on boolean values illustrates typical infix declarations.%
    55 \end{isamarkuptext}%
    56 \isamarkuptrue%
    57 \isacommand{definition}\isamarkupfalse%
    58 \ xor\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{6}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
    59 \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ B\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
    60 \begin{isamarkuptext}%
    61 \noindent Now \isa{xor\ A\ B} and \isa{A\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ B} refer to the
    62   same expression internally.  Any curried function with at least two
    63   arguments may be given infix syntax.  For partial applications with
    64   fewer than two operands, there is a notation using the prefix~\isa{op}.  For instance, \isa{xor} without arguments is represented as
    65   \isa{op\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}}; together with ordinary function application, this
    66   turns \isa{xor\ A} into \isa{op\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ A}.
    67 
    68   The keyword \isakeyword{infixl} seen above specifies an
    69   infix operator that is nested to the \emph{left}: in iterated
    70   applications the more complex expression appears on the left-hand
    71   side, and \isa{A\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ B\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ C} stands for \isa{{\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ C}.  Similarly, \isakeyword{infixr} means nesting to the
    72   \emph{right}, reading \isa{A\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ B\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ C} as \isa{A\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{28}{\isacharparenleft}}B\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ C{\isaliteral{29}{\isacharparenright}}}.  A \emph{non-oriented} declaration via \isakeyword{infix}
    73   would render \isa{A\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ B\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ C} illegal, but demand explicit
    74   parentheses to indicate the intended grouping.
    75 
    76   The string \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} in our annotation refers to the
    77   concrete syntax to represent the operator (a literal token), while
    78   the number \isa{{\isadigit{6}}{\isadigit{0}}} determines the precedence of the construct:
    79   the syntactic priorities of the arguments and result.  Isabelle/HOL
    80   already uses up many popular combinations of ASCII symbols for its
    81   own use, including both \isa{{\isaliteral{2B}{\isacharplus}}} and \isa{{\isaliteral{2B}{\isacharplus}}{\isaliteral{2B}{\isacharplus}}}.  Longer
    82   character combinations are more likely to be still available for
    83   user extensions, such as our~\isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}}.
    84 
    85   Operator precedences have a range of 0--1000.  Very low or high
    86   priorities are reserved for the meta-logic.  HOL syntax mainly uses
    87   the range of 10--100: the equality infix \isa{{\isaliteral{3D}{\isacharequal}}} is centered at
    88   50; logical connectives (like \isa{{\isaliteral{5C3C6F723E}{\isasymor}}} and \isa{{\isaliteral{5C3C616E643E}{\isasymand}}}) are
    89   below 50; algebraic ones (like \isa{{\isaliteral{2B}{\isacharplus}}} and \isa{{\isaliteral{2A}{\isacharasterisk}}}) are
    90   above 50.  User syntax should strive to coexist with common HOL
    91   forms, or use the mostly unused range 100--900.%
    92 \end{isamarkuptext}%
    93 \isamarkuptrue%
    94 %
    95 \isamarkupsubsection{Mathematical Symbols \label{sec:syntax-symbols}%
    96 }
    97 \isamarkuptrue%
    98 %
    99 \begin{isamarkuptext}%
   100 Concrete syntax based on ASCII characters has inherent limitations.
   101   Mathematical notation demands a larger repertoire of glyphs.
   102   Several standards of extended character sets have been proposed over
   103   decades, but none has become universally available so far.  Isabelle
   104   has its own notion of \bfindex{symbols} as the smallest entities of
   105   source text, without referring to internal encodings.  There are
   106   three kinds of such ``generalized characters'':
   107 
   108   \begin{enumerate}
   109 
   110   \item 7-bit ASCII characters
   111 
   112   \item named symbols: \verb,\,\verb,<,$ident$\verb,>,
   113 
   114   \item named control symbols: \verb,\,\verb,<^,$ident$\verb,>,
   115 
   116   \end{enumerate}
   117 
   118   Here $ident$ is any sequence of letters. 
   119   This results in an infinite store of symbols, whose
   120   interpretation is left to further front-end tools.  For example, the
   121   user-interface of Proof~General + X-Symbol and the Isabelle document
   122   processor (see \S\ref{sec:document-preparation}) display the
   123   \verb,\,\verb,<forall>, symbol as~\isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}}.
   124 
   125   A list of standard Isabelle symbols is given in
   126   \cite{isabelle-isar-ref}.  You may introduce your own
   127   interpretation of further symbols by configuring the appropriate
   128   front-end tool accordingly, e.g.\ by defining certain {\LaTeX}
   129   macros (see also \S\ref{sec:doc-prep-symbols}).  There are also a
   130   few predefined control symbols, such as \verb,\,\verb,<^sub>, and
   131   \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent
   132   printable symbol, respectively.  For example, \verb,A\<^sup>\<star>, is
   133   output as \isa{A\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{5C3C737461723E}{\isasymstar}}}.
   134 
   135   A number of symbols are considered letters by the Isabelle lexer and
   136   can be used as part of identifiers. These are the greek letters
   137   \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}} (\verb+\+\verb+<alpha>+), \isa{{\isaliteral{5C3C626574613E}{\isasymbeta}}}
   138   (\verb+\+\verb+<beta>+), etc. (excluding \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}),
   139   special letters like \isa{{\isaliteral{5C3C413E}{\isasymA}}} (\verb+\+\verb+<A>+) and \isa{{\isaliteral{5C3C41413E}{\isasymAA}}} (\verb+\+\verb+<AA>+), and the control symbols
   140   \verb+\+\verb+<^isub>+ and \verb+\+\verb+<^isup>+ for single letter
   141   sub and super scripts. This means that the input
   142 
   143   \medskip
   144   {\small\noindent \verb,\,\verb,<forall>\,\verb,<alpha>\<^isub>1.,~\verb,\,\verb,<alpha>\<^isub>1 = \,\verb,<Pi>\<^isup>\<A>,}
   145 
   146   \medskip
   147   \noindent is recognized as the term \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C50693E}{\isasymPi}}\isaliteral{5C3C5E697375703E}{}\isactrlisup {\isaliteral{5C3C413E}{\isasymA}}} 
   148   by Isabelle. Note that \isa{{\isaliteral{5C3C50693E}{\isasymPi}}\isaliteral{5C3C5E697375703E}{}\isactrlisup {\isaliteral{5C3C413E}{\isasymA}}} is a single
   149   syntactic entity, not an exponentiation.
   150 
   151   Replacing our previous definition of \isa{xor} by the
   152   following specifies an Isabelle symbol for the new operator:%
   153 \end{isamarkuptext}%
   154 \isamarkuptrue%
   155 %
   156 \isadelimML
   157 %
   158 \endisadelimML
   159 %
   160 \isatagML
   161 %
   162 \endisatagML
   163 {\isafoldML}%
   164 %
   165 \isadelimML
   166 %
   167 \endisadelimML
   168 \isacommand{definition}\isamarkupfalse%
   169 \ xor\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F706C75733E}{\isasymoplus}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{6}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
   170 \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ B\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
   171 \isadelimML
   172 %
   173 \endisadelimML
   174 %
   175 \isatagML
   176 %
   177 \endisatagML
   178 {\isafoldML}%
   179 %
   180 \isadelimML
   181 %
   182 \endisadelimML
   183 %
   184 \begin{isamarkuptext}%
   185 \noindent The X-Symbol package within Proof~General provides several
   186   input methods to enter \isa{{\isaliteral{5C3C6F706C75733E}{\isasymoplus}}} in the text.  If all fails one may
   187   just type a named entity \verb,\,\verb,<oplus>, by hand; the
   188   corresponding symbol will be displayed after further input.
   189 
   190   More flexible is to provide alternative syntax forms
   191   through the \bfindex{print mode} concept~\cite{isabelle-ref}.  By
   192   convention, the mode of ``$xsymbols$'' is enabled whenever
   193   Proof~General's X-Symbol mode or {\LaTeX} output is active.  Now
   194   consider the following hybrid declaration of \isa{xor}:%
   195 \end{isamarkuptext}%
   196 \isamarkuptrue%
   197 %
   198 \isadelimML
   199 %
   200 \endisadelimML
   201 %
   202 \isatagML
   203 %
   204 \endisatagML
   205 {\isafoldML}%
   206 %
   207 \isadelimML
   208 %
   209 \endisadelimML
   210 \isacommand{definition}\isamarkupfalse%
   211 \ xor\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5C3C69676E6F72653E}{\isasymignore}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{6}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
   212 \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5C3C69676E6F72653E}{\isasymignore}}\ B\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
   213 \isanewline
   214 \isacommand{notation}\isamarkupfalse%
   215 \ {\isaliteral{28}{\isacharparenleft}}xsymbols{\isaliteral{29}{\isacharparenright}}\ xor\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F706C75733E}{\isasymoplus}}{\isaliteral{5C3C69676E6F72653E}{\isasymignore}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{6}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}%
   216 \isadelimML
   217 %
   218 \endisadelimML
   219 %
   220 \isatagML
   221 %
   222 \endisatagML
   223 {\isafoldML}%
   224 %
   225 \isadelimML
   226 %
   227 \endisadelimML
   228 %
   229 \begin{isamarkuptext}%
   230 \noindent
   231 The \commdx{notation} command associates a mixfix
   232 annotation with a known constant.  The print mode specification,
   233 here \isa{{\isaliteral{28}{\isacharparenleft}}xsymbols{\isaliteral{29}{\isacharparenright}}}, is optional.
   234 
   235 We may now write \isa{A\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5D}{\isacharbrackright}}\ B} or \isa{A\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ B} in input, while
   236 output uses the nicer syntax of $xsymbols$ whenever that print mode is
   237 active.  Such an arrangement is particularly useful for interactive
   238 development, where users may type ASCII text and see mathematical
   239 symbols displayed during proofs.%
   240 \end{isamarkuptext}%
   241 \isamarkuptrue%
   242 %
   243 \isamarkupsubsection{Prefix Annotations%
   244 }
   245 \isamarkuptrue%
   246 %
   247 \begin{isamarkuptext}%
   248 Prefix syntax annotations\index{prefix annotation} are another form
   249   of mixfixes \cite{isabelle-ref}, without any template arguments or
   250   priorities --- just some literal syntax.  The following example
   251   associates common symbols with the constructors of a datatype.%
   252 \end{isamarkuptext}%
   253 \isamarkuptrue%
   254 \isacommand{datatype}\isamarkupfalse%
   255 \ currency\ {\isaliteral{3D}{\isacharequal}}\isanewline
   256 \ \ \ \ Euro\ nat\ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6575726F3E}{\isasymeuro}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
   257 \ \ {\isaliteral{7C}{\isacharbar}}\ Pounds\ nat\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C706F756E64733E}{\isasympounds}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
   258 \ \ {\isaliteral{7C}{\isacharbar}}\ Yen\ nat\ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C79656E3E}{\isasymyen}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
   259 \ \ {\isaliteral{7C}{\isacharbar}}\ Dollar\ nat\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{24}{\isachardollar}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}%
   260 \begin{isamarkuptext}%
   261 \noindent Here the mixfix annotations on the rightmost column happen
   262   to consist of a single Isabelle symbol each: \verb,\,\verb,<euro>,,
   263   \verb,\,\verb,<pounds>,, \verb,\,\verb,<yen>,, and \verb,$,.  Recall
   264   that a constructor like \isa{Euro} actually is a function \isa{nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ currency}.  The expression \isa{Euro\ {\isadigit{1}}{\isadigit{0}}} will be
   265   printed as \isa{{\isaliteral{5C3C6575726F3E}{\isasymeuro}}\ {\isadigit{1}}{\isadigit{0}}}; only the head of the application is
   266   subject to our concrete syntax.  This rather simple form already
   267   achieves conformance with notational standards of the European
   268   Commission.
   269 
   270   Prefix syntax works the same way for other commands that introduce new constants, e.g. \isakeyword{primrec}.%
   271 \end{isamarkuptext}%
   272 \isamarkuptrue%
   273 %
   274 \isamarkupsubsection{Abbreviations \label{sec:abbreviations}%
   275 }
   276 \isamarkuptrue%
   277 %
   278 \begin{isamarkuptext}%
   279 Mixfix syntax annotations merely decorate particular constant
   280 application forms with concrete syntax, for instance replacing
   281 \isa{xor\ A\ B} by \isa{A\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ B}.  Occasionally, the relationship
   282 between some piece of notation and its internal form is more
   283 complicated.  Here we need \emph{abbreviations}.
   284 
   285 Command \commdx{abbreviation} introduces an uninterpreted notational
   286 constant as an abbreviation for a complex term. Abbreviations are
   287 unfolded upon parsing and re-introduced upon printing. This provides a
   288 simple mechanism for syntactic macros.
   289 
   290 A typical use of abbreviations is to introduce relational notation for
   291 membership in a set of pairs, replacing \isa{{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ sim} by
   292 \isa{x\ {\isaliteral{5C3C617070726F783E}{\isasymapprox}}\ y}. We assume that a constant \isa{sim} of type
   293 \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ set} has been introduced at this point.%
   294 \end{isamarkuptext}%
   295 \isamarkuptrue%
   296 \isacommand{abbreviation}\isamarkupfalse%
   297 \ sim{\isadigit{2}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infix}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C617070726F783E}{\isasymapprox}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{5}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
   298 \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C617070726F783E}{\isasymapprox}}\ y\ \ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ \ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ sim{\isaliteral{22}{\isachardoublequoteclose}}%
   299 \begin{isamarkuptext}%
   300 \noindent The given meta-equality is used as a rewrite rule
   301 after parsing (replacing \mbox{\isa{x\ {\isaliteral{5C3C617070726F783E}{\isasymapprox}}\ y}} by \isa{{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ sim}) and before printing (turning \isa{{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ sim} back into
   302 \mbox{\isa{x\ {\isaliteral{5C3C617070726F783E}{\isasymapprox}}\ y}}). The name of the dummy constant \isa{sim{\isadigit{2}}}
   303 does not matter, as long as it is unique.
   304 
   305 Another common application of abbreviations is to
   306 provide variant versions of fundamental relational expressions, such
   307 as \isa{{\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}} for negated equalities.  The following declaration
   308 stems from Isabelle/HOL itself:%
   309 \end{isamarkuptext}%
   310 \isamarkuptrue%
   311 \isacommand{abbreviation}\isamarkupfalse%
   312 \ not{\isaliteral{5F}{\isacharunderscore}}equal\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7E}{\isachartilde}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{5C3C69676E6F72653E}{\isasymignore}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{5}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
   313 \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{7E}{\isachartilde}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{5C3C69676E6F72653E}{\isasymignore}}\ y\ \ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ \ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
   314 \isanewline
   315 \isacommand{notation}\isamarkupfalse%
   316 \ {\isaliteral{28}{\isacharparenleft}}xsymbols{\isaliteral{29}{\isacharparenright}}\ not{\isaliteral{5F}{\isacharunderscore}}equal\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infix}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}{\isaliteral{5C3C69676E6F72653E}{\isasymignore}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{5}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}%
   317 \begin{isamarkuptext}%
   318 \noindent The notation \isa{{\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}} is introduced separately to restrict it
   319 to the \emph{xsymbols} mode.
   320 
   321 Abbreviations are appropriate when the defined concept is a
   322 simple variation on an existing one.  But because of the automatic
   323 folding and unfolding of abbreviations, they do not scale up well to
   324 large hierarchies of concepts. Abbreviations do not replace
   325 definitions.
   326 
   327 Abbreviations are a simplified form of the general concept of
   328 \emph{syntax translations}; even heavier transformations may be
   329 written in ML \cite{isabelle-ref}.%
   330 \end{isamarkuptext}%
   331 \isamarkuptrue%
   332 %
   333 \isamarkupsection{Document Preparation \label{sec:document-preparation}%
   334 }
   335 \isamarkuptrue%
   336 %
   337 \begin{isamarkuptext}%
   338 Isabelle/Isar is centered around the concept of \bfindex{formal
   339   proof documents}\index{documents|bold}.  The outcome of a formal
   340   development effort is meant to be a human-readable record, presented
   341   as browsable PDF file or printed on paper.  The overall document
   342   structure follows traditional mathematical articles, with sections,
   343   intermediate explanations, definitions, theorems and proofs.
   344 
   345   \medskip The Isabelle document preparation system essentially acts
   346   as a front-end to {\LaTeX}.  After checking specifications and
   347   proofs formally, the theory sources are turned into typesetting
   348   instructions in a schematic manner.  This lets you write authentic
   349   reports on theory developments with little effort: many technical
   350   consistency checks are handled by the system.
   351 
   352   Here is an example to illustrate the idea of Isabelle document
   353   preparation.%
   354 \end{isamarkuptext}%
   355 \isamarkuptrue%
   356 %
   357 \begin{quotation}
   358 %
   359 \begin{isamarkuptext}%
   360 The following datatype definition of \isa{{\isaliteral{27}{\isacharprime}}a\ bintree} models
   361   binary trees with nodes being decorated by elements of type \isa{{\isaliteral{27}{\isacharprime}}a}.%
   362 \end{isamarkuptext}%
   363 \isamarkuptrue%
   364 \isacommand{datatype}\isamarkupfalse%
   365 \ {\isaliteral{27}{\isacharprime}}a\ bintree\ {\isaliteral{3D}{\isacharequal}}\isanewline
   366 \ \ \ \ \ Leaf\ {\isaliteral{7C}{\isacharbar}}\ Branch\ {\isaliteral{27}{\isacharprime}}a\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bintree{\isaliteral{22}{\isachardoublequoteclose}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bintree{\isaliteral{22}{\isachardoublequoteclose}}%
   367 \begin{isamarkuptext}%
   368 \noindent The datatype induction rule generated here is of the form
   369   \begin{isabelle}%
   370 \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}P\ Leaf{\isaliteral{3B}{\isacharsemicolon}}\isanewline
   371 \isaindent{\ \ }{\isaliteral{5C3C416E643E}{\isasymAnd}}a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isaliteral{2E}{\isachardot}}\isanewline
   372 \isaindent{\ \ \ \ \ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}P\ bintree{\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\ P\ bintree{\isadigit{2}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}Branch\ a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline
   373 \isaindent{\ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ bintree%
   374 \end{isabelle}%
   375 \end{isamarkuptext}%
   376 \isamarkuptrue%
   377 %
   378 \end{quotation}
   379 %
   380 \begin{isamarkuptext}%
   381 \noindent The above document output has been produced as follows:
   382 
   383   \begin{ttbox}
   384   text {\ttlbrace}*
   385     The following datatype definition of {\at}{\ttlbrace}text "'a bintree"{\ttrbrace}
   386     models binary trees with nodes being decorated by elements
   387     of type {\at}{\ttlbrace}typ 'a{\ttrbrace}.
   388   *{\ttrbrace}
   389 
   390   datatype 'a bintree =
   391     Leaf | Branch 'a  "'a bintree"  "'a bintree"
   392   \end{ttbox}
   393   \begin{ttbox}
   394   text {\ttlbrace}*
   395     {\ttback}noindent The datatype induction rule generated here is
   396     of the form {\at}{\ttlbrace}thm [display] bintree.induct [no_vars]{\ttrbrace}
   397   *{\ttrbrace}
   398   \end{ttbox}\vspace{-\medskipamount}
   399 
   400   \noindent Here we have augmented the theory by formal comments
   401   (using \isakeyword{text} blocks), the informal parts may again refer
   402   to formal entities by means of ``antiquotations'' (such as
   403   \texttt{\at}\verb,{text "'a bintree"}, or
   404   \texttt{\at}\verb,{typ 'a},), see also \S\ref{sec:doc-prep-text}.%
   405 \end{isamarkuptext}%
   406 \isamarkuptrue%
   407 %
   408 \isamarkupsubsection{Isabelle Sessions%
   409 }
   410 \isamarkuptrue%
   411 %
   412 \begin{isamarkuptext}%
   413 In contrast to the highly interactive mode of Isabelle/Isar theory
   414   development, the document preparation stage essentially works in
   415   batch-mode.  An Isabelle \bfindex{session} consists of a collection
   416   of source files that may contribute to an output document.  Each
   417   session is derived from a single parent, usually an object-logic
   418   image like \texttt{HOL}.  This results in an overall tree structure,
   419   which is reflected by the output location in the file system
   420   (usually rooted at \verb,~/.isabelle/IsabelleXXXX/browser_info,).
   421 
   422   \medskip The easiest way to manage Isabelle sessions is via
   423   \texttt{isabelle mkdir} (generates an initial session source setup)
   424   and \texttt{isabelle make} (run sessions controlled by
   425   \texttt{IsaMakefile}).  For example, a new session
   426   \texttt{MySession} derived from \texttt{HOL} may be produced as
   427   follows:
   428 
   429 \begin{verbatim}
   430   isabelle mkdir HOL MySession
   431   isabelle make
   432 \end{verbatim}
   433 
   434   The \texttt{isabelle make} job also informs about the file-system
   435   location of the ultimate results.  The above dry run should be able
   436   to produce some \texttt{document.pdf} (with dummy title, empty table
   437   of contents etc.).  Any failure at this stage usually indicates
   438   technical problems of the {\LaTeX} installation.
   439 
   440   \medskip The detailed arrangement of the session sources is as
   441   follows.
   442 
   443   \begin{itemize}
   444 
   445   \item Directory \texttt{MySession} holds the required theory files
   446   $T@1$\texttt{.thy}, \dots, $T@n$\texttt{.thy}.
   447 
   448   \item File \texttt{MySession/ROOT.ML} holds appropriate ML commands
   449   for loading all wanted theories, usually just
   450   ``\texttt{use_thy"$T@i$";}'' for any $T@i$ in leaf position of the
   451   dependency graph.
   452 
   453   \item Directory \texttt{MySession/document} contains everything
   454   required for the {\LaTeX} stage; only \texttt{root.tex} needs to be
   455   provided initially.
   456 
   457   The latter file holds appropriate {\LaTeX} code to commence a
   458   document (\verb,\documentclass, etc.), and to include the generated
   459   files $T@i$\texttt{.tex} for each theory.  Isabelle will generate a
   460   file \texttt{session.tex} holding {\LaTeX} commands to include all
   461   generated theory output files in topologically sorted order, so
   462   \verb,\input{session}, in the body of \texttt{root.tex} does the job
   463   in most situations.
   464 
   465   \item \texttt{IsaMakefile} holds appropriate dependencies and
   466   invocations of Isabelle tools to control the batch job.  In fact,
   467   several sessions may be managed by the same \texttt{IsaMakefile}.
   468   See the \emph{Isabelle System Manual} \cite{isabelle-sys} 
   469   for further details, especially on
   470   \texttt{isabelle usedir} and \texttt{isabelle make}.
   471 
   472   \end{itemize}
   473 
   474   One may now start to populate the directory \texttt{MySession}, and
   475   the file \texttt{MySession/ROOT.ML} accordingly.  The file
   476   \texttt{MySession/document/root.tex} should also be adapted at some
   477   point; the default version is mostly self-explanatory.  Note that
   478   \verb,\isabellestyle, enables fine-tuning of the general appearance
   479   of characters and mathematical symbols (see also
   480   \S\ref{sec:doc-prep-symbols}).
   481 
   482   Especially observe the included {\LaTeX} packages \texttt{isabelle}
   483   (mandatory), \texttt{isabellesym} (required for mathematical
   484   symbols), and the final \texttt{pdfsetup} (provides sane defaults
   485   for \texttt{hyperref}, including URL markup).  All three are
   486   distributed with Isabelle. Further packages may be required in
   487   particular applications, say for unusual mathematical symbols.
   488 
   489   \medskip Any additional files for the {\LaTeX} stage go into the
   490   \texttt{MySession/document} directory as well.  In particular,
   491   adding a file named \texttt{root.bib} causes an automatic run of
   492   \texttt{bibtex} to process a bibliographic database; see also
   493   \texttt{isabelle document} \cite{isabelle-sys}.
   494 
   495   \medskip Any failure of the document preparation phase in an
   496   Isabelle batch session leaves the generated sources in their target
   497   location, identified by the accompanying error message.  This lets
   498   you trace {\LaTeX} problems with the generated files at hand.%
   499 \end{isamarkuptext}%
   500 \isamarkuptrue%
   501 %
   502 \isamarkupsubsection{Structure Markup%
   503 }
   504 \isamarkuptrue%
   505 %
   506 \begin{isamarkuptext}%
   507 The large-scale structure of Isabelle documents follows existing
   508   {\LaTeX} conventions, with chapters, sections, subsubsections etc.
   509   The Isar language includes separate \bfindex{markup commands}, which
   510   do not affect the formal meaning of a theory (or proof), but result
   511   in corresponding {\LaTeX} elements.
   512 
   513   There are separate markup commands depending on the textual context:
   514   in header position (just before \isakeyword{theory}), within the
   515   theory body, or within a proof.  The header needs to be treated
   516   specially here, since ordinary theory and proof commands may only
   517   occur \emph{after} the initial \isakeyword{theory} specification.
   518 
   519   \medskip
   520 
   521   \begin{tabular}{llll}
   522   header & theory & proof & default meaning \\\hline
   523     & \commdx{chapter} & & \verb,\chapter, \\
   524   \commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\
   525     & \commdx{subsection} & \commdx{subsect} & \verb,\subsection, \\
   526     & \commdx{subsubsection} & \commdx{subsubsect} & \verb,\subsubsection, \\
   527   \end{tabular}
   528 
   529   \medskip
   530 
   531   From the Isabelle perspective, each markup command takes a single
   532   $text$ argument (delimited by \verb,",~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb,", or
   533   \verb,{,\verb,*,~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb,*,\verb,},).  After stripping any
   534   surrounding white space, the argument is passed to a {\LaTeX} macro
   535   \verb,\isamarkupXYZ, for command \isakeyword{XYZ}.  These macros are
   536   defined in \verb,isabelle.sty, according to the meaning given in the
   537   rightmost column above.
   538 
   539   \medskip The following source fragment illustrates structure markup
   540   of a theory.  Note that {\LaTeX} labels may be included inside of
   541   section headings as well.
   542 
   543   \begin{ttbox}
   544   header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
   545 
   546   theory Foo_Bar
   547   imports Main
   548   begin
   549 
   550   subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
   551 
   552   definition foo :: \dots
   553 
   554   definition bar :: \dots
   555 
   556   subsection {\ttlbrace}* Derived rules *{\ttrbrace}
   557 
   558   lemma fooI: \dots
   559   lemma fooE: \dots
   560 
   561   subsection {\ttlbrace}* Main theorem {\ttback}label{\ttlbrace}sec:main-theorem{\ttrbrace} *{\ttrbrace}
   562 
   563   theorem main: \dots
   564 
   565   end
   566   \end{ttbox}\vspace{-\medskipamount}
   567 
   568   You may occasionally want to change the meaning of markup commands,
   569   say via \verb,\renewcommand, in \texttt{root.tex}.  For example,
   570   \verb,\isamarkupheader, is a good candidate for some tuning.  We
   571   could move it up in the hierarchy to become \verb,\chapter,.
   572 
   573 \begin{verbatim}
   574   \renewcommand{\isamarkupheader}[1]{\chapter{#1}}
   575 \end{verbatim}
   576 
   577   \noindent Now we must change the document class given in
   578   \texttt{root.tex} to something that supports chapters.  A suitable
   579   command is \verb,\documentclass{report},.
   580 
   581   \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to
   582   hold the name of the current theory context.  This is particularly
   583   useful for document headings:
   584 
   585 \begin{verbatim}
   586   \renewcommand{\isamarkupheader}[1]
   587   {\chapter{#1}\markright{THEORY~\isabellecontext}}
   588 \end{verbatim}
   589 
   590   \noindent Make sure to include something like
   591   \verb,\pagestyle{headings}, in \texttt{root.tex}; the document
   592   should have more than two pages to show the effect.%
   593 \end{isamarkuptext}%
   594 \isamarkuptrue%
   595 %
   596 \isamarkupsubsection{Formal Comments and Antiquotations \label{sec:doc-prep-text}%
   597 }
   598 \isamarkuptrue%
   599 %
   600 \begin{isamarkuptext}%
   601 Isabelle \bfindex{source comments}, which are of the form
   602   \verb,(,\verb,*,~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb,*,\verb,),, essentially act like
   603   white space and do not really contribute to the content.  They
   604   mainly serve technical purposes to mark certain oddities in the raw
   605   input text.  In contrast, \bfindex{formal comments} are portions of
   606   text that are associated with formal Isabelle/Isar commands
   607   (\bfindex{marginal comments}), or as standalone paragraphs within a
   608   theory or proof context (\bfindex{text blocks}).
   609 
   610   \medskip Marginal comments are part of each command's concrete
   611   syntax \cite{isabelle-ref}; the common form is ``\verb,--,~$text$''
   612   where $text$ is delimited by \verb,",\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}\verb,", or
   613   \verb,{,\verb,*,~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb,*,\verb,}, as before.  Multiple
   614   marginal comments may be given at the same time.  Here is a simple
   615   example:%
   616 \end{isamarkuptext}%
   617 \isamarkuptrue%
   618 \isacommand{lemma}\isamarkupfalse%
   619 \ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
   620 \ \ %
   621 \isamarkupcmt{a triviality of propositional logic%
   622 }
   623 \isanewline
   624 \ \ %
   625 \isamarkupcmt{(should not really bother)%
   626 }
   627 \isanewline
   628 %
   629 \isadelimproof
   630 \ \ %
   631 \endisadelimproof
   632 %
   633 \isatagproof
   634 \isacommand{by}\isamarkupfalse%
   635 \ {\isaliteral{28}{\isacharparenleft}}rule\ impI{\isaliteral{29}{\isacharparenright}}\ %
   636 \isamarkupcmt{implicit assumption step involved here%
   637 }
   638 %
   639 \endisatagproof
   640 {\isafoldproof}%
   641 %
   642 \isadelimproof
   643 %
   644 \endisadelimproof
   645 %
   646 \begin{isamarkuptext}%
   647 \noindent The above output has been produced as follows:
   648 
   649 \begin{verbatim}
   650   lemma "A --> A"
   651     -- "a triviality of propositional logic"
   652     -- "(should not really bother)"
   653     by (rule impI) -- "implicit assumption step involved here"
   654 \end{verbatim}
   655 
   656   From the {\LaTeX} viewpoint, ``\verb,--,'' acts like a markup
   657   command, associated with the macro \verb,\isamarkupcmt, (taking a
   658   single argument).
   659 
   660   \medskip Text blocks are introduced by the commands \bfindex{text}
   661   and \bfindex{txt}, for theory and proof contexts, respectively.
   662   Each takes again a single $text$ argument, which is interpreted as a
   663   free-form paragraph in {\LaTeX} (surrounded by some additional
   664   vertical space).  This behavior may be changed by redefining the
   665   {\LaTeX} environments of \verb,isamarkuptext, or
   666   \verb,isamarkuptxt,, respectively (via \verb,\renewenvironment,) The
   667   text style of the body is determined by \verb,\isastyletext, and
   668   \verb,\isastyletxt,; the default setup uses a smaller font within
   669   proofs.  This may be changed as follows:
   670 
   671 \begin{verbatim}
   672   \renewcommand{\isastyletxt}{\isastyletext}
   673 \end{verbatim}
   674 
   675   \medskip The $text$ part of Isabelle markup commands essentially
   676   inserts \emph{quoted material} into a formal text, mainly for
   677   instruction of the reader.  An \bfindex{antiquotation} is again a
   678   formal object embedded into such an informal portion.  The
   679   interpretation of antiquotations is limited to some well-formedness
   680   checks, with the result being pretty printed to the resulting
   681   document.  Quoted text blocks together with antiquotations provide
   682   an attractive means of referring to formal entities, with good
   683   confidence in getting the technical details right (especially syntax
   684   and types).
   685 
   686   The general syntax of antiquotations is as follows:
   687   \texttt{{\at}{\ttlbrace}$name$ $arguments${\ttrbrace}}, or
   688   \texttt{{\at}{\ttlbrace}$name$ [$options$] $arguments${\ttrbrace}}
   689   for a comma-separated list of options consisting of a $name$ or
   690   \texttt{$name$=$value$} each.  The syntax of $arguments$ depends on
   691   the kind of antiquotation, it generally follows the same conventions
   692   for types, terms, or theorems as in the formal part of a theory.
   693 
   694   \medskip This sentence demonstrates quotations and antiquotations:
   695   \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x\ y{\isaliteral{2E}{\isachardot}}\ x} is a well-typed term.
   696 
   697   \medskip\noindent The output above was produced as follows:
   698   \begin{ttbox}
   699 text {\ttlbrace}*
   700   This sentence demonstrates quotations and antiquotations:
   701   {\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term.
   702 *{\ttrbrace}
   703   \end{ttbox}\vspace{-\medskipamount}
   704 
   705   The notational change from the ASCII character~\verb,%, to the
   706   symbol~\isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}} reveals that Isabelle printed this term, after
   707   parsing and type-checking.  Document preparation enables symbolic
   708   output by default.
   709 
   710   \medskip The next example includes an option to show the type of all
   711   variables.  The antiquotation
   712   \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces the
   713   output \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ y{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}b{\isaliteral{2E}{\isachardot}}\ x}.  Type inference has figured
   714   out the most general typings in the present theory context.  Terms
   715   may acquire different typings due to constraints imposed by their
   716   environment; within a proof, for example, variables are given the
   717   same types as they have in the main goal statement.
   718 
   719   \medskip Several further kinds of antiquotations and options are
   720   available \cite{isabelle-isar-ref}.  Here are a few commonly used
   721   combinations:
   722 
   723   \medskip
   724 
   725   \begin{tabular}{ll}
   726   \texttt{\at}\verb,{typ,~$\tau$\verb,}, & print type $\tau$ \\
   727   \texttt{\at}\verb,{const,~$c$\verb,}, & check existence of $c$ and print it \\
   728   \texttt{\at}\verb,{term,~$t$\verb,}, & print term $t$ \\
   729   \texttt{\at}\verb,{prop,~$\phi$\verb,}, & print proposition $\phi$ \\
   730   \texttt{\at}\verb,{prop [display],~$\phi$\verb,}, & print large proposition $\phi$ (with linebreaks) \\
   731   \texttt{\at}\verb,{prop [source],~$\phi$\verb,}, & check proposition $\phi$, print its input \\
   732   \texttt{\at}\verb,{thm,~$a$\verb,}, & print fact $a$ \\
   733   \texttt{\at}\verb,{thm,~$a$~\verb,[no_vars]}, & print fact $a$, fixing schematic variables \\
   734   \texttt{\at}\verb,{thm [source],~$a$\verb,}, & check availability of fact $a$, print its name \\
   735   \texttt{\at}\verb,{text,~$s$\verb,}, & print uninterpreted text $s$ \\
   736   \end{tabular}
   737 
   738   \medskip
   739 
   740   Note that \attrdx{no_vars} given above is \emph{not} an
   741   antiquotation option, but an attribute of the theorem argument given
   742   here.  This might be useful with a diagnostic command like
   743   \isakeyword{thm}, too.
   744 
   745   \medskip The \texttt{\at}\verb,{text, $s$\verb,}, antiquotation is
   746   particularly interesting.  Embedding uninterpreted text within an
   747   informal body might appear useless at first sight.  Here the key
   748   virtue is that the string $s$ is processed as Isabelle output,
   749   interpreting Isabelle symbols appropriately.
   750 
   751   For example, \texttt{\at}\verb,{text "\<forall>\<exists>"}, produces \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}}, according to the standard interpretation of these symbol
   752   (cf.\ \S\ref{sec:doc-prep-symbols}).  Thus we achieve consistent
   753   mathematical notation in both the formal and informal parts of the
   754   document very easily, independently of the term language of
   755   Isabelle.  Manual {\LaTeX} code would leave more control over the
   756   typesetting, but is also slightly more tedious.%
   757 \end{isamarkuptext}%
   758 \isamarkuptrue%
   759 %
   760 \isamarkupsubsection{Interpretation of Symbols \label{sec:doc-prep-symbols}%
   761 }
   762 \isamarkuptrue%
   763 %
   764 \begin{isamarkuptext}%
   765 As has been pointed out before (\S\ref{sec:syntax-symbols}),
   766   Isabelle symbols are the smallest syntactic entities --- a
   767   straightforward generalization of ASCII characters.  While Isabelle
   768   does not impose any interpretation of the infinite collection of
   769   named symbols, {\LaTeX} documents use canonical glyphs for certain
   770   standard symbols \cite{isabelle-isar-ref}.
   771 
   772   The {\LaTeX} code produced from Isabelle text follows a simple
   773   scheme.  You can tune the final appearance by redefining certain
   774   macros, say in \texttt{root.tex} of the document.
   775 
   776   \begin{enumerate}
   777 
   778   \item 7-bit ASCII characters: letters \texttt{A\dots Z} and
   779   \texttt{a\dots z} are output directly, digits are passed as an
   780   argument to the \verb,\isadigit, macro, other characters are
   781   replaced by specifically named macros of the form
   782   \verb,\isacharXYZ,.
   783 
   784   \item Named symbols: \verb,\,\verb,<XYZ>, is turned into
   785   \verb,{\isasymXYZ},; note the additional braces.
   786 
   787   \item Named control symbols: \verb,\,\verb,<^XYZ>, is turned into
   788   \verb,\isactrlXYZ,; subsequent symbols may act as arguments if the
   789   control macro is defined accordingly.
   790 
   791   \end{enumerate}
   792 
   793   You may occasionally wish to give new {\LaTeX} interpretations of
   794   named symbols.  This merely requires an appropriate definition of
   795   \verb,\isasymXYZ,, for \verb,\,\verb,<XYZ>, (see
   796   \texttt{isabelle.sty} for working examples).  Control symbols are
   797   slightly more difficult to get right, though.
   798 
   799   \medskip The \verb,\isabellestyle, macro provides a high-level
   800   interface to tune the general appearance of individual symbols.  For
   801   example, \verb,\isabellestyle{it}, uses the italics text style to
   802   mimic the general appearance of the {\LaTeX} math mode; double
   803   quotes are not printed at all.  The resulting quality of typesetting
   804   is quite good, so this should be the default style for work that
   805   gets distributed to a broader audience.%
   806 \end{isamarkuptext}%
   807 \isamarkuptrue%
   808 %
   809 \isamarkupsubsection{Suppressing Output \label{sec:doc-prep-suppress}%
   810 }
   811 \isamarkuptrue%
   812 %
   813 \begin{isamarkuptext}%
   814 By default, Isabelle's document system generates a {\LaTeX} file for
   815   each theory that gets loaded while running the session.  The
   816   generated \texttt{session.tex} will include all of these in order of
   817   appearance, which in turn gets included by the standard
   818   \texttt{root.tex}.  Certainly one may change the order or suppress
   819   unwanted theories by ignoring \texttt{session.tex} and load
   820   individual files directly in \texttt{root.tex}.  On the other hand,
   821   such an arrangement requires additional maintenance whenever the
   822   collection of theories changes.
   823 
   824   Alternatively, one may tune the theory loading process in
   825   \texttt{ROOT.ML} itself: traversal of the theory dependency graph
   826   may be fine-tuned by adding \verb,use_thy, invocations, although
   827   topological sorting still has to be observed.  Moreover, the ML
   828   operator \verb,no_document, temporarily disables document generation
   829   while executing a theory loader command.  Its usage is like this:
   830 
   831 \begin{verbatim}
   832   no_document use_thy "T";
   833 \end{verbatim}
   834 
   835   \medskip Theory output may be suppressed more selectively, either
   836   via \bfindex{tagged command regions} or \bfindex{ignored material}.
   837 
   838   Tagged command regions works by annotating commands with named tags,
   839   which correspond to certain {\LaTeX} markup that tells how to treat
   840   particular parts of a document when doing the actual type-setting.
   841   By default, certain Isabelle/Isar commands are implicitly marked up
   842   using the predefined tags ``\emph{theory}'' (for theory begin and
   843   end), ``\emph{proof}'' (for proof commands), and ``\emph{ML}'' (for
   844   commands involving ML code).  Users may add their own tags using the
   845   \verb,%,\emph{tag} notation right after a command name.  In the
   846   subsequent example we hide a particularly irrelevant proof:%
   847 \end{isamarkuptext}%
   848 \isamarkuptrue%
   849 \isacommand{lemma}\isamarkupfalse%
   850 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{22}{\isachardoublequoteclose}}%
   851 \isadeliminvisible
   852 \ %
   853 \endisadeliminvisible
   854 %
   855 \isataginvisible
   856 \isacommand{by}\isamarkupfalse%
   857 \ {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{29}{\isacharparenright}}%
   858 \endisataginvisible
   859 {\isafoldinvisible}%
   860 %
   861 \isadeliminvisible
   862 %
   863 \endisadeliminvisible
   864 %
   865 \begin{isamarkuptext}%
   866 The original source has been ``\verb,lemma "x = x" by %invisible (simp),''.
   867   Tags observe the structure of proofs; adjacent commands with the
   868   same tag are joined into a single region.  The Isabelle document
   869   preparation system allows the user to specify how to interpret a
   870   tagged region, in order to keep, drop, or fold the corresponding
   871   parts of the document.  See the \emph{Isabelle System Manual}
   872   \cite{isabelle-sys} for further details, especially on
   873   \texttt{isabelle usedir} and \texttt{isabelle document}.
   874 
   875   Ignored material is specified by delimiting the original formal
   876   source with special source comments
   877   \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
   878   \verb,(,\verb,*,\verb,>,\verb,*,\verb,),.  These parts are stripped
   879   before the type-setting phase, without affecting the formal checking
   880   of the theory, of course.  For example, we may hide parts of a proof
   881   that seem unfit for general public inspection.  The following
   882   ``fully automatic'' proof is actually a fake:%
   883 \end{isamarkuptext}%
   884 \isamarkuptrue%
   885 \isacommand{lemma}\isamarkupfalse%
   886 \ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}int{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isadigit{0}}\ {\isaliteral{3C}{\isacharless}}\ x\ {\isaliteral{2A}{\isacharasterisk}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
   887 %
   888 \isadelimproof
   889 \ \ %
   890 \endisadelimproof
   891 %
   892 \isatagproof
   893 \isacommand{by}\isamarkupfalse%
   894 \ {\isaliteral{28}{\isacharparenleft}}auto{\isaliteral{29}{\isacharparenright}}%
   895 \endisatagproof
   896 {\isafoldproof}%
   897 %
   898 \isadelimproof
   899 %
   900 \endisadelimproof
   901 %
   902 \begin{isamarkuptext}%
   903 \noindent The real source of the proof has been as follows:
   904 
   905 \begin{verbatim}
   906   by (auto(*<*)simp add: zero_less_mult_iff(*>*))
   907 \end{verbatim}
   908 %(*
   909 
   910   \medskip Suppressing portions of printed text demands care.  You
   911   should not misrepresent the underlying theory development.  It is
   912   easy to invalidate the visible text by hiding references to
   913   questionable axioms, for example.%
   914 \end{isamarkuptext}%
   915 \isamarkuptrue%
   916 %
   917 \isadelimtheory
   918 %
   919 \endisadelimtheory
   920 %
   921 \isatagtheory
   922 %
   923 \endisatagtheory
   924 {\isafoldtheory}%
   925 %
   926 \isadelimtheory
   927 %
   928 \endisadelimtheory
   929 \end{isabellebody}%
   930 %%% Local Variables:
   931 %%% mode: latex
   932 %%% TeX-master: "root"
   933 %%% End: