*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] question about locales and locale parameters*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Wed, 14 Apr 2010 09:55:45 -0700*Cc*: isabelle-users at cl.cam.ac.uk, Viorel Preoteasa <viorel.preoteasa at abo.fi>*In-reply-to*: <4BC5B709.1030009@informatik.tu-muenchen.de>*References*: <4BC4C03F.9060001@abo.fi> <4BC5B709.1030009@informatik.tu-muenchen.de>*Sender*: huffman.brian.c at gmail.com

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

**Follow-Ups**:**Re: [isabelle] question about locales and locale parameters***From:*Alexander Krauss

**References**:**[isabelle] question about locales and locale parameters***From:*Viorel Preoteasa

**Re: [isabelle] question about locales and locale parameters***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] Specification depends on extra type variables
- Next by Date: Re: [isabelle] question about locales and locale parameters
- Previous by Thread: Re: [isabelle] question about locales and locale parameters
- Next by Thread: Re: [isabelle] question about locales and locale parameters
- Cl-isabelle-users April 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list