[isabelle-dev] [isabelle] Simplification in locales
matthews at galois.com
Thu Jul 3 23:32:27 CEST 2008
>> lemma f_cong [cong]: "y = z ==> l.f x y = l.f x z"
> Well spotted. We have also toyed with this idea but hadn't done
> about it yet because locales are still not 100% finished.
Ok, then I'll continue this thread on isabelle-dev.
Brian's idea does indeed help with rewriting. However, the congruence
rule needs to be slightly more general to handle higher-order
occurrences of local functions:
lemma f_cong [cong]: "l.f x = l.f x"
You can also prove this lemma in the locale itself, which results in
this odd-looking rule:
lemma (in l) f_cong [cong]: "f = f"
But I'm not sure what side effects these congruence rules will have in
interpretations of l. Is there a way to only apply a theorem attribute
inside a locale and its descendants, but not in other locale
More information about the isabelle-dev