author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 124  858ab9a9b047 
permissions  rwrr 
0  1 
(* Title: ZF/listfn 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1993 University of Cambridge 

5 

6 
Functions for Lists in ZermeloFraenkel Set Theory 

7 

8 
map is a binding operator  it applies to metalevel functions, not 

9 
objectlevel 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" 

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

21 
hd,tl :: "i=>i" 
1c0926788772
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 

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset

36 

1c0926788772
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)" 
1c0926788772
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)" 
1c0926788772
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))" 
1c0926788772
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 