# [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.