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

Membership

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)) (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](Member a l /\ Eq (f a) b))
  Member_append = ... :
    {s|Type}{l1,l2:list s}{a:s}
    iff (Member a (append l1 l2)) (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))
     (Member (Fst p) l1 /\ Member (Snd p) l2)
  Member_build = ... :
    {s|Type}{f:nat->s}{n:nat}{a:s}
    iff (Member a (build_list f n)) (Ex ([k:nat](Lt k n /\ Eq (f k) a)))



Lego
1998-06-15