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