1: \begin{abstract}

2: Previous formulations of group theory in ACL2 and Nqthm, based on either {\tt encapsulate} or {\tt defn\-sk}, have been limited by their

3: 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

4: 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

5: theory that remedies this deficiency, based on an explicit representation of a group as an operation table.  We define a {\tt defgroup} macro

6: for generating parametrized families of groups, which we apply to the additive and multiplicative groups of integers modulo $n$, the symmetric

7: groups, arbitrary quotient groups, and cyclic subgroups.  In addition to a proof of Lagrange's Theorem, we provide an inductive proof of

8: a theorem of Cauchy: {\it If the order of a group $G$ is divisible by a prime $p$, then $G$ has an element of order $p$.}

9: \end{abstract}

10: