A symbolic approach to abstract algebra in HOL Light

Abstract. Formalising algebraic structures (groups, rings, fields, vector spaces, lattices, . . . ) is known to be challenging task which is often under- taken by exploiting various kind of extra-logical mechanisms (axiomatic classes, modules, locales, coercions, . . . ) provided by most modern theo- rem provers. We want to explore an alternative strategy, where algebraic structures are implemented via a deep embedding of mathematical formulas and are managed as first class objects in the HOL theory. Along the way, we provide a mechanism of generalised conversions, which extends Paulson’s conversions by allowing to compute with equivalence relations. We developed generalised conversions to support rewriting in our system, but they can be used independently and may have an interest in its own.