[isabelle] question about locales and locale parameters



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.