|
12197
|
1 |
(* Title: ZF/UNITY/ListPlus.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Sidi O Ehmety, Cambridge University Computer Laboratory
|
|
|
4 |
Copyright 2001 University of Cambridge
|
|
|
5 |
|
|
|
6 |
More about lists
|
|
|
7 |
|
|
|
8 |
*)
|
|
|
9 |
|
|
|
10 |
ListPlus = NatPlus +
|
|
|
11 |
|
|
|
12 |
constdefs
|
|
|
13 |
(* Function `take' returns the first n elements of a list *)
|
|
|
14 |
take :: [i,i]=>i
|
|
|
15 |
"take(n, as) == list_rec(lam n:nat. [],
|
|
|
16 |
%a l r. lam n:nat. nat_case([], %m. Cons(a, r`m), n), as)`n"
|
|
|
17 |
|
|
|
18 |
(* Function `nth' returns the (n+1)th element in a list (not defined at Nil) *)
|
|
|
19 |
|
|
|
20 |
nth :: [i, i]=>i
|
|
|
21 |
"nth(n, as) == list_rec(lam n:nat. 0,
|
|
|
22 |
%a l r. lam n:nat. nat_case(a, %m. r`m, n), as)`n"
|
|
|
23 |
|
|
|
24 |
end |