3 \def\isabellecontext{Documents}%
6 \isamarkupsection{Concrete Syntax \label{sec:concrete-syntax}%
10 \begin{isamarkuptext}%
11 The core concept of Isabelle's framework for concrete syntax is that
12 of \bfindex{mixfix annotations}. Associated with any kind of
13 constant declaration, mixfixes affect both the grammar productions
14 for the parser and output templates for the pretty printer.
16 In full generality, parser and pretty printer configuration is a
17 subtle affair \cite{isabelle-ref}. Your syntax specifications need
18 to interact properly with the existing setup of Isabelle/Pure and
19 Isabelle/HOL\@. To avoid creating ambiguities with existing
20 elements, it is particularly important to give new syntactic
21 constructs the right precedence.
23 \medskip Subsequently we introduce a few simple syntax declaration
24 forms that already cover many common situations fairly well.%
28 \isamarkupsubsection{Infix Annotations%
32 \begin{isamarkuptext}%
33 Syntax annotations may be included wherever constants are declared,
34 such as \isacommand{consts} and \isacommand{constdefs} --- and also
35 \isacommand{datatype}, which declares constructor operations.
36 Type-constructors may be annotated as well, although this is less
37 frequently encountered in practice (the infix type \isa{{\isasymtimes}} comes
40 Infix declarations\index{infix annotations} provide a useful special
41 case of mixfixes. The following example of the exclusive-or
42 operation on boolean values illustrates typical infix declarations.%
45 \isacommand{constdefs}\isanewline
46 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
47 \ \ {\isachardoublequote}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
49 \begin{isamarkuptext}%
50 \noindent Now \isa{xor\ A\ B} and \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} refer to the
51 same expression internally. Any curried function with at least two
52 arguments may be given infix syntax. For partial applications with
53 fewer than two operands, there is a notation using the prefix~\isa{op}. For instance, \isa{xor} without arguments is represented as
54 \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}}; together with ordinary function application, this
55 turns \isa{xor\ A} into \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ A}.
57 \medskip The keyword \isakeyword{infixl} seen above specifies an
58 infix operator that is nested to the \emph{left}: in iterated
59 applications the more complex expression appears on the left-hand
60 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
61 \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}
62 would render \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} illegal, but demand explicit
63 parentheses to indicate the intended grouping.
65 The string \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}} in our annotation refers to the
66 concrete syntax to represent the operator (a literal token), while
67 the number \isa{{\isadigit{6}}{\isadigit{0}}} determines the precedence of the construct:
68 the syntactic priorities of the arguments and result. Isabelle/HOL
69 already uses up many popular combinations of ASCII symbols for its
70 own use, including both \isa{{\isacharplus}} and \isa{{\isacharplus}{\isacharplus}}. Longer
71 character combinations are more likely to be still available for
72 user extensions, such as our~\isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}}.
74 Operator precedences have a range of 0--1000. Very low or high
75 priorities are reserved for the meta-logic. HOL syntax mainly uses
76 the range of 10--100: the equality infix \isa{{\isacharequal}} is centered at
77 50; logical connectives (like \isa{{\isasymor}} and \isa{{\isasymand}}) are
78 below 50; algebraic ones (like \isa{{\isacharplus}} and \isa{{\isacharasterisk}}) are
79 above 50. User syntax should strive to coexist with common HOL
80 forms, or use the mostly unused range 100--900.%
84 \isamarkupsubsection{Mathematical Symbols \label{sec:syntax-symbols}%
88 \begin{isamarkuptext}%
89 Concrete syntax based on ASCII characters has inherent limitations.
90 Mathematical notation demands a larger repertoire of glyphs.
91 Several standards of extended character sets have been proposed over
92 decades, but none has become universally available so far. Isabelle
93 has its own notion of \bfindex{symbols} as the smallest entities of
94 source text, without referring to internal encodings. There are
95 three kinds of such ``generalized characters'':
99 \item 7-bit ASCII characters
101 \item named symbols: \verb,\,\verb,<,$ident$\verb,>,
103 \item named control symbols: \verb,\,\verb,<^,$ident$\verb,>,
107 Here $ident$ is any sequence of letters.
108 This results in an infinite store of symbols, whose
109 interpretation is left to further front-end tools. For example, the
110 user-interface of Proof~General + X-Symbol and the Isabelle document
111 processor (see \S\ref{sec:document-preparation}) display the
112 \verb,\,\verb,<forall>, symbol as~\isa{{\isasymforall}}.
114 A list of standard Isabelle symbols is given in
115 \cite[appendix~A]{isabelle-sys}. You may introduce your own
116 interpretation of further symbols by configuring the appropriate
117 front-end tool accordingly, e.g.\ by defining certain {\LaTeX}
118 macros (see also \S\ref{sec:doc-prep-symbols}). There are also a
119 few predefined control symbols, such as \verb,\,\verb,<^sub>, and
120 \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent
121 printable symbol, respectively. For example, \verb,A\<^sup>\<star>, is
122 output as \isa{A\isactrlsup {\isasymstar}}.
124 A number of symbols are considered letters by the Isabelle lexer
125 and can be used as part of identifiers. These are the greek letters
126 \isa{{\isasymalpha}} (\verb+\+\verb+<alpha>+), \isa{{\isasymbeta}}, etc apart from
127 \isa{{\isasymlambda}}, caligraphic letters like \isa{{\isasymA}}
128 (\verb+\+\verb+<A>+) and \isa{{\isasymAA}} (\verb+\+\verb+<AA>+),
129 and the special control symbols \verb+\+\verb+<^isub>+ and
130 \verb+\+\verb+<^isup>+ for single letter sub and super scripts. This
134 {\small\noindent \verb,\,\verb,<forall>\,\verb,<alpha>\<^isub>1.\,\verb,<alpha>\<^isub>1=\,\verb,<Pi>\<^isup>\<A>,}
137 \noindent is recognized as the term \isa{{\isasymforall}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isachardot}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isacharequal}\ {\isasymPi}\isactrlisup {\isasymA}}
138 by Isabelle. Note that \isa{{\isasymPi}\isactrlisup {\isasymA}} is a single entity like
139 \isa{PA}, not an exponentiation.
142 \medskip Replacing our definition of \isa{xor} by the following
143 specifies an Isabelle symbol for the new operator:%
148 \isacommand{constdefs}\isanewline
149 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
150 \ \ {\isachardoublequote}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
153 \begin{isamarkuptext}%
154 \noindent The X-Symbol package within Proof~General provides several
155 input methods to enter \isa{{\isasymoplus}} in the text. If all fails one may
156 just type a named entity \verb,\,\verb,<oplus>, by hand; the
157 corresponding symbol will be displayed after further input.
159 \medskip More flexible is to provide alternative syntax forms
160 through the \bfindex{print mode} concept~\cite{isabelle-ref}. By
161 convention, the mode of ``$xsymbols$'' is enabled whenever
162 Proof~General's X-Symbol mode or {\LaTeX} output is active. Now
163 consider the following hybrid declaration of \isa{xor}:%
168 \isacommand{constdefs}\isanewline
169 \ \ 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
170 \ \ {\isachardoublequote}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isasymignore}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline
173 \isacommand{syntax}\ {\isacharparenleft}xsymbols{\isacharparenright}\isanewline
174 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
177 \begin{isamarkuptext}%
178 The \commdx{syntax} command introduced here acts like
179 \isakeyword{consts}, but without declaring a logical constant. The
180 print mode specification of \isakeyword{syntax}, here \isa{{\isacharparenleft}xsymbols{\isacharparenright}}, is optional. Also note that its type merely serves
181 for syntactic purposes, and is \emph{not} checked for consistency
182 with the real constant.
184 \medskip We may now write \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} or \isa{A\ {\isasymoplus}\ B} in
185 input, while output uses the nicer syntax of $xsymbols$ whenever
186 that print mode is active. Such an arrangement is particularly
187 useful for interactive development, where users may type ASCII text
188 and see mathematical symbols displayed during proofs.%
192 \isamarkupsubsection{Prefix Annotations%
196 \begin{isamarkuptext}%
197 Prefix syntax annotations\index{prefix annotation} are another form
198 of mixfixes \cite{isabelle-ref}, without any template arguments or
199 priorities --- just some literal syntax. The following example
200 associates common symbols with the constructors of a datatype.%
203 \isacommand{datatype}\ currency\ {\isacharequal}\isanewline
204 \ \ \ \ Euro\ nat\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymeuro}{\isachardoublequote}{\isacharparenright}\isanewline
205 \ \ {\isacharbar}\ Pounds\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isasympounds}{\isachardoublequote}{\isacharparenright}\isanewline
206 \ \ {\isacharbar}\ Yen\ nat\ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymyen}{\isachardoublequote}{\isacharparenright}\isanewline
207 \ \ {\isacharbar}\ Dollar\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isachardollar}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
209 \begin{isamarkuptext}%
210 \noindent Here the mixfix annotations on the rightmost column happen
211 to consist of a single Isabelle symbol each: \verb,\,\verb,<euro>,,
212 \verb,\,\verb,<pounds>,, \verb,\,\verb,<yen>,, and \verb,$,. Recall
213 that a constructor like \isa{Euro} actually is a function \isa{nat\ {\isasymRightarrow}\ currency}. The expression \isa{Euro\ {\isadigit{1}}{\isadigit{0}}} will be
214 printed as \isa{{\isasymeuro}\ {\isadigit{1}}{\isadigit{0}}}; only the head of the application is
215 subject to our concrete syntax. This rather simple form already
216 achieves conformance with notational standards of the European
219 Prefix syntax works the same way for \isakeyword{consts} or
220 \isakeyword{constdefs}.%
224 \isamarkupsubsection{Syntax Translations \label{sec:syntax-translations}%
228 \begin{isamarkuptext}%
229 Mixfix syntax annotations merely decorate particular constant
230 application forms with concrete syntax, for instance replacing \
231 \isa{xor\ A\ B} by \isa{A\ {\isasymoplus}\ B}. Occasionally, the
232 relationship between some piece of notation and its internal form is
233 more complicated. Here we need \bfindex{syntax translations}.
235 Using the \isakeyword{syntax}\index{syntax (command)}, command we
236 introduce uninterpreted notational elements. Then
237 \commdx{translations} relate input forms to complex logical
238 expressions. This provides a simple mechanism for syntactic macros;
239 even heavier transformations may be written in ML
242 \medskip A typical use of syntax translations is to introduce
243 relational notation for membership in a set of pair, replacing \
244 \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} by \isa{x\ {\isasymapprox}\ y}.%
247 \isacommand{consts}\isanewline
248 \ \ sim\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set{\isachardoublequote}\isanewline
251 \isacommand{syntax}\isanewline
252 \ \ {\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
254 \isacommand{translations}\isanewline
255 \ \ {\isachardoublequote}x\ {\isasymapprox}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim{\isachardoublequote}\isamarkupfalse%
257 \begin{isamarkuptext}%
258 \noindent Here the name of the dummy constant \isa{{\isacharunderscore}sim} does
259 not matter, as long as it is not used elsewhere. Prefixing an
260 underscore is a common convention. The \isakeyword{translations}
261 declaration already uses concrete syntax on the left-hand side;
262 internally we relate a raw application \isa{{\isacharunderscore}sim\ x\ y} with
263 \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim}.
265 \medskip Another common application of syntax translations is to
266 provide variant versions of fundamental relational expressions, such
267 as \isa{{\isasymnoteq}} for negated equalities. The following declaration
268 stems from Isabelle/HOL itself:%
271 \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
273 \isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}{\isasymignore}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
275 \begin{isamarkuptext}%
276 \noindent Normally one would introduce derived concepts like this
277 within the logic, using \isakeyword{consts} + \isakeyword{defs}
278 instead of \isakeyword{syntax} + \isakeyword{translations}. The
279 present formulation has the virtue that expressions are immediately
280 replaced by the ``definition'' upon parsing; the effect is reversed
283 This sort of translation is appropriate when the defined concept is
284 a trivial variation on an existing one. On the other hand, syntax
285 translations do not scale up well to large hierarchies of concepts.
286 Translations do not replace definitions!%
290 \isamarkupsection{Document Preparation \label{sec:document-preparation}%
294 \begin{isamarkuptext}%
295 Isabelle/Isar is centered around the concept of \bfindex{formal
296 proof documents}\index{documents|bold}. The outcome of a formal
297 development effort is meant to be a human-readable record, presented
298 as browsable PDF file or printed on paper. The overall document
299 structure follows traditional mathematical articles, with sections,
300 intermediate explanations, definitions, theorems and proofs.
302 \medskip The Isabelle document preparation system essentially acts
303 as a front-end to {\LaTeX}. After checking specifications and
304 proofs formally, the theory sources are turned into typesetting
305 instructions in a schematic manner. This lets you write authentic
306 reports on theory developments with little effort: many technical
307 consistency checks are handled by the system.
309 Here is an example to illustrate the idea of Isabelle document
316 \begin{isamarkuptext}%
317 The following datatype definition of \isa{{\isacharprime}a\ bintree} models
318 binary trees with nodes being decorated by elements of type \isa{{\isacharprime}a}.%
321 \isacommand{datatype}\ {\isacharprime}a\ bintree\ {\isacharequal}\isanewline
322 \ \ \ \ \ Leaf\ {\isacharbar}\ Branch\ {\isacharprime}a\ \ {\isachardoublequote}{\isacharprime}a\ bintree{\isachardoublequote}\ \ {\isachardoublequote}{\isacharprime}a\ bintree{\isachardoublequote}\isamarkupfalse%
324 \begin{isamarkuptext}%
325 \noindent The datatype induction rule generated here is of the form
327 \ {\isasymlbrakk}P\ Leaf{\isacharsemicolon}\isanewline
328 \isaindent{\ \ }{\isasymAnd}a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isachardot}\isanewline
329 \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
330 \isaindent{\ }{\isasymLongrightarrow}\ P\ bintree%
337 \begin{isamarkuptext}%
338 \noindent The above document output has been produced as follows:
342 The following datatype definition of {\at}{\ttlbrace}text "'a bintree"{\ttrbrace}
343 models binary trees with nodes being decorated by elements
344 of type {\at}{\ttlbrace}typ 'a{\ttrbrace}.
347 datatype 'a bintree =
348 Leaf | Branch 'a "'a bintree" "'a bintree"
352 {\ttback}noindent The datatype induction rule generated here is
353 of the form {\at}{\ttlbrace}thm [display] bintree.induct [no_vars]{\ttrbrace}
355 \end{ttbox}\vspace{-\medskipamount}
357 \noindent Here we have augmented the theory by formal comments
358 (using \isakeyword{text} blocks), the informal parts may again refer
359 to formal entities by means of ``antiquotations'' (such as
360 \texttt{\at}\verb,{text "'a bintree"}, or
361 \texttt{\at}\verb,{typ 'a},), see also \S\ref{sec:doc-prep-text}.%
365 \isamarkupsubsection{Isabelle Sessions%
369 \begin{isamarkuptext}%
370 In contrast to the highly interactive mode of Isabelle/Isar theory
371 development, the document preparation stage essentially works in
372 batch-mode. An Isabelle \bfindex{session} consists of a collection
373 of source files that may contribute to an output document. Each
374 session is derived from a single parent, usually an object-logic
375 image like \texttt{HOL}. This results in an overall tree structure,
376 which is reflected by the output location in the file system
377 (usually rooted at \verb,~/isabelle/browser_info,).
379 \medskip The easiest way to manage Isabelle sessions is via
380 \texttt{isatool mkdir} (generates an initial session source setup)
381 and \texttt{isatool make} (run sessions controlled by
382 \texttt{IsaMakefile}). For example, a new session
383 \texttt{MySession} derived from \texttt{HOL} may be produced as
387 isatool mkdir HOL MySession
391 The \texttt{isatool make} job also informs about the file-system
392 location of the ultimate results. The above dry run should be able
393 to produce some \texttt{document.pdf} (with dummy title, empty table
394 of contents etc.). Any failure at this stage usually indicates
395 technical problems of the {\LaTeX} installation.\footnote{Especially
396 make sure that \texttt{pdflatex} is present; if in doubt one may
397 fall back on DVI output by changing \texttt{usedir} options in
398 \texttt{IsaMakefile} \cite{isabelle-sys}.}
400 \medskip The detailed arrangement of the session sources is as
405 \item Directory \texttt{MySession} holds the required theory files
406 $T@1$\texttt{.thy}, \dots, $T@n$\texttt{.thy}.
408 \item File \texttt{MySession/ROOT.ML} holds appropriate ML commands
409 for loading all wanted theories, usually just
410 ``\texttt{use_thy"$T@i$";}'' for any $T@i$ in leaf position of the
413 \item Directory \texttt{MySession/document} contains everything
414 required for the {\LaTeX} stage; only \texttt{root.tex} needs to be
417 The latter file holds appropriate {\LaTeX} code to commence a
418 document (\verb,\documentclass, etc.), and to include the generated
419 files $T@i$\texttt{.tex} for each theory. Isabelle will generate a
420 file \texttt{session.tex} holding {\LaTeX} commands to include all
421 generated theory output files in topologically sorted order, so
422 \verb,\input{session}, in the body of \texttt{root.tex} does the job
425 \item \texttt{IsaMakefile} holds appropriate dependencies and
426 invocations of Isabelle tools to control the batch job. In fact,
427 several sessions may be managed by the same \texttt{IsaMakefile}.
428 See the \emph{Isabelle System Manual} \cite{isabelle-sys}
429 for further details, especially on
430 \texttt{isatool usedir} and \texttt{isatool make}.
434 One may now start to populate the directory \texttt{MySession}, and
435 the file \texttt{MySession/ROOT.ML} accordingly. The file
436 \texttt{MySession/document/root.tex} should also be adapted at some
437 point; the default version is mostly self-explanatory. Note that
438 \verb,\isabellestyle, enables fine-tuning of the general appearance
439 of characters and mathematical symbols (see also
440 \S\ref{sec:doc-prep-symbols}).
442 Especially observe the included {\LaTeX} packages \texttt{isabelle}
443 (mandatory), \texttt{isabellesym} (required for mathematical
444 symbols), and the final \texttt{pdfsetup} (provides sane defaults
445 for \texttt{hyperref}, including URL markup). All three are
446 distributed with Isabelle. Further packages may be required in
447 particular applications, say for unusual mathematical symbols.
449 \medskip Any additional files for the {\LaTeX} stage go into the
450 \texttt{MySession/document} directory as well. In particular,
451 adding a file named \texttt{root.bib} causes an automatic run of
452 \texttt{bibtex} to process a bibliographic database; see also
453 \texttt{isatool document} \cite{isabelle-sys}.
455 \medskip Any failure of the document preparation phase in an
456 Isabelle batch session leaves the generated sources in their target
457 location, identified by the accompanying error message. This lets
458 you trace {\LaTeX} problems with the generated files at hand.%
462 \isamarkupsubsection{Structure Markup%
466 \begin{isamarkuptext}%
467 The large-scale structure of Isabelle documents follows existing
468 {\LaTeX} conventions, with chapters, sections, subsubsections etc.
469 The Isar language includes separate \bfindex{markup commands}, which
470 do not affect the formal meaning of a theory (or proof), but result
471 in corresponding {\LaTeX} elements.
473 There are separate markup commands depending on the textual context:
474 in header position (just before \isakeyword{theory}), within the
475 theory body, or within a proof. The header needs to be treated
476 specially here, since ordinary theory and proof commands may only
477 occur \emph{after} the initial \isakeyword{theory} specification.
481 \begin{tabular}{llll}
482 header & theory & proof & default meaning \\\hline
483 & \commdx{chapter} & & \verb,\chapter, \\
484 \commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\
485 & \commdx{subsection} & \commdx{subsect} & \verb,\subsection, \\
486 & \commdx{subsubsection} & \commdx{subsubsect} & \verb,\subsubsection, \\
491 From the Isabelle perspective, each markup command takes a single
492 $text$ argument (delimited by \verb,",~\isa{{\isasymdots}}~\verb,", or
493 \verb,{,\verb,*,~\isa{{\isasymdots}}~\verb,*,\verb,},). After stripping any
494 surrounding white space, the argument is passed to a {\LaTeX} macro
495 \verb,\isamarkupXYZ, for command \isakeyword{XYZ}. These macros are
496 defined in \verb,isabelle.sty, according to the meaning given in the
497 rightmost column above.
499 \medskip The following source fragment illustrates structure markup
500 of a theory. Note that {\LaTeX} labels may be included inside of
501 section headings as well.
504 header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
510 subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
518 subsection {\ttlbrace}* Derived rules *{\ttrbrace}
523 subsection {\ttlbrace}* Main theorem {\ttback}label{\ttlbrace}sec:main-theorem{\ttrbrace} *{\ttrbrace}
528 \end{ttbox}\vspace{-\medskipamount}
530 You may occasionally want to change the meaning of markup commands,
531 say via \verb,\renewcommand, in \texttt{root.tex}. For example,
532 \verb,\isamarkupheader, is a good candidate for some tuning. We
533 could move it up in the hierarchy to become \verb,\chapter,.
536 \renewcommand{\isamarkupheader}[1]{\chapter{#1}}
539 \noindent Now we must change the document class given in
540 \texttt{root.tex} to something that supports chapters. A suitable
541 command is \verb,\documentclass{report},.
543 \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to
544 hold the name of the current theory context. This is particularly
545 useful for document headings:
548 \renewcommand{\isamarkupheader}[1]
549 {\chapter{#1}\markright{THEORY~\isabellecontext}}
552 \noindent Make sure to include something like
553 \verb,\pagestyle{headings}, in \texttt{root.tex}; the document
554 should have more than two pages to show the effect.%
558 \isamarkupsubsection{Formal Comments and Antiquotations \label{sec:doc-prep-text}%
562 \begin{isamarkuptext}%
563 Isabelle \bfindex{source comments}, which are of the form
564 \verb,(,\verb,*,~\isa{{\isasymdots}}~\verb,*,\verb,),, essentially act like
565 white space and do not really contribute to the content. They
566 mainly serve technical purposes to mark certain oddities in the raw
567 input text. In contrast, \bfindex{formal comments} are portions of
568 text that are associated with formal Isabelle/Isar commands
569 (\bfindex{marginal comments}), or as standalone paragraphs within a
570 theory or proof context (\bfindex{text blocks}).
572 \medskip Marginal comments are part of each command's concrete
573 syntax \cite{isabelle-ref}; the common form is ``\verb,--,~$text$''
574 where $text$ is delimited by \verb,",\isa{{\isasymdots}}\verb,", or
575 \verb,{,\verb,*,~\isa{{\isasymdots}}~\verb,*,\verb,}, as before. Multiple
576 marginal comments may be given at the same time. Here is a simple
580 \isacommand{lemma}\ {\isachardoublequote}A\ {\isacharminus}{\isacharminus}{\isachargreater}\ A{\isachardoublequote}\isanewline
582 \isamarkupcmt{a triviality of propositional logic%
586 \isamarkupcmt{(should not really bother)%
590 \isacommand{by}\ {\isacharparenleft}rule\ impI{\isacharparenright}\ %
591 \isamarkupcmt{implicit assumption step involved here%
595 \begin{isamarkuptext}%
596 \noindent The above output has been produced as follows:
600 -- "a triviality of propositional logic"
601 -- "(should not really bother)"
602 by (rule impI) -- "implicit assumption step involved here"
605 From the {\LaTeX} viewpoint, ``\verb,--,'' acts like a markup
606 command, associated with the macro \verb,\isamarkupcmt, (taking a
609 \medskip Text blocks are introduced by the commands \bfindex{text}
610 and \bfindex{txt}, for theory and proof contexts, respectively.
611 Each takes again a single $text$ argument, which is interpreted as a
612 free-form paragraph in {\LaTeX} (surrounded by some additional
613 vertical space). This behavior may be changed by redefining the
614 {\LaTeX} environments of \verb,isamarkuptext, or
615 \verb,isamarkuptxt,, respectively (via \verb,\renewenvironment,) The
616 text style of the body is determined by \verb,\isastyletext, and
617 \verb,\isastyletxt,; the default setup uses a smaller font within
618 proofs. This may be changed as follows:
621 \renewcommand{\isastyletxt}{\isastyletext}
624 \medskip The $text$ part of Isabelle markup commands essentially
625 inserts \emph{quoted material} into a formal text, mainly for
626 instruction of the reader. An \bfindex{antiquotation} is again a
627 formal object embedded into such an informal portion. The
628 interpretation of antiquotations is limited to some well-formedness
629 checks, with the result being pretty printed to the resulting
630 document. Quoted text blocks together with antiquotations provide
631 an attractive means of referring to formal entities, with good
632 confidence in getting the technical details right (especially syntax
635 The general syntax of antiquotations is as follows:
636 \texttt{{\at}{\ttlbrace}$name$ $arguments${\ttrbrace}}, or
637 \texttt{{\at}{\ttlbrace}$name$ [$options$] $arguments${\ttrbrace}}
638 for a comma-separated list of options consisting of a $name$ or
639 \texttt{$name$=$value$} each. The syntax of $arguments$ depends on
640 the kind of antiquotation, it generally follows the same conventions
641 for types, terms, or theorems as in the formal part of a theory.
643 \medskip This sentence demonstrates quotations and antiquotations:
644 \isa{{\isasymlambda}x\ y{\isachardot}\ x} is a well-typed term.
646 \medskip\noindent The output above was produced as follows:
649 This sentence demonstrates quotations and antiquotations:
650 {\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term.
652 \end{ttbox}\vspace{-\medskipamount}
654 The notational change from the ASCII character~\verb,%, to the
655 symbol~\isa{{\isasymlambda}} reveals that Isabelle printed this term, after
656 parsing and type-checking. Document preparation enables symbolic
659 \medskip The next example includes an option to modify Isabelle's
660 \verb,show_types, flag. The antiquotation
661 \texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces the
662 output \isa{{\isasymlambda}{\isacharparenleft}x{\isasymColon}{\isacharprime}a{\isacharparenright}\ y{\isasymColon}{\isacharprime}b{\isachardot}\ x}. Type inference has figured
663 out the most general typings in the present theory context. Terms
664 may acquire different typings due to constraints imposed by their
665 environment; within a proof, for example, variables are given the
666 same types as they have in the main goal statement.
668 \medskip Several further kinds of antiquotations and options are
669 available \cite{isabelle-sys}. Here are a few commonly used
675 \texttt{\at}\verb,{typ,~$\tau$\verb,}, & print type $\tau$ \\
676 \texttt{\at}\verb,{term,~$t$\verb,}, & print term $t$ \\
677 \texttt{\at}\verb,{prop,~$\phi$\verb,}, & print proposition $\phi$ \\
678 \texttt{\at}\verb,{prop [display],~$\phi$\verb,}, & print large proposition $\phi$ (with linebreaks) \\
679 \texttt{\at}\verb,{prop [source],~$\phi$\verb,}, & check proposition $\phi$, print its input \\
680 \texttt{\at}\verb,{thm,~$a$\verb,}, & print fact $a$ \\
681 \texttt{\at}\verb,{thm,~$a$~\verb,[no_vars]}, & print fact $a$, fixing schematic variables \\
682 \texttt{\at}\verb,{thm [source],~$a$\verb,}, & check availability of fact $a$, print its name \\
683 \texttt{\at}\verb,{text,~$s$\verb,}, & print uninterpreted text $s$ \\
688 Note that \attrdx{no_vars} given above is \emph{not} an
689 antiquotation option, but an attribute of the theorem argument given
690 here. This might be useful with a diagnostic command like
691 \isakeyword{thm}, too.
693 \medskip The \texttt{\at}\verb,{text, $s$\verb,}, antiquotation is
694 particularly interesting. Embedding uninterpreted text within an
695 informal body might appear useless at first sight. Here the key
696 virtue is that the string $s$ is processed as Isabelle output,
697 interpreting Isabelle symbols appropriately.
699 For example, \texttt{\at}\verb,{text "\<forall>\<exists>"}, produces \isa{{\isasymforall}{\isasymexists}}, according to the standard interpretation of these symbol
700 (cf.\ \S\ref{sec:doc-prep-symbols}). Thus we achieve consistent
701 mathematical notation in both the formal and informal parts of the
702 document very easily, independently of the term language of
703 Isabelle. Manual {\LaTeX} code would leave more control over the
704 typesetting, but is also slightly more tedious.%
708 \isamarkupsubsection{Interpretation of Symbols \label{sec:doc-prep-symbols}%
712 \begin{isamarkuptext}%
713 As has been pointed out before (\S\ref{sec:syntax-symbols}),
714 Isabelle symbols are the smallest syntactic entities --- a
715 straightforward generalization of ASCII characters. While Isabelle
716 does not impose any interpretation of the infinite collection of
717 named symbols, {\LaTeX} documents use canonical glyphs for certain
718 standard symbols \cite[appendix~A]{isabelle-sys}.
720 The {\LaTeX} code produced from Isabelle text follows a simple
721 scheme. You can tune the final appearance by redefining certain
722 macros, say in \texttt{root.tex} of the document.
726 \item 7-bit ASCII characters: letters \texttt{A\dots Z} and
727 \texttt{a\dots z} are output directly, digits are passed as an
728 argument to the \verb,\isadigit, macro, other characters are
729 replaced by specifically named macros of the form
732 \item Named symbols: \verb,\,\verb,<XYZ>, is turned into
733 \verb,{\isasymXYZ},; note the additional braces.
735 \item Named control symbols: \verb,\,\verb,<^XYZ>, is turned into
736 \verb,\isactrlXYZ,; subsequent symbols may act as arguments if the
737 control macro is defined accordingly.
741 You may occasionally wish to give new {\LaTeX} interpretations of
742 named symbols. This merely requires an appropriate definition of
743 \verb,\isasymXYZ,, for \verb,\,\verb,<XYZ>, (see
744 \texttt{isabelle.sty} for working examples). Control symbols are
745 slightly more difficult to get right, though.
747 \medskip The \verb,\isabellestyle, macro provides a high-level
748 interface to tune the general appearance of individual symbols. For
749 example, \verb,\isabellestyle{it}, uses the italics text style to
750 mimic the general appearance of the {\LaTeX} math mode; double
751 quotes are not printed at all. The resulting quality of typesetting
752 is quite good, so this should be the default style for work that
753 gets distributed to a broader audience.%
757 \isamarkupsubsection{Suppressing Output \label{sec:doc-prep-suppress}%
761 \begin{isamarkuptext}%
762 By default, Isabelle's document system generates a {\LaTeX} file for
763 each theory that gets loaded while running the session. The
764 generated \texttt{session.tex} will include all of these in order of
765 appearance, which in turn gets included by the standard
766 \texttt{root.tex}. Certainly one may change the order or suppress
767 unwanted theories by ignoring \texttt{session.tex} and load
768 individual files directly in \texttt{root.tex}. On the other hand,
769 such an arrangement requires additional maintenance whenever the
770 collection of theories changes.
772 Alternatively, one may tune the theory loading process in
773 \texttt{ROOT.ML} itself: traversal of the theory dependency graph
774 may be fine-tuned by adding \verb,use_thy, invocations, although
775 topological sorting still has to be observed. Moreover, the ML
776 operator \verb,no_document, temporarily disables document generation
777 while executing a theory loader command. Its usage is like this:
780 no_document use_thy "T";
783 \medskip Theory output may be suppressed more selectively. Research
784 articles and slides usually do not include the formal content in
785 full. Delimiting \bfindex{ignored material} by the special source
786 comments \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
787 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), tells the document
788 preparation system to suppress these parts; the formal checking of
789 the theory is unchanged, of course.
791 In this example, we hide a theory's \isakeyword{theory} and
792 \isakeyword{end} brackets:
797 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
799 \texttt{import Main} \\
801 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
803 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
805 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
810 Text may be suppressed in a fine-grained manner. We may even hide
811 vital parts of a proof, pretending that things have been simpler
812 than they really were. For example, this ``fully automatic'' proof
816 \isacommand{lemma}\ {\isachardoublequote}x\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isacharless}\ x\ {\isacharasterisk}\ x{\isachardoublequote}\isanewline
818 \isacommand{by}\ {\isacharparenleft}auto{\isacharparenright}\isamarkupfalse%
820 \begin{isamarkuptext}%
821 \noindent Here the real source of the proof has been as follows:
824 by (auto(*<*)simp add: zero_less_mult_iff(*>*))
828 \medskip Suppressing portions of printed text demands care. You
829 should not misrepresent the underlying theory development. It is
830 easy to invalidate the visible text by hiding references to
833 % I removed this because the page overflowed and I disagree a little. TN
835 % Authentic reports of Isabelle/Isar theories, say as part of a
836 % library, should suppress nothing. Other users may need the full
837 % information for their own derivative work. If a particular
838 % formalization appears inadequate for general public coverage, it is
839 % often more appropriate to think of a better way in the first place.
841 \medskip Some technical subtleties of the
842 \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),
843 elements need to be kept in mind, too --- the system performs few
844 sanity checks here. Arguments of markup commands and formal
845 comments must not be hidden, otherwise presentation fails. Open and
846 close parentheses need to be inserted carefully; it is easy to hide
847 the wrong parts, especially after rearranging the theory text.%
854 %%% TeX-master: "root"