20946
|
1 |
|
|
2 |
(* $Id$ *)
|
|
3 |
|
|
4 |
theory Classes
|
|
5 |
imports Main
|
|
6 |
begin
|
|
7 |
|
|
8 |
(*<*)
|
|
9 |
syntax
|
|
10 |
"_alpha" :: "type" ("\<alpha>")
|
|
11 |
"_alpha_ofsort" :: "sort \<Rightarrow> type" ("\<alpha>()::_" [0] 1000)
|
|
12 |
"_beta" :: "type" ("\<beta>")
|
|
13 |
"_beta_ofsort" :: "sort \<Rightarrow> type" ("\<beta>()::_" [0] 1000)
|
|
14 |
"_gamma" :: "type" ("\<gamma>")
|
|
15 |
"_gamma_ofsort" :: "sort \<Rightarrow> type" ("\<gamma>()::_" [0] 1000)
|
|
16 |
"_alpha_f" :: "type" ("\<alpha>\<^sub>f")
|
|
17 |
"_alpha_f_ofsort" :: "sort \<Rightarrow> type" ("\<alpha>\<^sub>f()::_" [0] 1000)
|
|
18 |
"_beta_f" :: "type" ("\<beta>\<^sub>f")
|
|
19 |
"_beta_f_ofsort" :: "sort \<Rightarrow> type" ("\<beta>\<^sub>f()::_" [0] 1000)
|
|
20 |
"_gamma_f" :: "type" ("\<gamma>\<^sub>f")
|
|
21 |
"_gamma_ofsort_f" :: "sort \<Rightarrow> type" ("\<gamma>\<^sub>f()::_" [0] 1000)
|
|
22 |
|
|
23 |
parse_ast_translation {*
|
|
24 |
let
|
|
25 |
fun alpha_ast_tr [] = Syntax.Variable "'a"
|
|
26 |
| alpha_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
|
|
27 |
fun alpha_ofsort_ast_tr [ast] =
|
|
28 |
Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'a", ast]
|
|
29 |
| alpha_ofsort_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
|
|
30 |
fun beta_ast_tr [] = Syntax.Variable "'b"
|
|
31 |
| beta_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
|
|
32 |
fun beta_ofsort_ast_tr [ast] =
|
|
33 |
Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'b", ast]
|
|
34 |
| beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
|
|
35 |
fun gamma_ast_tr [] = Syntax.Variable "'c"
|
|
36 |
| gamma_ast_tr asts = raise Syntax.AST ("gamma_ast_tr", asts);
|
|
37 |
fun gamma_ofsort_ast_tr [ast] =
|
|
38 |
Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'c", ast]
|
|
39 |
| gamma_ofsort_ast_tr asts = raise Syntax.AST ("gamma_ast_tr", asts);
|
|
40 |
fun alpha_f_ast_tr [] = Syntax.Variable "'a_f"
|
|
41 |
| alpha_f_ast_tr asts = raise Syntax.AST ("alpha_f_ast_tr", asts);
|
|
42 |
fun alpha_f_ofsort_ast_tr [ast] =
|
|
43 |
Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'a_f", ast]
|
|
44 |
| alpha_f_ofsort_ast_tr asts = raise Syntax.AST ("alpha_f_ast_tr", asts);
|
|
45 |
fun beta_f_ast_tr [] = Syntax.Variable "'b_f"
|
|
46 |
| beta_f_ast_tr asts = raise Syntax.AST ("beta_f_ast_tr", asts);
|
|
47 |
fun beta_f_ofsort_ast_tr [ast] =
|
|
48 |
Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'b_f", ast]
|
|
49 |
| beta_f_ofsort_ast_tr asts = raise Syntax.AST ("beta_f_ast_tr", asts);
|
|
50 |
fun gamma_f_ast_tr [] = Syntax.Variable "'c_f"
|
|
51 |
| gamma_f_ast_tr asts = raise Syntax.AST ("gamma_f_ast_tr", asts);
|
|
52 |
fun gamma_f_ofsort_ast_tr [ast] =
|
|
53 |
Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'c_f", ast]
|
|
54 |
| gamma_f_ofsort_ast_tr asts = raise Syntax.AST ("gamma_f_ast_tr", asts);
|
|
55 |
in [
|
|
56 |
("_alpha", alpha_ast_tr), ("_alpha_ofsort", alpha_ofsort_ast_tr),
|
|
57 |
("_beta", beta_ast_tr), ("_beta_ofsort", beta_ofsort_ast_tr),
|
|
58 |
("_gamma", gamma_ast_tr), ("_gamma_ofsort", gamma_ofsort_ast_tr),
|
|
59 |
("_alpha_f", alpha_f_ast_tr), ("_alpha_f_ofsort", alpha_f_ofsort_ast_tr),
|
|
60 |
("_beta_f", beta_f_ast_tr), ("_beta_f_ofsort", beta_f_ofsort_ast_tr),
|
|
61 |
("_gamma_f", gamma_f_ast_tr), ("_gamma_f_ofsort", gamma_f_ofsort_ast_tr)
|
|
62 |
] end
|
|
63 |
*}
|
|
64 |
(*>*)
|
|
65 |
|
|
66 |
|
|
67 |
chapter {* Haskell-style classes with Isabelle/Isar *}
|
|
68 |
|
|
69 |
section {* Introduction *}
|
|
70 |
|
|
71 |
text {*
|
|
72 |
The well-known concept of type classes
|
|
73 |
\cite{wadler89how,peterson93implementing,hall96type,Nipkow-Prehofer:1993,Nipkow:1993,Wenzel:1997}
|
|
74 |
offers a useful structuring mechanism for programs and proofs, which
|
|
75 |
is more light-weight than a fully featured module mechanism. Type
|
|
76 |
classes are able to qualify types by associating operations and
|
|
77 |
logical properties. For example, class @{text "eq"} could provide
|
|
78 |
an equivalence relation @{text "="} on type @{text "\<alpha>"}, and class
|
|
79 |
@{text "ord"} could extend @{text "eq"} by providing a strict order
|
|
80 |
@{text "<"} etc.
|
|
81 |
|
|
82 |
Isabelle/Isar offers Haskell-style type classes, combining operational
|
|
83 |
and logical specifications.
|
|
84 |
*}
|
|
85 |
|
|
86 |
section {* A simple algebra example \label{sec:example} *}
|
|
87 |
|
|
88 |
text {*
|
|
89 |
We demonstrate common elements of structured specifications and
|
|
90 |
abstract reasoning with type classes by the algebraic hierarchy of
|
|
91 |
semigroups, monoids and groups. Our background theory is that of
|
|
92 |
Isabelle/HOL \cite{Nipkow-et-al:2002:tutorial}, which uses fairly
|
|
93 |
standard notation from mathematics and functional programming. We
|
|
94 |
also refer to basic vernacular commands for definitions and
|
|
95 |
statements, e.g.\ @{text "\<DEFINITION>"} and @{text "\<LEMMA>"};
|
|
96 |
proofs will be recorded using structured elements of Isabelle/Isar
|
|
97 |
\cite{Wenzel-PhD,Nipkow:2002}, notably @{text "\<PROOF>"}/@{text
|
|
98 |
"\<QED>"} and @{text "\<FIX>"}/@{text "\<ASSUME>"}/@{text
|
|
99 |
"\<SHOW>"}.
|
|
100 |
|
|
101 |
Our main concern are the new @{text "\<CLASS>"}
|
|
102 |
and @{text "\<INSTANCE>"} elements used below.
|
|
103 |
Here we merely present the
|
|
104 |
look-and-feel for end users, which is quite similar to Haskell's
|
|
105 |
\texttt{class} and \texttt{instance} \cite{hall96type}, but
|
|
106 |
augmented by logical specifications and proofs;
|
|
107 |
Internally, those are mapped to more primitive Isabelle concepts.
|
|
108 |
See \cite{haftmann_wenzel2006classes} for more detail.
|
|
109 |
*}
|
|
110 |
|
|
111 |
|
|
112 |
subsection {* Class definition *}
|
|
113 |
|
|
114 |
text {*
|
|
115 |
Depending on an arbitrary type @{text "\<alpha>"}, class @{text
|
|
116 |
"semigroup"} introduces a binary operation @{text "\<circ>"} that is
|
|
117 |
assumed to be associative:
|
|
118 |
*}
|
|
119 |
|
|
120 |
class semigroup =
|
|
121 |
fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" (infixl "\<^loc>\<otimes>" 70)
|
|
122 |
assumes assoc: "(x \<^loc>\<otimes> y) \<^loc>\<otimes> z = x \<^loc>\<otimes> (y \<^loc>\<otimes> z)"
|
|
123 |
|
|
124 |
text {*
|
|
125 |
\noindent This @{text "\<CLASS>"} specification consists of two
|
|
126 |
parts: the \qn{operational} part names the class operation (@{text
|
|
127 |
"\<FIXES>"}), the \qn{logical} part specifies properties on them
|
|
128 |
(@{text "\<ASSUMES>"}). The local @{text "\<FIXES>"} and @{text
|
|
129 |
"\<ASSUMES>"} are lifted to the theory toplevel, yielding the global
|
|
130 |
operation @{term [source] "mult :: \<alpha>::semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the
|
|
131 |
global theorem @{text "semigroup.assoc:"}~@{prop [source] "\<And>x y
|
|
132 |
z::\<alpha>::semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}.
|
|
133 |
*}
|
|
134 |
|
|
135 |
|
|
136 |
subsection {* Class instantiation \label{sec:class_inst} *}
|
|
137 |
|
|
138 |
text {*
|
|
139 |
The concrete type @{text "int"} is made a @{text "semigroup"}
|
|
140 |
instance by providing a suitable definition for the class operation
|
|
141 |
@{text "mult"} and a proof for the specification of @{text "assoc"}.
|
|
142 |
*}
|
|
143 |
|
|
144 |
instance int :: semigroup
|
|
145 |
mult_int_def: "\<And>i j :: int. i \<otimes> j \<equiv> i + j"
|
|
146 |
proof
|
|
147 |
fix i j k :: int have "(i + j) + k = i + (j + k)" by simp
|
|
148 |
then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)" unfolding mult_int_def .
|
|
149 |
qed
|
|
150 |
|
|
151 |
text {*
|
|
152 |
\noindent From now on, the type-checker will consider @{text "int"}
|
|
153 |
as a @{text "semigroup"} automatically, i.e.\ any general results
|
|
154 |
are immediately available on concrete instances.
|
|
155 |
|
|
156 |
Another instance of @{text "semigroup"} are the natural numbers:
|
|
157 |
*}
|
|
158 |
|
|
159 |
instance nat :: semigroup
|
|
160 |
"m \<otimes> n \<equiv> m + n"
|
|
161 |
proof
|
|
162 |
fix m n q :: nat
|
|
163 |
show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" unfolding semigroup_nat_def by simp
|
|
164 |
qed
|
|
165 |
|
|
166 |
text {*
|
|
167 |
Also @{text "list"}s form a semigroup with @{const "op @"} as
|
|
168 |
operation:
|
|
169 |
*}
|
|
170 |
|
|
171 |
instance list :: (type) semigroup
|
|
172 |
"xs \<otimes> ys \<equiv> xs @ ys"
|
|
173 |
proof
|
|
174 |
fix xs ys zs :: "\<alpha> list"
|
|
175 |
show "xs \<otimes> ys \<otimes> zs = xs \<otimes> (ys \<otimes> zs)"
|
|
176 |
proof -
|
|
177 |
from semigroup_list_def have "\<And>xs ys\<Colon>\<alpha> list. xs \<otimes> ys \<equiv> xs @ ys" .
|
|
178 |
thus ?thesis by simp
|
|
179 |
qed
|
|
180 |
qed
|
|
181 |
|
|
182 |
|
|
183 |
subsection {* Subclasses *}
|
|
184 |
|
|
185 |
text {*
|
|
186 |
We define a subclass @{text "monoidl"} (a semigroup with an left-hand neutral)
|
|
187 |
by extending @{text "semigroup"}
|
|
188 |
with one additional operation @{text "neutral"} together
|
|
189 |
with its property:
|
|
190 |
*}
|
|
191 |
|
|
192 |
class monoidl = semigroup +
|
|
193 |
fixes neutral :: "\<alpha>" ("\<^loc>\<one>")
|
|
194 |
assumes neutl: "\<^loc>\<one> \<^loc>\<otimes> x = x"
|
|
195 |
|
|
196 |
text {*
|
|
197 |
\noindent Again, we make some instances, by
|
|
198 |
providing suitable operation definitions and proofs for the
|
|
199 |
additional specifications.
|
|
200 |
*}
|
|
201 |
|
|
202 |
instance nat :: monoidl
|
|
203 |
"\<one> \<equiv> 0"
|
|
204 |
proof
|
|
205 |
fix n :: nat
|
|
206 |
show "\<one> \<otimes> n = n" unfolding neutral_nat_def mult_nat_def by simp
|
|
207 |
qed
|
|
208 |
|
|
209 |
instance int :: monoidl
|
|
210 |
"\<one> \<equiv> 0"
|
|
211 |
proof
|
|
212 |
fix k :: int
|
|
213 |
show "\<one> \<otimes> k = k" unfolding neutral_int_def mult_int_def by simp
|
|
214 |
qed
|
|
215 |
|
|
216 |
instance list :: (type) monoidl
|
|
217 |
"\<one> \<equiv> []"
|
|
218 |
proof
|
|
219 |
fix xs :: "\<alpha> list"
|
|
220 |
show "\<one> \<otimes> xs = xs"
|
|
221 |
proof -
|
|
222 |
from mult_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" .
|
|
223 |
moreover from mult_list_def neutral_list_def have "\<one> \<equiv> []\<Colon>\<alpha> list" by simp
|
|
224 |
ultimately show ?thesis by simp
|
|
225 |
qed
|
|
226 |
qed
|
|
227 |
|
|
228 |
text {*
|
|
229 |
To finish our small algebra example, we add @{text "monoid"}
|
|
230 |
and @{text "group"} classes with corresponding instances
|
|
231 |
*}
|
|
232 |
|
|
233 |
class monoid = monoidl +
|
|
234 |
assumes neutr: "x \<^loc>\<otimes> \<^loc>\<one> = x"
|
|
235 |
|
|
236 |
instance nat :: monoid
|
|
237 |
proof
|
|
238 |
fix n :: nat
|
|
239 |
show "n \<otimes> \<one> = n" unfolding neutral_nat_def mult_nat_def by simp
|
|
240 |
qed
|
|
241 |
|
|
242 |
instance int :: monoid
|
|
243 |
proof
|
|
244 |
fix k :: int
|
|
245 |
show "k \<otimes> \<one> = k" unfolding neutral_int_def mult_int_def by simp
|
|
246 |
qed
|
|
247 |
|
|
248 |
instance list :: (type) monoid
|
|
249 |
proof
|
|
250 |
fix xs :: "\<alpha> list"
|
|
251 |
show "xs \<otimes> \<one> = xs"
|
|
252 |
proof -
|
|
253 |
from mult_list_def have "\<And>xs ys\<Colon>\<alpha> list. xs \<otimes> ys \<equiv> xs @ ys" .
|
|
254 |
moreover from mult_list_def neutral_list_def have "\<one> \<equiv> []\<Colon>'a list" by simp
|
|
255 |
ultimately show ?thesis by simp
|
|
256 |
qed
|
|
257 |
qed
|
|
258 |
|
|
259 |
class group = monoidl +
|
|
260 |
fixes inverse :: "\<alpha> \<Rightarrow> \<alpha>" ("(_\<^loc>\<div>)" [1000] 999)
|
|
261 |
assumes invl: "x\<^loc>\<div> \<^loc>\<otimes> x = \<^loc>\<one>"
|
|
262 |
|
|
263 |
instance int :: group
|
|
264 |
"i\<div> \<equiv> - i"
|
|
265 |
proof
|
|
266 |
fix i :: int
|
|
267 |
have "-i + i = 0" by simp
|
|
268 |
then show "i\<div> \<otimes> i = \<one>" unfolding mult_int_def and neutral_int_def and inverse_int_def .
|
|
269 |
qed
|
|
270 |
|
|
271 |
|
|
272 |
subsection {* Abstract reasoning *}
|
|
273 |
|
|
274 |
text {*
|
|
275 |
Abstract theories enable reasoning at a general level, while results
|
|
276 |
are implicitly transferred to all instances. For example, we can
|
|
277 |
now establish the @{text "left_cancel"} lemma for groups, which
|
|
278 |
states that the function @{text "(x \<circ>)"} is injective:
|
|
279 |
*}
|
|
280 |
|
|
281 |
lemma (in group) left_cancel: "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z \<longleftrightarrow> y = z"
|
|
282 |
proof
|
|
283 |
assume "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z"
|
|
284 |
then have "x\<^loc>\<div> \<^loc>\<otimes> (x \<^loc>\<otimes> y) = x\<^loc>\<div> \<^loc>\<otimes> (x \<^loc>\<otimes> z)" by simp
|
|
285 |
then have "(x\<^loc>\<div> \<^loc>\<otimes> x) \<^loc>\<otimes> y = (x\<^loc>\<div> \<^loc>\<otimes> x) \<^loc>\<otimes> z" using assoc by simp
|
|
286 |
then show "y = z" using neutl and invl by simp
|
|
287 |
next
|
|
288 |
assume "y = z"
|
|
289 |
then show "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z" by simp
|
|
290 |
qed
|
|
291 |
|
|
292 |
text {*
|
|
293 |
\noindent Here the \qt{@{text "\<IN> group"}} target specification
|
|
294 |
indicates that the result is recorded within that context for later
|
|
295 |
use. This local theorem is also lifted to the global one @{text
|
|
296 |
"group.left_cancel:"} @{prop [source] "\<And>x y z::\<alpha>::group. x \<otimes> y = x \<otimes>
|
|
297 |
z \<longleftrightarrow> y = z"}. Since type @{text "int"} has been made an instance of
|
|
298 |
@{text "group"} before, we may refer to that fact as well: @{prop
|
|
299 |
[source] "\<And>x y z::int. x \<otimes> y = x \<otimes> z \<longleftrightarrow> y = z"}.
|
|
300 |
*}
|
|
301 |
|
|
302 |
|
|
303 |
(*subsection {* Derived definitions *}
|
|
304 |
|
|
305 |
text {*
|
|
306 |
*}*)
|
|
307 |
|
|
308 |
|
|
309 |
subsection {* Additional subclass relations *}
|
|
310 |
|
|
311 |
text {*
|
|
312 |
Any @{text "group"} is also a @{text "monoid"}; this
|
|
313 |
can be made explicit by claiming an additional subclass relation,
|
|
314 |
together with a proof of the logical difference:
|
|
315 |
*}
|
|
316 |
|
|
317 |
instance group < monoid
|
|
318 |
proof -
|
|
319 |
fix x
|
|
320 |
from invl have "x\<^loc>\<div> \<^loc>\<otimes> x = \<^loc>\<one>" by simp
|
|
321 |
with assoc [symmetric] neutl invl have "x\<^loc>\<div> \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<one>) = x\<^loc>\<div> \<^loc>\<otimes> x" by simp
|
|
322 |
with left_cancel show "x \<^loc>\<otimes> \<^loc>\<one> = x" by simp
|
|
323 |
qed
|
|
324 |
|
|
325 |
|
|
326 |
(* subsection {* Same logical content -- different syntax *}
|
|
327 |
|
|
328 |
text {*
|
|
329 |
|
|
330 |
*} *)
|
|
331 |
|
|
332 |
|
|
333 |
section {* Code generation *}
|
|
334 |
|
|
335 |
text {*
|
|
336 |
Code generation takes account of type classes,
|
|
337 |
resulting either in Haskell type classes or SML dictionaries.
|
|
338 |
As example, we define the natural power function on groups:
|
|
339 |
*}
|
|
340 |
|
|
341 |
function
|
|
342 |
pow_nat :: "nat \<Rightarrow> 'a\<Colon>monoidl \<Rightarrow> 'a\<Colon>monoidl" where
|
|
343 |
"pow_nat 0 x = \<one>"
|
|
344 |
"pow_nat (Suc n) x = x \<otimes> pow_nat n x"
|
|
345 |
by pat_completeness auto
|
|
346 |
termination pow_nat by (auto_term "measure fst")
|
|
347 |
declare pow_nat.simps [code func]
|
|
348 |
|
|
349 |
definition
|
|
350 |
pow_int :: "int \<Rightarrow> 'a\<Colon>group \<Rightarrow> 'a\<Colon>group"
|
|
351 |
"pow_int k x = (if k >= 0
|
|
352 |
then pow_nat (nat k) x
|
|
353 |
else (pow_nat (nat (- k)) x)\<div>)"
|
|
354 |
|
|
355 |
definition
|
|
356 |
example :: int
|
|
357 |
"example = pow_int 10 (-2)"
|
|
358 |
|
|
359 |
text {*
|
|
360 |
\noindent Now we generate and compile code for SML:
|
|
361 |
*}
|
|
362 |
|
|
363 |
code_gen example (SML -)
|
|
364 |
|
|
365 |
text {*
|
|
366 |
\noindent The result is as expected:
|
|
367 |
*}
|
|
368 |
|
|
369 |
ML {*
|
|
370 |
if ROOT.Classes.example = ~20 then () else error "Wrong result"
|
|
371 |
*}
|
|
372 |
|
|
373 |
end
|