Re: [isabelle] sublocale problem



Dear Esseger,

1. Interpretations can be given name prefixes to avoid clashes. For example,

interpretation prefix!: AAA M2 T2

2. Unfortunately, the sublocale command does not export the rule for showing the locale predicate of superlocales. Consequently, I recommend to first prove sublocale proof obligation in a lemma and then use the lemma for discharging the goal in the sublocale command. Here's an example:

context AAA begin
lemma BBB: "BBB M T" <proof>
sublocale BBB M T by(rule BBB)
end

Hope this helps,
Andreas

On 13/10/15 22:52, Esseger wrote:
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.