*To*: "Thiemann, Rene" <Rene.Thiemann at uibk.ac.at>*Subject*: Re: [isabelle] Semirings in HOL/Algebra/Ring*From*: Larry Paulson <lp15 at cam.ac.uk>*Date*: Fri, 27 Mar 2015 14:24:34 +0000*Cc*: Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <003D7F9D-E24A-4FEB-BB4B-BBF264448860@exchange.uibk.ac.at>*References*: <003D7F9D-E24A-4FEB-BB4B-BBF264448860@exchange.uibk.ac.at>

Looks like a good idea to me. Are there any drawbacks? Larry Paulson > On 27 Mar 2015, at 14:11, Thiemann, Rene <Rene.Thiemann at uibk.ac.at> wrote: > > Dear all, > > I wonder whether it is worthwhile to include the notion of a semiring into HOL/Algebra/Ring. > My motivation is an extension of the current AFP/Matrix-entry such that the elements of the matrices > don't have to be class-instances of class semiring, but that they are connected via a locale > semiring. However, currently such a locale does not exist > (only a locale for rings is defined, which rules out the natural numbers), one cannot conveniently study > the semiring of matrices of the natural numbers. > > To this end, I would like to modify the locale-structure in HOL-algebra as follows: > > An additional locale semiring: > > locale semiring = abelian_monoid R + monoid R for R (structure) + > assumes l_distr: "[| x â carrier R; y â carrier R; z â carrier R |] > ==> (x â y) â z = x â z â y â z" > and r_distr: "[| x â carrier R; y â carrier R; z â carrier R |] > ==> z â (x â y) = z â x â z â y" > and l_null[simp]: "x â carrier R ==> ð â x = ð" > and r_null[simp]: "x â carrier R ==> x â ð = ð" > > Prove the sublocale-property: > > context ring > > sublocale ring <= semiring > > ... > > > Prove several properties like finsum_ldistr already in semiring. > > Of course, I can also just copy HOL/Algebra/Ring and modify it locally, > but I believe that semirings should be valuable for other Isabelle users, too. > > If desired, I can update a recent repository version and discuss this change further on Isabelle-dev. > > Any comments are welcome, > RenÃ > > >

**References**:**[isabelle] Semirings in HOL/Algebra/Ring***From:*Thiemann, Rene

- Previous by Date: [isabelle] Semirings in HOL/Algebra/Ring
- Next by Date: [isabelle] Error using 'descending' to prove property over quotient
- Previous by Thread: [isabelle] Semirings in HOL/Algebra/Ring
- Next by Thread: [isabelle] Error using 'descending' to prove property over quotient
- Cl-isabelle-users March 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