11647
|
1 |
(*<*)
|
|
2 |
theory Documents = Main:
|
|
3 |
(*>*)
|
|
4 |
|
12629
|
5 |
section {* Concrete syntax \label{sec:concrete-syntax} *}
|
|
6 |
|
|
7 |
text {*
|
|
8 |
Concerning Isabelle's ``inner'' language of simply-typed @{text
|
|
9 |
\<lambda>}-calculus, the core concept of Isabelle's elaborate infrastructure
|
|
10 |
for concrete syntax is that of general \emph{mixfix
|
|
11 |
annotations}\index{mixfix annotations|bold}. Associated with any
|
|
12 |
kind of name and type declaration, mixfixes give rise both to
|
|
13 |
grammar productions for the parser and output templates for the
|
|
14 |
pretty printer.
|
|
15 |
|
|
16 |
In full generality, the whole affair of parser and pretty printer
|
|
17 |
configuration is rather subtle. Any syntax specifications given by
|
|
18 |
end-users need to interact properly with the existing setup of
|
|
19 |
Isabelle/Pure and Isabelle/HOL; see \cite{isabelle-ref} for further
|
|
20 |
details. It is particularly important to get the precedence of new
|
|
21 |
syntactic constructs right, avoiding ambiguities with existing
|
|
22 |
elements.
|
|
23 |
|
|
24 |
\medskip Subsequently we introduce a few simple declaration forms
|
|
25 |
that already cover the most common situations fairly well.
|
|
26 |
*}
|
|
27 |
|
|
28 |
|
|
29 |
subsection {* Infixes *}
|
|
30 |
|
|
31 |
text {*
|
|
32 |
Syntax annotations may be included wherever constants are declared
|
|
33 |
directly or indirectly, including \isacommand{consts},
|
|
34 |
\isacommand{constdefs}, or \isacommand{datatype} (for the
|
|
35 |
constructor operations). Type-constructors may be annotated as
|
|
36 |
well, although this is less frequently encountered in practice
|
|
37 |
(@{text "*"} and @{text "+"} types may come to mind).
|
|
38 |
|
|
39 |
Infix declarations\index{infix annotations|bold} provide a useful
|
|
40 |
special case of mixfixes, where users need not care about the full
|
|
41 |
details of priorities, nesting, spacing, etc. The subsequent
|
|
42 |
example of the exclusive-or operation on boolean values illustrates
|
|
43 |
typical infix declarations.
|
|
44 |
*}
|
|
45 |
|
|
46 |
constdefs
|
|
47 |
xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "[+]" 60)
|
|
48 |
"A [+] B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
|
|
49 |
|
|
50 |
text {*
|
|
51 |
Any curried function with at least two arguments may be associated
|
|
52 |
with infix syntax: @{text "xor A B"} and @{text "A [+] B"} refer to
|
|
53 |
the same expression internally. In partial applications with less
|
|
54 |
than two operands there is a special notation with \isa{op} prefix:
|
|
55 |
@{text xor} without arguments is represented as @{text "op [+]"};
|
|
56 |
combined with plain prefix application this turns @{text "xor A"}
|
|
57 |
into @{text "op [+] A"}.
|
|
58 |
|
|
59 |
\medskip The string @{text [source] "[+]"} in the above declaration
|
|
60 |
refers to the bit of concrete syntax to represent the operator,
|
|
61 |
while the number @{text 60} determines the precedence of the whole
|
|
62 |
construct.
|
|
63 |
|
|
64 |
As it happens, Isabelle/HOL already spends many popular combinations
|
|
65 |
of ASCII symbols for its own use, including both @{text "+"} and
|
|
66 |
@{text "++"}. Slightly more awkward combinations like the present
|
|
67 |
@{text "[+]"} tend to be available for user extensions. The current
|
|
68 |
arrangement of inner syntax may be inspected via
|
|
69 |
\commdx{print\protect\_syntax}, albeit its output is enormous.
|
|
70 |
|
|
71 |
Operator precedence also needs some special considerations. The
|
|
72 |
admissible range is 0--1000. Very low or high priorities are
|
|
73 |
basically reserved for the meta-logic. Syntax of Isabelle/HOL
|
|
74 |
mainly uses the range of 10--100: the equality infix @{text "="} is
|
|
75 |
centered at 50, logical connectives (like @{text "\<or>"} and @{text
|
|
76 |
"\<and>"}) are below 50, and algebraic ones (like @{text "+"} and @{text
|
|
77 |
"*"}) above 50. User syntax should strive to coexist with common
|
|
78 |
HOL forms, or use the mostly unused range 100--900.
|
|
79 |
|
|
80 |
\medskip The keyword \isakeyword{infixl} specifies an operator that
|
|
81 |
is nested to the \emph{left}: in iterated applications the more
|
|
82 |
complex expression appears on the left-hand side: @{term "A [+] B
|
|
83 |
[+] C"} stands for @{text "(A [+] B) [+] C"}. Similarly,
|
12635
|
84 |
\isakeyword{infixr} refers to nesting to the \emph{right}, reading
|
|
85 |
@{term "A [+] B [+] C"} as @{text "A [+] (B [+] C)"}. In contrast,
|
|
86 |
a \emph{non-oriented} declaration via \isakeyword{infix} would
|
|
87 |
always demand explicit parentheses.
|
12629
|
88 |
|
|
89 |
Many binary operations observe the associative law, so the exact
|
|
90 |
grouping does not matter. Nevertheless, formal statements need be
|
|
91 |
given in a particular format, associativity needs to be treated
|
|
92 |
explicitly within the logic. Exclusive-or is happens to be
|
|
93 |
associative, as shown below.
|
|
94 |
*}
|
|
95 |
|
|
96 |
lemma xor_assoc: "(A [+] B) [+] C = A [+] (B [+] C)"
|
|
97 |
by (auto simp add: xor_def)
|
|
98 |
|
|
99 |
text {*
|
|
100 |
Such rules may be used in simplification to regroup nested
|
|
101 |
expressions as required. Note that the system would actually print
|
|
102 |
the above statement as @{term "A [+] B [+] C = A [+] (B [+] C)"}
|
|
103 |
(due to nesting to the left). We have preferred to give the fully
|
12635
|
104 |
parenthesized form in the text for clarity. Only in rare situations
|
|
105 |
one may consider to force parentheses by use of non-oriented infix
|
|
106 |
syntax; equality would probably be a typical candidate.
|
12629
|
107 |
*}
|
|
108 |
|
12635
|
109 |
|
12629
|
110 |
subsection {* Mathematical symbols \label{sec:thy-present-symbols} *}
|
|
111 |
|
|
112 |
text {*
|
12635
|
113 |
Concrete syntax based on plain ASCII characters has its inherent
|
|
114 |
limitations. Rich mathematical notation demands a larger repertoire
|
|
115 |
of symbols. Several standards of extended character sets have been
|
|
116 |
proposed over decades, but none has become universally available so
|
|
117 |
far, not even Unicode\index{Unicode}.
|
|
118 |
|
|
119 |
Isabelle supports a generic notion of
|
|
120 |
\emph{symbols}\index{symbols|bold} as the smallest entities of
|
|
121 |
source text, without referring to internal encodings. Such
|
|
122 |
``generalized characters'' may be of one of the following three
|
|
123 |
kinds:
|
|
124 |
|
|
125 |
\begin{enumerate}
|
|
126 |
|
|
127 |
\item Traditional 7-bit ASCII characters.
|
|
128 |
|
|
129 |
\item Named symbols: \verb,\,\verb,<,$ident$\verb,>, (or
|
|
130 |
\verb,\\,\verb,<,$ident$\verb,>,).
|
12629
|
131 |
|
12635
|
132 |
\item Named control symbols: \verb,\,\verb,<^,$ident$\verb,>, (or
|
|
133 |
\verb,\\,\verb,<^,$ident$\verb,>,).
|
|
134 |
|
|
135 |
\end{enumerate}
|
|
136 |
|
|
137 |
Here $ident$ may be any identifier according to the usual Isabelle
|
|
138 |
conventions. This results in an infinite store of symbols, whose
|
|
139 |
interpretation is left to further front-end tools. For example, the
|
|
140 |
\verb,\,\verb,<forall>, symbol of Isabelle is really displayed as
|
|
141 |
$\forall$ --- both by the user-interface of Proof~General + X-Symbol
|
|
142 |
and the Isabelle document processor (see \S\ref{FIXME}).
|
|
143 |
|
|
144 |
A list of standard Isabelle symbols is given in
|
|
145 |
\cite[appendix~A]{isabelle-sys}. Users may introduce their own
|
|
146 |
interpretation of further symbols by configuring the appropriate
|
|
147 |
front-end tool accordingly, e.g.\ defining appropriate {\LaTeX}
|
|
148 |
macros for document preparation. There are also a few predefined
|
|
149 |
control symbols, such as \verb,\,\verb,<^sub>, and
|
|
150 |
\verb,\,\verb,<^sup>, for sub- and superscript of the subsequent
|
|
151 |
(printable) symbol, respectively.
|
|
152 |
|
|
153 |
\medskip The following version of our @{text xor} definition uses a
|
|
154 |
standard Isabelle symbol to achieve typographically pleasing output.
|
12629
|
155 |
*}
|
|
156 |
|
|
157 |
(*<*)
|
|
158 |
hide const xor
|
|
159 |
ML_setup {* Context.>> (Theory.add_path "1") *}
|
|
160 |
(*>*)
|
|
161 |
constdefs
|
|
162 |
xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "\<oplus>" 60)
|
|
163 |
"A \<oplus> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
|
12635
|
164 |
(*<*)
|
|
165 |
local
|
|
166 |
(*>*)
|
12629
|
167 |
|
12635
|
168 |
text {*
|
|
169 |
The X-Symbol package within Proof~General provides several input
|
|
170 |
methods to enter @{text \<oplus>} in the text. If all fails one may just
|
|
171 |
type \verb,\,\verb,<oplus>, by hand; the display is adapted
|
|
172 |
immediately after continuing further input.
|
|
173 |
|
|
174 |
\medskip A slightly more refined scheme is to provide alternative
|
|
175 |
syntax via the \emph{print mode}\index{print mode} concept of
|
|
176 |
Isabelle (see also \cite{isabelle-ref}). By convention, the mode
|
|
177 |
``$xsymbols$'' is enabled whenever X-Symbol is active. Consider the
|
|
178 |
following hybrid declaration of @{text xor}.
|
|
179 |
*}
|
|
180 |
|
|
181 |
(*<*)
|
|
182 |
hide const xor
|
|
183 |
ML_setup {* Context.>> (Theory.add_path "2") *}
|
|
184 |
(*>*)
|
|
185 |
constdefs
|
|
186 |
xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "[+]\<ignore>" 60)
|
|
187 |
"A [+]\<ignore> B \<equiv> (A \<and> \<not> B) \<or> (\<not> A \<and> B)"
|
|
188 |
|
|
189 |
syntax (xsymbols)
|
|
190 |
xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "\<oplus>\<ignore>" 60)
|
12629
|
191 |
(*<*)
|
|
192 |
local
|
|
193 |
(*>*)
|
|
194 |
|
12635
|
195 |
text {*
|
|
196 |
Here the \commdx{syntax} command acts like \isakeyword{consts}, but
|
|
197 |
without declaring a logical constant, and with an optional print
|
|
198 |
mode specification. Note that the type declaration given here
|
|
199 |
merely serves for syntactic purposes, and is not checked for
|
|
200 |
consistency with the real constant.
|
|
201 |
|
|
202 |
\medskip Now we may write either @{text "[+]"} or @{text "\<oplus>"} in
|
|
203 |
input, while output uses the nicer syntax of $xsymbols$, provided
|
|
204 |
that print mode is presently active. This scheme is particularly
|
|
205 |
useful for interactive development, with the user typing plain ASCII
|
|
206 |
text, but gaining improved visual feedback from the system (say in
|
|
207 |
current goal output).
|
|
208 |
|
|
209 |
\begin{warn}
|
|
210 |
Using alternative syntax declarations easily results in varying
|
|
211 |
versions of input sources. Isabelle provides no systematic way to
|
|
212 |
convert alternative expressions back and forth. Print modes only
|
|
213 |
affect situations where formal entities are pretty printed by the
|
|
214 |
Isabelle process (e.g.\ output of terms and types), but not the
|
|
215 |
original theory text.
|
|
216 |
\end{warn}
|
|
217 |
|
|
218 |
\medskip The following variant makes the alternative @{text \<oplus>}
|
|
219 |
notation only available for output. Thus we may enforce input
|
|
220 |
sources to refer to plain ASCII only.
|
|
221 |
*}
|
|
222 |
|
|
223 |
syntax (xsymbols output)
|
|
224 |
xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" (infixl "\<oplus>\<ignore>" 60)
|
|
225 |
|
12629
|
226 |
|
|
227 |
subsection {* Prefixes *}
|
|
228 |
|
|
229 |
text {*
|
12635
|
230 |
Prefix syntax annotations\index{prefix annotation|bold} are just a
|
|
231 |
very degenerate of the general mixfix form \cite{isabelle-ref},
|
|
232 |
without any template arguments or priorities --- just some piece of
|
|
233 |
literal syntax.
|
|
234 |
|
|
235 |
The following example illustrates this idea idea by associating
|
|
236 |
common symbols with the constructors of a currency datatype.
|
12629
|
237 |
*}
|
|
238 |
|
|
239 |
datatype currency =
|
|
240 |
Euro nat ("\<euro>")
|
|
241 |
| Pounds nat ("\<pounds>")
|
|
242 |
| Yen nat ("\<yen>")
|
|
243 |
| Dollar nat ("$")
|
|
244 |
|
|
245 |
text {*
|
12635
|
246 |
Here the degenerate mixfix annotations on the rightmost column
|
|
247 |
happen to consist of a single Isabelle symbol each:
|
|
248 |
\verb,\,\verb,<euro>,, \verb,\,\verb,<pounds>,,
|
|
249 |
\verb,\,\verb,<yen>,, and \verb,\,$,.
|
|
250 |
|
|
251 |
Recall that a constructor like @{text Euro} actually is a function
|
|
252 |
@{typ "nat \<Rightarrow> currency"}. An expression like @{text "Euro 10"} will
|
|
253 |
be printed as @{term "\<euro> 10"}. Merely the head of the application is
|
|
254 |
subject to our trivial concrete syntax; this form is sufficient to
|
|
255 |
achieve fair conformance to EU~Commission standards of currency
|
|
256 |
notation.
|
12629
|
257 |
|
12635
|
258 |
\medskip Certainly, the same idea of prefix syntax also works for
|
|
259 |
\isakeyword{consts}, \isakeyword{constdefs} etc. For example, we
|
|
260 |
might introduce a (slightly unrealistic) function to calculate an
|
|
261 |
abstract currency value, by cases on the datatype constructors and
|
|
262 |
fixed exchange rates.
|
|
263 |
*}
|
|
264 |
|
|
265 |
consts
|
|
266 |
currency :: "currency \<Rightarrow> nat" ("\<currency>")
|
|
267 |
|
|
268 |
text {*
|
|
269 |
\noindent The funny symbol encountered here is that of
|
|
270 |
\verb,\<currency>,.
|
12629
|
271 |
*}
|
|
272 |
|
|
273 |
|
|
274 |
subsection {* Syntax translations \label{sec:def-translations} *}
|
|
275 |
|
|
276 |
text{*
|
|
277 |
FIXME
|
|
278 |
|
|
279 |
\index{syntax translations|(}%
|
|
280 |
\index{translations@\isacommand {translations} (command)|(}
|
|
281 |
Isabelle offers an additional definitional facility,
|
|
282 |
\textbf{syntax translations}.
|
|
283 |
They resemble macros: upon parsing, the defined concept is immediately
|
|
284 |
replaced by its definition. This effect is reversed upon printing. For example,
|
|
285 |
the symbol @{text"\<noteq>"} is defined via a syntax translation:
|
|
286 |
*}
|
|
287 |
|
|
288 |
translations "x \<noteq> y" \<rightleftharpoons> "\<not>(x = y)"
|
|
289 |
|
|
290 |
text{*\index{$IsaEqTrans@\isasymrightleftharpoons}
|
|
291 |
\noindent
|
|
292 |
Internally, @{text"\<noteq>"} never appears.
|
|
293 |
|
|
294 |
In addition to @{text"\<rightleftharpoons>"} there are
|
|
295 |
@{text"\<rightharpoonup>"}\index{$IsaEqTrans1@\isasymrightharpoonup}
|
|
296 |
and @{text"\<leftharpoondown>"}\index{$IsaEqTrans2@\isasymleftharpoondown}
|
|
297 |
for uni-directional translations, which only affect
|
|
298 |
parsing or printing. This tutorial will not cover the details of
|
|
299 |
translations. We have mentioned the concept merely because it
|
|
300 |
crops up occasionally; a number of HOL's built-in constructs are defined
|
|
301 |
via translations. Translations are preferable to definitions when the new
|
|
302 |
concept is a trivial variation on an existing one. For example, we
|
|
303 |
don't need to derive new theorems about @{text"\<noteq>"}, since existing theorems
|
|
304 |
about @{text"="} still apply.%
|
|
305 |
\index{syntax translations|)}%
|
|
306 |
\index{translations@\isacommand {translations} (command)|)}
|
|
307 |
*}
|
|
308 |
|
|
309 |
|
|
310 |
section {* Document preparation *}
|
|
311 |
|
|
312 |
subsection {* Batch-mode sessions *}
|
|
313 |
|
|
314 |
subsection {* {\LaTeX} macros *}
|
|
315 |
|
|
316 |
subsubsection {* Structure markup *}
|
|
317 |
|
|
318 |
subsubsection {* Symbols and characters *}
|
|
319 |
|
|
320 |
text {*
|
|
321 |
FIXME
|
|
322 |
|
|
323 |
|
|
324 |
*}
|
|
325 |
|
11647
|
326 |
(*<*)
|
|
327 |
end
|
|
328 |
(*>*)
|