10305
|
1 |
(*<*)theory Overloading0 = Main:(*>*)
|
|
2 |
|
10328
|
3 |
text{* We start with a concept that is required for type classes but already
|
|
4 |
useful on its own: \emph{overloading}. Isabelle allows overloading: a
|
|
5 |
constant may have multiple definitions at non-overlapping types. *}
|
|
6 |
|
10305
|
7 |
subsubsection{*An initial example*}
|
|
8 |
|
10328
|
9 |
text{*
|
|
10 |
If we want to introduce the notion of an \emph{inverse} for arbitrary types we
|
10305
|
11 |
give it a polymorphic type *}
|
|
12 |
|
|
13 |
consts inverse :: "'a \<Rightarrow> 'a"
|
|
14 |
|
|
15 |
text{*\noindent
|
|
16 |
and provide different definitions at different instances:
|
|
17 |
*}
|
|
18 |
|
|
19 |
defs (overloaded)
|
|
20 |
inverse_bool: "inverse(b::bool) \<equiv> \<not> b"
|
|
21 |
inverse_set: "inverse(A::'a set) \<equiv> -A"
|
|
22 |
inverse_pair: "inverse(p) \<equiv> (inverse(fst p), inverse(snd p))"
|
|
23 |
|
|
24 |
text{*\noindent
|
|
25 |
Isabelle will not complain because the three definitions do not overlap: no
|
|
26 |
two of the three types @{typ bool}, @{typ"'a set"} and @{typ"'a \<times> 'b"} have a
|
|
27 |
common instance. What is more, the recursion in @{thm[source]inverse_pair} is
|
|
28 |
benign because the type of @{term inverse} becomes smaller: on the left it is
|
|
29 |
@{typ"'a \<times> 'b \<Rightarrow> 'a \<times> 'b"} but on the right @{typ"'a \<Rightarrow> 'a"} and @{typ"'b \<Rightarrow>
|
10328
|
30 |
'b"}. The annotation @{text"(overloaded)"} tells Isabelle that the definitions do
|
10305
|
31 |
intentionally define @{term inverse} only at instances of its declared type
|
|
32 |
@{typ"'a \<Rightarrow> 'a"} --- this merely supresses warnings to that effect.
|
|
33 |
|
|
34 |
However, there is nothing to prevent the user from forming terms such as
|
|
35 |
@{term"inverse []"} and proving theorems as @{prop"inverse [] = inverse []"},
|
|
36 |
although we never defined inverse on lists. We hasten to say that there is
|
|
37 |
nothing wrong with such terms and theorems. But it would be nice if we could
|
|
38 |
prevent their formation, simply because it is very likely that the user did
|
|
39 |
not mean to write what he did. Thus he had better not waste his time pursuing
|
|
40 |
it further. This requires the use of type classes.
|
|
41 |
*}
|
|
42 |
(*<*)end(*>*)
|