[isabelle-dev] Shadowing of theorem names in locales
ballarin at in.tum.de
Mon Oct 8 20:13:55 CEST 2012
Name bindings in locales should be treated uniformly regardless of the
background theory the locale happens to be in, so this can be
considered a defect in the implementation. My guess is that this is
caused by the full internal name containing theory information.
Otherwise I would expect the local theory active at the point of
declaration of the second theorem to reject binding the duplicate name.
On the other hand, if theory information is not stored in the internal
name, theory merges can result in invalid locales (that is, locales
that cannot even be activated, leaving alone interpreted).
Quoting Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:
> Hi all,
> currently, theorem names in locales can be shadowed (given that
> declarations are in different theories, otherwise the foundation level
> would reject the declaration since the two foundation theorems would
> have the same name).
> After some pondering I would argue that this should be forbidden:
> * (Complete) shadowing is a constant source of confusion.
> * Global interpretations are impossible then, since they would result in
> two global theorems with the same name.
> Any comments?
> PGP available:
More information about the isabelle-dev