Exploring the Structure of an Algebra Text with Locales

Abstract

Locales, the module system of the theorem prover Isabelle, were designed so that developments in abstract algebra could be represented faithfully and concisely. Whether these goals were met is assessed through a case study. Parts of an algebra textbook, Jacobson’s Basic Algebra, that are challenging structurally were formalised. Key parts of the formalisation are presented in greater detail. An analysis of the work from both qualitative and quantitative perspectives substantiates that the design goals were met. In particular, the size ratio of formal to “pen and paper” text does not increase when going further into the book. The analysis also yields guidance on locales including patterns of use, which are identified and described.

1 Introduction

Locales are the module system of the theorem prover Isabelle. Since their conception in the late nineties [18] locales have seen a considerable evolution from the initial design. Today, locales are widely used. A count in January 2019 yielded that 219 of the 455 entries of the Archive of Formal Proofs (www.isa-afp.org, development version) use locales.¹ The proportion of entries declaring locales is roughly 50% across the domains of Computer Science, Logic and Mathematics, which are distinguished in the archive. Only for Tools the proportion is significantly lower with only three of the 13 entries containing locale declarations.

The services provided by locales go beyond those of module systems known from programming languages. They are integrated with Isabelle’s proof language Isar and are designed to provide adequate support for reasoning about algebraic structures. The objective of the study presented here is to gain confidence that this is the case. A fragment of a mathematics textbook is translated into a formal, machine-checkable document in a faithful manner. That is, definitions in the formal document should reflect those of the mathematical text and likewise the formal proofs follow their informal counterparts closely. The challenge sought is finding an adequate module structure for the “pen-and-paper” text reflecting the concepts found there—with the purpose of understanding the capabilities of locales. For the module structure to be considered adequate, objects of discourse, algebraic structures and their elements, should be similarly concise and no significant additional proof work should be required in the formal text. On the other hand, we do not worry about the precise notation of the objects of discourse and also take into consideration that proof scripts tend to be longer than informal proofs.

What would be a suitable text for such a study? It should, of course, be from the domain of abstract algebra. For practical reasons it should be self-contained and of moderate size. This suggests fairly elementary material from an algebra textbook. The first volume of Jacobson’s Basic Algebra [16] was chosen, mostly due to the author’s familiarity with the book. The text is demanding from the outset (especially for a computer scientist) and is probably not the preferred choice of text for a regular formalisation effort, where a low-level style is of advantage.

The formalised fragment stretches over a bit more than the first one hundred pages of the book. As a continuous body it would amount to 11.4 pages. It covers monoids, groups and rings and arrives at the fundamental theorems of homomorphisms of each of these structures. The choice enables studying how constructions for algebraic structures build on top of each other. For the purpose of this study, it does not matter that similar material has been formalised before.

The report starts with an introduction to locales. A walk through the formalised material follows. Space constraints do not permit going through the entire body. Key parts are presented, and the focus is on the role of locales. In the subsequent review the formalisation is assessed based on the goals set out above. Changes to the locale implementation that were triggered by the work are briefly explained, and usage patterns of locales identified in the work are presented. A discussion of what can be learnt from the case study concludes the analysis.

The discussed formal proof documents are available in the Archive of Formal Proofs [7].

2 Locales

Locales are an extension of Isabelle’s Isar proof language [25] by means of manipulating “knowledge containers” or modules, which were designed for representing algebraic structures. The central concept is the locale, a theory functor that maps parameter operations (or simply parameters) and a specification to defined operations (involving the parameters) and theorems (implied by the specification). A sketch of locales follows. My detailed account on the semantics of locales is the exhaustive reference [6]. There, locales are also related to ML-style module systems [15] and other means of reuse in both provers and programming languages.

2.1 Declaring Locales

In its simplest form, a locale declaration consists of a and an clause:

The $\overline{y}$ are the parameters and $A_1 \wedge \cdots \wedge A_j$ is the specification of the locale. The $A_i$ are versions of the user input where free variables except parameters are universally closed. They are also called axioms or assumptions of the locale. For example, a locale for monoids may be declared like this:²

Types, in particular types of the parameters, may be left implicit. They are inferred automatically. The theory of a locale n is elaborated in context blocks:

The locale n is the target of the block. These commands are available in context blocks:

The first command, , declares a new defined operation c with defining equation $c \equiv t$ and optional concrete syntax; enables changing the concrete syntax of an existing operation; introduces a theorem B named b. Declarations in a context block are persistent—that is, they are present in subsequent context blocks of the same target. Parameters and specification of a locale are the header, the collections of declarations made in its context blocks form the body.

Locales are hierarchic and a graph of interdependent locales is maintained by the system. Dependencies may be given when declaring a locale through a locale expression at the beginning of the declaration,

or between existing locales through a sublocale declaration:

Dependencies declared via the command are derived. The system creates a proof obligation, which must be discharged by supplying a proof. A locale expression consists of a sequence of locale instances followed by an optional clause:

A locale instance is either positional:

or by name:

Here, q is an optional qualifier, n the instantiated locale, $\overline{y}$ are its parameters, $\overline{t}$ terms from the target and $\overline{ eq }$ optional equations. Terms are substituted for the parameters of the instantiated locale—in the positional case, in declaration order of the parameters. The qualifier q, if present, is prepended to names of derived operations and of theorems. Qualifiers are used to distinguish multiple instances of the same locale. The purpose of the equations is explained below.

In a locale declaration, the clause defines the parameters $\overline{x}$ of the locale expression and the context of the locale instances.³ The expression denotes locale instances that are imported to the declared locale. That is, the specifications of the imported instances contribute to the specification of the declared locale, and their declarations (definitions and theorems) are available in its body. The following declaration involves an expression consisting of a single instance and a for clause:

The notation refers to the operation. As a notational convenience uninstantiated parameters in locale instances are implicitly added to the for clause. This is useful when constructing linear locale hierarchies—for example, the above declaration may be abbreviated to

albeit yielding the different parameter order .

