# Re: [isabelle] Strange errors involving locales

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
On 18/03/15 15:23, Eugene W. Stark wrote:

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

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