Hi Tobias, >> 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 > anything > 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 interpretations? Thanks, -john
