3 \def\isabellecontext{Documents}%
6 \isamarkupsection{Concrete Syntax \label{sec:concrete-syntax}%
10 \begin{isamarkuptext}%
11 Concerning Isabelle's ``inner'' language of simply-typed \isa{{\isasymlambda}}-calculus, the core concept of Isabelle's elaborate
12 infrastructure for concrete syntax is that of general
13 \bfindex{mixfix annotations}. Associated with any kind of constant
14 declaration, mixfixes affect both the grammar productions for the
15 parser and output templates for the pretty printer.
17 In full generality, the whole affair of parser and pretty printer
18 configuration is rather subtle, see \cite{isabelle-ref} for further
19 details. Any syntax specifications given by end-users need to
20 interact properly with the existing setup of Isabelle/Pure and
21 Isabelle/HOL. It is particularly important to get the precedence of
22 new syntactic constructs right, avoiding ambiguities with existing
25 \medskip Subsequently we introduce a few simple declaration forms
26 that already cover the most common situations fairly well.%
30 \isamarkupsubsection{Infix Annotations%
34 \begin{isamarkuptext}%
35 Syntax annotations may be included wherever constants are declared
36 directly or indirectly, including \isacommand{consts},
37 \isacommand{constdefs}, or \isacommand{datatype} (for the
38 constructor operations). Type-constructors may be annotated as
39 well, although this is less frequently encountered in practice
40 (\isa{{\isacharasterisk}} and \isa{{\isacharplus}} types may come to mind).
42 Infix declarations\index{infix annotations} provide a useful special
43 case of mixfixes, where users need not care about the full details
44 of priorities, nesting, spacing, etc. The subsequent example of the
45 exclusive-or operation on boolean values illustrates typical infix
46 declarations arising in practice.%
49 \isacommand{constdefs}\isanewline
50 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
51 \ \ {\isachardoublequote}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
53 \begin{isamarkuptext}%
54 \noindent Now \isa{xor\ A\ B} and \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} refer to the
55 same expression internally. Any curried function with at least two
56 arguments may be associated with infix syntax. For partial
57 applications with less than two operands there is a special notation
58 with \isa{op} prefix: \isa{xor} without arguments is represented
59 as \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}}; together with plain prefix application this
60 turns \isa{xor\ A} into \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ A}.
62 \medskip The string \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}} in the above annotation
63 refers to the bit of concrete syntax to represent the operator,
64 while the number \isa{{\isadigit{6}}{\isadigit{0}}} determines the precedence of the
65 construct (i.e.\ the syntactic priorities of the arguments and
68 As it happens, Isabelle/HOL already spends many popular combinations
69 of ASCII symbols for its own use, including both \isa{{\isacharplus}} and
70 \isa{{\isacharplus}{\isacharplus}}. Slightly more awkward combinations like the present
71 \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}} tend to be available for user extensions. The current
72 arrangement of inner syntax may be inspected via
73 \commdx{print\protect\_syntax}, albeit its output is enormous.
75 Operator precedence also needs some special considerations. The
76 admissible range is 0--1000. Very low or high priorities are
77 basically reserved for the meta-logic. Syntax of Isabelle/HOL
78 mainly uses the range of 10--100: the equality infix \isa{{\isacharequal}} is
79 centered at 50, logical connectives (like \isa{{\isasymor}} and \isa{{\isasymand}}) are below 50, and algebraic ones (like \isa{{\isacharplus}} and \isa{{\isacharasterisk}}) above 50. User syntax should strive to coexist with common
80 HOL forms, or use the mostly unused range 100--900.
82 \medskip The keyword \isakeyword{infixl} specifies an operator that
83 is nested to the \emph{left}: in iterated applications the more
84 complex expression appears on the left-hand side: \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} stands for \isa{{\isacharparenleft}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B{\isacharparenright}\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C}. Similarly,
85 \isakeyword{infixr} specifies to nesting to the \emph{right},
86 reading \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} as \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}. In
87 contrast, a \emph{non-oriented} declaration via \isakeyword{infix}
88 would have rendered \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} illegal, but demand
89 explicit parentheses about the intended grouping.%
93 \isamarkupsubsection{Mathematical Symbols \label{sec:syntax-symbols}%
97 \begin{isamarkuptext}%
98 Concrete syntax based on plain ASCII characters has its inherent
99 limitations. Rich mathematical notation demands a larger repertoire
100 of symbols. Several standards of extended character sets have been
101 proposed over decades, but none has become universally available so
102 far, not even Unicode\index{Unicode}. Isabelle supports a generic
103 notion of \bfindex{symbols} as the smallest entities of source text,
104 without referring to internal encodings.
106 There are three kinds of such ``generalized characters'' available:
110 \item 7-bit ASCII characters
112 \item named symbols: \verb,\,\verb,<,$ident$\verb,>,
114 \item named control symbols: \verb,\,\verb,<^,$ident$\verb,>,
118 Here $ident$ may be any identifier according to the usual Isabelle
119 conventions. This results in an infinite store of symbols, whose
120 interpretation is left to further front-end tools. For example,
121 both by the user-interface of Proof~General + X-Symbol and the
122 Isabelle document processor (see \S\ref{sec:document-preparation})
123 display the \verb,\,\verb,<forall>, symbol really as ``$\forall$''.
125 A list of standard Isabelle symbols is given in
126 \cite[appendix~A]{isabelle-sys}. Users may introduce their 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 shown as ``\isa{A\isactrlsup {\isasymstar}}''.
135 \medskip The following version of our \isa{xor} definition uses a
136 standard Isabelle symbol to achieve typographically pleasing output.%
141 \isacommand{constdefs}\isanewline
142 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
143 \ \ {\isachardoublequote}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
146 \begin{isamarkuptext}%
147 \noindent The X-Symbol package within Proof~General provides several
148 input methods to enter \isa{{\isasymoplus}} in the text. If all fails one may
149 just type \verb,\,\verb,<oplus>, by hand; the display will be
150 adapted immediately after continuing input.
152 \medskip A slightly more refined scheme is to provide alternative
153 syntax via the \bfindex{print mode} concept of Isabelle (see also
154 \cite{isabelle-ref}). By convention, the mode of ``$xsymbols$'' is
155 enabled whenever Proof~General's X-Symbol mode (or {\LaTeX} output)
156 is active. Consider the following hybrid declaration of \isa{xor}.%
161 \isacommand{constdefs}\isanewline
162 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
163 \ \ {\isachardoublequote}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline
166 \isacommand{syntax}\ {\isacharparenleft}xsymbols{\isacharparenright}\isanewline
167 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
170 \begin{isamarkuptext}%
171 The \commdx{syntax} command introduced here acts like
172 \isakeyword{consts}, but without declaring a logical constant; an
173 optional print mode specification may be given, too. Note that the
174 type declaration given here merely serves for syntactic purposes,
175 and is not checked for consistency with the real constant.
177 \medskip We may now write either \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}} or \isa{{\isasymoplus}} in
178 input, while output uses the nicer syntax of $xsymbols$, provided
179 that print mode is presently active. Such an arrangement is
180 particularly useful for interactive development, where users may
181 type plain ASCII text, but gain improved visual feedback from the
182 system (say in current goal output).
185 Alternative syntax declarations are apt to result in varying
186 occurrences of concrete syntax in the input sources. Isabelle
187 provides no systematic way to convert alternative syntax expressions
188 back and forth; print modes only affect situations where formal
189 entities are pretty printed by the Isabelle process (e.g.\ output of
190 terms and types), but not the original theory text.
193 \medskip The following variant makes the alternative \isa{{\isasymoplus}}
194 notation only available for output. Thus we may enforce input
195 sources to refer to plain ASCII only, but effectively disable
196 cut-and-paste from output as well.%
199 \isacommand{syntax}\ {\isacharparenleft}xsymbols\ \isakeyword{output}{\isacharparenright}\isanewline
200 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
202 \isamarkupsubsection{Prefix Annotations%
206 \begin{isamarkuptext}%
207 Prefix syntax annotations\index{prefix annotation} are just another
208 degenerate form of general mixfixes \cite{isabelle-ref}, without any
209 template arguments or priorities --- just some bits of literal
210 syntax. The following example illustrates this idea idea by
211 associating common symbols with the constructors of a datatype.%
214 \isacommand{datatype}\ currency\ {\isacharequal}\isanewline
215 \ \ \ \ Euro\ nat\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymeuro}{\isachardoublequote}{\isacharparenright}\isanewline
216 \ \ {\isacharbar}\ Pounds\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isasympounds}{\isachardoublequote}{\isacharparenright}\isanewline
217 \ \ {\isacharbar}\ Yen\ nat\ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymyen}{\isachardoublequote}{\isacharparenright}\isanewline
218 \ \ {\isacharbar}\ Dollar\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isachardollar}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
220 \begin{isamarkuptext}%
221 \noindent Here the mixfix annotations on the rightmost column happen
222 to consist of a single Isabelle symbol each: \verb,\,\verb,<euro>,,
223 \verb,\,\verb,<pounds>,, \verb,\,\verb,<yen>,, and \verb,$,. Recall
224 that a constructor like \isa{Euro} actually is a function \isa{nat\ {\isasymRightarrow}\ currency}. An expression like \isa{Euro\ {\isadigit{1}}{\isadigit{0}}} will be
225 printed as \isa{{\isasymeuro}\ {\isadigit{1}}{\isadigit{0}}}; only the head of the application is
226 subject to our concrete syntax. This simple form already achieves
227 conformance with notational standards of the European Commission.
229 \medskip Certainly, the same idea of prefix syntax also works for
230 \isakeyword{consts}, \isakeyword{constdefs} etc. The slightly
231 unusual syntax declaration below decorates the existing \isa{currency} type with the international currency symbol \isa{{\isasymcurrency}}
232 (\verb,\,\verb,<currency>,).%
235 \isacommand{syntax}\isanewline
236 \ \ currency\ {\isacharcolon}{\isacharcolon}\ type\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymcurrency}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
238 \begin{isamarkuptext}%
239 \noindent Here \isa{type} refers to the builtin syntactic category
240 of Isabelle types. We may now write down funny things like \isa{{\isasymeuro}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ {\isasymcurrency}}, for example.%
244 \isamarkupsubsection{Syntax Translations \label{sec:syntax-translations}%
248 \begin{isamarkuptext}%
249 Mixfix syntax annotations work well for those situations where a
250 particular constant application forms need to be decorated by
251 concrete syntax; just reconsider \isa{xor\ A\ B} versus \isa{A\ {\isasymoplus}\ B} covered before. Occasionally, the relationship between some
252 piece of notation and its internal form is slightly more involved.
253 Here the concept of \bfindex{syntax translations} enters the scene.
255 Using the raw \isakeyword{syntax}\index{syntax (command)} command we
256 may introduce uninterpreted notational elements, while
257 \commdx{translations} relates the input forms with more complex
258 logical expressions. This essentially provides a simple mechanism
259 for for syntactic macros; even heavier transformations may be
260 programmed in ML \cite{isabelle-ref}.
262 \medskip A typical example of syntax translations is to decorate
263 relational expressions (set membership of tuples) with nice symbolic
264 notation, such as \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} versus \isa{x\ {\isasymapprox}\ y}.%
267 \isacommand{consts}\isanewline
268 \ \ sim\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set{\isachardoublequote}\isanewline
271 \isacommand{syntax}\isanewline
272 \ \ {\isachardoublequote}{\isacharunderscore}sim{\isachardoublequote}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infix}\ {\isachardoublequote}{\isasymapprox}{\isachardoublequote}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline
274 \isacommand{translations}\isanewline
275 \ \ {\isachardoublequote}x\ {\isasymapprox}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim{\isachardoublequote}\isamarkupfalse%
277 \begin{isamarkuptext}%
278 \noindent Here the name of the dummy constant \isa{{\isacharunderscore}sim} does
279 not really matter, as long as it is not used elsewhere. Prefixing
280 an underscore is a common convention. The \isakeyword{translations}
281 declaration already uses concrete syntax on the left-hand side;
282 internally we relate a raw application \isa{{\isacharunderscore}sim\ x\ y} with
283 \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim}.
285 \medskip Another common application of syntax translations is to
286 provide variant versions of fundamental relational expressions, such
287 as \isa{{\isasymnoteq}} for negated equalities. The following declaration
288 stems from Isabelle/HOL itself:%
291 \isacommand{syntax}\ {\isachardoublequote}{\isacharunderscore}not{\isacharunderscore}equal{\isachardoublequote}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymnoteq}{\isasymignore}{\isachardoublequote}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline
293 \isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}{\isasymignore}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
295 \begin{isamarkuptext}%
296 \noindent Normally one would introduce derived concepts like this
297 within the logic, using \isakeyword{consts} + \isakeyword{defs}
298 instead of \isakeyword{syntax} + \isakeyword{translations}. The
299 present formulation has the virtue that expressions are immediately
300 replaced by its ``definition'' upon parsing; the effect is reversed
301 upon printing. Internally, \isa{{\isasymnoteq}} never appears.
303 Simulating definitions via translations is adequate for very basic
304 logical concepts, where a new representation is a trivial variation
305 on an existing one. On the other hand, syntax translations do not
306 scale up well to large hierarchies of concepts built on each other.%
310 \isamarkupsection{Document Preparation \label{sec:document-preparation}%
314 \begin{isamarkuptext}%
315 Isabelle/Isar is centered around the concept of \bfindex{formal
316 proof documents}\index{documents|bold}. Ultimately the result of
317 the user's theory development efforts is meant to be a
318 human-readable record, presented as a browsable PDF file or printed
319 on paper. The overall document structure follows traditional
320 mathematical articles, with sectioning, intermediate explanations,
321 definitions, theorem statements and proofs.
323 The Isar proof language \cite{Wenzel-PhD}, which is not covered in
324 this book, admits to write formal proof texts that are acceptable
325 both to the machine and human readers at the same time. Thus
326 marginal comments and explanations may be kept at a minimum. Even
327 without proper coverage of human-readable proofs, Isabelle document
328 is very useful to produce formally derived texts (elaborating on the
329 specifications etc.). Unstructured proof scripts given here may be
330 just ignored by readers, or intentionally suppressed from the text
331 by the writer (see also \S\ref{sec:doc-prep-suppress}).
333 \medskip The Isabelle document preparation system essentially acts
334 like a formal front-end to {\LaTeX}. After checking specifications
335 and proofs, the theory sources are turned into typesetting
336 instructions in a well-defined manner. This enables users to write
337 authentic reports on formal theory developments with little
338 additional effort, the most tedious consistency checks are handled
343 \isamarkupsubsection{Isabelle Sessions%
347 \begin{isamarkuptext}%
348 In contrast to the highly interactive mode of Isabelle/Isar theory
349 development, the document preparation stage essentially works in
350 batch-mode. An Isabelle \bfindex{session} essentially consists of a
351 collection of theory source files that contribute to a single output
352 document eventually. Session is derived from a single parent each
353 (usually an object-logic image like \texttt{HOL}), resulting in an
354 overall tree structure that is reflected in the output location
355 within the file system (usually rooted at
356 \verb,~/isabelle/browser_info,).
358 Here is the canonical arrangement of sources of a session called
363 \item Directory \texttt{MySession} contains the required theory
364 files ($A@1$\texttt{.thy}, \dots, $A@n$\texttt{.thy}).
366 \item File \texttt{MySession/ROOT.ML} holds appropriate ML commands
367 for loading all wanted theories, usually just
368 ``\texttt{use_thy~"$A@i$";}'' for any $A@i$ in leaf position of the
369 theory dependency graph.
371 \item Directory \texttt{MySession/document} contains everything
372 required for the {\LaTeX} stage; only \texttt{root.tex} needs to be
375 The latter file holds appropriate {\LaTeX} code to commence a
376 document (\verb,\documentclass, etc.), and to include the generated
377 files $A@i$\texttt{.tex} for each theory. The generated
378 \texttt{session.tex} will hold {\LaTeX} commands to include all
379 theory output files in topologically sorted order, so
380 \verb,\input{session}, in \texttt{root.tex} will do it in most
383 \item In addition, \texttt{IsaMakefile} outside of the directory
384 \texttt{MySession} holds appropriate dependencies and invocations of
385 Isabelle tools to control the batch job. In fact, several sessions
386 may be controlled by the same \texttt{IsaMakefile}. See also
387 \cite{isabelle-sys} for further details, especially on
388 \texttt{isatool usedir} and \texttt{isatool make}.
392 With everything put in its proper place, \texttt{isatool make}
393 should be sufficient to process the Isabelle session completely,
394 with the generated document appearing in its proper place.
396 \medskip In practice, users may want to have \texttt{isatool mkdir}
397 generate an initial working setup without further ado. For example,
398 an empty session \texttt{MySession} derived from \texttt{HOL} may be
402 isatool mkdir HOL MySession
406 This processes the session with sensible default options, including
407 verbose mode to tell the user where the ultimate results will
408 appear. The above dry run should produce should already be able to
409 produce a single page of output (with a dummy title, empty table of
410 contents etc.). Any failure at that stage is likely to indicate
411 technical problems with the user's {\LaTeX}
412 installation.\footnote{Especially make sure that \texttt{pdflatex}
413 is present; if all fails one may fall back on DVI output by changing
414 \texttt{usedir} options \cite{isabelle-sys}.}
416 \medskip One may now start to populate the directory
417 \texttt{MySession}, and the file \texttt{MySession/ROOT.ML}
418 accordingly. \texttt{MySession/document/root.tex} should be also
419 adapted at some point; the default version is mostly
420 self-explanatory. Note that the \verb,\isabellestyle, enables
421 fine-tuning of the general appearance of characters and mathematical
422 symbols (see also \S\ref{sec:doc-prep-symbols}).
424 Especially note the standard inclusion of {\LaTeX} packages
425 \texttt{isabelle} (mandatory), and \texttt{isabellesym} (required
426 for mathematical symbols), and the final \texttt{pdfsetup} (provides
427 handsome defaults for \texttt{hyperref}, including URL markup).
428 Further {\LaTeX} packages further packages may required in
429 particular applications, e.g.\ for unusual Isabelle symbols.
431 \medskip Further auxiliary files for the {\LaTeX} stage should be
432 included in the \texttt{MySession/document} directory, e.g.\
433 additional {\TeX} sources or graphics. In particular, adding
434 \texttt{root.bib} here (with that specific name) causes an automatic
435 run of \texttt{bibtex} to process a bibliographic database; see for
436 further commodities \texttt{isatool document} covered in
439 \medskip Any failure of the document preparation phase in an
440 Isabelle batch session leaves the generated sources in there target
441 location (as pointed out by the accompanied error message). In case
442 of {\LaTeX} errors, users may trace error messages at the file
443 position of the generated text.%
447 \isamarkupsubsection{Structure Markup%
451 \begin{isamarkuptext}%
452 The large-scale structure of Isabelle documents follows existing
453 {\LaTeX} conventions, with chapters, sections, subsubsections etc.
454 The Isar language includes separate \bfindex{markup commands}, which
455 do not effect the formal content of a theory (or proof), but result
456 in corresponding {\LaTeX} elements issued to the output.
458 There are separate markup commands for different formal contexts: in
459 header position (just before a \isakeyword{theory} command), within
460 the theory body, or within a proof. Note that the header needs to
461 be treated specially, since ordinary theory and proof commands may
462 only occur \emph{after} the initial \isakeyword{theory}
467 \begin{tabular}{llll}
468 header & theory & proof & default meaning \\\hline
469 & \commdx{chapter} & & \verb,\chapter, \\
470 \commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\
471 & \commdx{subsection} & \commdx{subsect} & \verb,\subsection, \\
472 & \commdx{subsubsection} & \commdx{subsubsect} & \verb,\subsubsection, \\
477 From the Isabelle perspective, each markup command takes a single
478 $text$ argument (delimited by \verb,",\dots\verb,", or
479 \verb,{,\verb,*,~\dots~\verb,*,\verb,},). After stripping any
480 surrounding white space, the argument is passed to a {\LaTeX} macro
481 \verb,\isamarkupXYZ, for any command \isakeyword{XYZ}. These macros
482 are defined in \verb,isabelle.sty, according to the meaning given in
483 the rightmost column above.
485 \medskip The following source fragment illustrates structure markup
486 of a theory. Note that {\LaTeX} labels may be included inside of
487 section headings as well.
490 header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
492 theory Foo_Bar = Main:
494 subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
502 subsection {\ttlbrace}* Derived rules *{\ttrbrace}
507 subsection {\ttlbrace}* Main theorem {\ttback}label{\ttlbrace}sec:main-theorem{\ttrbrace} *{\ttrbrace}
514 Users may occasionally want to change the meaning of markup
515 commands, say via \verb,\renewcommand, in \texttt{root.tex}. The
516 \verb,\isamarkupheader, is a good candidate for some adaption, e.g.\
517 moving it up in the hierarchy to become \verb,\chapter,.
520 \renewcommand{\isamarkupheader}[1]{\chapter{#1}}
523 \noindent Certainly, this requires to change the default
524 \verb,\documentclass{article}, in \texttt{root.tex} to something
525 that supports the notion of chapters in the first place, e.g.\
526 \verb,\documentclass{report},.
528 \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to
529 hold the name of the current theory context. This is particularly
530 useful for document headings:
533 \renewcommand{\isamarkupheader}[1]
534 {\chapter{#1}\markright{THEORY~\isabellecontext}}
537 \noindent Make sure to include something like
538 \verb,\pagestyle{headings}, in \texttt{root.tex}; the document
539 should have more than 2 pages to show the effect.%
543 \isamarkupsubsection{Formal Comments and Antiquotations%
547 \begin{isamarkuptext}%
550 Source comments of the form \verb,(,\verb,*,~\dots~\verb,*,\verb,),
551 essentially act like white space and do not contribute to the formal
552 text at all. They mainly serve technical purposes to mark certain
553 oddities or problems with the raw sources.
555 In contrast, \bfindex{formal comments} are portions of text that are
556 associated with formal Isabelle/Isar commands (\bfindex{marginal
557 comments}), or even as stanalone paragraphs positioned explicitly
558 within a theory or proof context (\bfindex{text blocks}).
560 \medskip Marginal comments are part of each command's concrete
561 syntax \cite{isabelle-ref}; the common form \verb,--,~text, where
562 $text$, delimited by \verb,",\dots\verb,", or
563 \verb,{,\verb,*,~\dots~\verb,*,\verb,}, as usual. Multiple marginal
564 comments may be given at the same time. Here is a simple example:
568 -- "a triviality of propositional logic"
569 -- "(should not really bother)"
570 by (rule impI) -- "implicit assumption step involved here"
573 From the {\LaTeX} view, \verb,--, acts like a markup command, the
574 corresponding macro is \verb,\isamarkupcmt, (of a single argument).
576 \medskip The commands \bfindex{text} and \bfindex{txt} both
577 introduce a text block (for theory and proof contexts,
578 respectively), taking a single $text$ argument. The {\LaTeX} output
579 appears as a free-form text, surrounded with separate paragraphs and
580 additional vertical spacing. This behavior is determined by the
581 {\LaTeX} environment definitions \verb,isamarkuptext, and
582 \verb,isamarkuptxt,, respectively. This may be changed via
583 \verb,\renewenvironment,, but it is often sufficient to redefine
584 \verb,\isastyletext, or \verb,\isastyletxt, only, which determine
587 \medskip The $text$ part of each of the various markup commands
588 considered so far essentially inserts \emph{quoted} material within
589 a formal text, essentially for instruction of the reader only
590 (arbitrary {\LaTeX} macros may be included).
592 An \bfindex{antiquotation} is again a formal object that has been
593 embedded into such an informal portion of text. Typically, the
594 interpretation of an antiquotation is limited to well-formedness
595 checks, with the result being pretty printed into the resulting
596 document output. So quoted text blocks together with antiquotations
597 provide very handsome means to reference formal entities within
598 informal expositions, with a high level of confidence in the
599 technical details (especially syntax and types).
601 The general format of antiquotations is as follows:
602 \texttt{{\at}{\ttlbrace}$name$ $arguments${\ttrbrace}}, or
603 \texttt{{\at}{\ttlbrace}$name$ [$options$] $arguments${\ttrbrace}}
604 for a comma-separated list of $name$ or assignments
605 \texttt{$name$=$value$} of $options$ (see \cite{isabelle-isar-ref}
606 for details). The syntax of $arguments$ depends on the
607 antiquotation name, it generally follows the same conventions for
608 types, terms, or theorems as in the formal part of a theory.
610 \medskip Here is an example use of the quotation-antiquotation
611 technique: \isa{{\isasymlambda}x\ y{\isachardot}\ x} is a well-typed term.
613 \medskip This output has been produced as follows:
616 Here is an example use of the quotation-antiquotation technique:
617 {\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term.
621 From the notational change of the ASCII character \verb,%, to the
622 symbol \isa{{\isasymlambda}} we see that the term really got printed by the
623 system --- recall that the document preparation system enables
624 symbolic output by default.
626 \medskip In the following example we include an option to enable the
627 \verb,show_types, flag of Isabelle: the antiquotation
628 \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces \isa{{\isasymlambda}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ y{\isasymColon}{\isacharprime}b{\isachardot}\ x}. Here type-inference has figured out the
629 most general typings in the present (theory) context. Within a
630 proof, one may get different results according to typings that have
631 already been figured out in the text so far, say some fixed
632 variables in the main statement given before hand.
634 \medskip Several further kinds of antiquotations (and options) are
635 available \cite{isabelle-sys}. The most commonly used combinations
641 \texttt{\at}\verb,{typ,~$\tau$\verb,}, & print type $\tau$ \\
642 \texttt{\at}\verb,{term,~$t$\verb,}, & print term $t$ \\
643 \texttt{\at}\verb,{prop,~$\phi$\verb,}, & print proposition $\phi$ \\
644 \texttt{\at}\verb,{prop [source],~$\phi$\verb,}, & check proposition $\phi$, print its input \\
645 \texttt{\at}\verb,{thm,~$a$\verb,}, & print fact $a$ \\
646 \texttt{\at}\verb,{thm,~$a$~\verb,[no_vars]}, & print fact $a$, fixing schematic variables \\
647 \texttt{\at}\verb,{thm [source],~$a$\verb,}, & check availability of fact $a$, print its name \\
648 \texttt{\at}\verb,{text,~$s$\verb,}, & print uninterpreted text $s$ \\
653 Note that \verb,no_vars, given above is \emph{not} an option, but
654 merely an attribute of the theorem argument given here.
656 The \texttt{\at}\verb,{text, $s$\verb,}, antiquotation is
657 particularly interesting. Embedding uninterpreted text within an
658 informal text body might appear useless at first sight. Here the
659 key virtue is that the string $s$ is processed as proper Isabelle
660 output, interpreting Isabelle symbols (\S\ref{sec:syntax-symbols})
663 For example, \texttt{\at}\verb,{text "\<forall>\<exists>"}, produces \isa{{\isasymforall}{\isasymexists}},
664 according to the standard interpretation of these symbol (cf.\
665 \S\ref{sec:doc-prep-symbols}). Thus we achieve consistent
666 mathematical notation in both the formal and informal parts of the
667 document very easily. Manual {\LaTeX} code leaves more control over
668 the type-setting, but is slightly more tedious. Also note that
669 Isabelle symbols may be also displayed within the editor buffer of
674 \isamarkupsubsection{Interpretation of symbols \label{sec:doc-prep-symbols}%
678 \begin{isamarkuptext}%
681 According to \S\ref{sec:syntax-symbols}, the smalles syntactic
682 entities of Isabelle text are symbols, a straight-forward
683 generalization of ASCII characters. Concerning document
684 preperation, symbols are translated uniformly to {\LaTeX} code as
687 \begin{enumerate} \item 7-bit ASCII characters: letters
688 \texttt{A\dots Z} and \texttt{a\dots z} are output verbatim, digits
689 are passed as an argument to the \verb,\isadigit, macro, other
690 characters are replaced by specific macros \verb,\isacharXYZ, (see
691 also \texttt{isabelle.sty}).
693 \item Named symbols: \verb,\,\verb,<,$XYZ$\verb,>, become
694 \verb,\{\isasym,$XYZ$\verb,}, each (note the additional braces).
695 See \cite[appendix~A]{isabelle-sys} and \texttt{isabellesym.sty} for
696 the collection of predefined standard symbols.
698 \item Named control symbols: \verb,\,\verb,<^,$XYZ$\verb,>, become
699 \verb,\isactrl,$XYZ$; subsequent symbols may act as arguments, if
700 the corresponding macro is defined accordingly.
705 \isamarkupsubsection{Suppressing Output \label{sec:doc-prep-suppress}%
709 \begin{isamarkuptext}%
710 By default Isabelle's document system generates a {\LaTeX} source
711 file for each theory that happens to get loaded during the session.
712 The generated \texttt{session.tex} will include all of these in
713 order of appearance, which in turn gets included by the standard
714 \texttt{root.tex}. Certainly one may change the order of appearance
715 or suppress unwanted theories by ignoring \texttt{session.tex} and
716 include individual files in \texttt{root.tex} by hand. On the other
717 hand, such an arrangement requires additional maintenance chores
718 whenever the collection of theories changes.
720 Alternatively, one may tune the theory loading process in
721 \texttt{ROOT.ML} itself: traversal of the theory dependency graph
722 may be fine-tuned by adding further \verb,use_thy, invocations,
723 although topological sorting still has to be observed. Moreover,
724 the ML operator \verb,no_document, temporarily disables document
725 generation while executing a theory loader command; its usage is
729 no_document use_thy "A";
732 \medskip Theory output may be also suppressed in smaller portions as
733 well. For example, research papers or slides usually do not include
734 the formal content in full. In order to delimit \bfindex{ignored
735 material} special source comments
736 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
737 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), may be included in the
738 text. Only the document preparation system is affected, the formal
739 checking the theory is performed as before.
741 In the following example we suppress the slightly formalistic
742 \isakeyword{theory} + \isakeyword{end} surroundings a theory.
747 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
748 \texttt{theory A = Main:} \\
749 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
751 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
753 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
758 Text may be suppressed in a fine grained manner. For example, we
759 may even drop vital parts of a formal proof, pretending that things
760 have been simpler than in reality. For example, the following
761 ``fully automatic'' proof is actually a fake:%
764 \isacommand{lemma}\ {\isachardoublequote}x\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isacharless}\ x\ {\isacharasterisk}\ x{\isachardoublequote}\isanewline
766 \isacommand{by}\ {\isacharparenleft}auto{\isacharparenright}\isamarkupfalse%
768 \begin{isamarkuptext}%
769 \noindent Here the real source of the proof has been as follows:
772 by (auto(*<*)simp add: int_less_le(*>*))
776 \medskip Ignoring portions of printed does demand some care by the
777 user. First of all, the writer is responsible not to obfuscate the
778 underlying formal development in an unduly manner. It is fairly
779 easy to invalidate the remaining visible text, e.g.\ by referencing
780 questionable formal items (strange definitions, arbitrary axioms
781 etc.) that have been hidden from sight beforehand.
783 Some minor technical subtleties of the
784 \verb,(,\verb,*,\verb,<,\verb,*,\verb,),-\verb,(,\verb,*,\verb,>,\verb,*,\verb,),
785 elements need to be kept in mind as well, since the system performs
786 little sanity checks here. Arguments of markup commands and formal
787 comments must not be hidden, otherwise presentation fails. Open and
788 close parentheses need to be inserted carefully; it is fairly easy
789 to hide the wrong parts, especially after rearranging the sources.
791 \medskip Authentic reports of formal theories, say as part of a
792 library, usually should refrain from suppressing parts of the text
793 at all. Other users may need the full information for their own
794 derivative work. If a particular formalization appears inadequate
795 for general public coverage, it is often more appropriate to think
796 of a better way in the first place.%
803 %%% TeX-master: "root"