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 \cite{isabelle-ref} for further
19 details. Any syntax specifications given by end-users need to
20 interact properly with the existing setup of Isabelle/Pure and
21 Isabelle/HOL. It is particularly important to get the precedence of
22 new syntactic constructs right, avoiding ambiguities with existing
25 \medskip Subsequently we introduce a few simple declaration forms
26 that already cover the most common situations fairly well.%
30 \isamarkupsubsection{Infix Annotations%
34 \begin{isamarkuptext}%
35 Syntax annotations may be included wherever constants are declared
36 directly or indirectly, including \isacommand{consts},
37 \isacommand{constdefs}, or \isacommand{datatype} (for the
38 constructor operations). Type-constructors may be annotated as
39 well, although this is less frequently encountered in practice
40 (\isa{{\isacharasterisk}} and \isa{{\isacharplus}} types may come to mind).
42 Infix declarations\index{infix annotations} provide a useful special
43 case of mixfixes, where users need not care about the full details
44 of priorities, nesting, spacing, etc. The subsequent example of the
45 exclusive-or operation on boolean values illustrates typical infix
46 declarations arising in practice.%
49 \isacommand{constdefs}\isanewline
50 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline
51 \ \ {\isachardoublequote}A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
53 \begin{isamarkuptext}%
54 \noindent Now \isa{xor\ A\ B} and \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B} refer to the
55 same expression internally. Any curried function with at least two
56 arguments may be associated with infix syntax. For partial
57 applications with less than two operands there is a special notation
58 with \isa{op} prefix: \isa{xor} without arguments is represented
59 as \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}}; together with plain prefix application this
60 turns \isa{xor\ A} into \isa{op\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ A}.
62 \medskip The string \isa{{\isachardoublequote}{\isacharbrackleft}{\isacharplus}{\isacharbrackright}{\isachardoublequote}} in the above annotation
63 refers to the bit of concrete syntax to represent the operator,
64 while the number \isa{{\isadigit{6}}{\isadigit{0}}} determines the precedence of the
65 construct (i.e.\ the syntactic priorities of the arguments and
68 As it happens, Isabelle/HOL already spends many popular combinations
69 of ASCII symbols for its own use, including both \isa{{\isacharplus}} and
70 \isa{{\isacharplus}{\isacharplus}}. Slightly more awkward combinations like the present
71 \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}} tend to be available for user extensions. The current
72 arrangement of inner syntax may be inspected via
73 \commdx{print\protect\_syntax}, albeit its output is enormous.
75 Operator precedence also needs some special considerations. The
76 admissible range is 0--1000. Very low or high priorities are
77 basically reserved for the meta-logic. Syntax of Isabelle/HOL
78 mainly uses the range of 10--100: the equality infix \isa{{\isacharequal}} is
79 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
80 HOL forms, or use the mostly unused range 100--900.
82 \medskip The keyword \isakeyword{infixl} specifies an operator that
83 is nested to the \emph{left}: in iterated applications the more
84 complex expression appears on the left-hand side: \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,
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 have rendered \isa{A\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ B\ {\isacharbrackleft}{\isacharplus}{\isacharbrackright}\ C} illegal, but demand
89 explicit parentheses about the intended grouping.%
93 \isamarkupsubsection{Mathematical 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 symbols. Several standards of extended character sets have been
101 proposed over decades, but none has become universally available so
102 far, not even Unicode\index{Unicode}. Isabelle supports a generic
103 notion of \bfindex{symbols} as the smallest entities of source text,
104 without referring to internal encodings.
106 There are three kinds of such ``generalized characters'' available:
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$ may be any identifier according to the usual Isabelle
119 conventions. This results in an infinite store of symbols, whose
120 interpretation is left to further front-end tools. For example,
121 both by the user-interface of Proof~General + X-Symbol and the
122 Isabelle document processor (see \S\ref{sec:document-preparation})
123 display the \verb,\,\verb,<forall>, symbol really as ``$\forall$''.
125 A list of standard Isabelle symbols is given in
126 \cite[appendix~A]{isabelle-sys}. Users may introduce their 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 shown as ``\isa{A\isactrlsup {\isasymstar}}''.
135 \medskip The following version of our \isa{xor} definition uses a
136 standard Isabelle symbol to achieve typographically pleasing output.%
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 \verb,\,\verb,<oplus>, by hand; the display will be
150 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. 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 here merely serves for syntactic purposes,
175 and is not checked for consistency with the real constant.
177 \medskip We may now write either \isa{{\isacharbrackleft}{\isacharplus}{\isacharbrackright}} or \isa{{\isasymoplus}} in
178 input, while output uses the nicer syntax of $xsymbols$, provided
179 that print mode is presently active. Such an arrangement is
180 particularly useful for interactive development, where users may
181 type plain ASCII text, but gain improved visual feedback from the
182 system (say in current goal output).
185 Alternative syntax declarations are apt to result in varying
186 occurrences of concrete syntax in the input sources. Isabelle
187 provides no systematic way to convert alternative syntax expressions
188 back and forth; print modes only affect situations where formal
189 entities are pretty printed by the Isabelle process (e.g.\ output of
190 terms and types), but not the original theory text.
193 \medskip The following variant makes the alternative \isa{{\isasymoplus}}
194 notation only available for output. Thus we may enforce input
195 sources to refer to plain ASCII only, but effectively disable
196 cut-and-paste from output as well.%
199 \isacommand{syntax}\ {\isacharparenleft}xsymbols\ \isakeyword{output}{\isacharparenright}\isanewline
200 \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isasymoplus}{\isasymignore}{\isachardoublequote}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse%
202 \isamarkupsubsection{Prefix Annotations%
206 \begin{isamarkuptext}%
207 Prefix syntax annotations\index{prefix annotation} are just another
208 degenerate form of general mixfixes \cite{isabelle-ref}, without any
209 template arguments or priorities --- just some bits of literal
210 syntax. The following example illustrates this idea idea by
211 associating common symbols with the constructors of a datatype.%
214 \isacommand{datatype}\ currency\ {\isacharequal}\isanewline
215 \ \ \ \ Euro\ nat\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymeuro}{\isachardoublequote}{\isacharparenright}\isanewline
216 \ \ {\isacharbar}\ Pounds\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isasympounds}{\isachardoublequote}{\isacharparenright}\isanewline
217 \ \ {\isacharbar}\ Yen\ nat\ \ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymyen}{\isachardoublequote}{\isacharparenright}\isanewline
218 \ \ {\isacharbar}\ Dollar\ nat\ \ {\isacharparenleft}{\isachardoublequote}{\isachardollar}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
220 \begin{isamarkuptext}%
221 \noindent Here the mixfix annotations on the rightmost column happen
222 to consist of a single Isabelle symbol each: \verb,\,\verb,<euro>,,
223 \verb,\,\verb,<pounds>,, \verb,\,\verb,<yen>,, and \verb,$,. Recall
224 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
225 printed as \isa{{\isasymeuro}\ {\isadigit{1}}{\isadigit{0}}}; only the head of the application is
226 subject to our concrete syntax. This simple form already achieves
227 conformance with notational standards of the European Commission.
229 \medskip Certainly, the same idea of prefix syntax also works for
230 \isakeyword{consts}, \isakeyword{constdefs} etc. The slightly
231 unusual syntax declaration below decorates the existing \isa{currency} type with the international currency symbol \isa{{\isasymcurrency}}
232 (\verb,\,\verb,<currency>,).%
235 \isacommand{syntax}\isanewline
236 \ \ currency\ {\isacharcolon}{\isacharcolon}\ type\ \ \ \ {\isacharparenleft}{\isachardoublequote}{\isasymcurrency}{\isachardoublequote}{\isacharparenright}\isamarkupfalse%
238 \begin{isamarkuptext}%
239 \noindent Here \isa{type} refers to the builtin syntactic category
240 of Isabelle types. We may now write down funny things like \isa{{\isasymeuro}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ {\isasymcurrency}}, for example.%
244 \isamarkupsubsection{Syntax Translations \label{sec:syntax-translations}%
248 \begin{isamarkuptext}%
249 Mixfix syntax annotations work well for those situations where a
250 particular constant application forms need to be decorated by
251 concrete syntax; just reconsider \isa{xor\ A\ B} versus \isa{A\ {\isasymoplus}\ B} covered before. Occasionally, the relationship between some
252 piece of notation and its internal form is slightly more involved.
253 Here the concept of \bfindex{syntax translations} enters the scene.
255 Using the raw \isakeyword{syntax}\index{syntax (command)} command we
256 may introduce uninterpreted notational elements, while
257 \commdx{translations} relates the input forms with more complex
258 logical expressions. This essentially provides a simple mechanism
259 for for syntactic macros; even heavier transformations may be
260 programmed in ML \cite{isabelle-ref}.
262 \medskip A typical example of syntax translations is to decorate
263 relational expressions (set membership of tuples) with nice symbolic
264 notation, such as \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim} versus \isa{x\ {\isasymapprox}\ y}.%
267 \isacommand{consts}\isanewline
268 \ \ sim\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set{\isachardoublequote}\isanewline
271 \isacommand{syntax}\isanewline
272 \ \ {\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
274 \isacommand{translations}\isanewline
275 \ \ {\isachardoublequote}x\ {\isasymapprox}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim{\isachardoublequote}\isamarkupfalse%
277 \begin{isamarkuptext}%
278 \noindent Here the name of the dummy constant \isa{{\isacharunderscore}sim} does
279 not really matter, as long as it is not used elsewhere. Prefixing
280 an underscore is a common convention. The \isakeyword{translations}
281 declaration already uses concrete syntax on the left-hand side;
282 internally we relate a raw application \isa{{\isacharunderscore}sim\ x\ y} with
283 \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ sim}.
285 \medskip Another common application of syntax translations is to
286 provide variant versions of fundamental relational expressions, such
287 as \isa{{\isasymnoteq}} for negated equalities. The following declaration
288 stems from Isabelle/HOL itself:%
291 \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
293 \isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}{\isasymignore}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
295 \begin{isamarkuptext}%
296 \noindent Normally one would introduce derived concepts like this
297 within the logic, using \isakeyword{consts} + \isakeyword{defs}
298 instead of \isakeyword{syntax} + \isakeyword{translations}. The
299 present formulation has the virtue that expressions are immediately
300 replaced by its ``definition'' upon parsing; the effect is reversed
301 upon printing. Internally, \isa{{\isasymnoteq}} never appears.
303 Simulating definitions via translations is adequate for very basic
304 logical concepts, where a new representation is a trivial variation
305 on an existing one. On the other hand, syntax translations do not
306 scale up well to large hierarchies of concepts built on each other.%
310 \isamarkupsection{Document Preparation \label{sec:document-preparation}%
314 \begin{isamarkuptext}%
315 Isabelle/Isar is centered around the concept of \bfindex{formal
316 proof documents}\index{documents|bold}. Ultimately the result of
317 the user's theory development efforts is meant to be a
318 human-readable record, presented as a browsable PDF file or printed
319 on paper. The overall document structure follows traditional
320 mathematical articles, with sectioning, intermediate explanations,
321 definitions, theorem statements and proofs.
323 The Isar proof language \cite{Wenzel-PhD}, which is not covered in
324 this book, admits to write formal proof texts that are acceptable
325 both to the machine and human readers at the same time. Thus
326 marginal comments and explanations may be kept at a minimum. Even
327 without proper coverage of human-readable proofs, Isabelle document
328 is very useful to produce formally derived texts (elaborating on the
329 specifications etc.). Unstructured proof scripts given here may be
330 just ignored by readers, or intentionally suppressed from the text
331 by the writer (see also \S\ref{sec:doc-prep-suppress}).
333 \medskip The Isabelle document preparation system essentially acts
334 like a formal front-end to {\LaTeX}. After checking specifications
335 and proofs, the theory sources are turned into typesetting
336 instructions in a well-defined manner. This enables users to write
337 authentic reports on formal theory developments with little
338 additional effort, the most tedious consistency checks are handled
343 \isamarkupsubsection{Isabelle Sessions%
347 \begin{isamarkuptext}%
348 In contrast to the highly interactive mode of Isabelle/Isar theory
349 development, the document preparation stage essentially works in
350 batch-mode. An Isabelle \bfindex{session} essentially consists of a
351 collection of theory source files that contribute to a single output
352 document eventually. Session is derived from a single parent each
353 (usually an object-logic image like \texttt{HOL}), resulting in an
354 overall tree structure that is reflected in the output location
355 within the file system (usually rooted at
356 \verb,~/isabelle/browser_info,).
358 Here is the canonical arrangement of sources of a session called
363 \item Directory \texttt{MySession} contains the required theory
364 files ($A@1$\texttt{.thy}, \dots, $A@n$\texttt{.thy}).
366 \item File \texttt{MySession/ROOT.ML} holds appropriate ML commands
367 for loading all wanted theories, usually just
368 ``\texttt{use_thy~"$A@i$";}'' for any $A@i$ in leaf position of the
369 theory dependency graph.
371 \item Directory \texttt{MySession/document} contains everything
372 required for the {\LaTeX} stage; only \texttt{root.tex} needs to be
375 The latter file holds appropriate {\LaTeX} code to commence a
376 document (\verb,\documentclass, etc.), and to include the generated
377 files $A@i$\texttt{.tex} for each theory. The generated
378 \texttt{session.tex} will hold {\LaTeX} commands to include all
379 theory output files in topologically sorted order, so
380 \verb,\input{session}, in \texttt{root.tex} will do it in most
383 \item In addition, \texttt{IsaMakefile} outside of the directory
384 \texttt{MySession} holds appropriate dependencies and invocations of
385 Isabelle tools to control the batch job. In fact, several sessions
386 may be controlled by the same \texttt{IsaMakefile}. See also
387 \cite{isabelle-sys} for further details, especially on
388 \texttt{isatool usedir} and \texttt{isatool make}.
392 With everything put in its proper place, \texttt{isatool make}
393 should be sufficient to process the Isabelle session completely,
394 with the generated document appearing in its proper place.
396 \medskip In practice, users may want to have \texttt{isatool mkdir}
397 generate an initial working setup without further ado. For example,
398 an empty session \texttt{MySession} derived from \texttt{HOL} may be
402 isatool mkdir HOL MySession
406 This processes the session with sensible default options, including
407 verbose mode to tell the user where the ultimate results will
408 appear. The above dry run should produce should already be able to
409 produce a single page of output (with a dummy title, empty table of
410 contents etc.). Any failure at that stage is likely to indicate
411 technical problems with the user's {\LaTeX}
412 installation.\footnote{Especially make sure that \texttt{pdflatex}
413 is present; if all fails one may fall back on DVI output by changing
414 \texttt{usedir} options \cite{isabelle-sys}.}
416 \medskip One may now start to populate the directory
417 \texttt{MySession}, and the file \texttt{MySession/ROOT.ML}
418 accordingly. \texttt{MySession/document/root.tex} should be also
419 adapted at some point; the default version is mostly
422 Especially note the standard inclusion of {\LaTeX} packages
423 \texttt{isabelle} (mandatory), and \texttt{isabellesym} (required
424 for mathematical symbols), and the final \texttt{pdfsetup} (provides
425 handsome defaults for \texttt{hyperref}, including URL markup).
426 Further {\LaTeX} packages further packages may required in
427 particular applications, e.g.\ for unusual Isabelle symbols.
429 \medskip Further auxiliary files for the {\LaTeX} stage should be
430 included in the \texttt{MySession/document} directory, e.g.\
431 additional {\TeX} sources or graphics. In particular, adding
432 \texttt{root.bib} here (with that specific name) causes an automatic
433 run of \texttt{bibtex} to process a bibliographic database; see for
434 further commodities \texttt{isatool document} covered in
437 \medskip Any failure of the document preparation phase in an
438 Isabelle batch session leaves the generated sources in there target
439 location (as pointed out by the accompanied error message). In case
440 of {\LaTeX} errors, users may trace error messages at the file
441 position of the generated text.%
445 \isamarkupsubsection{Structure Markup%
449 \begin{isamarkuptext}%
450 The large-scale structure of Isabelle documents follows existing
451 {\LaTeX} conventions, with chapters, sections, subsubsections etc.
452 The Isar language includes separate \bfindex{markup commands}, which
453 do not effect the formal content of a theory (or proof), but result
454 in corresponding {\LaTeX} elements issued to the output.
456 There are separate markup commands for different formal contexts: in
457 header position (just before a \isakeyword{theory} command), within
458 the theory body, or within a proof. Note that the header needs to
459 be treated specially, since ordinary theory and proof commands may
460 only occur \emph{after} the initial \isakeyword{theory}
465 \begin{tabular}{llll}
466 header & theory & proof & default meaning \\\hline
467 & \commdx{chapter} & & \verb,\chapter, \\
468 \commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\
469 & \commdx{subsection} & \commdx{subsect} & \verb,\subsection, \\
470 & \commdx{subsubsection} & \commdx{subsubsect} & \verb,\subsubsection, \\
475 From the Isabelle perspective, each markup command takes a single
476 text argument (delimited by \verb,",\dots\verb,", or
477 \verb,{,\verb,*,~\dots~\verb,*,\verb,},). After stripping any
478 surrounding white space, the argument is passed to a {\LaTeX} macro
479 \verb,\isamarkupXYZ, for any command \isakeyword{XYZ}. These macros
480 are defined in \verb,isabelle.sty, according to the meaning given in
481 the rightmost column above.
483 \medskip The following source fragment illustrates structure markup
484 of a theory. Note that {\LaTeX} labels may be included inside of
485 section headings as well.
488 header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
490 theory Foo_Bar = Main:
492 subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
500 subsection {\ttlbrace}* Derived rules *{\ttrbrace}
505 subsection {\ttlbrace}* Main theorem {\ttback}label{\ttlbrace}sec:main-theorem{\ttrbrace} *{\ttrbrace}
512 Users may occasionally want to change the meaning of markup
513 commands, say via \verb,\renewcommand, in \texttt{root.tex}. The
514 \verb,\isamarkupheader, is a good candidate for some adaption, e.g.\
515 moving it up in the hierarchy to become \verb,\chapter,.
518 \renewcommand{\isamarkupheader}[1]{\chapter{#1}}
521 \noindent Certainly, this requires to change the default
522 \verb,\documentclass{article}, in \texttt{root.tex} to something
523 that supports the notion of chapters in the first place, e.g.\
524 \verb,\documentclass{report},.
526 \medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to
527 hold the name of the current theory context. This is particularly
528 useful for document headings:
531 \renewcommand{\isamarkupheader}[1]
532 {\chapter{#1}\markright{THEORY~\isabellecontext}}
535 \noindent Make sure to include something like
536 \verb,\pagestyle{headings}, in \texttt{root.tex}; the document
537 should have more than 2 pages to show the effect.%
541 \isamarkupsubsection{Formal Comments and Antiquotations%
545 \begin{isamarkuptext}%
546 Comments of the form \verb,(,\verb,*,~\dots~\verb,*,\verb,),
552 \isamarkupsubsection{Symbols and Characters \label{sec:doc-prep-symbols}%
556 \begin{isamarkuptext}%
557 FIXME \verb,\isabellestyle,%
561 \isamarkupsubsection{Suppressing Output \label{sec:doc-prep-suppress}%
565 \begin{isamarkuptext}%
566 By default Isabelle's document system generates a {\LaTeX} source
567 file for each theory that happens to get loaded during the session.
568 The generated \texttt{session.tex} will include all of these in
569 order of appearance, which in turn gets included by the standard
570 \texttt{root.tex}. Certainly one may change the order of appearance
571 or suppress unwanted theories by ignoring \texttt{session.tex} and
572 include individual files in \texttt{root.tex} by hand. On the other
573 hand, such an arrangement requires additional maintenance chores
574 whenever the collection of theories changes.
576 Alternatively, one may tune the theory loading process in
577 \texttt{ROOT.ML} itself: traversal of the theory dependency graph
578 may be fine-tuned by adding further \verb,use_thy, invocations,
579 although topological sorting still has to be observed. Moreover,
580 the ML operator \verb,no_document, temporarily disables document
581 generation while executing a theory loader command; its usage is
585 no_document use_thy "A";
588 \medskip Theory output may be also suppressed in smaller portions as
589 well. For example, research papers or slides usually do not include
590 the formal content in full. In order to delimit \bfindex{ignored
591 material} special source comments
592 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
593 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), may be included in the
594 text. Only the document preparation system is affected, the formal
595 checking the theory is performed as before.
597 In the following example we suppress the slightly formalistic
598 \isakeyword{theory} + \isakeyword{end} surroundings a theory.
603 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
604 \texttt{theory A = Main:} \\
605 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
607 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
609 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
614 Text may be suppressed in a fine grained manner. For example, we
615 may even drop vital parts of a formal proof, pretending that things
616 have been simpler than in reality. For example, the following
617 ``fully automatic'' proof is actually a fake:%
620 \isacommand{lemma}\ {\isachardoublequote}x\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}int{\isacharparenright}\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isacharless}\ x\ {\isacharasterisk}\ x{\isachardoublequote}\isanewline
622 \isacommand{by}\ {\isacharparenleft}auto{\isacharparenright}\isamarkupfalse%
624 \begin{isamarkuptext}%
625 \noindent Here the real source of the proof has been as follows:
628 by (auto(*<*)simp add: int_less_le(*>*))
631 \medskip Ignoring portions of printed does demand some care by the
632 user. First of all, the writer is responsible not to obfuscate the
633 underlying formal development in an unduly manner. It is fairly
634 easy to invalidate the remaining visible text, e.g.\ by referencing
635 questionable formal items (strange definitions, arbitrary axioms
636 etc.) that have been hidden from sight beforehand.
638 Some minor technical subtleties of the
639 \verb,(,\verb,*,\verb,<,\verb,*,\verb,),-\verb,(,\verb,*,\verb,>,\verb,*,\verb,),
640 elements need to be kept in mind as well, since the system performs
641 little sanity checks here. Arguments of markup commands and formal
642 comments must not be hidden, otherwise presentation fails. Open and
643 close parentheses need to be inserted carefully; it is fairly easy
644 to hide the wrong parts, especially after rearranging the sources.
646 \medskip Authentic reports of formal theories, say as part of a
647 library, usually should refrain from suppressing parts of the text
648 at all. Other users may need the full information for their own
649 derivative work. If a particular formalization appears inadequate
650 for general public coverage, it is often more appropriate to think
651 of a better way in the first place.%
658 %%% TeX-master: "root"