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