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