The sublocale command lets one change existing locale hierarchies: for a locale n, modifies the graph of locales maintained by the system as if the declaration of the target n imported $expression$. This makes the bodies of the instantiated locales available in n (the target of the operation). For example,

asserts that the carrier set of the submonoid and the monoid operations indeed form a monoid. The notational variant is available in context blocks, and the command applies to the target of the block. The specification of the target is required to imply the specifications of the instantiated locales. Proof obligations are generated and must be discharged.

The sublocale command is not restricted to instantiating locale parameters; rewrites clauses in locale instances enable specifying rewrite rules for replacing defined operations of a locale by terms from the target. In combination with instantiation they provide signature morphisms [11] on locales. The rewrite rules yield additional proof obligations.

2.2 Reasoning with Locales

Locales are extra-logical. The functors they represent are not encoded in Isabelle’s logic. Instead, whenever a locale is visited—that is, a context block entered—the locale is activated:

• The locale graph is traversed and all reachable locale instances are activated recursively.

• The body of the locale is added to the context, making its declarations available.

The precise working of activation is described in my detailed account [6].

Activation of a locale initialises a context, so it can be worked in. It is also possible to activate additional locale instances in the current context, which can be a theory, a context block or a proof. We will only encounter the command applicable in context blocks:

It enriches the current block by the information on the instances identified by $expression$ and stored in the respective locales. The operation is also known as theory interpretation [10]. The difference to the sublocale command is that its effect is temporary and limited to that block. The command does not change the locale hierarchy permanently.

We also need to briefly look at how the proof obligations created by and are represented. Each locale n is accompanied by a locale predicaten, which reflects the specification of n in the logic. The locale instance $n \, \overline{t}$ is represented by the proposition $n \, \overline{t}$. The method (which is integrated with Isabelle’s default method, so it rarely occurs explicitly in proof scripts) provides backward reasoning on locale predicates and is used for refining proof obligations. It reduces atomic propositions on locale predicates to locale axioms, on which then further reasoning can take place. For a locale that imports a hierarchy of locales, this includes corresponding instances of axioms of the imported locales. The method is aware of the locale instances that are active in the current context and discharges matching subgoals during the reduction process automatically. The latter enables a technique called bootstrapping, which will be discussed in the course of the paper.

3 The Formalisation

The formalised material is from the first three chapters of Jacobson’s Basic Algebra I [16] and covers all that the author undertakes to arrive at the fundamental theorem of homomorphisms of rings, also known as the universal property of ring homomorphisms. Cosets are introduced as orbits of translations, and so we can afford a short detour to Cayley’s theorems for monoids and groups.

Fig. 1

Locale hierarchy of maps and monoid homomorphisms.

means that y imports x,

that the relationship is established through a sublocale declaration. Bijective maps are directly based on maps rather than on surjective and injective maps. This is to make better use of knowledge on bijective functions already available in Isabelle

3.1 Concepts from Set Theory

In Isabelle/HOL denotes the set of functions with domain and co-domain . Extensionality is achieved by mapping values outside to an arbitrary but fixed value about which nothing can be proved [12]. Elements of are obtained with bounded abstraction . Composition is defined as and is the image of under . Since an element of does not encode its domain, occasionally it needs to be made explict, such as in . Rather than developing maps from scratch the existing concepts are used. The declaration

enables working with maps at the level of locales. Locales for injective, surjective and bijective maps are declared as well. Figure 1 shows the hierarchy of these locales, along with those of monoid homomorphisms, which are introduced later.

Jacobson’s treatment of equivalence classes [16, p. 11] is interesting enough to warrant its formalisation. He simultaneously develops the concepts of equivalence relation E on and partition P of a set S and then shows that they are equivalent. Both are straightforwardly translated to locales, and , respectively. In the context of the natural map is defined as

and the quotient set S / E is the associated partition into classes:

That and are the same thing is asserted through suitable mutual sublocale declarations.

The next topic is factoring a map through an equivalence relation. Every map $\alpha$ gives rise to an equivalence relation $E_\alpha$ in S where $a E_\alpha b$ if and only if $\alpha (a) = \alpha (b)$. It is convenient to analyse this situation in a dedicated context:

Both locales have the same parameters and specification but their bodies differ; is a clone of . While inherits the declarations of the latter does not inherit the declarations of the former. The context is declared a sublocale of an instance of with $E_\alpha$ as the relation.

The map $\alpha$ gives rise to the induced map $\bar{\alpha }$ on the quotient set such that $\bar{\alpha }(\bar{a}) = \alpha (a)$. With the above sublocale declaration the definition of the induced map is

where now represents the quotient set $S / E_\alpha$ and is the definite selection operator. Reasoning about functions defined on equivalence classes can be technically challenging [21]. The theorem

leads to concise proof scripts. Used as an elimination rule, a goal about an arbitrary element of the quotient set is reduced to a goal about an element of the underlying set. Theorems on the factorisation of $\alpha$ into natural and induced maps follow.

Sublocale declarations assert surjectivity and injectivity of the involved maps:

This completes the statement of the universal property of the map $\alpha$.

3.2 Abstract Monoids and Groups

Jacobson’s definitions of monoids and groups and the associated substructures can be expressed with locales in a straightforward manner. For the corresponding monoid locales, see the examples in Sect. 2.2. The notions of invertibility and inverse are defined in the context of monoids:

Then, following Jacobson, “a group G (or (G, p, 1)) is a monoid all of whose elements are invertible” [16, Def. 1.2]:

Further “a submonoid of a monoid M [is] a subgroup if, regarded as a monoid, it is a group” [16, p. 31]:

The inverse operations of the group and the subgroup are different, even though Jacobson does not make this explicit. The lemma

helps simplify expressions in subgroups involving both group and subgroup operations.

Jacobson’s unusual decision to define the inverse operation rather than make it a parameter of the structure poses no problems to locales. In a sublocale declaration or interpretation the operation can be mapped to an operation from the target context via a rewrites clause.

3.3 Monoids and Groups of Transformations

