author | nipkow |
Sun, 05 Jan 2003 21:03:14 +0100 | |
changeset 13771 | 6cd59cc885a1 |
parent 124 | 858ab9a9b047 |
permissions | -rw-r--r-- |
0 | 1 |
(* Title: ZF/list-fn |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1993 University of Cambridge |
|
5 |
||
6 |
Functions for 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 |
||
124 | 13 |
ListFn = List + "constructor" + |
0 | 14 |
consts |
15 |
"@" :: "[i,i]=>i" (infixr 60) |
|
16 |
list_rec :: "[i, i, [i,i,i]=>i] => i" |
|
17 |
map :: "[i=>i, i] => i" |
|
18 |
length,rev :: "i=>i" |
|
19 |
flat :: "i=>i" |
|
20 |
list_add :: "i=>i" |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset
|
21 |
hd,tl :: "i=>i" |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset
|
22 |
drop :: "[i,i]=>i" |
0 | 23 |
|
24 |
(* List Enumeration *) |
|
25 |
"[]" :: "i" ("[]") |
|
43 | 26 |
"@List" :: "is => i" ("[(_)]") |
0 | 27 |
|
28 |
||
29 |
translations |
|
30 |
"[x, xs]" == "Cons(x, [xs])" |
|
31 |
"[x]" == "Cons(x, [])" |
|
32 |
"[]" == "Nil" |
|
33 |
||
34 |
||
35 |
rules |
|
15
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset
|
36 |
|
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset
|
37 |
hd_def "hd(l) == list_case(0, %x xs.x, l)" |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset
|
38 |
tl_def "tl(l) == list_case(Nil, %x xs.xs, l)" |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset
|
39 |
drop_def "drop(i,l) == rec(i, l, %j r. tl(r))" |
6c6d2f6e3185
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset
|
40 |
|
0 | 41 |
list_rec_def |
42 |
"list_rec(l,c,h) == Vrec(l, %l g.list_case(c, %x xs. h(x, xs, g`xs), l))" |
|
43 |
||
44 |
map_def "map(f,l) == list_rec(l, Nil, %x xs r. Cons(f(x), r))" |
|
45 |
length_def "length(l) == list_rec(l, 0, %x xs r. succ(r))" |
|
46 |
app_def "xs@ys == list_rec(xs, ys, %x xs r. Cons(x,r))" |
|
47 |
rev_def "rev(l) == list_rec(l, Nil, %x xs r. r @ [x])" |
|
48 |
flat_def "flat(ls) == list_rec(ls, Nil, %l ls r. l @ r)" |
|
49 |
list_add_def "list_add(l) == list_rec(l, 0, %x xs r. x#+r)" |
|
50 |
end |