Email Gateway (Aug 19 2022 at 11:54): Email Gateway (Aug 19 2022 at 11:54):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear all,
There are multiple definitions of a map function in Isabelle/HOL, e.g., List.map,
RBT_Impl.map, Mapping.map. While the constants are hidden with hide_const (open) to ensure
that plain "map" resolves to List.map, the theorems about these map functions are
typically not. What bothers me (and René Thiemann who brought my attention to this issue)
now, is that hide_fact (open) does not work for some of these theorems. In detail, the
theorem RBT_Impl.map.simps hides List.map.simps whenever one imports RBT_Impl. As
map.simps is already a qualified name, one cannot openly hide the one from RBT_Impl.
How can I hide RBT_Impl.map.simps such that map.simps resolves to List.map.simps?
I know that "hide_fact RBT_Impl.map.simps" achieves this, but then, they are not
accessible at all.
(Of course, one could define an alias like map_simps in RBT_Impl first, then hide that
openly, and hide RBT_Impl.map.simps fully. But does this really have to be this
complicated? And if so, should we follow this path?)
Andreas
Email Gateway (Aug 19 2022 at 11:55):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
I dimly remember stumbling over the same issue when reworking all the
funny sequence theories in HOL-Main. I escaped the situation when I
realized that I could do the whole stuff with plain definitions instead
of primrec etc. But this is of course not the way to got with RBT.
I am at a loss to propose any strategy at the moment, but I deem it
needs a further refinement iteration of namespace handling to make any
substantial progress here.
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 11:59):From: Makarius <makarius@sketis.net>
Note that the "hide_const (open)" scheme became popular some years ago as
a temporaryworkaround* until the system provides more direct ways to
introduce names in a qualified manner. (As a general principle it is
better to say at the place where things are declared how there naming and
binding polices should work, and not patch the name space later on via
hiding.)
A proper solution is still not there, and won't be in the coming release
either. It also reminds me that another name space reform is still in the
pipeline for many years: qualified theory names according to their
session; maybe also some indication of 'private' theory to make it harder
to import things belong theory Main of Isabelle/HOL.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC