Re: [isabelle] a lemma for List

Thanks for the suggestion. However, when I asked sledgehammer (what would I do without it???), it came up with the following proof:

by (simp add: assms take_Suc_conv_app_nth)

This is too simple to warrant adding the lemma.


On 06/09/2021 10:16, Stepan Holub wrote:
Hello, maybe,


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


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

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