*To*: Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] Changing definition of finprod*From*: "Thiemann, Rene" <Rene.Thiemann at uibk.ac.at>*Date*: Fri, 17 Apr 2015 09:55:32 +0000*Accept-language*: de-DE, de-AT, en-US*Thread-index*: AQHQePSkJQcbFTL/EES1JH/JTQ+IVw==*Thread-topic*: 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**

- Previous by Date: Re: [isabelle] Isabelle2015-RC0 available for testing
- Next by Date: [isabelle] Isabelle: A logic of total functions (?)
- Previous by Thread: [isabelle] CICM 2015 Doctoral Programme [Second Call for Applications]
- Next by Thread: [isabelle] Isabelle: A logic of total functions (?)
- Cl-isabelle-users April 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list