# [isabelle] Very strange behaviour of interpretation

Hi all,

`I just stumbled over the following, strange behaviour of interpretation
``for locales in Isabelle 2009: Suppose, L is a locale which fixes only
``parameters and makes a definition:
`
locale L = fixes a :: "nat list"
begin
definition foo where "foo = a"
end

`When I interpret L, where the parameter is instantiated with a function
``applied to a parameter, which itself is not bound, the following strange
``behaviour occurs:
`
definition bar where "bar f = [Suc f]"
interpretation itrprt: L "bar f" .
thm itrprt.foo_def
prints "L.foo (bar f) = bar f" in the response buffer of ProofGeneral.

`The important thing is that f is not free (?f), but highlighted like a
``variable in a proof that has not been mentioned before. In particular,
``it becomes almost impossible to use trprt.foo_def for proving:
`
lemma test: "itrprt.foo 0 = [Suc 0]"
displays the goal "L.foo (bar 0) = [Suc 0]", but
unfolding itrprt.foo_def
does not affect it. Now, I restate the lemma more complicately:
lemma test': fixes f
defines "f == 0"
shows "itrprt.foo f = [Suc f]"
Here, "unfolding itrprt.foo_def" DOES unfold the definition of L.foo.

`Apparently, the locally bound f is identified with the unbound f in the
``generated theorem itrprt.foo_def.
``If f is replaced with g in this lemma, "unfolding itrprt.foo_def" does
``not change the goal.
`
If, however, I add an assumption to L, things again are different:
locale L2 = fixes a :: "nat list"
assumes "a ~= []"
begin
definition foo2 where "foo2 = a"
end
interpretation itrprt2: L2 "bar f" by(unfold_locales)(simp add: bar_def)
thm itrprt2.foo2_def

`produces "L2.foo2 (bar ?f) = bar ?f" with the f being now free. Hence,
``test can be shown using this theorem.
`

`What is happening here? Is this behaviour intended? Am I using the
``interpretation syntax in a wrong manner?
`
Regards,
Andreas

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