[isabelle] Type parameters in a locale? Datatypes in a locale?

Consider the following in HOL

locale label = bounded_lattice +
  fixes lblRem :: "'a \<Rightarrow> 'b \<Rightarrow>  'a"
  and canElim :: "'b \<Rightarrow> 'a \<Rightarrow> bool"

First question: which type variable of the locale "label" ('a or 'b,
or neither) is understood to be the single type variable of
"bounded_lattice"?  I want 'a to be the lattice.  How can I say that?

In the locale context I want to define a datatype

datatype ('a,'b) expr = ...

where 'a and 'b are the type variables of the locale, and 'a is the
lattice.  It seems that datatype definitions are not accepted in a
locale context, so I defined ('a,'b) expr before the locale and tried
to instantiate it with 'a and 'b inside the locale.

type_synonym exp = "('a,'b) expr"

This fails: '*** Extra variables on rhs: "'b", "'a"'.  In my mind, the
type variables 'a and 'b are somehow fixed in the locale context, so
are not extra variables on rhs.  That is, in any (concrete?) instance
of the locale 'a and 'b will be fixed, so I should be able to give
them symbolic names and use them as if they were declared (say with
typedecl) inside the locale context.

I try something else:

type_synonym ('a,'b) exp = "('a,'b) expr"

This fails too: '*** Locally fixed type arguments "'a", "'b" in type
declaration "exp"'  So Isabelle also thinks 'a and 'b are fixed in the
locale context.

Now I'm stuck.  Can I do what I'm trying to do.? If not, is there a
logical reason why not?


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