3 \def\isabellecontext{Documents}%
6 \isamarkupsection{Concrete Syntax \label{sec:concrete-syntax}%
10 \begin{isamarkuptext}%
11 The core concept of Isabelle's elaborate infrastructure for concrete
12 syntax is that of general \bfindex{mixfix annotations}. Associated
13 with any kind of constant declaration, mixfixes affect both the
14 grammar productions for the parser and output templates for the
17 In full generality, parser and pretty printer configuration is a
18 rather subtle affair, see \cite{isabelle-ref} for details. Syntax
19 specifications given by end-users need to interact properly with the
20 existing setup of Isabelle/Pure and Isabelle/HOL. It is
21 particularly important to get the precedence of new syntactic
22 constructs right, avoiding ambiguities with existing elements.
24 \medskip Subsequently we introduce a few simple syntax declaration
25 forms that already cover many common situations fairly well.%
29 \isamarkupsubsection{Infix Annotations%
33 \begin{isamarkuptext}%
34 Syntax annotations may be included wherever constants are declared
35 directly or indirectly, including \isacommand{consts},
36 \isacommand{constdefs}, or \isacommand{datatype} (for the
37 constructor operations). Type-constructors may be annotated as
38 well, although this is less frequently encountered in practice (the
39 infix type \isa{{\isasymtimes}} comes to mind).
41 Infix declarations\index{infix annotations} provide a useful special
42 case of mixfixes, where users need not care about the full details
43 of priorities, nesting, spacing, etc. The following example of the
44 exclusive-or operation on boolean values illustrates typical infix
45 declarations arising in practice.%
48 \isacommand{constdefs}\isanewline
49 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
50 \ \ {\isachardoublequote}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
52 \begin{isamarkuptext}%
53 \noindent Now \isa{xor\ A\ B} and \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} refer to the
54 same expression internally. Any curried function with at least two
55 arguments may be associated with infix syntax. For partial
56 applications with less than two operands there is a special notation
57 with \isa{op} prefix: \isa{xor} without arguments is represented
58 as \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}}; together with plain prefix application this
59 turns \isa{xor\ A} into \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ A}.
61 \medskip The keyword \isakeyword{infixl} seen above specifies an
62 infix operator that is nested to the \emph{left}: in iterated
63 applications the more complex expression appears on the left-hand
64 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}.
65 Similarly, \isakeyword{infixr} specifies nesting to the
66 \emph{right}, reading \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} as \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}. In contrast, a \emph{non-oriented} declaration via
67 \isakeyword{infix} would render \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} illegal, but
68 demand explicit parentheses to indicate the intended grouping.
70 The string \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}} in our annotation refers to the
71 concrete syntax to represent the operator (a literal token), while
72 the number \isa{{\isadigit{6}}{\isadigit{0}}} determines the precedence of the construct
73 (i.e.\ the syntactic priorities of the arguments and result). As it
74 happens, Isabelle/HOL already uses up many popular combinations of
75 ASCII symbols for its own use, including both \isa{{\isacharplus}} and \isa{{\isacharplus}{\isacharplus}}. As a rule of thumb, more awkward character combinations are
76 more likely to be still available for user extensions, just as our
77 present \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}}.
79 Operator precedence also needs some special considerations. The
80 admissible range is 0--1000. Very low or high priorities are
81 basically reserved for the meta-logic. Syntax of Isabelle/HOL
82 mainly uses the range of 10--100: the equality infix \isa{{\isacharequal}} is
83 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
84 HOL forms, or use the mostly unused range 100--900.%
88 \isamarkupsubsection{Mathematical Symbols \label{sec:syntax-symbols}%
92 \begin{isamarkuptext}%
93 Concrete syntax based on plain ASCII characters has its inherent
94 limitations. Rich mathematical notation demands a larger repertoire
95 of glyphs. Several standards of extended character sets have been
96 proposed over decades, but none has become universally available so
97 far. Isabelle supports a generic notion of \bfindex{symbols} as the
98 smallest entities of source text, without referring to internal
99 encodings. There are three kinds of such ``generalized
104 \item 7-bit ASCII characters
106 \item named symbols: \verb,\,\verb,<,$ident$\verb,>,
108 \item named control symbols: \verb,\,\verb,<^,$ident$\verb,>,
112 Here $ident$ may be any identifier according to the usual Isabelle
113 conventions. This results in an infinite store of symbols, whose
114 interpretation is left to further front-end tools. For example,
115 both the user-interface of Proof~General + X-Symbol and the Isabelle
116 document processor (see \S\ref{sec:document-preparation}) display
117 the \verb,\,\verb,<forall>, symbol as \isa{{\isasymforall}}.
119 A list of standard Isabelle symbols is given in
120 \cite[appendix~A]{isabelle-sys}. Users may introduce their own
121 interpretation of further symbols by configuring the appropriate
122 front-end tool accordingly, e.g.\ by defining certain {\LaTeX}
123 macros (see also \S\ref{sec:doc-prep-symbols}). There are also a
124 few predefined control symbols, such as \verb,\,\verb,<^sub>, and
125 \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent
126 (printable) symbol, respectively. For example, \verb,A\<^sup>\<star>, is
127 output as \isa{A\isactrlsup {\isasymstar}}.
129 \medskip The following version of our \isa{xor} definition uses a
130 standard Isabelle symbol to achieve typographically more pleasing
136 \isacommand{constdefs}\isanewline
137 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
138 \ \ {\isachardoublequote}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
141 \begin{isamarkuptext}%
142 \noindent The X-Symbol package within Proof~General provides several
143 input methods to enter \isa{{\isasymoplus}} in the text. If all fails one may
144 just type a named entity \verb,\,\verb,<oplus>, by hand; the display
145 will be adapted immediately after continuing input.
147 \medskip A slightly more refined scheme of providing alternative
148 syntax forms uses the \bfindex{print mode} concept of Isabelle (see
149 also \cite{isabelle-ref}). By convention, the mode of
150 ``$xsymbols$'' is enabled whenever Proof~General's X-Symbol mode or
151 {\LaTeX} output is active. Now consider the following hybrid
152 declaration of \isa{xor}:%
157 \isacommand{constdefs}\isanewline
158 \ \ 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
159 \ \ {\isachardoublequote}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline
162 \isacommand{syntax}\ {\isacharparenleft}xsymbols{\isacharparenright}\isanewline
163 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
166 \begin{isamarkuptext}%
167 The \commdx{syntax} command introduced here acts like
168 \isakeyword{consts}, but without declaring a logical constant. The
169 print mode specification of \isakeyword{syntax}, here \isa{{\isacharparenleft}xsymbols{\isacharparenright}}, is optional. Also note that its type merely serves
170 for syntactic purposes, and is \emph{not} checked for consistency
171 with the real constant.
173 \medskip We may now write \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} or \isa{A\ {\isasymoplus}\ B} in
174 input, while output uses the nicer syntax of $xsymbols$, provided
175 that print mode is active. Such an arrangement is particularly
176 useful for interactive development, where users may type plain ASCII
177 text, but gain improved visual feedback from the system.%
181 \isamarkupsubsection{Prefix Annotations%
185 \begin{isamarkuptext}%
186 Prefix syntax annotations\index{prefix annotation} are another
187 degenerate form of mixfixes \cite{isabelle-ref}, without any
188 template arguments or priorities --- just some bits of literal
189 syntax. The following example illustrates this idea idea by
190 associating common symbols with the constructors of a datatype.%
193 \isacommand{datatype}\ currency\ {\isacharequal}\isanewline
194 \ \ \ \ Euro\ nat\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymeuro}{\isachardoublequote}{\isacharparenright}\isanewline
195 \ \ {\isacharbar}\ Pounds\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isasympounds}{\isachardoublequote}{\isacharparenright}\isanewline
196 \ \ {\isacharbar}\ Yen\ nat\ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymyen}{\isachardoublequote}{\isacharparenright}\isanewline
197 \ \ {\isacharbar}\ Dollar\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isachardollar}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
199 \begin{isamarkuptext}%
200 \noindent Here the mixfix annotations on the rightmost column happen
201 to consist of a single Isabelle symbol each: \verb,\,\verb,<euro>,,
202 \verb,\,\verb,<pounds>,, \verb,\,\verb,<yen>,, and \verb,$,. Recall
203 that a constructor like \isa{Euro} actually is a function \isa{nat\ {\isasymRightarrow}\ currency}. The expression \isa{Euro\ {\isadigit{1}}{\isadigit{0}}} will be
204 printed as \isa{{\isasymeuro}\ {\isadigit{1}}{\isadigit{0}}}; only the head of the application is
205 subject to our concrete syntax. This rather simple form already
206 achieves conformance with notational standards of the European
209 Prefix syntax also works for plain \isakeyword{consts} or
210 \isakeyword{constdefs}, of course.%
214 \isamarkupsubsection{Syntax Translations \label{sec:syntax-translations}%
218 \begin{isamarkuptext}%
219 Mixfix syntax annotations work well in those situations where
220 particular constant application forms need to be decorated by
221 concrete syntax; e.g.\ \isa{xor\ A\ B} versus \isa{A\ {\isasymoplus}\ B}
222 covered before. Occasionally the relationship between some piece of
223 notation and its internal form is slightly more involved. Here the
224 concept of \bfindex{syntax translations} enters the scene.
226 Using the raw \isakeyword{syntax}\index{syntax (command)} command we
227 may introduce uninterpreted notational elements, while
228 \commdx{translations} relate input forms with more complex logical
229 expressions. This essentially provides a simple mechanism for
230 syntactic macros; even heavier transformations may be written in ML
233 \medskip A typical example of syntax translations is to decorate
234 relational expressions (set-membership of tuples) with symbolic
235 notation, e.g.\ \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} versus \isa{x\ {\isasymapprox}\ y}.%
238 \isacommand{consts}\isanewline
239 \ \ sim\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set{\isachardoublequote}\isanewline
242 \isacommand{syntax}\isanewline
243 \ \ {\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
245 \isacommand{translations}\isanewline
246 \ \ {\isachardoublequote}x\ {\isasymapprox}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim{\isachardoublequote}\isamarkupfalse%
248 \begin{isamarkuptext}%
249 \noindent Here the name of the dummy constant \isa{{\isacharunderscore}sim} does
250 not really matter, as long as it is not used elsewhere. Prefixing
251 an underscore is a common convention. The \isakeyword{translations}
252 declaration already uses concrete syntax on the left-hand side;
253 internally we relate a raw application \isa{{\isacharunderscore}sim\ x\ y} with
254 \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim}.
256 \medskip Another common application of syntax translations is to
257 provide variant versions of fundamental relational expressions, such
258 as \isa{{\isasymnoteq}} for negated equalities. The following declaration
259 stems from Isabelle/HOL itself:%
262 \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
264 \isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}{\isasymignore}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
266 \begin{isamarkuptext}%
267 \noindent Normally one would introduce derived concepts like this
268 within the logic, using \isakeyword{consts} + \isakeyword{defs}
269 instead of \isakeyword{syntax} + \isakeyword{translations}. The
270 present formulation has the virtue that expressions are immediately
271 replaced by the ``definition'' upon parsing; the effect is reversed
274 Simulating definitions via translations is adequate for very basic
275 principles, where a new representation is a trivial variation on an
276 existing one. On the other hand, syntax translations do not scale
277 up well to large hierarchies of concepts built on each other.%
281 \isamarkupsection{Document Preparation \label{sec:document-preparation}%
285 \begin{isamarkuptext}%
286 Isabelle/Isar is centered around the concept of \bfindex{formal
287 proof documents}\index{documents|bold}. The ultimate result of a
288 formal development effort is meant to be a human-readable record,
289 presented as browsable PDF file or printed on paper. The overall
290 document structure follows traditional mathematical articles, with
291 sections, intermediate explanations, definitions, theorems and
294 \medskip The Isabelle document preparation system essentially acts
295 as a front-end to {\LaTeX}. After checking specifications and
296 proofs formally, the theory sources are turned into typesetting
297 instructions in a schematic manner. This enables users to write
298 authentic reports on theory developments with little effort --- many
299 technical consistency checks are handled by the system.
301 Here is an example to illustrate the idea of Isabelle document
308 \begin{isamarkuptext}%
309 The following datatype definition of \isa{{\isacharprime}a\ bintree} models
310 binary trees with nodes being decorated by elements of type \isa{{\isacharprime}a}.%
313 \isacommand{datatype}\ {\isacharprime}a\ bintree\ {\isacharequal}\isanewline
314 \ \ \ \ \ Leaf\ {\isacharbar}\ Branch\ {\isacharprime}a\ \ {\isachardoublequote}{\isacharprime}a\ bintree{\isachardoublequote}\ \ {\isachardoublequote}{\isacharprime}a\ bintree{\isachardoublequote}\isamarkupfalse%
316 \begin{isamarkuptext}%
317 \noindent The datatype induction rule generated here is of the form
319 \ {\isasymlbrakk}P\ Leaf{\isacharsemicolon}\isanewline
320 \isaindent{\ \ \ \ }{\isasymAnd}a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isachardot}\isanewline
321 \isaindent{\ \ \ \ \ \ \ }{\isasymlbrakk}P\ bintree{\isadigit{1}}{\isacharsemicolon}\ P\ bintree{\isadigit{2}}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Branch\ a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isacharparenright}{\isasymrbrakk}\isanewline
322 \isaindent{\ }{\isasymLongrightarrow}\ P\ bintree%
329 \begin{isamarkuptext}%
330 The above document output has been produced by the following theory
335 The following datatype definition of {\at}{\ttlbrace}text "'a bintree"{\ttrbrace}
336 models binary trees with nodes being decorated by elements
337 of type {\at}{\ttlbrace}typ 'a{\ttrbrace}.
340 datatype 'a bintree =
341 Leaf | Branch 'a "'a bintree" "'a bintree"
344 {\ttback}noindent The datatype induction rule generated here is
345 of the form {\at}{\ttlbrace}thm [display] bintree.induct [no_vars]{\ttrbrace}
349 \noindent Here we have augmented the theory by formal comments
350 (using \isakeyword{text} blocks). The informal parts may again
351 refer to formal entities by means of ``antiquotations'' (such as
352 \texttt{\at}\verb,{text "'a bintree"}, or
353 \texttt{\at}\verb,{typ 'a},), see also \S\ref{sec:doc-prep-text}.%
357 \isamarkupsubsection{Isabelle Sessions%
361 \begin{isamarkuptext}%
362 In contrast to the highly interactive mode of Isabelle/Isar theory
363 development, the document preparation stage essentially works in
364 batch-mode. An Isabelle \bfindex{session} consists of a collection
365 of source files that may contribute to an output document
366 eventually. Each session is derived from a single parent, usually
367 an object-logic image like \texttt{HOL}. This results in an overall
368 tree structure, which is reflected by the output location in the
369 file system (usually rooted at \verb,~/isabelle/browser_info,).
371 \medskip The easiest way to manage Isabelle sessions is via
372 \texttt{isatool mkdir} (generates an initial session source setup)
373 and \texttt{isatool make} (run sessions controlled by
374 \texttt{IsaMakefile}). For example, a new session
375 \texttt{MySession} derived from \texttt{HOL} may be produced as
379 isatool mkdir HOL MySession
383 The \texttt{isatool make} job also informs about the file-system
384 location of the ultimate results. The above dry run should be able
385 to produce some \texttt{document.pdf} (with dummy title, empty table
386 of contents etc.). Any failure at this stage usually indicates
387 technical problems of the {\LaTeX} installation.\footnote{Especially
388 make sure that \texttt{pdflatex} is present; if all fails one may
389 fall back on DVI output by changing \texttt{usedir} options in
390 \texttt{IsaMakefile} \cite{isabelle-sys}.}
392 \medskip The detailed arrangement of the session sources is as
397 \item Directory \texttt{MySession} holds the required theory files
398 $T@1$\texttt{.thy}, \dots, $T@n$\texttt{.thy}.
400 \item File \texttt{MySession/ROOT.ML} holds appropriate ML commands
401 for loading all wanted theories, usually just
402 ``\texttt{use_thy"$T@i$";}'' for any $T@i$ in leaf position of the
405 \item Directory \texttt{MySession/document} contains everything
406 required for the {\LaTeX} stage; only \texttt{root.tex} needs to be
409 The latter file holds appropriate {\LaTeX} code to commence a
410 document (\verb,\documentclass, etc.), and to include the generated
411 files $T@i$\texttt{.tex} for each theory. Isabelle will generate a
412 file \texttt{session.tex} holding {\LaTeX} commands to include all
413 generated theory output files in topologically sorted order, so
414 \verb,\input{session}, in the body of \texttt{root.tex} does the job
417 \item \texttt{IsaMakefile} holds appropriate dependencies and
418 invocations of Isabelle tools to control the batch job. In fact,
419 several sessions may be managed by the same \texttt{IsaMakefile}.
420 See also \cite{isabelle-sys} for further details, especially on
421 \texttt{isatool usedir} and \texttt{isatool make}.
425 One may now start to populate the directory \texttt{MySession}, and
426 the file \texttt{MySession/ROOT.ML} accordingly.
427 \texttt{MySession/document/root.tex} should also be adapted at some
428 point; the default version is mostly self-explanatory. Note that
429 \verb,\isabellestyle, enables fine-tuning of the general appearance
430 of characters and mathematical symbols (see also
431 \S\ref{sec:doc-prep-symbols}).
433 Especially observe the included {\LaTeX} packages \texttt{isabelle}
434 (mandatory), \texttt{isabellesym} (required for mathematical
435 symbols), and the final \texttt{pdfsetup} (provides sane defaults
436 for \texttt{hyperref}, including URL markup) --- all three are
437 distributed with Isabelle. Further packages may be required in
438 particular applications, e.g.\ for unusual mathematical symbols.
440 \medskip Any additional files for the {\LaTeX} stage go into the
441 \texttt{MySession/document} directory as well. In particular,
442 adding \texttt{root.bib} (with that specific name) causes an
443 automatic run of \texttt{bibtex} to process a bibliographic
444 database; see also \texttt{isatool document} in \cite{isabelle-sys}.
446 \medskip Any failure of the document preparation phase in an
447 Isabelle batch session leaves the generated sources in their target
448 location (as pointed out by the accompanied error message). This
449 enables users to trace {\LaTeX} problems with the generated files at
454 \isamarkupsubsection{Structure Markup%
458 \begin{isamarkuptext}%
459 The large-scale structure of Isabelle documents follows existing
460 {\LaTeX} conventions, with chapters, sections, subsubsections etc.
461 The Isar language includes separate \bfindex{markup commands}, which
462 do not affect the formal meaning of a theory (or proof), but result
463 in corresponding {\LaTeX} elements.
465 There are separate markup commands depending on the textual context:
466 in header position (just before \isakeyword{theory}), within the
467 theory body, or within a proof. The header needs to be treated
468 specially here, since ordinary theory and proof commands may only
469 occur \emph{after} the initial \isakeyword{theory} specification.
473 \begin{tabular}{llll}
474 header & theory & proof & default meaning \\\hline
475 & \commdx{chapter} & & \verb,\chapter, \\
476 \commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\
477 & \commdx{subsection} & \commdx{subsect} & \verb,\subsection, \\
478 & \commdx{subsubsection} & \commdx{subsubsect} & \verb,\subsubsection, \\
483 From the Isabelle perspective, each markup command takes a single
484 $text$ argument (delimited by \verb,",~\isa{{\isasymdots}}~\verb,", or
485 \verb,{,\verb,*,~\isa{{\isasymdots}}~\verb,*,\verb,},). After stripping any
486 surrounding white space, the argument is passed to a {\LaTeX} macro
487 \verb,\isamarkupXYZ, for any command \isakeyword{XYZ}. These macros
488 are defined in \verb,isabelle.sty, according to the meaning given in
489 the rightmost column above.
491 \medskip The following source fragment illustrates structure markup
492 of a theory. Note that {\LaTeX} labels may be included inside of
493 section headings as well.
496 header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
498 theory Foo_Bar = Main:
500 subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
508 subsection {\ttlbrace}* Derived rules *{\ttrbrace}
513 subsection {\ttlbrace}* Main theorem {\ttback}label{\ttlbrace}sec:main-theorem{\ttrbrace} *{\ttrbrace}
520 Users may occasionally want to change the meaning of markup
521 commands, say via \verb,\renewcommand, in \texttt{root.tex};
522 \verb,\isamarkupheader, is a good candidate for some tuning, e.g.\
523 moving it up in the hierarchy to become \verb,\chapter,.
526 \renewcommand{\isamarkupheader}[1]{\chapter{#1}}
529 \noindent That particular modification requires change to the
530 document class given in \texttt{root.tex} to something that supports
531 the notion of chapters in the first place, such as
532 \verb,\documentclass{report},.
534 \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to
535 hold the name of the current theory context. This is particularly
536 useful for document headings:
539 \renewcommand{\isamarkupheader}[1]
540 {\chapter{#1}\markright{THEORY~\isabellecontext}}
543 \noindent Make sure to include something like
544 \verb,\pagestyle{headings}, in \texttt{root.tex}; the document
545 should have more than 2 pages to show the effect.%
549 \isamarkupsubsection{Formal Comments and Antiquotations \label{sec:doc-prep-text}%
553 \begin{isamarkuptext}%
554 Isabelle \bfindex{source comments}, which are of the form
555 \verb,(,\verb,*,~\isa{{\isasymdots}}~\verb,*,\verb,),, essentially act like
556 white space and do not really contribute to the content. They
557 mainly serve technical purposes to mark certain oddities in the raw
558 input text. In contrast, \bfindex{formal comments} are portions of
559 text that are associated with formal Isabelle/Isar commands
560 (\bfindex{marginal comments}), or as standalone paragraphs within a
561 theory or proof context (\bfindex{text blocks}).
563 \medskip Marginal comments are part of each command's concrete
564 syntax \cite{isabelle-ref}; the common form is ``\verb,--,~$text$''
565 where $text$ is delimited by \verb,",\isa{{\isasymdots}}\verb,", or
566 \verb,{,\verb,*,~\isa{{\isasymdots}}~\verb,*,\verb,}, as before. Multiple
567 marginal comments may be given at the same time. Here is a simple
571 \isacommand{lemma}\ {\isachardoublequote}A\ {\isacharminus}{\isacharminus}{\isachargreater}\ A{\isachardoublequote}\isanewline
573 \isamarkupcmt{a triviality of propositional logic%
577 \isamarkupcmt{(should not really bother)%
581 \isacommand{by}\ {\isacharparenleft}rule\ impI{\isacharparenright}\ %
582 \isamarkupcmt{implicit assumption step involved here%
586 \begin{isamarkuptext}%
587 \noindent The above output has been produced as follows:
591 -- "a triviality of propositional logic"
592 -- "(should not really bother)"
593 by (rule impI) -- "implicit assumption step involved here"
596 From the {\LaTeX} viewpoint, ``\verb,--,'' acts like a markup
597 command, associated with the macro \verb,\isamarkupcmt, (taking a
600 \medskip Text blocks are introduced by the commands \bfindex{text}
601 and \bfindex{txt}, for theory and proof contexts, respectively.
602 Each takes again a single $text$ argument, which is interpreted as a
603 free-form paragraph in {\LaTeX} (surrounded by some additional
604 vertical space). This behavior may be changed by redefining the
605 {\LaTeX} environments of \verb,isamarkuptext, or
606 \verb,isamarkuptxt,, respectively (via \verb,\renewenvironment,) The
607 text style of the body is determined by \verb,\isastyletext, and
608 \verb,\isastyletxt,; the default setup uses a smaller font within
609 proofs. This may be changed as follows:
612 \renewcommand{\isastyletxt}{\isastyletext}
615 \medskip The $text$ part of each of the various markup commands
616 considered so far essentially inserts \emph{quoted material} into a
617 formal text, mainly for instruction of the reader. An
618 \bfindex{antiquotation} is again a formal object embedded into such
619 an informal portion. The interpretation of antiquotations is
620 limited to some well-formedness checks, with the result being pretty
621 printed to the resulting document. Quoted text blocks together with
622 antiquotations provide very useful means to reference formal
623 entities, with good confidence in getting the technical details
624 right (especially syntax and types).
626 The general syntax of antiquotations is as follows:
627 \texttt{{\at}{\ttlbrace}$name$ $arguments${\ttrbrace}}, or
628 \texttt{{\at}{\ttlbrace}$name$ [$options$] $arguments${\ttrbrace}}
629 for a comma-separated list of options consisting of a $name$ or
630 \texttt{$name$=$value$}. The syntax of $arguments$ depends on the
631 kind of antiquotation, it generally follows the same conventions for
632 types, terms, or theorems as in the formal part of a theory.
634 \medskip Here is an example of the quotation-antiquotation
635 technique: \isa{{\isasymlambda}x\ y{\isachardot}\ x} is a well-typed term.
637 \medskip\noindent The above output has been produced as follows:
640 Here is an example of the quotation-antiquotation technique:
641 {\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term.
645 From the notational change of the ASCII character \verb,%, to the
646 symbol \isa{{\isasymlambda}} we see that the term really got printed by the
647 system (after parsing and type-checking) --- document preparation
648 enables symbolic output by default.
650 \medskip The next example includes an option to modify the
651 \verb,show_types, flag of Isabelle:
652 \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces \isa{{\isasymlambda}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ y{\isasymColon}{\isacharprime}b{\isachardot}\ x}. Type-inference has figured out the most
653 general typings in the present (theory) context. Note that term
654 fragments may acquire different typings due to constraints imposed
655 by previous text (say within a proof), e.g.\ due to the main goal
656 statement given beforehand.
658 \medskip Several further kinds of antiquotations (and options) are
659 available \cite{isabelle-sys}. Here are a few commonly used
665 \texttt{\at}\verb,{typ,~$\tau$\verb,}, & print type $\tau$ \\
666 \texttt{\at}\verb,{term,~$t$\verb,}, & print term $t$ \\
667 \texttt{\at}\verb,{prop,~$\phi$\verb,}, & print proposition $\phi$ \\
668 \texttt{\at}\verb,{prop [display],~$\phi$\verb,}, & print large proposition $\phi$ (with linebreaks) \\
669 \texttt{\at}\verb,{prop [source],~$\phi$\verb,}, & check proposition $\phi$, print its input \\
670 \texttt{\at}\verb,{thm,~$a$\verb,}, & print fact $a$ \\
671 \texttt{\at}\verb,{thm,~$a$~\verb,[no_vars]}, & print fact $a$, fixing schematic variables \\
672 \texttt{\at}\verb,{thm [source],~$a$\verb,}, & check availability of fact $a$, print its name \\
673 \texttt{\at}\verb,{text,~$s$\verb,}, & print uninterpreted text $s$ \\
678 Note that \attrdx{no_vars} given above is \emph{not} an
679 antiquotation option, but an attribute of the theorem argument given
680 here. This might be useful with a diagnostic command like
681 \isakeyword{thm}, too.
683 \medskip The \texttt{\at}\verb,{text, $s$\verb,}, antiquotation is
684 particularly interesting. Embedding uninterpreted text within an
685 informal body might appear useless at first sight. Here the key
686 virtue is that the string $s$ is processed as Isabelle output,
687 interpreting Isabelle symbols appropriately.
689 For example, \texttt{\at}\verb,{text "\<forall>\<exists>"}, produces \isa{{\isasymforall}{\isasymexists}}, according to the standard interpretation of these symbol
690 (cf.\ \S\ref{sec:doc-prep-symbols}). Thus we achieve consistent
691 mathematical notation in both the formal and informal parts of the
692 document very easily. Manual {\LaTeX} code would leave more control
693 over the typesetting, but is also slightly more tedious.%
697 \isamarkupsubsection{Interpretation of Symbols \label{sec:doc-prep-symbols}%
701 \begin{isamarkuptext}%
702 As has been pointed out before (\S\ref{sec:syntax-symbols}),
703 Isabelle symbols are the smallest syntactic entities --- a
704 straightforward generalization of ASCII characters. While Isabelle
705 does not impose any interpretation of the infinite collection of
706 named symbols, {\LaTeX} documents show canonical glyphs for certain
707 standard symbols \cite[appendix~A]{isabelle-sys}.
709 The {\LaTeX} code produced from Isabelle text follows a relatively
710 simple scheme. Users may wish to tune the final appearance by
711 redefining certain macros, say in \texttt{root.tex} of the document.
715 \item 7-bit ASCII characters: letters \texttt{A\dots Z} and
716 \texttt{a\dots z} are output directly, digits are passed as an
717 argument to the \verb,\isadigit, macro, other characters are
718 replaced by specifically named macros of the form
721 \item Named symbols: \verb,\,\verb,<,$XYZ$\verb,>, is turned into
722 \verb,{\isasym,$XYZ$\verb,},; note the additional braces.
724 \item Named control symbols: \verb,\,\verb,<^,$XYZ$\verb,>, is
725 turned into \verb,\isactrl,$XYZ$; subsequent symbols may act as
726 arguments if the corresponding macro is defined accordingly.
730 Users may occasionally wish to give new {\LaTeX} interpretations of
731 named symbols; this merely requires an appropriate definition of
732 \verb,\isasym,$XYZ$\verb,, for \verb,\,\verb,<,$XYZ$\verb,>, (see
733 \texttt{isabelle.sty} for working examples). Control symbols are
734 slightly more difficult to get right, though.
736 \medskip The \verb,\isabellestyle, macro provides a high-level
737 interface to tune the general appearance of individual symbols. For
738 example, \verb,\isabellestyle{it}, uses the italics text style to
739 mimic the general appearance of the {\LaTeX} math mode; double
740 quotes are not printed at all. The resulting quality of typesetting
741 is quite good, so this should be the default style for work that
742 gets distributed to a broader audience.%
746 \isamarkupsubsection{Suppressing Output \label{sec:doc-prep-suppress}%
750 \begin{isamarkuptext}%
751 By default, Isabelle's document system generates a {\LaTeX} file for
752 each theory that gets loaded while running the session. The
753 generated \texttt{session.tex} will include all of these in order of
754 appearance, which in turn gets included by the standard
755 \texttt{root.tex}. Certainly one may change the order or suppress
756 unwanted theories by ignoring \texttt{session.tex} and load
757 individual files directly in \texttt{root.tex}. On the other hand,
758 such an arrangement requires additional maintenance whenever the
759 collection of theories changes.
761 Alternatively, one may tune the theory loading process in
762 \texttt{ROOT.ML} itself: traversal of the theory dependency graph
763 may be fine-tuned by adding \verb,use_thy, invocations, although
764 topological sorting still has to be observed. Moreover, the ML
765 operator \verb,no_document, temporarily disables document generation
766 while executing a theory loader command; its usage is like this:
769 no_document use_thy "T";
772 \medskip Theory output may also be suppressed in smaller portions.
773 For example, research articles, or slides usually do not include the
774 formal content in full. In order to delimit \bfindex{ignored
775 material} special source comments
776 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
777 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), may be included in the
778 text. Only the document preparation system is affected, the formal
779 checking of the theory is performed unchanged.
781 In the subsequent example we suppress the slightly formalistic
782 \isakeyword{theory} + \isakeyword{end} surroundings a theory.
787 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
788 \texttt{theory T = Main:} \\
789 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
791 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
793 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
798 Text may be suppressed in a fine-grained manner. We may even drop
799 vital parts of a proof, pretending that things have been simpler
800 than in reality. For example, this ``fully automatic'' proof is
804 \isacommand{lemma}\ {\isachardoublequote}x\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isacharless}\ x\ {\isacharasterisk}\ x{\isachardoublequote}\isanewline
806 \isacommand{by}\ {\isacharparenleft}auto{\isacharparenright}\isamarkupfalse%
808 \begin{isamarkuptext}%
809 \noindent Here the real source of the proof has been as follows:
812 by (auto(*<*)simp add: int_less_le(*>*))
816 \medskip Ignoring portions of printed text does demand some care by
817 the writer. First of all, the user is responsible not to obfuscate
818 the underlying theory development in an unduly manner. It is fairly
819 easy to invalidate the visible text, e.g.\ by referencing
820 questionable formal items (strange definitions, arbitrary axioms
821 etc.) that have been hidden from sight beforehand.
823 Authentic reports of Isabelle/Isar theories, say as part of a
824 library, should refrain from suppressing parts of the text at all.
825 Other users may need the full information for their own derivative
826 work. If a particular formalization appears inadequate for general
827 public coverage, it is often more appropriate to think of a better
828 way in the first place.
830 \medskip Some technical subtleties of the
831 \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),
832 elements need to be kept in mind, too --- the system performs little
833 sanity checks here. Arguments of markup commands and formal
834 comments must not be hidden, otherwise presentation fails. Open and
835 close parentheses need to be inserted carefully; it is fairly easy
836 to hide the wrong parts, especially after rearranging the theory
844 %%% TeX-master: "root"