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