Email Gateway (Aug 19 2022 at 17:33): Email Gateway (Aug 19 2022 at 17:33):From: "Eugene W. Stark" <stark@cs.stonybrook.edu>
I wanted to use locales to represent a relationship between
three classes of structures: A, B, and C, where C includes
all the constants and axioms of both A and B, and where
an instance of either A or B can be definitionally extended
to an instance of C.
The code below abstracts what I was trying to do.
However, only one of the two sublocale declarations will succeed;
in the presence of one an attempt to introduce the second will
fail with a "duplicate constant" error.
How should I think about what is happening here in order to
understand why there is a duplicate constant, and is there any
way to work around this to do what I was trying to do?
Thanks for your forbearance and assistance.
- Gene Stark
theory Strange1
imports Main
begin
locale A =
fixes a
assumes "a = a"
begin
definition b' where "b' = a"
end
locale B =
fixes b
assumes "b = b"
begin
definition a' where "a' = b"
end
locale C = A a + B b
for a :: 'a and b :: 'a +
assumes "a = b"
sublocale A ⊆ C a b'
proof
show "b' = b'" by auto
show "a = b'" using b'_def by auto
qed
sublocale B ⊆ C a' b (* Duplicate constant: local.a' vs. local.a' *)
proof
show "a' = a'" by auto
show "a' = b" using a'_def by auto
qed
end
Email Gateway (Aug 19 2022 at 17:34):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Eugene,
In your example, you are creating a cycle in the sublocale graph (C is a sublocale of A
and B, and both A and B shall be sublocales of C). To see what happens, it is best to
explore all the interpretations that you create. In the following picture, -> denotes an
edge in the sublocale graph.
C a b -> A a -> C a b' -> A a (subsumed by previous interpretation)
| |
| +----> B b' -> C a' b -> A a'
|
+----> ...
As you can see, with both sublocale commands, you try to interpret the locale A twice.
Once with the parameter a, once with the parameter a'. Logically, both are the same by the
definition, but Isabelle cannot see this. Thus, when you open the locale context C a b,
you would want to define a' from A with respect to the locale parameter a and once more
with respect to the parameter a'. As a' can only be defined once, you get an error as
expected.
In general, I recommend to avoid cyclic locale dependencies. Except for rare cases, they
most likely get you into trouble. If you want to have B extended to C definitionally, then
define a new locale B_extended and make only B_extended a sublocale of C. Then, you avoid
the cycles and name space problems.
Best,
Andreas
Last updated: Apr 25 2024 at 20:15 UTC