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

[Makarius]

On Mon, 16 Sep 2013, Josh Tilles wrote:

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

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