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> 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.


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