From: Lawrence Paulson <lp15@cam.ac.uk>
We use qualified names to disambiguate when the same identifier is used in multiple theories. But sometimes a slight change to the theory hierarchy causes a new name space to predominate, requiring substantial changes to qualify all the names that had referred to the other name space. In the case of datatype constructors, one can even have conflicting names within a single theory. Is there, or could there be, a way to set a default name space in a particular context?
Larry
From: Makarius <makarius@sketis.net>
On 13/10/2025 11:42, Lawrence Paulson wrote:
We use qualified names to disambiguate when the same identifier is used in
multiple theories. But sometimes a slight change to the theory hierarchy
causes a new name space to predominate, requiring substantial changes to
qualify all the names that had referred to the other name space. In the case
of datatype constructors, one can even have conflicting names within a single
theory. Is there, or could there be, a way to set a default name space in a
particular context?
I don't quite understand the phrase "set a default name space" in the context
of Isabelle. Is that a notion from different proof assistants (or programming
languages). Isabelle name spaces and access policies work quite differently
--- and not easily changed.
Further, the same principle applies as for performance tuning (last time with
classical.ML). We do need explicit empirical proof of actual problems, e.g. as
public entries in AFP. Odd applications that are nowhere visible are by
definition non-existant.
Very often, such applications can be done in a better way. There is even the
'alias' command for unusual situations.
Makarius
From: Manuel Eberl <manuel@pruvisto.org>
I think what Larry is referring to is that when the short name of a
constant or theorem (mostly it is constants that cause this problem) is
not unique then which constant you get when you type the short name is
somewhat unpredictable. Then you have to use the long, qualified name to
disambiguate.
This can be quite annoying when, during refactoring, you have to import
an additional theory and suddenly lots of constants get resolved
differently and you have to change every single occurrence to the new name.
The classic example that keeps bothering me is polynomials: there are
constants called "smult", "degree", etc. both for the univariate
polynomials in HOL-Computational_Algebra (arguably the most important
ones) and for multivariate polynomials (in the AFP entry of the same
name) and for the univariate polynomials in HOL-Algebra. If you do maths
in Isabelle/HOL, you will sooner or later end up transitively importing
HOL-Algebra, and suddenly "smult" is the "smult" from HOL-Algebra, which
is rarely the one you want since the HOL-Computational_Algebra
polynomials are used much more.
Thus, it would be nice to specify that "smult" should by default always
mean "Polynomial.smult" (the one from HOL-Computational_Algebra), either
globally or at least within some context.
I don't have any concrete occurrences of this, but if you search the AFP
for "Polynomial.smult" or "Polynomial.degree" there are hundreds of matches.
Cheers,
Manuel
On 13/10/2025 12:43, Makarius wrote:
On 13/10/2025 11:42, Lawrence Paulson wrote:
We use qualified names to disambiguate when the same identifier is
used in multiple theories. But sometimes a slight change to the
theory hierarchy causes a new name space to predominate, requiring
substantial changes to qualify all the names that had referred to the
other name space. In the case of datatype constructors, one can even
have conflicting names within a single theory. Is there, or could
there be, a way to set a default name space in a particular context?I don't quite understand the phrase "set a default name space" in the
context of Isabelle. Is that a notion from different proof assistants
(or programming languages). Isabelle name spaces and access policies
work quite differently --- and not easily changed.Further, the same principle applies as for performance tuning (last
time with classical.ML). We do need explicit empirical proof of actual
problems, e.g. as public entries in AFP. Odd applications that are
nowhere visible are by definition non-existant.Very often, such applications can be done in a better way. There is
even the 'alias' command for unusual situations.Makarius
Last updated: Oct 20 2025 at 16:27 UTC