20946
|
1 |
|
|
2 |
(* $Id$ *)
|
|
3 |
|
22317
|
4 |
(*<*)
|
20946
|
5 |
theory Classes
|
|
6 |
imports Main
|
|
7 |
begin
|
|
8 |
|
22317
|
9 |
ML {*
|
|
10 |
CodegenSerializer.code_width := 74;
|
|
11 |
*}
|
|
12 |
|
20946
|
13 |
syntax
|
|
14 |
"_alpha" :: "type" ("\<alpha>")
|
22479
|
15 |
"_alpha_ofsort" :: "sort \<Rightarrow> type" ("\<alpha>()\<Colon>_" [0] 1000)
|
20946
|
16 |
"_beta" :: "type" ("\<beta>")
|
22479
|
17 |
"_beta_ofsort" :: "sort \<Rightarrow> type" ("\<beta>()\<Colon>_" [0] 1000)
|
20946
|
18 |
"_gamma" :: "type" ("\<gamma>")
|
22479
|
19 |
"_gamma_ofsort" :: "sort \<Rightarrow> type" ("\<gamma>()\<Colon>_" [0] 1000)
|
20946
|
20 |
"_alpha_f" :: "type" ("\<alpha>\<^sub>f")
|
22479
|
21 |
"_alpha_f_ofsort" :: "sort \<Rightarrow> type" ("\<alpha>\<^sub>f()\<Colon>_" [0] 1000)
|
20946
|
22 |
"_beta_f" :: "type" ("\<beta>\<^sub>f")
|
22479
|
23 |
"_beta_f_ofsort" :: "sort \<Rightarrow> type" ("\<beta>\<^sub>f()\<Colon>_" [0] 1000)
|
20946
|
24 |
"_gamma_f" :: "type" ("\<gamma>\<^sub>f")
|
22479
|
25 |
"_gamma_ofsort_f" :: "sort \<Rightarrow> type" ("\<gamma>\<^sub>f()\<Colon>_" [0] 1000)
|
20946
|
26 |
|
|
27 |
parse_ast_translation {*
|
|
28 |
let
|
|
29 |
fun alpha_ast_tr [] = Syntax.Variable "'a"
|
|
30 |
| alpha_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
|
|
31 |
fun alpha_ofsort_ast_tr [ast] =
|
|
32 |
Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'a", ast]
|
|
33 |
| alpha_ofsort_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
|
|
34 |
fun beta_ast_tr [] = Syntax.Variable "'b"
|
|
35 |
| beta_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
|
|
36 |
fun beta_ofsort_ast_tr [ast] =
|
|
37 |
Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'b", ast]
|
|
38 |
| beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
|
|
39 |
fun gamma_ast_tr [] = Syntax.Variable "'c"
|
|
40 |
| gamma_ast_tr asts = raise Syntax.AST ("gamma_ast_tr", asts);
|
|
41 |
fun gamma_ofsort_ast_tr [ast] =
|
|
42 |
Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'c", ast]
|
|
43 |
| gamma_ofsort_ast_tr asts = raise Syntax.AST ("gamma_ast_tr", asts);
|
|
44 |
fun alpha_f_ast_tr [] = Syntax.Variable "'a_f"
|
|
45 |
| alpha_f_ast_tr asts = raise Syntax.AST ("alpha_f_ast_tr", asts);
|
|
46 |
fun alpha_f_ofsort_ast_tr [ast] =
|
|
47 |
Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'a_f", ast]
|
|
48 |
| alpha_f_ofsort_ast_tr asts = raise Syntax.AST ("alpha_f_ast_tr", asts);
|
|
49 |
fun beta_f_ast_tr [] = Syntax.Variable "'b_f"
|
|
50 |
| beta_f_ast_tr asts = raise Syntax.AST ("beta_f_ast_tr", asts);
|
|
51 |
fun beta_f_ofsort_ast_tr [ast] =
|
|
52 |
Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'b_f", ast]
|
|
53 |
| beta_f_ofsort_ast_tr asts = raise Syntax.AST ("beta_f_ast_tr", asts);
|
|
54 |
fun gamma_f_ast_tr [] = Syntax.Variable "'c_f"
|
|
55 |
| gamma_f_ast_tr asts = raise Syntax.AST ("gamma_f_ast_tr", asts);
|
|
56 |
fun gamma_f_ofsort_ast_tr [ast] =
|
|
57 |
Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'c_f", ast]
|
|
58 |
| gamma_f_ofsort_ast_tr asts = raise Syntax.AST ("gamma_f_ast_tr", asts);
|
|
59 |
in [
|
|
60 |
("_alpha", alpha_ast_tr), ("_alpha_ofsort", alpha_ofsort_ast_tr),
|
|
61 |
("_beta", beta_ast_tr), ("_beta_ofsort", beta_ofsort_ast_tr),
|
|
62 |
("_gamma", gamma_ast_tr), ("_gamma_ofsort", gamma_ofsort_ast_tr),
|
|
63 |
("_alpha_f", alpha_f_ast_tr), ("_alpha_f_ofsort", alpha_f_ofsort_ast_tr),
|
|
64 |
("_beta_f", beta_f_ast_tr), ("_beta_f_ofsort", beta_f_ofsort_ast_tr),
|
|
65 |
("_gamma_f", gamma_f_ast_tr), ("_gamma_f_ofsort", gamma_f_ofsort_ast_tr)
|
|
66 |
] end
|
|
67 |
*}
|
|
68 |
(*>*)
|
|
69 |
|
|
70 |
|
|
71 |
chapter {* Haskell-style classes with Isabelle/Isar *}
|
|
72 |
|
|
73 |
section {* Introduction *}
|
|
74 |
|
|
75 |
text {*
|
22317
|
76 |
Type classes were introduces by Wadler and Blott \cite{wadler89how}
|
|
77 |
into the Haskell language, to allow for a reasonable implementation
|
|
78 |
of overloading\footnote{throughout this tutorial, we are referring
|
|
79 |
to classical Haskell 1.0 type classes, not considering
|
|
80 |
later additions in expressiveness}.
|
|
81 |
As a canonical example, a polymorphic equality function
|
|
82 |
@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} which is overloaded on different
|
|
83 |
types for @{text "\<alpha>"}, which is achieves by splitting introduction
|
|
84 |
of the @{text eq} function from its overloaded definitions by means
|
|
85 |
of @{text class} and @{text instance} declarations:
|
|
86 |
|
|
87 |
\medskip\noindent\hspace*{2ex}@{text "class eq where"}\footnote{syntax here is a kind of isabellized Haskell} \\
|
|
88 |
\hspace*{4ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
|
20946
|
89 |
|
22317
|
90 |
\medskip\noindent\hspace*{2ex}@{text "instance nat \<Colon> eq where"} \\
|
|
91 |
\hspace*{4ex}@{text "eq 0 0 = True"} \\
|
|
92 |
\hspace*{4ex}@{text "eq 0 _ = False"} \\
|
|
93 |
\hspace*{4ex}@{text "eq _ 0 = False"} \\
|
|
94 |
\hspace*{4ex}@{text "eq (Suc n) (Suc m) = eq n m"}
|
|
95 |
|
|
96 |
\medskip\noindent\hspace*{2ex}@{text "instance (\<alpha>\<Colon>eq, \<beta>\<Colon>eq) pair \<Colon> eq where"} \\
|
|
97 |
\hspace*{4ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 && eq y1 y2"}
|
20946
|
98 |
|
22317
|
99 |
\medskip\noindent\hspace*{2ex}@{text "class ord extends eq where"} \\
|
|
100 |
\hspace*{4ex}@{text "less_eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
|
|
101 |
\hspace*{4ex}@{text "less \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
|
|
102 |
|
|
103 |
\medskip Type variables are annotated with (finitly many) classes;
|
|
104 |
these annotations are assertions that a particular polymorphic type
|
|
105 |
provides definitions for overloaded functions.
|
|
106 |
|
|
107 |
Indeed, type classes not only allow for simple overloading
|
|
108 |
but form a generic calculus, an instance of order-sorted
|
|
109 |
algebra \cite{Nipkow-Prehofer:1993,Nipkow:1993,Wenzel:1997}.
|
20946
|
110 |
|
22317
|
111 |
From a software enigineering point of view, type classes
|
|
112 |
correspond to interfaces in object-oriented languages like Java;
|
|
113 |
so, it is naturally desirable that type classes do not only
|
|
114 |
provide functions (class operations) but also state specifications
|
|
115 |
implementations must obey. For example, the @{text "class eq"}
|
|
116 |
above could be given the following specification:
|
|
117 |
|
|
118 |
\medskip\noindent\hspace*{2ex}@{text "class eq where"} \\
|
|
119 |
\hspace*{4ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
|
|
120 |
\hspace*{2ex}@{text "satisfying"} \\
|
|
121 |
\hspace*{4ex}@{text "refl: eq x x"} \\
|
|
122 |
\hspace*{4ex}@{text "sym: eq x y \<longleftrightarrow> eq x y"} \\
|
|
123 |
\hspace*{4ex}@{text "trans: eq x y \<and> eq y z \<longrightarrow> eq x z"}
|
|
124 |
|
|
125 |
\medskip From a theoretic point of view, type classes are leightweight
|
22347
|
126 |
modules; Haskell type classes may be emulated by
|
22317
|
127 |
SML functors \cite{classes_modules}.
|
|
128 |
Isabelle/Isar offers a discipline of type classes which brings
|
|
129 |
all those aspects together:
|
|
130 |
|
|
131 |
\begin{enumerate}
|
|
132 |
\item specifying abstract operations togehter with
|
|
133 |
corresponding specifications,
|
|
134 |
\item instantating those abstract operations by a particular
|
|
135 |
type
|
|
136 |
\item in connection with a ``less ad-hoc'' approach to overloading,
|
|
137 |
\item with a direct link to the Isabelle module system (aka locales).
|
|
138 |
\end{enumerate}
|
|
139 |
|
|
140 |
Isar type classes also directly support code generation
|
|
141 |
in as Haskell like fashion.
|
|
142 |
|
|
143 |
This tutorial demonstrates common elements of structured specifications
|
|
144 |
and abstract reasoning with type classes by the algebraic hierarchy of
|
20946
|
145 |
semigroups, monoids and groups. Our background theory is that of
|
22317
|
146 |
Isabelle/HOL \cite{Nipkow-et-al:2002:tutorial}, for which some
|
|
147 |
familiarity is assumed.
|
20946
|
148 |
|
22317
|
149 |
Here we merely present the look-and-feel for end users.
|
20946
|
150 |
Internally, those are mapped to more primitive Isabelle concepts.
|
|
151 |
See \cite{haftmann_wenzel2006classes} for more detail.
|
|
152 |
*}
|
|
153 |
|
22317
|
154 |
section {* A simple algebra example \label{sec:example} *}
|
20946
|
155 |
|
|
156 |
subsection {* Class definition *}
|
|
157 |
|
|
158 |
text {*
|
|
159 |
Depending on an arbitrary type @{text "\<alpha>"}, class @{text
|
|
160 |
"semigroup"} introduces a binary operation @{text "\<circ>"} that is
|
|
161 |
assumed to be associative:
|
|
162 |
*}
|
|
163 |
|
22473
|
164 |
class semigroup = type +
|
20946
|
165 |
fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" (infixl "\<^loc>\<otimes>" 70)
|
|
166 |
assumes assoc: "(x \<^loc>\<otimes> y) \<^loc>\<otimes> z = x \<^loc>\<otimes> (y \<^loc>\<otimes> z)"
|
|
167 |
|
|
168 |
text {*
|
|
169 |
\noindent This @{text "\<CLASS>"} specification consists of two
|
|
170 |
parts: the \qn{operational} part names the class operation (@{text
|
|
171 |
"\<FIXES>"}), the \qn{logical} part specifies properties on them
|
|
172 |
(@{text "\<ASSUMES>"}). The local @{text "\<FIXES>"} and @{text
|
|
173 |
"\<ASSUMES>"} are lifted to the theory toplevel, yielding the global
|
22479
|
174 |
operation @{term [source] "mult \<Colon> \<alpha>\<Colon>semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the
|
20946
|
175 |
global theorem @{text "semigroup.assoc:"}~@{prop [source] "\<And>x y
|
22479
|
176 |
z \<Colon> \<alpha>\<Colon>semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}.
|
20946
|
177 |
*}
|
|
178 |
|
|
179 |
|
|
180 |
subsection {* Class instantiation \label{sec:class_inst} *}
|
|
181 |
|
|
182 |
text {*
|
|
183 |
The concrete type @{text "int"} is made a @{text "semigroup"}
|
|
184 |
instance by providing a suitable definition for the class operation
|
|
185 |
@{text "mult"} and a proof for the specification of @{text "assoc"}.
|
|
186 |
*}
|
|
187 |
|
|
188 |
instance int :: semigroup
|
22479
|
189 |
mult_int_def: "\<And>i j \<Colon> int. i \<otimes> j \<equiv> i + j"
|
20946
|
190 |
proof
|
22317
|
191 |
fix i j k :: int have "(i + j) + k = i + (j + k)" by simp
|
|
192 |
then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)" unfolding mult_int_def .
|
20946
|
193 |
qed
|
|
194 |
|
|
195 |
text {*
|
|
196 |
\noindent From now on, the type-checker will consider @{text "int"}
|
|
197 |
as a @{text "semigroup"} automatically, i.e.\ any general results
|
|
198 |
are immediately available on concrete instances.
|
|
199 |
|
22317
|
200 |
Note that the first proof step is the @{text default} method,
|
|
201 |
which for instantiation proofs maps to the @{text intro_classes} method.
|
|
202 |
This boils down an instantiation judgement to the relevant primitive
|
|
203 |
proof goals and should conveniently always be the first method applied
|
|
204 |
in an instantiation proof.
|
|
205 |
|
20946
|
206 |
Another instance of @{text "semigroup"} are the natural numbers:
|
|
207 |
*}
|
|
208 |
|
|
209 |
instance nat :: semigroup
|
22317
|
210 |
mult_nat_def: "m \<otimes> n \<equiv> m + n"
|
20946
|
211 |
proof
|
|
212 |
fix m n q :: nat
|
22317
|
213 |
show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" unfolding mult_nat_def by simp
|
20946
|
214 |
qed
|
|
215 |
|
|
216 |
text {*
|
|
217 |
Also @{text "list"}s form a semigroup with @{const "op @"} as
|
|
218 |
operation:
|
|
219 |
*}
|
|
220 |
|
|
221 |
instance list :: (type) semigroup
|
22317
|
222 |
mult_list_def: "xs \<otimes> ys \<equiv> xs @ ys"
|
20946
|
223 |
proof
|
|
224 |
fix xs ys zs :: "\<alpha> list"
|
|
225 |
show "xs \<otimes> ys \<otimes> zs = xs \<otimes> (ys \<otimes> zs)"
|
|
226 |
proof -
|
22317
|
227 |
from mult_list_def have "\<And>xs ys\<Colon>\<alpha> list. xs \<otimes> ys \<equiv> xs @ ys" .
|
20946
|
228 |
thus ?thesis by simp
|
|
229 |
qed
|
|
230 |
qed
|
|
231 |
|
|
232 |
|
|
233 |
subsection {* Subclasses *}
|
|
234 |
|
|
235 |
text {*
|
22317
|
236 |
We define a subclass @{text "monoidl"} (a semigroup with a left-hand neutral)
|
20946
|
237 |
by extending @{text "semigroup"}
|
|
238 |
with one additional operation @{text "neutral"} together
|
|
239 |
with its property:
|
|
240 |
*}
|
|
241 |
|
|
242 |
class monoidl = semigroup +
|
|
243 |
fixes neutral :: "\<alpha>" ("\<^loc>\<one>")
|
|
244 |
assumes neutl: "\<^loc>\<one> \<^loc>\<otimes> x = x"
|
|
245 |
|
|
246 |
text {*
|
|
247 |
\noindent Again, we make some instances, by
|
|
248 |
providing suitable operation definitions and proofs for the
|
|
249 |
additional specifications.
|
|
250 |
*}
|
|
251 |
|
|
252 |
instance nat :: monoidl
|
22317
|
253 |
neutral_nat_def: "\<one> \<equiv> 0"
|
20946
|
254 |
proof
|
|
255 |
fix n :: nat
|
|
256 |
show "\<one> \<otimes> n = n" unfolding neutral_nat_def mult_nat_def by simp
|
|
257 |
qed
|
|
258 |
|
|
259 |
instance int :: monoidl
|
22317
|
260 |
neutral_int_def: "\<one> \<equiv> 0"
|
20946
|
261 |
proof
|
|
262 |
fix k :: int
|
|
263 |
show "\<one> \<otimes> k = k" unfolding neutral_int_def mult_int_def by simp
|
|
264 |
qed
|
|
265 |
|
|
266 |
instance list :: (type) monoidl
|
22317
|
267 |
neutral_list_def: "\<one> \<equiv> []"
|
20946
|
268 |
proof
|
|
269 |
fix xs :: "\<alpha> list"
|
|
270 |
show "\<one> \<otimes> xs = xs"
|
|
271 |
proof -
|
22347
|
272 |
from mult_list_def have "\<And>xs ys\<Colon>\<alpha> list. xs \<otimes> ys \<equiv> xs @ ys" .
|
20946
|
273 |
moreover from mult_list_def neutral_list_def have "\<one> \<equiv> []\<Colon>\<alpha> list" by simp
|
|
274 |
ultimately show ?thesis by simp
|
|
275 |
qed
|
|
276 |
qed
|
|
277 |
|
|
278 |
text {*
|
22317
|
279 |
\noindent Fully-fledged monoids are modelled by another subclass
|
|
280 |
which does not add new operations but tightens the specification:
|
20946
|
281 |
*}
|
|
282 |
|
|
283 |
class monoid = monoidl +
|
|
284 |
assumes neutr: "x \<^loc>\<otimes> \<^loc>\<one> = x"
|
|
285 |
|
22317
|
286 |
text {*
|
|
287 |
\noindent Instantiations may also be given simultaneously for different
|
|
288 |
type constructors:
|
|
289 |
*}
|
|
290 |
|
|
291 |
instance nat :: monoid and int :: monoid and list :: (type) monoid
|
20946
|
292 |
proof
|
|
293 |
fix n :: nat
|
|
294 |
show "n \<otimes> \<one> = n" unfolding neutral_nat_def mult_nat_def by simp
|
22317
|
295 |
next
|
20946
|
296 |
fix k :: int
|
|
297 |
show "k \<otimes> \<one> = k" unfolding neutral_int_def mult_int_def by simp
|
22317
|
298 |
next
|
20946
|
299 |
fix xs :: "\<alpha> list"
|
|
300 |
show "xs \<otimes> \<one> = xs"
|
|
301 |
proof -
|
|
302 |
from mult_list_def have "\<And>xs ys\<Colon>\<alpha> list. xs \<otimes> ys \<equiv> xs @ ys" .
|
22347
|
303 |
moreover from mult_list_def neutral_list_def have "\<one> \<equiv> []\<Colon>\<alpha> list" by simp
|
20946
|
304 |
ultimately show ?thesis by simp
|
|
305 |
qed
|
22317
|
306 |
qed
|
|
307 |
|
|
308 |
text {*
|
|
309 |
\noindent To finish our small algebra example, we add a @{text "group"} class
|
|
310 |
with a corresponding instance:
|
|
311 |
*}
|
20946
|
312 |
|
|
313 |
class group = monoidl +
|
|
314 |
fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>" ("(_\<^loc>\<div>)" [1000] 999)
|
|
315 |
assumes invl: "x\<^loc>\<div> \<^loc>\<otimes> x = \<^loc>\<one>"
|
|
316 |
|
|
317 |
instance int :: group
|
22317
|
318 |
inverse_int_def: "i\<div> \<equiv> - i"
|
20946
|
319 |
proof
|
|
320 |
fix i :: int
|
|
321 |
have "-i + i = 0" by simp
|
|
322 |
then show "i\<div> \<otimes> i = \<one>" unfolding mult_int_def and neutral_int_def and inverse_int_def .
|
|
323 |
qed
|
|
324 |
|
22317
|
325 |
section {* Type classes as locales *}
|
|
326 |
|
|
327 |
subsection {* A look behind the scene *}
|
|
328 |
|
22347
|
329 |
text {*
|
|
330 |
The example above gives an impression how Isar type classes work
|
|
331 |
in practice. As stated in the introduction, classes also provide
|
|
332 |
a link to Isar's locale system. Indeed, the logical core of a class
|
|
333 |
is nothing else than a locale:
|
|
334 |
*}
|
|
335 |
|
22473
|
336 |
class idem = type +
|
22347
|
337 |
fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
|
|
338 |
assumes idem: "f (f x) = f x"
|
22317
|
339 |
|
|
340 |
text {*
|
22347
|
341 |
\noindent essentially introduces the locale
|
|
342 |
*}
|
22317
|
343 |
|
22347
|
344 |
(*<*) setup {* Sign.add_path "foo" *} (*>*)
|
|
345 |
|
|
346 |
locale idem =
|
|
347 |
fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
|
|
348 |
assumes idem: "f (f x) = f x"
|
|
349 |
|
|
350 |
text {* \noindent together with corresponding constant(s) and axclass *}
|
|
351 |
|
|
352 |
consts f :: "\<alpha> \<Rightarrow> \<alpha>"
|
|
353 |
|
|
354 |
axclass idem < type
|
|
355 |
idem: "f (f x) = f x"
|
|
356 |
|
|
357 |
text {* This axclass is coupled to the locale by means of an interpretation: *}
|
|
358 |
|
|
359 |
interpretation idem_class:
|
|
360 |
idem ["f \<Colon> ('a\<Colon>idem) \<Rightarrow> \<alpha>"]
|
|
361 |
by unfold_locales (rule idem)
|
|
362 |
|
|
363 |
(*<*) setup {* Sign.parent_path *} (*>*)
|
|
364 |
|
|
365 |
text {*
|
|
366 |
This give you at hand the full power of the Isabelle module system;
|
|
367 |
conclusions in locale @{text idem} are implicitly propagated
|
22479
|
368 |
to class @{text idem}.
|
22317
|
369 |
*}
|
20946
|
370 |
|
|
371 |
subsection {* Abstract reasoning *}
|
|
372 |
|
|
373 |
text {*
|
22347
|
374 |
Isabelle locales enable reasoning at a general level, while results
|
20946
|
375 |
are implicitly transferred to all instances. For example, we can
|
|
376 |
now establish the @{text "left_cancel"} lemma for groups, which
|
|
377 |
states that the function @{text "(x \<circ>)"} is injective:
|
|
378 |
*}
|
|
379 |
|
|
380 |
lemma (in group) left_cancel: "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z \<longleftrightarrow> y = z"
|
|
381 |
proof
|
|
382 |
assume "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z"
|
22347
|
383 |
then have "x\<^loc>\<div> \<^loc>\<otimes> (x \<^loc>\<otimes> y) = x\<^loc>\<div> \<^loc>\<otimes> (x \<^loc>\<otimes> z)" by simp
|
|
384 |
then have "(x\<^loc>\<div> \<^loc>\<otimes> x) \<^loc>\<otimes> y = (x\<^loc>\<div> \<^loc>\<otimes> x) \<^loc>\<otimes> z" using assoc by simp
|
|
385 |
then show "y = z" using neutl and invl by simp
|
20946
|
386 |
next
|
|
387 |
assume "y = z"
|
22347
|
388 |
then show "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z" by simp
|
20946
|
389 |
qed
|
|
390 |
|
|
391 |
text {*
|
|
392 |
\noindent Here the \qt{@{text "\<IN> group"}} target specification
|
|
393 |
indicates that the result is recorded within that context for later
|
|
394 |
use. This local theorem is also lifted to the global one @{text
|
22479
|
395 |
"group.left_cancel:"} @{prop [source] "\<And>x y z \<Colon> \<alpha>\<Colon>group. x \<otimes> y = x \<otimes>
|
20946
|
396 |
z \<longleftrightarrow> y = z"}. Since type @{text "int"} has been made an instance of
|
|
397 |
@{text "group"} before, we may refer to that fact as well: @{prop
|
22479
|
398 |
[source] "\<And>x y z \<Colon> int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}.
|
20946
|
399 |
*}
|
|
400 |
|
|
401 |
|
|
402 |
(*subsection {* Derived definitions *}
|
|
403 |
|
|
404 |
text {*
|
|
405 |
*}*)
|
|
406 |
|
22347
|
407 |
(* subsection {* Additional subclass relations *}
|
|
408 |
|
|
409 |
text {*
|
|
410 |
Any @{text "group"} is also a @{text "monoid"}; this
|
|
411 |
can be made explicit by claiming an additional subclass relation,
|
|
412 |
together with a proof of the logical difference:
|
|
413 |
*}
|
|
414 |
|
|
415 |
instance group < monoid
|
|
416 |
proof -
|
|
417 |
fix x
|
|
418 |
from invl have "x\<^loc>\<div> \<^loc>\<otimes> x = \<^loc>\<one>" by simp
|
|
419 |
with assoc [symmetric] neutl invl have "x\<^loc>\<div> \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<one>) = x\<^loc>\<div> \<^loc>\<otimes> x" by simp
|
|
420 |
with left_cancel show "x \<^loc>\<otimes> \<^loc>\<one> = x" by simp
|
|
421 |
qed *)
|
|
422 |
|
22317
|
423 |
section {* Further issues *}
|
20946
|
424 |
|
22317
|
425 |
subsection {* Code generation *}
|
|
426 |
|
|
427 |
text {*
|
|
428 |
Turning back to the first motivation for type classes,
|
|
429 |
namely overloading, it is obvious that overloading
|
|
430 |
stemming from @{text "\<CLASS>"} and @{text "\<INSTANCE>"}
|
|
431 |
statements naturally maps to Haskell type classes.
|
|
432 |
The code generator framework \cite{isabelle-codegen}
|
|
433 |
takes this into account. Concerning target languages
|
|
434 |
lacking type classes (e.g.~SML), type classes
|
|
435 |
are implemented by explicit dictionary construction.
|
|
436 |
As example, the natural power function on groups:
|
|
437 |
*}
|
|
438 |
|
|
439 |
fun
|
22347
|
440 |
pow_nat :: "nat \<Rightarrow> \<alpha>\<Colon>monoidl \<Rightarrow> \<alpha>\<Colon>monoidl" where
|
22317
|
441 |
"pow_nat 0 x = \<one>"
|
22479
|
442 |
| "pow_nat (Suc n) x = x \<otimes> pow_nat n x"
|
22317
|
443 |
|
|
444 |
definition
|
22347
|
445 |
pow_int :: "int \<Rightarrow> \<alpha>\<Colon>group \<Rightarrow> \<alpha>\<Colon>group" where
|
22317
|
446 |
"pow_int k x = (if k >= 0
|
|
447 |
then pow_nat (nat k) x
|
|
448 |
else (pow_nat (nat (- k)) x)\<div>)"
|
|
449 |
|
|
450 |
definition
|
|
451 |
example :: int where
|
|
452 |
"example = pow_int 10 (-2)"
|
|
453 |
|
|
454 |
text {*
|
|
455 |
\noindent This maps to Haskell as:
|
|
456 |
*}
|
|
457 |
|
|
458 |
code_gen example (Haskell "code_examples/")
|
|
459 |
(* NOTE: you may use Haskell only once in this document, otherwise
|
|
460 |
you have to work in distinct subdirectories *)
|
|
461 |
|
|
462 |
text {*
|
|
463 |
\lsthaskell{Thy/code_examples/Classes.hs}
|
|
464 |
|
|
465 |
\noindent (we have left out all other modules).
|
|
466 |
|
|
467 |
\noindent The whole code in SML with explicit dictionary passing:
|
|
468 |
*}
|
|
469 |
|
|
470 |
code_gen example (*<*)(SML #)(*>*)(SML "code_examples/classes.ML")
|
|
471 |
|
|
472 |
text {*
|
|
473 |
\lstsml{Thy/code_examples/classes.ML}
|
|
474 |
*}
|
|
475 |
|
|
476 |
|
|
477 |
(* subsection {* Different syntax for same specifications *}
|
20946
|
478 |
|
|
479 |
text {*
|
|
480 |
|
22479
|
481 |
subsection {* Syntactic classes *}
|
22317
|
482 |
|
20946
|
483 |
*} *)
|
|
484 |
|
|
485 |
end
|