Re: [isabelle] List.nth_drop

I incorporated your suggestion of weaking the assumption to "n <= length xs". As a result a handful of proofs in the AFP broke and became simpler, as one would hope.

Thank you

On 01/10/2017 22:45, Fabian Hellauer wrote:

I think I found a useful generalisation of List.nth_drop :

lemma nth_drop':
 Â "n <= length xs ==> drop n xs ! i = xs!(n + i)"
apply (induct n arbitrary: xs, auto)
 Âapply (case_tac xs, auto)

lemma nth_drop [simp]:
 Â "n + i <= length xs ==> drop n xs !i = xs!(n + i)"
 Â by (simp add: nth_drop')

...unless maybe the intention of the strict precondition is that one "gets stuck" early

when trying to prove something about too large indices? In that case, it is not strict enough:

thm nth_drop[of "length xs" 0 xs]

is a statement about element 0 of an empty list.

Putting a "<" in the precondition would fix that, I think.



Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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