# [isabelle] sublocale problem

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

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