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%
14 \begin{isamarkuptext}%
15 If we want to introduce the notion of an \emph{inverse} for arbitrary types we
16 give it a polymorphic type%
18 \isacommand{consts}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}%
19 \begin{isamarkuptext}%
21 and provide different definitions at different instances:%
23 \isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
24 inverse{\isacharunderscore}bool{\isacharcolon}\ {\isachardoublequote}inverse{\isacharparenleft}b{\isacharcolon}{\isacharcolon}bool{\isacharparenright}\ {\isasymequiv}\ {\isasymnot}\ b{\isachardoublequote}\isanewline
25 inverse{\isacharunderscore}set{\isacharcolon}\ \ {\isachardoublequote}inverse{\isacharparenleft}A{\isacharcolon}{\isacharcolon}{\isacharprime}a\ set{\isacharparenright}\ {\isasymequiv}\ {\isacharminus}A{\isachardoublequote}\isanewline
26 inverse{\isacharunderscore}pair{\isacharcolon}\ {\isachardoublequote}inverse{\isacharparenleft}p{\isacharparenright}\ {\isasymequiv}\ {\isacharparenleft}inverse{\isacharparenleft}fst\ p{\isacharparenright}{\isacharcomma}\ inverse{\isacharparenleft}snd\ p{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
27 \begin{isamarkuptext}%
29 Isabelle will not complain because the three definitions do not overlap: no
30 two of the three types \isa{bool}, \isa{{\isacharprime}a\ set} and \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} have a
31 common instance. What is more, the recursion in \isa{inverse{\isacharunderscore}pair} is
32 benign because the type of \isa{inverse} becomes smaller: on the
33 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
34 \isa{{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b}. The annotation \isa{{\isacharparenleft}overloaded{\isacharparenright}} tells Isabelle that
35 the definitions do intentionally define \isa{inverse} only at
36 instances of its declared type \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely supresses
37 warnings to that effect.
39 However, there is nothing to prevent the user from forming terms such as
40 \isa{{\isachardoublequote}inverse\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}} and proving theorems as \isa{{\isachardoublequote}inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ inverse\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}}, although we never defined inverse on lists. We hasten to say
41 that there is nothing wrong with such terms and theorems. But it would be
42 nice if we could prevent their formation, simply because it is very likely
43 that the user did not mean to write what he did. Thus he had better not waste
44 his time pursuing it further. This requires the use of type classes.%
49 %%% TeX-master: "root"