Re: [isabelle] Symmetric Difference of sets
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,
On Wed, Mar 10, 2010 at 8:55 AM, Iain Whiteside
<i.whiteside at sms.ed.ac.uk> wrote:
> 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.
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
This archive was generated by a fusion of
Pipermail (Mailman edition) and