[isabelle] Lemmas in locales
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,
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and