Re: [isabelle] thus, hence
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] thus, hence
- From: Tobias Nipkow <nipkow at in.tum.de>
- Date: Fri, 19 Oct 2012 07:29:55 +0200
- In-reply-to: <5080A942.firstname.lastname@example.org>
- References: <CAHPz_MptGHQPi+5mtx+OeZSBuR=2yzib5mZMH1sZJuqV5NFZJw@mail.gmail.com> <CAAPnxw0bFKyUcf_puXQO+gPLHrsqVHFfqhyOTGxF=G5i22xHTQ@mail.gmail.com> <alpine.LNX.email@example.com> <5080A942.firstname.lastname@example.org>
- User-agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:16.0) Gecko/20121010 Thunderbird/16.0.1
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 ;-)
This archive was generated by a fusion of
Pipermail (Mailman edition) and