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))