Re: [isabelle] Proof state in Isar proof style are difficult to follow
- To: ehmety at univ-nkc.mr
- Subject: Re: [isabelle] Proof state in Isar proof style are difficult to follow
- From: Makarius <makarius at sketis.net>
- Date: Thu, 6 Apr 2006 14:54:21 +0200 (CEST)
- Cc: isabelle-users at cl.cam.ac.uk
- In-reply-to: <email@example.com>
- References: <firstname.lastname@example.org> <email@example.com> <firstname.lastname@example.org>
On Wed, 22 Mar 2006, ehmety at univ-nkc.mr wrote:
> I was used to ML proof style and now I am trying to learn the isar mode.
> But I found it very hard to follow. I am not sure whether this is normal
> or I am missing something
It is indeed hard to convert oneself from tactical proving to structured
proof composition in Isar. Certain old habits need to be unlearned --
after being identified as such in the first place.
Most notably direct focus on goal states is superceded by building up a
local context of parameters, assumptions, facts etc. that is eventually
ready to solve a pending problem.
> This kind of displays confuses me.
This is a known problem of Isar. There are many ways to perform a proof
(both structured and unstructured) but different information is relevant
in different situations. The system does not impose a particular policy
here, but leaves it to the user to figure out relevant bits required to
proceed with the reasoning.
For beginners it is best to step through existing structured proof texts
without taking the state display too seriously. In fact, Isar proofs can
be easily maintained without looking at internal states at all. It is
still necessary for interactive development, though.
There is an interesting paper by Dixon and Fleuriot
boldly points out that proof state display should be suppressed
altogether, replacing it by a metaphor of editing the structured proof
text as a hierarchical outline that is completed incrementally.
This archive was generated by a fusion of
Pipermail (Mailman edition) and