[isabelle-dev] Fwd: [isabelle] Changing definition of finprod

Larry Paulson lp15 at cam.ac.uk
Fri Apr 17 12:22:02 CEST 2015


This sounds like a good proposal to me. Do we have time before the fork?
Larry

> Begin forwarded message:
> 
> From: "Thiemann, Rene" <Rene.Thiemann at uibk.ac.at>
> Subject: [isabelle] Changing definition of finprod
> Date: 17 April 2015 10:55:32 BST
> To: Cl-isabelle Users <cl-isabelle-users at 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é
> 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: finprod.patch
Type: application/octet-stream
Size: 1830 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20150417/efcf3d6a/attachment.obj>
-------------- next part --------------
> 



More information about the isabelle-dev mailing list