next up previous contents
Next: Distinctness Up: List Previous: The Relation Adjoin


Using the relation Adjoin we define the membership relation between elements of some type and lists over that type.

 ** Module lib_list_Member Imports lib_list_Adjoin lib_list_prod
  Member = ... : {s|Type}s->(list s)->Prop
  not_Member_nil = ... : {s|Type}{a|s}not (Member a (nil s))
  Mem_ind = ... :
    {s|Type}{l|list s}{a,b|s}
    iff (Member b (cons a l)) (or (Member b l) (Eq a b))
  Member_Adjoin = ... :
    {s|Type}{l,al|list s}{a,b|s}(not (Eq a b))->(Adjoin a l al)->
    (Member b al)->Member b l
  Member_map = ... :
    {s|Type}{u|Type}{l:list s}{a:s}{f:s->u}(Member a l)->
    Member (f a) (map f l)
  Member_map_inv = ... :
    {s|Type}{u|Type}{l:list s}{b:u}{f:s->u}(Member b (map f l))->
    Ex ([a:s]and (Member a l) (Eq (f a) b))
  Member_append = ... :
    {s|Type}{l1,l2:list s}{a:s}
    iff (Member a (append l1 l2)) (or (Member a l1) (Member a l2))
  Member_prod = ... :
    {s|Type}{u|Type}{l1:list s}{l2:list u}{p:prod s u}
    iff (Member p (prod_list l1 l2))
        (and (Member (Fst p) l1) (Member (Snd p) l2))
  Member_build = ... :
    iff (Member a (build_list f n))
        (Ex ([k:nat]and (Lt k n) (Eq (f k) a)))

Fri May 24 19:01:27 BST 1996