I think I found a useful generalisation of List.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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and