3 Abstract Algebra I

However, the right way to formalise advanced algebra is not obvious. During the formal development the user has to decide how mathematical structures should be best organized in the proof assistant so that they can be used mechanically in an efficient way. It is well-known in the Isabelle community that the main algebra library needs to be rebuilt from scratch. In fact, there are many libraries for algebra in Isabelle: HOL-Algebra6 from the previous millennium (1999), the more recent HOL- Computational_Algebra7, and moreover some entries in the Archive of Formal Proofs8 like Groups, Rings and Modules [18] and Vector Spaces [21] among others. As a result, there is a lot of overlapping material, which makes the status of algebra confusing and unclear for the newcomer in the Isabelle world

-- Citation from Simple Type Theory is not too Simple

There is no point in studying legacy code. We will import code from outside of Main.

3.1 Semiring

The rest of

class semiring = ab_semigroup_add + semigroup_mult +
  assumes distrib_right [algebra_simps, algebra_split_simps]: "(a + b) * c = a * c + b * c"
  assumes distrib_left [algebra_simps, algebra_split_simps]: "a * (b + c) = a * b + a * c"
begin

text ‹For the ‹combine_numerals› simproc›
lemma combine_common_factor: "a * e + (b * e + c) = (a + b) * e + c"
  by (simp add: distrib_right ac_simps)

end