author nipkow Wed Dec 06 13:22:58 2000 +0100 (2000-12-06) changeset 10608 620647438780 parent 10538 d1bf9ca9008d child 10885 90695f46440b permissions -rw-r--r--
*** empty log message ***
     1 (*<*)theory Overloading0 = Main:(*>*)

     2

     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

     7 subsubsection{*An initial example*}

     8

     9 text{*

    10 If we want to introduce the notion of an \emph{inverse} for arbitrary types we

    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[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.

    34

    35 However, there is nothing to prevent the user from forming terms such as

    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.

    42 *}

    43 (*<*)end(*>*)