    Next: Membership Up: List Previous: Lists and products

## The Relation Adjoin

This file defines the relation Adjoin over lists and proves some of its properties. This relation can be used to define permutations, as seen below.

``` ** Module lib_list_Adjoin Imports lib_list_length
Adjoin = ... : {s|Type}s->(list s)->(list s)->Prop
ad1 = ... : {s|Type}{a:s}{xs:list s}Adjoin a xs (cons a xs)
ad2 = ... :
{s|Type}{xs|list s}{a|s}{axs|list s}(Adjoin a xs axs)->{b:s}
Adjoin a (cons b xs) (cons b axs)
Adjoin_elim_nondep = ... :
{s|Type}{T:s->(list s)->(list s)->Prop}
({a:s}{xs:list s}T a xs (cons a xs))->
({xs|list s}{a|s}{axs|list s}(Adjoin a xs axs)->(T a xs axs)->{b:s}
T a (cons b xs) (cons b axs))->{a|s}{xs,ys|list s}
(Adjoin a xs ys)->T a xs ys
Adjoin_inv = ... :
{s|Type}{a|s}{xs,ys|list s}(Adjoin a xs ys)->
or (Eq ys (cons a xs))
(Ex ([xs':list s]
Ex ([ys':list s]
Ex ([c:s]
and (Eq xs (cons c xs'))
(and (Eq ys (cons c ys')) (Adjoin a xs' ys')))))
)
Adjoin_inv_corr1 = ... :
{s|Type}{a,b|s}{xs,ys|list s}(Adjoin a (cons b xs) ys)->
or (Eq ys (cons a (cons b xs)))
(Ex ([ys':list s]and (Eq ys (cons b ys')) (Adjoin a xs ys')))
Adjoin_inv_corr2 = ... :
{s|Type}{a,b|s}{xs,ys|list s}(Adjoin a xs (cons b ys))->
or (and (Eq a b) (Eq xs ys))
(Ex ([xs':list s]and (Eq xs (cons b xs')) (Adjoin a xs' ys)))
Adjoin_inv_corr3 = ... :
{s|Type}{a|s}{xs|list s}(Adjoin a (nil s) xs)->
Eq xs (cons a (nil s))
Adjoin_inv_corr4 = ... :
{s|Type}{a|s}{xs|list s}not (Adjoin a xs (nil s))
Adjoin_inv_corr5 = ... :
{s|Type}{a|s}{xs|list s}(Adjoin a xs (cons a (nil s)))->
Eq xs (nil s)
Adjoin_com1 = ... :
{s|Type}{a,b|s}{xs,us,ys|list s}(Adjoin a xs ys)->(Adjoin b ys us)->
Ex ([zs:list s]and (Adjoin b xs zs) (Adjoin a zs us))
Adjoin_com2 = ... :
{s|Type}{a,b|s}{xs,us,zs|list s}(Adjoin b zs xs)->(Adjoin a zs us)->
Ex ([ys:list s]and (Adjoin a xs ys) (Adjoin b us ys))
Adjoin_com3 = ... :
{s|Type}{a,b|s}{xs,us,ys|list s}(Adjoin a xs ys)->(Adjoin b us ys)->
or (and (Eq us xs) (Eq b a))
(Ex ([zs:list s]and (Adjoin b zs xs) (Adjoin a zs us)))
Adjoin_length_suc = ... :
{s|Type}{a|s}{l,al|list s}(Adjoin a l al)->
Eq (length al) (suc (length l))```

Lego
Fri May 24 19:01:27 BST 1996