[isabelle-dev] Shadowing of theorem names in locales

[Clemens Ballarin]

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

Clemens


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?
>
> Cheers,
> 	Florian
>
> --
>
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>