Re: [isabelle] remdups_adj crucial lemma



Dear all,

> It seems to me that we need an abstract nonrecursive characterisation of
> remdups_adj from which specific lemmas follow easily. Is the following correct?
> 
> remdups_adj xs = ys <->
> EX f::nat => nat. mono f & f ` {0 ..< size xs} = {0 ..< size ys}
>  & (ALL i < size xs. xs!i = ys!(f i)
>       & (xs!i = xs!(i+1) <-> f i = f(i+1)))
> It should be sound (-->), but is it complete (<--)?

At least there needs to be one more implication added, since
otherwise the reference to xs!(i+1) is critical.

remdups_adj xs = ys <->
EX f::nat => nat. mono f & f ` {0 ..< size xs} = {0 ..< size ys}
 & (ALL i < size xs. xs!i = ys!(f i)
      & (i + 1 < size xs --> (xs!i = xs!(i+1) <-> f i = f(i+1))))

Otherwise, it looks good (soundness and completeness can easily be proven
for lists upto length 1, but the inductive case became quite tedious in my proof attempt)

René



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.