[isabelle] thus, hence (was: Eliminating two quantifiers in structural proof)
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: [isabelle] thus, hence (was: Eliminating two quantifiers in structural proof)
- From: Christian Sternagel <c-sterna at jaist.ac.jp>
- Date: Fri, 19 Oct 2012 10:13:38 +0900
- In-reply-to: <alpine.LNX.email@example.com>
- References: <CAHPz_MptGHQPi+5mtx+OeZSBuR=2yzib5mZMH1sZJuqV5NFZJw@mail.gmail.com> <CAAPnxw0bFKyUcf_puXQO+gPLHrsqVHFfqhyOTGxF=G5i22xHTQ@mail.gmail.com> <alpine.LNX.firstname.lastname@example.org>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:16.0) Gecko/20121009 Thunderbird/16.0
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?
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and