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