*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Issue with multiple superclasses*From*: Joachim Breitner <breitner at kit.edu>*Date*: Tue, 24 Jul 2012 18:00:06 +0200*Sender*: Joachim Breitner <msg at joachim-breitner.de>

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

**Attachment:
signature.asc**

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

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