Re: [isabelle] Collections: problems with sets of sets



Hi Stephan,

I have been playing with the Collection framework lately and having
trouble when trying to set up executable sets of sets. The theory
below illustrates the problem: the function maxima is meant to
compute the maximal sets contained in a set of sets. Using the value
command, I can evaluate the function for the empty and for singleton
sets, but evaluation fails for any argument containing two or more
element sets.

There seems to be a problem with the setup of type Dlist. I reduced your example to a minimal one, which does not use the Collection framework.

The problem goes away when I remove the [code nbe] declaration that comes after the instance proof of equal in Dlist.thy (http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2011/src/HOL/Library/Dlist.thy#l128). I don't know about the precise semantics of [code nbe] wrt. normal code equations, but it seems to override the previous code equation.

Maybe Florian can comment...

Alex





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