Email Gateway (Oct 29 2022 at 13:22): Email Gateway (Oct 29 2022 at 13:22):From: Asta Halkjær From <andro.from@gmail.com>
Hi,
The following outline of a proof works for me, but is silly:
proof (induct p arbitrary: i rule: wf_induct[where r=‹measure size›])
case 1
then show ?case ..
next
case (2 x)
then show ?case
using LEMMA[of i x] by (cases x) auto
qed
It is silly, because I do not actually need wellformed induction to prove
the lemma. Structural induction would work fine.
What greatly shortens the proof, however, is that rule: wf_induct...
enables the line using LEMMA[of i x] by (cases x) auto.
With structural induction, it seems that I would have to write out all the
cases to be able to do a similar instantiation of LEMMA (without which the
automation is not powerful enough).
That is, I want to avoid doing something like this with many cases:
proof (induct p arbitrary: i)
case (1 a)
then show ?case
using LEMMA[of i ‹1 a›] by auto
next
case (2 b c)
then show ?case
using LEMMA[of i ‹2 b c›] by auto
next
etc.
What is the best way to do this?
Best,
Asta
Last updated: Nov 04 2025 at 12:49 UTC