[isabelle] Lemmas in locales

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'

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?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.