Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] sublocale problem


view this post on Zulip 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

view this post on Zulip 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

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

view this post on Zulip 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.

  1. 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: Mar 28 2024 at 12:29 UTC