doc-src/TutorialI/Types/Overloading0.thy
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 ***
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(*>*)