[isabelle-dev] Shadowing of theorem names in locales

[Clemens Ballarin]

I recently tried to make HOL-Algebra compliant to this, but  
unfortunately got stuck in HOL already, where Big_Operators didn't  
comply either (but that's unlikely the only theory).

If we are serious about forbidding duplicate theorem names eventually  
we probably need to start by introducing a flag to enable/disable  
this, so that it doesn't get introduced by accident to theories where  
duplicate names had already been eliminated.  As other have noted  
before, this is not going to be a one-man effort.  It is quite a bit  
of work, but more importantly, it involves design decisions (namely  
whether to rename theorems or introduce qualifiers) which is best done  
by a theory's author.

Clemens


Quoting Makarius <makarius at sketis.net>:

> On Tue, 9 Oct 2012, Makarius wrote:
>
>> On Sun, 7 Oct 2012, Florian Haftmann wrote:
>>
>>> 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.
>>
>> I've started some experiments with this idea and will report the  
>> empirical results soon ...
>
> After some detours I am now back on Isabelle/28e37eab4e6f.
>
> In principle, the last big reform of locale + interpretation name  
> space prefixes has addressed the situation already, where each  
> locale scope is locally strict, but composing several of them in  
> locale expressions etc. works by mandatory or non-mandatory prefixes.
>
> Actual strictness checking is part of the underlying name space  
> policy, when bindings are applied and react with some naming. The  
> "local" context of the locale construction is particularly important  
> here.  It was merely a historical left-over that fact bindings were  
> not checked strictly:
>
>   (1) in distant past facts were never strict and totally un-authentic
>
>   (2) the Isar proof "body" mode allows to override 'notes' as it does for
>       'fixes'.
>
> 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.
>
> (For me it was interesting to see how Isabell/jEdit works on the  
> JinjaThreads monster session.  See also AFP/77f79b2076f1 of the  
> result of investing 3GB for poly, 4GB for java, and quite a bit of  
> CPU time and elapsed time.)
>
>
> 	Makarius
>