Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Semirings in HOL/Algebra/Ring


view this post on Zulip Email Gateway (Aug 19 2022 at 17:32):

From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
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é

view this post on Zulip Email Gateway (Aug 19 2022 at 17:32):

From: Larry Paulson <lp15@cam.ac.uk>
Looks like a good idea to me. Are there any drawbacks?
Larry Paulson


Last updated: Mar 28 2024 at 16:17 UTC