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

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

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