*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Problem with unfolding definitions while instantiating class*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Mon, 09 Jun 2014 11:54:14 +0200*In-reply-to*: <CA+fzNkK-mqrvjsH64ou4omMrXs-oytMjsiFp-b6SXe0+pGCwrQ@mail.gmail.com>*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> <CA+fzNkK-mqrvjsH64ou4omMrXs-oytMjsiFp-b6SXe0+pGCwrQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:24.0) Gecko/20100101 Thunderbird/24.5.0

On 06/06/2014 15:17, Nils Jähnig wrote: > 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. In order to have most general types, the set of all instantiations must satisfy certain constraints. Tobias > 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). >

**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

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

- Previous by Date: Re: [isabelle] Problem with unfolding definitions while instantiating class
- Next by Date: Re: [isabelle] Problem with unfolding definitions while instantiating class
- 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