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