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

[Josh Tilles]

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)

>
>
>
>  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.

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.

>
>
>
>         Makarius
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130916/a56d5c8e/attachment-0002.html>