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 |
|
13 ListFn = List + "constructor" + |
|
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" |
|
21 hd,tl :: "i=>i" |
|
22 drop :: "[i,i]=>i" |
|
23 |
|
24 (* List Enumeration *) |
|
25 "[]" :: "i" ("[]") |
|
26 "@List" :: "is => i" ("[(_)]") |
|
27 |
|
28 |
|
29 translations |
|
30 "[x, xs]" == "Cons(x, [xs])" |
|
31 "[x]" == "Cons(x, [])" |
|
32 "[]" == "Nil" |
|
33 |
|
34 |
|
35 rules |
|
36 |
|
37 hd_def "hd(l) == list_case(0, %x xs.x, l)" |
|
38 tl_def "tl(l) == list_case(Nil, %x xs.xs, l)" |
|
39 drop_def "drop(i,l) == rec(i, l, %j r. tl(r))" |
|
40 |
|
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 |
|