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

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> wrote:

> > On 18 Jul 2019, at 00:11, mailing-list anonymous <
> mailing.list.anonymous at> 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.