[isabelle-dev] Shadowing of theorem names in locales
hoelzl at in.tum.de
Thu Oct 11 14:50:48 CEST 2012
HOL-Probability (in Isabelle/bb5db3d1d6dd) and
Ordinary_Differential_Equations (in AFP/e9fa38f86b76) work now with this
A surprising change is found in Markov_Models:
We get an error when an assumption has the same name as a fact in the
lemma X: "True" ..
lemma assumes X: "X" shows "True"
^- raises "Duplicate fact declaration "local.X" vs. "local.X""
Is this easily avoidable? I think this might confuse people and add a
maintenance burden when one adds a fact to a locale with a popular name.
Am Mittwoch, den 10.10.2012, 16:51 +0200 schrieb Makarius:
> 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 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.)
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev