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.