[isabelle] [Isabelle2016-1-RC2] Proof outlines for induction proofs with several simultaneous goals



Dear Makarius,

Thanks for implementing proof outlines in Isabelle2016-1-RC2. I really find them useful. Unfortunately, they are not yet right for induction proofs with several goals. Here's a small example:

lemma
  fixes xs :: "'a list"
  shows "xs = xs" "xs @ xs = xs @ xs"
proof(induction xs)

The suggested proof outline is

  case Nil
  then show ?thesis sorry
next
  case (Cons a xs)
  then show ?thesis sorry
qed


There are two things wrong here. First, ?thesis is not a term abbreviation in the induction proof, so I get a corresponding error there. Second, the sub-cases are missing.

I would have expected an outline like the following:

  case Nil
  { case 1
    then show ?case sorry
  next
    case 2
    then show ?case sorry
  }
next
  case (Cons a xs)
  { case 1
    then show ?case sorry
  next
    case 2
    then show ?case sorry
  }
qed

Are you aware of the problem?

Best,
Andreas




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