Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] elimination rule for length s = Suc n

view this post on Zulip Email Gateway (May 17 2021 at 14:42):

From: Jakub Kądziołka <kuba@kadziolka.net>
Dear all,

I was surprised to learn that nothing like the following elimination
rule is present in Main:

lemma length_Suc_elim[elim!]:
assumes "length s = Suc n"
assumes "⋀a s'. length s' = n ⟹ P (a # s')"
shows "P s"
apply (cases s)
using assms by auto

What's the usual way of eliminating an assumption like "length s = Suc
n"?

Regards,
Jakub Kądziołka

view this post on Zulip Email Gateway (May 17 2021 at 15:46):

From: Manuel Eberl <eberlm@in.tum.de>
length_Suc_conv works pretty well as a simp rule.

Manuel
smime.p7s

view this post on Zulip Email Gateway (May 17 2021 at 15:49):

From: Tobias Nipkow <nipkow@in.tum.de>
Rewriting with length_Suc_conv does the job for me

Tobias
smime.p7s

Last updated: Jan 04 2025 at 20:18 UTC