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 |
|
10885
|
7 |
subsubsection{*An Initial Example*}
|
10305
|
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
|
10538
|
28 |
benign because the type of @{term[source]inverse} becomes smaller: on the
|
|
29 |
left it is @{typ"'a \<times> 'b \<Rightarrow> 'a \<times> 'b"} but on the right @{typ"'a \<Rightarrow> 'a"} and
|
|
30 |
@{typ"'b \<Rightarrow> 'b"}. The annotation @{text"(overloaded)"} tells Isabelle that
|
|
31 |
the definitions do intentionally define @{term[source]inverse} only at
|
|
32 |
instances of its declared type @{typ"'a \<Rightarrow> 'a"} --- this merely supresses
|
|
33 |
warnings to that effect.
|
10305
|
34 |
|
|
35 |
However, there is nothing to prevent the user from forming terms such as
|
10538
|
36 |
@{term[source]"inverse []"} and proving theorems as @{prop[source]"inverse []
|
|
37 |
= inverse []"}, although we never defined inverse on lists. We hasten to say
|
|
38 |
that there is nothing wrong with such terms and theorems. But it would be
|
|
39 |
nice if we could prevent their formation, simply because it is very likely
|
|
40 |
that the user did not mean to write what he did. Thus he had better not waste
|
|
41 |
his time pursuing it further. This requires the use of type classes.
|
10305
|
42 |
*}
|
|
43 |
(*<*)end(*>*)
|