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



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Ã
> 
> 
> 





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