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