[isabelle-dev] Converting existing proofs from apply-style to "structured" Isar-style
merelyapseudonym at gmail.com
Tue Sep 17 03:50:46 CEST 2013
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.
> 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?
> 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
> 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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev