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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
