author  wenzelm 
Sat, 05 Apr 2014 15:03:40 +0200  
changeset 56421  1ffd7eaa778b 
parent 54665  617ddc60f914 
child 58842  22b87ab47d3b 
permissions  rwrr 
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 

5 
text {* Type classes allow \emph{overloading}; thus a constant may 

6 
have multiple definitions at nonoverlapping types. *} 

7 

8 
subsubsection {* Overloading *} 

9 

54665  10 
text {* We can introduce a binary infix addition operator @{text "\<oplus>"} 
31680  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 

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 

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 

38325  58 
instantiation prod :: (plus, plus) plus 
31680  59 
begin 
60 

38325  61 
text {* \noindent Here we instantiate the product type @{type prod} to 
31680  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(*>*) 