*To*: Joachim Breitner <breitner at kit.edu>*Subject*: Re: [isabelle] Issue with multiple superclasses*From*: Brian Huffman <huffman at in.tum.de>*Date*: Tue, 24 Jul 2012 19:43:42 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <1343145606.4230.37.camel@kirk>*References*: <1343145606.4230.37.camel@kirk>

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

**Follow-Ups**:**Re: [isabelle] Issue with multiple superclasses***From:*Joachim Breitner

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

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