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 


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
