*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Collections: problems with sets of sets*From*: Stephan Merz <Stephan.Merz at loria.fr>*Date*: Sun, 10 Jul 2011 12:44:38 +0200

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. Thanks, Stephan

**Attachment:
Maxima.thy**

**Follow-Ups**:**Re: [isabelle] Collections: problems with sets of sets***From:*Alexander Krauss

- Previous by Date: Re: [isabelle] Problems with Logic.mk_implies + compose_tac
- Next by Date: Re: [isabelle] Untyped formalized systems are wrong (blog post)
- Previous by Thread: Re: [isabelle] Strange behaviour. Errors depend on file length.
- Next by Thread: Re: [isabelle] Collections: problems with sets of sets
- Cl-isabelle-users July 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list