[isabelle] Issue with multiple superclasses



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
Description: This is a digitally signed message part



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.