Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] a lemma for List

Email Gateway (Sep 06 2021 at 08:17):

From: Stepan Holub <holub@karlin.mff.cuni.cz>
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

Email Gateway (Sep 07 2021 at 16:01):

From: Tobias Nipkow <nipkow@in.tum.de>
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.

Tobias
smime.p7s

Last updated: Jan 04 2025 at 20:18 UTC