Re: [isabelle] question about locales and locale parameters

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  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,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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