[isabelle] structured induction



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.  Even more, I have the
common example

lemma
assumes h:"inductiveR x"
and





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