Email Gateway (Aug 22 2022 at 16:15): Email Gateway (Aug 22 2022 at 16:15):From: Fabian Hellauer <hellauer@in.tum.de>
Hello,
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)
done
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.
Cheers
Fabian
Email Gateway (Aug 22 2022 at 16:16):From: Tobias Nipkow <nipkow@in.tum.de>
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
Tobias
smime.p7s
Last updated: Apr 19 2024 at 12:27 UTC