[isabelle] Changing definition of finprod



Dear all,

recently I started to formalize linear algebra results based on HOL-Algebra (Matrices, Determinants, Eigenvalues, Gauss-Jordan-Elimination, â)

while doing this I noticed a annoying difference between setprod and finprod (or setsum and finsum):
the set-based variants define the sum or product of an infinite set as the neutral element, whereas finsum and finprod take âundefinedâ.

To have more similarity between the two operators I propose to change the definition of finprod from âundefinedâ to 1 (which entails 0 for finsum).

Then a lot of lemmas for finprod and finsum can be simplified where often the assumption âfinite Aâ is now obsolete (and they more closely relate to corresponding setprod and setsum lemmas).

If this change is appreciated, then can someone please include the following patch?
It adapts all of HOL/Algebra to the change and also those entries of the AFP which rely on HOL-Algebra still compile
(Free-Groups Jordan_Hoelder Koenigsberg_Friendship Lehmer Matrix Perfect-Number-Thm Secondary_Sylow Tarskis_Geometry VectorSpace)

I tested everything with Isabelle 8614f8f0fb4b and AFP 7c57eabaad4b.

Best regards,
RenÃ

Attachment: finprod.patch
Description: finprod.patch



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