*To*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Subject*: Re: [isabelle] question about locales and locale parameters*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Wed, 14 Apr 2010 14:37:29 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <4BC4C03F.9060001@abo.fi>*Organization*: TU München, Lehrstuhl Software and Systems Engineering*References*: <4BC4C03F.9060001@abo.fi>*User-agent*: Thunderbird 2.0.0.24 (X11/20100411)

Hi Viorel, > locale test = > fixes none :: "'index" > begin; > > primrec > label:: "('a => 'index) => ('a list) => ('a => 'index)" where > "label lbl [] = lbl" | > "label lbl (y # S) = label (lbl(y := none)) S"; > > lemma first: "f x = none ==> f = label (f(x := i)) [x]"; > by auto; > > 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. Once "test.label none" has been unfolded to "test.label (f x)", the local theorems (in test) are not applicable any more. The global foundational theorems test.label.simps etc. could be used; however I do recommend to avoid that unfolding from the very beginning. Hope this helps, Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

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

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

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

- Previous by Date: Re: [isabelle] question about locales and locale parameters
- Next by Date: Re: [isabelle] Specification depends on extra type variables
- 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