[isabelle-dev] HOL/Rings.thy: {left,right}_distrib
Tjark Weber
webertj at in.tum.de
Tue Oct 16 13:22:29 CEST 2012
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
More information about the isabelle-dev
mailing list