Re: [isabelle] remdups_adj crucial lemma



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

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