For monoids and groups of transformations, which are monoids and groups whose elements are maps (or transformations) on some set S, the translation into locales is less obvious. For a set S the set M(S) of maps of S into itself forms a monoid. This is the monoid of all transformations. Composition is the binary operation and the identity map the unit element. A submonoid of M(S) is called a monoid of transformations [16, p. 29].

The formalisation starts with a locale that postulates the set S:⁴

The type constraint ensures that is a set. The monoid of all transformations is identified in the context:

The locale for a transformation monoid M of S follows:

Similarly, the invertible elements of the monoid of all transformations M(S) form a group, the symmetric group$\mathop {\mathrm {Sym}} S$:

is defined in the context of and denotes the invertible elements of . In the formalisation, the parameter of is implicit. The locale for a transformation group G of S follows:

3.4 Isomorphism. Cayley’s Theorem

“Two monoids (M, p, 1) and $(M, p', 1')$ are said to be isomorphic if there exists a bijective map $\eta$ of M to $M'$ such that $\eta (1) = 1'$, $\eta (xy) = \eta (x)\eta (y)$, $x, y \in M$” [16, Def. 1.3]. The definition straightforwardly translates into a locale declaration:⁵

The monoid locales are distinguished by suitable qualifiers, and adequate notation is provided.

“Any monoid is isomorphic to a monoid of transformations” and “any group is isomorphic to a group of transformations” [16, Cayley’s theorem]. In the proof, an isomorphism from the monoid (M, p, 1) (or group (G, p, 1)) to a monoid (or group) of transformations of the set M (or G) is defined. The isomorphism takes an element a to the map $a_L : x \rightarrow ax$, called the left translation of a.

The formalisation takes place in the contexts of dedicated clones of locales of monoids and groups for left translations, in the monoid case,

and the subsequent statements will be in this context. First,

is defined, and will be used to denote . The proof that this function is the required isomorphism is prepared in a sequence of three sublocale declarations, where each enriches the context to simplify the subsequent proofs.

The line of reasoning follows that of Jacobson. First the context is extended by the monoid of all transformations of . The proof is trivial since has no assumptions. It is then shown that the image of under , is a submonoid of the monoid of all transformations and therefore a monoid of transformations. That is an isomorphism comes next, and the third sublocale declaration asserts that a translation is a map.

This concludes reasoning in . Building up the context in several steps, here through sublocale declarations, I call bootstrapping.

In the final step, the result is transferred to by means of a temporary interpretation:

With this technique, which I call loose coupling, left translations are kept separate from monoids.

The corresponding work for groups takes place in and builds on the monoids case:

In addition to the monoid case it needs to be shown that is a transformation group. Since has the inverse for all the are bijective and is closed under inverses. No additional work on the isomorphism property is required. Cayley’s theorem for groups follows, again by means of a temporary interpretation, in the locale.

3.5 Orbits. Cosets of a Subgroup

For any transformation group G of a set S the relation $\sim _G$ on S, where $x \sim _G y$ if $y = \alpha (x)$ for some $\alpha \in G$, is an equivalence relation. The equivalence classes are called the G-orbits and constitute a partition of S [16, p. 51]. The correct context for the formalisation is :

With these declarations denotes the orbit of an .

Right cosets $Hx = \{hx \mid h \in H\}$ are defined in the context of a subgroup H of a group G and are the orbits of left translations [16, p. 52]:

In the formalisation right cosets are denoted by rather than, for example, . This is achieved by pulling the declaration up to an auxiliary locale where is not a parameter.

Now for the correspondence to orbits. Let $G_L$ be the left translations of G. The subset $H_L(G)$ of left translations $h_L$ (in G) for $h \in H$ is a subgroup of $G_L$ and hence a group of transformations of G.

Here denotes $H_L(G)$. The $H_L(G)$-orbit of $x \in G$ is the right coset Hx

The number of distinct cosets [G : H] is called the index of H in G. For finite groups Lagrange’s theorem $|G| = |H|[G : H]$ follows:

This concludes the section on right cosets. The index is defined as the cardinality of the partition . In the context of it has no parameters.

3.6 Congruences. Quotient Monoids and Groups

For a monoid $(M, \cdot , 1)$ a congruence E is an equivalence relation that respects composition—if $(a, a') \in E$ and $(b, b') \in E$ then $(a \cdot b, a' \cdot b') \in E$ [16, Def. 1.4]. Composition in M can be lifted to a binary operation $\bar{\cdot }$ of the quotient set M / E, yielding the quotient monoid $(M / E, \bar{\cdot }, \bar{1})$. If the monoid is a group the construction yields a group.

The formalisation takes place in two locales:

The lifted binary operation is defined in and denoted with square brackets:

denotes the natural map and the quotient set M / E (see Sect. 3.1). The operation maps into the quotient set and commutes with the natural map:

That the quotient construction yields a monoid is expressed through a sublocale declaration:

In the group case additionally “every $\bar{a}$ is invertible and its inverse is $\overline{a^{-1}}$” [16, p. 55]

and the construction yields a group:

For groups, an alternative characterisation of congruences exists. “A subgroup K of G is said to be normal [...] if $g^{-1}kg \in K$ for every $g \in G$ and $k \in K$” [16, Def. 1.5],

and there is a one-to-one correspondence between group congruences and normal subgroups: “Let G be a group and $\equiv$ a congruence on G. Then the congruence class $K = \bar{1}$ of the unit is a normal subgroup of G and for any $g \in G$, $\bar{g} = Kg = gK$ [...]. Conversely let K be any normal subgroup of G, then $\equiv$ defined by $a \equiv b$ if $a^{-1}b \in K$ is a congruence relation in G whose associated congruence classes are the left (or right) cosets gK” [16, Thm. 1.6]. As a consequence, results on normal subgroups are applicable to group congruences and vice versa. In the formalisation, results are made available to both contexts through mutual sublocale declarations.

Work for the direction from congruences to normal subgroups takes place in where represents Jacobson’s K. First

provides coset notation. Then and are shown and

