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