Email Gateway (Aug 22 2022 at 19:01): Email Gateway (Aug 22 2022 at 19:01):From: "John F. Hughes" <jfh@cs.brown.edu>
I'd like to be able to do the kind of thing done in most abstract algebra
texts when they're introducing groups, namely, say something like "the
integers, with negation and addition, and 0 as the identity element,
constitute a group, indeed, an abelian group." That's a tiny theorem,
right? We have to show that there is an identity (easy), that there are
inverses (again easy), that addition is associative (follows from
properties of the integers), and commutative (also easy). So it's easy, but
it's also something to be proved.
A little harder is showing that {Z, O, T} , a set of three distinct
elements (named to remind us of "zero, one, two", together with an
"inverse" function (inv(Z) = Z, inv(O) = T, inv (T) = O) and a "mul"
function (which I won't write out, but it corresponds to addition mod 3) is
actually an abelian group. The only real messiness is in proving
associativity of the "multiplication" operation, for which we can no longer
rely on properties of the integers.
Is there a way to state or prove either of these small theorems using, say,
the HOL/Groups.thy as a starting point?
[My real interest is in showing that certain things are projective
geometries, but the methods should be very similar, I hope.]
--John
Email Gateway (Aug 22 2022 at 19:01):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear John,
I’m not sure what exactly you’re aiming at:
Definitely there are Isabelle classes for groups, abelian groups, etc.,
and the integers with 0, +, - satisfy these laws as is shown in the Isabelle distribution.
Moreover, also modulo-rings like int mod 3 have been formalized and instantiated.
For instance, in AFP/Berlekamp_Zassenhaus/Finite_Field you find modulo-rings,
prime fields, etc. with instance-proofs.
There is also a locale-based hierarchy on groups, … in HOL-Algebra.
Hope this helps,
René
signature.asc
Email Gateway (Aug 22 2022 at 19:01):From: Lawrence Paulson <lp15@cam.ac.uk>
See below. I intend to include this in the Algebra library for the next release.
Larry
subsection‹The additive group of integers›
definition integer_group
where "integer_group = ⦇carrier = UNIV, monoid.mult = (+), one = (0::int)⦈"
lemma group_integer_group [simp]: "group integer_group"
unfolding integer_group_def
proof (rule groupI; simp)
show "⋀x::int. ∃y. y + x = 0"
by presburger
qed
lemma carrier_integer_group [simp]: "carrier integer_group = UNIV"
by (auto simp: integer_group_def)
lemma one_integer_group [simp]: "𝟭⇘integer_group⇙ = 0"
by (auto simp: integer_group_def)
lemma mult_integer_group [simp]: "x ⊗⇘integer_group⇙ y = x + y"
by (auto simp: integer_group_def)
lemma inv_integer_group [simp]: "inv⇘integer_group⇙ x = -x"
by (rule group.inv_equality [OF group_integer_group]) (auto simp: integer_group_def)
lemma abelian_integer_group: "comm_group integer_group"
by (rule group.group_comm_groupI [OF group_integer_group]) (auto simp: integer_group_def)
Last updated: Nov 21 2024 at 12:39 UTC