[isabelle-dev] Semantics of hide (open)
Makarius
makarius at sketis.net
Mon Jan 7 11:43:16 CET 2013
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
More information about the isabelle-dev
mailing list