11647
|
1 |
(*<*)
|
|
2 |
theory Documents = Main:
|
|
3 |
(*>*)
|
|
4 |
|
12648
|
5 |
section {* Concrete Syntax \label{sec:concrete-syntax} *}
|
12629
|
6 |
|
|
7 |
text {*
|
|
8 |
Concerning Isabelle's ``inner'' language of simply-typed @{text
|
|
9 |
\<lambda>}-calculus, the core concept of Isabelle's elaborate infrastructure
|
12645
|
10 |
for concrete syntax is that of general \bfindex{mixfix annotations}.
|
|
11 |
Associated with any kind of name and type declaration, mixfixes give
|
|
12 |
rise both to grammar productions for the parser and output templates
|
|
13 |
for the pretty printer.
|
12629
|
14 |
|
|
15 |
In full generality, the whole affair of parser and pretty printer
|
|
16 |
configuration is rather subtle. Any syntax specifications given by
|
|
17 |
end-users need to interact properly with the existing setup of
|
|
18 |
Isabelle/Pure and Isabelle/HOL; see \cite{isabelle-ref} for further
|
|
19 |
details. It is particularly important to get the precedence of new
|
|
20 |
syntactic constructs right, avoiding ambiguities with existing
|
|
21 |
elements.
|
|
22 |
|
|
23 |
\medskip Subsequently we introduce a few simple declaration forms
|
|
24 |
that already cover the most common situations fairly well.
|
|
25 |
*}
|
|
26 |
|
|
27 |
|
12648
|
28 |
subsection {* Infix Annotations *}
|
12629
|
29 |
|
|
30 |
text {*
|
|
31 |
Syntax annotations may be included wherever constants are declared
|
|
32 |
directly or indirectly, including \isacommand{consts},
|
|
33 |
\isacommand{constdefs}, or \isacommand{datatype} (for the
|
|
34 |
constructor operations). Type-constructors may be annotated as
|
|
35 |
well, although this is less frequently encountered in practice
|
|
36 |
(@{text "*"} and @{text "+"} types may come to mind).
|
|
37 |
|
12645
|
38 |
Infix declarations\index{infix annotations} provide a useful special
|
|
39 |
case of mixfixes, where users need not care about the full details
|
|
40 |
of priorities, nesting, spacing, etc. The subsequent example of the
|
|
41 |
exclusive-or operation on boolean values illustrates typical infix
|
|
42 |
declarations.
|
12629
|
43 |
*}
|
|
44 |
|
|
45 |
constdefs
|
|
46 |
xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "[+]" 60)
|
|
47 |
"A [+] B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
|
|
48 |
|
|
49 |
text {*
|
|
50 |
Any curried function with at least two arguments may be associated
|
|
51 |
with infix syntax: @{text "xor A B"} and @{text "A [+] B"} refer to
|
|
52 |
the same expression internally. In partial applications with less
|
|
53 |
than two operands there is a special notation with \isa{op} prefix:
|
|
54 |
@{text xor} without arguments is represented as @{text "op [+]"};
|
|
55 |
combined with plain prefix application this turns @{text "xor A"}
|
|
56 |
into @{text "op [+] A"}.
|
|
57 |
|
|
58 |
\medskip The string @{text [source] "[+]"} in the above declaration
|
|
59 |
refers to the bit of concrete syntax to represent the operator,
|
|
60 |
while the number @{text 60} determines the precedence of the whole
|
|
61 |
construct.
|
|
62 |
|
|
63 |
As it happens, Isabelle/HOL already spends many popular combinations
|
|
64 |
of ASCII symbols for its own use, including both @{text "+"} and
|
|
65 |
@{text "++"}. Slightly more awkward combinations like the present
|
|
66 |
@{text "[+]"} tend to be available for user extensions. The current
|
|
67 |
arrangement of inner syntax may be inspected via
|
|
68 |
\commdx{print\protect\_syntax}, albeit its output is enormous.
|
|
69 |
|
|
70 |
Operator precedence also needs some special considerations. The
|
|
71 |
admissible range is 0--1000. Very low or high priorities are
|
|
72 |
basically reserved for the meta-logic. Syntax of Isabelle/HOL
|
|
73 |
mainly uses the range of 10--100: the equality infix @{text "="} is
|
|
74 |
centered at 50, logical connectives (like @{text "\<or>"} and @{text
|
|
75 |
"\<and>"}) are below 50, and algebraic ones (like @{text "+"} and @{text
|
|
76 |
"*"}) above 50. User syntax should strive to coexist with common
|
|
77 |
HOL forms, or use the mostly unused range 100--900.
|
|
78 |
|
|
79 |
\medskip The keyword \isakeyword{infixl} specifies an operator that
|
|
80 |
is nested to the \emph{left}: in iterated applications the more
|
|
81 |
complex expression appears on the left-hand side: @{term "A [+] B
|
|
82 |
[+] C"} stands for @{text "(A [+] B) [+] C"}. Similarly,
|
12635
|
83 |
\isakeyword{infixr} refers to nesting to the \emph{right}, reading
|
|
84 |
@{term "A [+] B [+] C"} as @{text "A [+] (B [+] C)"}. In contrast,
|
|
85 |
a \emph{non-oriented} declaration via \isakeyword{infix} would
|
|
86 |
always demand explicit parentheses.
|
12648
|
87 |
|
12629
|
88 |
Many binary operations observe the associative law, so the exact
|
|
89 |
grouping does not matter. Nevertheless, formal statements need be
|
|
90 |
given in a particular format, associativity needs to be treated
|
|
91 |
explicitly within the logic. Exclusive-or is happens to be
|
|
92 |
associative, as shown below.
|
|
93 |
*}
|
|
94 |
|
|
95 |
lemma xor_assoc: "(A [+] B) [+] C = A [+] (B [+] C)"
|
|
96 |
by (auto simp add: xor_def)
|
|
97 |
|
|
98 |
text {*
|
|
99 |
Such rules may be used in simplification to regroup nested
|
|
100 |
expressions as required. Note that the system would actually print
|
|
101 |
the above statement as @{term "A [+] B [+] C = A [+] (B [+] C)"}
|
|
102 |
(due to nesting to the left). We have preferred to give the fully
|
12635
|
103 |
parenthesized form in the text for clarity. Only in rare situations
|
|
104 |
one may consider to force parentheses by use of non-oriented infix
|
|
105 |
syntax; equality would probably be a typical candidate.
|
12629
|
106 |
*}
|
|
107 |
|
12635
|
108 |
|
12648
|
109 |
subsection {* Mathematical Symbols \label{sec:thy-present-symbols} *}
|
12629
|
110 |
|
|
111 |
text {*
|
12635
|
112 |
Concrete syntax based on plain ASCII characters has its inherent
|
|
113 |
limitations. Rich mathematical notation demands a larger repertoire
|
|
114 |
of symbols. Several standards of extended character sets have been
|
|
115 |
proposed over decades, but none has become universally available so
|
|
116 |
far, not even Unicode\index{Unicode}.
|
|
117 |
|
12645
|
118 |
Isabelle supports a generic notion of \bfindex{symbols} as the
|
|
119 |
smallest entities of source text, without referring to internal
|
|
120 |
encodings. Such ``generalized characters'' may be of one of the
|
|
121 |
following three kinds:
|
12635
|
122 |
|
|
123 |
\begin{enumerate}
|
|
124 |
|
|
125 |
\item Traditional 7-bit ASCII characters.
|
|
126 |
|
|
127 |
\item Named symbols: \verb,\,\verb,<,$ident$\verb,>, (or
|
|
128 |
\verb,\\,\verb,<,$ident$\verb,>,).
|
12629
|
129 |
|
12635
|
130 |
\item Named control symbols: \verb,\,\verb,<^,$ident$\verb,>, (or
|
|
131 |
\verb,\\,\verb,<^,$ident$\verb,>,).
|
|
132 |
|
|
133 |
\end{enumerate}
|
|
134 |
|
|
135 |
Here $ident$ may be any identifier according to the usual Isabelle
|
|
136 |
conventions. This results in an infinite store of symbols, whose
|
|
137 |
interpretation is left to further front-end tools. For example, the
|
|
138 |
\verb,\,\verb,<forall>, symbol of Isabelle is really displayed as
|
|
139 |
$\forall$ --- both by the user-interface of Proof~General + X-Symbol
|
|
140 |
and the Isabelle document processor (see \S\ref{FIXME}).
|
|
141 |
|
|
142 |
A list of standard Isabelle symbols is given in
|
|
143 |
\cite[appendix~A]{isabelle-sys}. Users may introduce their own
|
|
144 |
interpretation of further symbols by configuring the appropriate
|
|
145 |
front-end tool accordingly, e.g.\ defining appropriate {\LaTeX}
|
|
146 |
macros for document preparation. There are also a few predefined
|
|
147 |
control symbols, such as \verb,\,\verb,<^sub>, and
|
|
148 |
\verb,\,\verb,<^sup>, for sub- and superscript of the subsequent
|
|
149 |
(printable) symbol, respectively.
|
|
150 |
|
|
151 |
\medskip The following version of our @{text xor} definition uses a
|
|
152 |
standard Isabelle symbol to achieve typographically pleasing output.
|
12629
|
153 |
*}
|
|
154 |
|
|
155 |
(*<*)
|
|
156 |
hide const xor
|
|
157 |
ML_setup {* Context.>> (Theory.add_path "1") *}
|
|
158 |
(*>*)
|
|
159 |
constdefs
|
|
160 |
xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "\<oplus>" 60)
|
|
161 |
"A \<oplus> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
|
12635
|
162 |
(*<*)
|
|
163 |
local
|
|
164 |
(*>*)
|
12629
|
165 |
|
12635
|
166 |
text {*
|
|
167 |
The X-Symbol package within Proof~General provides several input
|
|
168 |
methods to enter @{text \<oplus>} in the text. If all fails one may just
|
|
169 |
type \verb,\,\verb,<oplus>, by hand; the display is adapted
|
|
170 |
immediately after continuing further input.
|
|
171 |
|
|
172 |
\medskip A slightly more refined scheme is to provide alternative
|
12645
|
173 |
syntax via the \bfindex{print mode} concept of Isabelle (see also
|
|
174 |
\cite{isabelle-ref}). By convention, the mode ``$xsymbols$'' is
|
|
175 |
enabled whenever X-Symbol is active. Consider the following hybrid
|
|
176 |
declaration of @{text xor}.
|
12635
|
177 |
*}
|
|
178 |
|
|
179 |
(*<*)
|
|
180 |
hide const xor
|
|
181 |
ML_setup {* Context.>> (Theory.add_path "2") *}
|
|
182 |
(*>*)
|
|
183 |
constdefs
|
|
184 |
xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "[+]\<ignore>" 60)
|
|
185 |
"A [+]\<ignore> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
|
|
186 |
|
|
187 |
syntax (xsymbols)
|
|
188 |
xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "\<oplus>\<ignore>" 60)
|
12629
|
189 |
(*<*)
|
|
190 |
local
|
|
191 |
(*>*)
|
|
192 |
|
12635
|
193 |
text {*
|
|
194 |
Here the \commdx{syntax} command acts like \isakeyword{consts}, but
|
|
195 |
without declaring a logical constant, and with an optional print
|
|
196 |
mode specification. Note that the type declaration given here
|
|
197 |
merely serves for syntactic purposes, and is not checked for
|
|
198 |
consistency with the real constant.
|
|
199 |
|
|
200 |
\medskip Now we may write either @{text "[+]"} or @{text "\<oplus>"} in
|
|
201 |
input, while output uses the nicer syntax of $xsymbols$, provided
|
|
202 |
that print mode is presently active. This scheme is particularly
|
|
203 |
useful for interactive development, with the user typing plain ASCII
|
|
204 |
text, but gaining improved visual feedback from the system (say in
|
|
205 |
current goal output).
|
|
206 |
|
|
207 |
\begin{warn}
|
|
208 |
Using alternative syntax declarations easily results in varying
|
|
209 |
versions of input sources. Isabelle provides no systematic way to
|
|
210 |
convert alternative expressions back and forth. Print modes only
|
|
211 |
affect situations where formal entities are pretty printed by the
|
|
212 |
Isabelle process (e.g.\ output of terms and types), but not the
|
|
213 |
original theory text.
|
|
214 |
\end{warn}
|
|
215 |
|
|
216 |
\medskip The following variant makes the alternative @{text \<oplus>}
|
|
217 |
notation only available for output. Thus we may enforce input
|
|
218 |
sources to refer to plain ASCII only.
|
|
219 |
*}
|
|
220 |
|
|
221 |
syntax (xsymbols output)
|
|
222 |
xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "\<oplus>\<ignore>" 60)
|
|
223 |
|
12629
|
224 |
|
12648
|
225 |
subsection {* Prefix Annotations *}
|
12629
|
226 |
|
|
227 |
text {*
|
12645
|
228 |
Prefix syntax annotations\index{prefix annotation} are just a very
|
|
229 |
degenerate of the general mixfix form \cite{isabelle-ref}, without
|
|
230 |
any template arguments or priorities --- just some piece of literal
|
|
231 |
syntax.
|
12635
|
232 |
|
|
233 |
The following example illustrates this idea idea by associating
|
|
234 |
common symbols with the constructors of a currency datatype.
|
12629
|
235 |
*}
|
|
236 |
|
|
237 |
datatype currency =
|
|
238 |
Euro nat ("\<euro>")
|
|
239 |
| Pounds nat ("\<pounds>")
|
|
240 |
| Yen nat ("\<yen>")
|
|
241 |
| Dollar nat ("$")
|
|
242 |
|
|
243 |
text {*
|
12635
|
244 |
Here the degenerate mixfix annotations on the rightmost column
|
|
245 |
happen to consist of a single Isabelle symbol each:
|
|
246 |
\verb,\,\verb,<euro>,, \verb,\,\verb,<pounds>,,
|
12645
|
247 |
\verb,\,\verb,<yen>,, \verb,$,.
|
12635
|
248 |
|
|
249 |
Recall that a constructor like @{text Euro} actually is a function
|
|
250 |
@{typ "nat \<Rightarrow> currency"}. An expression like @{text "Euro 10"} will
|
12645
|
251 |
be printed as @{term "\<euro> 10"}. Only the head of the application is
|
|
252 |
subject to our concrete syntax; this simple form already achieves
|
|
253 |
conformance with notational standards of the European Commission.
|
12629
|
254 |
|
12635
|
255 |
\medskip Certainly, the same idea of prefix syntax also works for
|
|
256 |
\isakeyword{consts}, \isakeyword{constdefs} etc. For example, we
|
|
257 |
might introduce a (slightly unrealistic) function to calculate an
|
|
258 |
abstract currency value, by cases on the datatype constructors and
|
12645
|
259 |
fixed exchange rates. The funny symbol used here is that of
|
|
260 |
\verb,\<currency>,.
|
12635
|
261 |
*}
|
|
262 |
|
|
263 |
consts
|
|
264 |
currency :: "currency \<Rightarrow> nat" ("\<currency>")
|
|
265 |
|
12629
|
266 |
|
12648
|
267 |
subsection {* Syntax Translations \label{sec:def-translations} *}
|
12629
|
268 |
|
|
269 |
text{*
|
|
270 |
FIXME
|
|
271 |
|
|
272 |
\index{syntax translations|(}%
|
|
273 |
\index{translations@\isacommand {translations} (command)|(}
|
|
274 |
Isabelle offers an additional definitional facility,
|
|
275 |
\textbf{syntax translations}.
|
|
276 |
They resemble macros: upon parsing, the defined concept is immediately
|
|
277 |
replaced by its definition. This effect is reversed upon printing. For example,
|
|
278 |
the symbol @{text"\<noteq>"} is defined via a syntax translation:
|
|
279 |
*}
|
|
280 |
|
|
281 |
translations "x \<noteq> y" \<rightleftharpoons> "\<not>(x = y)"
|
|
282 |
|
|
283 |
text{*\index{$IsaEqTrans@\isasymrightleftharpoons}
|
|
284 |
\noindent
|
|
285 |
Internally, @{text"\<noteq>"} never appears.
|
|
286 |
|
|
287 |
In addition to @{text"\<rightleftharpoons>"} there are
|
|
288 |
@{text"\<rightharpoonup>"}\index{$IsaEqTrans1@\isasymrightharpoonup}
|
|
289 |
and @{text"\<leftharpoondown>"}\index{$IsaEqTrans2@\isasymleftharpoondown}
|
|
290 |
for uni-directional translations, which only affect
|
|
291 |
parsing or printing. This tutorial will not cover the details of
|
|
292 |
translations. We have mentioned the concept merely because it
|
|
293 |
crops up occasionally; a number of HOL's built-in constructs are defined
|
12648
|
294 |
via translations. Translations are preferable to definitions when the new
|
12629
|
295 |
concept is a trivial variation on an existing one. For example, we
|
|
296 |
don't need to derive new theorems about @{text"\<noteq>"}, since existing theorems
|
|
297 |
about @{text"="} still apply.%
|
|
298 |
\index{syntax translations|)}%
|
|
299 |
\index{translations@\isacommand {translations} (command)|)}
|
|
300 |
*}
|
|
301 |
|
|
302 |
|
12648
|
303 |
section {* Document Preparation *}
|
12629
|
304 |
|
12645
|
305 |
text {*
|
|
306 |
Isabelle/Isar is centered around a certain notion of \bfindex{formal
|
|
307 |
proof documents}\index{documents|bold}: ultimately the result of the
|
|
308 |
user's theory development efforts is a human-readable record --- as
|
|
309 |
a browsable PDF file or printed on paper. The overall document
|
|
310 |
structure follows traditional mathematical articles, with
|
|
311 |
sectioning, explanations, definitions, theorem statements, and
|
|
312 |
proofs.
|
12629
|
313 |
|
12645
|
314 |
The Isar proof language \cite{Wenzel-PhD}, which is not covered in
|
|
315 |
this book, admits to write formal proof texts that are acceptable
|
|
316 |
both to the machine and human readers at the same time. Thus
|
|
317 |
marginal comments and explanations may be kept at a minimum.
|
|
318 |
Nevertheless, Isabelle document output is still useful without
|
|
319 |
actual Isar proof texts; formal specifications usually deserve their
|
|
320 |
own coverage in the text, while unstructured proof scripts may be
|
|
321 |
just ignore by readers (or intentionally suppressed from the text).
|
12629
|
322 |
|
12645
|
323 |
\medskip The Isabelle document preparation system essentially acts
|
|
324 |
like a formal front-end for {\LaTeX}. After checking definitions
|
|
325 |
and proofs the theory sources are turned into typesetting
|
|
326 |
instructions, so the final document is known to observe quite strong
|
|
327 |
``soundness'' properties. This enables users to write authentic
|
|
328 |
reports on formal theory developments with little additional effort,
|
|
329 |
the most tedious consistency checks are handled by the system.
|
|
330 |
*}
|
|
331 |
|
|
332 |
|
12648
|
333 |
subsection {* Isabelle Sessions *}
|
12629
|
334 |
|
|
335 |
text {*
|
12645
|
336 |
In contrast to the highly interactive mode of the formal parts of
|
|
337 |
Isabelle/Isar theory development, the document preparation stage
|
|
338 |
essentially works in batch-mode. This revolves around the concept
|
|
339 |
of a \bfindex{session}, which essentially consists of a collection
|
|
340 |
of theory source files that contribute to a single output document.
|
|
341 |
Each session is derived from a parent one (usually an object-logic
|
|
342 |
image such as \texttt{HOL}); this results in an overall tree
|
|
343 |
structure of Isabelle sessions.
|
|
344 |
|
|
345 |
The canonical arrangement of source files of a session called
|
|
346 |
\texttt{MySession} is as follows:
|
|
347 |
|
|
348 |
\begin{itemize}
|
|
349 |
|
|
350 |
\item Directory \texttt{MySession} contains the required theory
|
|
351 |
files, say $A@1$\texttt{.thy}, \dots, $A@n$\texttt{.thy}.
|
|
352 |
|
|
353 |
\item File \texttt{MySession/ROOT.ML} holds appropriate ML commands
|
|
354 |
for loading all wanted theories, usually just
|
|
355 |
\texttt{use_thy~"$A@i$"} for any $A@i$ in leaf position of the
|
|
356 |
theory dependency graph.
|
|
357 |
|
|
358 |
\item Directory \texttt{MySession/document} contains everything
|
|
359 |
required for the {\LaTeX} stage, but only \texttt{root.tex} needs to
|
|
360 |
be provided initially. The latter file holds appropriate {\LaTeX}
|
|
361 |
code to commence a document (\verb,\documentclass, etc.), and to
|
|
362 |
include the generated files $A@i$\texttt{.tex} for each theory. The
|
|
363 |
generated file \texttt{session.tex} holds {\LaTeX} commands to
|
|
364 |
include \emph{all} theory output files in topologically sorted
|
|
365 |
order.
|
|
366 |
|
|
367 |
\item In addition an \texttt{IsaMakefile} outside of directory
|
|
368 |
\texttt{MySession} holds appropriate dependencies and invocations of
|
|
369 |
Isabelle tools to control the batch job. The details are covered in
|
|
370 |
\cite{isabelle-sys}; \texttt{isatool usedir} is the most important
|
|
371 |
entry point.
|
|
372 |
|
|
373 |
\end{itemize}
|
|
374 |
|
|
375 |
With everything put in its proper place, \texttt{isatool make}
|
|
376 |
should be sufficient to process the Isabelle session completely,
|
|
377 |
with the generated document appearing in its proper place (within
|
|
378 |
\verb,~/isabelle/browser_info,).
|
|
379 |
|
12648
|
380 |
In practice, users may want to have \texttt{isatool mkdir} generate
|
12645
|
381 |
an initial working setup without further ado. For example, an empty
|
|
382 |
session \texttt{MySession} derived from \texttt{HOL} may be produced
|
|
383 |
as follows:
|
|
384 |
|
|
385 |
\begin{verbatim}
|
|
386 |
isatool mkdir HOL MySession
|
|
387 |
isatool make
|
|
388 |
\end{verbatim}
|
|
389 |
|
|
390 |
This runs the session with sensible default options, including
|
|
391 |
verbose mode to tell the user where the result will appear. The
|
|
392 |
above dry run should produce should produce a single page of output
|
|
393 |
(with a dummy title, empty table of contents etc.). Any failure at
|
|
394 |
that stage is likely to indicate some technical problems with your
|
|
395 |
{\LaTeX} installation.\footnote{Especially make sure that
|
|
396 |
\texttt{pdflatex} is present.}
|
|
397 |
|
|
398 |
\medskip Users may now start to populate the directory
|
|
399 |
\texttt{MySession}, and the file \texttt{MySession/ROOT.ML}
|
|
400 |
accordingly. \texttt{MySession/document/root.tex} should be also
|
|
401 |
adapted at some point; the generated version is mostly
|
12648
|
402 |
self-explanatory. The default versions includes the
|
|
403 |
\texttt{isabelle} (mandatory) and \texttt{isabellesym} (required for
|
|
404 |
mathematical symbols); further packages may required, e.g.\ for
|
|
405 |
unusual Isabelle symbols.
|
12645
|
406 |
|
|
407 |
Realistic applications may demand additional files in
|
|
408 |
\texttt{MySession/document} for the {\LaTeX} stage, such as
|
|
409 |
\texttt{root.bib} for the bibliographic database.\footnote{Using
|
|
410 |
that particular name of \texttt{root.bib}, the Isabelle document
|
|
411 |
processor (actually \texttt{isatool document} \cite{isabelle-sys})
|
|
412 |
will be smart enough to invoke \texttt{bibtex} accordingly.}
|
|
413 |
|
|
414 |
\medskip Failure of the document preparation phase in an Isabelle
|
|
415 |
batch session leaves the generated sources in there target location
|
|
416 |
(as pointed out by the accompanied error message). In case of
|
|
417 |
{\LaTeX} errors, users may trace error messages at the file position
|
|
418 |
of the generated text.
|
|
419 |
*}
|
|
420 |
|
|
421 |
|
12648
|
422 |
subsection {* Structure Markup *}
|
12645
|
423 |
|
|
424 |
subsubsection {* Sections *}
|
|
425 |
|
|
426 |
text {*
|
12648
|
427 |
FIXME \verb,\label, within sections;
|
|
428 |
|
12645
|
429 |
The large-scale structure of Isabelle documents closely follows
|
|
430 |
{\LaTeX} convention, with chapters, sections, subsubsections etc.
|
|
431 |
The formal Isar language includes separate structure \bfindex{markup
|
|
432 |
commands}, which do not effect the formal content of a theory (or
|
|
433 |
proof), but results in corresponding {\LaTeX} elements issued to the
|
|
434 |
output.
|
12629
|
435 |
|
12645
|
436 |
There are different markup commands for different formal contexts:
|
|
437 |
in header position (just before a \isakeyword{theory} command),
|
|
438 |
within the theory body, or within a proof. Note that the header
|
|
439 |
needs to be treated specially, since ordinary theory and proof
|
|
440 |
commands may only occur \emph{after} the initial \isakeyword{theory}
|
|
441 |
specification.
|
|
442 |
|
|
443 |
\smallskip
|
|
444 |
|
|
445 |
\begin{tabular}{llll}
|
|
446 |
header & theory & proof & default meaning \\\hline
|
|
447 |
& \commdx{chapter} & & \verb,\chapter, \\
|
|
448 |
\commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\
|
|
449 |
& \commdx{subsection} & \commdx{subsect} & \verb,\subsection, \\
|
|
450 |
& \commdx{subsubsection} & \commdx{subsubsect} & \verb,\subsubsection, \\
|
|
451 |
\end{tabular}
|
|
452 |
|
|
453 |
\medskip
|
|
454 |
|
|
455 |
From the Isabelle perspective, each markup command takes a single
|
|
456 |
text argument (delimited by \verb,",\dots\verb,", or
|
|
457 |
\verb,{,\verb,*,~\dots~\verb,*,\verb,},). After stripping
|
|
458 |
surrounding white space, the argument is passed to a {\LaTeX} macro
|
|
459 |
\verb,\isamarkupXXX, for any command \isakeyword{XXX}. The latter
|
|
460 |
are defined in \verb,isabelle.sty, according to the rightmost column
|
|
461 |
above.
|
|
462 |
|
|
463 |
\medskip The following source fragment illustrates structure markup
|
12648
|
464 |
of a theory. Note that {\LaTeX} labels may well be included inside
|
|
465 |
of section headings as well.
|
12645
|
466 |
|
|
467 |
\begin{ttbox}
|
|
468 |
header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
|
|
469 |
|
|
470 |
theory Foo_Bar = Main:
|
|
471 |
|
|
472 |
subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
|
|
473 |
|
|
474 |
consts
|
|
475 |
foo :: \dots
|
|
476 |
bar :: \dots
|
12648
|
477 |
|
12645
|
478 |
defs \dots
|
12648
|
479 |
|
12645
|
480 |
subsection {\ttlbrace}* Derived rules *{\ttrbrace}
|
|
481 |
|
|
482 |
lemma fooI: \dots
|
|
483 |
lemma fooE: \dots
|
|
484 |
|
12648
|
485 |
subsection {\ttlbrace}* Main theorem {\ttback}label{\ttlbrace}sec:main-theorem{\ttrbrace} *{\ttrbrace}
|
12645
|
486 |
|
|
487 |
theorem main: \dots
|
|
488 |
|
|
489 |
end
|
|
490 |
\end{ttbox}
|
|
491 |
|
12648
|
492 |
Users may occasionally want to change the meaning of some markup
|
|
493 |
commands, typically via appropriate use of \verb,\renewcommand, in
|
|
494 |
\texttt{root.tex}. The \verb,\isamarkupheader, is a good candidate
|
|
495 |
for some adaption, e.g.\ moving it up in the hierarchy to become
|
|
496 |
\verb,\chapter,.
|
12645
|
497 |
|
|
498 |
\begin{verbatim}
|
|
499 |
\renewcommand{\isamarkupheader}[1]{\chapter{#1}}
|
|
500 |
\end{verbatim}
|
|
501 |
|
|
502 |
Certainly, this requires to change the default
|
|
503 |
\verb,\documentclass{article}, in \texttt{root.tex} to something
|
|
504 |
that supports the notion of chapters in the first place, e.g.\
|
12648
|
505 |
\verb,\documentclass{report},.
|
12645
|
506 |
|
12648
|
507 |
\medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to
|
|
508 |
hold the name of the current theory context. This is particularly
|
|
509 |
useful for document headings or footings, e.g.\ like this:
|
12645
|
510 |
|
|
511 |
\begin{verbatim}
|
|
512 |
\renewcommand{\isamarkupheader}[1]%
|
|
513 |
{\chapter{#1}\markright{THEORY~\isabellecontext}}
|
|
514 |
\end{verbatim}
|
|
515 |
|
|
516 |
\noindent Make sure to include something like
|
12648
|
517 |
\verb,\pagestyle{headings}, in \texttt{root.tex}; the document
|
|
518 |
should have more than 2 pages to show the effect.
|
12645
|
519 |
*}
|
|
520 |
|
|
521 |
|
12648
|
522 |
subsection {* Formal Comments and Antiquotations *}
|
12645
|
523 |
|
|
524 |
text {*
|
12648
|
525 |
Comments of the form \verb,(,\verb,*,~\dots~\verb,*,\verb,),
|
12645
|
526 |
|
|
527 |
*}
|
|
528 |
|
|
529 |
|
12648
|
530 |
subsection {* Symbols and Characters *}
|
12645
|
531 |
|
|
532 |
text {*
|
|
533 |
FIXME \verb,\isabellestyle,
|
|
534 |
*}
|
|
535 |
|
|
536 |
|
12648
|
537 |
subsection {* Suppressing Output *}
|
12645
|
538 |
|
|
539 |
text {*
|
12648
|
540 |
By default Isabelle's document system generates a {\LaTeX} source
|
|
541 |
file for each theory that happens to get loaded during the session.
|
|
542 |
The generated \texttt{session.tex} file will include all of these in
|
|
543 |
order of appearance, which in turn gets included by the standard
|
|
544 |
\texttt{root.tex} file. Certainly one may change the order of
|
|
545 |
appearance or suppress unwanted theories by ignoring
|
|
546 |
\texttt{session.tex} and include individual files in
|
|
547 |
\texttt{root.tex} by hand. On the other hand, such an arrangement
|
|
548 |
requires additional efforts for maintenance.
|
|
549 |
|
|
550 |
Alternatively, one may tune the theory loading process in
|
|
551 |
\texttt{ROOT.ML}: traversal of the theory dependency graph may be
|
|
552 |
fine-tuned by adding further \verb,use_thy, invocations, although
|
|
553 |
topological sorting needs to be preserved. Moreover, the ML
|
|
554 |
operator \verb,no_document, temporarily disables document generation
|
|
555 |
while executing a theory loader command; the usage is like this:
|
|
556 |
|
|
557 |
\begin{verbatim}
|
|
558 |
no_document use_thy "Aux";
|
|
559 |
\end{verbatim}
|
12645
|
560 |
|
12648
|
561 |
Theory output may be also suppressed \emph{partially} as well.
|
|
562 |
Typical applications include research papers or slides based on
|
|
563 |
formal developments --- these usually do not show the full formal
|
|
564 |
content. The special source comments
|
|
565 |
\verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
|
|
566 |
\verb,(,\verb,*,\verb,>,\verb,*,\verb,), are interpreted by the
|
|
567 |
document generator as open and close parenthesis for
|
|
568 |
\bfindex{ignored material}. Any text inside of (potentially nested)
|
|
569 |
\verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\dots~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),
|
|
570 |
parentheses is just ignored from the output --- after correct formal
|
|
571 |
checking.
|
|
572 |
|
|
573 |
In the following example we suppress the slightly formalistic
|
|
574 |
\isakeyword{theory} and \isakeyword{end} part of a theory text.
|
|
575 |
|
|
576 |
\medskip
|
|
577 |
|
|
578 |
\begin{tabular}{l}
|
|
579 |
\verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
|
|
580 |
\texttt{theory A = Main:} \\
|
|
581 |
\verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
|
|
582 |
~~$\vdots$ \\
|
|
583 |
\verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
|
|
584 |
\texttt{end} \\
|
|
585 |
\verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
|
|
586 |
\end{tabular}
|
|
587 |
|
|
588 |
\medskip
|
|
589 |
|
|
590 |
Ignoring portions of printed text like this demands some special
|
|
591 |
care. FIXME
|
12629
|
592 |
*}
|
|
593 |
|
11647
|
594 |
(*<*)
|
|
595 |
end
|
|
596 |
(*>*)
|