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