author | wenzelm |
Fri, 12 Jan 2018 14:08:53 +0100 | |
changeset 67406 | 23307fd33906 |
parent 58842 | 22b87ab47d3b |
child 69505 | cc2d676d5395 |
permissions | -rw-r--r-- |
31680 | 1 |
(*<*)theory Overloading imports Main Setup begin |
2 |
||
36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
wenzelm
parents:
31707
diff
changeset
|
3 |
hide_class (open) plus (*>*) |
31680 | 4 |
|
67406 | 5 |
text \<open>Type classes allow \emph{overloading}; thus a constant may |
6 |
have multiple definitions at non-overlapping types.\<close> |
|
31680 | 7 |
|
67406 | 8 |
subsubsection \<open>Overloading\<close> |
31680 | 9 |
|
67406 | 10 |
text \<open>We can introduce a binary infix addition operator @{text "\<oplus>"} |
11 |
for arbitrary types by means of a type class:\<close> |
|
31680 | 12 |
|
13 |
class plus = |
|
14 |
fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<oplus>" 70) |
|
15 |
||
67406 | 16 |
text \<open>\noindent This introduces a new class @{class [source] plus}, |
31680 | 17 |
along with a constant @{const [source] plus} with nice infix syntax. |
18 |
@{const [source] plus} is also named \emph{class operation}. The type |
|
31682 | 19 |
of @{const [source] plus} carries a class constraint @{typ [source] "'a |
31680 | 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 |
|
67406 | 23 |
to be an \bfindex{instance} of @{class [source] plus}:\<close> |
31680 | 24 |
|
25 |
instantiation nat :: plus |
|
26 |
begin |
|
27 |
||
67406 | 28 |
text \<open>\noindent Command \isacommand{instantiation} opens a local |
31680 | 29 |
theory context. Here we can now instantiate @{const [source] plus} on |
67406 | 30 |
@{typ nat}:\<close> |
31680 | 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 |
||
67406 | 36 |
text \<open>\noindent Note that the name @{const [source] plus} carries a |
31680 | 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 |
|
58842 | 40 |
using the @{command "print_context"} command. |
31680 | 41 |
|
42 |
Although class @{class [source] plus} has no axioms, the instantiation must be |
|
67406 | 43 |
formally concluded by a (trivial) instantiation proof ``..'':\<close> |
31680 | 44 |
|
45 |
instance .. |
|
46 |
||
67406 | 47 |
text \<open>\noindent More interesting \isacommand{instance} proofs will |
31680 | 48 |
arise below. |
49 |
||
67406 | 50 |
The instantiation is finished by an explicit\<close> |
31680 | 51 |
|
52 |
end |
|
53 |
||
67406 | 54 |
text \<open>\noindent From now on, terms like @{term "Suc (m \<oplus> 2)"} are |
55 |
legal.\<close> |
|
31680 | 56 |
|
38325 | 57 |
instantiation prod :: (plus, plus) plus |
31680 | 58 |
begin |
59 |
||
67406 | 60 |
text \<open>\noindent Here we instantiate the product type @{type prod} to |
31680 | 61 |
class @{class [source] plus}, given that its type arguments are of |
67406 | 62 |
class @{class [source] plus}:\<close> |
31680 | 63 |
|
64 |
fun plus_prod :: "'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b" where |
|
65 |
"(x, y) \<oplus> (w, z) = (x \<oplus> w, y \<oplus> z)" |
|
66 |
||
67406 | 67 |
text \<open>\noindent Obviously, overloaded specifications may include |
68 |
recursion over the syntactic structure of types.\<close> |
|
31680 | 69 |
|
70 |
instance .. |
|
71 |
||
72 |
end |
|
73 |
||
67406 | 74 |
text \<open>\noindent This way we have encoded the canonical lifting of |
75 |
binary operations to products by means of type classes.\<close> |
|
31680 | 76 |
|
77 |
(*<*)end(*>*) |