# [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'
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

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