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


(*) called a foundational term in Isabelle parlance

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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