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