[isabelle] Very strange behaviour of interpretation
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
definition bar where "bar f = [Suc f]"
interpretation itrprt: L "bar f" .
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
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)
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