Email Gateway (Aug 18 2022 at 14:53): Email Gateway (Aug 18 2022 at 14:53):From: Iain Whiteside <i.whiteside@sms.ed.ac.uk>
Hi All,
I was looking for the symmetric difference operation on sets in Isabelle/HOL, but couldn't find it in Set.thy. Does anyone know if it exists anywhere else? I thought I'd better check before I go ahead and define it myself.
Thanks,
Iain
Email Gateway (Aug 18 2022 at 14:53):From: Lawrence Paulson <lp15@cam.ac.uk>
I don't believe it has ever been defined.
Larry Paulson
Email Gateway (Aug 18 2022 at 14:53):From: Tobias Nipkow <nipkow@in.tum.de>
I recommend not to make it a definition but an abbreviation, which saves
you having to prove intro and elim rules and instrument the automatic
provers.
Tobias
Iain Whiteside wrote:
Email Gateway (Aug 18 2022 at 14:54):From: Brian Huffman <brianh@cs.pdx.edu>
Hi Iain,
If you do define it yourself, you might find the Boolean_Algebra
theory (from HOL/Library) useful. It defines a locale "boolean" for
boolean algebras, and also a sublocale "boolean_xor" for those that
also have the xor operation defined. Originally the library was
intended to support bitwise arithmetic, but it should work perfectly
with a symmetric difference operation on sets.
If you do a locale interpretation with your symmetric difference
operation, the locale will generate lots of useful lemmas for you
automatically, such as associativity, commutativity, distributive laws
with intersection, etc.
Hope this helps,
Last updated: Nov 21 2024 at 12:39 UTC