5 \isamarkupsubsection{Syntax Translations% |
5 \isamarkupsubsection{Syntax Translations% |
6 } |
6 } |
7 % |
7 % |
8 \begin{isamarkuptext}% |
8 \begin{isamarkuptext}% |
9 \label{sec:def-translations} |
9 \label{sec:def-translations} |
|
10 \indexbold{syntax translations|(}% |
|
11 \indexbold{translations@\isacommand {translations} (command)|(} |
10 Isabelle offers an additional definition-like facility, |
12 Isabelle offers an additional definition-like facility, |
11 \textbf{syntax translations}\indexbold{syntax translation}. |
13 \textbf{syntax translations}. |
12 They resemble macros: upon parsing, the defined concept is immediately |
14 They resemble macros: upon parsing, the defined concept is immediately |
13 replaced by its definition, and this is reversed upon printing. For example, |
15 replaced by its definition, and this is reversed upon printing. For example, |
14 the symbol \isa{{\isasymnoteq}} is defined via a syntax translation:% |
16 the symbol \isa{{\isasymnoteq}} is defined via a syntax translation:% |
15 \end{isamarkuptext}% |
17 \end{isamarkuptext}% |
16 \isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}{\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}% |
18 \isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}{\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}% |
17 \begin{isamarkuptext}% |
19 \begin{isamarkuptext}% |
18 \indexbold{*translations}\indexbold{$IsaEqTrans@\isasymrightleftharpoons} |
20 \indexbold{$IsaEqTrans@\isasymrightleftharpoons} |
19 \noindent |
21 \noindent |
20 Internally, \isa{{\isasymnoteq}} never appears. |
22 Internally, \isa{{\isasymnoteq}} never appears. |
21 |
23 |
22 In addition to \isa{{\isasymrightleftharpoons}} there are |
24 In addition to \isa{{\isasymrightleftharpoons}} there are |
23 \isa{{\isasymrightharpoonup}}\indexbold{$IsaEqTrans1@\isasymrightharpoonup} |
25 \isa{{\isasymrightharpoonup}}\indexbold{$IsaEqTrans1@\isasymrightharpoonup} |
28 crops up occasionally: a number of HOL's built-in constructs are defined |
30 crops up occasionally: a number of HOL's built-in constructs are defined |
29 via translations. Translations are preferable to definitions when the new |
31 via translations. Translations are preferable to definitions when the new |
30 concept is a trivial variation on an existing one. For example, we |
32 concept is a trivial variation on an existing one. For example, we |
31 don't need to derive new theorems about \isa{{\isasymnoteq}}, since existing theorems |
33 don't need to derive new theorems about \isa{{\isasymnoteq}}, since existing theorems |
32 about \isa{{\isacharequal}} still apply.% |
34 about \isa{{\isacharequal}} still apply.% |
|
35 \indexbold{syntax translations|)}% |
|
36 \indexbold{translations@\isacommand {translations} (command)|)}% |
33 \end{isamarkuptext}% |
37 \end{isamarkuptext}% |
34 \end{isabellebody}% |
38 \end{isabellebody}% |
35 %%% Local Variables: |
39 %%% Local Variables: |
36 %%% mode: latex |
40 %%% mode: latex |
37 %%% TeX-master: "root" |
41 %%% TeX-master: "root" |