Theory Overloading

(*<*)theory Overloading imports "../Setup" begin

hide_class (open) plus (*>*)

text ‹Type classes allow \emph{overloading}; thus a constant may
have multiple definitions at non-overlapping types.›

subsubsection ‹Overloading›

text ‹We can introduce a binary infix addition operator ‹⊕›
for arbitrary types by means of a type class:›

class plus =
  fixes plus :: "'a ⇒ 'a ⇒ 'a" (infixl "⊕" 70)

text ‹\noindent This introduces a new class @{class [source] plus},
along with a constant @{const [source] plus} with nice infix syntax.
@{const [source] plus} is also named \emph{class operation}.  The type
of @{const [source] plus} carries a class constraint @{typ [source] "'a
:: plus"} on its type variable, meaning that only types of class
@{class [source] plus} can be instantiated for @{typ [source] "'a"}.
To breathe life into @{class [source] plus} we need to declare a type
to be an \bfindex{instance} of @{class [source] plus}:›

instantiation nat :: plus
begin

text ‹\noindent Command \isacommand{instantiation} opens a local
theory context.  Here we can now instantiate @{const [source] plus} on
\<^typ>‹nat›:›

primrec plus_nat :: "nat ⇒ nat ⇒ nat" where
    "(0::nat) ⊕ n = n"
  | "Suc m ⊕ n = Suc (m ⊕ n)"

text ‹\noindent Note that the name @{const [source] plus} carries a
suffix ‹_nat›; by default, the local name of a class operation
‹f› to be instantiated on type constructor ‹κ› is mangled
as ‹f_κ›.  In case of uncertainty, these names may be inspected
using the @{command "print_context"} command.

Although class @{class [source] plus} has no axioms, the instantiation must be
formally concluded by a (trivial) instantiation proof ``..'':›

instance ..

text ‹\noindent More interesting \isacommand{instance} proofs will
arise below.

The instantiation is finished by an explicit›

end

text ‹\noindent From now on, terms like \<^term>‹Suc (m ⊕ 2)› are
legal.›

instantiation prod :: (plus, plus) plus
begin

text ‹\noindent Here we instantiate the product type \<^type>‹prod› to
class @{class [source] plus}, given that its type arguments are of
class @{class [source] plus}:›

fun plus_prod :: "'a × 'b ⇒ 'a × 'b ⇒ 'a × 'b" where
  "(x, y) ⊕ (w, z) = (x ⊕ w, y ⊕ z)"

text ‹\noindent Obviously, overloaded specifications may include
recursion over the syntactic structure of types.›

instance ..

end

text ‹\noindent This way we have encoded the canonical lifting of
binary operations to products by means of type classes.›

(*<*)end(*>*)