I am having a problem with sublocales as follows.
Suppose I have a locale AAA (with two parameters M and T), in which I defined a lot of
objects. I have proved that AAA is a sublocale of a locale BBB. I am proving a theorem in
AAA. During the proof, I construct two objects M2 and T2, and I can prove "AAA M2 T2".
Then, I would like to apply to M2 and T2 a theorem of BBB. I tried two approaches:
1) interpret AAA M2 T2
to get all the theorems of AAA and BBB for M2 T2. However, there are a lot of name
clashes, between all the objects already defined in the ambient AAA M T, and the new AAA
M2 T2, so this command is rejected.
2) have "BBB M2 T2"
If I could deduce this from "AAA M2 T2", then I could apply the theorems of BBB to M2 T2.
However, I did not find how to prove this using the already proved "sublocale AAA
\subseteq BBB"
To get 1) to work, I would for instance need all objects in AAA M2 T2 to be prefixed
automatically by something, say, to distinguish them from AAA M T.
To get 2) to work, I would need to have a lemma saying that "AAA M2 T2 ==> BBB M2 T2". Is
a lemma like this available somewhere once the sublocale inclusion is proved?
Anyway, any hints on better methods, or best practice, are welcome!
Best,
Esseger