# [isabelle] question about locales and locale parameters

*To*: isabelle-users at cl.cam.ac.uk
*Subject*: [isabelle] question about locales and locale parameters
*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>
*Date*: Tue, 13 Apr 2010 22:04:31 +0300
*User-agent*: Mozilla/5.0 (Windows; U; Windows NT 6.1; en-US; rv:1.9.1.9) Gecko/20100317 Thunderbird/3.0.4

Hello,
I have the following locale definition:
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 first lemma is proved by auto as one would expect, however the second
lemma is transformed into
f = test.label (f x) (f(x := i)) [x]
where test.label :: 'index => ('a => 'index) => 'a list => 'a => 'index
At first I had big problems understanding why label would have the

`first parameter of type 'index, then I figured out that this extra
``parameter
`is the parameter none fixed by the locale. This fact can also be deduced
from how second lemma was transformed by auto.
1. Within a locale I would expect the fixed parameters to behave as
constants.
2. Even if they are treated as variable in second lemma I would expect

`that the definition label can still be applied to test.label (f x) (f(x
``:= i)) [x]
`with (f x) instead on none. If that would be the case, then second lemma
should be discharged automatically.
3. Trying to apply the definition of label manually (unfold ...) (rule ...)
or (simp add: ...) does not change the goal
4. How do I prove f = test.label (f x) (f(x := i)) [x] ? I can prove
second lemma using by (case_tac "f x = none", auto) but the statement
" f = test.label (f x) (f(x := i)) [x]" occurs in a much more involved
result, and I cannot control how the simplifications are done before
getting this "unprovable" goal.
Best regards,
Viorel

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