# [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.*