# [isabelle] Another locale puzzle

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

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*