Re: [isabelle] Isabelle2016-1-RC3 available for testing: moreover then have



On 28/11/16 16:54, Bertram Felgenhauer via Cl-isabelle-users wrote:
> Dear Makarius,
> 
> Makarius wrote:
>> On 25/11/16 12:03, Christian Sternagel wrote:
>>>
>>> I use "moreover then have" a lot (mostly as the first "moreover"-step).
>>> But in the RC "then" is highlighted in red, which tells me that I
>>> shouldn't do this. Why?
>>
>> Conceptually, Isar has a primary thread of facts called "this" and a
>> secondary one called "calculation". There are certain policies how
>> "this" vs. "calculation" are updated, going back to my PhD thesis,
>> various papers, and the official isar-ref manual.
> 
> None of the above (nor the remainder of your email) explains what is
> wrong with "moreover then have". As I understand it, "moreover" updates
> the calculation, and "then" chains the same fact into the next goal.
> This is useful. Which principle is violated here?

When the calculational elements were introduced in Isar around
1999/2000, there was certain explicit structure to make sure that the
use of "this" for "calculation" resets the former. This structure was
lost in a later (undocumented) experiment. The highlighting as
"improper" reverses that to some extent, although it would have been
better to remove that feature altogether.

What is particularly bad about "moreover then have" is the implicit fork
of the flow of facts. I find it very hard to read and maintain such
proofs, so they are now formally marked as non-Isar. (The old experiment
to allow that intermittendly was based on the claim "Isar allows
arbitrarily bad proofs anyway".)


Isar is generally based on the principle "structure emerges from taking
arbitrariness away". The brush-up of Isar 2016 was a good opportunity to
emphasize this principle again (and more).

As usual, it might require some efforts to discontinue old habits, but
the Isar 2016 style as a whole leads to better structured and more
concise proofs in all examples that I have cleaned up recently.


It might actually help to proceed under the assumption that Isar 2016 is
a new proof language for Isabelle, not just 10-20 small add-ons and
reforms to the old one.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.