A Formalization of Finite Group Theory

Previous formulations of group theory in ACL2 and Nqthm, based on either encapsulate or defnsk, have been limited by their failure to provide a path to proof by induction on the order of a group, which is required for most interesting results in this domain beyond Lagrange's Theorem (asserting the divisibility of the order of a group by that of a subgroup). We describe an alternative approach to finite group theory that remedies this deficiency, based on an explicit representation of a group as an operation table. We define a defgroup macro for generating parametrized families of groups, which we apply to the additive and multiplicative groups of integers modulo n, the symmetric groups, arbitrary quotient groups, and cyclic subgroups. In addition to a proof of Lagrange's Theorem, we provide an inductive proof of a theorem of Cauchy: If the order of a group G is divisible by a prime p, then G has an element of order p.