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 also \cite{isabelle-ref}.
19 Syntax specifications given by end-users need to interact properly
20 with the 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 most 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
39 (\isa{{\isacharasterisk}} and \isa{{\isacharplus}} types may come 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 string \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}} in the above annotation
62 refers to the bit of concrete syntax to represent the operator,
63 while the number \isa{{\isadigit{6}}{\isadigit{0}}} determines the precedence of the
64 construct (i.e.\ the syntactic priorities of the arguments and
67 As it happens, Isabelle/HOL already spends many popular combinations
68 of ASCII symbols for its own use, including both \isa{{\isacharplus}} and
69 \isa{{\isacharplus}{\isacharplus}}. Slightly more awkward combinations like the present
70 \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}} tend to be available for user extensions. The current
71 arrangement of inner syntax may be inspected via
72 \commdx{print\protect\_syntax}, albeit its output is enormous.
74 Operator precedence also needs some special considerations. The
75 admissible range is 0--1000. Very low or high priorities are
76 basically reserved for the meta-logic. Syntax of Isabelle/HOL
77 mainly uses the range of 10--100: the equality infix \isa{{\isacharequal}} is
78 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
79 HOL forms, or use the mostly unused range 100--900.
81 The keyword \isakeyword{infixl} specifies an infix operator that is
82 nested to the \emph{left}: in iterated applications the more complex
83 expression appears on the left-hand side: \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C}
84 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 render \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} illegal, but demand explicit
89 parentheses to indicate 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 glyphs. Several standards of extended character sets have been
101 proposed over decades, but none has become universally available so
102 far. Isabelle supports a generic notion of \bfindex{symbols} as the
103 smallest entities of source text, without referring to internal
104 encodings. There are three kinds of such ``generalized
109 \item 7-bit ASCII characters
111 \item named symbols: \verb,\,\verb,<,$ident$\verb,>,
113 \item named control symbols: \verb,\,\verb,<^,$ident$\verb,>,
117 Here $ident$ may be any identifier according to the usual Isabelle
118 conventions. This results in an infinite store of symbols, whose
119 interpretation is left to further front-end tools. For example,
120 both the user-interface of Proof~General + X-Symbol and the Isabelle
121 document processor (see \S\ref{sec:document-preparation}) display
122 the \verb,\,\verb,<forall>, symbol really as \isa{{\isasymforall}}.
124 A list of standard Isabelle symbols is given in
125 \cite[appendix~A]{isabelle-sys}. Users may introduce their own
126 interpretation of further symbols by configuring the appropriate
127 front-end tool accordingly, e.g.\ by defining certain {\LaTeX}
128 macros (see also \S\ref{sec:doc-prep-symbols}). There are also a
129 few predefined control symbols, such as \verb,\,\verb,<^sub>, and
130 \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent
131 (printable) symbol, respectively. For example, \verb,A\<^sup>\<star>, is
132 output as \isa{A\isactrlsup {\isasymstar}}.
134 \medskip The following version of our \isa{xor} definition uses a
135 standard Isabelle symbol to achieve typographically more pleasing
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 a named entity \verb,\,\verb,<oplus>, by hand; the display
150 will be 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. Now 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 above merely serves for syntactic purposes,
175 and is not checked for consistency with the real constant.
177 \medskip We may now write \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} or \isa{A\ {\isasymoplus}\ B} in
178 input, while output uses the nicer syntax of $xsymbols$, provided
179 that print mode is active. Such an arrangement is particularly
180 useful for interactive development, where users may type plain ASCII
181 text, but gain improved visual feedback from the system.
184 Alternative syntax declarations are apt to result in varying
185 occurrences of concrete syntax in the input sources. Isabelle
186 provides no systematic way to convert alternative syntax expressions
187 back and forth; print modes only affect situations where formal
188 entities are pretty printed by the Isabelle process (e.g.\ output of
189 terms and types), but not the original theory text.
192 \medskip The following variant makes the alternative \isa{{\isasymoplus}}
193 notation only available for output. Thus we may enforce input
194 sources to refer to plain ASCII only, but effectively disable
195 cut-and-paste from output at the same time.%
198 \isacommand{syntax}\ {\isacharparenleft}xsymbols\ \isakeyword{output}{\isacharparenright}\isanewline
199 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
201 \isamarkupsubsection{Prefix Annotations%
205 \begin{isamarkuptext}%
206 Prefix syntax annotations\index{prefix annotation} are just another
207 degenerate form of mixfixes \cite{isabelle-ref}, without any
208 template arguments or priorities --- just some bits of literal
209 syntax. The following example illustrates this idea idea by
210 associating common symbols with the constructors of a datatype.%
213 \isacommand{datatype}\ currency\ {\isacharequal}\isanewline
214 \ \ \ \ Euro\ nat\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymeuro}{\isachardoublequote}{\isacharparenright}\isanewline
215 \ \ {\isacharbar}\ Pounds\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isasympounds}{\isachardoublequote}{\isacharparenright}\isanewline
216 \ \ {\isacharbar}\ Yen\ nat\ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymyen}{\isachardoublequote}{\isacharparenright}\isanewline
217 \ \ {\isacharbar}\ Dollar\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isachardollar}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
219 \begin{isamarkuptext}%
220 \noindent Here the mixfix annotations on the rightmost column happen
221 to consist of a single Isabelle symbol each: \verb,\,\verb,<euro>,,
222 \verb,\,\verb,<pounds>,, \verb,\,\verb,<yen>,, and \verb,$,. Recall
223 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
224 printed as \isa{{\isasymeuro}\ {\isadigit{1}}{\isadigit{0}}}; only the head of the application is
225 subject to our concrete syntax. This simple form already achieves
226 conformance with notational standards of the European Commission.
228 Prefix syntax also works for plain \isakeyword{consts} or
229 \isakeyword{constdefs}, of course.%
233 \isamarkupsubsection{Syntax Translations \label{sec:syntax-translations}%
237 \begin{isamarkuptext}%
238 Mixfix syntax annotations work well in those situations where
239 particular constant application forms need to be decorated by
240 concrete syntax; just reconsider \isa{xor\ A\ B} versus \isa{A\ {\isasymoplus}\ B} covered before. Occasionally the relationship between some
241 piece of notation and its internal form is slightly more involved.
242 Here the concept of \bfindex{syntax translations} enters the scene.
244 Using the raw \isakeyword{syntax}\index{syntax (command)} command we
245 may introduce uninterpreted notational elements, while
246 \commdx{translations} relates input forms with more complex logical
247 expressions. This essentially provides a simple mechanism for
248 syntactic macros; even heavier transformations may be written in ML
251 \medskip A typical example of syntax translations is to decorate
252 relational expressions (i.e.\ set-membership of tuples) with
253 handsome symbolic notation, such as \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} versus
254 \isa{x\ {\isasymapprox}\ y}.%
257 \isacommand{consts}\isanewline
258 \ \ sim\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set{\isachardoublequote}\isanewline
261 \isacommand{syntax}\isanewline
262 \ \ {\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
264 \isacommand{translations}\isanewline
265 \ \ {\isachardoublequote}x\ {\isasymapprox}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim{\isachardoublequote}\isamarkupfalse%
267 \begin{isamarkuptext}%
268 \noindent Here the name of the dummy constant \isa{{\isacharunderscore}sim} does
269 not really matter, as long as it is not used elsewhere. Prefixing
270 an underscore is a common convention. The \isakeyword{translations}
271 declaration already uses concrete syntax on the left-hand side;
272 internally we relate a raw application \isa{{\isacharunderscore}sim\ x\ y} with
273 \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim}.
275 \medskip Another common application of syntax translations is to
276 provide variant versions of fundamental relational expressions, such
277 as \isa{{\isasymnoteq}} for negated equalities. The following declaration
278 stems from Isabelle/HOL itself:%
281 \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
283 \isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}{\isasymignore}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
285 \begin{isamarkuptext}%
286 \noindent Normally one would introduce derived concepts like this
287 within the logic, using \isakeyword{consts} + \isakeyword{defs}
288 instead of \isakeyword{syntax} + \isakeyword{translations}. The
289 present formulation has the virtue that expressions are immediately
290 replaced by the ``definition'' upon parsing; the effect is reversed
293 Simulating definitions via translations is adequate for very basic
294 principles, where a new representation is a trivial variation on an
295 existing one. On the other hand, syntax translations do not scale
296 up well to large hierarchies of concepts built on each other.%
300 \isamarkupsection{Document Preparation \label{sec:document-preparation}%
304 \begin{isamarkuptext}%
305 Isabelle/Isar is centered around the concept of \bfindex{formal
306 proof documents}\index{documents|bold}. The ultimate result of a
307 formal development effort is meant to be a human-readable record,
308 presented as browsable PDF file or printed on paper. The overall
309 document structure follows traditional mathematical articles, with
310 sections, intermediate explanations, definitions, theorems and
313 The Isar proof language \cite{Wenzel-PhD}, which is not covered in
314 this book, admits to write formal proof texts that are acceptable
315 both to the machine and human readers at the same time. Thus
316 marginal comments and explanations may be kept at a minimum. Even
317 without proper coverage of human-readable proofs, Isabelle document
318 preparation is very useful to produce formally derived texts.
319 Unstructured proof scripts given here may be just ignored by
320 readers, or intentionally suppressed from the text by the writer
321 (see also \S\ref{sec:doc-prep-suppress}).
323 \medskip The Isabelle document preparation system essentially acts
324 as a front-end to {\LaTeX}. After checking specifications and
325 proofs formally, the theory sources are turned into typesetting
326 instructions in a schematic manner. This enables users to write
327 authentic reports on theory developments with little effort, where
328 most consistency checks are handled by the system.%
332 \isamarkupsubsection{Isabelle Sessions%
336 \begin{isamarkuptext}%
337 In contrast to the highly interactive mode of Isabelle/Isar theory
338 development, the document preparation stage essentially works in
339 batch-mode. An Isabelle \bfindex{session} consists of a collection
340 of theory source files that contribute to an output document
341 eventually. Each session is derived from a single parent, usually
342 an object-logic image like \texttt{HOL}. This results in an overall
343 tree structure, which is reflected by the output location in the
344 file system (usually rooted at \verb,~/isabelle/browser_info,).
346 \medskip The easiest way to manage Isabelle sessions is via
347 \texttt{isatool mkdir} (generates an initial source setup) and
348 \texttt{isatool make} (runs a session controlled by
349 \texttt{IsaMakefile}). For example, a new session
350 \texttt{MySession} derived from \texttt{HOL} may be produced as
354 isatool mkdir HOL MySession
358 The \texttt{isatool make} job tells about the file-system location
359 of the ultimate results. The above dry run should be able to
360 produce some \texttt{document.pdf} of a single page (with dummy
361 title, empty table of contents etc.). Any failure at that stage
362 usually indicates technical problems of the {\LaTeX}
363 installation.\footnote{Especially make sure that \texttt{pdflatex}
364 is present; if all fails one may fall back on DVI output by changing
365 \texttt{usedir} options in \texttt{IsaMakefile}
366 \cite{isabelle-sys}.}
368 \medskip The detailed arrangement of the session sources is as
373 \item Directory \texttt{MySession} holds the required theory files
374 $T@1$\texttt{.thy}, \dots, $T@n$\texttt{.thy}.
376 \item File \texttt{MySession/ROOT.ML} holds appropriate ML commands
377 for loading all wanted theories, usually just
378 ``\texttt{use_thy"$T@i$";}'' for any $T@i$ in leaf position of the
381 \item Directory \texttt{MySession/document} contains everything
382 required for the {\LaTeX} stage; only \texttt{root.tex} needs to be
385 The latter file holds appropriate {\LaTeX} code to commence a
386 document (\verb,\documentclass, etc.), and to include the generated
387 files $T@i$\texttt{.tex} for each theory. The generated
388 \texttt{session.tex} will contain {\LaTeX} commands to include all
389 generated files in topologically sorted order, so
390 \verb,\input{session}, in \texttt{root.tex} does the job in most
393 \item \texttt{IsaMakefile} holds appropriate dependencies and
394 invocations of Isabelle tools to control the batch job. In fact,
395 several sessions may be controlled by the same \texttt{IsaMakefile}.
396 See also \cite{isabelle-sys} for further details, especially on
397 \texttt{isatool usedir} and \texttt{isatool make}.
401 With everything put in its proper place, \texttt{isatool make}
402 should be sufficient to process the Isabelle session completely,
403 with the generated document appearing in its proper place.
405 \medskip One may now start to populate the directory
406 \texttt{MySession}, and the file \texttt{MySession/ROOT.ML}
407 accordingly. \texttt{MySession/document/root.tex} should also be
408 adapted at some point; the default version is mostly
409 self-explanatory. Note that \verb,\isabellestyle, enables
410 fine-tuning of the general appearance of characters and mathematical
411 symbols (see also \S\ref{sec:doc-prep-symbols}).
413 Especially observe inclusion of the {\LaTeX} packages
414 \texttt{isabelle} (mandatory), and \texttt{isabellesym} (required
415 for mathematical symbols), and the final \texttt{pdfsetup} (provides
416 handsome defaults for \texttt{hyperref}, including URL markup).
417 Further packages may be required in particular applications, e.g.\
418 for unusual Isabelle symbols.
420 \medskip Additional files for the {\LaTeX} stage may be included in
421 the directory \texttt{MySession/document}, too, such as {\TeX}
422 sources or graphics). In particular, adding \texttt{root.bib} here
423 (with that specific name) causes an automatic run of \texttt{bibtex}
424 to process a bibliographic database; see also \texttt{isatool
425 document} covered in \cite{isabelle-sys}.
427 \medskip Any failure of the document preparation phase in an
428 Isabelle batch session leaves the generated sources in their target
429 location (as pointed out by the accompanied error message). This
430 enables users to trace {\LaTeX} at the file positions of the
435 \isamarkupsubsection{Structure Markup%
439 \begin{isamarkuptext}%
440 The large-scale structure of Isabelle documents follows existing
441 {\LaTeX} conventions, with chapters, sections, subsubsections etc.
442 The Isar language includes separate \bfindex{markup commands}, which
443 do not affect the formal meaning of a theory (or proof), but result
444 in corresponding {\LaTeX} elements.
446 There are separate markup commands depending on the textual context:
447 in header position (just before \isakeyword{theory}), within the
448 theory body, or within a proof. The header needs to be treated
449 specially here, since ordinary theory and proof commands may only
450 occur \emph{after} the initial \isakeyword{theory} specification.
454 \begin{tabular}{llll}
455 header & theory & proof & default meaning \\\hline
456 & \commdx{chapter} & & \verb,\chapter, \\
457 \commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\
458 & \commdx{subsection} & \commdx{subsect} & \verb,\subsection, \\
459 & \commdx{subsubsection} & \commdx{subsubsect} & \verb,\subsubsection, \\
464 From the Isabelle perspective, each markup command takes a single
465 $text$ argument (delimited by \verb,",\dots\verb,", or
466 \verb,{,\verb,*,~\dots~\verb,*,\verb,},). After stripping any
467 surrounding white space, the argument is passed to a {\LaTeX} macro
468 \verb,\isamarkupXYZ, for any command \isakeyword{XYZ}. These macros
469 are defined in \verb,isabelle.sty, according to the meaning given in
470 the rightmost column above.
472 \medskip The following source fragment illustrates structure markup
473 of a theory. Note that {\LaTeX} labels may be included inside of
474 section headings as well.
477 header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
479 theory Foo_Bar = Main:
481 subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
489 subsection {\ttlbrace}* Derived rules *{\ttrbrace}
494 subsection {\ttlbrace}* Main theorem {\ttback}label{\ttlbrace}sec:main-theorem{\ttrbrace} *{\ttrbrace}
501 Users may occasionally want to change the meaning of markup
502 commands, say via \verb,\renewcommand, in \texttt{root.tex};
503 \verb,\isamarkupheader, is a good candidate for some tuning, e.g.\
504 moving it up in the hierarchy to become \verb,\chapter,.
507 \renewcommand{\isamarkupheader}[1]{\chapter{#1}}
510 \noindent Certainly, this requires to change the default
511 \verb,\documentclass{article}, in \texttt{root.tex} to something
512 that supports the notion of chapters in the first place, e.g.\
513 \verb,\documentclass{report},.
515 \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to
516 hold the name of the current theory context. This is particularly
517 useful for document headings:
520 \renewcommand{\isamarkupheader}[1]
521 {\chapter{#1}\markright{THEORY~\isabellecontext}}
524 \noindent Make sure to include something like
525 \verb,\pagestyle{headings}, in \texttt{root.tex}; the document
526 should have more than 2 pages to show the effect.%
530 \isamarkupsubsection{Formal Comments and Antiquotations%
534 \begin{isamarkuptext}%
535 Isabelle source comments, which are of the form
536 \verb,(,\verb,*,~\dots~\verb,*,\verb,),, essentially act like white
537 space and do not really contribute to the content. They mainly
538 serve technical purposes to mark certain oddities in the raw input
539 text. In contrast, \bfindex{formal comments} are portions of text
540 that are associated with formal Isabelle/Isar commands
541 (\bfindex{marginal comments}), or as standalone paragraphs within a
542 theory or proof context (\bfindex{text blocks}).
544 \medskip Marginal comments are part of each command's concrete
545 syntax \cite{isabelle-ref}; the common form is ``\verb,--,~$text$''
546 where $text$ is delimited by \verb,",\dots\verb,", or
547 \verb,{,\verb,*,~\dots~\verb,*,\verb,}, as before. Multiple
548 marginal comments may be given at the same time. Here is a simple
552 \isacommand{lemma}\ {\isachardoublequote}A\ {\isacharminus}{\isacharminus}{\isachargreater}\ A{\isachardoublequote}\isanewline
554 \isamarkupcmt{a triviality of propositional logic%
558 \isamarkupcmt{(should not really bother)%
562 \isacommand{by}\ {\isacharparenleft}rule\ impI{\isacharparenright}\ %
563 \isamarkupcmt{implicit assumption step involved here%
567 \begin{isamarkuptext}%
568 \noindent The above output has been produced as follows:
572 -- "a triviality of propositional logic"
573 -- "(should not really bother)"
574 by (rule impI) -- "implicit assumption step involved here"
577 From the {\LaTeX} viewpoint, ``\verb,--,'' acts like a markup
578 command, associated with the macro \verb,\isamarkupcmt, (taking a
581 \medskip Text blocks are introduced by the commands \bfindex{text}
582 and \bfindex{txt}, for theory and proof contexts, respectively.
583 Each takes again a single $text$ argument, which is interpreted as a
584 free-form paragraph in {\LaTeX} (surrounded by some additional
585 vertical space). This behavior may be changed by redefining the
586 {\LaTeX} environments of \verb,isamarkuptext, or
587 \verb,isamarkuptxt,, respectively (via \verb,\renewenvironment,) The
588 text style of the body is determined by \verb,\isastyletext, and
589 \verb,\isastyletxt,; the default setup uses a smaller font within
592 \medskip The $text$ part of each of the various markup commands
593 considered so far essentially inserts \emph{quoted material} into a
594 formal text, mainly for instruction of the reader. An
595 \bfindex{antiquotation} is again a formal object embedded into such
596 an informal portion. The interpretation of antiquotations is
597 limited to some well-formedness checks, with the result being pretty
598 printed to the resulting document. So quoted text blocks together
599 with antiquotations provide very handsome means to reference formal
600 entities with good confidence in getting the technical details right
601 (especially syntax and types).
603 The general syntax of antiquotations is as follows:
604 \texttt{{\at}{\ttlbrace}$name$ $arguments${\ttrbrace}}, or
605 \texttt{{\at}{\ttlbrace}$name$ [$options$] $arguments${\ttrbrace}}
606 for a comma-separated list of options consisting of a $name$ or
607 \texttt{$name$=$value$}. The syntax of $arguments$ depends on the
608 kind of antiquotation, it generally follows the same conventions for
609 types, terms, or theorems as in the formal part of a theory.
611 \medskip Here is an example of the quotation-antiquotation
612 technique: \isa{{\isasymlambda}x\ y{\isachardot}\ x} is a well-typed term.
614 \medskip\noindent The above output has been produced as follows:
617 Here is an example of the quotation-antiquotation technique:
618 {\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term.
622 From the notational change of the ASCII character \verb,%, to the
623 symbol \isa{{\isasymlambda}} we see that the term really got printed by the
624 system (after parsing and type-checking) --- document preparation
625 enables symbolic output by default.
627 \medskip The next example includes an option to modify the
628 \verb,show_types, flag of Isabelle:
629 \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
630 general typings in the present (theory) context. Note that term
631 fragments may acquire different typings due to constraints imposed
632 by previous text (say within a proof), e.g.\ due to the main goal
633 statement given beforehand.
635 \medskip Several further kinds of antiquotations (and options) are
636 available \cite{isabelle-sys}. Here are a few commonly used
642 \texttt{\at}\verb,{typ,~$\tau$\verb,}, & print type $\tau$ \\
643 \texttt{\at}\verb,{term,~$t$\verb,}, & print term $t$ \\
644 \texttt{\at}\verb,{prop,~$\phi$\verb,}, & print proposition $\phi$ \\
645 \texttt{\at}\verb,{prop [display],~$\phi$\verb,}, & print large proposition $\phi$ (with linebreaks) \\
646 \texttt{\at}\verb,{prop [source],~$\phi$\verb,}, & check proposition $\phi$, print its input \\
647 \texttt{\at}\verb,{thm,~$a$\verb,}, & print fact $a$ \\
648 \texttt{\at}\verb,{thm,~$a$~\verb,[no_vars]}, & print fact $a$, fixing schematic variables \\
649 \texttt{\at}\verb,{thm [source],~$a$\verb,}, & check validity of fact $a$, print its name \\
650 \texttt{\at}\verb,{text,~$s$\verb,}, & print uninterpreted text $s$ \\
655 Note that \attrdx{no_vars} given above is \emph{not} an
656 antiquotation option, but an attribute of the theorem argument given
657 here. This might be useful with a diagnostic command like
658 \isakeyword{thm}, too.
660 \medskip The \texttt{\at}\verb,{text, $s$\verb,}, antiquotation is
661 particularly interesting. Embedding uninterpreted text within an
662 informal body might appear useless at first sight. Here the key
663 virtue is that the string $s$ is processed as Isabelle output,
664 interpreting Isabelle symbols appropriately.
666 For example, \texttt{\at}\verb,{text "\<forall>\<exists>"}, produces \isa{{\isasymforall}{\isasymexists}}, according to the standard interpretation of these symbol
667 (cf.\ \S\ref{sec:doc-prep-symbols}). Thus we achieve consistent
668 mathematical notation in both the formal and informal parts of the
669 document very easily. Manual {\LaTeX} code would leave more control
670 over the typesetting, but is also slightly more tedious.%
674 \isamarkupsubsection{Interpretation of Symbols \label{sec:doc-prep-symbols}%
678 \begin{isamarkuptext}%
679 As has been pointed out before (\S\ref{sec:syntax-symbols}),
680 Isabelle symbols are the smallest syntactic entities --- a
681 straightforward generalization of ASCII characters. While Isabelle
682 does not impose any interpretation of the infinite collection of
683 named symbols, {\LaTeX} documents show canonical glyphs for certain
684 standard symbols \cite[appendix~A]{isabelle-sys}.
686 The {\LaTeX} code produced from Isabelle text follows a relatively
687 simple scheme. Users may wish to tune the final appearance by
688 redefining certain macros, say in \texttt{root.tex} of the document.
692 \item 7-bit ASCII characters: letters \texttt{A\dots Z} and
693 \texttt{a\dots z} are output verbatim, digits are passed as an
694 argument to the \verb,\isadigit, macro, other characters are
695 replaced by specifically named macros of the form
698 \item Named symbols: \verb,\,\verb,<,$XYZ$\verb,>, become
699 \verb,{\isasym,$XYZ$\verb,}, each (note the additional braces).
701 \item Named control symbols: \verb,{\isasym,$XYZ$\verb,}, become
702 \verb,\isactrl,$XYZ$ each; subsequent symbols may act as arguments
703 if the corresponding macro is defined accordingly.
707 Users may occasionally wish to give new {\LaTeX} interpretations of
708 named symbols; this merely requires an appropriate definition of
709 \verb,\,\verb,<,$XYZ$\verb,>, (see \texttt{isabelle.sty} for working
710 examples). Control symbols are slightly more difficult to get
713 \medskip The \verb,\isabellestyle, macro provides a high-level
714 interface to tune the general appearance of individual symbols. For
715 example, \verb,\isabellestyle{it}, uses the italics text style to
716 mimic the general appearance of the {\LaTeX} math mode; double
717 quotes are not printed at all. The resulting quality of
718 typesetting is quite good, so this should usually be the default
719 style for real production work that gets distributed to a broader
724 \isamarkupsubsection{Suppressing Output \label{sec:doc-prep-suppress}%
728 \begin{isamarkuptext}%
729 By default, Isabelle's document system generates a {\LaTeX} source
730 file for each theory that happens to get loaded while running the
731 session. The generated \texttt{session.tex} will include all of
732 these in order of appearance, which in turn gets included by the
733 standard \texttt{root.tex}. Certainly one may change the order or
734 suppress unwanted theories by ignoring \texttt{session.tex} and
735 include individual files in \texttt{root.tex} by hand. On the other
736 hand, such an arrangement requires additional maintenance chores
737 whenever the collection of theories changes.
739 Alternatively, one may tune the theory loading process in
740 \texttt{ROOT.ML} itself: traversal of the theory dependency graph
741 may be fine-tuned by adding \verb,use_thy, invocations, although
742 topological sorting still has to be observed. Moreover, the ML
743 operator \verb,no_document, temporarily disables document generation
744 while executing a theory loader command; its usage is like this:
747 no_document use_thy "T";
750 \medskip Theory output may also be suppressed in smaller portions.
751 For example, research articles, or slides usually do not include the
752 formal content in full. In order to delimit \bfindex{ignored
753 material} special source comments
754 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
755 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), may be included in the
756 text. Only the document preparation system is affected, the formal
757 checking the theory is performed unchanged.
759 In the following example we suppress the slightly formalistic
760 \isakeyword{theory} + \isakeyword{end} surroundings a theory.
765 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
766 \texttt{theory T = Main:} \\
767 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
769 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
771 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
776 Text may be suppressed in a fine-grained manner. We may even drop
777 vital parts of a formal proof, pretending that things have been
778 simpler than in reality. For example, the following ``fully
779 automatic'' proof is actually a fake:%
782 \isacommand{lemma}\ {\isachardoublequote}x\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isacharless}\ x\ {\isacharasterisk}\ x{\isachardoublequote}\isanewline
784 \isacommand{by}\ {\isacharparenleft}auto{\isacharparenright}\isamarkupfalse%
786 \begin{isamarkuptext}%
787 \noindent Here the real source of the proof has been as follows:
790 by (auto(*<*)simp add: int_less_le(*>*))
794 \medskip Ignoring portions of printed text does demand some care by
795 the writer. First of all, the writer is responsible not to
796 obfuscate the underlying formal development in an unduly manner. It
797 is fairly easy to invalidate the remaining visible text, e.g.\ by
798 referencing questionable formal items (strange definitions,
799 arbitrary axioms etc.) that have been hidden from sight beforehand.
801 Authentic reports of formal theories, say as part of a library,
802 usually should refrain from suppressing parts of the text at all.
803 Other users may need the full information for their own derivative
804 work. If a particular formalization appears inadequate for general
805 public coverage, it is often more appropriate to think of a better
806 way in the first place.
808 \medskip Some technical subtleties of the
809 \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),
810 elements need to be kept in mind, too --- the system performs little
811 sanity checks here. Arguments of markup commands and formal
812 comments must not be hidden, otherwise presentation fails. Open and
813 close parentheses need to be inserted carefully; it is fairly easy
814 to hide the wrong parts, especially after rearranging the sources.%
821 %%% TeX-master: "root"