Re: [isabelle] sublocale problem
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)
Hope this helps,
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
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!
This archive was generated by a fusion of
Pipermail (Mailman edition) and