This file defines some basic list functions--where basic really just means pure list functions which do not require any other datatype. These functions include a head function--hd which takes an extra argument which is the value returned for a empty list, tail, fold, append, map and reverse. Some theorems about these functions are also given (but not enough).
** Module lib_list_basics Imports lib_list singleton = ... : {t|Type}t->list t hd = ... : {t|Type}t->(list t)->t tail = ... : {t|Type}(list t)->list t fold = ... : {s|Type}{t|Type}(t->s->t)->t->(list s)->t foldright = ... : {B|Type}{A|Type}(A->B->B)->(list A)->B->B foldleft = ... : {B|Type}{A|Type}(A->B->B)->(list A)->B->B map = ... : {s|Type}{t|Type}(s->t)->(list s)->list t append = ... : {t|Type}(list t)->(list t)->list t tack = ... : {t|Type}t->(list t)->list t reverse = ... : {t|Type}(list t)->list t flatten = ... : {t|Type}(list (list t))->list t cons_injective = ... : {t|Type}{k,l|list t}{x,y|t}(Eq (cons x k) (cons y l))-> Eq (tail (cons x k)) (tail (cons y l)) cons_inj = ... : {s|Type}{a,b|s}{xs,ys|list s}(Eq (cons a xs) (cons b ys))-> (Eq a b /\ Eq xs ys) l_not_cons_l = ... : {t|Type}{l:list t}{x:t}not (Eq l (cons x l)) append_cons = ... : {t|Type}{k,l:list t}{x:t} Ex2 ([y:t][j:list t]Eq (append k (cons x l)) (cons y j)) nil_not_append_cons = ... : {t|Type}{x:t}{k,l:list t}not (Eq (nil t) (append k (cons x l))) append_assoc = ... : {t|Type}{j,k,l:list t} Eq (append j (append k l)) (append (append j k) l) append_nil = ... : {t|Type}{l:list t}Eq (append l (nil t)) l append_reverse = ... : {t|Type}{l,m:list t} Eq (reverse (append l m)) (append (reverse m) (reverse l)) append_strict = ... : {t|Type}{k,l:list t}(Eq (append k l) (nil t))-> (Eq k (nil t) /\ Eq l (nil t)) double_reverse_is_identity = ... : {t|Type}{l:list t}Eq (reverse (reverse l)) l foldright_append_lem = ... : {s|Type}{t|Type}{g:s->t->t}{G,H:list s}{b:t} Eq (foldright g (append G H) b) (foldright g G (foldright g H b)) foldleft_append_lem = ... : {s|Type}{t|Type}{g:s->t->t}{G,H:list s}{b:t} Eq (foldleft g (append G H) b) (foldleft g H (foldleft g G b))