doc-src/TutorialI/Misc/document/Translations.tex

the one-point rule for bounded quantifiers

%
\begin{isabellebody}%
\def\isabellecontext{Translations}%
%
\isamarkupsubsection{Syntax Translations%
}
%
\begin{isamarkuptext}%
\label{sec:def-translations}
Isabelle offers an additional definition-like facility,
\textbf{syntax translations}\indexbold{syntax translation}.
They resemble macros: upon parsing, the defined concept is immediately
replaced by its definition, and this is reversed upon printing. For example,
the symbol \isa{{\isasymnoteq}} is defined via a syntax translation:%
\end{isamarkuptext}%
\isacommand{translations}\ {\isachardoublequote}x\ {\isasymnoteq}\ y{\isachardoublequote}\ {\isasymrightleftharpoons}\ {\isachardoublequote}{\isasymnot}{\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\indexbold{*translations}\indexbold{$IsaEqTrans@\isasymrightleftharpoons}
\noindent
Internally, \isa{{\isasymnoteq}} never appears.

In addition to \isa{{\isasymrightleftharpoons}} there are
\isa{{\isasymrightharpoonup}}\indexbold{$IsaEqTrans1@\isasymrightharpoonup}
and \isa{{\isasymleftharpoondown}}\indexbold{$IsaEqTrans2@\isasymleftharpoondown}
for uni-directional translations, which only affect
parsing or printing.  We do not want to cover the details of
translations at this point.  We haved mentioned the concept merely because it
crops up occasionally: a number of HOL's built-in constructs are defined
via translations.  Translations are preferable to definitions when the new 
concept is a trivial variation on an existing one.  For example, we
don't need to derive new theorems about \isa{{\isasymnoteq}}, since existing theorems
about \isa{{\isacharequal}} still apply.%
\end{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: