*To*: Randy Pollack <rpollack at inf.ed.ac.uk>*Subject*: Re: [isabelle] Type parameters in a locale? Datatypes in a locale?*From*: Clemens Ballarin <ballarin at in.tum.de>*Date*: Mon, 27 Jun 2011 22:46:06 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <BANLkTi=L01Pi8EGDm0oQW2E6pctvR8eqOA@mail.gmail.com>*References*: <20110625114529.158851w3os0eo56h@mailbroy.in.tum.de> <BANLkTi=L01Pi8EGDm0oQW2E6pctvR8eqOA@mail.gmail.com>*User-agent*: Internet Messaging Program (IMP) H3 (4.3.8)

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

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

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

**Follow-Ups**:**Re: [isabelle] Type parameters in a locale? Datatypes in a locale?***From:*Florian Haftmann

**References**:**Re: [isabelle] Type parameters in a locale? Datatypes in a locale?***From:*Clemens Ballarin

**Re: [isabelle] Type parameters in a locale? Datatypes in a locale?***From:*Randy Pollack

- Previous by Date: Re: [isabelle] case split on tuples
- Next by Date: [isabelle] Z3 on a Mac
- Previous by Thread: Re: [isabelle] Type parameters in a locale? Datatypes in a locale?
- Next by Thread: Re: [isabelle] Type parameters in a locale? Datatypes in a locale?
- Cl-isabelle-users June 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list