[isabelle-dev] HOL/Rings.thy: {left,right}_distrib

[Tobias Nipkow]

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
>