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