[isabelle-dev] Converting existing proofs from apply-style to "structured" Isar-style

[Makarius]

On Tue, 30 Jul 2013, Josh Tilles wrote:

> QUESTION STATED BRIEFLY:
> If I convert existing proofs in src/HOL/**.thy from apply-style to
> Isar-style, would those changes be welcome in the main repository?

It depends which part of the repository are affected.  To get changes 
accepted, someone who is an "expert" on that area of sources needs to 
apply them.  Finding out works by broadcasting here on this mailing list. 
(Changes in main HOL are always critical, since almost everything else 
depends on it, also performance-wise.)


> EXPLANATION/DETAIL:
>> From what I've read in the documentation, structured Isar proofs are
> preferred over apply-style proofs in every case except for
> prototyping/experimentation.

Unstructured proof scripts (now called "apply style) and structured Isar 
proofs are historically, technically, conceptually somehow related, 
although in retrospect this is somehow accidental.  The Isabelle/Isar 
system was made in a way to include the old script style as "guest" to the 
new approach.  This worked so smoothly that people sometimes think that 
Isar is still about "proof scripts", but it is actually about "proof 
documents".

Moving back and forth between the two styles works for many Isabelle 
experts after some practice, although my impression in recent years is 
that it would be better to teach people just one style from the start, and 
not pretend that one is a prerequisite to the other.  (E.g. in 
Isabelle2013 'by' no longer needs to be broken up into 1-2 'apply' to 
diagnose its failure.)

There is a long story behind that, of how the system presents it by 
default and how the manuals are written.  And it is getting more and more 
off-topic for isabelle-dev, which is about the development process, and 
exploring / testing intermediate Isabelle snapshots between official 
releases -- i.e. the everyday struggles with ongoing changes, not a 
relaxed discussion about the big picture.


 	Makarius