[isabelle-dev] Shadowing of theorem names in locales

[Johannes Hölzl]

HOL-Probability (in Isabelle/bb5db3d1d6dd) and
Ordinary_Differential_Equations (in AFP/e9fa38f86b76) work now with this
patch.

A surprising change is found in Markov_Models:

  We get an error when an assumption has the same name as a fact in the
  locale:

    locale loc
    begin
      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.

 - Johannes



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
>        '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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev