From: Jakub Kądziołka <email@example.com>
I was surprised to learn that nothing like the following elimination
rule is present in Main:
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
From: Manuel Eberl <firstname.lastname@example.org>
length_Suc_conv works pretty well as a simp rule.
From: Tobias Nipkow <email@example.com>
Rewriting with length_Suc_conv does the job for me
Last updated: Sep 25 2021 at 09:17 UTC