Re: [isabelle] Lemmas in locales



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







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