|
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 Listn = Err + |
|
10 |
|
11 constdefs |
|
12 |
|
13 list :: nat => 'a set => 'a list set |
|
14 "list n A == {xs. length xs = n & set xs <= A}" |
|
15 |
|
16 le :: 'a ord => ('a list)ord |
|
17 "le r == list_all2 (%x y. x <=_r y)" |
|
18 |
|
19 syntax "@lesublist" :: 'a list => 'a ord => 'a list => bool |
|
20 ("(_ /<=[_] _)" [50, 0, 51] 50) |
|
21 syntax "@lesssublist" :: 'a list => 'a ord => 'a list => bool |
|
22 ("(_ /<[_] _)" [50, 0, 51] 50) |
|
23 translations |
|
24 "x <=[r] y" == "x <=_(Listn.le r) y" |
|
25 "x <[r] y" == "x <_(Listn.le r) y" |
|
26 |
|
27 constdefs |
|
28 map2 :: ('a => 'b => 'c) => 'a list => 'b list => 'c list |
|
29 "map2 f == (%xs ys. map (split f) (zip xs ys))" |
|
30 |
|
31 syntax "@plussublist" :: 'a list => ('a => 'b => 'c) => 'b list => 'c list |
|
32 ("(_ /+[_] _)" [65, 0, 66] 65) |
|
33 translations "x +[f] y" == "x +_(map2 f) y" |
|
34 |
|
35 consts coalesce :: 'a err list => 'a list err |
|
36 primrec |
|
37 "coalesce [] = OK[]" |
|
38 "coalesce (ex#exs) = Err.sup (op #) ex (coalesce exs)" |
|
39 |
|
40 constdefs |
|
41 sl :: nat => 'a sl => 'a list sl |
|
42 "sl n == %(A,r,f). (list n A, le r, map2 f)" |
|
43 |
|
44 sup :: ('a => 'b => 'c err) => 'a list => 'b list => 'c list err |
|
45 "sup f == %xs ys. if size xs = size ys then coalesce(xs +[f] ys) else Err" |
|
46 |
|
47 upto_esl :: nat => 'a esl => 'a list esl |
|
48 "upto_esl m == %(A,r,f). (Union{list n A |n. n <= m}, le r, sup f)" |
|
49 |
|
50 end |