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 \ '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) \ \ b"  nipkow@10305  21 inverse_set: "inverse(A::'a set) \ -A"  nipkow@10305  22 inverse_pair: "inverse(p) \ (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 \ '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 \ 'b \ 'a \ 'b"} but on the right @{typ"'a \ 'a"} and  nipkow@10538  30 @{typ"'b \ '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 \ '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(*>*)