1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{Overloading{\isadigit{0}}}% |
3 \def\isabellecontext{Overloading{\isadigit{0}}}% |
4 % |
4 % |
|
5 \begin{isamarkuptext}% |
|
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.% |
|
9 \end{isamarkuptext}% |
|
10 % |
5 \isamarkupsubsubsection{An initial example} |
11 \isamarkupsubsubsection{An initial example} |
6 % |
12 % |
7 \begin{isamarkuptext}% |
13 \begin{isamarkuptext}% |
8 We start with a concept that is required for type classes but already |
14 If we want to introduce the notion of an \emph{inverse} for arbitrary types we |
9 useful on its own: \emph{overloading}. Isabelle allows overloading: a |
|
10 constant may have multiple definitions at non-overlapping types. For example, |
|
11 if we want to introduce the notion of an \emph{inverse} at arbitrary types we |
|
12 give it a polymorphic type% |
15 give it a polymorphic type% |
13 \end{isamarkuptext}% |
16 \end{isamarkuptext}% |
14 \isacommand{consts}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}% |
17 \isacommand{consts}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}% |
15 \begin{isamarkuptext}% |
18 \begin{isamarkuptext}% |
16 \noindent |
19 \noindent |
24 \noindent |
27 \noindent |
25 Isabelle will not complain because the three definitions do not overlap: no |
28 Isabelle will not complain because the three definitions do not overlap: no |
26 two of the three types \isa{bool}, \isa{{\isacharprime}a\ set} and \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} have a |
29 two of the three types \isa{bool}, \isa{{\isacharprime}a\ set} and \isa{{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b} have a |
27 common instance. What is more, the recursion in \isa{inverse{\isacharunderscore}pair} is |
30 common instance. What is more, the recursion in \isa{inverse{\isacharunderscore}pair} is |
28 benign because the type of \isa{inverse} becomes smaller: on the left it is |
31 benign because the type of \isa{inverse} becomes smaller: on the left it is |
29 \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 \isa{{\isacharparenleft}overloaded{\isacharparenright}} tells Isabelle that the definitions do |
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 |
30 intentionally define \isa{inverse} only at instances of its declared type |
33 intentionally define \isa{inverse} only at instances of its declared type |
31 \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely supresses warnings to that effect. |
34 \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a} --- this merely supresses warnings to that effect. |
32 |
35 |
33 However, there is nothing to prevent the user from forming terms such as |
36 However, there is nothing to prevent the user from forming terms such as |
34 \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}} and proving theorems as \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ inverse\ {\isacharbrackleft}{\isacharbrackright}}, |
37 \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}} and proving theorems as \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ inverse\ {\isacharbrackleft}{\isacharbrackright}}, |