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