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
"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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and