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

Thanks, but I'm still stumped.  Let's go through a simplified example.
 I'm using

theory testing imports Main begin   (** nothing up my sleeve **)
thm le_supI1                        (* some theorem from semilattice_sup *)

Prints out

(?x\<Colon>?'a\<Colon>semilattice_sup) \<le>
(?a\<Colon>?'a\<Colon>semilattice_sup) \<Longrightarrow>
?x \<le> sup ?a (?b\<Colon>?'a\<Colon>semilattice_sup)

Why?  The notation
\<le>  (from class order) is preserved, but the notation "\<squnion>"
for sup (from
class semilattice_sup is gone.

I want to create a new locale, extending lattice with a new operator.  The new
operator may mention several type variables, one specific one of which
should be the
same as the lattice type.  This was my original question.

I first tried this:

locale label = lattice +
  fixes noperator :: "'a::lattice \<Rightarrow> 'b"

This doesn't seem to work:

locale label =
  fixes less_eq :: "'c\<Colon>type \<Rightarrow> 'c\<Colon>type
\<Rightarrow> bool"
    and less :: "'c\<Colon>type \<Rightarrow> 'c\<Colon>type
\<Rightarrow> bool"
    and inf :: "'c\<Colon>type \<Rightarrow> 'c\<Colon>type
\<Rightarrow> 'c\<Colon>type"
    and sup :: "'c\<Colon>type \<Rightarrow> 'c\<Colon>type
\<Rightarrow> 'c\<Colon>type"
    and nopr :: "'b\<Colon>type \<Rightarrow> 'a\<Colon>lattice"

"noperator" is not constrained to have type 'c, which seems to be the
lattice type here.
And why does 'c have sort "type" instead of sort "lattice"?

So following Clemens' suggestion, I write:

locale label = lattice less_eq
  for less_eq::"'a::lattice \<Rightarrow> 'a \<Rightarrow> bool"
(infix "\<le>" 50) +
  fixes noperator :: "'a \<Rightarrow> 'b"

locale label =
  fixes less :: "'a\<Colon>lattice \<Rightarrow> 'a\<Colon>lattice
\<Rightarrow> bool"
    and inf :: "'a\<Colon>lattice \<Rightarrow> 'a\<Colon>lattice
\<Rightarrow> 'a\<Colon>lattice"
    and sup :: "'a\<Colon>lattice \<Rightarrow> 'a\<Colon>lattice
\<Rightarrow> 'a\<Colon>lattice"
    and less_eq :: "'a\<Colon>lattice \<Rightarrow> 'a\<Colon>lattice
\<Rightarrow> bool"
    and noperator :: "'a\<Colon>lattice \<Rightarrow> 'b\<Colon>type"

That looks better, and printing "le_supI1" as above gives:

(?x\<Colon>'a\<Colon>lattice) \<le> (?a\<Colon>'a\<Colon>lattice)
?x \<le> (sup\<Colon>'a\<Colon>lattice \<Rightarrow> 'a\<Colon>lattice
\<Rightarrow> 'a\<Colon>lattice) ?a (?b\<Colon>'a\<Colon>lattice)

But when I try to state this myself:

lemma "x \<le> a \<Longrightarrow> x \<le> (sup a b)"

*** Ambiguous input, 4 terms are type correct:
*** ((x \<le> a) \<Longrightarrow> (x \<le> (sup a b)))
*** ((x \<le> a) \<Longrightarrow> (x \<le> (sup a b)))
*** ((x \<le> a) \<Longrightarrow> (x \<le> (sup a b)))
*** ((x \<le> a) \<Longrightarrow> (x \<le> (sup a b)))

What do you suggest?

On Tue, Jun 28, 2011 at 1:45 PM, Florian Haftmann
<florian.haftmann at> wrote:
> Hi all,
>> Class syntax is declared
>> both at the theory level and in the class context.
> Not exactly.  Class syntax is *only* declared at the theory level, but
> inside the class context occurences of the global class operations on
> the type parameter 'a of the class are improved to their local
> counterparts.  This allows to use syntax uniformly (c.f. class tutorial,
> §3.6).
> Hope this helps,
>        Florian
> --
> Home:
> PGP available:

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