[isabelle-dev] Converting existing proofs from apply-style to "structured" Isar-style
merelyapseudonym at gmail.com
Tue Sep 17 04:03:29 CEST 2013
On Wed, Jul 31, 2013 at 9:55 AM, Makarius <makarius at sketis.net> wrote:
> 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.
That sounds perfectly reasonable. Should I share my changes by just
attaching patches the "broadcasting" emails?
> (Changes in main HOL are always critical, since almost everything else
> depends on it, also performance-wise.)
Interesting—I had assumed that changing the proof of a lemma and/or theorem
had no functional impact on the code once said lemma/theorem had been
verified. Am I incorrect about that? (If the explanation is complicated,
please don't feel obligated to go into complete detail. A one-word answer
will tell me all I probably *need* to know. Any further explanation would
just be to satisfy my beginner's curiosity)
>>> From what I've read in the documentation, structured Isar proofs are
>> preferred over apply-style proofs in every case except for
> 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
> 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
> 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.
I apologize if I brought up an already over-discussed topic. If I have any
further questions about "proof scripts" vs "proof documents", I'll begin in
the isabelle-users mailing list.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev