On Mon, 16 Sep 2013, Josh Tilles wrote:
On Tue, Jul 30, 2013 at 3:42 PM, Lawrence Paulson <[email protected]> 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?
Depends on the situation. Conceptually, the Isar 'by' command takes first
an "initial method" to split up the problem in a top-down manner (using
its facts that are passed to it), and second a "terminal method" to solve
what comes out of that.
This structured double-step is conceptually different from the sequential
composition of the two proof methods. (When facts are involved it is also
operationally different.) So when that was the real intention of the
proof author, even without knowing about such fine points, it is
appropriate to make just one Isar 'by' step from certain minimal apply
scripts. In other situations it is a lost cause -- no structure to be
recovered so easily.
After developing some routine with Isar, you should get an idea what to do
when. It requires some practice to develop proper style -- just line wine
tasting.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
