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 nonoverlapping 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(*>*)
