Re: [isabelle] Proof state in Isar proof style are difficult to follow

On Wed, 22 Mar 2006, ehmety at 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 that 
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 MHonArc.