[isabelle] thus, hence (was: Eliminating two quantifiers in structural proof)



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?

cheers

chris





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