10305
|
1 |
(*<*)theory Overloading0 = Main:(*>*)
|
|
2 |
|
10328
|
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 |
|
10885
|
7 |
subsubsection{*An Initial Example*}
|
10305
|
8 |
|
10328
|
9 |
text{*
|
|
10 |
If we want to introduce the notion of an \emph{inverse} for arbitrary types we
|
10305
|
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
|
10538
|
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
|
11196
|
30 |
@{typ"'b \<Rightarrow> 'b"}. The annotation @{text"("}\isacommand{overloaded}@{text")"} tells Isabelle that
|
10538
|
31 |
the definitions do intentionally define @{term[source]inverse} only at
|
11310
|
32 |
instances of its declared type @{typ"'a \<Rightarrow> 'a"} --- this merely suppresses
|
10538
|
33 |
warnings to that effect.
|
10305
|
34 |
|
|
35 |
However, there is nothing to prevent the user from forming terms such as
|
11213
|
36 |
@{text"inverse []"} and proving theorems such as @{text"inverse []
|
11494
|
37 |
= inverse []"} when inverse is not defined on lists. Proving theorems about
|
|
38 |
undefined constants does not endanger soundness, but it is pointless.
|
|
39 |
To prevent such terms from even being formed requires the use of type classes.
|
10305
|
40 |
*}
|
|
41 |
(*<*)end(*>*)
|