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 nonoverlapping 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(*>*)
