31680
|
1 |
(*<*)theory Overloading imports Main Setup begin
|
|
2 |
|
|
3 |
hide (open) "class" plus (*>*)
|
|
4 |
|
|
5 |
text {* Type classes allow \emph{overloading}; thus a constant may
|
|
6 |
have multiple definitions at non-overlapping types. *}
|
|
7 |
|
|
8 |
subsubsection {* Overloading *}
|
|
9 |
|
|
10 |
text {* We can introduce a binary infix addition operator @{text "\<otimes>"}
|
|
11 |
for arbitrary types by means of a type class: *}
|
|
12 |
|
|
13 |
class plus =
|
|
14 |
fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<oplus>" 70)
|
|
15 |
|
|
16 |
text {* \noindent This introduces a new class @{class [source] plus},
|
|
17 |
along with a constant @{const [source] plus} with nice infix syntax.
|
|
18 |
@{const [source] plus} is also named \emph{class operation}. The type
|
|
19 |
of @{const [source] plus} carries a sort constraint @{typ [source] "'a
|
|
20 |
:: plus"} on its type variable, meaning that only types of class
|
|
21 |
@{class [source] plus} can be instantiated for @{typ [source] "'a"}.
|
|
22 |
To breathe life into @{class [source] plus} we need to declare a type
|
|
23 |
to be an \bfindex{instance} of @{class [source] plus}: *}
|
|
24 |
|
|
25 |
instantiation nat :: plus
|
|
26 |
begin
|
|
27 |
|
|
28 |
text {* \noindent Command \isacommand{instantiation} opens a local
|
|
29 |
theory context. Here we can now instantiate @{const [source] plus} on
|
|
30 |
@{typ nat}: *}
|
|
31 |
|
|
32 |
primrec plus_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
|
|
33 |
"(0::nat) \<oplus> n = n"
|
|
34 |
| "Suc m \<oplus> n = Suc (m \<oplus> n)"
|
|
35 |
|
|
36 |
text {* \noindent Note that the name @{const [source] plus} carries a
|
|
37 |
suffix @{text "_nat"}; by default, the local name of a class operation
|
|
38 |
@{text f} to be instantiated on type constructor @{text \<kappa>} is mangled
|
|
39 |
as @{text f_\<kappa>}. In case of uncertainty, these names may be inspected
|
|
40 |
using the @{command "print_context"} command or the corresponding
|
|
41 |
ProofGeneral button.
|
|
42 |
|
|
43 |
Although class @{class [source] plus} has no axioms, the instantiation must be
|
|
44 |
formally concluded by a (trivial) instantiation proof ``..'': *}
|
|
45 |
|
|
46 |
instance ..
|
|
47 |
|
|
48 |
text {* \noindent More interesting \isacommand{instance} proofs will
|
|
49 |
arise below.
|
|
50 |
|
|
51 |
The instantiation is finished by an explicit *}
|
|
52 |
|
|
53 |
end
|
|
54 |
|
|
55 |
text {* \noindent From now on, terms like @{term "Suc (m \<oplus> 2)"} are
|
|
56 |
legal. *}
|
|
57 |
|
|
58 |
instantiation "*" :: (plus, plus) plus
|
|
59 |
begin
|
|
60 |
|
|
61 |
text {* \noindent Here we instantiate the product type @{type "*"} to
|
|
62 |
class @{class [source] plus}, given that its type arguments are of
|
|
63 |
class @{class [source] plus}: *}
|
|
64 |
|
|
65 |
fun plus_prod :: "'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b" where
|
|
66 |
"(x, y) \<oplus> (w, z) = (x \<oplus> w, y \<oplus> z)"
|
|
67 |
|
|
68 |
text {* \noindent Obviously, overloaded specifications may include
|
|
69 |
recursion over the syntactic structure of types. *}
|
|
70 |
|
|
71 |
instance ..
|
|
72 |
|
|
73 |
end
|
|
74 |
|
|
75 |
text {* \noindent This way we have encoded the canonical lifting of
|
|
76 |
binary operations to products by means of type classes. *}
|
|
77 |
|
|
78 |
(*<*)end(*>*)
|