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