Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] [Isabelle2016-1-RC2] Proof outlines for induct...

Email Gateway (Aug 22 2022 at 14:37):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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

Email Gateway (Aug 22 2022 at 14:46):

From: Makarius <makarius@sketis.net>
I have not been aware of this particular problem, only of the general
observation that this new feature is somehow heuristic / partial. I will
improve on that eventually, but not for this release.

Makarius

Last updated: Apr 19 2024 at 01:05 UTC