Re: [isabelle] Combining locales?

Hi Clemens,

I like your suggestion.  However I guess I didn't understand it.

locale labelAuth =
  label: lattice where
  le = lblle and lt = lbllt and inf = lblinf and sup = lblsup
  auth: lattice where
  le = authle and lt = authlt and inf = authinf and sup = authsup

returns error message

*** "le" not a parameter of instantiated expression
*** At command "locale" (line 3 of

I tried a few other syntaxes without success, e.g.

locale labelAuth =
  label: lattice where label.le = lblle

*** Outer syntax error (line 4 of
command expected,
*** but keyword where (line 4 of
was found

I'm completely floundering.  I found no explanation I could understand
in the Tutorial on Locales.

On Mon, Nov 14, 2011 at 3:25 PM, Clemens Ballarin <ballarin at> wrote:
> If this resolves the problem, then not only the order of the arguments of
> the locale predicate but also the order of the locale parameters has
> changed.  The latter is, of course, not internal if a class is used as a
> locale.
> Randy can make the locale expression invariant to such changes by using
> named instantiation syntax like this:
> labelAuth =
>  label: lattice
>   where le = lblle and lt = lbllt and inf = lblinf and sup = lblsup +
>  auth: lattice
>   ...
> Clemens
> Quoting Alexander Krauss <krauss at>:
>> Hi Randy,
>> On 11/14/2011 07:40 PM, Florian Haftmann wrote:
>>> I dimly remember that there have been changes in the type class import
>>> hierarchy which changed the order of arguments for locale predicates,
>>> but I can't recall exactly which.  Maybe somebody else can comment?
>> The change was 5e51075cbd97, and here is the NEWS entry:
>> * Added syntactic classes "inf" and "sup" for the respective
>> constants.  INCOMPATIBILITY: Changes in the argument order of the
>> (mostly internal) locale predicates for some derived classes.
>> Your definition works again, when lblinf/authinf are moved to the front.
>> The dependence of the predicate arguments on the specifics of the hierarchy
>> is a bit unfortunate...
>> Alex

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