Next: Permutation Up: List Previous: Membership

## Distinctness

We defines the property Distin, that all the elements of a list are distinct. Like that of Adjoin, we use the impredicative definition and prove a an elimination rule.

``` ** Module lib_list_Distin Imports lib_list_Member lib_nat_Le
Distin = ... : {s|Type}(list s)->Prop
Dis1 = ... : {s|Type}Distin (nil s)
Dis2 = ... :
{s|Type}{a:s}{xs:list s}(not (Member a xs))->(Distin xs)->
Distin (cons a xs)
Dis_elim = ... :
{s|Type}{T:(list s)->Prop}(T (nil s))->
({a:s}{xs:list s}(not (Member a xs))->(T xs)->T (cons a xs))->
{xs:list s}(Distin xs)->T xs
Distin_inv = ... :
{s|Type}{a|s}{l|list s}(Distin (cons a l))->
and (not (Member a l)) (Distin l)
Distin_append = ... :
{s|Type}{l1,l2:list s}(Distin l1)->(Distin l2)->
({a:s}(Member a l1)->not (Member a l2))->Distin (append l1 l2)
Distin_inj_map = ... :
{s|Type}{u|Type}{l:list s}{f:s->u}
({a1,a2:s}(Member a1 l)->(Member a2 l)->(Eq (f a1) (f a2))->
Eq a1 a2)->(Distin l)->Distin (map f l)
Distin_prod = ... :
{s|Type}{u|Type}{l1:list s}{l2:list u}(Distin l1)->(Distin l2)->
Distin (prod_list l1 l2)
Distin_inj_build = ... :
{s|Type}{f:nat->s}{n:nat}
({k1,k2:nat}(Lt k1 n)->(Lt k2 n)->(Eq (f k1) (f k2))->Eq k1 k2)->
Distin (build_list f n)
Distin_sublist_Le_length = ... :
{s|Type}{xs,ys:list s}(Distin xs)->
({a:s}(Member a xs)->Member a ys)->Le (length xs) (length ys)```

Lego
Fri May 24 19:01:27 BST 1996