1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Overloading}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 % |
|
18 \begin{isamarkuptext}% |
|
19 Type classes allow \emph{overloading}; thus a constant may |
|
20 have multiple definitions at non-overlapping types.% |
|
21 \end{isamarkuptext}% |
|
22 \isamarkuptrue% |
|
23 % |
|
24 \isamarkupsubsubsection{Overloading% |
|
25 } |
|
26 \isamarkuptrue% |
|
27 % |
|
28 \begin{isamarkuptext}% |
|
29 We can introduce a binary infix addition operator \isa{{\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}} |
|
30 for arbitrary types by means of a type class:% |
|
31 \end{isamarkuptext}% |
|
32 \isamarkuptrue% |
|
33 \isacommand{class}\isamarkupfalse% |
|
34 \ plus\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
35 \ \ \isakeyword{fixes}\ plus\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F706C75733E}{\isasymoplus}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{7}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}% |
|
36 \begin{isamarkuptext}% |
|
37 \noindent This introduces a new class \isa{plus}, |
|
38 along with a constant \isa{plus} with nice infix syntax. |
|
39 \isa{plus} is also named \emph{class operation}. The type |
|
40 of \isa{plus} carries a class constraint \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ plus{\isaliteral{22}{\isachardoublequote}}} on its type variable, meaning that only types of class |
|
41 \isa{plus} can be instantiated for \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}}. |
|
42 To breathe life into \isa{plus} we need to declare a type |
|
43 to be an \bfindex{instance} of \isa{plus}:% |
|
44 \end{isamarkuptext}% |
|
45 \isamarkuptrue% |
|
46 \isacommand{instantiation}\isamarkupfalse% |
|
47 \ nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ plus\isanewline |
|
48 \isakeyword{begin}% |
|
49 \begin{isamarkuptext}% |
|
50 \noindent Command \isacommand{instantiation} opens a local |
|
51 theory context. Here we can now instantiate \isa{plus} on |
|
52 \isa{nat}:% |
|
53 \end{isamarkuptext}% |
|
54 \isamarkuptrue% |
|
55 \isacommand{primrec}\isamarkupfalse% |
|
56 \ plus{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
57 \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ n\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
58 \ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}Suc\ m\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ n\ {\isaliteral{3D}{\isacharequal}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
59 \begin{isamarkuptext}% |
|
60 \noindent Note that the name \isa{plus} carries a |
|
61 suffix \isa{{\isaliteral{5F}{\isacharunderscore}}nat}; by default, the local name of a class operation |
|
62 \isa{f} to be instantiated on type constructor \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} is mangled |
|
63 as \isa{f{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}}. In case of uncertainty, these names may be inspected |
|
64 using the \hyperlink{command.print-context}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}context}}}} command or the corresponding |
|
65 ProofGeneral button. |
|
66 |
|
67 Although class \isa{plus} has no axioms, the instantiation must be |
|
68 formally concluded by a (trivial) instantiation proof ``..'':% |
|
69 \end{isamarkuptext}% |
|
70 \isamarkuptrue% |
|
71 \isacommand{instance}\isamarkupfalse% |
|
72 % |
|
73 \isadelimproof |
|
74 \ % |
|
75 \endisadelimproof |
|
76 % |
|
77 \isatagproof |
|
78 \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
|
79 % |
|
80 \endisatagproof |
|
81 {\isafoldproof}% |
|
82 % |
|
83 \isadelimproof |
|
84 % |
|
85 \endisadelimproof |
|
86 % |
|
87 \begin{isamarkuptext}% |
|
88 \noindent More interesting \isacommand{instance} proofs will |
|
89 arise below. |
|
90 |
|
91 The instantiation is finished by an explicit% |
|
92 \end{isamarkuptext}% |
|
93 \isamarkuptrue% |
|
94 \isacommand{end}\isamarkupfalse% |
|
95 % |
|
96 \begin{isamarkuptext}% |
|
97 \noindent From now on, terms like \isa{Suc\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} are |
|
98 legal.% |
|
99 \end{isamarkuptext}% |
|
100 \isamarkuptrue% |
|
101 \isacommand{instantiation}\isamarkupfalse% |
|
102 \ prod\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}plus{\isaliteral{2C}{\isacharcomma}}\ plus{\isaliteral{29}{\isacharparenright}}\ plus\isanewline |
|
103 \isakeyword{begin}% |
|
104 \begin{isamarkuptext}% |
|
105 \noindent Here we instantiate the product type \isa{prod} to |
|
106 class \isa{plus}, given that its type arguments are of |
|
107 class \isa{plus}:% |
|
108 \end{isamarkuptext}% |
|
109 \isamarkuptrue% |
|
110 \isacommand{fun}\isamarkupfalse% |
|
111 \ plus{\isaliteral{5F}{\isacharunderscore}}prod\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
112 \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ {\isaliteral{28}{\isacharparenleft}}w{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ w{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ z{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
113 \begin{isamarkuptext}% |
|
114 \noindent Obviously, overloaded specifications may include |
|
115 recursion over the syntactic structure of types.% |
|
116 \end{isamarkuptext}% |
|
117 \isamarkuptrue% |
|
118 \isacommand{instance}\isamarkupfalse% |
|
119 % |
|
120 \isadelimproof |
|
121 \ % |
|
122 \endisadelimproof |
|
123 % |
|
124 \isatagproof |
|
125 \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% |
|
126 % |
|
127 \endisatagproof |
|
128 {\isafoldproof}% |
|
129 % |
|
130 \isadelimproof |
|
131 % |
|
132 \endisadelimproof |
|
133 \isanewline |
|
134 \isanewline |
|
135 \isacommand{end}\isamarkupfalse% |
|
136 % |
|
137 \begin{isamarkuptext}% |
|
138 \noindent This way we have encoded the canonical lifting of |
|
139 binary operations to products by means of type classes.% |
|
140 \end{isamarkuptext}% |
|
141 \isamarkuptrue% |
|
142 % |
|
143 \isadelimtheory |
|
144 % |
|
145 \endisadelimtheory |
|
146 % |
|
147 \isatagtheory |
|
148 % |
|
149 \endisatagtheory |
|
150 {\isafoldtheory}% |
|
151 % |
|
152 \isadelimtheory |
|
153 % |
|
154 \endisadelimtheory |
|
155 \end{isabellebody}% |
|
156 %%% Local Variables: |
|
157 %%% mode: latex |
|
158 %%% TeX-master: "root" |
|
159 %%% End: |
|