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
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
Description: OpenPGP digital signature



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