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
"/home/rpollack/work/seas/crash/ubreeze/isabelle/experiments/localeTypeUnif.thy")

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

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

*** Outer syntax error (line 4 of
"/home/rpollack/work/seas/crash/ubreeze/isabelle/experiments/localeTypeUnif.thy"):
command expected,
*** but keyword where (line 4 of
"/home/rpollack/work/seas/crash/ubreeze/isabelle/experiments/localeTypeUnif.thy")
was found

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

Best,
Randy
--
On Mon, Nov 14, 2011 at 3:25 PM, Clemens Ballarin <ballarin at in.tum.de> 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 in.tum.de>:
>
>> 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.