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

[Brian Huffman]

On Tue, Oct 16, 2012 at 1:22 PM, Tjark Weber <webertj at in.tum.de> wrote:
> 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?

I have always disliked these theorem names that include "distrib": It
makes the name longer without actually indicating which function is
involved.

Here are the names I would prefer:

mult_add_left: "(a + b) * c = a * c + b * c"
mult_add_right: "a * (b + c) = a * b + a * c"

The above names follow the pattern of many rewrite rules already in
the Isabelle libraries:

mult_zero_left: "0 * a = 0"
mult_zero_right: "a * 0 = 0"
mult_minus_left: "- a * b = - (a * b)"
mult_minus_right: "a * - b = - (a * b)"
Un_UNIV_left: "UNIV \<union> A = UNIV"
Un_UNIV_right: "A \<union> UNIV = UNIV"
Un_empty_left: "{} \<union> A = A"
Un_empty_right: "A \<union> {} = A"
Un_insert_left: "insert a B \<union> C = insert a (B \<union> C)"
Un_insert_right: "A \<union> insert a B = insert a (A \<union> B)"

etc, etc.

- Brian