This sounds like a good proposal to me. Do we have time before the fork?
Larry
Begin forwarded message:
From: Thiemann, Rene rene.thiem...@uibk.ac.at
Subject: [isabelle] Changing definition of finprod
Date: 17 April 2015 10:55:32 BST
To: Cl-isabelle Users cl-isabelle-us...@lists.cam.ac.uk
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é
finprod.patch
Description: Binary data
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
