Next: List Basics Up: List Previous: List

## List Definitions

The basic file contains the definition of list and the usual elimination, reduction, iteration and double elimination rules plus the characterisation theorems.

``` ** Module lib_list Imports lib_eq_basics
\$list : (Type)->Type(list)
\$nil : {t:Type}list t
\$cons1 : {t:Type}t->(list t)->list t
\$list_elim :
{t:Type}{C_list:(list t)->Type}(C_list (nil t))->
({x1:t}{x2:list t}(C_list x2)->C_list (cons1 t x1 x2))->{z:list t}
C_list z
[[t:Type][C_list:(list t)->Type][f_nil:C_list (nil t)]
[f_cons1:{x1:t}{x2:list t}(C_list x2)->C_list (cons1 t x1 x2)][x1:t]
[x2:list t]
list_elim t C_list f_nil f_cons1 (nil t)  ==>  f_nil
|| list_elim t C_list f_nil f_cons1 (cons1 t x1 x2)  ==>
f_cons1 x1 x2 (list_elim t C_list f_nil f_cons1 x2)]

cons = ... : {t|Type}t->(list t)->list t
list_rec = ... : {s|Type}{t|Type}t->(s->(list s)->t->t)->(list s)->t
list_iter = ... : {s|Type}{t|Type}t->(s->t->t)->(list s)->t
list_ind = ... :
{s|Type}{P:(list s)->Prop}(P (nil s))->
({x:s}{l:list s}(P l)->P (cons x l))->{l:list s}P l
list_double_elim = ... :
{s|Type}{T:(list s)->(list s)->Type}(T (nil s) (nil s))->
({x:s}{l:list s}(T (nil s) l)->T (nil s) (cons x l))->
({x:s}{l:list s}({l':list s}T l l')->T (cons x l) (nil s))->
({x:s}{l:list s}({l':list s}T l l')->{y:s}{l':list s}
(T (cons x l) l')->T (cons x l) (cons y l'))->{l,l':list s}T l l'
is_nil = ... : {t|Type}(list t)->Prop
is_cons = ... : {t|Type}(list t)->Prop
nil_or_cons = ... : {t|Type}{l:list t}or (is_nil l) (is_cons l)
nil_not_cons = ... :
{t|Type}{l:list t}{x:t}not (Eq (nil t) (cons x l))```

Lego
Fri May 24 19:01:27 BST 1996