# Re: [isabelle] Simplification in locales

```Quoting John Matthews <matthews at galois.com>:

```
```I'm running into some behavior of locales that seems to violate
"locality". I'm using Isabelle2008. If I define the following locale

locale l =
fixes x :: nat
begin

definition
f :: "nat => nat" where
"f y = x + y"

end
```
```...
```
```If, however, I add a
hypothesis about x to the lemma and try to simplify it again:

lemma (in l)
"x = y ==> f y = 2 * y"

then I'd expect the lemma to be provable, but instead I get the
following subgoal:

1.  x = y ==> l.f y y = 2 * y
```
```
```
I think I understand what is going on here. When you define the constant f inside the locale l, it defines a global constant named "l.f", which has extra parameters corresponding to the locale fixes.
```
```
Within the context of locale l, when you write "f", this is really just an abbreviation for "l.f x". So your lemma is really equivalent to:
```
lemma (in l) "x = y ==> l.f x y = 2 * y"

The simplifier then happily rewrites x to y in the conclusion:

1. x = y ==> l.f y y = 2 * y

```
```Eliminating the locale l and replacing "fixes x :: nat" with "consts x
:: nat" causes the lemma to be provable, so it seems that the
abstraction of a locale as a local theory is being violated somehow.
```
```
```
I agree that the locale abstraction is being violated in this case. Even if locale-defined constants are implemented as abbreviations, this should not be apparent to the user. Here's my idea for a possible remedy: Within the locale, the simplifier should use a congruence rule that prevents the implicit parameters from being rewritten:
```
lemma f_cong [cong]: "y = z ==> l.f x y = l.f x z"

- Brian

```

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