Re: [isabelle] Problem with unfolding definitions while instantiating class
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
>>> 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) . Different type, different definitions.
In order to have most general types, the set of all instantiations must satisfy
> 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 .
> 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
>>> 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
>> 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.
> attempting to
> instantiation "fun" :: (type, ccpo) sup
> threw the error
> Conflict of type arities:
> fun :: (type, ccpo) sup and
> fun :: (type, lattice) sup
> I solved my other problem, how to access the definition for chain while
> instantiating pcpo, by instantiating cpo first, where the defintion was
> My (unmet) expectation was that either I am prompted to define, or it is
> defined (and the definition accessible).
This archive was generated by a fusion of
Pipermail (Mailman edition) and