# [isabelle] Semirings in HOL/Algebra/Ring

*To*: Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>
*Subject*: [isabelle] Semirings in HOL/Algebra/Ring
*From*: "Thiemann, Rene" <Rene.Thiemann at uibk.ac.at>
*Date*: Fri, 27 Mar 2015 14:11:24 +0000
*Accept-language*: de-DE, de-AT, en-US
*Thread-index*: AQHQaJfokWd2Wm8XskOwPvX+lGw02g==
*Thread-topic*: Semirings in HOL/Algebra/Ring

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Ã

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*