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

[Jasmin Christian Blanchette]

Hi Tjark,

Am 16.10.2012 um 13:22 schrieb Tjark Weber:

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

My only opinion is that the "swapping" should be done by inventing new names first, e.g. "distrib_left" and "distrib_right", so that porting is an idempotent operation. Whether the old names should be temporarily available for compatibility, and whether "distrib_xxx" should later be renamed "xxx_distrib", are questions where I have no ready-made answer.

Jasmin