follows. The other direction takes place in where is defined as $a \equiv b$ if $a^{-1}b \in K$. The latter “is equivalent to saying that $b \in aK$, or that b is in the orbit of a relative to the transformation group $K_R(G)$” [16, p. 56].⁶

The rewrites clause effectuates the replacement of the transformation group’s equivalence relation by .

The orbit of a transformation group is an equivalence, and since K is a normal subgroup it is also a congruence:

This concludes the formalisation. Intermediate results temporarily provided by the interpretation commands are either no longer required (transformation groups) or are subsumed by later sublocale declarations ( is a subgroup).

3.7 Homomorphisms

The fundamental theorems of monoid, group and ring homomorphisms are variants of the factoring of a map $\alpha$, through the equivalence relation $E_\alpha$, into a surjective natural map and an injective induced map (Sect. 3.1). The involved sets are algebraic structures and the maps homomorphisms between them.

Homomorphism locales build on those of the respective maps. The locale for monoid homomorphisms is analogous to that for isomorphisms (see Sect. 3.4) but is based on instead of . Locales for monoid monomorphisms (injective) and epimorphisms (surjective) are declared as well. The hierarchy of the declared locales is shown in Fig. 1. The fundamental theorem of homomorphisms of monoids [16, p. 61] states that a homomorphism $\eta$ of a monoid M into a monoid $M'$ can be factored, in a unique manner, into an epimorphism $\nu$ and a monomorphism $\bar{\eta }$. The formalisation takes place in the dedicated context

and consists of a sequence of sublocale declarations. The factoring is through the equivalence relation $E_\eta$ and

extends the context with the associated declarations and results. Recall from Sect. 3.1 that denotes the natural map $\nu$, the induced map $\bar{\eta }$ and the quotient set $M/E_\eta$. The equivalence, denoted by , is a congruence

and therefore $M/E_\eta$ a monoid. That the natural and induced maps are homomorphisms is now immediate:

The same reasoning is applicable to group homomorphisms, and Jacobson also works out the details for that. He then presents a second proof, without recourse to congruences, where the factor group G / L, for some normal subgroup L of G contained in the kernel $\ker \eta$ of $\eta$, replaces the quotient group. The formalisation for groups follows the second approach, and the locale reflects the described situation:

The fundamental theorem follows for $L = \ker \eta$:

3.8 Rings

Jacobson’s definition of rings is: “A ring is a structure consisting of a non-vacuous set R together with two binary compositions $+$, $\cdot$ in R and two distinguished elements $0, 1 \in R$ such that 1. $(R, +, 0)$ is an abelian group. 2. $(R, \cdot , 1)$ is a monoid. 3. The distributive laws D $a(b+c) = ab + ac$ [and] $(b+c)a = ba + bc$ hold for all $a, b, c \in R$” [16, Def. 2.1]. It translates into the following locale:

The additive and multiplicative structures are identified by the qualifiers and , respectively. The declaration also shows how notation for unary minus and inverse are obtained.

Ring congruences and homomorphisms are likewise composed from the respective structures of additive group and multiplicative monoid. Jacobson repeats the construction discussed at the end of the previous section for an ideal I contained in the kernel of the ring homomorphism $\eta$. This situation is represented by the locale . Finally, is the context in which the fundamental theorem of ring homomorphisms is stated and shown. Figure 3 shows the hierarchy of the involved locales.

4 Review

This study completes work the author had announced several years ago [5]. The formalisation effort is probably in the order of three person months.

Finding a suitable module structure for Jacobson’s text has not been straightforward. The interrelations are complex. Frequently, decisions had to be revised when it came to using concepts in later sections. The main difficulty was that, of course, the mathematical text does not make it explicit how knowledge needs to be structured so it can be re-used mechanically. An example are translations, which are instances of monoids and groups of transformations. They are instrumental in the proof of Cayley’s theorem and later in the characterisation of cosets as orbits. While translations are defined in the context of monoids, it turned out left and right translations better be declared in separate locales, so the knowledge specific to each could be activated individually when needed. On the other hand, the equivalence relation $\sim _G$ of a group G of transformations was defined in the locale for transformation groups and linked to the equivalence relation locale through a sublocale declaration, so this knowledge is automatically available for left and right translations. At times, several attempts to finding the right module structure were needed. To aid library design the concepts of clone and loose coupling were identified. They are explained below in Sect. 4.4.

Fig. 2

Locale hierarchy of congruences, normal subgroups and ideals

Fig. 3

Locale hierarchy of the fundamental theorem of ring homomorphisms

Insufficient means for configuring notation were another source of difficulty. This was a design flaw, which was corrected (see also Sect. 4.3). In spite of these difficulties the outcome of the case study is satisfactory. The formalisation is readable, concise, even polished and appears natural.

Figures 1, 2 and 3 show parts of the sublocale graph. The entire graph consists of 51 locales and is too large to reproduce. Table 1 shows examples of Jacobson’s notation and their correspondents in the formalisation. The latter is sufficiently concise, with one exception: the notion of invertibility for group transformations is . It occurs in the statement that left translations are invertible, which Jacobson spells out directly, without reference to this predicate. Since it occurs in a few isolated places only, there was no need for finding concise notation.

Table 1 Symbols in Jacobson’s text and their representation in the formalisation code

4.1 Representing Algebraic Structures

In Isabelle simple algebraic structures can be represented as type classes [13]. But since a type class can only have a single parameter, expressiveness is restricted—for example, univariate polynomial rings can be represented but not vector spaces in general.

Other approaches to abstract algebra in higher-order logic are based on representing structures as terms rather than types. They are all variations of a technique first worked out by Elsa Gunter in the domain of group theory.

4.1.1 Foundations

In Gunter’s formalisation [12] a group structure is a pair of carrier set and binary composition operation and ${ group } \$ a predicate whose definition is the group axioms: ${ group } \ \, (G, {\textit{prod}} \ )$ if and only if $(G, {\textit{prod}} \ )$ is a group. Defined operations—here, the identity element $id$ and the operation $inv$ mapping an element to its inverse—have the group structure as an additional argument. The definition of $inv$ illustrates this:

