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 <makar...@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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
