[isabelle-dev] Shadowing of theorem names in locales

[Makarius]

On Wed, 10 Oct 2012, Makarius wrote:

> After some detours I am now back on Isabelle/28e37eab4e6f.
>
> So with the "ch-strict" changeset applied to the critical spot of local 
> notes, the namespace policy enforces the concentual locale scopes.
>
> Applying this in practice leads to many surprises about situations found in 
> existing theory libraries, though.  Some of the changsets leading up to 
> Isabelle/28e37eab4e6f already sort this out.  Some other ad-hoc changes are 
> attached as ch-test here.
>
>
> With Isabelle/28e37eab4e6f + ch-strict + ch-test and AFP/77f79b2076f1
> the following sessions fail:
>
> BDD, Dijkstra_Shortest_Path, Free-Groups, Group-Ring-Module, HOL-Algebra, 
> HOL-Number_Theory, HOL-ex, JinjaThreads, KBPs, Markov_Models, Ordinal, 
> Ordinary_Differential_Equations, Pi_Calculus, Presburger-Automata, 
> PseudoHoops, Psi_Calculi, Refine_Monadic, Simpl, Slicing, Topology, 
> Transitive-Closure-II, Valuation
>
> So the question if ch-strict can be activated soon is mainly a matter of 
> library space.  It is up to emerging volunteers to sort it out further.

What is the situation with this fine point of authentic local notes?  The 
general plan is to make Local_Theory.define/note more uniform in the name 
space treatment, which is conceptually part of the game already, but was 
not yet pushed through for various historical reasons.

Johannes has updated his sessions, but very little happened elsewhere.

Concerning accidental/unintended name clashes, the half-open question for 
me is, how to name sublocale ranges more systematically.  There might be 
some conventions known by locale experts that are worth sharing here.


 	Makarius