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 Here is the canonical arrangement of sources of a session
347 called \texttt{MySession}:
351 \item Directory \texttt{MySession} holds the required theory files
352 $T@1$\texttt{.thy}, \dots, $T@n$\texttt{.thy}.
354 \item File \texttt{MySession/ROOT.ML} holds appropriate ML commands
355 for loading all wanted theories, usually just
356 ``\texttt{use_thy"$T@i$";}'' for any $T@i$ in leaf position of the
359 \item Directory \texttt{MySession/document} contains everything
360 required for the {\LaTeX} stage; only \texttt{root.tex} needs to be
363 The latter file holds appropriate {\LaTeX} code to commence a
364 document (\verb,\documentclass, etc.), and to include the generated
365 files $T@i$\texttt{.tex} for each theory. The generated
366 \texttt{session.tex} will contain {\LaTeX} commands to include all
367 generated files in topologically sorted order, so
368 \verb,\input{session}, in \texttt{root.tex} does the job in most
371 \item \texttt{IsaMakefile} holds appropriate dependencies and
372 invocations of Isabelle tools to control the batch job. In fact,
373 several sessions may be controlled by the same \texttt{IsaMakefile}.
374 See also \cite{isabelle-sys} for further details, especially on
375 \texttt{isatool usedir} and \texttt{isatool make}.
379 With everything put in its proper place, \texttt{isatool make}
380 should be sufficient to process the Isabelle session completely,
381 with the generated document appearing in its proper place.
383 \medskip In reality, users may want to have \texttt{isatool mkdir}
384 generate an initial working setup without further ado. For example,
385 a new session \texttt{MySession} derived from \texttt{HOL} may be
389 isatool mkdir HOL MySession
393 This processes the session with sensible default options, including
394 verbose mode to tell the user where the ultimate results will
395 appear. The above dry run should already be able to produce a
396 single page of output (with a dummy title, empty table of contents
397 etc.). Any failure at that stage is likely to indicate technical
398 problems with the user's {\LaTeX} installation.\footnote{Especially
399 make sure that \texttt{pdflatex} is present; if all fails one may
400 fall back on DVI output by changing \texttt{usedir} options in
401 \texttt{IsaMakefile} \cite{isabelle-sys}.}
403 \medskip One may now start to populate the directory
404 \texttt{MySession}, and the file \texttt{MySession/ROOT.ML}
405 accordingly. \texttt{MySession/document/root.tex} should also be
406 adapted at some point; the default version is mostly
407 self-explanatory. Note that \verb,\isabellestyle, enables
408 fine-tuning of the general appearance of characters and mathematical
409 symbols (see also \S\ref{sec:doc-prep-symbols}).
411 Especially observe inclusion of the {\LaTeX} packages
412 \texttt{isabelle} (mandatory), and \texttt{isabellesym} (required
413 for mathematical symbols), and the final \texttt{pdfsetup} (provides
414 handsome defaults for \texttt{hyperref}, including URL markup).
415 Further packages may be required in particular applications, e.g.\
416 for unusual Isabelle symbols.
418 \medskip Additional files for the {\LaTeX} stage may be included in
419 the directory \texttt{MySession/document}, too, such as {\TeX}
420 sources or graphics). In particular, adding \texttt{root.bib} here
421 (with that specific name) causes an automatic run of \texttt{bibtex}
422 to process a bibliographic database; see also \texttt{isatool
423 document} covered in \cite{isabelle-sys}.
425 \medskip Any failure of the document preparation phase in an
426 Isabelle batch session leaves the generated sources in their target
427 location (as pointed out by the accompanied error message). This
428 enables users to trace {\LaTeX} at the file positions of the
433 \isamarkupsubsection{Structure Markup%
437 \begin{isamarkuptext}%
438 The large-scale structure of Isabelle documents follows existing
439 {\LaTeX} conventions, with chapters, sections, subsubsections etc.
440 The Isar language includes separate \bfindex{markup commands}, which
441 do not affect the formal meaning of a theory (or proof), but result
442 in corresponding {\LaTeX} elements.
444 There are separate markup commands depending on the textual context:
445 in header position (just before \isakeyword{theory}), within the
446 theory body, or within a proof. The header needs to be treated
447 specially here, since ordinary theory and proof commands may only
448 occur \emph{after} the initial \isakeyword{theory} specification.
452 \begin{tabular}{llll}
453 header & theory & proof & default meaning \\\hline
454 & \commdx{chapter} & & \verb,\chapter, \\
455 \commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\
456 & \commdx{subsection} & \commdx{subsect} & \verb,\subsection, \\
457 & \commdx{subsubsection} & \commdx{subsubsect} & \verb,\subsubsection, \\
462 From the Isabelle perspective, each markup command takes a single
463 $text$ argument (delimited by \verb,",\dots\verb,", or
464 \verb,{,\verb,*,~\dots~\verb,*,\verb,},). After stripping any
465 surrounding white space, the argument is passed to a {\LaTeX} macro
466 \verb,\isamarkupXYZ, for any command \isakeyword{XYZ}. These macros
467 are defined in \verb,isabelle.sty, according to the meaning given in
468 the rightmost column above.
470 \medskip The following source fragment illustrates structure markup
471 of a theory. Note that {\LaTeX} labels may be included inside of
472 section headings as well.
475 header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
477 theory Foo_Bar = Main:
479 subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
487 subsection {\ttlbrace}* Derived rules *{\ttrbrace}
492 subsection {\ttlbrace}* Main theorem {\ttback}label{\ttlbrace}sec:main-theorem{\ttrbrace} *{\ttrbrace}
499 Users may occasionally want to change the meaning of markup
500 commands, say via \verb,\renewcommand, in \texttt{root.tex};
501 \verb,\isamarkupheader, is a good candidate for some tuning, e.g.\
502 moving it up in the hierarchy to become \verb,\chapter,.
505 \renewcommand{\isamarkupheader}[1]{\chapter{#1}}
508 \noindent Certainly, this requires to change the default
509 \verb,\documentclass{article}, in \texttt{root.tex} to something
510 that supports the notion of chapters in the first place, e.g.\
511 \verb,\documentclass{report},.
513 \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to
514 hold the name of the current theory context. This is particularly
515 useful for document headings:
518 \renewcommand{\isamarkupheader}[1]
519 {\chapter{#1}\markright{THEORY~\isabellecontext}}
522 \noindent Make sure to include something like
523 \verb,\pagestyle{headings}, in \texttt{root.tex}; the document
524 should have more than 2 pages to show the effect.%
528 \isamarkupsubsection{Formal Comments and Antiquotations%
532 \begin{isamarkuptext}%
533 Isabelle source comments, which are of the form
534 \verb,(,\verb,*,~\dots~\verb,*,\verb,),, essentially act like white
535 space and do not really contribute to the content. They mainly
536 serve technical purposes to mark certain oddities in the raw input
537 text. In contrast, \bfindex{formal comments} are portions of text
538 that are associated with formal Isabelle/Isar commands
539 (\bfindex{marginal comments}), or as standalone paragraphs within a
540 theory or proof context (\bfindex{text blocks}).
542 \medskip Marginal comments are part of each command's concrete
543 syntax \cite{isabelle-ref}; the common form is ``\verb,--,~$text$''
544 where $text$ is delimited by \verb,",\dots\verb,", or
545 \verb,{,\verb,*,~\dots~\verb,*,\verb,}, as before. Multiple
546 marginal comments may be given at the same time. Here is a simple
550 \isacommand{lemma}\ {\isachardoublequote}A\ {\isacharminus}{\isacharminus}{\isachargreater}\ A{\isachardoublequote}\isanewline
552 \isamarkupcmt{a triviality of propositional logic%
556 \isamarkupcmt{(should not really bother)%
560 \isacommand{by}\ {\isacharparenleft}rule\ impI{\isacharparenright}\ %
561 \isamarkupcmt{implicit assumption step involved here%
565 \begin{isamarkuptext}%
566 \noindent The above output has been produced as follows:
570 -- "a triviality of propositional logic"
571 -- "(should not really bother)"
572 by (rule impI) -- "implicit assumption step involved here"
575 From the {\LaTeX} viewpoint, ``\verb,--,'' acts like a markup
576 command, associated with the macro \verb,\isamarkupcmt, (taking a
579 \medskip Text blocks are introduced by the commands \bfindex{text}
580 and \bfindex{txt}, for theory and proof contexts, respectively.
581 Each takes again a single $text$ argument, which is interpreted as a
582 free-form paragraph in {\LaTeX} (surrounded by some additional
583 vertical space). This behavior may be changed by redefining the
584 {\LaTeX} environments of \verb,isamarkuptext, or
585 \verb,isamarkuptxt,, respectively (via \verb,\renewenvironment,) The
586 text style of the body is determined by \verb,\isastyletext, and
587 \verb,\isastyletxt,; the default setup uses a smaller font within
590 \medskip The $text$ part of each of the various markup commands
591 considered so far essentially inserts \emph{quoted material} into a
592 formal text, mainly for instruction of the reader. An
593 \bfindex{antiquotation} is again a formal object embedded into such
594 an informal portion. The interpretation of antiquotations is
595 limited to some well-formedness checks, with the result being pretty
596 printed to the resulting document. So quoted text blocks together
597 with antiquotations provide very handsome means to reference formal
598 entities with good confidence in getting the technical details right
599 (especially syntax and types).
601 The general syntax 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 options consisting of a $name$ or
605 \texttt{$name$=$value$}. The syntax of $arguments$ depends on the
606 kind of antiquotation, it generally follows the same conventions for
607 types, terms, or theorems as in the formal part of a theory.
609 \medskip Here is an example of the quotation-antiquotation
610 technique: \isa{{\isasymlambda}x\ y{\isachardot}\ x} is a well-typed term.
612 \medskip\noindent The above output has been produced as follows:
615 Here is an example of the quotation-antiquotation technique:
616 {\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term.
620 From the notational change of the ASCII character \verb,%, to the
621 symbol \isa{{\isasymlambda}} we see that the term really got printed by the
622 system (after parsing and type-checking) --- document preparation
623 enables symbolic output by default.
625 \medskip The next example includes an option to modify the
626 \verb,show_types, flag of Isabelle:
627 \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
628 general typings in the present (theory) context. Note that term
629 fragments may acquire different typings due to constraints imposed
630 by previous text (say within a proof), e.g.\ due to the main goal
631 statement given beforehand.
633 \medskip Several further kinds of antiquotations (and options) are
634 available \cite{isabelle-sys}. Here are a few commonly used
640 \texttt{\at}\verb,{typ,~$\tau$\verb,}, & print type $\tau$ \\
641 \texttt{\at}\verb,{term,~$t$\verb,}, & print term $t$ \\
642 \texttt{\at}\verb,{prop,~$\phi$\verb,}, & print proposition $\phi$ \\
643 \texttt{\at}\verb,{prop [display],~$\phi$\verb,}, & print large proposition $\phi$ (with linebreaks) \\
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 validity of fact $a$, print its name \\
648 \texttt{\at}\verb,{text,~$s$\verb,}, & print uninterpreted text $s$ \\
653 Note that \attrdx{no_vars} given above is \emph{not} an
654 antiquotation option, but an attribute of the theorem argument given
655 here. This might be useful with a diagnostic command like
656 \isakeyword{thm}, too.
658 \medskip The \texttt{\at}\verb,{text, $s$\verb,}, antiquotation is
659 particularly interesting. Embedding uninterpreted text within an
660 informal body might appear useless at first sight. Here the key
661 virtue is that the string $s$ is processed as Isabelle output,
662 interpreting Isabelle symbols appropriately.
664 For example, \texttt{\at}\verb,{text "\<forall>\<exists>"}, produces \isa{{\isasymforall}{\isasymexists}}, according to the standard interpretation of these symbol
665 (cf.\ \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 would leave more control
668 over the typesetting, but is also slightly more tedious.%
672 \isamarkupsubsection{Interpretation of Symbols \label{sec:doc-prep-symbols}%
676 \begin{isamarkuptext}%
677 As has been pointed out before (\S\ref{sec:syntax-symbols}),
678 Isabelle symbols are the smallest syntactic entities --- a
679 straightforward generalization of ASCII characters. While Isabelle
680 does not impose any interpretation of the infinite collection of
681 named symbols, {\LaTeX} documents show canonical glyphs for certain
682 standard symbols \cite[appendix~A]{isabelle-sys}.
684 The {\LaTeX} code produced from Isabelle text follows a relatively
685 simple scheme. Users may wish to tune the final appearance by
686 redefining certain macros, say in \texttt{root.tex} of the document.
690 \item 7-bit ASCII characters: letters \texttt{A\dots Z} and
691 \texttt{a\dots z} are output verbatim, digits are passed as an
692 argument to the \verb,\isadigit, macro, other characters are
693 replaced by specifically named macros of the form
696 \item Named symbols: \verb,\,\verb,<,$XYZ$\verb,>, become
697 \verb,{\isasym,$XYZ$\verb,}, each (note the additional braces).
699 \item Named control symbols: \verb,{\isasym,$XYZ$\verb,}, become
700 \verb,\isactrl,$XYZ$ each; subsequent symbols may act as arguments
701 if the corresponding macro is defined accordingly.
705 Users may occasionally wish to give new {\LaTeX} interpretations of
706 named symbols; this merely requires an appropriate definition of
707 \verb,\,\verb,<,$XYZ$\verb,>, (see \texttt{isabelle.sty} for working
708 examples). Control symbols are slightly more difficult to get
711 \medskip The \verb,\isabellestyle, macro provides a high-level
712 interface to tune the general appearance of individual symbols. For
713 example, \verb,\isabellestyle{it}, uses the italics text style to
714 mimic the general appearance of the {\LaTeX} math mode; double
715 quotes are not printed at all. The resulting quality of
716 typesetting is quite good, so this should usually be the default
717 style for real production work that gets distributed to a broader
722 \isamarkupsubsection{Suppressing Output \label{sec:doc-prep-suppress}%
726 \begin{isamarkuptext}%
727 By default, Isabelle's document system generates a {\LaTeX} source
728 file for each theory that happens to get loaded while running the
729 session. The generated \texttt{session.tex} will include all of
730 these in order of appearance, which in turn gets included by the
731 standard \texttt{root.tex}. Certainly one may change the order or
732 suppress unwanted theories by ignoring \texttt{session.tex} and
733 include individual files in \texttt{root.tex} by hand. On the other
734 hand, such an arrangement requires additional maintenance chores
735 whenever the collection of theories changes.
737 Alternatively, one may tune the theory loading process in
738 \texttt{ROOT.ML} itself: traversal of the theory dependency graph
739 may be fine-tuned by adding \verb,use_thy, invocations, although
740 topological sorting still has to be observed. Moreover, the ML
741 operator \verb,no_document, temporarily disables document generation
742 while executing a theory loader command; its usage is like this:
745 no_document use_thy "T";
748 \medskip Theory output may also be suppressed in smaller portions.
749 For example, research articles, or slides usually do not include the
750 formal content in full. In order to delimit \bfindex{ignored
751 material} special source comments
752 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
753 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), may be included in the
754 text. Only the document preparation system is affected, the formal
755 checking the theory is performed unchanged.
757 In the following example we suppress the slightly formalistic
758 \isakeyword{theory} + \isakeyword{end} surroundings a theory.
763 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
764 \texttt{theory T = Main:} \\
765 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
767 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
769 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
774 Text may be suppressed in a fine-grained manner. We may even drop
775 vital parts of a formal proof, pretending that things have been
776 simpler than in reality. For example, the following ``fully
777 automatic'' proof is actually a fake:%
780 \isacommand{lemma}\ {\isachardoublequote}x\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isacharless}\ x\ {\isacharasterisk}\ x{\isachardoublequote}\isanewline
782 \isacommand{by}\ {\isacharparenleft}auto{\isacharparenright}\isamarkupfalse%
784 \begin{isamarkuptext}%
785 \noindent Here the real source of the proof has been as follows:
788 by (auto(*<*)simp add: int_less_le(*>*))
792 \medskip Ignoring portions of printed text does demand some care by
793 the writer. First of all, the writer is responsible not to
794 obfuscate the underlying formal development in an unduly manner. It
795 is fairly easy to invalidate the remaining visible text, e.g.\ by
796 referencing questionable formal items (strange definitions,
797 arbitrary axioms etc.) that have been hidden from sight beforehand.
799 Authentic reports of formal theories, say as part of a library,
800 usually should refrain from suppressing parts of the text at all.
801 Other users may need the full information for their own derivative
802 work. If a particular formalization appears inadequate for general
803 public coverage, it is often more appropriate to think of a better
804 way in the first place.
806 \medskip Some technical subtleties of the
807 \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),
808 elements need to be kept in mind, too --- the system performs little
809 sanity checks here. Arguments of markup commands and formal
810 comments must not be hidden, otherwise presentation fails. Open and
811 close parentheses need to be inserted carefully; it is fairly easy
812 to hide the wrong parts, especially after rearranging the sources.%
819 %%% TeX-master: "root"