[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
locale A =
assumes "a = a"
definition b' where "b' = a"
locale B =
assumes "b = b"
definition a' where "a' = b"
locale C = A a + B b
for a :: 'a and b :: 'a +
assumes "a = b"
sublocale A â C a b'
show "b' = b'" by auto
show "a = b'" using b'_def by auto
sublocale B â C a' b (* Duplicate constant: local.a' vs. local.a' *)
show "a' = a'" by auto
show "a' = b" using a'_def by auto
This archive was generated by a fusion of
Pipermail (Mailman edition) and