Re: [isabelle] Symmetric Difference of sets



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,
- Brian

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.
>
> Thanks,
>
> Iain
> --
> 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 MHonArc.