Re: [isabelle] thus, hence



Am 19/10/2012 03:13, schrieb Christian Sternagel:
>> Note that the abbreviations "thus == then show" and "hence == then have"
>> are merely historical accidents.  They require fewer bytes in memory,
>> but more typing by the user and more explanations to newcomers.  The
>> reason is that the chaining or not chaining for elementary 'show' and
>> 'have' elements are often changed during the proof development.  And
>> there are further combinators like 'also' and 'moreover' that can be
>> combined with 'have' or 'show', and other goal elements like 'obtain'
>> that can participate in the chaining of facts in the same manner.
>>
>> So there is a large combinatorial space of
>>
>>    (then | from | with | ... | also | finally | moreover | ultimately)
>>      (have | show | obtain | interpret ...)
>>
>> which is better spelled out as such explicitly, without the somewhat
>> pointless shortcuts 'hence' and 'thus' getting in the way.
> I figure you thus (sorry) discourage the usage of "hence" and "thus". I have
> often wondered myself whether I should use those idioms or not. Currently I do,
> but especially your point about "chaining or not chaining" is very true and
> hence (sorry again) "hence" and "thus" almost always cause more typing than they
> save. I guess it is a reasonable convention to not use them in your proves?

Just as reasonable as using them - it's a pro-choice system ;-)

Tobias

> cheers
> 
> chris





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