*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] Problem with unfolding definitions while instantiating class*From*: Nils Jähnig <nils.jaehnig at tu-berlin.de>*Date*: Fri, 6 Jun 2014 15:17:35 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <5391A2A6.5050205@in.tum.de>*References*: <CA+fzNkKLf8K2pxj2U=Rr=-s=4RRBY8c4uMNXoeB1KRYWonY2KA@mail.gmail.com> <5390EAD1.2070908@cse.unsw.edu.au> <CA+fzNk+uQ-92XbTbwwKz2ydYB5NfGHywSDC_G-+U4Uftuadcqg@mail.gmail.com> <5391A2A6.5050205@in.tum.de>

Hello Tobias, thank you for your answer. > > And is it just me not understanding the type classes or overloading, or > is > > it really strange that definitions of one type class use definitions of > > another (stronger!) type class? > > What do you mean? > I expected the following behavior: "fun"::(type, ccpo) does not care about definitions for "fun"::(type, lattice) [1]. Different type, different definitions. If the type "inherits" from another type (i.e. is a supertype, as ccpo is to order and sup), then it is wanted to "inherit" defintions [2]. I'm not sure if I am thinking to object oriented. I thought locals introduce some sort of namespace, which could be used to differentiate between different Sup definitions for different types. > > I would also be grateful for explanations why it doesn't work, or why I > am > > trying in a wrong direction. > > As Dave said, it is not your fault, the setup in Main is not fine-grained > enough. You can modify Complete_Lattice as follows to make it work, but > your > theories will no longer work with the distribution: replace the block [...] > Thank you for the tip, but I don't want to modify the distribution theories. I was hoping more for something lika a "redefine" command inside of a type instantiation. Just out of curiosity, is there a place where I could vote for a change of Complete_lattices.thy? And would it be a complete waste of time to do so? > PS Do not import individual theories that are part of Main (like > Complete_Partial_Order), start from Main instead. Otherwise you get some > fragment of Main with unpredictable behaviour. > > I was hoping to not load Complete_lattices and its definitions this way, and thereby be prompted to define Sup_fun by myself. Nils [1]: attempting to instantiation "fun" :: (type, ccpo) sup begin threw the error Conflict of type arities: fun :: (type, ccpo) sup and fun :: (type, lattice) sup [2]: I solved my other problem, how to access the definition for chain while instantiating pcpo, by instantiating cpo first, where the defintion was available. My (unmet) expectation was that either I am prompted to define, or it is defined (and the definition accessible).

**Follow-Ups**:**Re: [isabelle] Problem with unfolding definitions while instantiating class***From:*Florian Haftmann

**Re: [isabelle] Problem with unfolding definitions while instantiating class***From:*Tobias Nipkow

**References**:**[isabelle] Problem with unfolding definitions while instantiating class***From:*Nils Jähnig

**Re: [isabelle] Problem with unfolding definitions while instantiating class***From:*David Cock

**Re: [isabelle] Problem with unfolding definitions while instantiating class***From:*Nils Jähnig

**Re: [isabelle] Problem with unfolding definitions while instantiating class***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Problem with unfolding definitions while instantiating class
- Next by Date: [isabelle] New AFP entry: Boolean Expression Checkers
- Previous by Thread: Re: [isabelle] Problem with unfolding definitions while instantiating class
- Next by Thread: Re: [isabelle] Problem with unfolding definitions while instantiating class
- Cl-isabelle-users June 2014 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