doc-src/TutorialI/Types/document/Overloading0.tex

code antiquotation roaring ahead

%
\begin{isabellebody}%
\def\isabellecontext{Overloading{\isadigit{0}}}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\begin{isamarkuptext}%
We start with a concept that is required for type classes but already
useful on its own: \emph{overloading}. Isabelle allows overloading: a
constant may have multiple definitions at non-overlapping types.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsubsubsection{An Initial Example%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
If we want to introduce the notion of an \emph{inverse} for arbitrary types we
give it a polymorphic type%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{consts}\isamarkupfalse%
\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
and provide different definitions at different instances:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{defs}\isamarkupfalse%
\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
inverse{\isacharunderscore}bool{\isacharcolon}\ {\isachardoublequoteopen}inverse{\isacharparenleft}b{\isacharcolon}{\isacharcolon}bool{\isacharparenright}\ {\isasymequiv}\ {\isasymnot}\ b{\isachardoublequoteclose}\isanewline
inverse{\isacharunderscore}set{\isacharcolon}\ \ {\isachardoublequoteopen}inverse{\isacharparenleft}A{\isacharcolon}{\isacharcolon}{\isacharprime}a\ set{\isacharparenright}\ {\isasymequiv}\ {\isacharminus}A{\isachardoublequoteclose}\isanewline
inverse{\isacharunderscore}pair{\isacharcolon}\ {\isachardoublequoteopen}inverse{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ {\isacharparenleft}inverse{\isacharparenleft}fst\ p{\isacharparenright}{\isacharcomma}\ inverse{\isacharparenleft}snd\ p{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
Isabelle will not complain because the three definitions do not overlap: no
two of the three types \isa{bool}, \isa{{\isacharprime}a\ set} and \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} have a
common instance. What is more, the recursion in \isa{inverse{\isacharunderscore}pair} is
benign because the type of \isa{inverse} becomes smaller: on the
left it is \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} but on the right \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} and
\isa{{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}. The annotation \isa{{\isacharparenleft}}\isacommand{overloaded}\isa{{\isacharparenright}} tells Isabelle that
the definitions do intentionally define \isa{inverse} only at
instances of its declared type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely suppresses
warnings to that effect.

However, there is nothing to prevent the user from forming terms such as
\isa{inverse\ {\isacharbrackleft}{\isacharbrackright}} and proving theorems such as \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ inverse\ {\isacharbrackleft}{\isacharbrackright}} when inverse is not defined on lists.  Proving theorems about
unspecified constants does not endanger soundness, but it is pointless.
To prevent such terms from even being formed requires the use of type classes.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: