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.