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