*To*: Peter Lammich <peter.lammich at uni-muenster.de>*Subject*: Re: [isabelle] Fwd: Collections: problems with sets of sets*From*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Date*: Tue, 12 Jul 2011 08:10:44 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Stephan Merz <Stephan.Merz at loria.fr>*In-reply-to*: <4E1B6252.8000100@uni-muenster.de>*References*: <4E1A9E09.4080504@kit.edu> <B189A051-158E-4088-8C79-1FA13E04C2D5@loria.fr> <4E1B6252.8000100@uni-muenster.de>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.13) Gecko/20101208 Thunderbird/3.1.7

Hi Peter and Stephan,

Andreas

A more general solution would be to abstract over the equality operator in the set's locales such that user-defined equalities could be used. However, neither Peter nor me have attempted to do that yet.However, we know that problem and have already discussed it. I think that the result was that it is, in principle, possible. The set implementation would then store custom equals (and hashcode, compare, etc.) functions, that have to be specified, e.g. on construction of a set (empty-operation). The data structure invariant (and the precondition of the empty-operation) would require that the custom equals, hashcode, compare, etc functions are sensible. A default empty-operation, setting the functions to default values (e.g. op =, op<), would still be possible. Best, Peter

-- Karlsruher Institut für Technologie IPD Snelting Andreas Lochbihler wissenschaftlicher Mitarbeiter Adenauerring 20a, Geb. 50.41, Raum 031 76131 Karlsruhe Telefon: +49 721 608-47399 Fax: +49 721 608-48457 E-Mail: andreas.lochbihler at kit.edu http://pp.info.uni-karlsruhe.de

**References**:**[isabelle] Fwd: Collections: problems with sets of sets***From:*Stephan Merz

**Re: [isabelle] Fwd: Collections: problems with sets of sets***From:*Peter Lammich

- Previous by Date: Re: [isabelle] Fwd: Collections: problems with sets of sets
- Next by Date: [isabelle] Status of HOL/Import
- Previous by Thread: Re: [isabelle] Fwd: Collections: problems with sets of sets
- Next by Thread: [isabelle] Status of HOL/Import
- 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