[isabelle-dev] Shadowing of theorem names in locales
ballarin at in.tum.de
Tue Jun 4 22:01:13 CEST 2013
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.
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
> So with the "ch-strict" changeset applied to the critical spot of
> local notes, the namespace policy enforces the concentual locale
> 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,
> 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.)
More information about the isabelle-dev