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