Re: [isabelle] question about locales and locale parameters
On Wed, Apr 14, 2010 at 5:37 AM, Florian Haftmann
<florian.haftmann at informatik.tu-muenchen.de> wrote:
> Hi Viorel,
>> locale test =
>> fixes none :: "'index"
>> label:: "('a => 'index) => ('a list) => ('a => 'index)" where
>> lemma second: "none = f x ==> f = label (f(x := i)) [x]";
>> apply auto;
> the matter is: internally, "label" (in test) is represented as
> "test.label none". Therefore the assumption "none = f x" rewrites this
> to "test.label (f x)" (c.f. also
> http://www4.in.tum.de/~wenzelm/papers/local-theory.pdf). You could call
> this a misbehaviour of the simplifier.
It seems that inside the locale, "label == test.label none" is
registered as a local *abbreviation*. As such, its argument ("none")
is still visible to the simplifier.
Is there any reason why "label == test.label none" could not be
implemented instead as a local *definition*? I'm thinking of how the
"def" command works within a proof script: This adds a definition that
is unfolded when the lemma is exported, but within the proof, the
simplifier just sees an opaque constant.
If locally-defined constants were treated this way in locales, I think
the behavior would cause many fewer surprises for users.
This same issue has been brought up on this list before, nearly two years ago:
At the time, I recommended using a congruence rule as a quick
workaround to prevent the simplifier from tampering with hidden
parameters of locally-defined constants. But I think a "def"-like
mechanism is a better solution.
This archive was generated by a fusion of
Pipermail (Mailman edition) and