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