# Re: [isabelle] structured induction

On Sun, May 15, 2011 at 2:56 PM, Randy Pollack <rpollack at inf.ed.ac.uk> wrote:
> In the following example (taken from
> ~~/src/HOL/Induct/Common_Patterns.thy) there is apparently unnecessary
> duplication.
>
> lemma
> fixes n :: nat
> shows "P n" and "Q n"
> proof (induct n)
> case 0 case 1
> show "P 0" sorry
> next
> case 0 case 2
> show "Q 0" sorry
> next
> case (Suc n) case 1
> note hyps = `P n` `Q n` (**** this line ... ****)
> show "P (Suc n)" sorry
> next
> case (Suc n) case 2
> note hyps = `P n` `Q n` (**** ... duplicated ***)
> show "Q (Suc n)" sorry
> qed
Hi Randy,
It is the "next" command that removes the local definition of "hyps"
from scope. Maybe you could try something like this:
lemma
fixes n :: nat
shows "P n" and "Q n"
proof (induct n)
case 0
case 1
show "P 0" sorry
case 2
show "Q 0" sorry
next
case (Suc n)
note hyps = `P n` `Q n`
case 1
show "P (Suc n)" using hyps sorry
case 2
show "Q (Suc n)" using hyps sorry
qed
>
> I want to know how to avoid this duplication. Even more, I have the
> common example
>
> lemma
> assumes h:"inductiveR x"
> and
It looks like the rest of your question was cut off. Could you resend it?
- Brian

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*