*To*: Christian Sternagel <c-sterna at jaist.ac.jp>*Subject*: Re: [isabelle] HOLCF equality*From*: Brian Huffman <huffman at in.tum.de>*Date*: Mon, 9 Jul 2012 10:30:21 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4FF7C034.2090409@jaist.ac.jp>*References*: <4FF7B559.4010204@jaist.ac.jp> <4FF7C034.2090409@jaist.ac.jp>

On Sat, Jul 7, 2012 at 6:51 AM, Christian Sternagel <c-sterna at jaist.ac.jp> wrote: > When trying to define my own type class (I dropped all axioms for the sake > of a minimal example) > > class eq = > fixes eq :: "'a → 'a → tr" Hi Chris, Try "print_classes" after this definition, and you will see that class "eq" has "domain" as a superclass. The reason is that HOLCF declares class "domain" (consisting of types embeddable into the universal domain type "udom") as the default sort, so each occurrence of 'a in the type signature is treated as "'a::domain". You can override this by re-declaring a different default sort, or with a sort annotation: class eq = fixes eq :: "'a::cpo → 'a → tr" > and instantiating the lift type > > declare [[names_long]] > > instantiation lift :: (type) eq > begin > > I obtain > > Conflict of type arities for classes Representable.predomain < > Bifinite.profinite: > Lift.lift :: (HOL.type) > Representable.predomain and > Lift.lift :: (Countable.countable) > Bifinite.profinite > > which I don't understand. What is happening here? For type "'a lift" to be in class "domain", type 'a must be in class "countable". Now you are attempting to show that type "'a lift" is in class "eq" (a subclass of "domain") if 'a is in class "type" (a superclass of "countable"). Such combinations of instances are illegal in Isabelle, because they would cause problems with principal types for type inference. (I think the technical term for the requirement is "regularity", "co-regularity", or something like that.) If you keep "domain" as a superclass of "eq", then the following instance for "lift" will work: instantiation lift :: (countable) eq - Brian

**References**:**[isabelle] HOLCF equality***From:*Christian Sternagel

**Re: [isabelle] HOLCF equality***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] I want to print axiomatization info
- Next by Date: Re: [isabelle] HOLCF equality
- Previous by Thread: Re: [isabelle] HOLCF equality
- Next by Thread: Re: [isabelle] HOLCF equality
- 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