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"
>>   begin;
>>
>>   primrec
>>     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:

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2008-June/msg00089.html

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.

- Brian





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