[isabelle-dev] Semantics of hide (open)

[Makarius]

On Fri, 28 Dec 2012, Florian Haftmann wrote:

> I have the situation that I want to define via primrec a function with 
> an existing popular name (append) but retain the commonplace accesses 
> append for List.append and append.simps for List.append.simps (see 
> attached theory for a contrieved example).  With the existing semantics 
> of hide (open), I cannot achieve the desired effect; either (with 
> (open)), append.simps remains shadowed, or (without (open)) I am not 
> able to access Thy.append.simps any longer.

Quoting the example:

   hide_fact (open) append.simps
   thm append.simps -- {* the nonsense thms; would expect List.append.simps instead *}

Quiting the isar-ref manual:

   ... with the "(open)" option, only the base name is hidden.

The manual also agrees with the implementation of Name_Space.hide as far 
as I can see in 5min, so the expectation of the example is wrong.


> Maybe there is some confusion what the semantics of hide (open) is 
> exactly supposed to be.  But since the current state of affairs gives no 
> tool at hand to resolve situations as sketched above, this is a serious 
> obstacle.

The "hide" feature was added as a temporary workaround for the lack of 
proper scope management many years ago.  In the meantime we managed to get 
a bit further with the "naming + binding = name + accesses" equation, but 
not with scoping of theories and contexts.  I still would like to see that 
appear eventually, and "hide" become obsolete then.  (It will mean that 
names behave uniformly, i.e. different categories like "const" and "fact" 
need to agree in their visibility.)


 	Makarius