Email Gateway (Aug 18 2022 at 13:34): Email Gateway (Aug 18 2022 at 13:34):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
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
Email Gateway (Aug 18 2022 at 13:34):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,
since f is a new parameter, it must be fixed explicitly:
interpretation itrprt: L "bar f" for f .
Tthen everything looks as expected.
I remember that there has been some discussion whether free variable
should be fixed automatically, but I on my behalf cannot tell what its
result are.
Hope this helps
Florian
signature.asc
Last updated: May 03 2024 at 08:18 UTC