11208
|
1 |
(*<*)
|
|
2 |
theory Translations = Main:
|
|
3 |
(*>*)
|
|
4 |
subsection{*Syntax Translations*}
|
|
5 |
|
|
6 |
text{*\label{sec:def-translations}
|
|
7 |
Isabelle offers an additional definition-like facility,
|
|
8 |
\textbf{syntax translations}\indexbold{syntax translation}.
|
11211
|
9 |
They resemble macros: upon parsing, the defined concept is immediately
|
11208
|
10 |
replaced by its definition, and this is reversed upon printing. For example,
|
|
11 |
the symbol @{text"\<noteq>"} is defined via a syntax translation:
|
|
12 |
*}
|
|
13 |
|
|
14 |
translations "x \<noteq> y" \<rightleftharpoons> "\<not>(x = y)"
|
|
15 |
|
|
16 |
text{*\indexbold{*translations}\indexbold{$IsaEqTrans@\isasymrightleftharpoons}
|
|
17 |
\noindent
|
|
18 |
Internally, @{text"\<noteq>"} never appears.
|
|
19 |
|
|
20 |
In addition to @{text"\<rightleftharpoons>"} there are
|
|
21 |
@{text"\<rightharpoonup>"}\indexbold{$IsaEqTrans1@\isasymrightharpoonup}
|
|
22 |
and @{text"\<leftharpoondown>"}\indexbold{$IsaEqTrans2@\isasymleftharpoondown}
|
11211
|
23 |
for uni-directional translations, which only affect
|
|
24 |
parsing or printing. We do not want to cover the details of
|
11208
|
25 |
translations at this point. We haved mentioned the concept merely because it
|
11211
|
26 |
crops up occasionally: a number of HOL's built-in constructs are defined
|
|
27 |
via translations. Translations are preferable to definitions when the new
|
|
28 |
concept is a trivial variation on an existing one. For example, we
|
|
29 |
don't need to derive new theorems about @{text"\<noteq>"}, since existing theorems
|
|
30 |
about @{text"="} still apply.
|
|
31 |
*}
|
11208
|
32 |
|
|
33 |
(*<*)
|
|
34 |
end
|
|
35 |
(*>*)
|