3 \def\isabellecontext{Documents}%
18 \isamarkupsection{Concrete Syntax \label{sec:concrete-syntax}%
22 \begin{isamarkuptext}%
23 The core concept of Isabelle's framework for concrete syntax is that
24 of \bfindex{mixfix annotations}. Associated with any kind of
25 constant declaration, mixfixes affect both the grammar productions
26 for the parser and output templates for the pretty printer.
28 In full generality, parser and pretty printer configuration is a
29 subtle affair~\cite{isabelle-ref}. Your syntax specifications need
30 to interact properly with the existing setup of Isabelle/Pure and
31 Isabelle/HOL\@. To avoid creating ambiguities with existing
32 elements, it is particularly important to give new syntactic
33 constructs the right precedence.
35 Below we introduce a few simple syntax declaration
36 forms that already cover many common situations fairly well.%
40 \isamarkupsubsection{Infix Annotations%
44 \begin{isamarkuptext}%
45 Syntax annotations may be included wherever constants are declared,
46 such as \isacommand{definition} and \isacommand{primrec} --- and also
47 \isacommand{datatype}, which declares constructor operations.
48 Type-constructors may be annotated as well, although this is less
49 frequently encountered in practice (the infix type \isa{{\isasymtimes}} comes
52 Infix declarations\index{infix annotations} provide a useful special
53 case of mixfixes. The following example of the exclusive-or
54 operation on boolean values illustrates typical infix declarations.%
57 \isacommand{definition}\isamarkupfalse%
58 \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
59 \isakeyword{where}\ {\isachardoublequoteopen}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequoteclose}%
60 \begin{isamarkuptext}%
61 \noindent Now \isa{xor\ A\ B} and \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} refer to the
62 same expression internally. Any curried function with at least two
63 arguments may be given infix syntax. For partial applications with
64 fewer than two operands, there is a notation using the prefix~\isa{op}. For instance, \isa{xor} without arguments is represented as
65 \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}}; together with ordinary function application, this
66 turns \isa{xor\ A} into \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ A}.
68 The keyword \isakeyword{infixl} seen above specifies an
69 infix operator that is nested to the \emph{left}: in iterated
70 applications the more complex expression appears on the left-hand
71 side, and \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} stands for \isa{{\isacharparenleft}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B{\isacharparenright}\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C}. Similarly, \isakeyword{infixr} means nesting to the
72 \emph{right}, reading \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} as \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ {\isacharparenleft}B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C{\isacharparenright}}. A \emph{non-oriented} declaration via \isakeyword{infix}
73 would render \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} illegal, but demand explicit
74 parentheses to indicate the intended grouping.
76 The string \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}} in our annotation refers to the
77 concrete syntax to represent the operator (a literal token), while
78 the number \isa{{\isadigit{6}}{\isadigit{0}}} determines the precedence of the construct:
79 the syntactic priorities of the arguments and result. Isabelle/HOL
80 already uses up many popular combinations of ASCII symbols for its
81 own use, including both \isa{{\isacharplus}} and \isa{{\isacharplus}{\isacharplus}}. Longer
82 character combinations are more likely to be still available for
83 user extensions, such as our~\isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}}.
85 Operator precedences have a range of 0--1000. Very low or high
86 priorities are reserved for the meta-logic. HOL syntax mainly uses
87 the range of 10--100: the equality infix \isa{{\isacharequal}} is centered at
88 50; logical connectives (like \isa{{\isasymor}} and \isa{{\isasymand}}) are
89 below 50; algebraic ones (like \isa{{\isacharplus}} and \isa{{\isacharasterisk}}) are
90 above 50. User syntax should strive to coexist with common HOL
91 forms, or use the mostly unused range 100--900.%
95 \isamarkupsubsection{Mathematical Symbols \label{sec:syntax-symbols}%
99 \begin{isamarkuptext}%
100 Concrete syntax based on ASCII characters has inherent limitations.
101 Mathematical notation demands a larger repertoire of glyphs.
102 Several standards of extended character sets have been proposed over
103 decades, but none has become universally available so far. Isabelle
104 has its own notion of \bfindex{symbols} as the smallest entities of
105 source text, without referring to internal encodings. There are
106 three kinds of such ``generalized characters'':
110 \item 7-bit ASCII characters
112 \item named symbols: \verb,\,\verb,<,$ident$\verb,>,
114 \item named control symbols: \verb,\,\verb,<^,$ident$\verb,>,
118 Here $ident$ is any sequence of letters.
119 This results in an infinite store of symbols, whose
120 interpretation is left to further front-end tools. For example, the
121 user-interface of Proof~General + X-Symbol and the Isabelle document
122 processor (see \S\ref{sec:document-preparation}) display the
123 \verb,\,\verb,<forall>, symbol as~\isa{{\isasymforall}}.
125 A list of standard Isabelle symbols is given in
126 \cite{isabelle-isar-ref}. You may introduce your own
127 interpretation of further symbols by configuring the appropriate
128 front-end tool accordingly, e.g.\ by defining certain {\LaTeX}
129 macros (see also \S\ref{sec:doc-prep-symbols}). There are also a
130 few predefined control symbols, such as \verb,\,\verb,<^sub>, and
131 \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent
132 printable symbol, respectively. For example, \verb,A\<^sup>\<star>, is
133 output as \isa{A\isactrlsup {\isasymstar}}.
135 A number of symbols are considered letters by the Isabelle lexer and
136 can be used as part of identifiers. These are the greek letters
137 \isa{{\isasymalpha}} (\verb+\+\verb+<alpha>+), \isa{{\isasymbeta}}
138 (\verb+\+\verb+<beta>+), etc. (excluding \isa{{\isasymlambda}}),
139 special letters like \isa{{\isasymA}} (\verb+\+\verb+<A>+) and \isa{{\isasymAA}} (\verb+\+\verb+<AA>+), and the control symbols
140 \verb+\+\verb+<^isub>+ and \verb+\+\verb+<^isup>+ for single letter
141 sub and super scripts. This means that the input
144 {\small\noindent \verb,\,\verb,<forall>\,\verb,<alpha>\<^isub>1.,~\verb,\,\verb,<alpha>\<^isub>1 = \,\verb,<Pi>\<^isup>\<A>,}
147 \noindent is recognized as the term \isa{{\isasymforall}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isachardot}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isacharequal}\ {\isasymPi}\isactrlisup {\isasymA}}
148 by Isabelle. Note that \isa{{\isasymPi}\isactrlisup {\isasymA}} is a single
149 syntactic entity, not an exponentiation.
151 Replacing our previous definition of \isa{xor} by the
152 following specifies an Isabelle symbol for the new operator:%
168 \isacommand{definition}\isamarkupfalse%
169 \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
170 \isakeyword{where}\ {\isachardoublequoteopen}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequoteclose}%
171 \begin{isamarkuptext}%
172 \noindent The X-Symbol package within Proof~General provides several
173 input methods to enter \isa{{\isasymoplus}} in the text. If all fails one may
174 just type a named entity \verb,\,\verb,<oplus>, by hand; the
175 corresponding symbol will be displayed after further input.
177 More flexible is to provide alternative syntax forms
178 through the \bfindex{print mode} concept~\cite{isabelle-ref}. By
179 convention, the mode of ``$xsymbols$'' is enabled whenever
180 Proof~General's X-Symbol mode or {\LaTeX} output is active. Now
181 consider the following hybrid declaration of \isa{xor}:%
197 \isacommand{definition}\isamarkupfalse%
198 \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
199 \isakeyword{where}\ {\isachardoublequoteopen}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequoteclose}\isanewline
201 \isacommand{notation}\isamarkupfalse%
202 \ {\isacharparenleft}xsymbols{\isacharparenright}\ xor\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}%
203 \begin{isamarkuptext}%
205 The \commdx{notation} command associates a mixfix
206 annotation with a known constant. The print mode specification,
207 here \isa{{\isacharparenleft}xsymbols{\isacharparenright}}, is optional.
209 We may now write \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} or \isa{A\ {\isasymoplus}\ B} in input, while
210 output uses the nicer syntax of $xsymbols$ whenever that print mode is
211 active. Such an arrangement is particularly useful for interactive
212 development, where users may type ASCII text and see mathematical
213 symbols displayed during proofs.%
217 \isamarkupsubsection{Prefix Annotations%
221 \begin{isamarkuptext}%
222 Prefix syntax annotations\index{prefix annotation} are another form
223 of mixfixes \cite{isabelle-ref}, without any template arguments or
224 priorities --- just some literal syntax. The following example
225 associates common symbols with the constructors of a datatype.%
228 \isacommand{datatype}\isamarkupfalse%
229 \ currency\ {\isacharequal}\isanewline
230 \ \ \ \ Euro\ nat\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isasymeuro}{\isachardoublequoteclose}{\isacharparenright}\isanewline
231 \ \ {\isacharbar}\ Pounds\ nat\ \ {\isacharparenleft}{\isachardoublequoteopen}{\isasympounds}{\isachardoublequoteclose}{\isacharparenright}\isanewline
232 \ \ {\isacharbar}\ Yen\ nat\ \ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isasymyen}{\isachardoublequoteclose}{\isacharparenright}\isanewline
233 \ \ {\isacharbar}\ Dollar\ nat\ \ {\isacharparenleft}{\isachardoublequoteopen}{\isachardollar}{\isachardoublequoteclose}{\isacharparenright}%
234 \begin{isamarkuptext}%
235 \noindent Here the mixfix annotations on the rightmost column happen
236 to consist of a single Isabelle symbol each: \verb,\,\verb,<euro>,,
237 \verb,\,\verb,<pounds>,, \verb,\,\verb,<yen>,, and \verb,$,. Recall
238 that a constructor like \isa{Euro} actually is a function \isa{nat\ {\isasymRightarrow}\ currency}. The expression \isa{Euro\ {\isadigit{1}}{\isadigit{0}}} will be
239 printed as \isa{{\isasymeuro}\ {\isadigit{1}}{\isadigit{0}}}; only the head of the application is
240 subject to our concrete syntax. This rather simple form already
241 achieves conformance with notational standards of the European
244 Prefix syntax works the same way for other commands that introduce new constants, e.g. \isakeyword{primrec}.%
248 \isamarkupsubsection{Abbreviations \label{sec:abbreviations}%
252 \begin{isamarkuptext}%
253 Mixfix syntax annotations merely decorate particular constant
254 application forms with concrete syntax, for instance replacing
255 \isa{xor\ A\ B} by \isa{A\ {\isasymoplus}\ B}. Occasionally, the relationship
256 between some piece of notation and its internal form is more
257 complicated. Here we need \emph{abbreviations}.
259 Command \commdx{abbreviation} introduces an uninterpreted notational
260 constant as an abbreviation for a complex term. Abbreviations are
261 unfolded upon parsing and re-introduced upon printing. This provides a
262 simple mechanism for syntactic macros.
264 A typical use of abbreviations is to introduce relational notation for
265 membership in a set of pairs, replacing \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} by
266 \isa{x\ {\isasymapprox}\ y}. We assume that a constant \isa{sim} of type
267 \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set} has been introduced at this point.%
270 \isacommand{abbreviation}\isamarkupfalse%
271 \ sim{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ {\isacharparenleft}\isakeyword{infix}\ {\isachardoublequoteopen}{\isasymapprox}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline
272 \isakeyword{where}\ {\isachardoublequoteopen}x\ {\isasymapprox}\ y\ \ {\isasymequiv}\ \ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim{\isachardoublequoteclose}%
273 \begin{isamarkuptext}%
274 \noindent The given meta-equality is used as a rewrite rule
275 after parsing (replacing \mbox{\isa{x\ {\isasymapprox}\ y}} by \isa{{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ sim}) and before printing (turning \isa{{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ sim} back into
276 \mbox{\isa{x\ {\isasymapprox}\ y}}). The name of the dummy constant \isa{sim{\isadigit{2}}}
277 does not matter, as long as it is unique.
279 Another common application of abbreviations is to
280 provide variant versions of fundamental relational expressions, such
281 as \isa{{\isasymnoteq}} for negated equalities. The following declaration
282 stems from Isabelle/HOL itself:%
285 \isacommand{abbreviation}\isamarkupfalse%
286 \ not{\isacharunderscore}equal\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isachartilde}{\isacharequal}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\isanewline
287 \isakeyword{where}\ {\isachardoublequoteopen}x\ {\isachartilde}{\isacharequal}{\isasymignore}\ y\ \ {\isasymequiv}\ \ {\isasymnot}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
289 \isacommand{notation}\isamarkupfalse%
290 \ {\isacharparenleft}xsymbols{\isacharparenright}\ not{\isacharunderscore}equal\ {\isacharparenleft}\isakeyword{infix}\ {\isachardoublequoteopen}{\isasymnoteq}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}%
291 \begin{isamarkuptext}%
292 \noindent The notation \isa{{\isasymnoteq}} is introduced separately to restrict it
293 to the \emph{xsymbols} mode.
295 Abbreviations are appropriate when the defined concept is a
296 simple variation on an existing one. But because of the automatic
297 folding and unfolding of abbreviations, they do not scale up well to
298 large hierarchies of concepts. Abbreviations do not replace
301 Abbreviations are a simplified form of the general concept of
302 \emph{syntax translations}; even heavier transformations may be
303 written in ML \cite{isabelle-ref}.%
307 \isamarkupsection{Document Preparation \label{sec:document-preparation}%
311 \begin{isamarkuptext}%
312 Isabelle/Isar is centered around the concept of \bfindex{formal
313 proof documents}\index{documents|bold}. The outcome of a formal
314 development effort is meant to be a human-readable record, presented
315 as browsable PDF file or printed on paper. The overall document
316 structure follows traditional mathematical articles, with sections,
317 intermediate explanations, definitions, theorems and proofs.
319 \medskip The Isabelle document preparation system essentially acts
320 as a front-end to {\LaTeX}. After checking specifications and
321 proofs formally, the theory sources are turned into typesetting
322 instructions in a schematic manner. This lets you write authentic
323 reports on theory developments with little effort: many technical
324 consistency checks are handled by the system.
326 Here is an example to illustrate the idea of Isabelle document
333 \begin{isamarkuptext}%
334 The following datatype definition of \isa{{\isacharprime}a\ bintree} models
335 binary trees with nodes being decorated by elements of type \isa{{\isacharprime}a}.%
338 \isacommand{datatype}\isamarkupfalse%
339 \ {\isacharprime}a\ bintree\ {\isacharequal}\isanewline
340 \ \ \ \ \ Leaf\ {\isacharbar}\ Branch\ {\isacharprime}a\ \ {\isachardoublequoteopen}{\isacharprime}a\ bintree{\isachardoublequoteclose}\ \ {\isachardoublequoteopen}{\isacharprime}a\ bintree{\isachardoublequoteclose}%
341 \begin{isamarkuptext}%
342 \noindent The datatype induction rule generated here is of the form
344 \ {\isasymlbrakk}P\ Leaf{\isacharsemicolon}\isanewline
345 \isaindent{\ \ }{\isasymAnd}a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isachardot}\isanewline
346 \isaindent{\ \ \ \ \ }{\isasymlbrakk}P\ bintree{\isadigit{1}}{\isacharsemicolon}\ P\ bintree{\isadigit{2}}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Branch\ a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isacharparenright}{\isasymrbrakk}\isanewline
347 \isaindent{\ }{\isasymLongrightarrow}\ P\ bintree%
354 \begin{isamarkuptext}%
355 \noindent The above document output has been produced as follows:
359 The following datatype definition of {\at}{\ttlbrace}text "'a bintree"{\ttrbrace}
360 models binary trees with nodes being decorated by elements
361 of type {\at}{\ttlbrace}typ 'a{\ttrbrace}.
364 datatype 'a bintree =
365 Leaf | Branch 'a "'a bintree" "'a bintree"
369 {\ttback}noindent The datatype induction rule generated here is
370 of the form {\at}{\ttlbrace}thm [display] bintree.induct [no_vars]{\ttrbrace}
372 \end{ttbox}\vspace{-\medskipamount}
374 \noindent Here we have augmented the theory by formal comments
375 (using \isakeyword{text} blocks), the informal parts may again refer
376 to formal entities by means of ``antiquotations'' (such as
377 \texttt{\at}\verb,{text "'a bintree"}, or
378 \texttt{\at}\verb,{typ 'a},), see also \S\ref{sec:doc-prep-text}.%
382 \isamarkupsubsection{Isabelle Sessions%
386 \begin{isamarkuptext}%
387 In contrast to the highly interactive mode of Isabelle/Isar theory
388 development, the document preparation stage essentially works in
389 batch-mode. An Isabelle \bfindex{session} consists of a collection
390 of source files that may contribute to an output document. Each
391 session is derived from a single parent, usually an object-logic
392 image like \texttt{HOL}. This results in an overall tree structure,
393 which is reflected by the output location in the file system
394 (usually rooted at \verb,~/.isabelle/browser_info,).
396 \medskip The easiest way to manage Isabelle sessions is via
397 \texttt{isabelle mkdir} (generates an initial session source setup)
398 and \texttt{isabelle make} (run sessions controlled by
399 \texttt{IsaMakefile}). For example, a new session
400 \texttt{MySession} derived from \texttt{HOL} may be produced as
404 isabelle mkdir HOL MySession
408 The \texttt{isabelle make} job also informs about the file-system
409 location of the ultimate results. The above dry run should be able
410 to produce some \texttt{document.pdf} (with dummy title, empty table
411 of contents etc.). Any failure at this stage usually indicates
412 technical problems of the {\LaTeX} installation.
414 \medskip The detailed arrangement of the session sources is as
419 \item Directory \texttt{MySession} holds the required theory files
420 $T@1$\texttt{.thy}, \dots, $T@n$\texttt{.thy}.
422 \item File \texttt{MySession/ROOT.ML} holds appropriate ML commands
423 for loading all wanted theories, usually just
424 ``\texttt{use_thy"$T@i$";}'' for any $T@i$ in leaf position of the
427 \item Directory \texttt{MySession/document} contains everything
428 required for the {\LaTeX} stage; only \texttt{root.tex} needs to be
431 The latter file holds appropriate {\LaTeX} code to commence a
432 document (\verb,\documentclass, etc.), and to include the generated
433 files $T@i$\texttt{.tex} for each theory. Isabelle will generate a
434 file \texttt{session.tex} holding {\LaTeX} commands to include all
435 generated theory output files in topologically sorted order, so
436 \verb,\input{session}, in the body of \texttt{root.tex} does the job
439 \item \texttt{IsaMakefile} holds appropriate dependencies and
440 invocations of Isabelle tools to control the batch job. In fact,
441 several sessions may be managed by the same \texttt{IsaMakefile}.
442 See the \emph{Isabelle System Manual} \cite{isabelle-sys}
443 for further details, especially on
444 \texttt{isabelle usedir} and \texttt{isabelle make}.
448 One may now start to populate the directory \texttt{MySession}, and
449 the file \texttt{MySession/ROOT.ML} accordingly. The file
450 \texttt{MySession/document/root.tex} should also be adapted at some
451 point; the default version is mostly self-explanatory. Note that
452 \verb,\isabellestyle, enables fine-tuning of the general appearance
453 of characters and mathematical symbols (see also
454 \S\ref{sec:doc-prep-symbols}).
456 Especially observe the included {\LaTeX} packages \texttt{isabelle}
457 (mandatory), \texttt{isabellesym} (required for mathematical
458 symbols), and the final \texttt{pdfsetup} (provides sane defaults
459 for \texttt{hyperref}, including URL markup). All three are
460 distributed with Isabelle. Further packages may be required in
461 particular applications, say for unusual mathematical symbols.
463 \medskip Any additional files for the {\LaTeX} stage go into the
464 \texttt{MySession/document} directory as well. In particular,
465 adding a file named \texttt{root.bib} causes an automatic run of
466 \texttt{bibtex} to process a bibliographic database; see also
467 \texttt{isabelle document} \cite{isabelle-sys}.
469 \medskip Any failure of the document preparation phase in an
470 Isabelle batch session leaves the generated sources in their target
471 location, identified by the accompanying error message. This lets
472 you trace {\LaTeX} problems with the generated files at hand.%
476 \isamarkupsubsection{Structure Markup%
480 \begin{isamarkuptext}%
481 The large-scale structure of Isabelle documents follows existing
482 {\LaTeX} conventions, with chapters, sections, subsubsections etc.
483 The Isar language includes separate \bfindex{markup commands}, which
484 do not affect the formal meaning of a theory (or proof), but result
485 in corresponding {\LaTeX} elements.
487 There are separate markup commands depending on the textual context:
488 in header position (just before \isakeyword{theory}), within the
489 theory body, or within a proof. The header needs to be treated
490 specially here, since ordinary theory and proof commands may only
491 occur \emph{after} the initial \isakeyword{theory} specification.
495 \begin{tabular}{llll}
496 header & theory & proof & default meaning \\\hline
497 & \commdx{chapter} & & \verb,\chapter, \\
498 \commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\
499 & \commdx{subsection} & \commdx{subsect} & \verb,\subsection, \\
500 & \commdx{subsubsection} & \commdx{subsubsect} & \verb,\subsubsection, \\
505 From the Isabelle perspective, each markup command takes a single
506 $text$ argument (delimited by \verb,",~\isa{{\isasymdots}}~\verb,", or
507 \verb,{,\verb,*,~\isa{{\isasymdots}}~\verb,*,\verb,},). After stripping any
508 surrounding white space, the argument is passed to a {\LaTeX} macro
509 \verb,\isamarkupXYZ, for command \isakeyword{XYZ}. These macros are
510 defined in \verb,isabelle.sty, according to the meaning given in the
511 rightmost column above.
513 \medskip The following source fragment illustrates structure markup
514 of a theory. Note that {\LaTeX} labels may be included inside of
515 section headings as well.
518 header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
524 subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
526 definition foo :: \dots
528 definition bar :: \dots
530 subsection {\ttlbrace}* Derived rules *{\ttrbrace}
535 subsection {\ttlbrace}* Main theorem {\ttback}label{\ttlbrace}sec:main-theorem{\ttrbrace} *{\ttrbrace}
540 \end{ttbox}\vspace{-\medskipamount}
542 You may occasionally want to change the meaning of markup commands,
543 say via \verb,\renewcommand, in \texttt{root.tex}. For example,
544 \verb,\isamarkupheader, is a good candidate for some tuning. We
545 could move it up in the hierarchy to become \verb,\chapter,.
548 \renewcommand{\isamarkupheader}[1]{\chapter{#1}}
551 \noindent Now we must change the document class given in
552 \texttt{root.tex} to something that supports chapters. A suitable
553 command is \verb,\documentclass{report},.
555 \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to
556 hold the name of the current theory context. This is particularly
557 useful for document headings:
560 \renewcommand{\isamarkupheader}[1]
561 {\chapter{#1}\markright{THEORY~\isabellecontext}}
564 \noindent Make sure to include something like
565 \verb,\pagestyle{headings}, in \texttt{root.tex}; the document
566 should have more than two pages to show the effect.%
570 \isamarkupsubsection{Formal Comments and Antiquotations \label{sec:doc-prep-text}%
574 \begin{isamarkuptext}%
575 Isabelle \bfindex{source comments}, which are of the form
576 \verb,(,\verb,*,~\isa{{\isasymdots}}~\verb,*,\verb,),, essentially act like
577 white space and do not really contribute to the content. They
578 mainly serve technical purposes to mark certain oddities in the raw
579 input text. In contrast, \bfindex{formal comments} are portions of
580 text that are associated with formal Isabelle/Isar commands
581 (\bfindex{marginal comments}), or as standalone paragraphs within a
582 theory or proof context (\bfindex{text blocks}).
584 \medskip Marginal comments are part of each command's concrete
585 syntax \cite{isabelle-ref}; the common form is ``\verb,--,~$text$''
586 where $text$ is delimited by \verb,",\isa{{\isasymdots}}\verb,", or
587 \verb,{,\verb,*,~\isa{{\isasymdots}}~\verb,*,\verb,}, as before. Multiple
588 marginal comments may be given at the same time. Here is a simple
592 \isacommand{lemma}\isamarkupfalse%
593 \ {\isachardoublequoteopen}A\ {\isacharminus}{\isacharminus}{\isachargreater}\ A{\isachardoublequoteclose}\isanewline
595 \isamarkupcmt{a triviality of propositional logic%
599 \isamarkupcmt{(should not really bother)%
608 \isacommand{by}\isamarkupfalse%
609 \ {\isacharparenleft}rule\ impI{\isacharparenright}\ %
610 \isamarkupcmt{implicit assumption step involved here%
620 \begin{isamarkuptext}%
621 \noindent The above output has been produced as follows:
625 -- "a triviality of propositional logic"
626 -- "(should not really bother)"
627 by (rule impI) -- "implicit assumption step involved here"
630 From the {\LaTeX} viewpoint, ``\verb,--,'' acts like a markup
631 command, associated with the macro \verb,\isamarkupcmt, (taking a
634 \medskip Text blocks are introduced by the commands \bfindex{text}
635 and \bfindex{txt}, for theory and proof contexts, respectively.
636 Each takes again a single $text$ argument, which is interpreted as a
637 free-form paragraph in {\LaTeX} (surrounded by some additional
638 vertical space). This behavior may be changed by redefining the
639 {\LaTeX} environments of \verb,isamarkuptext, or
640 \verb,isamarkuptxt,, respectively (via \verb,\renewenvironment,) The
641 text style of the body is determined by \verb,\isastyletext, and
642 \verb,\isastyletxt,; the default setup uses a smaller font within
643 proofs. This may be changed as follows:
646 \renewcommand{\isastyletxt}{\isastyletext}
649 \medskip The $text$ part of Isabelle markup commands essentially
650 inserts \emph{quoted material} into a formal text, mainly for
651 instruction of the reader. An \bfindex{antiquotation} is again a
652 formal object embedded into such an informal portion. The
653 interpretation of antiquotations is limited to some well-formedness
654 checks, with the result being pretty printed to the resulting
655 document. Quoted text blocks together with antiquotations provide
656 an attractive means of referring to formal entities, with good
657 confidence in getting the technical details right (especially syntax
660 The general syntax of antiquotations is as follows:
661 \texttt{{\at}{\ttlbrace}$name$ $arguments${\ttrbrace}}, or
662 \texttt{{\at}{\ttlbrace}$name$ [$options$] $arguments${\ttrbrace}}
663 for a comma-separated list of options consisting of a $name$ or
664 \texttt{$name$=$value$} each. The syntax of $arguments$ depends on
665 the kind of antiquotation, it generally follows the same conventions
666 for types, terms, or theorems as in the formal part of a theory.
668 \medskip This sentence demonstrates quotations and antiquotations:
669 \isa{{\isasymlambda}x\ y{\isachardot}\ x} is a well-typed term.
671 \medskip\noindent The output above was produced as follows:
674 This sentence demonstrates quotations and antiquotations:
675 {\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term.
677 \end{ttbox}\vspace{-\medskipamount}
679 The notational change from the ASCII character~\verb,%, to the
680 symbol~\isa{{\isasymlambda}} reveals that Isabelle printed this term, after
681 parsing and type-checking. Document preparation enables symbolic
684 \medskip The next example includes an option to show the type of all
685 variables. The antiquotation
686 \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces the
687 output \isa{{\isasymlambda}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ y{\isasymColon}{\isacharprime}b{\isachardot}\ x}. Type inference has figured
688 out the most general typings in the present theory context. Terms
689 may acquire different typings due to constraints imposed by their
690 environment; within a proof, for example, variables are given the
691 same types as they have in the main goal statement.
693 \medskip Several further kinds of antiquotations and options are
694 available \cite{isabelle-isar-ref}. Here are a few commonly used
700 \texttt{\at}\verb,{typ,~$\tau$\verb,}, & print type $\tau$ \\
701 \texttt{\at}\verb,{const,~$c$\verb,}, & check existence of $c$ and print it \\
702 \texttt{\at}\verb,{term,~$t$\verb,}, & print term $t$ \\
703 \texttt{\at}\verb,{prop,~$\phi$\verb,}, & print proposition $\phi$ \\
704 \texttt{\at}\verb,{prop [display],~$\phi$\verb,}, & print large proposition $\phi$ (with linebreaks) \\
705 \texttt{\at}\verb,{prop [source],~$\phi$\verb,}, & check proposition $\phi$, print its input \\
706 \texttt{\at}\verb,{thm,~$a$\verb,}, & print fact $a$ \\
707 \texttt{\at}\verb,{thm,~$a$~\verb,[no_vars]}, & print fact $a$, fixing schematic variables \\
708 \texttt{\at}\verb,{thm [source],~$a$\verb,}, & check availability of fact $a$, print its name \\
709 \texttt{\at}\verb,{text,~$s$\verb,}, & print uninterpreted text $s$ \\
714 Note that \attrdx{no_vars} given above is \emph{not} an
715 antiquotation option, but an attribute of the theorem argument given
716 here. This might be useful with a diagnostic command like
717 \isakeyword{thm}, too.
719 \medskip The \texttt{\at}\verb,{text, $s$\verb,}, antiquotation is
720 particularly interesting. Embedding uninterpreted text within an
721 informal body might appear useless at first sight. Here the key
722 virtue is that the string $s$ is processed as Isabelle output,
723 interpreting Isabelle symbols appropriately.
725 For example, \texttt{\at}\verb,{text "\<forall>\<exists>"}, produces \isa{{\isasymforall}{\isasymexists}}, according to the standard interpretation of these symbol
726 (cf.\ \S\ref{sec:doc-prep-symbols}). Thus we achieve consistent
727 mathematical notation in both the formal and informal parts of the
728 document very easily, independently of the term language of
729 Isabelle. Manual {\LaTeX} code would leave more control over the
730 typesetting, but is also slightly more tedious.%
734 \isamarkupsubsection{Interpretation of Symbols \label{sec:doc-prep-symbols}%
738 \begin{isamarkuptext}%
739 As has been pointed out before (\S\ref{sec:syntax-symbols}),
740 Isabelle symbols are the smallest syntactic entities --- a
741 straightforward generalization of ASCII characters. While Isabelle
742 does not impose any interpretation of the infinite collection of
743 named symbols, {\LaTeX} documents use canonical glyphs for certain
744 standard symbols \cite{isabelle-isar-ref}.
746 The {\LaTeX} code produced from Isabelle text follows a simple
747 scheme. You can tune the final appearance by redefining certain
748 macros, say in \texttt{root.tex} of the document.
752 \item 7-bit ASCII characters: letters \texttt{A\dots Z} and
753 \texttt{a\dots z} are output directly, digits are passed as an
754 argument to the \verb,\isadigit, macro, other characters are
755 replaced by specifically named macros of the form
758 \item Named symbols: \verb,\,\verb,<XYZ>, is turned into
759 \verb,{\isasymXYZ},; note the additional braces.
761 \item Named control symbols: \verb,\,\verb,<^XYZ>, is turned into
762 \verb,\isactrlXYZ,; subsequent symbols may act as arguments if the
763 control macro is defined accordingly.
767 You may occasionally wish to give new {\LaTeX} interpretations of
768 named symbols. This merely requires an appropriate definition of
769 \verb,\isasymXYZ,, for \verb,\,\verb,<XYZ>, (see
770 \texttt{isabelle.sty} for working examples). Control symbols are
771 slightly more difficult to get right, though.
773 \medskip The \verb,\isabellestyle, macro provides a high-level
774 interface to tune the general appearance of individual symbols. For
775 example, \verb,\isabellestyle{it}, uses the italics text style to
776 mimic the general appearance of the {\LaTeX} math mode; double
777 quotes are not printed at all. The resulting quality of typesetting
778 is quite good, so this should be the default style for work that
779 gets distributed to a broader audience.%
783 \isamarkupsubsection{Suppressing Output \label{sec:doc-prep-suppress}%
787 \begin{isamarkuptext}%
788 By default, Isabelle's document system generates a {\LaTeX} file for
789 each theory that gets loaded while running the session. The
790 generated \texttt{session.tex} will include all of these in order of
791 appearance, which in turn gets included by the standard
792 \texttt{root.tex}. Certainly one may change the order or suppress
793 unwanted theories by ignoring \texttt{session.tex} and load
794 individual files directly in \texttt{root.tex}. On the other hand,
795 such an arrangement requires additional maintenance whenever the
796 collection of theories changes.
798 Alternatively, one may tune the theory loading process in
799 \texttt{ROOT.ML} itself: traversal of the theory dependency graph
800 may be fine-tuned by adding \verb,use_thy, invocations, although
801 topological sorting still has to be observed. Moreover, the ML
802 operator \verb,no_document, temporarily disables document generation
803 while executing a theory loader command. Its usage is like this:
806 no_document use_thy "T";
809 \medskip Theory output may be suppressed more selectively, either
810 via \bfindex{tagged command regions} or \bfindex{ignored material}.
812 Tagged command regions works by annotating commands with named tags,
813 which correspond to certain {\LaTeX} markup that tells how to treat
814 particular parts of a document when doing the actual type-setting.
815 By default, certain Isabelle/Isar commands are implicitly marked up
816 using the predefined tags ``\emph{theory}'' (for theory begin and
817 end), ``\emph{proof}'' (for proof commands), and ``\emph{ML}'' (for
818 commands involving ML code). Users may add their own tags using the
819 \verb,%,\emph{tag} notation right after a command name. In the
820 subsequent example we hide a particularly irrelevant proof:%
823 \isacommand{lemma}\isamarkupfalse%
824 \ {\isachardoublequoteopen}x\ {\isacharequal}\ x{\isachardoublequoteclose}%
827 \endisadeliminvisible
830 \isacommand{by}\isamarkupfalse%
831 \ {\isacharparenleft}simp{\isacharparenright}%
837 \endisadeliminvisible
839 \begin{isamarkuptext}%
840 The original source has been ``\verb,lemma "x = x" by %invisible (simp),''.
841 Tags observe the structure of proofs; adjacent commands with the
842 same tag are joined into a single region. The Isabelle document
843 preparation system allows the user to specify how to interpret a
844 tagged region, in order to keep, drop, or fold the corresponding
845 parts of the document. See the \emph{Isabelle System Manual}
846 \cite{isabelle-sys} for further details, especially on
847 \texttt{isabelle usedir} and \texttt{isabelle document}.
849 Ignored material is specified by delimiting the original formal
850 source with special source comments
851 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
852 \verb,(,\verb,*,\verb,>,\verb,*,\verb,),. These parts are stripped
853 before the type-setting phase, without affecting the formal checking
854 of the theory, of course. For example, we may hide parts of a proof
855 that seem unfit for general public inspection. The following
856 ``fully automatic'' proof is actually a fake:%
859 \isacommand{lemma}\isamarkupfalse%
860 \ {\isachardoublequoteopen}x\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isacharless}\ x\ {\isacharasterisk}\ x{\isachardoublequoteclose}\isanewline
867 \isacommand{by}\isamarkupfalse%
868 \ {\isacharparenleft}auto{\isacharparenright}%
876 \begin{isamarkuptext}%
877 \noindent The real source of the proof has been as follows:
880 by (auto(*<*)simp add: zero_less_mult_iff(*>*))
884 \medskip Suppressing portions of printed text demands care. You
885 should not misrepresent the underlying theory development. It is
886 easy to invalidate the visible text by hiding references to
887 questionable axioms, for example.%
906 %%% TeX-master: "root"