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