1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Translations}% |
|
4 \isamarkupfalse% |
|
5 % |
|
6 \isamarkupsubsection{Syntax Translations% |
|
7 } |
|
8 \isamarkuptrue% |
|
9 % |
|
10 \begin{isamarkuptext}% |
|
11 \label{sec:def-translations} |
|
12 \index{syntax translations|(}% |
|
13 \index{translations@\isacommand {translations} (command)|(} |
|
14 Isabelle offers an additional definitional facility, |
|
15 \textbf{syntax translations}. |
|
16 They resemble macros: upon parsing, the defined concept is immediately |
|
17 replaced by its definition. This effect is reversed upon printing. For example, |
|
18 the symbol \isa{{\isasymnoteq}} is defined via a syntax translation:% |
|
19 \end{isamarkuptext}% |
|
20 \isamarkuptrue% |
|
21 \isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}{\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
22 % |
|
23 \begin{isamarkuptext}% |
|
24 \index{$IsaEqTrans@\isasymrightleftharpoons} |
|
25 \noindent |
|
26 Internally, \isa{{\isasymnoteq}} never appears. |
|
27 |
|
28 In addition to \isa{{\isasymrightleftharpoons}} there are |
|
29 \isa{{\isasymrightharpoonup}}\index{$IsaEqTrans1@\isasymrightharpoonup} |
|
30 and \isa{{\isasymleftharpoondown}}\index{$IsaEqTrans2@\isasymleftharpoondown} |
|
31 for uni-directional translations, which only affect |
|
32 parsing or printing. This tutorial will not cover the details of |
|
33 translations. We have mentioned the concept merely because it |
|
34 crops up occasionally; a number of HOL's built-in constructs are defined |
|
35 via translations. Translations are preferable to definitions when the new |
|
36 concept is a trivial variation on an existing one. For example, we |
|
37 don't need to derive new theorems about \isa{{\isasymnoteq}}, since existing theorems |
|
38 about \isa{{\isacharequal}} still apply.% |
|
39 \index{syntax translations|)}% |
|
40 \index{translations@\isacommand {translations} (command)|)}% |
|
41 \end{isamarkuptext}% |
|
42 \isamarkuptrue% |
|
43 \isamarkupfalse% |
|
44 \end{isabellebody}% |
|
45 %%% Local Variables: |
|
46 %%% mode: latex |
|
47 %%% TeX-master: "root" |
|
48 %%% End: |
|