|
1 (* Title: HOL/BCV/Listn.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 2000 TUM |
|
5 |
|
6 Lists of a fixed length |
|
7 *) |
|
8 |
|
9 header "Fixed Length Lists" |
|
10 |
|
11 theory Listn = Err: |
|
12 |
|
13 constdefs |
|
14 |
|
15 list :: "nat => 'a set => 'a list set" |
|
16 "list n A == {xs. length xs = n & set xs <= A}" |
|
17 |
|
18 le :: "'a ord => ('a list)ord" |
|
19 "le r == list_all2 (%x y. x <=_r y)" |
|
20 |
|
21 syntax "@lesublist" :: "'a list => 'a ord => 'a list => bool" |
|
22 ("(_ /<=[_] _)" [50, 0, 51] 50) |
|
23 syntax "@lesssublist" :: "'a list => 'a ord => 'a list => bool" |
|
24 ("(_ /<[_] _)" [50, 0, 51] 50) |
|
25 translations |
|
26 "x <=[r] y" == "x <=_(Listn.le r) y" |
|
27 "x <[r] y" == "x <_(Listn.le r) y" |
|
28 |
|
29 constdefs |
|
30 map2 :: "('a => 'b => 'c) => 'a list => 'b list => 'c list" |
|
31 "map2 f == (%xs ys. map (split f) (zip xs ys))" |
|
32 |
|
33 syntax "@plussublist" :: "'a list => ('a => 'b => 'c) => 'b list => 'c list" |
|
34 ("(_ /+[_] _)" [65, 0, 66] 65) |
|
35 translations "x +[f] y" == "x +_(map2 f) y" |
|
36 |
|
37 consts coalesce :: "'a err list => 'a list err" |
|
38 primrec |
|
39 "coalesce [] = OK[]" |
|
40 "coalesce (ex#exs) = Err.sup (op #) ex (coalesce exs)" |
|
41 |
|
42 constdefs |
|
43 sl :: "nat => 'a sl => 'a list sl" |
|
44 "sl n == %(A,r,f). (list n A, le r, map2 f)" |
|
45 |
|
46 sup :: "('a => 'b => 'c err) => 'a list => 'b list => 'c list err" |
|
47 "sup f == %xs ys. if size xs = size ys then coalesce(xs +[f] ys) else Err" |
|
48 |
|
49 upto_esl :: "nat => 'a esl => 'a list esl" |
|
50 "upto_esl m == %(A,r,f). (Union{list n A |n. n <= m}, le r, sup f)" |
|
51 |
|
52 lemmas [simp] = set_update_subsetI |
|
53 |
|
54 lemma unfold_lesub_list: |
|
55 "xs <=[r] ys == Listn.le r xs ys" |
|
56 by (simp add: lesub_def) |
|
57 |
|
58 lemma Nil_le_conv [iff]: |
|
59 "([] <=[r] ys) = (ys = [])" |
|
60 apply (unfold lesub_def Listn.le_def) |
|
61 apply simp |
|
62 done |
|
63 |
|
64 lemma Cons_notle_Nil [iff]: |
|
65 "~ x#xs <=[r] []" |
|
66 apply (unfold lesub_def Listn.le_def) |
|
67 apply simp |
|
68 done |
|
69 |
|
70 |
|
71 lemma Cons_le_Cons [iff]: |
|
72 "x#xs <=[r] y#ys = (x <=_r y & xs <=[r] ys)" |
|
73 apply (unfold lesub_def Listn.le_def) |
|
74 apply simp |
|
75 done |
|
76 |
|
77 lemma Cons_less_Conss [simp]: |
|
78 "order r ==> |
|
79 x#xs <_(Listn.le r) y#ys = |
|
80 (x <_r y & xs <=[r] ys | x = y & xs <_(Listn.le r) ys)" |
|
81 apply (unfold lesssub_def) |
|
82 apply blast |
|
83 done |
|
84 |
|
85 lemma list_update_le_cong: |
|
86 "[| i<size xs; xs <=[r] ys; x <=_r y |] ==> xs[i:=x] <=[r] ys[i:=y]"; |
|
87 apply (unfold unfold_lesub_list) |
|
88 apply (unfold Listn.le_def) |
|
89 apply (simp add: list_all2_conv_all_nth nth_list_update) |
|
90 done |
|
91 |
|
92 |
|
93 lemma le_listD: |
|
94 "[| xs <=[r] ys; p < size xs |] ==> xs!p <=_r ys!p" |
|
95 apply (unfold Listn.le_def lesub_def) |
|
96 apply (simp add: list_all2_conv_all_nth) |
|
97 done |
|
98 |
|
99 lemma le_list_refl: |
|
100 "!x. x <=_r x ==> xs <=[r] xs" |
|
101 apply (unfold unfold_lesub_list) |
|
102 apply (simp add: Listn.le_def list_all2_conv_all_nth) |
|
103 done |
|
104 |
|
105 lemma le_list_trans: |
|
106 "[| order r; xs <=[r] ys; ys <=[r] zs |] ==> xs <=[r] zs" |
|
107 apply (unfold unfold_lesub_list) |
|
108 apply (simp add: Listn.le_def list_all2_conv_all_nth) |
|
109 apply clarify |
|
110 apply simp |
|
111 apply (blast intro: order_trans) |
|
112 done |
|
113 |
|
114 lemma le_list_antisym: |
|
115 "[| order r; xs <=[r] ys; ys <=[r] xs |] ==> xs = ys" |
|
116 apply (unfold unfold_lesub_list) |
|
117 apply (simp add: Listn.le_def list_all2_conv_all_nth) |
|
118 apply (rule nth_equalityI) |
|
119 apply blast |
|
120 apply clarify |
|
121 apply simp |
|
122 apply (blast intro: order_antisym) |
|
123 done |
|
124 |
|
125 lemma order_listI [simp, intro!]: |
|
126 "order r ==> order(Listn.le r)" |
|
127 apply (subst order_def) |
|
128 apply (blast intro: le_list_refl le_list_trans le_list_antisym |
|
129 dest: order_refl) |
|
130 done |
|
131 |
|
132 |
|
133 lemma lesub_list_impl_same_size [simp]: |
|
134 "xs <=[r] ys ==> size ys = size xs" |
|
135 apply (unfold Listn.le_def lesub_def) |
|
136 apply (simp add: list_all2_conv_all_nth) |
|
137 done |
|
138 |
|
139 lemma lesssub_list_impl_same_size: |
|
140 "xs <_(Listn.le r) ys ==> size ys = size xs" |
|
141 apply (unfold lesssub_def) |
|
142 apply auto |
|
143 done |
|
144 |
|
145 lemma listI: |
|
146 "[| length xs = n; set xs <= A |] ==> xs : list n A" |
|
147 apply (unfold list_def) |
|
148 apply blast |
|
149 done |
|
150 |
|
151 lemma listE_length [simp]: |
|
152 "xs : list n A ==> length xs = n" |
|
153 apply (unfold list_def) |
|
154 apply blast |
|
155 done |
|
156 |
|
157 lemma less_lengthI: |
|
158 "[| xs : list n A; p < n |] ==> p < length xs" |
|
159 by simp |
|
160 |
|
161 lemma listE_set [simp]: |
|
162 "xs : list n A ==> set xs <= A" |
|
163 apply (unfold list_def) |
|
164 apply blast |
|
165 done |
|
166 |
|
167 lemma list_0 [simp]: |
|
168 "list 0 A = {[]}" |
|
169 apply (unfold list_def) |
|
170 apply auto |
|
171 done |
|
172 |
|
173 lemma in_list_Suc_iff: |
|
174 "(xs : list (Suc n) A) = (? y:A. ? ys:list n A. xs = y#ys)" |
|
175 apply (unfold list_def) |
|
176 apply (case_tac "xs") |
|
177 apply auto |
|
178 done |
|
179 |
|
180 lemma Cons_in_list_Suc [iff]: |
|
181 "(x#xs : list (Suc n) A) = (x:A & xs : list n A)"; |
|
182 apply (simp add: in_list_Suc_iff) |
|
183 apply blast |
|
184 done |
|
185 |
|
186 lemma list_not_empty: |
|
187 "? a. a:A ==> ? xs. xs : list n A"; |
|
188 apply (induct "n") |
|
189 apply simp |
|
190 apply (simp add: in_list_Suc_iff) |
|
191 apply blast |
|
192 done |
|
193 |
|
194 |
|
195 lemma nth_in [rule_format, simp]: |
|
196 "!i n. length xs = n --> set xs <= A --> i < n --> (xs!i) : A" |
|
197 apply (induct "xs") |
|
198 apply simp |
|
199 apply (simp add: nth_Cons split: nat.split) |
|
200 done |
|
201 |
|
202 lemma listE_nth_in: |
|
203 "[| xs : list n A; i < n |] ==> (xs!i) : A" |
|
204 by auto |
|
205 |
|
206 lemma listt_update_in_list [simp, intro!]: |
|
207 "[| xs : list n A; x:A |] ==> xs[i := x] : list n A" |
|
208 apply (unfold list_def) |
|
209 apply simp |
|
210 done |
|
211 |
|
212 lemma plus_list_Nil [simp]: |
|
213 "[] +[f] xs = []" |
|
214 apply (unfold plussub_def map2_def) |
|
215 apply simp |
|
216 done |
|
217 |
|
218 lemma plus_list_Cons [simp]: |
|
219 "(x#xs) +[f] ys = (case ys of [] => [] | y#ys => (x +_f y)#(xs +[f] ys))" |
|
220 by (simp add: plussub_def map2_def split: list.split) |
|
221 |
|
222 lemma length_plus_list [rule_format, simp]: |
|
223 "!ys. length(xs +[f] ys) = min(length xs) (length ys)" |
|
224 apply (induct xs) |
|
225 apply simp |
|
226 apply clarify |
|
227 apply (simp (no_asm_simp) split: list.split) |
|
228 done |
|
229 |
|
230 lemma nth_plus_list [rule_format, simp]: |
|
231 "!xs ys i. length xs = n --> length ys = n --> i<n --> |
|
232 (xs +[f] ys)!i = (xs!i) +_f (ys!i)" |
|
233 apply (induct n) |
|
234 apply simp |
|
235 apply clarify |
|
236 apply (case_tac xs) |
|
237 apply simp |
|
238 apply (force simp add: nth_Cons split: list.split nat.split) |
|
239 done |
|
240 |
|
241 |
|
242 lemma plus_list_ub1 [rule_format]: |
|
243 "[| semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys |] |
|
244 ==> xs <=[r] xs +[f] ys" |
|
245 apply (unfold unfold_lesub_list) |
|
246 apply (simp add: Listn.le_def list_all2_conv_all_nth) |
|
247 done |
|
248 |
|
249 lemma plus_list_ub2: |
|
250 "[| semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys |] |
|
251 ==> ys <=[r] xs +[f] ys" |
|
252 apply (unfold unfold_lesub_list) |
|
253 apply (simp add: Listn.le_def list_all2_conv_all_nth) |
|
254 done |
|
255 |
|
256 lemma plus_list_lub [rule_format]: |
|
257 "semilat(A,r,f) ==> !xs ys zs. set xs <= A --> set ys <= A --> set zs <= A |
|
258 --> size xs = n & size ys = n --> |
|
259 xs <=[r] zs & ys <=[r] zs --> xs +[f] ys <=[r] zs" |
|
260 apply (unfold unfold_lesub_list) |
|
261 apply (simp add: Listn.le_def list_all2_conv_all_nth) |
|
262 done |
|
263 |
|
264 lemma list_update_incr [rule_format]: |
|
265 "[| semilat(A,r,f); x:A |] ==> set xs <= A --> |
|
266 (!i. i<size xs --> xs <=[r] xs[i := x +_f xs!i])" |
|
267 apply (unfold unfold_lesub_list) |
|
268 apply (simp add: Listn.le_def list_all2_conv_all_nth) |
|
269 apply (induct xs) |
|
270 apply simp |
|
271 apply (simp add: in_list_Suc_iff) |
|
272 apply clarify |
|
273 apply (simp add: nth_Cons split: nat.split) |
|
274 done |
|
275 |
|
276 lemma acc_le_listI [intro!]: |
|
277 "[| order r; acc r |] ==> acc(Listn.le r)" |
|
278 apply (unfold acc_def) |
|
279 apply (subgoal_tac |
|
280 "wf(UN n. {(ys,xs). size xs = n & size ys = n & xs <_(Listn.le r) ys})") |
|
281 apply (erule wf_subset) |
|
282 apply (blast intro: lesssub_list_impl_same_size) |
|
283 apply (rule wf_UN) |
|
284 prefer 2 |
|
285 apply clarify |
|
286 apply (rename_tac m n) |
|
287 apply (case_tac "m=n") |
|
288 apply simp |
|
289 apply (rule conjI) |
|
290 apply (fast intro!: equals0I dest: not_sym) |
|
291 apply (fast intro!: equals0I dest: not_sym) |
|
292 apply clarify |
|
293 apply (rename_tac n) |
|
294 apply (induct_tac n) |
|
295 apply (simp add: lesssub_def cong: conj_cong) |
|
296 apply (rename_tac k) |
|
297 apply (simp add: wf_eq_minimal) |
|
298 apply (simp (no_asm) add: length_Suc_conv cong: conj_cong) |
|
299 apply clarify |
|
300 apply (rename_tac M m) |
|
301 apply (case_tac "? x xs. size xs = k & x#xs : M") |
|
302 prefer 2 |
|
303 apply (erule thin_rl) |
|
304 apply (erule thin_rl) |
|
305 apply blast |
|
306 apply (erule_tac x = "{a. ? xs. size xs = k & a#xs:M}" in allE) |
|
307 apply (erule impE) |
|
308 apply blast |
|
309 apply (thin_tac "? x xs. ?P x xs") |
|
310 apply clarify |
|
311 apply (rename_tac maxA xs) |
|
312 apply (erule_tac x = "{ys. size ys = size xs & maxA#ys : M}" in allE) |
|
313 apply (erule impE) |
|
314 apply blast |
|
315 apply clarify |
|
316 apply (thin_tac "m : M") |
|
317 apply (thin_tac "maxA#xs : M") |
|
318 apply (rule bexI) |
|
319 prefer 2 |
|
320 apply assumption |
|
321 apply clarify |
|
322 apply simp |
|
323 apply blast |
|
324 done |
|
325 |
|
326 lemma closed_listI: |
|
327 "closed S f ==> closed (list n S) (map2 f)" |
|
328 apply (unfold closed_def) |
|
329 apply (induct n) |
|
330 apply simp |
|
331 apply clarify |
|
332 apply (simp add: in_list_Suc_iff) |
|
333 apply clarify |
|
334 apply simp |
|
335 apply blast |
|
336 done |
|
337 |
|
338 |
|
339 lemma semilat_Listn_sl: |
|
340 "!!L. semilat L ==> semilat (Listn.sl n L)" |
|
341 apply (unfold Listn.sl_def) |
|
342 apply (simp (no_asm_simp) only: split_tupled_all) |
|
343 apply (simp (no_asm) only: semilat_Def Product_Type.split) |
|
344 apply (rule conjI) |
|
345 apply simp |
|
346 apply (rule conjI) |
|
347 apply (simp only: semilatDclosedI closed_listI) |
|
348 apply (simp (no_asm) only: list_def) |
|
349 apply (simp (no_asm_simp) add: plus_list_ub1 plus_list_ub2 plus_list_lub) |
|
350 done |
|
351 |
|
352 |
|
353 lemma coalesce_in_err_list [rule_format]: |
|
354 "!xes. xes : list n (err A) --> coalesce xes : err(list n A)" |
|
355 apply (induct n) |
|
356 apply simp |
|
357 apply clarify |
|
358 apply (simp add: in_list_Suc_iff) |
|
359 apply clarify |
|
360 apply (simp (no_asm) add: plussub_def Err.sup_def lift2_def split: err.split) |
|
361 apply force |
|
362 done |
|
363 |
|
364 lemma lem: "!!x xs. x +_(op #) xs = x#xs" |
|
365 by (simp add: plussub_def) |
|
366 |
|
367 lemma coalesce_eq_OK1_D [rule_format]: |
|
368 "semilat(err A, Err.le r, lift2 f) ==> |
|
369 !xs. xs : list n A --> (!ys. ys : list n A --> |
|
370 (!zs. coalesce (xs +[f] ys) = OK zs --> xs <=[r] zs))" |
|
371 apply (induct n) |
|
372 apply simp |
|
373 apply clarify |
|
374 apply (simp add: in_list_Suc_iff) |
|
375 apply clarify |
|
376 apply (simp split: err.split_asm add: lem Err.sup_def lift2_def) |
|
377 apply (force simp add: semilat_le_err_OK1) |
|
378 done |
|
379 |
|
380 lemma coalesce_eq_OK2_D [rule_format]: |
|
381 "semilat(err A, Err.le r, lift2 f) ==> |
|
382 !xs. xs : list n A --> (!ys. ys : list n A --> |
|
383 (!zs. coalesce (xs +[f] ys) = OK zs --> ys <=[r] zs))" |
|
384 apply (induct n) |
|
385 apply simp |
|
386 apply clarify |
|
387 apply (simp add: in_list_Suc_iff) |
|
388 apply clarify |
|
389 apply (simp split: err.split_asm add: lem Err.sup_def lift2_def) |
|
390 apply (force simp add: semilat_le_err_OK2) |
|
391 done |
|
392 |
|
393 lemma lift2_le_ub: |
|
394 "[| semilat(err A, Err.le r, lift2 f); x:A; y:A; x +_f y = OK z; |
|
395 u:A; x <=_r u; y <=_r u |] ==> z <=_r u" |
|
396 apply (unfold semilat_Def plussub_def err_def) |
|
397 apply (simp add: lift2_def) |
|
398 apply clarify |
|
399 apply (rotate_tac -3) |
|
400 apply (erule thin_rl) |
|
401 apply (erule thin_rl) |
|
402 apply force |
|
403 done |
|
404 |
|
405 lemma coalesce_eq_OK_ub_D [rule_format]: |
|
406 "semilat(err A, Err.le r, lift2 f) ==> |
|
407 !xs. xs : list n A --> (!ys. ys : list n A --> |
|
408 (!zs us. coalesce (xs +[f] ys) = OK zs & xs <=[r] us & ys <=[r] us |
|
409 & us : list n A --> zs <=[r] us))" |
|
410 apply (induct n) |
|
411 apply simp |
|
412 apply clarify |
|
413 apply (simp add: in_list_Suc_iff) |
|
414 apply clarify |
|
415 apply (simp (no_asm_use) split: err.split_asm add: lem Err.sup_def lift2_def) |
|
416 apply clarify |
|
417 apply (rule conjI) |
|
418 apply (blast intro: lift2_le_ub) |
|
419 apply blast |
|
420 done |
|
421 |
|
422 lemma lift2_eq_ErrD: |
|
423 "[| x +_f y = Err; semilat(err A, Err.le r, lift2 f); x:A; y:A |] |
|
424 ==> ~(? u:A. x <=_r u & y <=_r u)" |
|
425 by (simp add: OK_plus_OK_eq_Err_conv [THEN iffD1]) |
|
426 |
|
427 |
|
428 lemma coalesce_eq_Err_D [rule_format]: |
|
429 "[| semilat(err A, Err.le r, lift2 f) |] |
|
430 ==> !xs. xs:list n A --> (!ys. ys:list n A --> |
|
431 coalesce (xs +[f] ys) = Err --> |
|
432 ~(? zs:list n A. xs <=[r] zs & ys <=[r] zs))" |
|
433 apply (induct n) |
|
434 apply simp |
|
435 apply clarify |
|
436 apply (simp add: in_list_Suc_iff) |
|
437 apply clarify |
|
438 apply (simp split: err.split_asm add: lem Err.sup_def lift2_def) |
|
439 apply (blast dest: lift2_eq_ErrD) |
|
440 apply blast |
|
441 done |
|
442 |
|
443 lemma closed_err_lift2_conv: |
|
444 "closed (err A) (lift2 f) = (!x:A. !y:A. x +_f y : err A)" |
|
445 apply (unfold closed_def) |
|
446 apply (simp add: err_def) |
|
447 done |
|
448 |
|
449 lemma closed_map2_list [rule_format]: |
|
450 "closed (err A) (lift2 f) ==> |
|
451 !xs. xs : list n A --> (!ys. ys : list n A --> |
|
452 map2 f xs ys : list n (err A))" |
|
453 apply (unfold map2_def) |
|
454 apply (induct n) |
|
455 apply simp |
|
456 apply clarify |
|
457 apply (simp add: in_list_Suc_iff) |
|
458 apply clarify |
|
459 apply (simp add: plussub_def closed_err_lift2_conv) |
|
460 apply blast |
|
461 done |
|
462 |
|
463 lemma closed_lift2_sup: |
|
464 "closed (err A) (lift2 f) ==> |
|
465 closed (err (list n A)) (lift2 (sup f))" |
|
466 by (fastsimp simp add: closed_def plussub_def sup_def lift2_def |
|
467 coalesce_in_err_list closed_map2_list |
|
468 split: err.split) |
|
469 |
|
470 lemma err_semilat_sup: |
|
471 "err_semilat (A,r,f) ==> |
|
472 err_semilat (list n A, Listn.le r, sup f)" |
|
473 apply (unfold Err.sl_def) |
|
474 apply (simp only: Product_Type.split) |
|
475 apply (simp (no_asm) only: semilat_Def plussub_def) |
|
476 apply (simp (no_asm_simp) only: semilatDclosedI closed_lift2_sup) |
|
477 apply (rule conjI) |
|
478 apply (drule semilatDorderI) |
|
479 apply simp |
|
480 apply (simp (no_asm) only: unfold_lesub_err Err.le_def err_def sup_def lift2_def) |
|
481 apply (simp (no_asm_simp) add: coalesce_eq_OK1_D coalesce_eq_OK2_D split: err.split) |
|
482 apply (blast intro: coalesce_eq_OK_ub_D dest: coalesce_eq_Err_D) |
|
483 done |
|
484 |
|
485 lemma err_semilat_upto_esl: |
|
486 "!!L. err_semilat L ==> err_semilat(upto_esl m L)" |
|
487 apply (unfold Listn.upto_esl_def) |
|
488 apply (simp (no_asm_simp) only: split_tupled_all) |
|
489 apply simp |
|
490 apply (fastsimp intro!: err_semilat_UnionI err_semilat_sup |
|
491 dest: lesub_list_impl_same_size |
|
492 simp add: plussub_def Listn.sup_def) |
|
493 done |
|
494 |
|
495 end |