Email Gateway (Aug 22 2022 at 10:59): Email Gateway (Aug 22 2022 at 10:59):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Gene,
bringing some light into these »stangenesses«…
signature.asc
Email Gateway (Aug 22 2022 at 11:07):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Consider the following two theories: Foo and Bar (below and attached).
Theory Foo defines a locale L containing a definition "foo", then
interprets that locale at the top level.
Theory Bar imports Foo, extends locale L via a context block with an
additional definition "bar", then attempts to construct an interpretation
named Foobar for locale L at the top level. After that, it tries
to reference the constants "Foo.foo", "Foo.bar", "Foobar.foo", and "Foobar.bar".
As expected, "Foo.foo" is recognized, however "Foo.bar" is not recognized.
I theorize that the interpretation declared in theory Foo is fixed at the
point of its declaration, and does not receive any additional facts that
result from later extensions to the locale. That is understandable in
terms of the way locales generally seem to work, but is perhaps not so useful
from a modularity point of view, because it forces a theory that interprets
a locale to import all possible extensions to that theory before declaring
the interpretation, otherwise such extensions become impossible.
It is also the case that neither "Foobar.foo" nor "Foobar.bar" are recognized.
This seems to be because the system recognizes an existing interpretation
with the same parameters (there aren't any parameters in this case, but
the same effect occurs if there are parameters) and does not create a new
interpretation, with the effect that the qualified names "Foobar.foo"
and "Foobar.bar" remain unbound. This occurs even though the locale L
was extended with an additional definition. So the extension is pointless
because there is no way to get access to the additional constant.
If the interpretation in theory Foo is commented out, then in theory Bar
reference to Foo.foo and Foo.bar fail -- this is expected. The references
to Foobar.foo and Foobar.bar now succeed, presumably due to there being
no pre-existing interpretation.
Besides the modularity issue, this example exhibits a complaint I have that
I am becoming more confident about, now that I have gotten some experience
using locales. I can well understand why the system will not create redundant
instantiations of a locale. However, as the example illustrates, this
results in the rather surprising effect that after declaring an interpretation,
qualified names that one might expect to have been introduced by that
declaration have in fact not been introduced. This is not just a surprise,
it is also detrimental to readability, because one is forced to use the
previously introduced names to refer to the existing entities, even though
it might make more sense in the current context to use different names.
My opinion is that every locale declaration ought to introduce new bindings
for qualified names, even if these names are aliases to existing names
entities for which other names already exist. Note that I am not saying that
redundant entities be created, just that new aliases for these entities should
become bound. This would obviously cause ambiguity in unparsing, as there
would potentially be multiple choices of names to use, but this already occurs
in the case of abbreviations.
- Gene Stark
theory Foo
imports Main
begin
locale L
begin
definition foo where "foo = True"
end
(* Comment or uncomment the following to observe changes in theory Bar. *)
interpretation L .
end
theory Bar
imports Main Foo
begin
context L
begin
definition bar where "bar = False"
end
interpretation Foobar: L .
(* With interpretation in Foo.thy commented this fails -- expected. *)
(* With interpretation in Foo.thy uncommented this succeeds -- expected. *)
lemma "Foo.foo = True" using Foo.foo_def by auto
(* With interpretation in Foo.thy commented out these succeed -- expected. *)
(* With interpretation in Foo.thy uncommented these fail -- strange. *)
lemma "Foobar.foo = True" using Foobar.foo_def by auto
lemma "Foobar.bar = False" using Foobar.bar_def by auto
(* This fails regardless -- strange. *)
lemma "Foo.bar = False" using Foo.bar_def by auto
Last updated: Apr 27 2024 at 01:05 UTC