Re: [isabelle] Variables in locale assumptions



Thanks for the explanations. It seems wise to keep it the way it is.

All the best,
Stephan


________________________________________
From: cl-isabelle-users-bounces at lists.cam.ac.uk [cl-isabelle-users-bounces at lists.cam.ac.uk] on behalf of Makarius [makarius at sketis.net]
Sent: Monday, February 24, 2014 1:41 PM
To: Lawrence Paulson
Cc: Peter Lammich; cl-isabelle-users at lists.cam.ac.uk List
Subject: Re: [isabelle] Variables in locale assumptions

On Sat, 22 Feb 2014, Lawrence Paulson wrote:

> Clearly every instance of a variable in a single formula must have the
> same type, and it’s natural to expect that every instance in a list of
> formulas should also have the same type. The alternative would be very
> confusing for readers, also in informal mathematics.
>
> On 22 Feb 2014, at 09:47, Peter Lammich <lammich at in.tum.de> wrote:
>
>>
>>> It's this type constraint that surprised me. The post by Makarius
>>> explains it, but as a user I would prefer to have complete separation.
>>> Is there a compelling reason why it's implemented as it is?
>>>
>>
>> I frequently run into another instance of this problem, when writing
>> something like:
>>
>> lemma foo:
>>  "x & y --> x"
>>  "x = y --> f x = f y"
>>
>> Note that foo(2) is: "?x::bool = ?y ...", which is usually not
>> what was intended.

The observation by Larry is correct.  He probably still remembers the time
when type-inference would only range over each term separately, causing
many strange effects and surprises.

When you write a simultaneous statement as above, or a long statement with
fixes/assumes/shows, the scope of free variables and their types ranges
over the whole clause. This is the intended way -- we have required many
years to get there.


A slightly different situation occurs in conceptually separate scopes that
happen to be written with free variables that share the type-inference
scope, but are logically separate.  There are two main situations for
this: the 'obtains' statement with several disjuctive branches, and the
implicit quantification of locale expressions that were encountered here.
Here I would prefer to keep type-information separate, according to the
logical structure.

When I introduced the latter locale convenience about 12 years ago, I was
aware of the snag with type-inference, and also aware of the lack of any
systematic documentation of type-inference in the Isabelle manuals (even
until today). Approximately every 5 years some user stumbles over that
detail.  The manuals could be improved at some point, but it is probably
more helpful to give more feedback about scopes and type-inference errors
in the Prover IDE.


        Makarius




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