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