next up previous contents
Next: Membership Up: List Previous: Lists and products

The Relation Adjoin

Intuitively, Adjoin a k l holds if it is possible to insert the element a in the list k and obtain the list l. 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 :
    {s|Type}{C_Adjoin:s->(list s)->(list s)->Prop}
    ({a:s}{xs:list s}C_Adjoin a xs (cons a xs))->
    ({xs|list s}{a|s}{axs|list s}(Adjoin a xs axs)->{b:s}
     (C_Adjoin a xs axs)->C_Adjoin a (cons b xs) (cons b axs))->{x1|s}
    {x2,x3|list s}(Adjoin x1 x2 x3)->C_Adjoin x1 x2 x3
[[s|Type][C_Adjoin:s->(list s)->(list s)->Prop]
 [f_ad1:{a1:s}{xs1:list s}C_Adjoin a1 xs1 (cons a1 xs1)]
 [f_ad2:{xs|list s}{a|s}{axs|list s}(Adjoin a xs axs)->{b:s}
  (C_Adjoin a xs axs)->C_Adjoin a (cons b xs) (cons b axs)][a1:s]
 [xs1:list s][xs|list s][a|s][axs|list s][x1:Adjoin a xs axs][b:s]
    Adjoin_elim C_Adjoin f_ad1 f_ad2 (ad1 a1 xs1)  ==>  f_ad1 a1 xs1
 || Adjoin_elim C_Adjoin f_ad1 f_ad2 (ad2 x1 b)  ==>
    f_ad2 x1 b (Adjoin_elim C_Adjoin f_ad1 f_ad2 x1)]

  Adjoin_inv = ... :
    {s|Type}{a|s}{xs,ys|list s}(Adjoin a xs ys)->
    (Eq ys (cons a xs) \/
     Ex ([xs':list s]
         Ex ([ys':list s]
             Ex ([c:s]
                 (Eq xs (cons c xs') /\ 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)->
    (Eq ys (cons a (cons b xs)) \/
     Ex ([ys':list s](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))->
    ((Eq a b /\ Eq xs ys) \/
     Ex ([xs':list s](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](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](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)->
    ((Eq us xs /\ Eq b a) \/
     Ex ([zs:list s](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
1998-06-15