*To*: Clemens Ballarin <ballarin at in.tum.de>*Subject*: Re: [isabelle] Type parameters in a locale? Datatypes in a locale?*From*: Randy Pollack <rpollack at inf.ed.ac.uk>*Date*: Sat, 25 Jun 2011 22:02:34 -0400*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <20110625114529.158851w3os0eo56h@mailbroy.in.tum.de>*References*: <20110625114529.158851w3os0eo56h@mailbroy.in.tum.de>*Sender*: rpollack0 at gmail.com

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:*Clemens Ballarin

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

- Previous by Date: Re: [isabelle] Type parameters in a locale? Datatypes in a locale?
- Next by Date: [isabelle] case split on tuples
- 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