author | wenzelm |
Sat, 05 Jan 2019 17:24:33 +0100 | |
changeset 69597 | ff784d5a5bfb |
parent 69505 | cc2d676d5395 |
child 76987 | 4c275405faae |
permissions | -rw-r--r-- |
11647 | 1 |
(*<*) |
16417 | 2 |
theory Documents imports Main begin |
11647 | 3 |
(*>*) |
4 |
||
67406 | 5 |
section \<open>Concrete Syntax \label{sec:concrete-syntax}\<close> |
12629 | 6 |
|
67406 | 7 |
text \<open> |
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 |
58620 | 14 |
subtle affair~@{cite "isabelle-isar-ref"}. Your syntax specifications need |
12766 | 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 |
|
25338 | 20 |
Below we introduce a few simple syntax declaration |
12743 | 21 |
forms that already cover many common situations fairly well. |
67406 | 22 |
\<close> |
12629 | 23 |
|
24 |
||
67406 | 25 |
subsection \<open>Infix Annotations\<close> |
12629 | 26 |
|
67406 | 27 |
text \<open> |
12764 | 28 |
Syntax annotations may be included wherever constants are declared, |
27015 | 29 |
such as \isacommand{definition} and \isacommand{primrec} --- and also |
12766 | 30 |
\isacommand{datatype}, which declares constructor operations. |
31 |
Type-constructors may be annotated as well, although this is less |
|
69505 | 32 |
frequently encountered in practice (the infix type \<open>\<times>\<close> comes |
12766 | 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. |
|
67406 | 38 |
\<close> |
12629 | 39 |
|
27015 | 40 |
definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "[+]" 60) |
41 |
where "A [+] B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)" |
|
12629 | 42 |
|
67406 | 43 |
text \<open> |
69505 | 44 |
\noindent Now \<open>xor A B\<close> and \<open>A [+] B\<close> refer to the |
12653 | 45 |
same expression internally. Any curried function with at least two |
12766 | 46 |
arguments may be given infix syntax. For partial applications with |
67398 | 47 |
fewer than two operands, the operator is enclosed in parentheses. |
69505 | 48 |
For instance, \<open>xor\<close> without arguments is represented as |
49 |
\<open>([+])\<close>; together with ordinary function application, this |
|
50 |
turns \<open>xor A\<close> into \<open>([+]) A\<close>. |
|
12629 | 51 |
|
25338 | 52 |
The keyword \isakeyword{infixl} seen above specifies an |
12746 | 53 |
infix operator that is nested to the \emph{left}: in iterated |
54 |
applications the more complex expression appears on the left-hand |
|
69597 | 55 |
side, and \<^term>\<open>A [+] B [+] C\<close> stands for \<open>(A [+] B) [+] |
69505 | 56 |
C\<close>. Similarly, \isakeyword{infixr} means nesting to the |
69597 | 57 |
\emph{right}, reading \<^term>\<open>A [+] B [+] C\<close> as \<open>A [+] (B |
69505 | 58 |
[+] C)\<close>. A \emph{non-oriented} declaration via \isakeyword{infix} |
69597 | 59 |
would render \<^term>\<open>A [+] B [+] C\<close> illegal, but demand explicit |
12766 | 60 |
parentheses to indicate the intended grouping. |
12743 | 61 |
|
12746 | 62 |
The string @{text [source] "[+]"} in our annotation refers to the |
63 |
concrete syntax to represent the operator (a literal token), while |
|
69505 | 64 |
the number \<open>60\<close> determines the precedence of the construct: |
12766 | 65 |
the syntactic priorities of the arguments and result. Isabelle/HOL |
66 |
already uses up many popular combinations of ASCII symbols for its |
|
69505 | 67 |
own use, including both \<open>+\<close> and \<open>++\<close>. Longer |
12766 | 68 |
character combinations are more likely to be still available for |
69505 | 69 |
user extensions, such as our~\<open>[+]\<close>. |
12629 | 70 |
|
12766 | 71 |
Operator precedences have a range of 0--1000. Very low or high |
72 |
priorities are reserved for the meta-logic. HOL syntax mainly uses |
|
69505 | 73 |
the range of 10--100: the equality infix \<open>=\<close> is centered at |
74 |
50; logical connectives (like \<open>\<or>\<close> and \<open>\<and>\<close>) are |
|
75 |
below 50; algebraic ones (like \<open>+\<close> and \<open>*\<close>) are |
|
12766 | 76 |
above 50. User syntax should strive to coexist with common HOL |
77 |
forms, or use the mostly unused range 100--900. |
|
67406 | 78 |
\<close> |
12629 | 79 |
|
12635 | 80 |
|
67406 | 81 |
subsection \<open>Mathematical Symbols \label{sec:syntax-symbols}\<close> |
12629 | 82 |
|
67406 | 83 |
text \<open> |
12766 | 84 |
Concrete syntax based on ASCII characters has inherent limitations. |
85 |
Mathematical notation demands a larger repertoire of glyphs. |
|
86 |
Several standards of extended character sets have been proposed over |
|
87 |
decades, but none has become universally available so far. Isabelle |
|
88 |
has its own notion of \bfindex{symbols} as the smallest entities of |
|
89 |
source text, without referring to internal encodings. There are |
|
90 |
three kinds of such ``generalized characters'': |
|
12635 | 91 |
|
92 |
\begin{enumerate} |
|
93 |
||
12653 | 94 |
\item 7-bit ASCII characters |
12635 | 95 |
|
12653 | 96 |
\item named symbols: \verb,\,\verb,<,$ident$\verb,>, |
12629 | 97 |
|
12653 | 98 |
\item named control symbols: \verb,\,\verb,<^,$ident$\verb,>, |
12635 | 99 |
|
100 |
\end{enumerate} |
|
101 |
||
14486 | 102 |
Here $ident$ is any sequence of letters. |
103 |
This results in an infinite store of symbols, whose |
|
12766 | 104 |
interpretation is left to further front-end tools. For example, the |
58842 | 105 |
Isabelle document processor (see \S\ref{sec:document-preparation}) |
69505 | 106 |
display the \verb,\,\verb,<forall>, symbol as~\<open>\<forall>\<close>. |
12635 | 107 |
|
108 |
A list of standard Isabelle symbols is given in |
|
58620 | 109 |
@{cite "isabelle-isar-ref"}. You may introduce your own |
12635 | 110 |
interpretation of further symbols by configuring the appropriate |
12653 | 111 |
front-end tool accordingly, e.g.\ by defining certain {\LaTeX} |
112 |
macros (see also \S\ref{sec:doc-prep-symbols}). There are also a |
|
113 |
few predefined control symbols, such as \verb,\,\verb,<^sub>, and |
|
12635 | 114 |
\verb,\,\verb,<^sup>, for sub- and superscript of the subsequent |
61593 | 115 |
printable symbol, respectively. For example, \<^verbatim>\<open>A\<^sup>\<star>\<close>, is |
69505 | 116 |
output as \<open>A\<^sup>\<star>\<close>. |
12635 | 117 |
|
17183 | 118 |
A number of symbols are considered letters by the Isabelle lexer and |
119 |
can be used as part of identifiers. These are the greek letters |
|
69505 | 120 |
\<open>\<alpha>\<close> (\verb+\+\verb+<alpha>+), \<open>\<beta>\<close> |
121 |
(\verb+\+\verb+<beta>+), etc. (excluding \<open>\<lambda>\<close>), |
|
122 |
special letters like \<open>\<A>\<close> (\verb+\+\verb+<A>+) and \<open>\<AA>\<close> (\verb+\+\verb+<AA>+). Moreover the control symbol |
|
52919 | 123 |
\verb+\+\verb+<^sub>+ may be used to subscript a single letter or digit |
124 |
in the trailing part of an identifier. This means that the input |
|
14486 | 125 |
|
126 |
\medskip |
|
61593 | 127 |
{\small\noindent \<^verbatim>\<open>\<forall>\<alpha>\<^sub>1. \<alpha>\<^sub>1 = \<Pi>\<^sub>\<A>\<close>} |
14486 | 128 |
|
129 |
\medskip |
|
69597 | 130 |
\noindent is recognized as the term \<^term>\<open>\<forall>\<alpha>\<^sub>1. \<alpha>\<^sub>1 = \<Pi>\<^sub>\<A>\<close> |
52919 | 131 |
by Isabelle. |
14486 | 132 |
|
69505 | 133 |
Replacing our previous definition of \<open>xor\<close> by the |
17183 | 134 |
following specifies an Isabelle symbol for the new operator: |
67406 | 135 |
\<close> |
12629 | 136 |
|
137 |
(*<*) |
|
36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
wenzelm
parents:
30649
diff
changeset
|
138 |
hide_const xor |
67406 | 139 |
setup \<open>Sign.add_path "version1"\<close> |
12629 | 140 |
(*>*) |
27015 | 141 |
definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "\<oplus>" 60) |
142 |
where "A \<oplus> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)" |
|
12635 | 143 |
(*<*) |
67406 | 144 |
setup \<open>Sign.local_path\<close> |
12635 | 145 |
(*>*) |
12629 | 146 |
|
67406 | 147 |
text \<open> |
58842 | 148 |
It is possible to provide alternative syntax forms |
58620 | 149 |
through the \bfindex{print mode} concept~@{cite "isabelle-isar-ref"}. By |
12766 | 150 |
convention, the mode of ``$xsymbols$'' is enabled whenever |
151 |
Proof~General's X-Symbol mode or {\LaTeX} output is active. Now |
|
69505 | 152 |
consider the following hybrid declaration of \<open>xor\<close>: |
67406 | 153 |
\<close> |
12635 | 154 |
|
155 |
(*<*) |
|
36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
wenzelm
parents:
30649
diff
changeset
|
156 |
hide_const xor |
67406 | 157 |
setup \<open>Sign.add_path "version2"\<close> |
12635 | 158 |
(*>*) |
27015 | 159 |
definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "[+]\<ignore>" 60) |
160 |
where "A [+]\<ignore> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)" |
|
12635 | 161 |
|
25338 | 162 |
notation (xsymbols) xor (infixl "\<oplus>\<ignore>" 60) |
12629 | 163 |
(*<*) |
67406 | 164 |
setup \<open>Sign.local_path\<close> |
12629 | 165 |
(*>*) |
166 |
||
67406 | 167 |
text \<open>\noindent |
27015 | 168 |
The \commdx{notation} command associates a mixfix |
169 |
annotation with a known constant. The print mode specification, |
|
69505 | 170 |
here \<open>(xsymbols)\<close>, is optional. |
12635 | 171 |
|
69505 | 172 |
We may now write \<open>A [+] B\<close> or \<open>A \<oplus> B\<close> in input, while |
25338 | 173 |
output uses the nicer syntax of $xsymbols$ whenever that print mode is |
174 |
active. Such an arrangement is particularly useful for interactive |
|
175 |
development, where users may type ASCII text and see mathematical |
|
67406 | 176 |
symbols displayed during proofs.\<close> |
12635 | 177 |
|
12629 | 178 |
|
67406 | 179 |
subsection \<open>Prefix Annotations\<close> |
12629 | 180 |
|
67406 | 181 |
text \<open> |
12766 | 182 |
Prefix syntax annotations\index{prefix annotation} are another form |
58620 | 183 |
of mixfixes @{cite "isabelle-isar-ref"}, without any template arguments or |
12766 | 184 |
priorities --- just some literal syntax. The following example |
185 |
associates common symbols with the constructors of a datatype. |
|
67406 | 186 |
\<close> |
12629 | 187 |
|
188 |
datatype currency = |
|
189 |
Euro nat ("\<euro>") |
|
190 |
| Pounds nat ("\<pounds>") |
|
191 |
| Yen nat ("\<yen>") |
|
192 |
| Dollar nat ("$") |
|
193 |
||
67406 | 194 |
text \<open> |
12653 | 195 |
\noindent Here the mixfix annotations on the rightmost column happen |
196 |
to consist of a single Isabelle symbol each: \verb,\,\verb,<euro>,, |
|
197 |
\verb,\,\verb,<pounds>,, \verb,\,\verb,<yen>,, and \verb,$,. Recall |
|
69597 | 198 |
that a constructor like \<open>Euro\<close> actually is a function \<^typ>\<open>nat \<Rightarrow> currency\<close>. The expression \<open>Euro 10\<close> will be |
199 |
printed as \<^term>\<open>\<euro> 10\<close>; 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 |
|
27015 | 204 |
Prefix syntax works the same way for other commands that introduce new constants, e.g. \isakeyword{primrec}. |
67406 | 205 |
\<close> |
12651 | 206 |
|
207 |
||
67406 | 208 |
subsection \<open>Abbreviations \label{sec:abbreviations}\<close> |
12651 | 209 |
|
67406 | 210 |
text\<open>Mixfix syntax annotations merely decorate particular constant |
25338 | 211 |
application forms with concrete syntax, for instance replacing |
69505 | 212 |
\<open>xor A B\<close> by \<open>A \<oplus> B\<close>. Occasionally, the relationship |
25338 | 213 |
between some piece of notation and its internal form is more |
214 |
complicated. Here we need \emph{abbreviations}. |
|
215 |
||
216 |
Command \commdx{abbreviation} introduces an uninterpreted notational |
|
217 |
constant as an abbreviation for a complex term. Abbreviations are |
|
218 |
unfolded upon parsing and re-introduced upon printing. This provides a |
|
219 |
simple mechanism for syntactic macros. |
|
12651 | 220 |
|
25338 | 221 |
A typical use of abbreviations is to introduce relational notation for |
69505 | 222 |
membership in a set of pairs, replacing \<open>(x, y) \<in> sim\<close> by |
223 |
\<open>x \<approx> y\<close>. We assume that a constant \<open>sim\<close> of type |
|
69597 | 224 |
\<^typ>\<open>('a \<times> 'a) set\<close> has been introduced at this point.\<close> |
27015 | 225 |
(*<*)consts sim :: "('a \<times> 'a) set"(*>*) |
25338 | 226 |
abbreviation sim2 :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<approx>" 50) |
227 |
where "x \<approx> y \<equiv> (x, y) \<in> sim" |
|
12651 | 228 |
|
67406 | 229 |
text \<open>\noindent The given meta-equality is used as a rewrite rule |
69597 | 230 |
after parsing (replacing \mbox{\<^prop>\<open>x \<approx> y\<close>} by \<open>(x,y) \<in> |
69505 | 231 |
sim\<close>) and before printing (turning \<open>(x,y) \<in> sim\<close> back into |
69597 | 232 |
\mbox{\<^prop>\<open>x \<approx> y\<close>}). The name of the dummy constant \<open>sim2\<close> |
25338 | 233 |
does not matter, as long as it is unique. |
234 |
||
235 |
Another common application of abbreviations is to |
|
236 |
provide variant versions of fundamental relational expressions, such |
|
69505 | 237 |
as \<open>\<noteq>\<close> for negated equalities. The following declaration |
25338 | 238 |
stems from Isabelle/HOL itself: |
67406 | 239 |
\<close> |
12635 | 240 |
|
25338 | 241 |
abbreviation not_equal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "~=\<ignore>" 50) |
242 |
where "x ~=\<ignore> y \<equiv> \<not> (x = y)" |
|
12629 | 243 |
|
25338 | 244 |
notation (xsymbols) not_equal (infix "\<noteq>\<ignore>" 50) |
245 |
||
69505 | 246 |
text \<open>\noindent The notation \<open>\<noteq>\<close> is introduced separately to restrict it |
25338 | 247 |
to the \emph{xsymbols} mode. |
12651 | 248 |
|
27015 | 249 |
Abbreviations are appropriate when the defined concept is a |
25338 | 250 |
simple variation on an existing one. But because of the automatic |
251 |
folding and unfolding of abbreviations, they do not scale up well to |
|
252 |
large hierarchies of concepts. Abbreviations do not replace |
|
253 |
definitions. |
|
12629 | 254 |
|
25338 | 255 |
Abbreviations are a simplified form of the general concept of |
256 |
\emph{syntax translations}; even heavier transformations may be |
|
58620 | 257 |
written in ML @{cite "isabelle-isar-ref"}. |
67406 | 258 |
\<close> |
12629 | 259 |
|
260 |
||
67406 | 261 |
section \<open>Document Preparation \label{sec:document-preparation}\<close> |
12629 | 262 |
|
67406 | 263 |
text \<open> |
12653 | 264 |
Isabelle/Isar is centered around the concept of \bfindex{formal |
12766 | 265 |
proof documents}\index{documents|bold}. The outcome of a formal |
266 |
development effort is meant to be a human-readable record, presented |
|
267 |
as browsable PDF file or printed on paper. The overall document |
|
268 |
structure follows traditional mathematical articles, with sections, |
|
269 |
intermediate explanations, definitions, theorems and proofs. |
|
12629 | 270 |
|
12645 | 271 |
\medskip The Isabelle document preparation system essentially acts |
12670 | 272 |
as a front-end to {\LaTeX}. After checking specifications and |
273 |
proofs formally, the theory sources are turned into typesetting |
|
12766 | 274 |
instructions in a schematic manner. This lets you write authentic |
275 |
reports on theory developments with little effort: many technical |
|
276 |
consistency checks are handled by the system. |
|
12744 | 277 |
|
278 |
Here is an example to illustrate the idea of Isabelle document |
|
279 |
preparation. |
|
67406 | 280 |
\<close> |
12744 | 281 |
|
67406 | 282 |
text_raw \<open>\begin{quotation}\<close> |
12746 | 283 |
|
67406 | 284 |
text \<open> |
69505 | 285 |
The following datatype definition of \<open>'a bintree\<close> models |
69597 | 286 |
binary trees with nodes being decorated by elements of type \<^typ>\<open>'a\<close>. |
67406 | 287 |
\<close> |
12744 | 288 |
|
289 |
datatype 'a bintree = |
|
12746 | 290 |
Leaf | Branch 'a "'a bintree" "'a bintree" |
12744 | 291 |
|
67406 | 292 |
text \<open> |
12744 | 293 |
\noindent The datatype induction rule generated here is of the form |
12746 | 294 |
@{thm [indent = 1, display] bintree.induct [no_vars]} |
67406 | 295 |
\<close> |
12744 | 296 |
|
67406 | 297 |
text_raw \<open>\end{quotation}\<close> |
12746 | 298 |
|
67406 | 299 |
text \<open> |
12766 | 300 |
\noindent The above document output has been produced as follows: |
12744 | 301 |
|
302 |
\begin{ttbox} |
|
303 |
text {\ttlbrace}* |
|
304 |
The following datatype definition of {\at}{\ttlbrace}text "'a bintree"{\ttrbrace} |
|
305 |
models binary trees with nodes being decorated by elements |
|
306 |
of type {\at}{\ttlbrace}typ 'a{\ttrbrace}. |
|
307 |
*{\ttrbrace} |
|
308 |
||
309 |
datatype 'a bintree = |
|
310 |
Leaf | Branch 'a "'a bintree" "'a bintree" |
|
12766 | 311 |
\end{ttbox} |
312 |
\begin{ttbox} |
|
12744 | 313 |
text {\ttlbrace}* |
314 |
{\ttback}noindent The datatype induction rule generated here is |
|
315 |
of the form {\at}{\ttlbrace}thm [display] bintree.induct [no_vars]{\ttrbrace} |
|
316 |
*{\ttrbrace} |
|
12766 | 317 |
\end{ttbox}\vspace{-\medskipamount} |
12744 | 318 |
|
12746 | 319 |
\noindent Here we have augmented the theory by formal comments |
12766 | 320 |
(using \isakeyword{text} blocks), the informal parts may again refer |
321 |
to formal entities by means of ``antiquotations'' (such as |
|
12744 | 322 |
\texttt{\at}\verb,{text "'a bintree"}, or |
12746 | 323 |
\texttt{\at}\verb,{typ 'a},), see also \S\ref{sec:doc-prep-text}. |
67406 | 324 |
\<close> |
12645 | 325 |
|
326 |
||
67406 | 327 |
subsection \<open>Isabelle Sessions\<close> |
12629 | 328 |
|
67406 | 329 |
text \<open> |
12653 | 330 |
In contrast to the highly interactive mode of Isabelle/Isar theory |
331 |
development, the document preparation stage essentially works in |
|
12670 | 332 |
batch-mode. An Isabelle \bfindex{session} consists of a collection |
12766 | 333 |
of source files that may contribute to an output document. Each |
334 |
session is derived from a single parent, usually an object-logic |
|
335 |
image like \texttt{HOL}. This results in an overall tree structure, |
|
336 |
which is reflected by the output location in the file system |
|
54936 | 337 |
(the root directory is determined by the Isabelle settings variable |
338 |
\verb,ISABELLE_BROWSER_INFO,). |
|
12645 | 339 |
|
12683 | 340 |
\medskip The easiest way to manage Isabelle sessions is via |
51057 | 341 |
\texttt{isabelle mkroot} (to generate an initial session source |
342 |
setup) and \texttt{isabelle build} (to run sessions as specified in |
|
343 |
the corresponding \texttt{ROOT} file). These Isabelle tools are |
|
344 |
described in further detail in the \emph{Isabelle System Manual} |
|
60270 | 345 |
@{cite "isabelle-system"}. |
51057 | 346 |
|
347 |
For example, a new session \texttt{MySession} (with document |
|
348 |
preparation) may be produced as follows: |
|
12683 | 349 |
|
350 |
\begin{verbatim} |
|
67042
677cab7c2b85
adapted to changed ROOT syntax (see 13857f49d215);
wenzelm
parents:
61593
diff
changeset
|
351 |
isabelle mkroot MySession |
51057 | 352 |
isabelle build -D MySession |
12683 | 353 |
\end{verbatim} |
354 |
||
51057 | 355 |
The \texttt{isabelle build} job also informs about the file-system |
12685 | 356 |
location of the ultimate results. The above dry run should be able |
357 |
to produce some \texttt{document.pdf} (with dummy title, empty table |
|
12743 | 358 |
of contents etc.). Any failure at this stage usually indicates |
17183 | 359 |
technical problems of the {\LaTeX} installation. |
12683 | 360 |
|
361 |
\medskip The detailed arrangement of the session sources is as |
|
12746 | 362 |
follows. |
12645 | 363 |
|
364 |
\begin{itemize} |
|
365 |
||
12670 | 366 |
\item Directory \texttt{MySession} holds the required theory files |
367 |
$T@1$\texttt{.thy}, \dots, $T@n$\texttt{.thy}. |
|
12645 | 368 |
|
51057 | 369 |
\item File \texttt{MySession/ROOT} specifies the session options and |
370 |
content, with declarations for all wanted theories; it is sufficient |
|
371 |
to specify the terminal nodes of the theory dependency graph. |
|
12645 | 372 |
|
373 |
\item Directory \texttt{MySession/document} contains everything |
|
12653 | 374 |
required for the {\LaTeX} stage; only \texttt{root.tex} needs to be |
375 |
provided initially. |
|
12645 | 376 |
|
12653 | 377 |
The latter file holds appropriate {\LaTeX} code to commence a |
378 |
document (\verb,\documentclass, etc.), and to include the generated |
|
12743 | 379 |
files $T@i$\texttt{.tex} for each theory. Isabelle will generate a |
380 |
file \texttt{session.tex} holding {\LaTeX} commands to include all |
|
12746 | 381 |
generated theory output files in topologically sorted order, so |
382 |
\verb,\input{session}, in the body of \texttt{root.tex} does the job |
|
383 |
in most situations. |
|
12653 | 384 |
|
12645 | 385 |
\end{itemize} |
386 |
||
51057 | 387 |
One may now start to populate the directory \texttt{MySession} and |
388 |
its \texttt{ROOT} file accordingly. The file |
|
12766 | 389 |
\texttt{MySession/document/root.tex} should also be adapted at some |
12685 | 390 |
point; the default version is mostly self-explanatory. Note that |
391 |
\verb,\isabellestyle, enables fine-tuning of the general appearance |
|
392 |
of characters and mathematical symbols (see also |
|
393 |
\S\ref{sec:doc-prep-symbols}). |
|
12653 | 394 |
|
12685 | 395 |
Especially observe the included {\LaTeX} packages \texttt{isabelle} |
396 |
(mandatory), \texttt{isabellesym} (required for mathematical |
|
12743 | 397 |
symbols), and the final \texttt{pdfsetup} (provides sane defaults |
12764 | 398 |
for \texttt{hyperref}, including URL markup). All three are |
12743 | 399 |
distributed with Isabelle. Further packages may be required in |
12764 | 400 |
particular applications, say for unusual mathematical symbols. |
12645 | 401 |
|
12746 | 402 |
\medskip Any additional files for the {\LaTeX} stage go into the |
403 |
\texttt{MySession/document} directory as well. In particular, |
|
12766 | 404 |
adding a file named \texttt{root.bib} causes an automatic run of |
405 |
\texttt{bibtex} to process a bibliographic database; see also |
|
60270 | 406 |
\texttt{isabelle document} @{cite "isabelle-system"}. |
12645 | 407 |
|
12653 | 408 |
\medskip Any failure of the document preparation phase in an |
12670 | 409 |
Isabelle batch session leaves the generated sources in their target |
12766 | 410 |
location, identified by the accompanying error message. This lets |
411 |
you trace {\LaTeX} problems with the generated files at hand. |
|
67406 | 412 |
\<close> |
12645 | 413 |
|
414 |
||
67406 | 415 |
subsection \<open>Structure Markup\<close> |
12645 | 416 |
|
67406 | 417 |
text \<open> |
12653 | 418 |
The large-scale structure of Isabelle documents follows existing |
419 |
{\LaTeX} conventions, with chapters, sections, subsubsections etc. |
|
420 |
The Isar language includes separate \bfindex{markup commands}, which |
|
12681 | 421 |
do not affect the formal meaning of a theory (or proof), but result |
12665 | 422 |
in corresponding {\LaTeX} elements. |
12645 | 423 |
|
424 |
From the Isabelle perspective, each markup command takes a single |
|
69505 | 425 |
$text$ argument (delimited by \verb,",~\<open>\<dots>\<close>~\verb,", or |
426 |
\verb,{,\verb,*,~\<open>\<dots>\<close>~\verb,*,\verb,},). After stripping any |
|
12645 | 427 |
surrounding white space, the argument is passed to a {\LaTeX} macro |
12766 | 428 |
\verb,\isamarkupXYZ, for command \isakeyword{XYZ}. These macros are |
429 |
defined in \verb,isabelle.sty, according to the meaning given in the |
|
430 |
rightmost column above. |
|
12645 | 431 |
|
432 |
\medskip The following source fragment illustrates structure markup |
|
12653 | 433 |
of a theory. Note that {\LaTeX} labels may be included inside of |
434 |
section headings as well. |
|
12645 | 435 |
|
436 |
\begin{ttbox} |
|
58869 | 437 |
section {\ttlbrace}* Some properties of Foo Bar elements *{\ttrbrace} |
12645 | 438 |
|
15136 | 439 |
theory Foo_Bar |
15141 | 440 |
imports Main |
15136 | 441 |
begin |
12645 | 442 |
|
443 |
subsection {\ttlbrace}* Basic definitions *{\ttrbrace} |
|
444 |
||
27027 | 445 |
definition foo :: \dots |
12648 | 446 |
|
27027 | 447 |
definition bar :: \dots |
12648 | 448 |
|
12645 | 449 |
subsection {\ttlbrace}* Derived rules *{\ttrbrace} |
450 |
||
451 |
lemma fooI: \dots |
|
452 |
lemma fooE: \dots |
|
453 |
||
12648 | 454 |
subsection {\ttlbrace}* Main theorem {\ttback}label{\ttlbrace}sec:main-theorem{\ttrbrace} *{\ttrbrace} |
12645 | 455 |
|
456 |
theorem main: \dots |
|
457 |
||
458 |
end |
|
58869 | 459 |
\end{ttbox} |
67406 | 460 |
\<close> |
12645 | 461 |
|
462 |
||
67406 | 463 |
subsection \<open>Formal Comments and Antiquotations \label{sec:doc-prep-text}\<close> |
12645 | 464 |
|
67406 | 465 |
text \<open> |
12744 | 466 |
Isabelle \bfindex{source comments}, which are of the form |
69505 | 467 |
\verb,(,\verb,*,~\<open>\<dots>\<close>~\verb,*,\verb,),, essentially act like |
12746 | 468 |
white space and do not really contribute to the content. They |
469 |
mainly serve technical purposes to mark certain oddities in the raw |
|
470 |
input text. In contrast, \bfindex{formal comments} are portions of |
|
471 |
text that are associated with formal Isabelle/Isar commands |
|
12681 | 472 |
(\bfindex{marginal comments}), or as standalone paragraphs within a |
12665 | 473 |
theory or proof context (\bfindex{text blocks}). |
12659 | 474 |
|
475 |
\medskip Marginal comments are part of each command's concrete |
|
58620 | 476 |
syntax @{cite "isabelle-isar-ref"}; the common form is ``\verb,--,~$text$'' |
69505 | 477 |
where $text$ is delimited by \verb,",\<open>\<dots>\<close>\verb,", or |
478 |
\verb,{,\verb,*,~\<open>\<dots>\<close>~\verb,*,\verb,}, as before. Multiple |
|
12670 | 479 |
marginal comments may be given at the same time. Here is a simple |
480 |
example: |
|
67406 | 481 |
\<close> |
12665 | 482 |
|
483 |
lemma "A --> A" |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
67406
diff
changeset
|
484 |
\<comment> \<open>a triviality of propositional logic\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
67406
diff
changeset
|
485 |
\<comment> \<open>(should not really bother)\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
67406
diff
changeset
|
486 |
by (rule impI) \<comment> \<open>implicit assumption step involved here\<close> |
12665 | 487 |
|
67406 | 488 |
text \<open> |
12665 | 489 |
\noindent The above output has been produced as follows: |
12659 | 490 |
|
491 |
\begin{verbatim} |
|
492 |
lemma "A --> A" |
|
493 |
-- "a triviality of propositional logic" |
|
494 |
-- "(should not really bother)" |
|
495 |
by (rule impI) -- "implicit assumption step involved here" |
|
496 |
\end{verbatim} |
|
497 |
||
12670 | 498 |
From the {\LaTeX} viewpoint, ``\verb,--,'' acts like a markup |
499 |
command, associated with the macro \verb,\isamarkupcmt, (taking a |
|
500 |
single argument). |
|
12659 | 501 |
|
12665 | 502 |
\medskip Text blocks are introduced by the commands \bfindex{text} |
59005 | 503 |
and \bfindex{txt}. Each takes again a single $text$ argument, |
504 |
which is interpreted as a free-form paragraph in {\LaTeX} |
|
505 |
(surrounded by some additional vertical space). The typesetting |
|
506 |
may be changed by redefining the {\LaTeX} environments of |
|
507 |
\verb,isamarkuptext, or \verb,isamarkuptxt,, respectively |
|
508 |
(via \verb,\renewenvironment,). |
|
12659 | 509 |
|
12766 | 510 |
\medskip The $text$ part of Isabelle markup commands essentially |
511 |
inserts \emph{quoted material} into a formal text, mainly for |
|
512 |
instruction of the reader. An \bfindex{antiquotation} is again a |
|
513 |
formal object embedded into such an informal portion. The |
|
514 |
interpretation of antiquotations is limited to some well-formedness |
|
515 |
checks, with the result being pretty printed to the resulting |
|
516 |
document. Quoted text blocks together with antiquotations provide |
|
517 |
an attractive means of referring to formal entities, with good |
|
518 |
confidence in getting the technical details right (especially syntax |
|
519 |
and types). |
|
12659 | 520 |
|
12665 | 521 |
The general syntax of antiquotations is as follows: |
12659 | 522 |
\texttt{{\at}{\ttlbrace}$name$ $arguments${\ttrbrace}}, or |
523 |
\texttt{{\at}{\ttlbrace}$name$ [$options$] $arguments${\ttrbrace}} |
|
12665 | 524 |
for a comma-separated list of options consisting of a $name$ or |
12766 | 525 |
\texttt{$name$=$value$} each. The syntax of $arguments$ depends on |
526 |
the kind of antiquotation, it generally follows the same conventions |
|
527 |
for types, terms, or theorems as in the formal part of a theory. |
|
12645 | 528 |
|
12766 | 529 |
\medskip This sentence demonstrates quotations and antiquotations: |
69597 | 530 |
\<^term>\<open>%x y. x\<close> is a well-typed term. |
12659 | 531 |
|
12764 | 532 |
\medskip\noindent The output above was produced as follows: |
12659 | 533 |
\begin{ttbox} |
534 |
text {\ttlbrace}* |
|
12764 | 535 |
This sentence demonstrates quotations and antiquotations: |
12659 | 536 |
{\at}{\ttlbrace}term "%x y. x"{\ttrbrace} is a well-typed term. |
537 |
*{\ttrbrace} |
|
12766 | 538 |
\end{ttbox}\vspace{-\medskipamount} |
12659 | 539 |
|
12764 | 540 |
The notational change from the ASCII character~\verb,%, to the |
69505 | 541 |
symbol~\<open>\<lambda>\<close> reveals that Isabelle printed this term, after |
12766 | 542 |
parsing and type-checking. Document preparation enables symbolic |
543 |
output by default. |
|
12659 | 544 |
|
16523 | 545 |
\medskip The next example includes an option to show the type of all |
546 |
variables. The antiquotation |
|
12766 | 547 |
\texttt{{\at}}\verb,{term [show_types] "%x y. x"}, produces the |
548 |
output @{term [show_types] "%x y. x"}. Type inference has figured |
|
549 |
out the most general typings in the present theory context. Terms |
|
550 |
may acquire different typings due to constraints imposed by their |
|
551 |
environment; within a proof, for example, variables are given the |
|
552 |
same types as they have in the main goal statement. |
|
12659 | 553 |
|
12764 | 554 |
\medskip Several further kinds of antiquotations and options are |
58620 | 555 |
available @{cite "isabelle-isar-ref"}. Here are a few commonly used |
12670 | 556 |
combinations: |
12659 | 557 |
|
558 |
\medskip |
|
12651 | 559 |
|
12659 | 560 |
\begin{tabular}{ll} |
561 |
\texttt{\at}\verb,{typ,~$\tau$\verb,}, & print type $\tau$ \\ |
|
25338 | 562 |
\texttt{\at}\verb,{const,~$c$\verb,}, & check existence of $c$ and print it \\ |
12659 | 563 |
\texttt{\at}\verb,{term,~$t$\verb,}, & print term $t$ \\ |
564 |
\texttt{\at}\verb,{prop,~$\phi$\verb,}, & print proposition $\phi$ \\ |
|
12665 | 565 |
\texttt{\at}\verb,{prop [display],~$\phi$\verb,}, & print large proposition $\phi$ (with linebreaks) \\ |
12659 | 566 |
\texttt{\at}\verb,{prop [source],~$\phi$\verb,}, & check proposition $\phi$, print its input \\ |
567 |
\texttt{\at}\verb,{thm,~$a$\verb,}, & print fact $a$ \\ |
|
568 |
\texttt{\at}\verb,{thm,~$a$~\verb,[no_vars]}, & print fact $a$, fixing schematic variables \\ |
|
12746 | 569 |
\texttt{\at}\verb,{thm [source],~$a$\verb,}, & check availability of fact $a$, print its name \\ |
12659 | 570 |
\texttt{\at}\verb,{text,~$s$\verb,}, & print uninterpreted text $s$ \\ |
571 |
\end{tabular} |
|
572 |
||
573 |
\medskip |
|
574 |
||
12665 | 575 |
Note that \attrdx{no_vars} given above is \emph{not} an |
576 |
antiquotation option, but an attribute of the theorem argument given |
|
577 |
here. This might be useful with a diagnostic command like |
|
578 |
\isakeyword{thm}, too. |
|
12659 | 579 |
|
12665 | 580 |
\medskip The \texttt{\at}\verb,{text, $s$\verb,}, antiquotation is |
12659 | 581 |
particularly interesting. Embedding uninterpreted text within an |
12665 | 582 |
informal body might appear useless at first sight. Here the key |
583 |
virtue is that the string $s$ is processed as Isabelle output, |
|
584 |
interpreting Isabelle symbols appropriately. |
|
12659 | 585 |
|
69505 | 586 |
For example, \texttt{\at}\verb,{text "\<forall>\<exists>"}, produces \<open>\<forall>\<exists>\<close>, according to the standard interpretation of these symbol |
12665 | 587 |
(cf.\ \S\ref{sec:doc-prep-symbols}). Thus we achieve consistent |
12659 | 588 |
mathematical notation in both the formal and informal parts of the |
12766 | 589 |
document very easily, independently of the term language of |
590 |
Isabelle. Manual {\LaTeX} code would leave more control over the |
|
591 |
typesetting, but is also slightly more tedious. |
|
67406 | 592 |
\<close> |
12645 | 593 |
|
594 |
||
67406 | 595 |
subsection \<open>Interpretation of Symbols \label{sec:doc-prep-symbols}\<close> |
12645 | 596 |
|
67406 | 597 |
text \<open> |
12665 | 598 |
As has been pointed out before (\S\ref{sec:syntax-symbols}), |
12670 | 599 |
Isabelle symbols are the smallest syntactic entities --- a |
12681 | 600 |
straightforward generalization of ASCII characters. While Isabelle |
12665 | 601 |
does not impose any interpretation of the infinite collection of |
12764 | 602 |
named symbols, {\LaTeX} documents use canonical glyphs for certain |
58620 | 603 |
standard symbols @{cite "isabelle-isar-ref"}. |
12659 | 604 |
|
12766 | 605 |
The {\LaTeX} code produced from Isabelle text follows a simple |
606 |
scheme. You can tune the final appearance by redefining certain |
|
607 |
macros, say in \texttt{root.tex} of the document. |
|
12670 | 608 |
|
609 |
\begin{enumerate} |
|
12659 | 610 |
|
12670 | 611 |
\item 7-bit ASCII characters: letters \texttt{A\dots Z} and |
12746 | 612 |
\texttt{a\dots z} are output directly, digits are passed as an |
12670 | 613 |
argument to the \verb,\isadigit, macro, other characters are |
614 |
replaced by specifically named macros of the form |
|
12665 | 615 |
\verb,\isacharXYZ,. |
12659 | 616 |
|
12766 | 617 |
\item Named symbols: \verb,\,\verb,<XYZ>, is turned into |
618 |
\verb,{\isasymXYZ},; note the additional braces. |
|
12659 | 619 |
|
12766 | 620 |
\item Named control symbols: \verb,\,\verb,<^XYZ>, is turned into |
621 |
\verb,\isactrlXYZ,; subsequent symbols may act as arguments if the |
|
622 |
control macro is defined accordingly. |
|
12670 | 623 |
|
12659 | 624 |
\end{enumerate} |
12665 | 625 |
|
12764 | 626 |
You may occasionally wish to give new {\LaTeX} interpretations of |
627 |
named symbols. This merely requires an appropriate definition of |
|
12766 | 628 |
\verb,\isasymXYZ,, for \verb,\,\verb,<XYZ>, (see |
12746 | 629 |
\texttt{isabelle.sty} for working examples). Control symbols are |
630 |
slightly more difficult to get right, though. |
|
12665 | 631 |
|
632 |
\medskip The \verb,\isabellestyle, macro provides a high-level |
|
633 |
interface to tune the general appearance of individual symbols. For |
|
12670 | 634 |
example, \verb,\isabellestyle{it}, uses the italics text style to |
635 |
mimic the general appearance of the {\LaTeX} math mode; double |
|
12743 | 636 |
quotes are not printed at all. The resulting quality of typesetting |
637 |
is quite good, so this should be the default style for work that |
|
638 |
gets distributed to a broader audience. |
|
67406 | 639 |
\<close> |
12645 | 640 |
|
641 |
||
67406 | 642 |
subsection \<open>Suppressing Output \label{sec:doc-prep-suppress}\<close> |
12645 | 643 |
|
67406 | 644 |
text \<open> |
12748 | 645 |
By default, Isabelle's document system generates a {\LaTeX} file for |
646 |
each theory that gets loaded while running the session. The |
|
647 |
generated \texttt{session.tex} will include all of these in order of |
|
648 |
appearance, which in turn gets included by the standard |
|
12743 | 649 |
\texttt{root.tex}. Certainly one may change the order or suppress |
12746 | 650 |
unwanted theories by ignoring \texttt{session.tex} and load |
651 |
individual files directly in \texttt{root.tex}. On the other hand, |
|
652 |
such an arrangement requires additional maintenance whenever the |
|
653 |
collection of theories changes. |
|
12648 | 654 |
|
655 |
Alternatively, one may tune the theory loading process in |
|
51057 | 656 |
\texttt{ROOT} itself: some sequential order of \textbf{theories} |
657 |
sections may enforce a certain traversal of the dependency graph, |
|
658 |
although this could degrade parallel processing. The nodes of each |
|
659 |
sub-graph that is specified here are presented in some topological |
|
660 |
order of their formal dependencies. |
|
661 |
||
662 |
Moreover, the system build option \verb,document=false, allows to |
|
663 |
disable document generation for some theories. Its usage in the |
|
664 |
session \texttt{ROOT} is like this: |
|
12648 | 665 |
|
666 |
\begin{verbatim} |
|
51057 | 667 |
theories [document = false] T |
12648 | 668 |
\end{verbatim} |
12645 | 669 |
|
17183 | 670 |
\medskip Theory output may be suppressed more selectively, either |
671 |
via \bfindex{tagged command regions} or \bfindex{ignored material}. |
|
12648 | 672 |
|
17183 | 673 |
Tagged command regions works by annotating commands with named tags, |
674 |
which correspond to certain {\LaTeX} markup that tells how to treat |
|
675 |
particular parts of a document when doing the actual type-setting. |
|
676 |
By default, certain Isabelle/Isar commands are implicitly marked up |
|
677 |
using the predefined tags ``\emph{theory}'' (for theory begin and |
|
678 |
end), ``\emph{proof}'' (for proof commands), and ``\emph{ML}'' (for |
|
679 |
commands involving ML code). Users may add their own tags using the |
|
680 |
\verb,%,\emph{tag} notation right after a command name. In the |
|
681 |
subsequent example we hide a particularly irrelevant proof: |
|
67406 | 682 |
\<close> |
12648 | 683 |
|
17183 | 684 |
lemma "x = x" by %invisible (simp) |
12648 | 685 |
|
67406 | 686 |
text \<open> |
17183 | 687 |
The original source has been ``\verb,lemma "x = x" by %invisible (simp),''. |
688 |
Tags observe the structure of proofs; adjacent commands with the |
|
689 |
same tag are joined into a single region. The Isabelle document |
|
690 |
preparation system allows the user to specify how to interpret a |
|
691 |
tagged region, in order to keep, drop, or fold the corresponding |
|
692 |
parts of the document. See the \emph{Isabelle System Manual} |
|
60270 | 693 |
@{cite "isabelle-system"} for further details, especially on |
51057 | 694 |
\texttt{isabelle build} and \texttt{isabelle document}. |
12648 | 695 |
|
17183 | 696 |
Ignored material is specified by delimiting the original formal |
697 |
source with special source comments |
|
698 |
\verb,(,\verb,*,\verb,<,\verb,*,\verb,), and |
|
699 |
\verb,(,\verb,*,\verb,>,\verb,*,\verb,),. These parts are stripped |
|
700 |
before the type-setting phase, without affecting the formal checking |
|
701 |
of the theory, of course. For example, we may hide parts of a proof |
|
702 |
that seem unfit for general public inspection. The following |
|
703 |
``fully automatic'' proof is actually a fake: |
|
67406 | 704 |
\<close> |
12651 | 705 |
|
706 |
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
|
707 |
by (auto(*<*)simp add: zero_less_mult_iff(*>*)) |
12651 | 708 |
|
67406 | 709 |
text \<open> |
17183 | 710 |
\noindent The real source of the proof has been as follows: |
12651 | 711 |
|
712 |
\begin{verbatim} |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
13439
diff
changeset
|
713 |
by (auto(*<*)simp add: zero_less_mult_iff(*>*)) |
12659 | 714 |
\end{verbatim} |
715 |
%(* |
|
12651 | 716 |
|
12766 | 717 |
\medskip Suppressing portions of printed text demands care. You |
718 |
should not misrepresent the underlying theory development. It is |
|
719 |
easy to invalidate the visible text by hiding references to |
|
17183 | 720 |
questionable axioms, for example. |
67406 | 721 |
\<close> |
12629 | 722 |
|
11647 | 723 |
(*<*) |
724 |
end |
|
725 |
(*>*) |