Re: [isabelle] How to use setsum for set addition?

Hi Bogdan,

the SetsAndFunctions theory already contains (among others) the following:

interpretation set_comm_monoid_add: comm_monoid_add "op ⊕ ::
('a::comm_monoid_add) set => 'a set => 'a set" "{0}"

I.e., the comm_monoid_add structure is interpreted on the set
operations, which gives you plenty of theorems:

find_theorems name: set_comm_monoid_add

A little bit unfortunate, the setsum on sets is represented as
"comm_monoid_add.setsum set_plus {0}" (*), but you can syntactically fix
this by introducing an abbreviation:

abbreviation "set_setsum ≡ comm_monoid_add.setsum set_plus {0}"

Now everything looks quite fine

find_theorems name: set_comm_monoid_add

If this abbreviation does not solve your issue, I can provide you with a
modified theory where set_setsum is a proper constant (this will be part
of the next Isabelle release).

Hope this helps,

(*) called a foundational term in Isabelle parlance



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.