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,

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

locale sub =
   fixes a :: 'a
   definition P :: "'a â bool"
   where "P x â True"

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

assumes "loc a b f" and "loc b c g"
shows "loc a c (g o f)"
   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.


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