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
>> 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).
> 




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