$$\begin{aligned} \mathop { inv } \mathcal {G} \, x \equiv \varepsilon y. \, y \in { fst } \ \mathcal {G} \wedge ({\textit{snd}} \ \mathcal {G} \, y \, x = \mathop { id } \mathcal {G}) \end{aligned}$$

For making the definitions, Hilbert’s indefinite choice operator $\varepsilon$ is employed.⁷

Gunter derives the fundamental theorem of group homomorphisms and thereby demonstrates that the approach is workable in principle. Theorems in the theory of groups are of the form ${ group } \ \mathcal {G} \Longrightarrow \cdots$, and the need for repeated explicit reference to the group structure makes statements unwieldy. For a limited scope of formalisation the problem can be addressed with ad hoc syntax translations quite successfully as demonstrated, for example, by work in the HOL4 system [9].

Locales are connected to Gunter’s approach through the concept of the locale predicate. For a locale n with parameters $\overline{x}$ theorems are internally also of the form $n \, \overline{x} \Longrightarrow \cdots$, but the context information is suppressed. While tuples could be used with locales, records or individual parameters are usually preferred.

4.1.2 Record Types

Replacing tuples by records is a straightforward variation, which allows for more suggestive notation such as ${\textit{prod}} \ \mathcal {G}$ instead of ${\textit{snd}} \ \mathcal {G}$. Syntax such as $x \cdot _{\mathcal {G}} y$ for ${\textit{prod}} \ \mathcal {G} \, x \, y$ becomes possible in a systematic manner. The use of records for representing algebraic structures in Isabelle was put forward by Kammüller [17]. Similar techniques for readable notation have also been employed early in type-theoretic provers [2].

Isabelle’s records are extensible, and this is useful for working with hierarchies of algebraic structures. However, Isabelle’s records only support single inheritance [20]—that is, a record declaration can only refer to one, not two or more, records for extension. Combining the ring structure from its additive group and multiplicative monoid substructures is not possible. This is a fundamental limitation. In Isabelle’s algebra library HOL-Algebra [8] this is worked around by extending the multiplicative monoid record by additive operations yielding the ring structure. A record for additive groups is not declared. Instead these have the ring structure type. The unused multiplicative operation fields are left undefined. The declaration of rings in the present study (Sect. 3.8) does not suffer from this limitation.

When using records, concrete syntax such as infix notation is declared outside of locales. Locales merely provide support for concise syntax for records through a special parameter annotation [3, Section 5]. The first annotated parameter is distinguished and can be omitted in theorem statements; $x \cdot _{\mathcal {G}} y$ can be written as $x \cdot y$ if $\mathcal {G}$ is the distinguished parameter. This is similar to but less elaborate than Coq’s canonical structures [19]. The notational improvement is limited. It is only effective for parameters. If $\mathop { Quot }$ maps a group $\mathcal {G}$ to its quotient group relative to a congruence $\mathcal {C}$ the composition of two elements of the quotient group would be denoted by $x \cdot _{\mathop { Quot }\mathcal {G} \, \mathcal {C}} y$.

4.1.3 Local Theories

With the introduction of local theories [14] defined operations became available in locales themselves. Previously, definitions had to be made outside of locales, and records offered a workable means of doing so. With local theories, a definition $c \equiv t$ in a locale n with parameters $\overline{x}$ yields the global definition

$$\begin{aligned} n \, \overline{x} \Longrightarrow n.c \, \overline{x} \equiv t[\overline{x}] \end{aligned}$$

of the qualified constant n.c. This is close to what Gunter did. Here, the definition takes place in the background. As in Gunter’s approach, it is lifted over the parameters. Additionally, it is logically restricted to $n \, \overline{x}$. Concise notation is achieved by presenting $n.c \, \overline{x}$ as c in the locale context.

Local theories enable representing both signature and theory of an algebraic structure solely with the facilities of locales. The present study demonstrates this approach and shows how concise notation is achieved. In contrast to records, with local theories syntax can be defined on a per-operation basis. This is more flexible than syntax declarations at the record level, but it may also yield more verbose locale declarations. The additional investment pays off easily with more concise notation in propositions and goal states. Analysing goal states is the bread and butter of interactive proof. Any effort to keep notation concise will quickly lead to increased productivity.

In the study, the need for tailored syntax has led to a significant amount of locale declarations that do not represent algebraic structures as such but nevertheless correspond to situations found in the formalised text. Examples are the locales and , which are clones of and , respectively, and also and . In total, 51 locales were declared in 2589 lines of formal text (1478 lines when empty lines and comments are excluded). This is significantly more than for comparable work. For example, HOL-Algebra, which is more than ten times larger, contained only 82 locales as of November 2018.

4.1.4 Interpretation

Interpretation is essential for transferring abstract results to situations of use, be they concrete or abstract themselves. The need was already recognised by Gunter, who presents instances of her group theory development for the integers and modular arithmetic [12, Appendices D and E]. How the interpreted theories were arrived at is not recorded. Presumably appropriate code for creating them was provided in ML, the meta language of the HOL system.

The interpretation facilities of locales proved flexible enough for representing Jacobson’s lines of argument faithfully through the formalised sections of his book. Notable examples of interpretation are encountered when the properties of quotient structures are established and when transformation groups are used. The latter are key to Cayley’s theorem and, since cosets are the orbits of group elements under translation, also to Lagrange’s theorem.

The initial design of locales [18] did not provide interpretation. Incidentally, Kammüller and Paulson show that the quotient construction over a group yields a group but do not make use of that result.⁸ Their proof of Lagrange’s theorem is elementary. It does not make the notion of transformation group explicit. The lack of interpretation is also apparent in their proof of Sylow’s first theorem. The formalised proof, due to Wielandt, is based on the action of the group, by left translation, on a set of subsets of certain cardinality. Jacobson outlines the technique [16, p. 83]. The required concepts are encoded in the locales and , which describe the specific group action required in that proof. Only later, when locale interpretation was available, von Raumer [24] factored out the concept of group action in his formalisation of further Sylow theorems and applied it, via interpretation, in the various proofs.

