# 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"
apply (simp add: f_def)
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.*