Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Lemmas in locales

Email Gateway (Aug 18 2022 at 11:53):

From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
Hi all,

I found the following behaviour of the lemmas command inside locales
rather strange and confusing. For example:

locale loc begin
definition a :: bool where "a == True"
definition b :: bool where "b == a"
lemma b_lemma: "b = True" unfolding b_def a_def ..

lemmas a_lemma' = b_lemma[unfolded b_def]
lemmas a_lemma = a_lemma'
end

Inside the locale, "thm a_lemma'" gives "a = True" as expected, outside
the locale, I get "b = True" for "thm loc.a_lemma'". Naturally, I would
want loc.a_lemma' to be "a = True" outside the locale, too.

Interestingly, loc.a_lemma really is "a = True", i.e. loc.a_lemma' is
not the same as loc.a_lemma although the definition suggests so.
By the way, the same seems to happen with other attributes like OF,
THEN, etc.

Is there some way to get the unfolded attribute beyond the end of the
locale other than interpreting the locale (which would do in the
example, but not in my actual setting) and other than declaring such
additional lemmata?

Regards,
Andreas

Email Gateway (Aug 18 2022 at 11:53):

From: Clemens Ballarin <ballarin@in.tum.de>
On 13 May 2008, at 14:04, Andreas Lochbihler wrote:

locale loc begin
definition a :: bool where "a == True"
definition b :: bool where "b == a"
lemma b_lemma: "b = True" unfolding b_def a_def ..

lemmas a_lemma' = b_lemma[unfolded b_def]
lemmas a_lemma = a_lemma'
end

Inside the locale, "thm a_lemma'" gives "a = True" as expected,
outside the locale, I get "b = True" for "thm loc.a_lemma'".
Naturally, I would want loc.a_lemma' to be "a = True" outside the
locale, too.

Attributes only apply to the version of the lemma inside the locale.
This is so, because declaring a lemma say [simp] in a locale should
not change the global simpset.

Declarations as

lemmas a_lemma' = b_lemma[unfolded b_def]

inside a locale should be avoided for another reason. Since the
attribute is executed whenever the locale is entered, if you have a
lot such declarations, the locale can become very slow.

Clemens

Last updated: May 03 2024 at 04:19 UTC