List Basics

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))