[isabelle] Collections: problems with sets of sets

Dear all,

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.

I've then exported ML code computing the maxima of a two-element set. When trying to evaluate this code, exception "Fail" is raised, and sure enough the code contains

  fun equal_dlista _ _ _ = raise Fail "equal_dlist";

which is responsible for this. However, looking into theory DList I find 

  instantiation dlist :: (equal) equal

so I presumed that appropriate code for checking equality of two dlists would be generated. (I haven't looked much further, though, how this code would be set up.)

Am I doing something wrong here, or is this a known limitation?

NB: When I try to replace lists ('a ls) by hash sets ('a hs), I get the more sensible error message

  No type arity HashMap.hashmap :: hashable

for the definition of maxima -- I can understand that there is no hash function set up for hash sets themselves.


Attachment: Maxima.thy
Description: Binary data

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