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