[isabelle-dev] [isabelle] Simplification in locales

[John Matthews]

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