Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Instantiating a lemma with each case of an ind...


view this post on Zulip 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: Mar 29 2024 at 08:18 UTC