3 \def\isabellecontext{Overloading{\isadigit{0}}}%
6 We start with a concept that is required for type classes but already
7 useful on its own: \emph{overloading}. Isabelle allows overloading: a
8 constant may have multiple definitions at non-overlapping types.%
11 \isamarkupsubsubsection{An initial example}
13 \begin{isamarkuptext}%
14 If we want to introduce the notion of an \emph{inverse} for arbitrary types we
15 give it a polymorphic type%
17 \isacommand{consts}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}%
18 \begin{isamarkuptext}%
20 and provide different definitions at different instances:%
22 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
23 inverse{\isacharunderscore}bool{\isacharcolon}\ {\isachardoublequote}inverse{\isacharparenleft}b{\isacharcolon}{\isacharcolon}bool{\isacharparenright}\ {\isasymequiv}\ {\isasymnot}\ b{\isachardoublequote}\isanewline
24 inverse{\isacharunderscore}set{\isacharcolon}\ \ {\isachardoublequote}inverse{\isacharparenleft}A{\isacharcolon}{\isacharcolon}{\isacharprime}a\ set{\isacharparenright}\ {\isasymequiv}\ {\isacharminus}A{\isachardoublequote}\isanewline
25 inverse{\isacharunderscore}pair{\isacharcolon}\ {\isachardoublequote}inverse{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ {\isacharparenleft}inverse{\isacharparenleft}fst\ p{\isacharparenright}{\isacharcomma}\ inverse{\isacharparenleft}snd\ p{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
26 \begin{isamarkuptext}%
28 Isabelle will not complain because the three definitions do not overlap: no
29 two of the three types \isa{bool}, \isa{{\isacharprime}a\ set} and \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} have a
30 common instance. What is more, the recursion in \isa{inverse{\isacharunderscore}pair} is
31 benign because the type of \isa{inverse} becomes smaller: on the left it is
32 \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}overloaded{\isacharparenright}} tells Isabelle that the definitions do
33 intentionally define \isa{inverse} only at instances of its declared type
34 \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely supresses warnings to that effect.
36 However, there is nothing to prevent the user from forming terms such as
37 \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}} and proving theorems as \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ inverse\ {\isacharbrackleft}{\isacharbrackright}},
38 although we never defined inverse on lists. We hasten to say that there is
39 nothing wrong with such terms and theorems. But it would be nice if we could
40 prevent their formation, simply because it is very likely that the user did
41 not mean to write what he did. Thus he had better not waste his time pursuing
42 it further. This requires the use of type classes.%
47 %%% TeX-master: "root"