|
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Classes}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 \isacommand{theory}\isamarkupfalse% |
|
11 \ Classes\isanewline |
|
12 \isakeyword{imports}\ Main\ Setup\isanewline |
|
13 \isakeyword{begin}% |
|
14 \endisatagtheory |
|
15 {\isafoldtheory}% |
|
16 % |
|
17 \isadelimtheory |
|
18 % |
|
19 \endisadelimtheory |
|
20 % |
|
21 \isamarkupsection{Introduction% |
|
22 } |
|
23 \isamarkuptrue% |
|
24 % |
|
25 \begin{isamarkuptext}% |
|
26 Type classes were introduces by Wadler and Blott \cite{wadler89how} |
|
27 into the Haskell language, to allow for a reasonable implementation |
|
28 of overloading\footnote{throughout this tutorial, we are referring |
|
29 to classical Haskell 1.0 type classes, not considering |
|
30 later additions in expressiveness}. |
|
31 As a canonical example, a polymorphic equality function |
|
32 \isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} which is overloaded on different |
|
33 types for \isa{{\isasymalpha}}, which is achieved by splitting introduction |
|
34 of the \isa{eq} function from its overloaded definitions by means |
|
35 of \isa{class} and \isa{instance} declarations: |
|
36 \footnote{syntax here is a kind of isabellized Haskell} |
|
37 |
|
38 \begin{quote} |
|
39 |
|
40 \noindent\isa{class\ eq\ where} \\ |
|
41 \hspace*{2ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} |
|
42 |
|
43 \medskip\noindent\isa{instance\ nat\ {\isasymColon}\ eq\ where} \\ |
|
44 \hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isadigit{0}}\ {\isacharequal}\ True} \\ |
|
45 \hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ False} \\ |
|
46 \hspace*{2ex}\isa{eq\ {\isacharunderscore}\ {\isadigit{0}}\ {\isacharequal}\ False} \\ |
|
47 \hspace*{2ex}\isa{eq\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ eq\ n\ m} |
|
48 |
|
49 \medskip\noindent\isa{instance\ {\isacharparenleft}{\isasymalpha}{\isasymColon}eq{\isacharcomma}\ {\isasymbeta}{\isasymColon}eq{\isacharparenright}\ pair\ {\isasymColon}\ eq\ where} \\ |
|
50 \hspace*{2ex}\isa{eq\ {\isacharparenleft}x{\isadigit{1}}{\isacharcomma}\ y{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ eq\ x{\isadigit{1}}\ x{\isadigit{2}}\ {\isasymand}\ eq\ y{\isadigit{1}}\ y{\isadigit{2}}} |
|
51 |
|
52 \medskip\noindent\isa{class\ ord\ extends\ eq\ where} \\ |
|
53 \hspace*{2ex}\isa{less{\isacharunderscore}eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\ |
|
54 \hspace*{2ex}\isa{less\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} |
|
55 |
|
56 \end{quote} |
|
57 |
|
58 \noindent Type variables are annotated with (finitely many) classes; |
|
59 these annotations are assertions that a particular polymorphic type |
|
60 provides definitions for overloaded functions. |
|
61 |
|
62 Indeed, type classes not only allow for simple overloading |
|
63 but form a generic calculus, an instance of order-sorted |
|
64 algebra \cite{Nipkow-Prehofer:1993,nipkow-sorts93,Wenzel:1997:TPHOL}. |
|
65 |
|
66 From a software engeneering point of view, type classes |
|
67 roughly correspond to interfaces in object-oriented languages like Java; |
|
68 so, it is naturally desirable that type classes do not only |
|
69 provide functions (class parameters) but also state specifications |
|
70 implementations must obey. For example, the \isa{class\ eq} |
|
71 above could be given the following specification, demanding that |
|
72 \isa{class\ eq} is an equivalence relation obeying reflexivity, |
|
73 symmetry and transitivity: |
|
74 |
|
75 \begin{quote} |
|
76 |
|
77 \noindent\isa{class\ eq\ where} \\ |
|
78 \hspace*{2ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\ |
|
79 \isa{satisfying} \\ |
|
80 \hspace*{2ex}\isa{refl{\isacharcolon}\ eq\ x\ x} \\ |
|
81 \hspace*{2ex}\isa{sym{\isacharcolon}\ eq\ x\ y\ {\isasymlongleftrightarrow}\ eq\ x\ y} \\ |
|
82 \hspace*{2ex}\isa{trans{\isacharcolon}\ eq\ x\ y\ {\isasymand}\ eq\ y\ z\ {\isasymlongrightarrow}\ eq\ x\ z} |
|
83 |
|
84 \end{quote} |
|
85 |
|
86 \noindent From a theoretic point of view, type classes are lightweight |
|
87 modules; Haskell type classes may be emulated by |
|
88 SML functors \cite{classes_modules}. |
|
89 Isabelle/Isar offers a discipline of type classes which brings |
|
90 all those aspects together: |
|
91 |
|
92 \begin{enumerate} |
|
93 \item specifying abstract parameters together with |
|
94 corresponding specifications, |
|
95 \item instantiating those abstract parameters by a particular |
|
96 type |
|
97 \item in connection with a ``less ad-hoc'' approach to overloading, |
|
98 \item with a direct link to the Isabelle module system |
|
99 (aka locales \cite{kammueller-locales}). |
|
100 \end{enumerate} |
|
101 |
|
102 \noindent Isar type classes also directly support code generation |
|
103 in a Haskell like fashion. |
|
104 |
|
105 This tutorial demonstrates common elements of structured specifications |
|
106 and abstract reasoning with type classes by the algebraic hierarchy of |
|
107 semigroups, monoids and groups. Our background theory is that of |
|
108 Isabelle/HOL \cite{isa-tutorial}, for which some |
|
109 familiarity is assumed. |
|
110 |
|
111 Here we merely present the look-and-feel for end users. |
|
112 Internally, those are mapped to more primitive Isabelle concepts. |
|
113 See \cite{Haftmann-Wenzel:2006:classes} for more detail.% |
|
114 \end{isamarkuptext}% |
|
115 \isamarkuptrue% |
|
116 % |
|
117 \isamarkupsection{A simple algebra example \label{sec:example}% |
|
118 } |
|
119 \isamarkuptrue% |
|
120 % |
|
121 \isamarkupsubsection{Class definition% |
|
122 } |
|
123 \isamarkuptrue% |
|
124 % |
|
125 \begin{isamarkuptext}% |
|
126 Depending on an arbitrary type \isa{{\isasymalpha}}, class \isa{semigroup} introduces a binary operator \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} that is |
|
127 assumed to be associative:% |
|
128 \end{isamarkuptext}% |
|
129 \isamarkuptrue% |
|
130 % |
|
131 \isadelimquote |
|
132 % |
|
133 \endisadelimquote |
|
134 % |
|
135 \isatagquote |
|
136 \isacommand{class}\isamarkupfalse% |
|
137 \ semigroup\ {\isacharequal}\isanewline |
|
138 \ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline |
|
139 \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}% |
|
140 \endisatagquote |
|
141 {\isafoldquote}% |
|
142 % |
|
143 \isadelimquote |
|
144 % |
|
145 \endisadelimquote |
|
146 % |
|
147 \begin{isamarkuptext}% |
|
148 \noindent This \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} specification consists of two |
|
149 parts: the \qn{operational} part names the class parameter |
|
150 (\hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}), the \qn{logical} part specifies properties on them |
|
151 (\hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}). The local \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} and |
|
152 \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} are lifted to the theory toplevel, |
|
153 yielding the global |
|
154 parameter \isa{{\isachardoublequote}mult\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the |
|
155 global theorem \hyperlink{fact.semigroup.assoc:}{\mbox{\isa{semigroup{\isachardot}assoc{\isacharcolon}}}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequote}}.% |
|
156 \end{isamarkuptext}% |
|
157 \isamarkuptrue% |
|
158 % |
|
159 \isamarkupsubsection{Class instantiation \label{sec:class_inst}% |
|
160 } |
|
161 \isamarkuptrue% |
|
162 % |
|
163 \begin{isamarkuptext}% |
|
164 The concrete type \isa{int} is made a \isa{semigroup} |
|
165 instance by providing a suitable definition for the class parameter |
|
166 \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} and a proof for the specification of \hyperlink{fact.assoc}{\mbox{\isa{assoc}}}. |
|
167 This is accomplished by the \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} target:% |
|
168 \end{isamarkuptext}% |
|
169 \isamarkuptrue% |
|
170 % |
|
171 \isadelimquote |
|
172 % |
|
173 \endisadelimquote |
|
174 % |
|
175 \isatagquote |
|
176 \isacommand{instantiation}\isamarkupfalse% |
|
177 \ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline |
|
178 \isakeyword{begin}\isanewline |
|
179 \isanewline |
|
180 \isacommand{definition}\isamarkupfalse% |
|
181 \isanewline |
|
182 \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymotimes}\ j\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
183 \isanewline |
|
184 \isacommand{instance}\isamarkupfalse% |
|
185 \ \isacommand{proof}\isamarkupfalse% |
|
186 \isanewline |
|
187 \ \ \isacommand{fix}\isamarkupfalse% |
|
188 \ i\ j\ k\ {\isacharcolon}{\isacharcolon}\ int\ \isacommand{have}\isamarkupfalse% |
|
189 \ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isacharplus}\ j{\isacharparenright}\ {\isacharplus}\ k\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j\ {\isacharplus}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
190 \ simp\isanewline |
|
191 \ \ \isacommand{then}\isamarkupfalse% |
|
192 \ \isacommand{show}\isamarkupfalse% |
|
193 \ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymotimes}\ j{\isacharparenright}\ {\isasymotimes}\ k\ {\isacharequal}\ i\ {\isasymotimes}\ {\isacharparenleft}j\ {\isasymotimes}\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
194 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
|
195 \ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse% |
|
196 \isanewline |
|
197 \isacommand{qed}\isamarkupfalse% |
|
198 \isanewline |
|
199 \isanewline |
|
200 \isacommand{end}\isamarkupfalse% |
|
201 % |
|
202 \endisatagquote |
|
203 {\isafoldquote}% |
|
204 % |
|
205 \isadelimquote |
|
206 % |
|
207 \endisadelimquote |
|
208 % |
|
209 \begin{isamarkuptext}% |
|
210 \noindent \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} allows to define class parameters |
|
211 at a particular instance using common specification tools (here, |
|
212 \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}). The concluding \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} |
|
213 opens a proof that the given parameters actually conform |
|
214 to the class specification. Note that the first proof step |
|
215 is the \hyperlink{method.default}{\mbox{\isa{default}}} method, |
|
216 which for such instance proofs maps to the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method. |
|
217 This boils down an instance judgement to the relevant primitive |
|
218 proof goals and should conveniently always be the first method applied |
|
219 in an instantiation proof. |
|
220 |
|
221 From now on, the type-checker will consider \isa{int} |
|
222 as a \isa{semigroup} automatically, i.e.\ any general results |
|
223 are immediately available on concrete instances. |
|
224 |
|
225 \medskip Another instance of \isa{semigroup} are the natural numbers:% |
|
226 \end{isamarkuptext}% |
|
227 \isamarkuptrue% |
|
228 % |
|
229 \isadelimquote |
|
230 % |
|
231 \endisadelimquote |
|
232 % |
|
233 \isatagquote |
|
234 \isacommand{instantiation}\isamarkupfalse% |
|
235 \ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline |
|
236 \isakeyword{begin}\isanewline |
|
237 \isanewline |
|
238 \isacommand{primrec}\isamarkupfalse% |
|
239 \ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline |
|
240 \ \ {\isachardoublequoteopen}{\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline |
|
241 \ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}m\ {\isasymotimes}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
242 \isanewline |
|
243 \isacommand{instance}\isamarkupfalse% |
|
244 \ \isacommand{proof}\isamarkupfalse% |
|
245 \isanewline |
|
246 \ \ \isacommand{fix}\isamarkupfalse% |
|
247 \ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\ \isanewline |
|
248 \ \ \isacommand{show}\isamarkupfalse% |
|
249 \ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
250 \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
251 \ {\isacharparenleft}induct\ m{\isacharparenright}\ auto\isanewline |
|
252 \isacommand{qed}\isamarkupfalse% |
|
253 \isanewline |
|
254 \isanewline |
|
255 \isacommand{end}\isamarkupfalse% |
|
256 % |
|
257 \endisatagquote |
|
258 {\isafoldquote}% |
|
259 % |
|
260 \isadelimquote |
|
261 % |
|
262 \endisadelimquote |
|
263 % |
|
264 \begin{isamarkuptext}% |
|
265 \noindent Note the occurence of the name \isa{mult{\isacharunderscore}nat} |
|
266 in the primrec declaration; by default, the local name of |
|
267 a class operation \isa{f} to instantiate on type constructor |
|
268 \isa{{\isasymkappa}} are mangled as \isa{f{\isacharunderscore}{\isasymkappa}}. In case of uncertainty, |
|
269 these names may be inspected using the \hyperlink{command.print-context}{\mbox{\isa{\isacommand{print{\isacharunderscore}context}}}} command |
|
270 or the corresponding ProofGeneral button.% |
|
271 \end{isamarkuptext}% |
|
272 \isamarkuptrue% |
|
273 % |
|
274 \isamarkupsubsection{Lifting and parametric types% |
|
275 } |
|
276 \isamarkuptrue% |
|
277 % |
|
278 \begin{isamarkuptext}% |
|
279 Overloaded definitions giving on class instantiation |
|
280 may include recursion over the syntactic structure of types. |
|
281 As a canonical example, we model product semigroups |
|
282 using our simple algebra:% |
|
283 \end{isamarkuptext}% |
|
284 \isamarkuptrue% |
|
285 % |
|
286 \isadelimquote |
|
287 % |
|
288 \endisadelimquote |
|
289 % |
|
290 \isatagquote |
|
291 \isacommand{instantiation}\isamarkupfalse% |
|
292 \ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline |
|
293 \isakeyword{begin}\isanewline |
|
294 \isanewline |
|
295 \isacommand{definition}\isamarkupfalse% |
|
296 \isanewline |
|
297 \ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}fst\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ fst\ p\isactrlisub {\isadigit{2}}{\isacharcomma}\ snd\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ snd\ p\isactrlisub {\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
298 \isanewline |
|
299 \isacommand{instance}\isamarkupfalse% |
|
300 \ \isacommand{proof}\isamarkupfalse% |
|
301 \isanewline |
|
302 \ \ \isacommand{fix}\isamarkupfalse% |
|
303 \ p\isactrlisub {\isadigit{1}}\ p\isactrlisub {\isadigit{2}}\ p\isactrlisub {\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}semigroup\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline |
|
304 \ \ \isacommand{show}\isamarkupfalse% |
|
305 \ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}\ {\isacharequal}\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ {\isacharparenleft}p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
306 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
|
307 \ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
308 \ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline |
|
309 \isacommand{qed}\isamarkupfalse% |
|
310 \ \ \ \ \ \ \isanewline |
|
311 \isanewline |
|
312 \isacommand{end}\isamarkupfalse% |
|
313 % |
|
314 \endisatagquote |
|
315 {\isafoldquote}% |
|
316 % |
|
317 \isadelimquote |
|
318 % |
|
319 \endisadelimquote |
|
320 % |
|
321 \begin{isamarkuptext}% |
|
322 \noindent Associativity from product semigroups is |
|
323 established using |
|
324 the definition of \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} on products and the hypothetical |
|
325 associativity of the type components; these hypotheses |
|
326 are facts due to the \isa{semigroup} constraints imposed |
|
327 on the type components by the \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} proposition. |
|
328 Indeed, this pattern often occurs with parametric types |
|
329 and type classes.% |
|
330 \end{isamarkuptext}% |
|
331 \isamarkuptrue% |
|
332 % |
|
333 \isamarkupsubsection{Subclassing% |
|
334 } |
|
335 \isamarkuptrue% |
|
336 % |
|
337 \begin{isamarkuptext}% |
|
338 We define a subclass \isa{monoidl} (a semigroup with a left-hand neutral) |
|
339 by extending \isa{semigroup} |
|
340 with one additional parameter \isa{neutral} together |
|
341 with its property:% |
|
342 \end{isamarkuptext}% |
|
343 \isamarkuptrue% |
|
344 % |
|
345 \isadelimquote |
|
346 % |
|
347 \endisadelimquote |
|
348 % |
|
349 \isatagquote |
|
350 \isacommand{class}\isamarkupfalse% |
|
351 \ monoidl\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline |
|
352 \ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline |
|
353 \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}% |
|
354 \endisatagquote |
|
355 {\isafoldquote}% |
|
356 % |
|
357 \isadelimquote |
|
358 % |
|
359 \endisadelimquote |
|
360 % |
|
361 \begin{isamarkuptext}% |
|
362 \noindent Again, we prove some instances, by |
|
363 providing suitable parameter definitions and proofs for the |
|
364 additional specifications. Observe that instantiations |
|
365 for types with the same arity may be simultaneous:% |
|
366 \end{isamarkuptext}% |
|
367 \isamarkuptrue% |
|
368 % |
|
369 \isadelimquote |
|
370 % |
|
371 \endisadelimquote |
|
372 % |
|
373 \isatagquote |
|
374 \isacommand{instantiation}\isamarkupfalse% |
|
375 \ nat\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline |
|
376 \isakeyword{begin}\isanewline |
|
377 \isanewline |
|
378 \isacommand{definition}\isamarkupfalse% |
|
379 \isanewline |
|
380 \ \ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
381 \isanewline |
|
382 \isacommand{definition}\isamarkupfalse% |
|
383 \isanewline |
|
384 \ \ neutral{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
385 \isanewline |
|
386 \isacommand{instance}\isamarkupfalse% |
|
387 \ \isacommand{proof}\isamarkupfalse% |
|
388 \isanewline |
|
389 \ \ \isacommand{fix}\isamarkupfalse% |
|
390 \ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline |
|
391 \ \ \isacommand{show}\isamarkupfalse% |
|
392 \ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline |
|
393 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
|
394 \ neutral{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
395 \ simp\isanewline |
|
396 \isacommand{next}\isamarkupfalse% |
|
397 \isanewline |
|
398 \ \ \isacommand{fix}\isamarkupfalse% |
|
399 \ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline |
|
400 \ \ \isacommand{show}\isamarkupfalse% |
|
401 \ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ k\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline |
|
402 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
|
403 \ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
404 \ simp\isanewline |
|
405 \isacommand{qed}\isamarkupfalse% |
|
406 \isanewline |
|
407 \isanewline |
|
408 \isacommand{end}\isamarkupfalse% |
|
409 \isanewline |
|
410 \isanewline |
|
411 \isacommand{instantiation}\isamarkupfalse% |
|
412 \ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoidl{\isacharcomma}\ monoidl{\isacharparenright}\ monoidl\isanewline |
|
413 \isakeyword{begin}\isanewline |
|
414 \isanewline |
|
415 \isacommand{definition}\isamarkupfalse% |
|
416 \isanewline |
|
417 \ \ neutral{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isasymone}{\isacharcomma}\ {\isasymone}{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
418 \isanewline |
|
419 \isacommand{instance}\isamarkupfalse% |
|
420 \ \isacommand{proof}\isamarkupfalse% |
|
421 \isanewline |
|
422 \ \ \isacommand{fix}\isamarkupfalse% |
|
423 \ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}monoidl\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}monoidl{\isachardoublequoteclose}\isanewline |
|
424 \ \ \isacommand{show}\isamarkupfalse% |
|
425 \ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline |
|
426 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
|
427 \ neutral{\isacharunderscore}prod{\isacharunderscore}def\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
428 \ {\isacharparenleft}simp\ add{\isacharcolon}\ neutl{\isacharparenright}\isanewline |
|
429 \isacommand{qed}\isamarkupfalse% |
|
430 \isanewline |
|
431 \isanewline |
|
432 \isacommand{end}\isamarkupfalse% |
|
433 % |
|
434 \endisatagquote |
|
435 {\isafoldquote}% |
|
436 % |
|
437 \isadelimquote |
|
438 % |
|
439 \endisadelimquote |
|
440 % |
|
441 \begin{isamarkuptext}% |
|
442 \noindent Fully-fledged monoids are modelled by another subclass |
|
443 which does not add new parameters but tightens the specification:% |
|
444 \end{isamarkuptext}% |
|
445 \isamarkuptrue% |
|
446 % |
|
447 \isadelimquote |
|
448 % |
|
449 \endisadelimquote |
|
450 % |
|
451 \isatagquote |
|
452 \isacommand{class}\isamarkupfalse% |
|
453 \ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline |
|
454 \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline |
|
455 \isanewline |
|
456 \isacommand{instantiation}\isamarkupfalse% |
|
457 \ nat\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoid\ \isanewline |
|
458 \isakeyword{begin}\isanewline |
|
459 \isanewline |
|
460 \isacommand{instance}\isamarkupfalse% |
|
461 \ \isacommand{proof}\isamarkupfalse% |
|
462 \isanewline |
|
463 \ \ \isacommand{fix}\isamarkupfalse% |
|
464 \ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline |
|
465 \ \ \isacommand{show}\isamarkupfalse% |
|
466 \ {\isachardoublequoteopen}n\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline |
|
467 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
|
468 \ neutral{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
469 \ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline |
|
470 \isacommand{next}\isamarkupfalse% |
|
471 \isanewline |
|
472 \ \ \isacommand{fix}\isamarkupfalse% |
|
473 \ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline |
|
474 \ \ \isacommand{show}\isamarkupfalse% |
|
475 \ {\isachardoublequoteopen}k\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline |
|
476 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
|
477 \ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
478 \ simp\isanewline |
|
479 \isacommand{qed}\isamarkupfalse% |
|
480 \isanewline |
|
481 \isanewline |
|
482 \isacommand{end}\isamarkupfalse% |
|
483 \isanewline |
|
484 \isanewline |
|
485 \isacommand{instantiation}\isamarkupfalse% |
|
486 \ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoid{\isacharcomma}\ monoid{\isacharparenright}\ monoid\isanewline |
|
487 \isakeyword{begin}\isanewline |
|
488 \isanewline |
|
489 \isacommand{instance}\isamarkupfalse% |
|
490 \ \isacommand{proof}\isamarkupfalse% |
|
491 \ \isanewline |
|
492 \ \ \isacommand{fix}\isamarkupfalse% |
|
493 \ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}monoid\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}monoid{\isachardoublequoteclose}\isanewline |
|
494 \ \ \isacommand{show}\isamarkupfalse% |
|
495 \ {\isachardoublequoteopen}p\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline |
|
496 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
|
497 \ neutral{\isacharunderscore}prod{\isacharunderscore}def\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% |
|
498 \ {\isacharparenleft}simp\ add{\isacharcolon}\ neutr{\isacharparenright}\isanewline |
|
499 \isacommand{qed}\isamarkupfalse% |
|
500 \isanewline |
|
501 \isanewline |
|
502 \isacommand{end}\isamarkupfalse% |
|
503 % |
|
504 \endisatagquote |
|
505 {\isafoldquote}% |
|
506 % |
|
507 \isadelimquote |
|
508 % |
|
509 \endisadelimquote |
|
510 % |
|
511 \begin{isamarkuptext}% |
|
512 \noindent To finish our small algebra example, we add a \isa{group} class |
|
513 with a corresponding instance:% |
|
514 \end{isamarkuptext}% |
|
515 \isamarkuptrue% |
|
516 % |
|
517 \isadelimquote |
|
518 % |
|
519 \endisadelimquote |
|
520 % |
|
521 \isatagquote |
|
522 \isacommand{class}\isamarkupfalse% |
|
523 \ group\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline |
|
524 \ \ \isakeyword{fixes}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline |
|
525 \ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline |
|
526 \isanewline |
|
527 \isacommand{instantiation}\isamarkupfalse% |
|
528 \ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline |
|
529 \isakeyword{begin}\isanewline |
|
530 \isanewline |
|
531 \isacommand{definition}\isamarkupfalse% |
|
532 \isanewline |
|
533 \ \ inverse{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}i{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
534 \isanewline |
|
535 \isacommand{instance}\isamarkupfalse% |
|
536 \ \isacommand{proof}\isamarkupfalse% |
|
537 \isanewline |
|
538 \ \ \isacommand{fix}\isamarkupfalse% |
|
539 \ i\ {\isacharcolon}{\isacharcolon}\ int\isanewline |
|
540 \ \ \isacommand{have}\isamarkupfalse% |
|
541 \ {\isachardoublequoteopen}{\isacharminus}i\ {\isacharplus}\ i\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
542 \ simp\isanewline |
|
543 \ \ \isacommand{then}\isamarkupfalse% |
|
544 \ \isacommand{show}\isamarkupfalse% |
|
545 \ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymotimes}\ i\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline |
|
546 \ \ \ \ \isacommand{unfolding}\isamarkupfalse% |
|
547 \ mult{\isacharunderscore}int{\isacharunderscore}def\ neutral{\isacharunderscore}int{\isacharunderscore}def\ inverse{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse% |
|
548 \isanewline |
|
549 \isacommand{qed}\isamarkupfalse% |
|
550 \isanewline |
|
551 \isanewline |
|
552 \isacommand{end}\isamarkupfalse% |
|
553 % |
|
554 \endisatagquote |
|
555 {\isafoldquote}% |
|
556 % |
|
557 \isadelimquote |
|
558 % |
|
559 \endisadelimquote |
|
560 % |
|
561 \isamarkupsection{Type classes as locales% |
|
562 } |
|
563 \isamarkuptrue% |
|
564 % |
|
565 \isamarkupsubsection{A look behind the scene% |
|
566 } |
|
567 \isamarkuptrue% |
|
568 % |
|
569 \begin{isamarkuptext}% |
|
570 The example above gives an impression how Isar type classes work |
|
571 in practice. As stated in the introduction, classes also provide |
|
572 a link to Isar's locale system. Indeed, the logical core of a class |
|
573 is nothing else than a locale:% |
|
574 \end{isamarkuptext}% |
|
575 \isamarkuptrue% |
|
576 % |
|
577 \isadelimquote |
|
578 % |
|
579 \endisadelimquote |
|
580 % |
|
581 \isatagquote |
|
582 \isacommand{class}\isamarkupfalse% |
|
583 \ idem\ {\isacharequal}\isanewline |
|
584 \ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline |
|
585 \ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}% |
|
586 \endisatagquote |
|
587 {\isafoldquote}% |
|
588 % |
|
589 \isadelimquote |
|
590 % |
|
591 \endisadelimquote |
|
592 % |
|
593 \begin{isamarkuptext}% |
|
594 \noindent essentially introduces the locale% |
|
595 \end{isamarkuptext}% |
|
596 \isamarkuptrue% |
|
597 \ % |
|
598 \isadeliminvisible |
|
599 % |
|
600 \endisadeliminvisible |
|
601 % |
|
602 \isataginvisible |
|
603 % |
|
604 \endisataginvisible |
|
605 {\isafoldinvisible}% |
|
606 % |
|
607 \isadeliminvisible |
|
608 % |
|
609 \endisadeliminvisible |
|
610 % |
|
611 \isadelimquote |
|
612 % |
|
613 \endisadelimquote |
|
614 % |
|
615 \isatagquote |
|
616 \isacommand{locale}\isamarkupfalse% |
|
617 \ idem\ {\isacharequal}\isanewline |
|
618 \ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline |
|
619 \ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}% |
|
620 \endisatagquote |
|
621 {\isafoldquote}% |
|
622 % |
|
623 \isadelimquote |
|
624 % |
|
625 \endisadelimquote |
|
626 % |
|
627 \begin{isamarkuptext}% |
|
628 \noindent together with corresponding constant(s):% |
|
629 \end{isamarkuptext}% |
|
630 \isamarkuptrue% |
|
631 % |
|
632 \isadelimquote |
|
633 % |
|
634 \endisadelimquote |
|
635 % |
|
636 \isatagquote |
|
637 \isacommand{consts}\isamarkupfalse% |
|
638 \ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}% |
|
639 \endisatagquote |
|
640 {\isafoldquote}% |
|
641 % |
|
642 \isadelimquote |
|
643 % |
|
644 \endisadelimquote |
|
645 % |
|
646 \begin{isamarkuptext}% |
|
647 \noindent The connection to the type system is done by means |
|
648 of a primitive axclass% |
|
649 \end{isamarkuptext}% |
|
650 \isamarkuptrue% |
|
651 \ % |
|
652 \isadeliminvisible |
|
653 % |
|
654 \endisadeliminvisible |
|
655 % |
|
656 \isataginvisible |
|
657 % |
|
658 \endisataginvisible |
|
659 {\isafoldinvisible}% |
|
660 % |
|
661 \isadeliminvisible |
|
662 % |
|
663 \endisadeliminvisible |
|
664 % |
|
665 \isadelimquote |
|
666 % |
|
667 \endisadelimquote |
|
668 % |
|
669 \isatagquote |
|
670 \isacommand{axclass}\isamarkupfalse% |
|
671 \ idem\ {\isacharless}\ type\isanewline |
|
672 \ \ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}\ % |
|
673 \endisatagquote |
|
674 {\isafoldquote}% |
|
675 % |
|
676 \isadelimquote |
|
677 % |
|
678 \endisadelimquote |
|
679 % |
|
680 \isadeliminvisible |
|
681 % |
|
682 \endisadeliminvisible |
|
683 % |
|
684 \isataginvisible |
|
685 % |
|
686 \endisataginvisible |
|
687 {\isafoldinvisible}% |
|
688 % |
|
689 \isadeliminvisible |
|
690 % |
|
691 \endisadeliminvisible |
|
692 % |
|
693 \begin{isamarkuptext}% |
|
694 \noindent together with a corresponding interpretation:% |
|
695 \end{isamarkuptext}% |
|
696 \isamarkuptrue% |
|
697 % |
|
698 \isadelimquote |
|
699 % |
|
700 \endisadelimquote |
|
701 % |
|
702 \isatagquote |
|
703 \isacommand{interpretation}\isamarkupfalse% |
|
704 \ idem{\isacharunderscore}class{\isacharcolon}\isanewline |
|
705 \ \ idem\ {\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isasymalpha}{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline |
|
706 \isacommand{proof}\isamarkupfalse% |
|
707 \ \isacommand{qed}\isamarkupfalse% |
|
708 \ {\isacharparenleft}rule\ idem{\isacharparenright}% |
|
709 \endisatagquote |
|
710 {\isafoldquote}% |
|
711 % |
|
712 \isadelimquote |
|
713 % |
|
714 \endisadelimquote |
|
715 % |
|
716 \begin{isamarkuptext}% |
|
717 \noindent This gives you at hand the full power of the Isabelle module system; |
|
718 conclusions in locale \isa{idem} are implicitly propagated |
|
719 to class \isa{idem}.% |
|
720 \end{isamarkuptext}% |
|
721 \isamarkuptrue% |
|
722 \ % |
|
723 \isadeliminvisible |
|
724 % |
|
725 \endisadeliminvisible |
|
726 % |
|
727 \isataginvisible |
|
728 % |
|
729 \endisataginvisible |
|
730 {\isafoldinvisible}% |
|
731 % |
|
732 \isadeliminvisible |
|
733 % |
|
734 \endisadeliminvisible |
|
735 % |
|
736 \isamarkupsubsection{Abstract reasoning% |
|
737 } |
|
738 \isamarkuptrue% |
|
739 % |
|
740 \begin{isamarkuptext}% |
|
741 Isabelle locales enable reasoning at a general level, while results |
|
742 are implicitly transferred to all instances. For example, we can |
|
743 now establish the \isa{left{\isacharunderscore}cancel} lemma for groups, which |
|
744 states that the function \isa{{\isacharparenleft}x\ {\isasymotimes}{\isacharparenright}} is injective:% |
|
745 \end{isamarkuptext}% |
|
746 \isamarkuptrue% |
|
747 % |
|
748 \isadelimquote |
|
749 % |
|
750 \endisadelimquote |
|
751 % |
|
752 \isatagquote |
|
753 \isacommand{lemma}\isamarkupfalse% |
|
754 \ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ left{\isacharunderscore}cancel{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline |
|
755 \isacommand{proof}\isamarkupfalse% |
|
756 \isanewline |
|
757 \ \ \isacommand{assume}\isamarkupfalse% |
|
758 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline |
|
759 \ \ \isacommand{then}\isamarkupfalse% |
|
760 \ \isacommand{have}\isamarkupfalse% |
|
761 \ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isacharequal}\ x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
762 \ simp\isanewline |
|
763 \ \ \isacommand{then}\isamarkupfalse% |
|
764 \ \isacommand{have}\isamarkupfalse% |
|
765 \ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymdiv}\ {\isasymotimes}\ x{\isacharparenright}\ {\isasymotimes}\ y\ {\isacharequal}\ {\isacharparenleft}x{\isasymdiv}\ {\isasymotimes}\ x{\isacharparenright}\ {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse% |
|
766 \ assoc\ \isacommand{by}\isamarkupfalse% |
|
767 \ simp\isanewline |
|
768 \ \ \isacommand{then}\isamarkupfalse% |
|
769 \ \isacommand{show}\isamarkupfalse% |
|
770 \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse% |
|
771 \ neutl\ \isakeyword{and}\ invl\ \isacommand{by}\isamarkupfalse% |
|
772 \ simp\isanewline |
|
773 \isacommand{next}\isamarkupfalse% |
|
774 \isanewline |
|
775 \ \ \isacommand{assume}\isamarkupfalse% |
|
776 \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline |
|
777 \ \ \isacommand{then}\isamarkupfalse% |
|
778 \ \isacommand{show}\isamarkupfalse% |
|
779 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
780 \ simp\isanewline |
|
781 \isacommand{qed}\isamarkupfalse% |
|
782 % |
|
783 \endisatagquote |
|
784 {\isafoldquote}% |
|
785 % |
|
786 \isadelimquote |
|
787 % |
|
788 \endisadelimquote |
|
789 % |
|
790 \begin{isamarkuptext}% |
|
791 \noindent Here the \qt{\hyperlink{keyword.in}{\mbox{\isa{\isakeyword{in}}}} \isa{group}} target specification |
|
792 indicates that the result is recorded within that context for later |
|
793 use. This local theorem is also lifted to the global one \hyperlink{fact.group.left-cancel:}{\mbox{\isa{group{\isachardot}left{\isacharunderscore}cancel{\isacharcolon}}}} \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}group{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}. Since type \isa{int} has been made an instance of |
|
794 \isa{group} before, we may refer to that fact as well: \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ int{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.% |
|
795 \end{isamarkuptext}% |
|
796 \isamarkuptrue% |
|
797 % |
|
798 \isamarkupsubsection{Derived definitions% |
|
799 } |
|
800 \isamarkuptrue% |
|
801 % |
|
802 \begin{isamarkuptext}% |
|
803 Isabelle locales support a concept of local definitions |
|
804 in locales:% |
|
805 \end{isamarkuptext}% |
|
806 \isamarkuptrue% |
|
807 % |
|
808 \isadelimquote |
|
809 % |
|
810 \endisadelimquote |
|
811 % |
|
812 \isatagquote |
|
813 \isacommand{primrec}\isamarkupfalse% |
|
814 \ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
|
815 \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline |
|
816 \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}% |
|
817 \endisatagquote |
|
818 {\isafoldquote}% |
|
819 % |
|
820 \isadelimquote |
|
821 % |
|
822 \endisadelimquote |
|
823 % |
|
824 \begin{isamarkuptext}% |
|
825 \noindent If the locale \isa{group} is also a class, this local |
|
826 definition is propagated onto a global definition of |
|
827 \isa{{\isachardoublequote}pow{\isacharunderscore}nat\ {\isasymColon}\ nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid{\isachardoublequote}} |
|
828 with corresponding theorems |
|
829 |
|
830 \isa{pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}\isasep\isanewline% |
|
831 pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x}. |
|
832 |
|
833 \noindent As you can see from this example, for local |
|
834 definitions you may use any specification tool |
|
835 which works together with locales (e.g. \cite{krauss2006}).% |
|
836 \end{isamarkuptext}% |
|
837 \isamarkuptrue% |
|
838 % |
|
839 \isamarkupsubsection{A functor analogy% |
|
840 } |
|
841 \isamarkuptrue% |
|
842 % |
|
843 \begin{isamarkuptext}% |
|
844 We introduced Isar classes by analogy to type classes |
|
845 functional programming; if we reconsider this in the |
|
846 context of what has been said about type classes and locales, |
|
847 we can drive this analogy further by stating that type |
|
848 classes essentially correspond to functors which have |
|
849 a canonical interpretation as type classes. |
|
850 Anyway, there is also the possibility of other interpretations. |
|
851 For example, also \isa{list}s form a monoid with |
|
852 \isa{append} and \isa{{\isacharbrackleft}{\isacharbrackright}} as operations, but it |
|
853 seems inappropriate to apply to lists |
|
854 the same operations as for genuinely algebraic types. |
|
855 In such a case, we simply can do a particular interpretation |
|
856 of monoids for lists:% |
|
857 \end{isamarkuptext}% |
|
858 \isamarkuptrue% |
|
859 % |
|
860 \isadelimquote |
|
861 % |
|
862 \endisadelimquote |
|
863 % |
|
864 \isatagquote |
|
865 \isacommand{interpretation}\isamarkupfalse% |
|
866 \ list{\isacharunderscore}monoid{\isacharbang}{\isacharcolon}\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline |
|
867 \ \ \isacommand{proof}\isamarkupfalse% |
|
868 \ \isacommand{qed}\isamarkupfalse% |
|
869 \ auto% |
|
870 \endisatagquote |
|
871 {\isafoldquote}% |
|
872 % |
|
873 \isadelimquote |
|
874 % |
|
875 \endisadelimquote |
|
876 % |
|
877 \begin{isamarkuptext}% |
|
878 \noindent This enables us to apply facts on monoids |
|
879 to lists, e.g. \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ x\ {\isacharequal}\ x}. |
|
880 |
|
881 When using this interpretation pattern, it may also |
|
882 be appropriate to map derived definitions accordingly:% |
|
883 \end{isamarkuptext}% |
|
884 \isamarkuptrue% |
|
885 % |
|
886 \isadelimquote |
|
887 % |
|
888 \endisadelimquote |
|
889 % |
|
890 \isatagquote |
|
891 \isacommand{primrec}\isamarkupfalse% |
|
892 \ replicate\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ list\ {\isasymRightarrow}\ {\isasymalpha}\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
|
893 \ \ {\isachardoublequoteopen}replicate\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline |
|
894 \ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline |
|
895 \isanewline |
|
896 \isacommand{interpretation}\isamarkupfalse% |
|
897 \ list{\isacharunderscore}monoid{\isacharbang}{\isacharcolon}\ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
|
898 \ \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline |
|
899 \isacommand{proof}\isamarkupfalse% |
|
900 \ {\isacharminus}\isanewline |
|
901 \ \ \isacommand{interpret}\isamarkupfalse% |
|
902 \ monoid\ append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% |
|
903 \isanewline |
|
904 \ \ \isacommand{show}\isamarkupfalse% |
|
905 \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline |
|
906 \ \ \isacommand{proof}\isamarkupfalse% |
|
907 \isanewline |
|
908 \ \ \ \ \isacommand{fix}\isamarkupfalse% |
|
909 \ n\isanewline |
|
910 \ \ \ \ \isacommand{show}\isamarkupfalse% |
|
911 \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ n\ {\isacharequal}\ replicate\ n{\isachardoublequoteclose}\isanewline |
|
912 \ \ \ \ \ \ \isacommand{by}\isamarkupfalse% |
|
913 \ {\isacharparenleft}induct\ n{\isacharparenright}\ auto\isanewline |
|
914 \ \ \isacommand{qed}\isamarkupfalse% |
|
915 \isanewline |
|
916 \isacommand{qed}\isamarkupfalse% |
|
917 \ intro{\isacharunderscore}locales% |
|
918 \endisatagquote |
|
919 {\isafoldquote}% |
|
920 % |
|
921 \isadelimquote |
|
922 % |
|
923 \endisadelimquote |
|
924 % |
|
925 \isamarkupsubsection{Additional subclass relations% |
|
926 } |
|
927 \isamarkuptrue% |
|
928 % |
|
929 \begin{isamarkuptext}% |
|
930 Any \isa{group} is also a \isa{monoid}; this |
|
931 can be made explicit by claiming an additional |
|
932 subclass relation, |
|
933 together with a proof of the logical difference:% |
|
934 \end{isamarkuptext}% |
|
935 \isamarkuptrue% |
|
936 % |
|
937 \isadelimquote |
|
938 % |
|
939 \endisadelimquote |
|
940 % |
|
941 \isatagquote |
|
942 \isacommand{subclass}\isamarkupfalse% |
|
943 \ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ monoid\isanewline |
|
944 \isacommand{proof}\isamarkupfalse% |
|
945 \isanewline |
|
946 \ \ \isacommand{fix}\isamarkupfalse% |
|
947 \ x\isanewline |
|
948 \ \ \isacommand{from}\isamarkupfalse% |
|
949 \ invl\ \isacommand{have}\isamarkupfalse% |
|
950 \ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
951 \ simp\isanewline |
|
952 \ \ \isacommand{with}\isamarkupfalse% |
|
953 \ assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}\ neutl\ invl\ \isacommand{have}\isamarkupfalse% |
|
954 \ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ {\isasymone}{\isacharparenright}\ {\isacharequal}\ x{\isasymdiv}\ {\isasymotimes}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
955 \ simp\isanewline |
|
956 \ \ \isacommand{with}\isamarkupfalse% |
|
957 \ left{\isacharunderscore}cancel\ \isacommand{show}\isamarkupfalse% |
|
958 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
|
959 \ simp\isanewline |
|
960 \isacommand{qed}\isamarkupfalse% |
|
961 % |
|
962 \endisatagquote |
|
963 {\isafoldquote}% |
|
964 % |
|
965 \isadelimquote |
|
966 % |
|
967 \endisadelimquote |
|
968 % |
|
969 \begin{isamarkuptext}% |
|
970 The logical proof is carried out on the locale level. |
|
971 Afterwards it is propagated |
|
972 to the type system, making \isa{group} an instance of |
|
973 \isa{monoid} by adding an additional edge |
|
974 to the graph of subclass relations |
|
975 (cf.\ \figref{fig:subclass}). |
|
976 |
|
977 \begin{figure}[htbp] |
|
978 \begin{center} |
|
979 \small |
|
980 \unitlength 0.6mm |
|
981 \begin{picture}(40,60)(0,0) |
|
982 \put(20,60){\makebox(0,0){\isa{semigroup}}} |
|
983 \put(20,40){\makebox(0,0){\isa{monoidl}}} |
|
984 \put(00,20){\makebox(0,0){\isa{monoid}}} |
|
985 \put(40,00){\makebox(0,0){\isa{group}}} |
|
986 \put(20,55){\vector(0,-1){10}} |
|
987 \put(15,35){\vector(-1,-1){10}} |
|
988 \put(25,35){\vector(1,-3){10}} |
|
989 \end{picture} |
|
990 \hspace{8em} |
|
991 \begin{picture}(40,60)(0,0) |
|
992 \put(20,60){\makebox(0,0){\isa{semigroup}}} |
|
993 \put(20,40){\makebox(0,0){\isa{monoidl}}} |
|
994 \put(00,20){\makebox(0,0){\isa{monoid}}} |
|
995 \put(40,00){\makebox(0,0){\isa{group}}} |
|
996 \put(20,55){\vector(0,-1){10}} |
|
997 \put(15,35){\vector(-1,-1){10}} |
|
998 \put(05,15){\vector(3,-1){30}} |
|
999 \end{picture} |
|
1000 \caption{Subclass relationship of monoids and groups: |
|
1001 before and after establishing the relationship |
|
1002 \isa{group\ {\isasymsubseteq}\ monoid}; transitive edges are left out.} |
|
1003 \label{fig:subclass} |
|
1004 \end{center} |
|
1005 \end{figure} |
|
1006 |
|
1007 For illustration, a derived definition |
|
1008 in \isa{group} which uses \isa{pow{\isacharunderscore}nat}:% |
|
1009 \end{isamarkuptext}% |
|
1010 \isamarkuptrue% |
|
1011 % |
|
1012 \isadelimquote |
|
1013 % |
|
1014 \endisadelimquote |
|
1015 % |
|
1016 \isatagquote |
|
1017 \isacommand{definition}\isamarkupfalse% |
|
1018 \ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
|
1019 \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline |
|
1020 \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline |
|
1021 \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}% |
|
1022 \endisatagquote |
|
1023 {\isafoldquote}% |
|
1024 % |
|
1025 \isadelimquote |
|
1026 % |
|
1027 \endisadelimquote |
|
1028 % |
|
1029 \begin{isamarkuptext}% |
|
1030 \noindent yields the global definition of |
|
1031 \isa{{\isachardoublequote}pow{\isacharunderscore}int\ {\isasymColon}\ int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequote}} |
|
1032 with the corresponding theorem \isa{pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ {\isadigit{0}}\ {\isasymle}\ k\ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}}.% |
|
1033 \end{isamarkuptext}% |
|
1034 \isamarkuptrue% |
|
1035 % |
|
1036 \isamarkupsubsection{A note on syntax% |
|
1037 } |
|
1038 \isamarkuptrue% |
|
1039 % |
|
1040 \begin{isamarkuptext}% |
|
1041 As a commodity, class context syntax allows to refer |
|
1042 to local class operations and their global counterparts |
|
1043 uniformly; type inference resolves ambiguities. For example:% |
|
1044 \end{isamarkuptext}% |
|
1045 \isamarkuptrue% |
|
1046 % |
|
1047 \isadelimquote |
|
1048 % |
|
1049 \endisadelimquote |
|
1050 % |
|
1051 \isatagquote |
|
1052 \isacommand{context}\isamarkupfalse% |
|
1053 \ semigroup\isanewline |
|
1054 \isakeyword{begin}\isanewline |
|
1055 \isanewline |
|
1056 \isacommand{term}\isamarkupfalse% |
|
1057 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y{\isachardoublequoteclose}\ % |
|
1058 \isamarkupcmt{example 1% |
|
1059 } |
|
1060 \isanewline |
|
1061 \isacommand{term}\isamarkupfalse% |
|
1062 \ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ y{\isachardoublequoteclose}\ % |
|
1063 \isamarkupcmt{example 2% |
|
1064 } |
|
1065 \isanewline |
|
1066 \isanewline |
|
1067 \isacommand{end}\isamarkupfalse% |
|
1068 \isanewline |
|
1069 \isanewline |
|
1070 \isacommand{term}\isamarkupfalse% |
|
1071 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y{\isachardoublequoteclose}\ % |
|
1072 \isamarkupcmt{example 3% |
|
1073 } |
|
1074 % |
|
1075 \endisatagquote |
|
1076 {\isafoldquote}% |
|
1077 % |
|
1078 \isadelimquote |
|
1079 % |
|
1080 \endisadelimquote |
|
1081 % |
|
1082 \begin{isamarkuptext}% |
|
1083 \noindent Here in example 1, the term refers to the local class operation |
|
1084 \isa{mult\ {\isacharbrackleft}{\isasymalpha}{\isacharbrackright}}, whereas in example 2 the type constraint |
|
1085 enforces the global class operation \isa{mult\ {\isacharbrackleft}nat{\isacharbrackright}}. |
|
1086 In the global context in example 3, the reference is |
|
1087 to the polymorphic global class operation \isa{mult\ {\isacharbrackleft}{\isacharquery}{\isasymalpha}\ {\isasymColon}\ semigroup{\isacharbrackright}}.% |
|
1088 \end{isamarkuptext}% |
|
1089 \isamarkuptrue% |
|
1090 % |
|
1091 \isamarkupsection{Further issues% |
|
1092 } |
|
1093 \isamarkuptrue% |
|
1094 % |
|
1095 \isamarkupsubsection{Type classes and code generation% |
|
1096 } |
|
1097 \isamarkuptrue% |
|
1098 % |
|
1099 \begin{isamarkuptext}% |
|
1100 Turning back to the first motivation for type classes, |
|
1101 namely overloading, it is obvious that overloading |
|
1102 stemming from \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} statements and |
|
1103 \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} |
|
1104 targets naturally maps to Haskell type classes. |
|
1105 The code generator framework \cite{isabelle-codegen} |
|
1106 takes this into account. Concerning target languages |
|
1107 lacking type classes (e.g.~SML), type classes |
|
1108 are implemented by explicit dictionary construction. |
|
1109 As example, let's go back to the power function:% |
|
1110 \end{isamarkuptext}% |
|
1111 \isamarkuptrue% |
|
1112 % |
|
1113 \isadelimquote |
|
1114 % |
|
1115 \endisadelimquote |
|
1116 % |
|
1117 \isatagquote |
|
1118 \isacommand{definition}\isamarkupfalse% |
|
1119 \ example\ {\isacharcolon}{\isacharcolon}\ int\ \isakeyword{where}\isanewline |
|
1120 \ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}% |
|
1121 \endisatagquote |
|
1122 {\isafoldquote}% |
|
1123 % |
|
1124 \isadelimquote |
|
1125 % |
|
1126 \endisadelimquote |
|
1127 % |
|
1128 \begin{isamarkuptext}% |
|
1129 \noindent This maps to Haskell as:% |
|
1130 \end{isamarkuptext}% |
|
1131 \isamarkuptrue% |
|
1132 % |
|
1133 \isadelimquote |
|
1134 % |
|
1135 \endisadelimquote |
|
1136 % |
|
1137 \isatagquote |
|
1138 % |
|
1139 \begin{isamarkuptext}% |
|
1140 \isatypewriter% |
|
1141 \noindent% |
|
1142 \hspace*{0pt}module Example where {\char123}\\ |
|
1143 \hspace*{0pt}\\ |
|
1144 \hspace*{0pt}\\ |
|
1145 \hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\ |
|
1146 \hspace*{0pt}\\ |
|
1147 \hspace*{0pt}nat{\char95}aux ::~Integer -> Nat -> Nat;\\ |
|
1148 \hspace*{0pt}nat{\char95}aux i n = (if i <= 0 then n else nat{\char95}aux (i - 1) (Suc n));\\ |
|
1149 \hspace*{0pt}\\ |
|
1150 \hspace*{0pt}nat ::~Integer -> Nat;\\ |
|
1151 \hspace*{0pt}nat i = nat{\char95}aux i Zero{\char95}nat;\\ |
|
1152 \hspace*{0pt}\\ |
|
1153 \hspace*{0pt}class Semigroup a where {\char123}\\ |
|
1154 \hspace*{0pt} ~mult ::~a -> a -> a;\\ |
|
1155 \hspace*{0pt}{\char125};\\ |
|
1156 \hspace*{0pt}\\ |
|
1157 \hspace*{0pt}class (Semigroup a) => Monoidl a where {\char123}\\ |
|
1158 \hspace*{0pt} ~neutral ::~a;\\ |
|
1159 \hspace*{0pt}{\char125};\\ |
|
1160 \hspace*{0pt}\\ |
|
1161 \hspace*{0pt}class (Monoidl a) => Monoid a where {\char123}\\ |
|
1162 \hspace*{0pt}{\char125};\\ |
|
1163 \hspace*{0pt}\\ |
|
1164 \hspace*{0pt}class (Monoid a) => Group a where {\char123}\\ |
|
1165 \hspace*{0pt} ~inverse ::~a -> a;\\ |
|
1166 \hspace*{0pt}{\char125};\\ |
|
1167 \hspace*{0pt}\\ |
|
1168 \hspace*{0pt}inverse{\char95}int ::~Integer -> Integer;\\ |
|
1169 \hspace*{0pt}inverse{\char95}int i = negate i;\\ |
|
1170 \hspace*{0pt}\\ |
|
1171 \hspace*{0pt}neutral{\char95}int ::~Integer;\\ |
|
1172 \hspace*{0pt}neutral{\char95}int = 0;\\ |
|
1173 \hspace*{0pt}\\ |
|
1174 \hspace*{0pt}mult{\char95}int ::~Integer -> Integer -> Integer;\\ |
|
1175 \hspace*{0pt}mult{\char95}int i j = i + j;\\ |
|
1176 \hspace*{0pt}\\ |
|
1177 \hspace*{0pt}instance Semigroup Integer where {\char123}\\ |
|
1178 \hspace*{0pt} ~mult = mult{\char95}int;\\ |
|
1179 \hspace*{0pt}{\char125};\\ |
|
1180 \hspace*{0pt}\\ |
|
1181 \hspace*{0pt}instance Monoidl Integer where {\char123}\\ |
|
1182 \hspace*{0pt} ~neutral = neutral{\char95}int;\\ |
|
1183 \hspace*{0pt}{\char125};\\ |
|
1184 \hspace*{0pt}\\ |
|
1185 \hspace*{0pt}instance Monoid Integer where {\char123}\\ |
|
1186 \hspace*{0pt}{\char125};\\ |
|
1187 \hspace*{0pt}\\ |
|
1188 \hspace*{0pt}instance Group Integer where {\char123}\\ |
|
1189 \hspace*{0pt} ~inverse = inverse{\char95}int;\\ |
|
1190 \hspace*{0pt}{\char125};\\ |
|
1191 \hspace*{0pt}\\ |
|
1192 \hspace*{0pt}pow{\char95}nat ::~forall a.~(Monoid a) => Nat -> a -> a;\\ |
|
1193 \hspace*{0pt}pow{\char95}nat Zero{\char95}nat x = neutral;\\ |
|
1194 \hspace*{0pt}pow{\char95}nat (Suc n) x = mult x (pow{\char95}nat n x);\\ |
|
1195 \hspace*{0pt}\\ |
|
1196 \hspace*{0pt}pow{\char95}int ::~forall a.~(Group a) => Integer -> a -> a;\\ |
|
1197 \hspace*{0pt}pow{\char95}int k x =\\ |
|
1198 \hspace*{0pt} ~(if 0 <= k then pow{\char95}nat (nat k) x\\ |
|
1199 \hspace*{0pt} ~~~else inverse (pow{\char95}nat (nat (negate k)) x));\\ |
|
1200 \hspace*{0pt}\\ |
|
1201 \hspace*{0pt}example ::~Integer;\\ |
|
1202 \hspace*{0pt}example = pow{\char95}int 10 (-2);\\ |
|
1203 \hspace*{0pt}\\ |
|
1204 \hspace*{0pt}{\char125}% |
|
1205 \end{isamarkuptext}% |
|
1206 \isamarkuptrue% |
|
1207 % |
|
1208 \endisatagquote |
|
1209 {\isafoldquote}% |
|
1210 % |
|
1211 \isadelimquote |
|
1212 % |
|
1213 \endisadelimquote |
|
1214 % |
|
1215 \begin{isamarkuptext}% |
|
1216 \noindent The whole code in SML with explicit dictionary passing:% |
|
1217 \end{isamarkuptext}% |
|
1218 \isamarkuptrue% |
|
1219 % |
|
1220 \isadelimquote |
|
1221 % |
|
1222 \endisadelimquote |
|
1223 % |
|
1224 \isatagquote |
|
1225 % |
|
1226 \begin{isamarkuptext}% |
|
1227 \isatypewriter% |
|
1228 \noindent% |
|
1229 \hspace*{0pt}structure Example = \\ |
|
1230 \hspace*{0pt}struct\\ |
|
1231 \hspace*{0pt}\\ |
|
1232 \hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\ |
|
1233 \hspace*{0pt}\\ |
|
1234 \hspace*{0pt}fun nat{\char95}aux i n =\\ |
|
1235 \hspace*{0pt} ~(if IntInf.<= (i,~(0 :~IntInf.int)) then n\\ |
|
1236 \hspace*{0pt} ~~~else nat{\char95}aux (IntInf.- (i,~(1 :~IntInf.int))) (Suc n));\\ |
|
1237 \hspace*{0pt}\\ |
|
1238 \hspace*{0pt}fun nat i = nat{\char95}aux i Zero{\char95}nat;\\ |
|
1239 \hspace*{0pt}\\ |
|
1240 \hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\ |
|
1241 \hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\ |
|
1242 \hspace*{0pt}\\ |
|
1243 \hspace*{0pt}type 'a monoidl =\\ |
|
1244 \hspace*{0pt} ~{\char123}Classes{\char95}{\char95}semigroup{\char95}monoidl :~'a semigroup,~neutral :~'a{\char125};\\ |
|
1245 \hspace*{0pt}fun semigroup{\char95}monoidl (A{\char95}:'a monoidl) = {\char35}Classes{\char95}{\char95}semigroup{\char95}monoidl A{\char95};\\ |
|
1246 \hspace*{0pt}fun neutral (A{\char95}:'a monoidl) = {\char35}neutral A{\char95};\\ |
|
1247 \hspace*{0pt}\\ |
|
1248 \hspace*{0pt}type 'a monoid = {\char123}Classes{\char95}{\char95}monoidl{\char95}monoid :~'a monoidl{\char125};\\ |
|
1249 \hspace*{0pt}fun monoidl{\char95}monoid (A{\char95}:'a monoid) = {\char35}Classes{\char95}{\char95}monoidl{\char95}monoid A{\char95};\\ |
|
1250 \hspace*{0pt}\\ |
|
1251 \hspace*{0pt}type 'a group = {\char123}Classes{\char95}{\char95}monoid{\char95}group :~'a monoid,~inverse :~'a -> 'a{\char125};\\ |
|
1252 \hspace*{0pt}fun monoid{\char95}group (A{\char95}:'a group) = {\char35}Classes{\char95}{\char95}monoid{\char95}group A{\char95};\\ |
|
1253 \hspace*{0pt}fun inverse (A{\char95}:'a group) = {\char35}inverse A{\char95};\\ |
|
1254 \hspace*{0pt}\\ |
|
1255 \hspace*{0pt}fun inverse{\char95}int i = IntInf.{\char126}~i;\\ |
|
1256 \hspace*{0pt}\\ |
|
1257 \hspace*{0pt}val neutral{\char95}int :~IntInf.int = (0 :~IntInf.int)\\ |
|
1258 \hspace*{0pt}\\ |
|
1259 \hspace*{0pt}fun mult{\char95}int i j = IntInf.+ (i,~j);\\ |
|
1260 \hspace*{0pt}\\ |
|
1261 \hspace*{0pt}val semigroup{\char95}int = {\char123}mult = mult{\char95}int{\char125}~:~IntInf.int semigroup;\\ |
|
1262 \hspace*{0pt}\\ |
|
1263 \hspace*{0pt}val monoidl{\char95}int =\\ |
|
1264 \hspace*{0pt} ~{\char123}Classes{\char95}{\char95}semigroup{\char95}monoidl = semigroup{\char95}int,~neutral = neutral{\char95}int{\char125}~:\\ |
|
1265 \hspace*{0pt} ~IntInf.int monoidl;\\ |
|
1266 \hspace*{0pt}\\ |
|
1267 \hspace*{0pt}val monoid{\char95}int = {\char123}Classes{\char95}{\char95}monoidl{\char95}monoid = monoidl{\char95}int{\char125}~:\\ |
|
1268 \hspace*{0pt} ~IntInf.int monoid;\\ |
|
1269 \hspace*{0pt}\\ |
|
1270 \hspace*{0pt}val group{\char95}int =\\ |
|
1271 \hspace*{0pt} ~{\char123}Classes{\char95}{\char95}monoid{\char95}group = monoid{\char95}int,~inverse = inverse{\char95}int{\char125}~:\\ |
|
1272 \hspace*{0pt} ~IntInf.int group;\\ |
|
1273 \hspace*{0pt}\\ |
|
1274 \hspace*{0pt}fun pow{\char95}nat A{\char95}~Zero{\char95}nat x = neutral (monoidl{\char95}monoid A{\char95})\\ |
|
1275 \hspace*{0pt} ~| pow{\char95}nat A{\char95}~(Suc n) x =\\ |
|
1276 \hspace*{0pt} ~~~mult ((semigroup{\char95}monoidl o monoidl{\char95}monoid) A{\char95}) x (pow{\char95}nat A{\char95}~n x);\\ |
|
1277 \hspace*{0pt}\\ |
|
1278 \hspace*{0pt}fun pow{\char95}int A{\char95}~k x =\\ |
|
1279 \hspace*{0pt} ~(if IntInf.<= ((0 :~IntInf.int),~k)\\ |
|
1280 \hspace*{0pt} ~~~then pow{\char95}nat (monoid{\char95}group A{\char95}) (nat k) x\\ |
|
1281 \hspace*{0pt} ~~~else inverse A{\char95}~(pow{\char95}nat (monoid{\char95}group A{\char95}) (nat (IntInf.{\char126}~k)) x));\\ |
|
1282 \hspace*{0pt}\\ |
|
1283 \hspace*{0pt}val example :~IntInf.int =\\ |
|
1284 \hspace*{0pt} ~pow{\char95}int group{\char95}int (10 :~IntInf.int) ({\char126}2 :~IntInf.int)\\ |
|
1285 \hspace*{0pt}\\ |
|
1286 \hspace*{0pt}end;~(*struct Example*)% |
|
1287 \end{isamarkuptext}% |
|
1288 \isamarkuptrue% |
|
1289 % |
|
1290 \endisatagquote |
|
1291 {\isafoldquote}% |
|
1292 % |
|
1293 \isadelimquote |
|
1294 % |
|
1295 \endisadelimquote |
|
1296 % |
|
1297 \isamarkupsubsection{Inspecting the type class universe% |
|
1298 } |
|
1299 \isamarkuptrue% |
|
1300 % |
|
1301 \begin{isamarkuptext}% |
|
1302 To facilitate orientation in complex subclass structures, |
|
1303 two diagnostics commands are provided: |
|
1304 |
|
1305 \begin{description} |
|
1306 |
|
1307 \item[\hyperlink{command.print-classes}{\mbox{\isa{\isacommand{print{\isacharunderscore}classes}}}}] print a list of all classes |
|
1308 together with associated operations etc. |
|
1309 |
|
1310 \item[\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}] visualizes the subclass relation |
|
1311 between all classes as a Hasse diagram. |
|
1312 |
|
1313 \end{description}% |
|
1314 \end{isamarkuptext}% |
|
1315 \isamarkuptrue% |
|
1316 % |
|
1317 \isadelimtheory |
|
1318 % |
|
1319 \endisadelimtheory |
|
1320 % |
|
1321 \isatagtheory |
|
1322 \isacommand{end}\isamarkupfalse% |
|
1323 % |
|
1324 \endisatagtheory |
|
1325 {\isafoldtheory}% |
|
1326 % |
|
1327 \isadelimtheory |
|
1328 % |
|
1329 \endisadelimtheory |
|
1330 \isanewline |
|
1331 \end{isabellebody}% |
|
1332 %%% Local Variables: |
|
1333 %%% mode: latex |
|
1334 %%% TeX-master: "root" |
|
1335 %%% End: |