# [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.