[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.