Email Gateway (Aug 22 2022 at 09:54): Email Gateway (Aug 22 2022 at 09:54):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear all,
I've been surprised by the behaviour of qualified in Isabelle2015-RC*. According to
Isar-ref, a qualified name is accessible outside of the context block only with additional
qualification. This seems to work fine for constants and plain definitions, but I run into
problems with packages like fun, inductive and primrec. The defined constants are only
accessibly with qualification, but not the generated theorems. Thus, they take precedence
over existing theorem names, which somewhat defeats the purpose of using qualified.
Below is a small example. Here, the generated theorem from the context rev.simps shadows
the existing theorem List.rev.simps. This makes qualified much less useful. Is there any
other way how I can avoid the shadowing? hide_fact (open) does not work either, here.
theory Scratch imports Main begin
term rev (* refers to List.rev *)
thm rev.simps (* refers to List.rev.simps *)
context begin
qualified fun rev :: "nat ⇒ nat" where "rev x = x"
end
term Scratch.rev (* refers to Scratch.rev as desired *)
term rev (* refers List.rev *)
thm rev.simps (* refers to Scratch.rev.simps, but should to List.rev.simps *)
end
Andreas
Email Gateway (Aug 22 2022 at 09:55):From: Makarius <makarius@sketis.net>
The 'qualified' modifier and "hide (open)" achieve a similar effect:
unqualified base name accesses are suppressed. In the examples considered
here, names like "rev.simps" are already qualified, so the is no change.
It was always like that, but it does not mean that further reforms are not
possible. After the release, I would like to re-open the can concerning
qualified name bindings again, to see if even more useful name space
policies can be allowed.
The present confusion is probably due to the wording "additional
qualification" in the isar-ref manual. I've changed that here:
https://bitbucket.org/isabelle_project/isabelle-release/commits/1f9e08394d46
Makarius
Email Gateway (Aug 22 2022 at 09:55):From: Lochbihler Andreas <andreas.lochbihler@inf.ethz.ch>
Hi Makarius,
The word additional in isar-ref indeed confused me and the new wording is clearer. But I am glad that you plan to have another look at the namespace issue after the release.
Thanks for the clarification,
Andreas
Last updated: Apr 25 2024 at 12:23 UTC