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

[Josh Tilles]

On Tue, Jul 30, 2013 at 3:42 PM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:

> This could be a valuable service, especially for long lists of applys.
>
Thank you for the encouragement! I'm glad to see you agree.

> (A proof like "by (induct n) auto" should be left alone.)
>
Understood. If I come across proofs comprising only two `apply`s, should I
tweak them to use the briefer `by method1 method2` form? Or would that be
considered a pedantic waste of time?

>
> Do ask an experienced user to examine your early attempts for beginner's
> mistakes, like labelling all intermediate results.
>
Happy to oblige.

>
> Larry
>
> On 30 Jul 2013, at 18:40, Josh Tilles <merelyapseudonym at gmail.com> 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?
>
> 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. (please let me know if I'm wrong about this
> observation)
> If newcomers to Isabelle/HOL "refactor" the lemmas & theories that were
> written in the apply-style, presumably that frees the experienced
> developers to spend their time on more creative endeavors.
> *My* goals: I want to learn more about the conceptual organization of
> Isabelle/HOL; and I want to make more of the implementation code
> demonstrate idiomatic Isar, thus giving Isabelle beginners many more
> examples to read and learn from.
>
> --Josh
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130916/a4fdd2e2/attachment.html>