Re: [isabelle] remdups_adj crucial lemma



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).
Sometimes, I find working on shorter proofs a nice exercise to
understand the system and for getting more out of the automation.

Note that the "0 < length xs" assumption on your lemma is not needed (it
is already implied by "j + 1 < length xs").




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