author | oheimb |
Wed, 03 Apr 2002 10:21:13 +0200 | |
changeset 13076 | 70704dd48bd5 |
parent 12789 | 459b5de466b2 |
child 13327 | be7105a066d3 |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/List |
516 | 2 |
ID: $Id$ |
1478 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
516 | 4 |
Copyright 1994 University of Cambridge |
5 |
||
6 |
Lists in Zermelo-Fraenkel Set Theory |
|
7 |
||
8 |
map is a binding operator -- it applies to meta-level functions, not |
|
9 |
object-level functions. This simplifies the final form of term_rec_conv, |
|
10 |
although complicating its derivation. |
|
11 |
*) |
|
12 |
||
9548 | 13 |
List = Datatype + ArithSimp + |
516 | 14 |
|
15 |
consts |
|
12789 | 16 |
list :: "i=>i" |
516 | 17 |
|
18 |
datatype |
|
581 | 19 |
"list(A)" = Nil | Cons ("a:A", "l: list(A)") |
516 | 20 |
|
21 |
||
2539 | 22 |
syntax |
23 |
"[]" :: i ("[]") |
|
12789 | 24 |
"@List" :: "is => i" ("[(_)]") |
2539 | 25 |
|
516 | 26 |
translations |
27 |
"[x, xs]" == "Cons(x, [xs])" |
|
28 |
"[x]" == "Cons(x, [])" |
|
29 |
"[]" == "Nil" |
|
30 |
||
31 |
||
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
32 |
consts |
12789 | 33 |
length :: "i=>i" |
34 |
hd :: "i=>i" |
|
35 |
tl :: "i=>i" |
|
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
36 |
|
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
37 |
primrec |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
38 |
"length([]) = 0" |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
39 |
"length(Cons(a,l)) = succ(length(l))" |
1806 | 40 |
|
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
41 |
primrec |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
42 |
"hd(Cons(a,l)) = a" |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
43 |
|
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
44 |
primrec |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
45 |
"tl([]) = []" |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
46 |
"tl(Cons(a,l)) = l" |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
47 |
|
6070 | 48 |
|
49 |
consts |
|
12789 | 50 |
map :: "[i=>i, i] => i" |
51 |
set_of_list :: "i=>i" |
|
52 |
"@" :: "[i,i]=>i" (infixr 60) |
|
6070 | 53 |
|
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
54 |
primrec |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
55 |
"map(f,[]) = []" |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
56 |
"map(f,Cons(a,l)) = Cons(f(a), map(f,l))" |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
57 |
|
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
58 |
primrec |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
59 |
"set_of_list([]) = 0" |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
60 |
"set_of_list(Cons(a,l)) = cons(a, set_of_list(l))" |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
61 |
|
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
62 |
primrec |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
63 |
"[] @ ys = ys" |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
64 |
"(Cons(a,l)) @ ys = Cons(a, l @ ys)" |
1806 | 65 |
|
6070 | 66 |
|
67 |
consts |
|
12789 | 68 |
rev :: "i=>i" |
69 |
flat :: "i=>i" |
|
70 |
list_add :: "i=>i" |
|
6070 | 71 |
|
6053
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
72 |
primrec |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
73 |
"rev([]) = []" |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
74 |
"rev(Cons(a,l)) = rev(l) @ [a]" |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
75 |
|
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
76 |
primrec |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
77 |
"flat([]) = []" |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
78 |
"flat(Cons(l,ls)) = l @ flat(ls)" |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
79 |
|
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
80 |
primrec |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
81 |
"list_add([]) = 0" |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
82 |
"list_add(Cons(a,l)) = a #+ list_add(l)" |
8a1059aa01f0
new inductive, datatype and primrec packages, etc.
paulson
parents:
3840
diff
changeset
|
83 |
|
6070 | 84 |
consts |
12789 | 85 |
drop :: "[i,i]=>i" |
6070 | 86 |
|
87 |
primrec |
|
88 |
drop_0 "drop(0,l) = l" |
|
89 |
drop_SUCC "drop(succ(i), l) = tl (drop(i,l))" |
|
516 | 90 |
|
12789 | 91 |
|
92 |
(*** Thanks to Sidi Ehmety for the following ***) |
|
93 |
||
94 |
constdefs |
|
95 |
(* Function `take' returns the first n elements of a list *) |
|
96 |
take :: "[i,i]=>i" |
|
97 |
"take(n, as) == list_rec(lam n:nat. [], |
|
98 |
%a l r. lam n:nat. nat_case([], %m. Cons(a, r`m), n), as)`n" |
|
99 |
||
100 |
(* Function `nth' returns the (n+1)th element in a list (not defined at Nil) *) |
|
101 |
nth :: "[i, i]=>i" |
|
102 |
"nth(n, as) == list_rec(lam n:nat. 0, |
|
103 |
%a l r. lam n:nat. nat_case(a, %m. r`m, n), as)`n" |
|
104 |
||
105 |
list_update :: "[i, i, i]=>i" |
|
106 |
"list_update(xs, i, v) == list_rec(lam n:nat. Nil, |
|
107 |
%u us vs. lam n:nat. nat_case(Cons(v, us), %m. Cons(u, vs`m), n), xs)`i" |
|
108 |
||
109 |
consts |
|
110 |
filter :: "[i=>o, i] => i" |
|
111 |
zip :: "[i, i]=>i" |
|
112 |
ziprel :: "[i,i]=>i" |
|
113 |
upt :: "[i, i] =>i" |
|
114 |
||
115 |
inductive domains "ziprel(A, B)" <= "list(A)*list(B)*list(A*B)" |
|
116 |
intrs |
|
117 |
ziprel_Nil1 "ys:list(B) ==><Nil, ys, Nil>:ziprel(A, B)" |
|
118 |
ziprel_Nil2 "xs:list(A) ==><xs, Nil, Nil>:ziprel(A, B)" |
|
119 |
ziprel_Cons "[| <xs, ys, zs>:ziprel(A, B); x:A; y:B |]==> |
|
120 |
<Cons(x, xs), Cons(y, ys), Cons(<x, y>, zs)>:ziprel(A,B)" |
|
121 |
type_intrs "list.intrs" |
|
122 |
||
123 |
defs |
|
124 |
zip_def "zip(xs, ys) == |
|
125 |
THE zs. <xs, ys, zs>:ziprel(set_of_list(xs),set_of_list(ys))" |
|
126 |
||
127 |
primrec |
|
128 |
"filter(P, Nil) = Nil" |
|
129 |
"filter(P, Cons(x, xs)) = |
|
130 |
(if P(x) then Cons(x, filter(P, xs)) else filter(P, xs))" |
|
131 |
||
132 |
primrec |
|
133 |
"upt(i, 0) = Nil" |
|
134 |
"upt(i, succ(j)) = (if i le j then upt(i, j)@[j] else Nil)" |
|
135 |
||
136 |
constdefs |
|
137 |
sublist :: "[i, i] => i" |
|
138 |
"sublist(xs, A)== |
|
139 |
map(fst, (filter(%p. snd(p): A, zip(xs, upt(0,length(xs))))))" |
|
140 |
||
141 |
min :: "[i,i] =>i" |
|
142 |
"min(x, y) == (if x le y then x else y)" |
|
143 |
||
144 |
max :: "[i, i] =>i" |
|
145 |
"max(x, y) == (if x le y then y else x)" |
|
146 |
||
516 | 147 |
end |