[isabelle-dev] HOL/Rings.thy: {left,right}_distrib
Tobias Nipkow
nipkow at in.tum.de
Tue Oct 16 17:43:19 CEST 2012
Am 16/10/2012 13:22, schrieb Tjark Weber:
> Hi,
>
> Class semiring in HOL/Rings.thy [1] assumes
>
> left_distrib: "(a + b) * c = a * c + b * c"
> right_distrib: "a * (b + c) = a * b + a * c"
>
> This is different from the terminology used in Wikipedia [2],
> MathWorld [3] and much of the literature, which call the first
> property right distributive, and the second left distributive.
>
> The difference in terminology becomes more than just slightly
> confusing when one wants to define near-semirings [4] and related
> structures, which satisfy only one of the two distributive laws.
>
> A rose by any other name would smell as sweet. Any opinions on
> swapping the names above?
We should certainly not contradict the mathematical usage. I favour Jasmin's
proposal because distributivity is such a well-known notion that I would not
like to get rid of it. The convention followed so far (at least losely) has been
to use "distrib" for + and *, and to mention the operators explicitly otherwise,
eg add_divide_distrib and power_mult_distrib. Except for the length, that seems
quite sensible.
Tobias
> Best regards,
> Tjark
>
> [1]
> http://isabelle.in.tum.de/repos/isabelle/file/4a15873c4ec9/src/HOL/Rings.thy#l17
> [2] http://en.wikipedia.org/wiki/Distributive_property#Definition
> [3] http://mathworld.wolfram.com/Distributive.html
> [4] http://en.wikipedia.org/wiki/Near-semiring
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
More information about the isabelle-dev
mailing list