Re: [isabelle] remdups_adj crucial lemma



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

Tobias

On 25/08/2014 17:10, Jakob von Raumer wrote:
> Wow, thank you! I really have to learn to search for short proofs (or in this
> case, remember to use the right induction lemmas). Another lemma, which is
> useful for working not with inductively defined lists but by indexing lists is
> the following: Adjacencies are preserved by remdups_adj in the sense that for
> each index in the reduced list there's an index in the original list so that the
> list entries coincide at this entry and their respective successors:
> https://gist.github.com/javra/11b9a6770cab2e17559d (I could work on a shorter
> proof the next days).
> 
> Best regards
> Jakob
> 
> 
> 2014-08-25 16:07 GMT+02:00 Tobias Nipkow <nipkow at in.tum.de
> <mailto:nipkow at in.tum.de>>:
> 
>     Important lemma. I have just added a more succinct proof of it due to Manuel
>     Eberl http://shodan.linuxd.org/paste/oyIsOBq1 to List.thy.
> 
>     Thanks to both of you!
>     Tobias
> 
>     On 23/08/2014 12:19, Jakob von Raumer wrote:
>     > Hello everyone,
>     >
>     > am I just bad at using find_theorems or is there no lemma that remdups_adj
>     > really yields lists with no adjacent entries being equal? If it's really
>     > missing, here's my somewhat lengthy proof:
>     > https://gist.github.com/javra/68c7f852a060d7cb6036
>     >
>     > Best regards
>     > Jakob
>     >
> 
> 




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