4.2 Quantitive Analysis

Locales seek to aid formalisation of mathematics in two ways: through concise and readable syntax for the objects of discourse, and by facilitating reuse throughout a mathematical development. Both are expected to have an impact on the size of a formal development.

4.2.1 Notation

Locales succeed at hiding the complex nature of objects of discourse. For example, for a normal subgroup K multiplication of cosets enjoys the property $(gK)(hK) = ghK$. In the presented formalisation, within , this statement is

and consists of 49 characters including whitespace. In contrast, the fully expanded internal version is quite large:

This is partly due to the module system relying on qualified names for accommodating name spaces and long parameter names. Gunter’s version of the same statement [12, p. 28, theorem QUOT_PROD], while being considerably shorter, has the same structure:

By dropping qualifiers and using short parameter names a shortened statement can be arrived at. It is of similar size than Gunter’s (150 vs. 146 characters):

An evaluation of the effect of locales on statement size by direct comparision of this study with Gunter’s work is not possible—her work only covers group theory and further is based on a different textbook, so most theorem statements differ fundamentally—yet it emerges from the above consideration that for a direct formalisation of Jacobson’s text using Gunter’s approach theorem sizes can be expected to be roughly like those of the shortened internal versions of the present study. Table 2 gives an overview over the 175 theorems of the study. Column (a) lists the size reduction with respect to the full, column (b) with respect to the shortened internal versions. For a direct formalisation using Gunter’s approach statements up to 5.7 times the size when using locales can be expected.

Table 2 Count of theorems and their reduction in size between non-locale and locale version

4.2.2 Structure

The ultimate benchmark is the mathematical text itself. For van Benthem Jutting’s formalisation [23] of Landau’s textbook Grundlagen der Analysis on complex arithmetic, the sizes of the Automath code and the formalised source were compared. According to Wiedijk [26], de Bruijn calls what is lost in conciseness in the translation the loss factor and observes that it is constant: “it does not increase if we go further in the book”. Wiedijk popularised de Bruijn’s loss factor as de Bruijn factor.

For the present study, in the Isabelle theory files each declaration is annotated with the corresponding source location (page and line numbers) in the textbook. Further, statements found there explicitly are marked as theorems (unless they have been translated in locale constructs) others as lemmas. This makes the correspondence very explicit, and has been helpful in keeping organised. It also enables providing quantitative information. 400 lines of Jacobson’s text, which corresponds to 11.4 pages of 35 lines each, were formalised, yielding about 1500 lines of formal development. Empty lines, source code comments and other passages of English text in the code are excluded from this count.

A precise breakdown is shown in Table 3. For the identified sections the ratio between code and text size (measured in lines) ranges from 1.0 to 6.5, except for right translations, which are left as an exercise to the reader, and for which the ratio therefore is much higher—28. It can be noted that the ratio is generally higher for sections on groups than on monoids. Certainly the need for numerous technical lemmas to simplify computation in abstract groups and the fact that the work on group homomorphisms is not based on that on monoid homomorphisms play a role here. On the other hand, the ratio drops again for the sections on rings, and we can conclude that as for van Benthem Jutting’s formalisation the ratio does not increase further into the text and reuse of monoid and group parts for rings works well.⁹

Table 3 Line count of Isabelle code compared to Jacobson’s text. Excludes empty lines, comments in source code etc

4.3 Improvements to Locales

The case study triggered improvements to locales, and in comparison to my detailed account on locales [6] these changes were made:

• The keyword for rewrite clauses was changed, from to . This improves the readability, in particular of named locale instances, which now use exclusively.

• Handling of syntax was modified so that can be used for changing notation. Previously was used. Syntax in locales is now more flexible. Notation can be more natural and conciser.

• It was necessary to make rewrite clauses part of locale instances. Previously, rewrite rules were processed after instantiation. The new approach is conceptually cleaner and provides means for avoiding syntax conflicts while locale expressions are parsed.

These changes had only a small impact on existing formalisations. The renamings required for the first change in the Isabelle distribution and the Archive of Formal Proofs could be handled in about one day. The other improvements are direct outcomes of the present study and were required for its successful completion. They were published with Isabelle 2016 and 2018 respectively. While the second change had no impact on existing developments in the Isabelle distribution and the Archive of Formal Proofs at all, it was important to ensure that it introduced no changes in the rendering of proof states. The third change did require surprisingly few isolated changes, which were not difficult to make.

4.4 Reasoning Patterns

Certain locale constructions were used repeatedly in the study. They are identified here to provide guidance. In the diagrams, in addition to the arrows

for import and

for sublocale declarations,

denotes temporary interpretation.

4.4.1 Clone

A clone y of a locale x is obtained as follows:

Both locales have the same parameters and specification, but their bodies differ. While y inherits all declarations of x, the latter does not inherit any of the former. Clones are useful for knowledge separation. Knowledge that is implied by a specification but does not belong to its main body, for example, might better be placed inside a clone. Clones may also be necessary for avoiding infinite chains of interpretation [4, Section 7.1].

The study contains several instances of the clone pattern. For example, (Sect. 3.1) is a clone of , (Sect. 3.4) a clone of , and the locales for the fundamental theorems of homomorphisms (Sects. 3.7 and 3.8) are clones of the respective homomorphism locales.

4.4.2 Bootstrapping

Let $x_1, \ldots , x_n$ be a locale hierarchy and the goal to interpret $x_n$, via some morphism $\phi$ in y. Let $\phi x_i$ denote the locale instance obtained by applying $\phi$ to the parameters (and defined operators) of $x_i$. Establishing the interpretations $\phi x_1, \ldots , \phi x_n$ one after the other may be significantly simpler then showing $\phi x_n$ directly. Be it that notation is introduced that makes the subsequent proof more concise, be it that suitable knowledge is introduced or, as happens frequently, both. In analogy to the start up of a computer system, where simple software enables the loading of more complex software from an input device, this process is called bootstrapping. In the context of y

