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