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
