Re: [isabelle] Problem with unfolding definitions while instantiating class



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



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