Email Gateway (Aug 19 2022 at 17:25): Email Gateway (Aug 19 2022 at 17:25):From: "Eugene W. Stark" <stark@cs.stonybrook.edu>
Can anyone explain the strange error described in the final comment
in the code below? It seems especially odd to me that the presence
of the error depends on the order of the preceding "interpret" lines.
The strange type inference behavior described in the comment
after the "assumes" line is also a puzzle to me.
In case my mailer has mutated the code, I've also attached the theory
file. Thanks for any help.
- Gene Stark
theory Buggy
imports Main
begin
locale sub =
fixes a :: 'a
begin
definition P :: "'a ⇒ bool"
where "P x ≡ True"
end
locale loc =
X: sub a + Y: sub b
for a and b +
fixes f :: "'a ⇒ 'b"
assumes "f a = b"
(*
* If the preceding line is removed, then constant "loc"
* ends up having type "'a ⇒'a ⇒ ('b ⇒ 'b) ⇒ bool
* instead of "'a ⇒ 'b ⇒ ('a ⇒ 'b) ⇒ bool
*)
lemma
assumes "loc a b f" and "loc b c g"
shows "loc a c (g o f)"
proof
interpret F: loc a b f using assms(1) by auto
interpret G: loc b c g using assms(2) by auto
have "⋀x. F.X.P x" using F.X.P_def by auto
have "⋀x. G.X.P x" using G.X.P_def by auto
(*
* Constant G.X.P is unrecognized in the preceding line.
* If the "interpret" lines are interchanged,
* there is no error.
*)
qed
end
Buggy.thy
Email Gateway (Aug 19 2022 at 17:25):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Gene,
I do not understand what problem you refer to in the first comment (about removing the
previous line). If I remove the "assume" clause, no constant loc is generated at all, as
there are no assumptions in loc or its ancestors.
Now to the problem with interpret. Interpretations (and also sublocale declarations) check
whether an interpretation of a locale with the same (or more general) parameters is
already present. If so, it does not interpret the locale, even if the name prefixes are
different. In your case,
interpret F: loc a b f using assms(1) by auto
introduces the interpretations
F: loc a b f, F.X: sub a, F.Y: sub b
Naively, the next interpret G: loc b c g generates the interpretations
G: loc b c g, G.X: sub b, G.Y: sub c
However, sub b has already been interpreted as F.X, so there is not another interpretation
for G.X. Consequently, you'd have to use the name F.Y to refer to G.X interpretations. If
you swap the declarations, you get G.X and F.X, but not F.Y by the analogous reasoning.
Hope this helps,
Andreas
Last updated: Apr 26 2024 at 08:19 UTC