|
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 + |
|
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 |
|
22 (* List Enumeration *) |
|
23 "[]" :: "i" ("[]") |
|
24 "@List" :: "args => i" ("[(_)]") |
|
25 |
|
26 |
|
27 translations |
|
28 "[x, xs]" == "Cons(x, [xs])" |
|
29 "[x]" == "Cons(x, [])" |
|
30 "[]" == "Nil" |
|
31 |
|
32 |
|
33 rules |
|
34 list_rec_def |
|
35 "list_rec(l,c,h) == Vrec(l, %l g.list_case(c, %x xs. h(x, xs, g`xs), l))" |
|
36 |
|
37 map_def "map(f,l) == list_rec(l, Nil, %x xs r. Cons(f(x), r))" |
|
38 length_def "length(l) == list_rec(l, 0, %x xs r. succ(r))" |
|
39 app_def "xs@ys == list_rec(xs, ys, %x xs r. Cons(x,r))" |
|
40 rev_def "rev(l) == list_rec(l, Nil, %x xs r. r @ [x])" |
|
41 flat_def "flat(ls) == list_rec(ls, Nil, %l ls r. l @ r)" |
|
42 list_add_def "list_add(l) == list_rec(l, 0, %x xs r. x#+r)" |
|
43 |
|
44 end |