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



There's two issues here:

locale label = lattice less_eq             (** as Clemens suggested **)
  for less_eq::"'a::lattice \<Rightarrow> 'a \<Rightarrow> bool" +

removes the syntax from the parameter. It can either be declared with a syntax annotation in the for clause or via the notation command. So, what you did I would have expected to work.

What happens in you case is that syntax from an imported class does not arrive at the locale.

class my_class =
  fixes operation :: "'a => 'a => 'a" (infixl "++" 60)
begin
  term operation  (* prints op ++ *)
end

locale my_locale = my_class
begin
  term operation  (* prints operation, concrete syntax lost *)
end

(If you make my_class a locale, the syntax arrives in the second locale.) I suspect this is either explained by the class package or perhaps local theories (Florian, Makarius?). Class syntax is declared both at the theory level and in the class context. This likely causes the syntax conflict you observe.

Clemens


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

Thanks Clemens and Makarius, but now I have a new problem with notation.

Consider this

context lattice begin
thm le_supI1             ** a theorem from the typeclass lattice **)

This prints out

?x \<le> ?a \<Longrightarrow> ?x \<le> sup ?a ?b

So the typeclass "lattice" from Main supplies notation for less_eq,
(and less) but not for sup (or inf).  I don't understand why, but I
know how to fix it: put

notation  sup (infixl "\<squnion>" 70)

in the context.

Now consider my locale

locale label = lattice less_eq             (** as Clemens suggested **)
  for less_eq::"'a::lattice \<Rightarrow> 'a \<Rightarrow> bool" +
  fixes oprn :: "'a \<Rightarrow> nat \<Rightarrow> 'a"
begin
thm le_supI1

This prints out

less_eq ?x ?a \<Longrightarrow> less_eq ?x (sup ?a ?b)

So my "for" clause for less_eq has removed (or shadowed?) the notation
\<le> from the typeclass lattice.

I tried

locale label2 = lattice less_eq less inf sup
  for less_eq::"'a::bounded_lattice \<Rightarrow> 'a \<Rightarrow> bool" +
  fixes oprn :: "'a \<Rightarrow> nat \<Rightarrow> 'a"
begin
notation
  less_eq  (infix "\<le>" 50) and
  less     (infix "<"  50) and
  inf      (infixl "\<sqinter>" 70) and
  sup      (infixl "\<squnion>" 70)
thm le_supI1

This prints out

?x \<le> ?a \<Longrightarrow> ?x \<le> ?a \<squnion> ?b

So it looks good.  But I try

lemma "x \<le> a \<Longrightarrow> x \<le> a \<squnion> b"

This gives

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

I guess some mixup between \<squnion> of lattice and \<squnion> of label1

What is the problem?  How can I fix it?

Thanks for any help,
Randy
--
On Sat, Jun 25, 2011 at 5:45 AM, Clemens Ballarin <ballarin at in.tum.de> wrote:
Quoting Randy Pollack <rpollack at inf.ed.ac.uk>:

Consider the following in HOL

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

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

This is not specified.  Use print_locale to find out what happened (you may
need to set show_types).

I want 'a to be the lattice.  How can I say that?

You need to mention the type variable in the imported expression.  This can
be done like this:

 locale label = bounded_lattice x for x :: "... 'a ..." + ...

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.

[...]

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

As Makarius already said, use ('a, 'b) expr in your locale.

Clemens










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