is established subsequently for $i = 1, \ldots , n -1$ and

follows eventually. All interpretations but the final one may be temporary.

In the study, bootstrapping occurs in several places. A prominent example is discussed in Sect. 3.6 where in the context of three sublocale declarations lead to the statement that left translations are monoid isomorphisms.

4.4.3 Functor

Let $x_1, \ldots , x_n$ and $y_1, \ldots , y_n$ be hierarchies of algebraic structures represented by locales, and let $\phi$ be a functor from $(x_i)$ to $(y_i)$. For example, let $(x_i)$ and $(y_i)$ be ring hierarchies and $\phi$ denote the construction of univariate polynomials. The connection of the hierarchies is achieved by a sequence of declarations

All instances $\phi x_i$ will share the same qualifier, which is indicated by the letter q in the diagram. In practice, declarations for the construction of $\phi$ lead to a hierarchy $y_1', \ldots , y_n'$ of locales in which the sublocale declarations take place.

An instance of the functor pattern in the study is the quotient construction for monoids, groups and rings. The locales , and form the source hierarchy $(x_i)$, and , and form the target hierarchy $(y_i')$; , which is also part of the source hierarchy, has no corresponding target and is not part of the functor (Fig. 2).

4.4.4 Loose Coupling

Let x be a locale containing a construction leading to some result—for example, a theorem $th$. Let y be a locale in which the result from x is to be used (in the general case, via some morphism $\phi$). If importing the entire context of $\phi x$ into y permanently is not desirable, loose coupling between x and y can be achieved through a temporary interpretation of $\phi x$ in y. After establishing the desired result $th$ in y, based on $\phi x$, closing the context for y discards $\phi x$ but $th$ remains.

Loose couplings are used in the study to transfer Cayley’s theorems back from to and from to . The monoid case is discussed in detail towards the end of Sect. 3.6

4.4.5 Mutual Sublocales

It occasionally happens that the same concept is arrived at through different paths. In the case of locales, the hierarchy can be consolidated through mutual sublocale declarations.

In the study this was made use of for the locale pairs and and and . Typically, defined operations of one locale are mapped to parameters of the other. Providing the correct mappings is essential for avoiding nontermination of the sublocale relation.

When I first realised this possibility [6, Section 5.3.2], I assumed it to be of theoretical interest only. Writers of mathematical libraries will conceivably be able to structure developments in a way that mutual sublocales are not required. Actually the feature has turned out to be relevant for being able to adequately reflect the structure of a mathematical text.

5 Discussion

What can be learnt from the study for the formalisation of algebra in Isabelle, and in simple type theory in general?

5.1 Complex Structures

Without any module support, syntax can quickly become unreadable and automation poor—for example, when groups themselves are denoted by large expressions.

Such situations were dealt with by dedicated locales, in which appropriate definitions were made. Examples are and where is the quotient set, the structure’s carrier set, and the binary operation (see Sect. 3.6). Given that the definition of the binary operation

involves selection and bounded abstraction, working without a definition would have been unwieldy. Not only is the syntax concise, also the configuration of reasoning tools (simplifier and classical reasoner) inherited from the locales for monoids and groups is not interfered with by conflicting setups of these tools for bounded abstraction.

The loss factors of the sections on quotient monoids and factor groups are not higher than those of the sections on abstract monoids and groups, respectively (Table 3). This supports that automation worked well, and that was also my experience while working on those proofs.

Exceptions to the approach were made where definitions outside the locale yielding concise notation within the locale were already available. A prominent example are monoids and groups of transformations, where binary operation and unit element were denoted by and , respectively. Definitions in the locales would merely have hidden the set parameter .

The functor pattern describes the general situation. The locales $y_i'$ on the right-hand side should have appropriate definitions that the parameters of the $x_i$ on the left-hand side can be mapped to. Additional definitions in $y_i'$ for concepts corresponding to defined operations of $x_i$ can be useful as well. These can be mapped via rewrites clauses.

The functor pattern also explains what is required for transferring the approach to other provers based on simple types such as the HOL4 system. Definitions in a locale correspond to global definitions (see Sect. 4.1.3) and are therefore not essential. Being able to lift knowledge from one context $x_i$ to another $y_i'$ is. The means for achieving this is, of course, theory interpretation, which is provided by locales through the sublocale and interpretation commands.

5.2 Conditional Definitions

Definitions in the study are conditional—that is, operations are only defined on the intended domain and not outside. This is in contrast to common practice in the HOL community, where often dummy values are chosen such that unnecessary proof obligations of the form “all values are in the carrier” can be avoided. For example, in a formalisation of homological algebra I was involved with completions were chosen to represent group homomorphisms [1]. These map values outside the domain to the unit element of the co-domain.

The motivation for choosing conditional definitions in the present study was, besides being faithful to Jacobson’s text, understanding whether they would pose problems with rewrites clauses, where conditional rewrite rules are not allowed. No such problems were encountered. Conditional definitions did cause additional work, but a small number of lemmas on undefinedness (three in set and four in group theory) helped resolve proof obligations largely through automation. Proof scripts did not grow significantly in size.

Conditional definitions do not necessarily lead to conditional theorems, as illustrated by the factorisation of a map or homomorphism $\alpha$ into induced and natural parts (Sect. 3.1):

This theorem holds for maps and homomorphisms, and Jacobson proves it at the most general level—for maps. Had completion semantics been adopted, would have had to be replaced by an operator returning, outside , the unit element of the co-domain. This would only have worked for homomorphisms, not maps, since in the context of the latter no distinguished element is available. Using dummy elements is appropriate for isolated applications but in libraries they pose the risk of precluding generalisation.

5.3 Limitations of Locales

Locales provide means for structuring formal developments, but they do not change the underlying logic, so they do not increase expressiveness. This is a fundamental limitation. On the other hand, locales work on top of any logic provided there is substitution [6, Section 3.1], so they could be provided for a wide range of provers.

Locales proved effective for reusing theorems, but there is room for improvement with regard to configuring notation. While it is often desirable to use the original notation for an operation from a dependency, sometimes it is not. For example, the notations for the binary operations of a homomorphism’s domain and co-domain need to differ. Locales have a simple heuristic to avoid conflicts: notation is retained as long as no parameter is renamed or instantiated. This heuristic repeatedly necessitated redeclaring monoid syntax for groups as the carrier set parameter is renamed from to . This could be improved, by separating signature morphisms from locale expressions. A renaming or instantiation could then be declared once, along with notation, and reused in multiple locale expressions. Since locale declarations are infrequent (compared to theorems) this was considered a minor annoyance that could be lived with.

Locales aim at being flexible, and they succeed in many ways: a locale can be revisited and extended—for example, by definitions and theorems—at any point in a formal development. Even the locale hierarchy can be changed without modifying the locale declarations. What is currently not possible is amending an existing locale interpretation with additional rewrites clauses. This functionality would enable, when a definition in a locale is made, mapping it to an existing concept in the interpretation target. The feature is currently only available through internal APIs, for use by the class package [13], and only for what corresponds to the interpretation command, not for sublocale. Making it available in Isar for interpretation would be straightforward. For sublocale the matter is more involved: the sublocale graph is labelled with morphisms, and I was never able to convince myself that amending these morphisms in the described manner would be robust enough. It is conceivable that such an amendment could break the locale hierarchy in unexpected ways. For symmetry, the feature is not provided for the interpretation command either.¹⁰

5.4 Abstract Algebra in Isabelle

Work on Isabelle’s library of abstract algebra HOL-Algebra [8] started before the design of locales was complete. Definitions in locales only became available later [14]. Algebraic structures were therefore represented by record types (as outlined in Sect. 4.1.2). Achieving concise notation is awkward. To illustrate, let $\mathop { Quot }\mathcal {G} \, \mathcal {C}$ again denote the quotient group of $\mathcal {G}$ relative to the congruence $\mathcal {C}$. The locale for the quotient group situtation would extend the group locale by an additional parameter $\mathcal {Q}$ and an additional assumption $\mathcal {Q} \equiv \mathop { Quot }\mathcal {G} \, \mathcal {C}$, such that $x \cdot _\mathcal {Q} y$ could be written instead of $x \cdot _{\mathop { Quot }\mathcal {G} \, \mathcal {C}} y$. The additional parameter and assumption would complicate using that locale. The case study shows that this can be improved in two ways:

• 1. Make the quotient group locale a clone of the group locale and define the quotient group $\mathcal {Q}$ within that.

• 2. As their means for composing structures is limited, avoid Isabelle/HOL’s records.

A full assessment whether improving HOL-Algebra in this way is feasible (and worth the effort) is beyond the scope of this discussion. I expect that the first change is fairly straightforward, but changes to the record package may be required for compatibility with definitions in locales. The second change will have a significant impact on work that depends on the library. This can possibly be mitigated by applying the functor pattern so that revised, record-free locales are mapped to existing, record-based ones, and dependent material could be converted gradually.

Since record types are not needed, locales can support abstract algebra in Isabelle’s set theory, Isabelle/ZF, equally well. Locales could, in principle, be provided for a wide range of logics and provers. Whether provers based on dependent types, which are a powerful means of representing algebraic structures themselves, could benefit from locales is less clear.

6 Conclusion

Gunter’s early work on algebra in simple type theory [12] is foundational and applied in variations in many formalisations. Locales are based on her approach too, and it is lifted to a module system with support for concise local notation, name space management, flexible means of creating and maintaining module hierarchies, and integration with the proof language. In my earlier, detailed account [6], locales are defined in terms of their operational semantics. There, their capabilities are explored by comparison to other structuring mechanisms including type classes, ML-style modules [15] and the module system of Coq [22]. The present case study complements this work by studying the particulars of formalising a mathematical text selected to be challenging from a structural, but not necessarily mathematical, perspective.

The formalised corpus sets out with equivalence classes and the factoring of maps and extends to the fundamental theorems of monoid, group and ring homomorphisms. Cosets are identified to be the orbits of translations, transformations on the underlying group, and their properties derived through this route. Quotient classes are shown to be the cosets of normal subgroups. The results derived on homomorphisms pick up from there, and their fundamental theorems build on the factoring of maps in a natural way.

An important result of the study is that locales alone are sufficient for representing algebraic structures in a concise and modular manner. Record types are not required. When choosing to group the parameters of an algebraic structure into a single record object it needs to be kept in mind that this approach tends to yield longer statements due to operations having additional record arguments that will be inferred only in simple situations. Also, Isabelle’s record types only allow linear structure hierarchies. By avoiding records in this case study, a natural declaration of the ring structure was straightforward.

Locales achieve concise statement notation by hiding parts of the internal representation of objects of discourse in the logic calculus, and by applying context-specific concrete syntax. Locales also achieve concise proofs by providing powerful means of reuse. The size ratio of formal to “pen-and-paper” development, de Bruijn’s loss factor, did not increase throughout the work and it was possible to lift the monoid and group results to rings in the formalisation as effectively as in the formalised text.

Locales declared in the case study are not confined to algebraic structures proper such as monoids, groups and rings. More complex and sometimes auxiliary situations—for example, that of a subgroup contained in the kernel of a homomorphism—are captured with locales as well. The module system makes transferring results from such intermediate constructs to contexts of use easy.

Several lessons can be learnt for formalisations in Isabelle. Reasoning patterns of locale use in the case study were identified and described. While these patterns occurred in the context of abstract algebra, they appear rather more intrinsic to how locales work than to the application domain, and so these patterns will also be useful in other domains. Dummy values, a means for avoiding undefinedness in definitions, need to be used with care, especially in libraries, since they can preclude desirable generalisation. In general, the case study provides a better specimen of using locales than Isabelle’s library of abstract algebra, HOL-Algebra [8], since it is based on more modern techniques. Guidance on how to proceed with the latter was given, but a full assessment is beyond the scope of this work.