Re: [isabelle] Combining locales?



Oops. Sorry, I did not look up the parameter names of lattice when I wrote this. They are less_eq, less, inf and sup.

locale labelAuth =
  label: lattice where
  less_eq = lblle and less = lbllt and inf = lblinf and sup = lblsup
  for lblle and lbllt and lblinf and lblsup

will work. An instantiation 'name = term' means that the parameter 'name' of lattice is instantiated with 'term', which is an expression over the parameters of the declared locale. You still need the for clause, and in your case of importing two instances you will need the parameter type declarations as well in order share the type parameters.

The Isabelle/Isar reference manual documents named instantiation, but there are indeed no examples.

Sorry again for the confusion.

Clemens


Randy Pollack <rpollack at inf.ed.ac.uk>:

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.