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



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.