*To*: Brian Huffman <huffman at in.tum.de>*Subject*: Re: [isabelle] Issue with multiple superclasses*From*: Joachim Breitner <breitner at kit.edu>*Date*: Wed, 25 Jul 2012 09:27:32 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <CAAMXsibBzC9oMzDoXeGijFXFzr_H09WO+haJ0P7fHPqfK73CeQ@mail.gmail.com>*References*: <1343145606.4230.37.camel@kirk> <CAAMXsibBzC9oMzDoXeGijFXFzr_H09WO+haJ0P7fHPqfK73CeQ@mail.gmail.com>*Sender*: Joachim Breitner <msg at joachim-breitner.de>

Dear Brian, thanks, that did the trick. I failed to notice the "begin po"-blocks that you wrapped your definitions in HOLCF in. Greetings, Joachim Am Dienstag, den 24.07.2012, 19:43 +0200 schrieb Brian Huffman: > Hi Joachim, > > A general principle for reasoning with classes is that if you want to > prove lemmas within the class context, you need to define *all* the > related constants inside the appropriate class contexts as well. > Otherwise you may run into problems with the so-called "base sort" > inferred for the classes. (To get a better idea of what is going on, > try turning on [[show_sorts]], and print the type of a class locale > predicate, e.g. "term class.Nonempty_Meet_cpo".) > > Most classes in the Isabelle libraries have "type" as the base sort > (this is the sort that type 'a will have within the class context) but > some classes in HOLCF have "cpo" as the base sort, due to the fact > that they refer to constants with continuous function types that are > only defined on class cpo. > > I haven't tried this code yet, but I would suggest changing > "definition is_lb" to "definition (in po) is_lb", and similarly for > is_glb; alternatively, wrap both definitions in a "context po begin > ... end" block. > > Hope this helps, > - Brian > > On Tue, Jul 24, 2012 at 6:00 PM, Joachim Breitner <breitner at kit.edu> wrote: > > Hello, > > > > I have a problem with type classes and multiple subclasses, and here is > > a stripped-town testcase: > > > > theory "Test" > > imports > > "~~/src/HOL/HOLCF/HOLCF" > > begin > > > > default_sort cpo > > > > class Top_cpo = cpo + > > assumes most: "∃x. ∀y. y ⊑ x" > > begin > > > > definition top :: "'a" > > where "top = (THE x. ∀y. y ⊑ x)" > > > > notation (xsymbols) > > top ("⊤") > > end > > > > definition is_lb :: "'a set => 'a => bool" (infix ">|" 55) where > > "S >| x <-> (∀y∈S. x ⊑ y)" > > > > definition is_glb :: "'a set => 'a => bool" (infix ">>|" 55) > > where > > "S >>| x <-> S >| x ∧ (∀u. S >| u --> u ⊑ x)" > > > > definition glb :: "'a set => 'a" ("⨅_" [60]60) where > > "glb S = (THE x. S >>| x)" > > > > class Nonempty_Meet_cpo = cpo + > > assumes nonempty_meet_exists: "S ≠ {} ⟹ ∃x. S >>| x" > > > > class Meet_cpo = Top_cpo + Nonempty_Meet_cpo > > begin > > lemma "∃ x. {} >>| (x::'a)" > > apply (rule_tac x = "⊤" in exI) > > (* > > Type unification failed: Variable 'a::cpo not of sort Top_cpo > > > > Failed to meet type constraint: > > > > Term: ⊤ :: ??'a > > Type: 'a > > *) > > oops > > > > end > > > > I would assume that the 'a inside the context of class will have that > > sort (Meet_cpo) and hence by implication Top_cpo, but it seems it does > > not. Would someone be so kind and help me out here? > > > > (This is on Isabelle2012.) > > > > Thanks, > > Joachim > > > > -- > > Dipl.-Math. Dipl.-Inform. Joachim Breitner > > Wissenschaftlicher Mitarbeiter > > http://pp.info.uni-karlsruhe.de/~breitner > -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.info.uni-karlsruhe.de/~breitner

**Attachment:
signature.asc**

**References**:**[isabelle] Issue with multiple superclasses***From:*Joachim Breitner

**Re: [isabelle] Issue with multiple superclasses***From:*Brian Huffman

- Previous by Date: Re: [isabelle] Unicode tokens in jedit
- Next by Date: Re: [isabelle] Unicode tokens in jedit
- Previous by Thread: Re: [isabelle] Issue with multiple superclasses
- Next by Thread: [isabelle] Proving cardinality
- Cl-isabelle-users July 2012 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