11647
|
1 |
(*<*)
|
|
2 |
theory Documents = Main:
|
|
3 |
(*>*)
|
|
4 |
|
12648
|
5 |
section {* Concrete Syntax \label{sec:concrete-syntax} *}
|
12629
|
6 |
|
|
7 |
text {*
|
12766
|
8 |
The core concept of Isabelle's framework for concrete syntax is that
|
|
9 |
of \bfindex{mixfix annotations}. Associated with any kind of
|
|
10 |
constant declaration, mixfixes affect both the grammar productions
|
|
11 |
for the parser and output templates for the pretty printer.
|
12629
|
12 |
|
12743
|
13 |
In full generality, parser and pretty printer configuration is a
|
12766
|
14 |
subtle affair \cite{isabelle-ref}. Your syntax specifications need
|
|
15 |
to interact properly with the existing setup of Isabelle/Pure and
|
|
16 |
Isabelle/HOL\@. To avoid creating ambiguities with existing
|
|
17 |
elements, it is particularly important to give new syntactic
|
12764
|
18 |
constructs the right precedence.
|
12629
|
19 |
|
12670
|
20 |
\medskip Subsequently we introduce a few simple syntax declaration
|
12743
|
21 |
forms that already cover many common situations fairly well.
|
12629
|
22 |
*}
|
|
23 |
|
|
24 |
|
12648
|
25 |
subsection {* Infix Annotations *}
|
12629
|
26 |
|
|
27 |
text {*
|
12764
|
28 |
Syntax annotations may be included wherever constants are declared,
|
12766
|
29 |
such as \isacommand{consts} and \isacommand{constdefs} --- and also
|
|
30 |
\isacommand{datatype}, which declares constructor operations.
|
|
31 |
Type-constructors may be annotated as well, although this is less
|
|
32 |
frequently encountered in practice (the infix type @{text "\<times>"} comes
|
|
33 |
to mind).
|
12629
|
34 |
|
12645
|
35 |
Infix declarations\index{infix annotations} provide a useful special
|
12766
|
36 |
case of mixfixes. The following example of the exclusive-or
|
|
37 |
operation on boolean values illustrates typical infix declarations.
|
12629
|
38 |
*}
|
|
39 |
|
|
40 |
constdefs
|
|
41 |
xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "[+]" 60)
|
|
42 |
"A [+] B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
|
|
43 |
|
|
44 |
text {*
|
12653
|
45 |
\noindent Now @{text "xor A B"} and @{text "A [+] B"} refer to the
|
|
46 |
same expression internally. Any curried function with at least two
|
12766
|
47 |
arguments may be given infix syntax. For partial applications with
|
|
48 |
fewer than two operands, there is a notation using the prefix~@{text
|
|
49 |
op}. For instance, @{text xor} without arguments is represented as
|
|
50 |
@{text "op [+]"}; together with ordinary function application, this
|
12653
|
51 |
turns @{text "xor A"} into @{text "op [+] A"}.
|
12629
|
52 |
|
12746
|
53 |
\medskip The keyword \isakeyword{infixl} seen above specifies an
|
|
54 |
infix operator that is nested to the \emph{left}: in iterated
|
|
55 |
applications the more complex expression appears on the left-hand
|
12766
|
56 |
side, and @{term "A [+] B [+] C"} stands for @{text "(A [+] B) [+]
|
|
57 |
C"}. Similarly, \isakeyword{infixr} means nesting to the
|
12746
|
58 |
\emph{right}, reading @{term "A [+] B [+] C"} as @{text "A [+] (B
|
12766
|
59 |
[+] C)"}. A \emph{non-oriented} declaration via \isakeyword{infix}
|
|
60 |
would render @{term "A [+] B [+] C"} illegal, but demand explicit
|
|
61 |
parentheses to indicate the intended grouping.
|
12743
|
62 |
|
12746
|
63 |
The string @{text [source] "[+]"} in our annotation refers to the
|
|
64 |
concrete syntax to represent the operator (a literal token), while
|
12764
|
65 |
the number @{text 60} determines the precedence of the construct:
|
12766
|
66 |
the syntactic priorities of the arguments and result. Isabelle/HOL
|
|
67 |
already uses up many popular combinations of ASCII symbols for its
|
|
68 |
own use, including both @{text "+"} and @{text "++"}. Longer
|
|
69 |
character combinations are more likely to be still available for
|
|
70 |
user extensions, such as our~@{text "[+]"}.
|
12629
|
71 |
|
12766
|
72 |
Operator precedences have a range of 0--1000. Very low or high
|
|
73 |
priorities are reserved for the meta-logic. HOL syntax mainly uses
|
|
74 |
the range of 10--100: the equality infix @{text "="} is centered at
|
|
75 |
50; logical connectives (like @{text "\<or>"} and @{text "\<and>"}) are
|
|
76 |
below 50; algebraic ones (like @{text "+"} and @{text "*"}) are
|
|
77 |
above 50. User syntax should strive to coexist with common HOL
|
|
78 |
forms, or use the mostly unused range 100--900.
|
12629
|
79 |
*}
|
|
80 |
|
12635
|
81 |
|
12659
|
82 |
subsection {* Mathematical Symbols \label{sec:syntax-symbols} *}
|
12629
|
83 |
|
|
84 |
text {*
|
12766
|
85 |
Concrete syntax based on ASCII characters has inherent limitations.
|
|
86 |
Mathematical notation demands a larger repertoire of glyphs.
|
|
87 |
Several standards of extended character sets have been proposed over
|
|
88 |
decades, but none has become universally available so far. Isabelle
|
|
89 |
has its own notion of \bfindex{symbols} as the smallest entities of
|
|
90 |
source text, without referring to internal encodings. There are
|
|
91 |
three kinds of such ``generalized characters'':
|
12635
|
92 |
|
|
93 |
\begin{enumerate}
|
|
94 |
|
12653
|
95 |
\item 7-bit ASCII characters
|
12635
|
96 |
|
12653
|
97 |
\item named symbols: \verb,\,\verb,<,$ident$\verb,>,
|
12629
|
98 |
|
12653
|
99 |
\item named control symbols: \verb,\,\verb,<^,$ident$\verb,>,
|
12635
|
100 |
|
|
101 |
\end{enumerate}
|
|
102 |
|
|
103 |
Here $ident$ may be any identifier according to the usual Isabelle
|
|
104 |
conventions. This results in an infinite store of symbols, whose
|
12766
|
105 |
interpretation is left to further front-end tools. For example, the
|
|
106 |
user-interface of Proof~General + X-Symbol and the Isabelle document
|
|
107 |
processor (see \S\ref{sec:document-preparation}) display the
|
|
108 |
\verb,\,\verb,<forall>, symbol as~@{text \<forall>}.
|
12635
|
109 |
|
|
110 |
A list of standard Isabelle symbols is given in
|
12766
|
111 |
\cite[appendix~A]{isabelle-sys}. You may introduce your own
|
12635
|
112 |
interpretation of further symbols by configuring the appropriate
|
12653
|
113 |
front-end tool accordingly, e.g.\ by defining certain {\LaTeX}
|
|
114 |
macros (see also \S\ref{sec:doc-prep-symbols}). There are also a
|
|
115 |
few predefined control symbols, such as \verb,\,\verb,<^sub>, and
|
12635
|
116 |
\verb,\,\verb,<^sup>, for sub- and superscript of the subsequent
|
12764
|
117 |
printable symbol, respectively. For example, \verb,A\<^sup>\<star>, is
|
12670
|
118 |
output as @{text "A\<^sup>\<star>"}.
|
12635
|
119 |
|
12766
|
120 |
\medskip Replacing our definition of @{text xor} by the following
|
12764
|
121 |
specifies a Isabelle symbol for the new operator:
|
12629
|
122 |
*}
|
|
123 |
|
|
124 |
(*<*)
|
|
125 |
hide const xor
|
12665
|
126 |
ML_setup {* Context.>> (Theory.add_path "version1") *}
|
12629
|
127 |
(*>*)
|
|
128 |
constdefs
|
|
129 |
xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "\<oplus>" 60)
|
|
130 |
"A \<oplus> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
|
12635
|
131 |
(*<*)
|
|
132 |
local
|
|
133 |
(*>*)
|
12629
|
134 |
|
12635
|
135 |
text {*
|
12653
|
136 |
\noindent The X-Symbol package within Proof~General provides several
|
|
137 |
input methods to enter @{text \<oplus>} in the text. If all fails one may
|
12766
|
138 |
just type a named entity \verb,\,\verb,<oplus>, by hand; the
|
|
139 |
corresponding symbol will be displayed after further input.
|
12635
|
140 |
|
12766
|
141 |
\medskip More flexible is to provide alternative syntax forms
|
|
142 |
through the \bfindex{print mode} concept~\cite{isabelle-ref}. By
|
|
143 |
convention, the mode of ``$xsymbols$'' is enabled whenever
|
|
144 |
Proof~General's X-Symbol mode or {\LaTeX} output is active. Now
|
|
145 |
consider the following hybrid declaration of @{text xor}:
|
12635
|
146 |
*}
|
|
147 |
|
|
148 |
(*<*)
|
|
149 |
hide const xor
|
12665
|
150 |
ML_setup {* Context.>> (Theory.add_path "version2") *}
|
12635
|
151 |
(*>*)
|
|
152 |
constdefs
|
|
153 |
xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "[+]\<ignore>" 60)
|
|
154 |
"A [+]\<ignore> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
|
|
155 |
|
|
156 |
syntax (xsymbols)
|
|
157 |
xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "\<oplus>\<ignore>" 60)
|
12629
|
158 |
(*<*)
|
|
159 |
local
|
|
160 |
(*>*)
|
|
161 |
|
12635
|
162 |
text {*
|
12653
|
163 |
The \commdx{syntax} command introduced here acts like
|
12743
|
164 |
\isakeyword{consts}, but without declaring a logical constant. The
|
12746
|
165 |
print mode specification of \isakeyword{syntax}, here @{text
|
|
166 |
"(xsymbols)"}, is optional. Also note that its type merely serves
|
|
167 |
for syntactic purposes, and is \emph{not} checked for consistency
|
|
168 |
with the real constant.
|
12635
|
169 |
|
12672
|
170 |
\medskip We may now write @{text "A [+] B"} or @{text "A \<oplus> B"} in
|
12766
|
171 |
input, while output uses the nicer syntax of $xsymbols$ whenever
|
12672
|
172 |
that print mode is active. Such an arrangement is particularly
|
12766
|
173 |
useful for interactive development, where users may type ASCII text
|
|
174 |
and see mathematical symbols displayed during proofs.
|
12635
|
175 |
*}
|
|
176 |
|
12629
|
177 |
|
12648
|
178 |
subsection {* Prefix Annotations *}
|
12629
|
179 |
|
|
180 |
text {*
|
12766
|
181 |
Prefix syntax annotations\index{prefix annotation} are another form
|
|
182 |
of mixfixes \cite{isabelle-ref}, without any template arguments or
|
|
183 |
priorities --- just some literal syntax. The following example
|
|
184 |
associates common symbols with the constructors of a datatype.
|
12629
|
185 |
*}
|
|
186 |
|
|
187 |
datatype currency =
|
|
188 |
Euro nat ("\<euro>")
|
|
189 |
| Pounds nat ("\<pounds>")
|
|
190 |
| Yen nat ("\<yen>")
|
|
191 |
| Dollar nat ("$")
|
|
192 |
|
|
193 |
text {*
|
12653
|
194 |
\noindent Here the mixfix annotations on the rightmost column happen
|
|
195 |
to consist of a single Isabelle symbol each: \verb,\,\verb,<euro>,,
|
|
196 |
\verb,\,\verb,<pounds>,, \verb,\,\verb,<yen>,, and \verb,$,. Recall
|
|
197 |
that a constructor like @{text Euro} actually is a function @{typ
|
12746
|
198 |
"nat \<Rightarrow> currency"}. The expression @{text "Euro 10"} will be
|
12653
|
199 |
printed as @{term "\<euro> 10"}; only the head of the application is
|
12743
|
200 |
subject to our concrete syntax. This rather simple form already
|
|
201 |
achieves conformance with notational standards of the European
|
|
202 |
Commission.
|
12629
|
203 |
|
12766
|
204 |
Prefix syntax works the same way for \isakeyword{consts} or
|
12764
|
205 |
\isakeyword{constdefs}.
|
12651
|
206 |
*}
|
|
207 |
|
|
208 |
|
|
209 |
subsection {* Syntax Translations \label{sec:syntax-translations} *}
|
|
210 |
|
|
211 |
text{*
|
12766
|
212 |
Mixfix syntax annotations merely decorate particular constant
|
|
213 |
application forms with concrete syntax, for instance replacing \
|
|
214 |
@{text "xor A B"} by @{text "A \<oplus> B"}. Occasionally, the
|
|
215 |
relationship between some piece of notation and its internal form is
|
|
216 |
more complicated. Here we need \bfindex{syntax translations}.
|
12651
|
217 |
|
12764
|
218 |
Using the \isakeyword{syntax}\index{syntax (command)}, command we
|
|
219 |
introduce uninterpreted notational elements. Then
|
|
220 |
\commdx{translations} relate input forms to complex logical
|
12766
|
221 |
expressions. This provides a simple mechanism for syntactic macros;
|
|
222 |
even heavier transformations may be written in ML
|
12670
|
223 |
\cite{isabelle-ref}.
|
12651
|
224 |
|
12764
|
225 |
\medskip A typical use of syntax translations is to introduce
|
12766
|
226 |
relational notation for membership in a set of pair, replacing \
|
|
227 |
@{text "(x, y) \<in> sim"} by @{text "x \<approx> y"}.
|
12635
|
228 |
*}
|
|
229 |
|
|
230 |
consts
|
12651
|
231 |
sim :: "('a \<times> 'a) set"
|
12629
|
232 |
|
12651
|
233 |
syntax
|
|
234 |
"_sim" :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<approx>" 50)
|
|
235 |
translations
|
|
236 |
"x \<approx> y" \<rightleftharpoons> "(x, y) \<in> sim"
|
12629
|
237 |
|
12651
|
238 |
text {*
|
|
239 |
\noindent Here the name of the dummy constant @{text "_sim"} does
|
12766
|
240 |
not matter, as long as it is not used elsewhere. Prefixing an
|
|
241 |
underscore is a common convention. The \isakeyword{translations}
|
12651
|
242 |
declaration already uses concrete syntax on the left-hand side;
|
|
243 |
internally we relate a raw application @{text "_sim x y"} with
|
|
244 |
@{text "(x, y) \<in> sim"}.
|
|
245 |
|
12653
|
246 |
\medskip Another common application of syntax translations is to
|
12651
|
247 |
provide variant versions of fundamental relational expressions, such
|
|
248 |
as @{text \<noteq>} for negated equalities. The following declaration
|
|
249 |
stems from Isabelle/HOL itself:
|
12629
|
250 |
*}
|
|
251 |
|
12651
|
252 |
syntax "_not_equal" :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<noteq>\<ignore>" 50)
|
|
253 |
translations "x \<noteq>\<ignore> y" \<rightleftharpoons> "\<not> (x = y)"
|
12629
|
254 |
|
12651
|
255 |
text {*
|
|
256 |
\noindent Normally one would introduce derived concepts like this
|
12653
|
257 |
within the logic, using \isakeyword{consts} + \isakeyword{defs}
|
|
258 |
instead of \isakeyword{syntax} + \isakeyword{translations}. The
|
12651
|
259 |
present formulation has the virtue that expressions are immediately
|
12665
|
260 |
replaced by the ``definition'' upon parsing; the effect is reversed
|
|
261 |
upon printing.
|
12651
|
262 |
|
12766
|
263 |
This sort of translation is appropriate when the defined concept is
|
|
264 |
a trivial variation on an existing one. On the other hand, syntax
|
|
265 |
translations do not scale up well to large hierarchies of concepts.
|
|
266 |
Translations do not replace definitions!
|
12629
|
267 |
*}
|
|
268 |
|
|
269 |
|
12653
|
270 |
section {* Document Preparation \label{sec:document-preparation} *}
|
12629
|
271 |
|
12645
|
272 |
text {*
|
12653
|
273 |
Isabelle/Isar is centered around the concept of \bfindex{formal
|
12766
|
274 |
proof documents}\index{documents|bold}. The outcome of a formal
|
|
275 |
development effort is meant to be a human-readable record, presented
|
|
276 |
as browsable PDF file or printed on paper. The overall document
|
|
277 |
structure follows traditional mathematical articles, with sections,
|
|
278 |
intermediate explanations, definitions, theorems and proofs.
|
12629
|
279 |
|
12645
|
280 |
\medskip The Isabelle document preparation system essentially acts
|
12670
|
281 |
as a front-end to {\LaTeX}. After checking specifications and
|
|
282 |
proofs formally, the theory sources are turned into typesetting
|
12766
|
283 |
instructions in a schematic manner. This lets you write authentic
|
|
284 |
reports on theory developments with little effort: many technical
|
|
285 |
consistency checks are handled by the system.
|
12744
|
286 |
|
|
287 |
Here is an example to illustrate the idea of Isabelle document
|
|
288 |
preparation.
|
12746
|
289 |
*}
|
12744
|
290 |
|
12746
|
291 |
text_raw {* \begin{quotation} *}
|
|
292 |
|
|
293 |
text {*
|
|
294 |
The following datatype definition of @{text "'a bintree"} models
|
|
295 |
binary trees with nodes being decorated by elements of type @{typ
|
|
296 |
'a}.
|
12744
|
297 |
*}
|
|
298 |
|
|
299 |
datatype 'a bintree =
|
12746
|
300 |
Leaf | Branch 'a "'a bintree" "'a bintree"
|
12744
|
301 |
|
|
302 |
text {*
|
|
303 |
\noindent The datatype induction rule generated here is of the form
|
12746
|
304 |
@{thm [indent = 1, display] bintree.induct [no_vars]}
|
|
305 |
*}
|
12744
|
306 |
|
12746
|
307 |
text_raw {* \end{quotation} *}
|
|
308 |
|
|
309 |
text {*
|
12766
|
310 |
\noindent The above document output has been produced as follows:
|
12744
|
311 |
|
|
312 |
\begin{ttbox}
|
|
313 |
text {\ttlbrace}*
|
|
314 |
The following datatype definition of {\at}{\ttlbrace}text "'a bintree"{\ttrbrace}
|
|
315 |
models binary trees with nodes being decorated by elements
|
|
316 |
of type {\at}{\ttlbrace}typ 'a{\ttrbrace}.
|
|
317 |
*{\ttrbrace}
|
|
318 |
|
|
319 |
datatype 'a bintree =
|
|
320 |
Leaf | Branch 'a "'a bintree" "'a bintree"
|
12766
|
321 |
\end{ttbox}
|
|
322 |
\begin{ttbox}
|
12744
|
323 |
text {\ttlbrace}*
|
|
324 |
{\ttback}noindent The datatype induction rule generated here is
|
|
325 |
of the form {\at}{\ttlbrace}thm [display] bintree.induct [no_vars]{\ttrbrace}
|
|
326 |
*{\ttrbrace}
|
12766
|
327 |
\end{ttbox}\vspace{-\medskipamount}
|
12744
|
328 |
|
12746
|
329 |
\noindent Here we have augmented the theory by formal comments
|
12766
|
330 |
(using \isakeyword{text} blocks), the informal parts may again refer
|
|
331 |
to formal entities by means of ``antiquotations'' (such as
|
12744
|
332 |
\texttt{\at}\verb,{text "'a bintree"}, or
|
12746
|
333 |
\texttt{\at}\verb,{typ 'a},), see also \S\ref{sec:doc-prep-text}.
|
12645
|
334 |
*}
|
|
335 |
|
|
336 |
|
12648
|
337 |
subsection {* Isabelle Sessions *}
|
12629
|
338 |
|
|
339 |
text {*
|
12653
|
340 |
In contrast to the highly interactive mode of Isabelle/Isar theory
|
|
341 |
development, the document preparation stage essentially works in
|
12670
|
342 |
batch-mode. An Isabelle \bfindex{session} consists of a collection
|
12766
|
343 |
of source files that may contribute to an output document. Each
|
|
344 |
session is derived from a single parent, usually an object-logic
|
|
345 |
image like \texttt{HOL}. This results in an overall tree structure,
|
|
346 |
which is reflected by the output location in the file system
|
|
347 |
(usually rooted at \verb,~/isabelle/browser_info,).
|
12645
|
348 |
|
12683
|
349 |
\medskip The easiest way to manage Isabelle sessions is via
|
12685
|
350 |
\texttt{isatool mkdir} (generates an initial session source setup)
|
|
351 |
and \texttt{isatool make} (run sessions controlled by
|
12683
|
352 |
\texttt{IsaMakefile}). For example, a new session
|
|
353 |
\texttt{MySession} derived from \texttt{HOL} may be produced as
|
|
354 |
follows:
|
|
355 |
|
|
356 |
\begin{verbatim}
|
|
357 |
isatool mkdir HOL MySession
|
|
358 |
isatool make
|
|
359 |
\end{verbatim}
|
|
360 |
|
12685
|
361 |
The \texttt{isatool make} job also informs about the file-system
|
|
362 |
location of the ultimate results. The above dry run should be able
|
|
363 |
to produce some \texttt{document.pdf} (with dummy title, empty table
|
12743
|
364 |
of contents etc.). Any failure at this stage usually indicates
|
12685
|
365 |
technical problems of the {\LaTeX} installation.\footnote{Especially
|
12766
|
366 |
make sure that \texttt{pdflatex} is present; if in doubt one may
|
12685
|
367 |
fall back on DVI output by changing \texttt{usedir} options in
|
|
368 |
\texttt{IsaMakefile} \cite{isabelle-sys}.}
|
12683
|
369 |
|
|
370 |
\medskip The detailed arrangement of the session sources is as
|
12746
|
371 |
follows.
|
12645
|
372 |
|
|
373 |
\begin{itemize}
|
|
374 |
|
12670
|
375 |
\item Directory \texttt{MySession} holds the required theory files
|
|
376 |
$T@1$\texttt{.thy}, \dots, $T@n$\texttt{.thy}.
|
12645
|
377 |
|
|
378 |
\item File \texttt{MySession/ROOT.ML} holds appropriate ML commands
|
|
379 |
for loading all wanted theories, usually just
|
12665
|
380 |
``\texttt{use_thy"$T@i$";}'' for any $T@i$ in leaf position of the
|
12670
|
381 |
dependency graph.
|
12645
|
382 |
|
|
383 |
\item Directory \texttt{MySession/document} contains everything
|
12653
|
384 |
required for the {\LaTeX} stage; only \texttt{root.tex} needs to be
|
|
385 |
provided initially.
|
12645
|
386 |
|
12653
|
387 |
The latter file holds appropriate {\LaTeX} code to commence a
|
|
388 |
document (\verb,\documentclass, etc.), and to include the generated
|
12743
|
389 |
files $T@i$\texttt{.tex} for each theory. Isabelle will generate a
|
|
390 |
file \texttt{session.tex} holding {\LaTeX} commands to include all
|
12746
|
391 |
generated theory output files in topologically sorted order, so
|
|
392 |
\verb,\input{session}, in the body of \texttt{root.tex} does the job
|
|
393 |
in most situations.
|
12653
|
394 |
|
12681
|
395 |
\item \texttt{IsaMakefile} holds appropriate dependencies and
|
|
396 |
invocations of Isabelle tools to control the batch job. In fact,
|
12746
|
397 |
several sessions may be managed by the same \texttt{IsaMakefile}.
|
12764
|
398 |
See the \emph{Isabelle System Manual} \cite{isabelle-sys}
|
|
399 |
for further details, especially on
|
12653
|
400 |
\texttt{isatool usedir} and \texttt{isatool make}.
|
12645
|
401 |
|
|
402 |
\end{itemize}
|
|
403 |
|
12685
|
404 |
One may now start to populate the directory \texttt{MySession}, and
|
12766
|
405 |
the file \texttt{MySession/ROOT.ML} accordingly. The file
|
|
406 |
\texttt{MySession/document/root.tex} should also be adapted at some
|
12685
|
407 |
point; the default version is mostly self-explanatory. Note that
|
|
408 |
\verb,\isabellestyle, enables fine-tuning of the general appearance
|
|
409 |
of characters and mathematical symbols (see also
|
|
410 |
\S\ref{sec:doc-prep-symbols}).
|
12653
|
411 |
|
12685
|
412 |
Especially observe the included {\LaTeX} packages \texttt{isabelle}
|
|
413 |
(mandatory), \texttt{isabellesym} (required for mathematical
|
12743
|
414 |
symbols), and the final \texttt{pdfsetup} (provides sane defaults
|
12764
|
415 |
for \texttt{hyperref}, including URL markup). All three are
|
12743
|
416 |
distributed with Isabelle. Further packages may be required in
|
12764
|
417 |
particular applications, say for unusual mathematical symbols.
|
12645
|
418 |
|
12746
|
419 |
\medskip Any additional files for the {\LaTeX} stage go into the
|
|
420 |
\texttt{MySession/document} directory as well. In particular,
|
12766
|
421 |
adding a file named \texttt{root.bib} causes an automatic run of
|
|
422 |
\texttt{bibtex} to process a bibliographic database; see also
|
|
423 |
\texttt{isatool document} \cite{isabelle-sys}.
|
12645
|
424 |
|
12653
|
425 |
\medskip Any failure of the document preparation phase in an
|
12670
|
426 |
Isabelle batch session leaves the generated sources in their target
|
12766
|
427 |
location, identified by the accompanying error message. This lets
|
|
428 |
you trace {\LaTeX} problems with the generated files at hand.
|
12645
|
429 |
*}
|
|
430 |
|
|
431 |
|
12648
|
432 |
subsection {* Structure Markup *}
|
12645
|
433 |
|
12653
|
434 |
text {*
|
|
435 |
The large-scale structure of Isabelle documents follows existing
|
|
436 |
{\LaTeX} conventions, with chapters, sections, subsubsections etc.
|
|
437 |
The Isar language includes separate \bfindex{markup commands}, which
|
12681
|
438 |
do not affect the formal meaning of a theory (or proof), but result
|
12665
|
439 |
in corresponding {\LaTeX} elements.
|
12645
|
440 |
|
12665
|
441 |
There are separate markup commands depending on the textual context:
|
|
442 |
in header position (just before \isakeyword{theory}), within the
|
|
443 |
theory body, or within a proof. The header needs to be treated
|
|
444 |
specially here, since ordinary theory and proof commands may only
|
|
445 |
occur \emph{after} the initial \isakeyword{theory} specification.
|
12645
|
446 |
|
12665
|
447 |
\medskip
|
12645
|
448 |
|
|
449 |
\begin{tabular}{llll}
|
|
450 |
header & theory & proof & default meaning \\\hline
|
|
451 |
& \commdx{chapter} & & \verb,\chapter, \\
|
|
452 |
\commdx{header} & \commdx{section} & \commdx{sect} & \verb,\section, \\
|
|
453 |
& \commdx{subsection} & \commdx{subsect} & \verb,\subsection, \\
|
|
454 |
& \commdx{subsubsection} & \commdx{subsubsect} & \verb,\subsubsection, \\
|
|
455 |
\end{tabular}
|
|
456 |
|
|
457 |
\medskip
|
|
458 |
|
|
459 |
From the Isabelle perspective, each markup command takes a single
|
12746
|
460 |
$text$ argument (delimited by \verb,",~@{text \<dots>}~\verb,", or
|
|
461 |
\verb,{,\verb,*,~@{text \<dots>}~\verb,*,\verb,},). After stripping any
|
12645
|
462 |
surrounding white space, the argument is passed to a {\LaTeX} macro
|
12766
|
463 |
\verb,\isamarkupXYZ, for command \isakeyword{XYZ}. These macros are
|
|
464 |
defined in \verb,isabelle.sty, according to the meaning given in the
|
|
465 |
rightmost column above.
|
12645
|
466 |
|
|
467 |
\medskip The following source fragment illustrates structure markup
|
12653
|
468 |
of a theory. Note that {\LaTeX} labels may be included inside of
|
|
469 |
section headings as well.
|
12645
|
470 |
|
|
471 |
\begin{ttbox}
|
|
472 |
header {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace}
|
|
473 |
|
|
474 |
theory Foo_Bar = Main:
|
|
475 |
|
|
476 |
subsection {\ttlbrace}* Basic definitions *{\ttrbrace}
|
|
477 |
|
|
478 |
consts
|
|
479 |
foo :: \dots
|
|
480 |
bar :: \dots
|
12648
|
481 |
|
12645
|
482 |
defs \dots
|
12648
|
483 |
|
12645
|
484 |
subsection {\ttlbrace}* Derived rules *{\ttrbrace}
|
|
485 |
|
|
486 |
lemma fooI: \dots
|
|
487 |
lemma fooE: \dots
|
|
488 |
|
12648
|
489 |
subsection {\ttlbrace}* Main theorem {\ttback}label{\ttlbrace}sec:main-theorem{\ttrbrace} *{\ttrbrace}
|
12645
|
490 |
|
|
491 |
theorem main: \dots
|
|
492 |
|
|
493 |
end
|
12766
|
494 |
\end{ttbox}\vspace{-\medskipamount}
|
12645
|
495 |
|
12766
|
496 |
You may occasionally want to change the meaning of markup commands,
|
|
497 |
say via \verb,\renewcommand, in \texttt{root.tex}. For example,
|
|
498 |
\verb,\isamarkupheader, is a good candidate for some tuning. We
|
|
499 |
could move it up in the hierarchy to become \verb,\chapter,.
|
12645
|
500 |
|
|
501 |
\begin{verbatim}
|
|
502 |
\renewcommand{\isamarkupheader}[1]{\chapter{#1}}
|
|
503 |
\end{verbatim}
|
|
504 |
|
12766
|
505 |
\noindent Now we must change the document class given in
|
|
506 |
\texttt{root.tex} to something that supports chapters. A suitable
|
|
507 |
command is \verb,\documentclass{report},.
|
12645
|
508 |
|
12648
|
509 |
\medskip The {\LaTeX} macro \verb,\isabellecontext, is maintained to
|
|
510 |
hold the name of the current theory context. This is particularly
|
12653
|
511 |
useful for document headings:
|
12645
|
512 |
|
|
513 |
\begin{verbatim}
|
12653
|
514 |
\renewcommand{\isamarkupheader}[1]
|
12645
|
515 |
{\chapter{#1}\markright{THEORY~\isabellecontext}}
|
|
516 |
\end{verbatim}
|
|
517 |
|
|
518 |
\noindent Make sure to include something like
|
12648
|
519 |
\verb,\pagestyle{headings}, in \texttt{root.tex}; the document
|
12764
|
520 |
should have more than two pages to show the effect.
|
12645
|
521 |
*}
|
|
522 |
|
|
523 |
|
12744
|
524 |
subsection {* Formal Comments and Antiquotations \label{sec:doc-prep-text} *}
|
12645
|
525 |
|
|
526 |
text {*
|
12744
|
527 |
Isabelle \bfindex{source comments}, which are of the form
|
12746
|
528 |
\verb,(,\verb,*,~@{text \<dots>}~\verb,*,\verb,),, essentially act like
|
|
529 |
white space and do not really contribute to the content. They
|
|
530 |
mainly serve technical purposes to mark certain oddities in the raw
|
|
531 |
input text. In contrast, \bfindex{formal comments} are portions of
|
|
532 |
text that are associated with formal Isabelle/Isar commands
|
12681
|
533 |
(\bfindex{marginal comments}), or as standalone paragraphs within a
|
12665
|
534 |
theory or proof context (\bfindex{text blocks}).
|
12659
|
535 |
|
|
536 |
\medskip Marginal comments are part of each command's concrete
|
12670
|
537 |
syntax \cite{isabelle-ref}; the common form is ``\verb,--,~$text$''
|
12746
|
538 |
where $text$ is delimited by \verb,",@{text \<dots>}\verb,", or
|
|
539 |
\verb,{,\verb,*,~@{text \<dots>}~\verb,*,\verb,}, as before. Multiple
|
12670
|
540 |
marginal comments may be given at the same time. Here is a simple
|
|
541 |
example:
|
12665
|
542 |
*}
|
|
543 |
|
|
544 |
lemma "A --> A"
|
|
545 |
-- "a triviality of propositional logic"
|
|
546 |
-- "(should not really bother)"
|
|
547 |
by (rule impI) -- "implicit assumption step involved here"
|
|
548 |
|
|
549 |
text {*
|
|
550 |
\noindent The above output has been produced as follows:
|
12659
|
551 |
|
|
552 |
\begin{verbatim}
|
|
553 |
lemma "A --> A"
|
|
554 |
-- "a triviality of propositional logic"
|
|
555 |
-- "(should not really bother)"
|
|
556 |
by (rule impI) -- "implicit assumption step involved here"
|
|
557 |
\end{verbatim}
|
|
558 |
|
12670
|
559 |
From the {\LaTeX} viewpoint, ``\verb,--,'' acts like a markup
|
|
560 |
command, associated with the macro \verb,\isamarkupcmt, (taking a
|
|
561 |
single argument).
|
12659
|
562 |
|
12665
|
563 |
\medskip Text blocks are introduced by the commands \bfindex{text}
|
|
564 |
and \bfindex{txt}, for theory and proof contexts, respectively.
|
|
565 |
Each takes again a single $text$ argument, which is interpreted as a
|
|
566 |
free-form paragraph in {\LaTeX} (surrounded by some additional
|
12670
|
567 |
vertical space). This behavior may be changed by redefining the
|
|
568 |
{\LaTeX} environments of \verb,isamarkuptext, or
|
|
569 |
\verb,isamarkuptxt,, respectively (via \verb,\renewenvironment,) The
|
|
570 |
text style of the body is determined by \verb,\isastyletext, and
|
|
571 |
\verb,\isastyletxt,; the default setup uses a smaller font within
|
12746
|
572 |
proofs. This may be changed as follows:
|
|
573 |
|
|
574 |
\begin{verbatim}
|
|
575 |
\renewcommand{\isastyletxt}{\isastyletext}
|
|
576 |
\end{verbatim}
|
12659
|
577 |
|
12766
|
578 |
\medskip The $text$ part of Isabelle markup commands essentially
|
|
579 |
inserts \emph{quoted material} into a formal text, mainly for
|
|
580 |
instruction of the reader. An \bfindex{antiquotation} is again a
|
|
581 |
formal object embedded into such an informal portion. The
|
|
582 |
interpretation of antiquotations is limited to some well-formedness
|
|
583 |
checks, with the result being pretty printed to the resulting
|
|
584 |
document. Quoted text blocks together with antiquotations provide
|
|
585 |
an attractive means of referring to formal entities, with good
|
|
586 |
confidence in getting the technical details right (especially syntax
|
|
587 |
and types).
|
12659
|
588 |
|
12665
|
589 |
The general syntax of antiquotations is as follows:
|
12659
|
590 |
\texttt{{\at}{\ttlbrace}$name$ $arguments${\ttrbrace}}, or
|
|
591 |
\texttt{{\at}{\ttlbrace}$name$ [$options$] $arguments${\ttrbrace}}
|
12665
|
592 |
for a comma-separated list of options consisting of a $name$ or
|
12766
|
593 |
\texttt{$name$=$value$} each. The syntax of $arguments$ depends on
|
|
594 |
the kind of antiquotation, it generally follows the same conventions
|
|
595 |
for types, terms, or theorems as in the formal part of a theory.
|
12645
|
596 |
|
12766
|
597 |
\medskip This sentence demonstrates quotations and antiquotations:
|
|
598 |
@{term "%x y. x"} is a well-typed term.
|
12659
|
599 |
|
12764
|
600 |
\medskip\noindent The output above was produced as follows:
|
12659
|
601 |
\begin{ttbox}
|
|
602 |
text {\ttlbrace}*
|
12764
|
603 |
This sentence demonstrates quotations and antiquotations:
|
12659
|
604 |
{\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term.
|
|
605 |
*{\ttrbrace}
|
12766
|
606 |
\end{ttbox}\vspace{-\medskipamount}
|
12659
|
607 |
|
12764
|
608 |
The notational change from the ASCII character~\verb,%, to the
|
12766
|
609 |
symbol~@{text \<lambda>} reveals that Isabelle printed this term, after
|
|
610 |
parsing and type-checking. Document preparation enables symbolic
|
|
611 |
output by default.
|
12659
|
612 |
|
12764
|
613 |
\medskip The next example includes an option to modify Isabelle's
|
|
614 |
\verb,show_types, flag. The antiquotation
|
12766
|
615 |
\texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces the
|
|
616 |
output @{term [show_types] "%x y. x"}. Type inference has figured
|
|
617 |
out the most general typings in the present theory context. Terms
|
|
618 |
may acquire different typings due to constraints imposed by their
|
|
619 |
environment; within a proof, for example, variables are given the
|
|
620 |
same types as they have in the main goal statement.
|
12659
|
621 |
|
12764
|
622 |
\medskip Several further kinds of antiquotations and options are
|
12665
|
623 |
available \cite{isabelle-sys}. Here are a few commonly used
|
12670
|
624 |
combinations:
|
12659
|
625 |
|
|
626 |
\medskip
|
12651
|
627 |
|
12659
|
628 |
\begin{tabular}{ll}
|
|
629 |
\texttt{\at}\verb,{typ,~$\tau$\verb,}, & print type $\tau$ \\
|
|
630 |
\texttt{\at}\verb,{term,~$t$\verb,}, & print term $t$ \\
|
|
631 |
\texttt{\at}\verb,{prop,~$\phi$\verb,}, & print proposition $\phi$ \\
|
12665
|
632 |
\texttt{\at}\verb,{prop [display],~$\phi$\verb,}, & print large proposition $\phi$ (with linebreaks) \\
|
12659
|
633 |
\texttt{\at}\verb,{prop [source],~$\phi$\verb,}, & check proposition $\phi$, print its input \\
|
|
634 |
\texttt{\at}\verb,{thm,~$a$\verb,}, & print fact $a$ \\
|
|
635 |
\texttt{\at}\verb,{thm,~$a$~\verb,[no_vars]}, & print fact $a$, fixing schematic variables \\
|
12746
|
636 |
\texttt{\at}\verb,{thm [source],~$a$\verb,}, & check availability of fact $a$, print its name \\
|
12659
|
637 |
\texttt{\at}\verb,{text,~$s$\verb,}, & print uninterpreted text $s$ \\
|
|
638 |
\end{tabular}
|
|
639 |
|
|
640 |
\medskip
|
|
641 |
|
12665
|
642 |
Note that \attrdx{no_vars} given above is \emph{not} an
|
|
643 |
antiquotation option, but an attribute of the theorem argument given
|
|
644 |
here. This might be useful with a diagnostic command like
|
|
645 |
\isakeyword{thm}, too.
|
12659
|
646 |
|
12665
|
647 |
\medskip The \texttt{\at}\verb,{text, $s$\verb,}, antiquotation is
|
12659
|
648 |
particularly interesting. Embedding uninterpreted text within an
|
12665
|
649 |
informal body might appear useless at first sight. Here the key
|
|
650 |
virtue is that the string $s$ is processed as Isabelle output,
|
|
651 |
interpreting Isabelle symbols appropriately.
|
12659
|
652 |
|
12665
|
653 |
For example, \texttt{\at}\verb,{text "\<forall>\<exists>"}, produces @{text
|
|
654 |
"\<forall>\<exists>"}, according to the standard interpretation of these symbol
|
|
655 |
(cf.\ \S\ref{sec:doc-prep-symbols}). Thus we achieve consistent
|
12659
|
656 |
mathematical notation in both the formal and informal parts of the
|
12766
|
657 |
document very easily, independently of the term language of
|
|
658 |
Isabelle. Manual {\LaTeX} code would leave more control over the
|
|
659 |
typesetting, but is also slightly more tedious.
|
12645
|
660 |
*}
|
|
661 |
|
|
662 |
|
12674
|
663 |
subsection {* Interpretation of Symbols \label{sec:doc-prep-symbols} *}
|
12645
|
664 |
|
|
665 |
text {*
|
12665
|
666 |
As has been pointed out before (\S\ref{sec:syntax-symbols}),
|
12670
|
667 |
Isabelle symbols are the smallest syntactic entities --- a
|
12681
|
668 |
straightforward generalization of ASCII characters. While Isabelle
|
12665
|
669 |
does not impose any interpretation of the infinite collection of
|
12764
|
670 |
named symbols, {\LaTeX} documents use canonical glyphs for certain
|
12670
|
671 |
standard symbols \cite[appendix~A]{isabelle-sys}.
|
12659
|
672 |
|
12766
|
673 |
The {\LaTeX} code produced from Isabelle text follows a simple
|
|
674 |
scheme. You can tune the final appearance by redefining certain
|
|
675 |
macros, say in \texttt{root.tex} of the document.
|
12670
|
676 |
|
|
677 |
\begin{enumerate}
|
12659
|
678 |
|
12670
|
679 |
\item 7-bit ASCII characters: letters \texttt{A\dots Z} and
|
12746
|
680 |
\texttt{a\dots z} are output directly, digits are passed as an
|
12670
|
681 |
argument to the \verb,\isadigit, macro, other characters are
|
|
682 |
replaced by specifically named macros of the form
|
12665
|
683 |
\verb,\isacharXYZ,.
|
12659
|
684 |
|
12766
|
685 |
\item Named symbols: \verb,\,\verb,<XYZ>, is turned into
|
|
686 |
\verb,{\isasymXYZ},; note the additional braces.
|
12659
|
687 |
|
12766
|
688 |
\item Named control symbols: \verb,\,\verb,<^XYZ>, is turned into
|
|
689 |
\verb,\isactrlXYZ,; subsequent symbols may act as arguments if the
|
|
690 |
control macro is defined accordingly.
|
12670
|
691 |
|
12659
|
692 |
\end{enumerate}
|
12665
|
693 |
|
12764
|
694 |
You may occasionally wish to give new {\LaTeX} interpretations of
|
|
695 |
named symbols. This merely requires an appropriate definition of
|
12766
|
696 |
\verb,\isasymXYZ,, for \verb,\,\verb,<XYZ>, (see
|
12746
|
697 |
\texttt{isabelle.sty} for working examples). Control symbols are
|
|
698 |
slightly more difficult to get right, though.
|
12665
|
699 |
|
|
700 |
\medskip The \verb,\isabellestyle, macro provides a high-level
|
|
701 |
interface to tune the general appearance of individual symbols. For
|
12670
|
702 |
example, \verb,\isabellestyle{it}, uses the italics text style to
|
|
703 |
mimic the general appearance of the {\LaTeX} math mode; double
|
12743
|
704 |
quotes are not printed at all. The resulting quality of typesetting
|
|
705 |
is quite good, so this should be the default style for work that
|
|
706 |
gets distributed to a broader audience.
|
12645
|
707 |
*}
|
|
708 |
|
|
709 |
|
12653
|
710 |
subsection {* Suppressing Output \label{sec:doc-prep-suppress} *}
|
12645
|
711 |
|
|
712 |
text {*
|
12748
|
713 |
By default, Isabelle's document system generates a {\LaTeX} file for
|
|
714 |
each theory that gets loaded while running the session. The
|
|
715 |
generated \texttt{session.tex} will include all of these in order of
|
|
716 |
appearance, which in turn gets included by the standard
|
12743
|
717 |
\texttt{root.tex}. Certainly one may change the order or suppress
|
12746
|
718 |
unwanted theories by ignoring \texttt{session.tex} and load
|
|
719 |
individual files directly in \texttt{root.tex}. On the other hand,
|
|
720 |
such an arrangement requires additional maintenance whenever the
|
|
721 |
collection of theories changes.
|
12648
|
722 |
|
|
723 |
Alternatively, one may tune the theory loading process in
|
12653
|
724 |
\texttt{ROOT.ML} itself: traversal of the theory dependency graph
|
12670
|
725 |
may be fine-tuned by adding \verb,use_thy, invocations, although
|
|
726 |
topological sorting still has to be observed. Moreover, the ML
|
|
727 |
operator \verb,no_document, temporarily disables document generation
|
12766
|
728 |
while executing a theory loader command. Its usage is like this:
|
12648
|
729 |
|
|
730 |
\begin{verbatim}
|
12665
|
731 |
no_document use_thy "T";
|
12648
|
732 |
\end{verbatim}
|
12645
|
733 |
|
12766
|
734 |
\medskip Theory output may be suppressed more selectively. Research
|
|
735 |
articles and slides usually do not include the formal content in
|
|
736 |
full. Delimiting \bfindex{ignored material} by the special source
|
|
737 |
comments \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
|
|
738 |
\verb,(,\verb,*,\verb,>,\verb,*,\verb,), tells the document
|
|
739 |
preparation system to suppress these parts; the formal checking of
|
12771
|
740 |
the theory is unchanged, of course.
|
12648
|
741 |
|
12766
|
742 |
In this example, we hide a theory's \isakeyword{theory} and
|
|
743 |
\isakeyword{end} brackets:
|
12648
|
744 |
|
|
745 |
\medskip
|
|
746 |
|
|
747 |
\begin{tabular}{l}
|
|
748 |
\verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
|
12665
|
749 |
\texttt{theory T = Main:} \\
|
12648
|
750 |
\verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
|
|
751 |
~~$\vdots$ \\
|
|
752 |
\verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
|
|
753 |
\texttt{end} \\
|
|
754 |
\verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
|
|
755 |
\end{tabular}
|
|
756 |
|
|
757 |
\medskip
|
|
758 |
|
12764
|
759 |
Text may be suppressed in a fine-grained manner. We may even hide
|
12746
|
760 |
vital parts of a proof, pretending that things have been simpler
|
12766
|
761 |
than they really were. For example, this ``fully automatic'' proof
|
|
762 |
is actually a fake:
|
12651
|
763 |
*}
|
|
764 |
|
|
765 |
lemma "x \<noteq> (0::int) \<Longrightarrow> 0 < x * x"
|
|
766 |
by (auto(*<*)simp add: int_less_le(*>*))
|
|
767 |
|
|
768 |
text {*
|
|
769 |
\noindent Here the real source of the proof has been as follows:
|
|
770 |
|
|
771 |
\begin{verbatim}
|
|
772 |
by (auto(*<*)simp add: int_less_le(*>*))
|
12659
|
773 |
\end{verbatim}
|
|
774 |
%(*
|
12651
|
775 |
|
12766
|
776 |
\medskip Suppressing portions of printed text demands care. You
|
|
777 |
should not misrepresent the underlying theory development. It is
|
|
778 |
easy to invalidate the visible text by hiding references to
|
|
779 |
questionable axioms.
|
12651
|
780 |
|
12746
|
781 |
Authentic reports of Isabelle/Isar theories, say as part of a
|
12766
|
782 |
library, should suppress nothing. Other users may need the full
|
|
783 |
information for their own derivative work. If a particular
|
|
784 |
formalization appears inadequate for general public coverage, it is
|
|
785 |
often more appropriate to think of a better way in the first place.
|
12670
|
786 |
|
|
787 |
\medskip Some technical subtleties of the
|
12665
|
788 |
\verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),
|
12764
|
789 |
elements need to be kept in mind, too --- the system performs few
|
12670
|
790 |
sanity checks here. Arguments of markup commands and formal
|
12651
|
791 |
comments must not be hidden, otherwise presentation fails. Open and
|
12750
|
792 |
close parentheses need to be inserted carefully; it is easy to hide
|
|
793 |
the wrong parts, especially after rearranging the theory text.
|
12629
|
794 |
*}
|
|
795 |
|
11647
|
796 |
(*<*)
|
|
797 |
end
|
|
798 |
(*>*)
|