# [isabelle] Simplification in locales

`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

`and then try to simplify the following (unprovable) lemma using the
``definition of f:
`
lemma (in l)
"f y = 2 * y"
apply (simp add: f_def)

`then I get the subgoal "x = y", as expected. 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

`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.
`
Thanks,
-john

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