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

From: Manuel Eberl <eberlm@in.tum.de>

length_Suc_conv works pretty well as a simp rule.

Manuel

smime.p7s

From: Tobias Nipkow <nipkow@in.tum.de>

Rewriting with length_Suc_conv does the job for me

Tobias

smime.p7s

Last updated: Sep 25 2021 at 09:17 UTC