[isabelle] a lemma for List



Hello, maybe,

List.hd_drop_conv_nth

could be complemented with

lemma last_take_conv_nth: assumes "n < length xs" shows "last (take (Suc n) xs) = xs!n"

a possible proof:
  using last_conv_nth[of "take (Suc n) xs"] assms
  unfolding min_absorb2[OF Suc_leI[OF assms], folded length_take] diff_Suc_1
            nth_take[OF lessI, of _ xs, symmetric] by force

Stepan

--
Tento e-mail byl zkontrolován na viry programem AVG.
http://www.avg.cz





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