Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] sublocale problem

Email Gateway (Aug 22 2022 at 11:44):

From: Esseger <esseger@free.fr>
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

Email Gateway (Aug 22 2022 at 11:45):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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

Email Gateway (Aug 22 2022 at 11:45):

From: Esseger <esseger@free.fr>
Le 14/10/2015 08:20, Andreas Lochbihler a écrit :

Dear Esseger,

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

interpretation prefix!: AAA M2 T2

That's exactly what I need, thanks a lot.

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

This is what I was doing, but it was getting tedious as in my use case
there is a chain of inclusions, so having a lemma for each inclusion was
really not convenient.

Best,
Esseger

Last updated: Nov 21 2024 at 12:39 UTC