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
Isabelle2011.

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"
begin

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"
begin

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)
\<Longrightarrow>
?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?

Thanks,
Randy
--
On Tue, Jun 28, 2011 at 1:45 PM, Florian Haftmann
<florian.haftmann at informatik.tu-muenchen.de> 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:
> http://www.in.tum.de/~haftmann
>
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>
>





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