Re: [isabelle] On the status of occurrences of variables with identical names/indexnames and different types in the same context/theorem/term



As a general rule, style is a matter of choice. This particular issue does not seem to arise frequently in practice. It is more common in the HOL world, but even there it doesn’t appear to be a source of controversy.

Larry Paulson 

> On 23 Jul 2019, at 21:59, mailing-list anonymous <mailing.list.anonymous at gmail.com> wrote:
> 
> Dear Lawrence Paulson/All,
> 
> Thank you for your reply.
> 
> I believe that it would be useful to explain what you stated in your email
> in the implementation manual. Of course, while it is difficult/impossible
> to introduce new theorems that use variables with the same name and
> different types using Isar commands only, it is very easy to do so via the
> public ML interface, even by mistake. Unless I have missed something, this
> issue does not seem to be covered at all (I believe that the manual merely
> states that the type inference mechanism rejects such cases). Given that
> using the variables with the same name and different types is considered to
> be a 'terrible' style, it makes me wonder why the public ML interface
> permits it at all... are there any use cases or any plans to exploit this
> feature of the logic in the future?
> 
> Thank you
> 
> 
> 
> 
> 
> 
> On Tue, Jul 23, 2019 at 1:06 PM Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> 
>>> On 18 Jul 2019, at 00:11, mailing-list anonymous <
>> mailing.list.anonymous at gmail.com> wrote:
>>> 
>>> More specifically, I have the following questions, the second being of
>>> certain practical significance:
>> 
>>> 1. Is introducing theorems that use differing types for variables with
>> the
>>> identical names/indexnames is considered to be a bad style, is it
>>> completely illegal or, perhaps, it is actively exploited by user packages
>>> that I am not aware of?
>> 
>> I think it’s terrible style, and as your example shows, you have to work
>> quite hard to accomplish this.
>> 
>>> 2. Is it acceptable for the user packages to assume that all variables in
>>> the theorems that they receive as inputs from the users do not have any
>>> occurrences of variables with the identical names/indexnames and
>> different
>>> types?
>> 
>> I think so.
>> 
>> Larry
> 
> 
> 
> -- 
> Please accept my apologies for posting anonymously. This is done to protect
> my privacy. I can make my identity and my real contact details available
> upon request in private communication under the condition that they are not
> to be mentioned on the mailing list.





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