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