# [isabelle] resend question about structured induction

```Sorry for just sending an incomplete message.

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

I want to know how to avoid this duplication.  I have the common example

lemma
assumes h:"inductiveR x" and j:"P x"
shows "Q1 x" and "Q2 x"
using h proof (induct)
(case ...) case 1 have "P x0" by fact show "Q1 x0" ...
case 2 have "P x0" by fact show "Q2 x0" ...

I want to eliminate the duplication in the last two lines.

In fact, playing with examples shows that

lemma
assumes h:"inductiveR x" and j:"P x"
shows "Q1 x" and "Q2 x"
using h proof (induct)
(case ...x0...)                  (** the fact "P x0" is not known here **)
case 1 have j:"P x0" by fact
show "Q1 x0" proof (... j ...)
case 2 show "Q2 x0" proof (... j ...)  (** why is j in scope here? **)

works.  I don't understand the scoping of facts in this example.

Thanks,
Randy

```

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