[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"

definition foo where "foo = a"


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 ~= []"
definition foo2 where "foo2 = a"
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?


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