author | haftmann |
Fri, 20 Oct 2006 17:07:41 +0200 | |
changeset 21080 | 7d73aa966207 |
parent 20597 | 65fe827aa595 |
child 21125 | 9b7d35ca1eef |
permissions | -rw-r--r-- |
20436 | 1 |
(* ID: $Id$ |
2 |
Author: Florian Haftmann, TU Muenchen |
|
3 |
*) |
|
4 |
||
5 |
header {* Collection classes as examples for code generation *} |
|
6 |
||
7 |
theory CodeCollections |
|
20597 | 8 |
imports Main |
20436 | 9 |
begin |
10 |
||
11 |
section {* Collection classes as examples for code generation *} |
|
12 |
||
13 |
class ordered = eq + |
|
14 |
constrains eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
15 |
fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^loc><<=" 65) |
|
16 |
fixes lt :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^loc><<" 65) |
|
17 |
assumes order_refl: "x \<^loc><<= x" |
|
18 |
assumes order_trans: "x \<^loc><<= y ==> y \<^loc><<= z ==> x \<^loc><<= z" |
|
19 |
assumes order_antisym: "x \<^loc><<= y ==> y \<^loc><<= x ==> x = y" |
|
20 |
||
21 |
declare order_refl [simp, intro] |
|
22 |
||
23 |
defs |
|
24 |
lt_def: "x << y == (x <<= y \<and> x \<noteq> y)" |
|
25 |
||
26 |
lemma lt_intro [intro]: |
|
27 |
assumes "x <<= y" and "x \<noteq> y" |
|
28 |
shows "x << y" |
|
29 |
unfolding lt_def .. |
|
30 |
||
31 |
lemma lt_elim [elim]: |
|
32 |
assumes "(x::'a::ordered) << y" |
|
33 |
and Q: "!!x y::'a::ordered. x <<= y \<Longrightarrow> x \<noteq> y \<Longrightarrow> P" |
|
34 |
shows P |
|
35 |
proof - |
|
36 |
from prems have R1: "x <<= y" and R2: "x \<noteq> y" by (simp_all add: lt_def) |
|
37 |
show P by (rule Q [OF R1 R2]) |
|
38 |
qed |
|
39 |
||
40 |
lemma lt_trans: |
|
41 |
assumes "x << y" and "y << z" |
|
42 |
shows "x << z" |
|
43 |
proof |
|
44 |
from prems lt_def have prems': "x <<= y" "y <<= z" by auto |
|
45 |
show "x <<= z" by (rule order_trans, auto intro: prems') |
|
46 |
next |
|
47 |
show "x \<noteq> z" |
|
48 |
proof |
|
49 |
from prems lt_def have prems': "x <<= y" "y <<= z" "x \<noteq> y" by auto |
|
50 |
assume "x = z" |
|
51 |
with prems' have "x <<= y" and "y <<= x" by auto |
|
52 |
with order_antisym have "x = y" . |
|
53 |
with prems' show False by auto |
|
54 |
qed |
|
55 |
qed |
|
56 |
||
57 |
definition (in ordered) |
|
58 |
min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
59 |
"min x y = (if x \<^loc><<= y then x else y)" |
|
60 |
max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
61 |
"max x y = (if x \<^loc><<= y then y else x)" |
|
62 |
||
63 |
definition |
|
64 |
min :: "'a::ordered \<Rightarrow> 'a \<Rightarrow> 'a" |
|
65 |
"min x y = (if x <<= y then x else y)" |
|
66 |
max :: "'a::ordered \<Rightarrow> 'a \<Rightarrow> 'a" |
|
67 |
"max x y = (if x <<= y then y else x)" |
|
68 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
69 |
fun abs_sorted :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
70 |
where |
20436 | 71 |
"abs_sorted cmp [] = True" |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
72 |
| "abs_sorted cmp [x] = True" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
73 |
| "abs_sorted cmp (x#y#xs) = (cmp x y \<and> abs_sorted cmp (y#xs))" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
74 |
|
20436 | 75 |
termination by (auto_term "measure (length o snd)") |
76 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
77 |
thm abs_sorted.simps |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
78 |
|
20436 | 79 |
abbreviation (in ordered) |
80 |
"sorted \<equiv> abs_sorted le" |
|
81 |
||
82 |
abbreviation |
|
83 |
"sorted \<equiv> abs_sorted le" |
|
84 |
||
85 |
lemma (in ordered) sorted_weakening: |
|
86 |
assumes "sorted (x # xs)" |
|
87 |
shows "sorted xs" |
|
88 |
using prems proof (induct xs) |
|
89 |
case Nil show ?case by simp |
|
90 |
next |
|
91 |
case (Cons x' xs) |
|
92 |
from this(5) have "sorted (x # x' # xs)" . |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
93 |
then show "sorted (x' # xs)" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
94 |
by auto |
20436 | 95 |
qed |
96 |
||
97 |
instance bool :: ordered |
|
98 |
"p <<= q == (p --> q)" |
|
99 |
by default (unfold ordered_bool_def, blast+) |
|
100 |
||
101 |
instance nat :: ordered |
|
102 |
"m <<= n == m <= n" |
|
103 |
by default (simp_all add: ordered_nat_def) |
|
104 |
||
105 |
instance int :: ordered |
|
106 |
"k <<= l == k <= l" |
|
107 |
by default (simp_all add: ordered_int_def) |
|
108 |
||
109 |
instance unit :: ordered |
|
110 |
"u <<= v == True" |
|
111 |
by default (simp_all add: ordered_unit_def) |
|
112 |
||
113 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
114 |
fun le_option' :: "'a::ordered option \<Rightarrow> 'a option \<Rightarrow> bool" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
115 |
where |
20436 | 116 |
"le_option' None y = True" |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
117 |
| "le_option' (Some x) None = False" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
118 |
| "le_option' (Some x) (Some y) = x <<= y" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
119 |
|
20436 | 120 |
termination by (auto_term "{}") |
121 |
||
20597 | 122 |
instance option :: (ordered) ordered |
20436 | 123 |
"x <<= y == le_option' x y" |
124 |
proof (default, unfold ordered_option_def) |
|
125 |
fix x |
|
126 |
show "le_option' x x" by (cases x) simp_all |
|
127 |
next |
|
128 |
fix x y z |
|
129 |
assume "le_option' x y" "le_option' y z" |
|
130 |
then show "le_option' x z" |
|
131 |
by (cases x, simp_all, cases y, simp_all, cases z, simp_all) |
|
132 |
(erule order_trans, assumption) |
|
133 |
next |
|
134 |
fix x y |
|
135 |
assume "le_option' x y" "le_option' y x" |
|
136 |
then show "x = y" |
|
137 |
by (cases x, simp_all, cases y, simp_all, cases y, simp_all) |
|
138 |
(erule order_antisym, assumption) |
|
139 |
qed |
|
140 |
||
141 |
lemma [simp, code]: |
|
142 |
"None <<= y = True" |
|
143 |
"Some x <<= None = False" |
|
144 |
"Some v <<= Some w = v <<= w" |
|
145 |
unfolding ordered_option_def le_option'.simps by rule+ |
|
146 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
147 |
fun le_pair' :: "'a::ordered \<times> 'b::ordered \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
148 |
where |
20436 | 149 |
"le_pair' (x1, y1) (x2, y2) = (x1 << x2 \<or> x1 = x2 \<and> y1 <<= y2)" |
150 |
termination by (auto_term "{}") |
|
151 |
||
20597 | 152 |
instance * :: (ordered, ordered) ordered |
20436 | 153 |
"x <<= y == le_pair' x y" |
154 |
apply (default, unfold "ordered_*_def", unfold split_paired_all) |
|
155 |
apply simp_all |
|
156 |
apply (auto intro: lt_trans order_trans)[1] |
|
157 |
unfolding lt_def apply (auto intro: order_antisym)[1] |
|
158 |
done |
|
159 |
||
160 |
lemma [simp, code]: |
|
161 |
"(x1, y1) <<= (x2, y2) = (x1 << x2 \<or> x1 = x2 \<and> y1 <<= y2)" |
|
162 |
unfolding "ordered_*_def" le_pair'.simps .. |
|
163 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
164 |
(* |
20436 | 165 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
166 |
fun le_list' :: "'a::ordered list \<Rightarrow> 'a list \<Rightarrow> bool" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
167 |
where |
20436 | 168 |
"le_list' [] ys = True" |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
169 |
| "le_list' (x#xs) [] = False" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
170 |
| "le_list' (x#xs) (y#ys) = (x << y \<or> x = y \<and> le_list' xs ys)" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
171 |
|
20436 | 172 |
termination by (auto_term "measure (length o fst)") |
173 |
||
174 |
instance (ordered) list :: ordered |
|
175 |
"xs <<= ys == le_list' xs ys" |
|
176 |
proof (default, unfold "ordered_list_def") |
|
177 |
fix xs |
|
178 |
show "le_list' xs xs" by (induct xs) simp_all |
|
179 |
next |
|
180 |
fix xs ys zs |
|
181 |
assume "le_list' xs ys" and "le_list' ys zs" |
|
182 |
then show "le_list' xs zs" |
|
183 |
apply (induct xs zs rule: le_list'.induct) |
|
184 |
apply simp_all |
|
185 |
apply (cases ys) apply simp_all |
|
186 |
||
187 |
apply (induct ys) apply simp_all |
|
188 |
apply (induct ys) |
|
189 |
apply simp_all |
|
190 |
apply (induct zs) |
|
191 |
apply simp_all |
|
192 |
next |
|
193 |
fix xs ys |
|
194 |
assume "le_list' xs ys" and "le_list' ys xs" |
|
195 |
show "xs = ys" sorry |
|
196 |
qed |
|
197 |
||
198 |
lemma [simp, code]: |
|
199 |
"[] <<= ys = True" |
|
200 |
"(x#xs) <<= [] = False" |
|
201 |
"(x#xs) <<= (y#ys) = (x << y \<or> x = y \<and> xs <<= ys)" |
|
202 |
unfolding "ordered_list_def" le_list'.simps by rule+*) |
|
203 |
||
204 |
class infimum = ordered + |
|
205 |
fixes inf |
|
206 |
assumes inf: "inf \<^loc><<= x" |
|
207 |
||
208 |
lemma (in infimum) |
|
209 |
assumes prem: "a \<^loc><<= inf" |
|
210 |
shows no_smaller: "a = inf" |
|
211 |
using prem inf by (rule order_antisym) |
|
212 |
||
213 |
||
214 |
ML {* set quick_and_dirty *} |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
215 |
function abs_max_of :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
216 |
where |
20436 | 217 |
"abs_max_of cmp inff [] = inff" |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
218 |
| "abs_max_of cmp inff [x] = x" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
219 |
| "abs_max_of cmp inff (x#xs) = |
20436 | 220 |
ordered.max cmp x (abs_max_of cmp inff xs)" |
221 |
apply pat_completeness sorry |
|
222 |
||
223 |
abbreviation (in infimum) |
|
224 |
"max_of xs \<equiv> abs_max_of le inf" |
|
225 |
||
226 |
abbreviation |
|
227 |
"max_of xs \<equiv> abs_max_of le inf" |
|
228 |
||
229 |
instance bool :: infimum |
|
230 |
"inf == False" |
|
231 |
by default (simp add: infimum_bool_def) |
|
232 |
||
233 |
instance nat :: infimum |
|
234 |
"inf == 0" |
|
235 |
by default (simp add: infimum_nat_def) |
|
236 |
||
237 |
instance unit :: infimum |
|
238 |
"inf == ()" |
|
239 |
by default (simp add: infimum_unit_def) |
|
240 |
||
20597 | 241 |
instance option :: (ordered) infimum |
20436 | 242 |
"inf == None" |
243 |
by default (simp add: infimum_option_def) |
|
244 |
||
20597 | 245 |
instance * :: (infimum, infimum) infimum |
20436 | 246 |
"inf == (inf, inf)" |
247 |
by default (unfold "infimum_*_def", unfold split_paired_all, auto intro: inf) |
|
248 |
||
249 |
class enum = ordered + |
|
250 |
fixes enum :: "'a list" |
|
251 |
assumes member_enum: "x \<in> set enum" |
|
252 |
and ordered_enum: "abs_sorted le enum" |
|
253 |
||
254 |
(* |
|
255 |
FIXME: |
|
256 |
- abbreviations must be propagated before locale introduction |
|
257 |
- then also now shadowing may occur |
|
258 |
*) |
|
259 |
(*abbreviation (in enum) |
|
260 |
"local.sorted \<equiv> abs_sorted le"*) |
|
261 |
||
262 |
instance bool :: enum |
|
263 |
(* FIXME: better name handling of definitions *) |
|
264 |
"_1": "enum == [False, True]" |
|
265 |
by default (simp_all add: enum_bool_def) |
|
266 |
||
267 |
instance unit :: enum |
|
268 |
"_2": "enum == [()]" |
|
269 |
by default (simp_all add: enum_unit_def) |
|
270 |
||
271 |
(*consts |
|
272 |
product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a * 'b) list" |
|
273 |
||
274 |
primrec |
|
275 |
"product [] ys = []" |
|
276 |
"product (x#xs) ys = map (Pair x) ys @ product xs ys" |
|
277 |
||
278 |
lemma product_all: |
|
279 |
assumes "x \<in> set xs" "y \<in> set ys" |
|
280 |
shows "(x, y) \<in> set (product xs ys)" |
|
281 |
using prems proof (induct xs) |
|
282 |
case Nil |
|
283 |
then have False by auto |
|
284 |
then show ?case .. |
|
285 |
next |
|
286 |
case (Cons z xs) |
|
287 |
then show ?case |
|
288 |
proof (cases "x = z") |
|
289 |
case True |
|
290 |
with Cons have "(x, y) \<in> set (product (x # xs) ys)" by simp |
|
291 |
with True show ?thesis by simp |
|
292 |
next |
|
293 |
case False |
|
294 |
with Cons have "x \<in> set xs" by auto |
|
295 |
with Cons have "(x, y) \<in> set (product xs ys)" by auto |
|
296 |
then show "(x, y) \<in> set (product (z#xs) ys)" by auto |
|
297 |
qed |
|
298 |
qed |
|
299 |
||
300 |
lemma product_sorted: |
|
301 |
assumes "sorted xs" "sorted ys" |
|
302 |
shows "sorted (product xs ys)" |
|
303 |
using prems proof (induct xs) |
|
304 |
case Nil |
|
305 |
then show ?case by simp |
|
306 |
next |
|
307 |
case (Cons x xs) |
|
308 |
from Cons ordered.sorted_weakening have "sorted xs" by auto |
|
309 |
with Cons have "sorted (product xs ys)" by auto |
|
310 |
then show ?case apply simp |
|
311 |
proof - |
|
312 |
assume |
|
313 |
apply simp |
|
314 |
||
315 |
proof (cases "x = z") |
|
316 |
case True |
|
317 |
with Cons have "(x, y) \<in> set (product (x # xs) ys)" by simp |
|
318 |
with True show ?thesis by simp |
|
319 |
next |
|
320 |
case False |
|
321 |
with Cons have "x \<in> set xs" by auto |
|
322 |
with Cons have "(x, y) \<in> set (product xs ys)" by auto |
|
323 |
then show "(x, y) \<in> set (product (z#xs) ys)" by auto |
|
324 |
qed |
|
325 |
qed |
|
326 |
||
327 |
instance (enum, enum) * :: enum |
|
328 |
"_3": "enum == product enum enum" |
|
329 |
apply default |
|
330 |
apply (simp_all add: "enum_*_def") |
|
331 |
apply (unfold split_paired_all) |
|
332 |
apply (rule product_all) |
|
333 |
apply (rule member_enum)+ |
|
334 |
sorry*) |
|
335 |
||
20597 | 336 |
instance option :: (enum) enum |
20436 | 337 |
"_4": "enum == None # map Some enum" |
338 |
proof (default, unfold enum_option_def) |
|
339 |
fix x :: "'a::enum option" |
|
340 |
show "x \<in> set (None # map Some enum)" |
|
341 |
proof (cases x) |
|
342 |
case None then show ?thesis by auto |
|
343 |
next |
|
344 |
case (Some x) then show ?thesis by (auto intro: member_enum) |
|
345 |
qed |
|
346 |
next |
|
347 |
show "sorted (None # map Some (enum :: ('a::enum) list))" |
|
348 |
sorry |
|
349 |
(*proof (cases "enum :: 'a list") |
|
350 |
case Nil then show ?thesis by simp |
|
351 |
next |
|
352 |
case (Cons x xs) |
|
353 |
then have "sorted (None # map Some (x # xs))" sorry |
|
354 |
then show ?thesis apply simp |
|
355 |
apply simp_all |
|
356 |
apply auto*) |
|
357 |
qed |
|
358 |
||
359 |
ML {* reset quick_and_dirty *} |
|
360 |
||
361 |
consts |
|
362 |
get_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a option" |
|
363 |
||
364 |
primrec |
|
365 |
"get_first p [] = None" |
|
366 |
"get_first p (x#xs) = (if p x then Some x else get_first p xs)" |
|
367 |
||
368 |
consts |
|
369 |
get_index :: "('a \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> nat option" |
|
370 |
||
371 |
primrec |
|
372 |
"get_index p n [] = None" |
|
373 |
"get_index p n (x#xs) = (if p x then Some n else get_index p (Suc n) xs)" |
|
374 |
||
375 |
definition |
|
376 |
between :: "'a::enum \<Rightarrow> 'a \<Rightarrow> 'a option" |
|
377 |
"between x y = get_first (\<lambda>z. x << z & z << y) enum" |
|
378 |
||
379 |
definition |
|
380 |
index :: "'a::enum \<Rightarrow> nat" |
|
381 |
"index x = the (get_index (\<lambda>y. y = x) 0 enum)" |
|
382 |
||
383 |
definition |
|
384 |
add :: "'a::enum \<Rightarrow> 'a \<Rightarrow> 'a" |
|
385 |
"add x y = |
|
386 |
(let |
|
387 |
enm = enum |
|
388 |
in enm ! ((index x + index y) mod length enm))" |
|
389 |
||
390 |
consts |
|
391 |
sum :: "'a::{enum, infimum} list \<Rightarrow> 'a" |
|
392 |
||
393 |
primrec |
|
394 |
"sum [] = inf" |
|
395 |
"sum (x#xs) = add x (sum xs)" |
|
396 |
||
397 |
definition |
|
398 |
"test1 = sum [None, Some True, None, Some False]" |
|
399 |
"test2 = (inf :: nat \<times> unit)" |
|
400 |
||
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20436
diff
changeset
|
401 |
code_gen "op <<=" |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20436
diff
changeset
|
402 |
code_gen "op <<" |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20436
diff
changeset
|
403 |
code_gen inf |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20436
diff
changeset
|
404 |
code_gen between |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20436
diff
changeset
|
405 |
code_gen index |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20436
diff
changeset
|
406 |
code_gen test1 |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20436
diff
changeset
|
407 |
code_gen test2 |
20436 | 408 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20436
diff
changeset
|
409 |
code_gen (SML -) |
21080 | 410 |
code_gen (Haskell -) |
20436 | 411 |
|
412 |
end |