next up previous contents
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))

Fri May 24 19:01:27 BST 1996