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


   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: