10.6092/issn.1972-5787/4566
A recurring proof obligation in modern mathematics, ranging from textbook exercises to deep research problems, is to show that a given function is a morphism in some category: in analysis and topology, for example, we frequently need to prove that functions are continuous, while in group theory we are constantly concerned with homomorphisms. This paper describes a generic procedure that automatically discharges routine instances of this kind of proof obligation in an interactive theorem prover. The proof procedure has been implemented and found very useful in a mathematical case studies carried out using the ProofPower system
application/pdf
1972-5787
4566
1
en
Robin Denis Arthan
Journal of Formalized Reasoning
formalised mathematics
Now f is continuous (exercise!)
Text.Serial.Journal
https://jfr.unibo.it/
9
QED 20th anniversary
2016-01-29
2014-12-12
2016-01-29
2016-12-23
33 -52
JFR
Robin Denis Arthan
2016/01/29
10.6092/issn.1972-5787/4566
33
Lemma 1 Ltd. & Department of Computer Science, Oxford University
1972-5787
1
formalised mathematics
en
52
Now f is continuous (exercise!)
https://jfr.unibo.it/article/download/4566/5723
9
Now f is continuous (exercise!)
R.D. ARTHAN
Lemma 1 Ltd. & Department of Computer Science, University of Oxford
rda@lemma-one.com


A recurring proof obligation in modern mathematics, ranging from textbook exercises to deep
research problems, is to show that a given function is a morphism in some category: in analysis
and topology, for example, we frequently need to prove that functions are continuous, while in
group theory we are constantly concerned with homomorphisms. This paper describes a generic
procedure that automatically discharges routine instances of this kind of proof obligation in an
interactive theorem prover. The proof procedure has been implemented and found very useful in
a mathematical case studies carried out using the ProofPower system




1.   INTRODUCTION
Consider the function f (x) = e2πix . If we are interested in algebraic properties of
f , we will want to know that it is a homomorphism from the additive group of
real numbers to the multiplicative group of non-zero complex numbers, while if we
are interested in topological properties, we will want to know that it is continuous
with respect to the appropriate topologies. As the title reminds us, in traditional
mathematical practice, discharging such proof obligations is often routine and they
are left as exercises for the reader. When we are using a mechanized theorem-
prover to formalise mathematics, these exercises are often tedious to carry out
manually and we can very reasonably expect automatic support to help us find the
proofs. This paper discusses a simple but effective generic approach to this kind of
problem, viewed as the problem of showing that a given set-theoretic function is a
morphism in some category of interest, e.g., the category of groups or the category
of topological spaces.
   Some work on this kind of automation in specific instances has already been done,
particularly in the context of proving continuity and differentiability in formalisa-
tions of analysis [Har98, Got00, Fle00, CF02, BLM12] . The goal of this paper
is to present a more general approach. We begin with a discussion of formalisa-
tions of the concrete categories such as Grp, Top, Rng and R−Vec that occur
so frequently in mathematical practice. The goal is not to formalise any category
theory, but rather to use some basic category-theoretic concepts to help structure
our thinking about the formalisation. The categories in question generally have a
rather different flavour from the categories that commonly occur in computer sci-
ence. For example, apart from the category of sets, cartesian closed categories are
rather rare in mathematics. We then show, by example, how routine proofs that
a given function is a morphism in a concrete category can be broken down into
two phases: (i) represent the candidate function as a composite built from ground
functions by morphism-preserving combinators, then (ii) decompose the assertion

This work was supported in part by EPSRC grant number EP/K503769/1.

                                       Journal of Formalized Reasoning Vol. 9, No. 1, 2016 Pages 33–52.
34     ·     R.D. Arthan

about the composite into (known) assertions about the ground functions. We then
show how this approach admits a straightforward implementation using tools that
are available “off-the-shelf” in programmable interactive theorem-proving systems
such as the various implementations of HOL. We conclude with a discussion of the
application of this approach in some mathematical cases studies carried out using
the ProofPower system.

2.    REPRESENTING A CONCRETE CATEGORY IN HOL
Recall, for example, from [Mac98], that a concrete category is a category in which
(i) each object X can be identified with an underlying set U (X) and (ii) the mor-
phisms X → Y can be identified with some collection of the set-theoretic functions
f : U (X) → U (Y ). Concrete categories arise in the very common mathematical sce-
nario in which one deals with sets equipped with some extra structure and functions
between the sets that “respect” the structure in some suitable sense. Examples of
concrete categories abound in modern mathematics: the following table lists just a
few to give a flavour.
                Name         Objects                   Morphisms
                Set          All sets                  Arbitrary functions
                Grp          Groups                    Group homomorphisms
                R−Vec        Real vector spaces        Linear maps
                Top          Topological spaces        Continuous functions
   Note that a category whose objects are naturally defined as sets but whose mor-
phisms are not functions between the sets may actually be a concrete category
under a suitable definition of the underlying set. For example, Rel, the category
of sets and relations, is a concrete category if one takes U (X) to be the power set
P(X) and identifies a relation R with the function A 7→ {y | ∃x ∈ A• x R y}. An
example of a category that is not equivalent to any concrete category is Toph, the
homotopy category, which has the same objects as Top, but where the morphisms
A → B comprise the homotopy equivalence classes of continuous functions from A
to B. The proof that Toph is not concrete is due to Freyd [Fre70, Fre04].
   The general problem we are concerned with is proving that some given set-
theoretic function is a morphism in some concrete category of interest. Our goal
is to set up a framework for solving this kind of problem automatically in a useful
range of practical situations. We will work in the ProofPower implementation of
Mike Gordon’s HOL. See [Gor00] for a survey of HOL and its various implementa-
tions and [AJ 1] for more information about the ProofPower implementation. We
begin with an extended example showing how the category Top has been formalised
in the ProofPower mathematical case studies [Art14] and discussing how one might
automate proofs of morphismhood in that formalisation.
2.1   Representing Top
It will be helpful to have in mind an example formalisation of a particular concrete
category: we will sketch the development of the category Top in the ProofPower
mathematical case studies. An object of Top is a topological space, which we


Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
                                                   Now f is continuous (exercise!)        ·     35

represent simply by giving the set of open sets1 : we say τ is a topology and write
τ ∈ Topology to mean that τ is a collection of sets of elements of some type
0
  a that is closed under arbitrary unions and binary (and hence arbitrary finite)
intersections. Thus Topology is the class of families of sets of elements of type 0 a
defined as follows in ProofPower-HOL, using the (postfix) powerset type constructor
P to formalise “class”, “family” and “set”:
            Topology : 0 a P P P


                Topology =
                {τ
                                  S
                |   (∀V • V ⊆ τ ⇒   V ∈ τ)
                ∧ (∀A B •A ∈ τ ∧ B ∈ τ ⇒ A ∩ B ∈ τ )}
   Here we use a notation for introducing new HOL constants that ProofPower has
borrowed from the Z specification language [Spi92]. In this notation, one gives type
constraints for the constant or constants being defined (in this case Topology) and
then, under the horizontal line, one gives a predicate giving the desired defining
property of the constant or constants (in this case an equation giving the value
of the constant). This maps onto a call of a primitive definitional principle that
requires an existence proof for the constants being introduced. The ProofPower-
HOL infrastructure includes a range of procedures for discharging the existence
proofs and these will automatically discharge the proof obligations in many cases
(including all the ones in this paper).
   It is pleasant to call the underlying set of a topology its space, which we can
define as a union, thus:
            Space T : 0 a P P → 0 a P

                                 S
            ∀τ • Space T τ =         τ
   If τ is a topology, we call its elements τ -open sets, so A ∈ τ formalises the
statement that A is τ -open. The cases studies proceed with other standard defi-
nitions, e.g., a set A is defined to be τ -closed if its complement Space T τ \ A is
τ -open. In particular, and central to the concerns of the present paper, the notion
of continuous function is formalised as follows:
1 Setsare represented in ProofPower as members of a polymorphic type 0 a SET defined to be in
one-to-one correspondence with the type of propositional functions on the type 0 a. The syntax
for set comprehension is implemented by the parser and pretty-printer which represent {x |t}
as SetComp(λx • t) where SetComp is the representation function for the type 0 a SET . In the
present paper, we are working in the context of a library theory which offers P as an abbreviation
for SET .




                                               Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
36     ·     R.D. Arthan

            $Continuous : (0 a P P × 0 b P P) → (0 a → 0 b) P


            ∀σ τ •     (σ, τ ) Continuous =
               {f
               |       (∀x • x ∈ Space T σ ⇒ f x ∈ Space T τ )
               ∧       (∀A• A ∈ τ ⇒ {x | x ∈ Space T σ ∧ f x ∈ A} ∈ σ)}
   Here Continuous is a postfix operator, whose operand comprises a pair of topolo-
gies, (σ, τ ) and whose value is a set of functions. (The “$” above is required to sup-
press the postfix status, allowing the name to be used in a declaration.) We say “f
is (σ, τ )-continuous” and write f ∈ (σ, τ ) Continuous if f maps the underlying
set of σ to that of τ and if for every τ -open set A, the inverse image of A under the
restriction of f to the space of σ is σ-open. Here we are working around the fact
that HOL functions are total on their types by using a total function to represent
its restriction to the space of σ. This is extremely convenient, since we can re-use
existing infrastructure for working with total functions. The price is that one has
to be careful when stating results involving equality between functions. For present
purposes, the advantages considerably outweigh the disadvantages.
   In summary, we have formalised the specific category Top by defining: (i) a class
Topology to represent ObjTop , (ii) a function Space T to represent the underlying
set operation UTop ( ), and (iii) a subset (σ, τ ) Continuous of the functions from
U (σ) to U (τ ) to represent MorTop (σ, τ ).

2.2   Proving morphismhood in (R; exp, sin, cos)Top
In the title of this section and some later sections, we adopt the following notational
convention: if C is a category, if o1 , o2 , . . . is a list of objects of C or operators on the
objects of C and if m1 , m2 , . . . is a list of morphisms of C or operators on the mor-
phisms of C, we write (o1 , o2 , . . . ; m1 , m2 , . . .)C for the subcategory of C generated
by the oi and mj . So (R; exp, sin, cos)Top is the subcategory of Top comprising
the single object R and all functions obtainable by composing the exponential, sine
and cosine functions.
  R, the space of real numbers with the usual topology, is formalised by specifying
the set OR of open sets:
            OR : R P P


            O R = {A | ∀t•t ∈ A
               ⇒ ∃x y•t ∈ OpenInterval x y ∧ OpenInterval x y ⊆ A}
   The exponential, sine and cosine functions may be characterized in several dif-
ferent ways: in the ProofPower formalisation, they are characterized by the usual
differential equations and the definitions are proved consistent using the power
series representations.
   It would be considered an easy textbook exercise in basic analysis to prove that
the function f (x) = sin(cos(exp(x))) is continuous: one simply observes that sin,
cos and exp are continuous and that the composition of two continuous functions
Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
                                                       Now f is continuous (exercise!)           ·     37

is continuous. Let us see how we might automate this kind of proof. Since, for the
moment, we are only interested in a single topological space O R , let us write Cts
for (O R , O R )Continuous. We will use the ProofPower syntax Sin x , Cos x , f o g
etc., for the formalised mathematics and the textbook syntax sin(x), cos(x), f ◦ g
etc. in the semi-formal narrative. We assume we have already proved the necessary
ground facts:
           ` Exp ∈ Cts
           ` Sin ∈ Cts
           ` Cos ∈ Cts
  We are given the goal2
           ?` (λx •Sin(Cos(Exp x ))) ∈ Cts
One’s first thought might be to express the compositionality property as follows:
           ` ∀f g• f ∈ Cts ∧ g ∈ Cts ⇒ (λx •f (g x )) ∈ Cts
and then to attack the goal by backchaining3 . I.e., one would first match the goal
with
        (λx •f (g x )) ∈ Cts
and use the compositionality property to reduce the problem to the subgoals
           ?` Sin ∈ Cts
           ?` (λx • Cos(Exp x )) ∈ Cts
then the former subgoal can be discharged as it is one of the ground facts and
the latter can again be matched with (λx • f (g x )) ∈ Cts. Unfortunately, this in-
volves general higher-order matching: the term (λx • f (g x )) ∈ Cts is not a linear
pattern4 in the sense of Miller [Mil91] and so the efficient Miller-Nipkow algorithm
[Nip93] does not apply. Although the general higher-order matching problem is
known to be decidable [Sti09], it is also known to be of non-elementary complexity.
We could write a custom function to deal with the particular cases of higher-order
matching needed here, but we prefer an approach that makes best use of existing
proof infrastructure (which includes first-order matching and higher-order matching
for linear patterns). With this in mind, we express the compositionality property
using the functional composition operator ◦:

2 We write ` φ for a theorem that has been proved and ?` φ for a conjecture or goal. More

generally, theorems and goals in HOL are sequents Γ ` φ and Γ ?` φ where the assumptions Γ
comprise a set of formulas, but we do not need sequents with assumptions here.
3 We use the term backchaining to describe a class of proof techniques that use a stock of universally

closed implications ∀x1 , . . . , xm • φ1 ∧ . . . ∧ φn ⇒ ψ, where possibly n = 0 so that the “implication”
is actually a ground fact. In a backchaining proof, given a goal ?` χ, we attempt to match χ with
the succedent ψ of each implication and when a substitution θ giving a match is found, we replace
the goal with the subgoals obtained by existentially closing (φ1 ∧ . . . ∧ φn )θ with respect to any
free variables that do not appear free in ψ and then carrying out logical simplifications such as
pushing the existential quantifiers in through conjunctions and breaking conjunctions into multiple
subgoals. We may also use application-specific heuristics. e.g., to choose existential witnesses.
4 A linear pattern is a λ-term in β-normal form in which in every subterm of the form f x . . . x
                                                                                                  1      n
where f is a variable, the xi are all η-equivalent to variables.


                                                   Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
38     ·     R.D. Arthan

           ` ∀f g• f ∈ Cts ∧ g ∈ Cts ⇒ g o f ∈ Cts
and translate our original goal:
           ?` (λx •Sin(Cos(Exp x )))∈ Cts
into
           ?` Sin o Cos o Exp ∈ Cts
The problem can then be solved just by backchaining using first-order matching:
higher-order matching for linear patterns will be important in the sequel, but we
do not need it yet.

2.3    Products
We say a concrete category C has standard products if the standard set-theoretic
product construction yields a product in C. That is to say, if X and Y are objects
of C, there is an object X ×C Y of C, such that (i) U (X ×C Y ) = U (X) × U (Y ), (ii)
the projections π1 : U (X × Y ) → U (X) and π2 : U (X × Y ) → U (Y ) are morphisms
of C and (iii), if f : Z → X and g : Z → Y are morphisms of C, there is a unique
morphism hf, gi : Z → X ×C Y such that f = π1 ◦ hf, gi and g = π2 ◦ hf, gi. (If one
drops requirement (i), this is the usual definition of a product.)
   Many useful examples of concrete categories have standard products, e.g., Top,
and any concrete category like the category of partially ordered groups that can be
axiomatized by first-order Horn clauses [Hod93, Chapter 9]. For a simple example
of a concrete category that has products but not standard products, choose some
set U with at least two elements and consider the category SU whose objects are
subsets of U and whose morphisms are the inclusions. If X, Y and Z are objects
of SU , there are morphisms from Z to X and from Z to Y iff Z ⊆ X ∩ Y , hence X
and Y have X ∩ Y as their product.
   In our running example, the product structure on Top is given on objects by the
product topology formalised in ProofPower as follows:
            $×T : 0 a P P → 0 b P P → (0 a × 0 b) P P


            ∀σ τ • (σ ×T τ ) =
               {C | ∀ x y• (x , y) ∈ C
                   ⇒ ∃A B • A ∈ σ ∧ B ∈ τ ∧ x ∈ A
                       ∧ y ∈ B ∧ (A × B ) ⊆ C }
The pairing operator hf, gi (which is the same in any concrete category with stan-
dard products) is provided already in the ProofPower-HOL library as if by the
following:
            Pair (0 a → 0 b) × (0 a → 0 c) → 0 a → 0 b × 0 c


            ∀ f g• Pair (f , g) = (λ x • (f x , g x ))
  Similarly, a concrete category C has standard sums if the standard set-theoretic
sum (i.e., disjoint union) yields a sum in C. Top has standard sums, but categories
Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
                                             Now f is continuous (exercise!)        ·     39

of algebras typically do not: for example, in the category of abelian groups, finite
sums are isomorphic to products: X +Y ' X ×Y . We will concentrate on products
in the present paper.
2.4   Proving morphismhood in (R, ×; hi, exp, sin, cos, +, ×)Top
Once we allow product topologies, we can construct an infinite number of distinct
topological spaces from the ground space R. We will therefore need to add the
following general compositionality property to our stock of facts.
          ` ∀ ρ σ τ f g • ρ ∈ Topology ∧ σ ∈ Topology ∧ τ ∈ Topology ∧
                  f ∈ (ρ, σ) Continuous ∧ g ∈ (σ, τ ) Continuous
              ⇒ g o f ∈ (ρ, τ ) Continuous
Note that when we match a subgoal such as
          ?` Sin o Cos ∈ (O R , O R ) Continuous
with the right-hand side of the implication in the above and then backchain, the
subgoal we get is existentially quantified in the intermediate topology σ:
          ?` ∃ σ• σ ∈ Topology ∧ Cos ∈ (O R , σ) Continuous
              ∧ Sin ∈ (σ, O R ) Continuous
  For the examples in this section, all topological spaces are obtained from the
standard topology on R using the product topology construction, hence we can
always select an appropriate existential witness in the above by inspecting the type
of σ, which in this example is; ((R)P)P, the type of a topology on R, so we will
instantiate σ to the standard topology OR .
  Specific to products, we have the facts that the projection function, π1 and π2
(written Fst and Snd in ProofPower-HOL) are continuous and that the pairing of
two continuous functions is continuous.
         ` ∀ σ τ • σ ∈ Topology ∧ τ ∈ Topology
              ⇒ Fst ∈ (σ ×T τ , σ) Continuous
         ` ∀ σ τ • σ ∈ Topology ∧ τ ∈ Topology
              ⇒ Snd ∈ (σ ×T τ , τ ) Continuous
         ` ∀ ρ σ τ f g• ρ ∈ Topology ∧ σ ∈ Topology ∧ τ ∈ Topology ∧
                   f ∈ (ρ, σ) Continuous ∧ g ∈ (ρ, τ ) Continuous
              ⇒ Pair (f , g) ∈ (ρ, σ ×T τ ) Continuous
  To use the above, we will need to prove that various instances of the product
topology are actually topologies, for which purpose we have the following fact:
          ` ∀ σ τ • σ ∈ Topology ∧ τ ∈ Topology ⇒ σ ×T τ ∈ Topology:
Let us see how we might prove a goal such as the following using our augmented
stock of facts,
          ?` (λx •(Sin(Exp x ), Cos (Exp x ))) ∈ (O R , O R ×T O R ) Continuous
  To apply our facts, we first translate the λ-abstraction in our goal using the
composition and pairing combinators to give:
          ?` Pair (Sin o Exp , Cos o Exp) ∈ (O R , O R ×T O R ) Continuous

                                         Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
40     ·     R.D. Arthan

Back-chaining with our facts now solves the problem. Of course to automate the
process we have just described, we need to automate the translation of the λ-
abstraction into the combinator form. We will describe a general scheme for this
in the next section.
   Our general translation scheme will also allow us to prove continuity of expres-
sions involving binary operators such as addition. For this, we need to address
the minor detail that ProofPower-HOL follows many type-theoretic formalisation of
mathematics in defining these as curried functions: they have type R → R → R.
So, for example, we translate the λ-abstraction:
           ?` (λ(x , y)• Exp(x + y)) ∈ (O R ×T O R , O R ) Continuous
into the combinator form:
          ?` Exp o Uncurry $+ o Pair (Fst, Snd )
              ∈ (O R ×T O R , O R ) Continuous
where the function Uncurry converts a two-place function into the corresponding
function on pairs. Given the additional fact:
           ` Uncurry $+ ∈ (O R ×T O R , O R ) Continuous
backchaining with our facts will yet again solve the goal.
  With just a little more work, we can deal with arbitrary exponential/trigonometric
polynomials. We have just to extend our approach to cover constant functions,
negation, multiplication and exponentiation with natural number exponents. For
these consider the following example:
           ?` (λx • 2 . ∗ ∼ (x b 4 )) ∈ (O R , O R ) Continuous


Here, ∼ : R → R is negation and b : R → N → R is the exponentiation
operator, which we think of as a family of continuous functions parametrized by a
natural number. We translate the goal into:
           ?` Uncurry $∗ o Pair (CombK 2 ., ∼ o (λ x • x b 4 ))
               ∈ (O R , O R ) Continuous
where CombK is the ProofPower-HOL name for the K combinator. This may be
solved by backchaining using the new facts:
           ∀ σ τ c• σ ∈ Topology ∧ τ ∈ Topology ∧ c ∈ Space T τ
               ⇒ CombK c ∈ (σ, τ ) Continuous
           ` Uncurry $∗ ∈ (O R ×T O R , O R ) Continuous
           ` ∼ ∈ (O R , O R ) Continuous
           ` ∀n• (λ x • x b n) ∈ (O R , O R ) Continuous
           ` ∀x • x ∈ Space T O R
   As a final example for this section, let us consider the famous complex function
f (z) = e2πiz . In the ProofPower-HOL formalisation, the goal stating that this
function is continuous is as follows:
          (λz • Exp(RC 2 . ∗ RC π ∗ I C ∗ z )) ∈ (O C , O C ) Continuous
where:

Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
                                            Now f is continuous (exercise!)         ·     41

—Exp is an (overloaded) alias for the complex exponential function defined (using
 its real name Exp C ) as follows:
           Exp C : C → C


           ∀z • Exp C z = RC (Exp(Re z )) ∗ (Cos (Im z ), Sin (Im z ))
—C is an abbreviation for the type R × R,
—RC is the inclusion of R as a subfield of C defined by ∀x • RC x = (x , 0 .),
—I C = (0 ., 1 .) is the complex number i,
—Re and Im are aliases for the C → R instances of Fst and Snd respectively,
—∗ is an (overloaded) alias for multiplication of complex numbers, and
—the exponential and trigonometric functions on the right-hand side of the equation
 have type R → R.
The goal translates into combinator form as follows:
          ?` Pair (
              Uncurry $∗ o Pair (
                  Exp o Uncurry $∗ o Pair (
                      CombK 2 .,
                      Uncurry $∗ o Pair (CombK π, ∼ o Im)),
                  Cos o Uncurry $∗ o Pair (
                      CombK 2 .,
                      Uncurry $∗ o Pair (CombK π, Re))),
              Uncurry $∗ o Pair (
                  Exp o Uncurry $∗ o Pair (
                      CombK 2 .,
                      Uncurry $∗ o Pair (CombK π, ∼ o Im)),
                  Sin o Uncurry $∗ o Pair (
                      CombK 2 .,
                      Uncurry $∗ o Pair (CombK π, Re))))
                                      ∈ (O C , O C ) Continuous
Note that the complexity of this formula arises because we are here treating C as
the R-algebra R[i], in order to view its topology as the topology of the plane R × R.
After expansion of the definition of the topology on the complex plane, namely
OC = OR × OR , backchaining with our existing stock of facts yet again solves this
goal.
2.5   Representing other categories
A concrete category such as Grp defined by first-order axioms over a finite signature
is naturally formalised in HOL as a subclass of a polymorphic labelled product type
with a component defining the underlying set of an object and a component for each
function or predicate symbol in the signature. For example, in ProofPower-HOL,
groups are formalised as a subclass of a labelled product with four components
defined using the following syntax:

                                         Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
42       ·       R.D. Arthan

             HOL Labelled Product

                 GROU P
                                        0
                  Car G             :     a P;
                                        0
                  Times G           :     a → 0 a → 0 a;
                                        0
                  Unit G            :     a;
                                        0
                  Inverse G         :     a → 0a


   The above syntax introduces a polymorphic labelled product type (0 a)GROUP
with components of the indicated names and types. The component Car G denotes
the underlying set of the group (a.k.a., its carrier set) and the remaining compo-
nents represent the multiplication, the identity element and the inverse function.
Groups are then defined by a polymorphic subclass Group of the type (0 a)GROUP
comprising the labelled 4-tuples that satisfy the group axioms. As with continu-
ous functions on topological spaces, group homomomorphisms are represented by
functions (0 a)GROUP → (0 b)GROUP whose restrictions to the carrier set of the
domain respect the group structure but whose behaviour outside the carrier set is
irrelevant. We define Homomorphis(G, H ) to be the set of homorphisms from G
to H.
2.6     Proving morphismhood in (R+ , C+ , C× ; exp, c × )Grp
The assertion that the function f (x) = e2πix defines a homomorphism from the
additive group of real numbers to the multiplicative group of positive complex
numbers is formalised as the following goal:
             ?` (λx • Exp(RC 2 . ∗ RC π ∗ I C ∗ RC x ))
                      ∈ Homomorphism (R+ , C∗ )
     If we translate the goal into:
             ?` Exp o $∗ (RC 2 .) o $∗ (RC π) o $∗ I C o RC
                     ∈ Homomorphism (R+ , C∗ )
      the goal will follow by backchaining using the following facts:
             ` Exp ∈ Homomorphism (C+ , C∗ );
             ` RC ∈ Homomorphism (R+ , C+ );
             ` ∀ c : C• $∗ c ∈ Homomorphism (C+ , C+ ):
             ` ∀ G H K f g•
                      G ∈ Group ∧ H ∈ Group ∧ K ∈ Group
                 ∧ f ∈ Homomorphism (G, H ) ∧ g ∈ Homomorphism (H , K )
                 ⇒ g o f ∈ Homomorphism (G, K )
             ` R+ ∈ Group
             ` C+ ∈ Group
             ` C∗ ∈ Group

3.     THE PROOF PROCEDURE
The examples of the previous section suggest a proof procedure for proving mor-
phismhood in a particular concrete category. The goals tackled by the proof pro-
Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
                                                 Now f is continuous (exercise!)         ·     43

cedure have the form
                                    ? ` f ∈ MorC (X, Y )
where:
—C is the concrete category of interest which is assumed to have standard prod-
 ucts5 ,
—f is a λ-abstraction representing a function that we wish to show is a morphism
 of C,
—X and Y are expressions formed from some given objects of C using the product
 in C.
  The proof procedure translates f into a combinator form and then attempts to
solve the resulting goal by backchaining with theorems asserting that the combi-
nators map morphisms to morphisms and that the given morphisms and objects
are indeed morphisms and objects of C. These theorems may impose additional
conditions, e.g., that some expression belongs to the underlying set of an object.
  We describe these two phases of the proof procedure in detail in sections 3.1
and 3.2 below.
3.1     Translation to combinator form
We will work in typed λ-calculus with paired abstractions and projection operators.
In this language we may write the addition operation on the real numbers either
using a paired abstraction: λ (x : R, y : R) • x + y or using the projections: λ p :
R × R • π1 (p) + π2 (p). This language is supported as derived syntax in all the
HOL implementation using Milner-Hindley type inference to allow the user to omit
inessential type constraints. For present purposes it is convenient to take this
language as primitive. In the abstract syntax of the language all type constraints
are explicit and and all type operators are written postfix ((α, β)→ rather than
α → β). The abstract syntax is thus given by the following grammar:
               Type = TyVar | (Type, ..., Type)TyOp
               Pat = Var : Type | (Pat, Pat)
               Term = Var : Type | Con : Type | Term Term | λPat• Term
Here TyVar and Var denote two infinite set of variables names. The set vars(p) ⊆
Var × Type of typed variables that occur in a pattern p is defined in the obvious
way. Patterns and terms are subject to the usual rules that assign a unique type
to each well-typed pattern or term. See [FL96] for details. In particular, a pattern
(p1 , p2 ) is only well-typed if vars(p1 ) ∩ vars(p2 ) = ∅, in which case its type is τ1 × τ2
where τi is the type of pi , i = 1, 2.
   We assume given a signature Σ defining the types and constants that we may use:
it gives the arity of each type operator and the polymorphic type of each constant.
Σ will include at least the (infix) binary type operators → and × and the following

5 Theprocedure is easily adapted to work for categories that do not have standard products just
by not providing the theorems and other parameters that relate to products.



                                              Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
44     ·        R.D. Arthan

constants (where α, β and γ are type variables):
                                I    :   α→α
                             ◦       :   (β → γ) → (α → β) → α → γ
                              πi     :   α×β →α
                              π2     :   α×β →β
                           h , i     :   (α → β) → (α → γ) → α → β × γ
                           ( , )     :   α→β →α×β
                               K     :   α→β→α
                         Uncurry     :   (α → β → γ) → α × β → γ
The translation into combinator form is parametrized by three sets of terms called
unary, binary and parametrized that denote morphisms of C represented in three dif-
ferent ways: unary represents morphisms represented directly as functions, e.g., exp
as a morphism R → R in Top; binary represents morphisms on product objects rep-
resented as curried functions e.g., multiplication represented with type R → R → R
rather than R × R → R; parametrized represents a family of objects parametrized
by a parameter passed as the second argument to a curried function, e.g., expo-
nentiation of real numbers by natural number coefficients represented with type
R → N → R. Note that a family of objects parametrized by a parameter passed as
the first argument to a curried function, e.g., c × : R → R can be represented by
including all their instances in the set unary.
   The translation is defined by repeated application of a set of rewrite rules defined
as follows, where p is a pattern, where x and y are typed variables (Var : Type),
c is a typed constant (Con : Type), where other metavariables are arbitrary terms
of the appropriate types meeting any side-conditions stated and where πxp is I, if
p = x, and is the composite of instances of π1 and π2 that extracts x from p, if
                         ((x ,y ),(x ,y ))
p 6= x ∈ vars(p), e.g., πy1 1 1 2 2 = π2 ◦ π1 .
                (λp• x)       ;   πxp                                  x ∈ vars(p)
                (λp• y)       ;   Ky                                   y 6∈ vars(p)
                 (λp• c)      ;   Kc
           (λp• (t1 , t2 ))   ;   h(λp• t1 ), (λp• t2 )i
               (λp• f t)      ;   f ◦ (λp• t)                          f ∈ unary
            (λp• g t1 t2 )    ;   Uncurry g ◦ h(λp• t1 ), (λp• t2 )i   g ∈ binary
              (λp• h t j)     ;   (λx • h x j) ◦ (λp• t)               h ∈ parametrized
   We will assume that the three sets of terms unary, binary and parametrized are
pairwise disjoint, that no instance of ( , ) or of ( , )(x) belongs to any of the three
sets and that no term in unary has the form s t where s ∈ binary ∪ parametrized.
These assumptions ensure that the rewrite rules are mutually exclusive. We will
also assume that no term in any of the three sets contains a subterm that is a λ-
abstraction or an instance of K, since that makes it easier to describe the properties
of the rewrite system and is not a significant shortcoming in practice.
   Let E be the smallest set of terms that contains all variables and constants
that are not subterms of any of the terms in the sets unary, binary or parametrized
and is such that whenever t1 , t2 ∈ E, then so also are (t1 , t2 ) and any of the
applications f t1 , g t1 t2 and h t1 j that are well-typed, where f ∈ unary, g ∈ binary,
h ∈ parametrized and j is any constant. If t is in E and p is any pattern, then it
Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
                                                    Now f is continuous (exercise!)         ·     45

is clear that λp• t can be rewritten using the above rules to a term t0 that can be
built from ground terms of the forms I, π1 , π2 , K y, K c, f , Uncurry g and λx• h x j
using composition ◦ and pairing ( , )6 .
   We now have to consider how to implement the rewrite system in practice. What
we will typically want to represent in the sets unary and binary includes (i) specific
morphisms, e.g., the monomorphic constant Exp : C → C as a group homomor-
phism from C+ to C∗ , (ii) families of morphisms defined by type instantiation, e.g.,
the set of all type instances of the polymorphic constant Fst : 0 a × 0 b → 0 a as
morphisms in any concrete category with standard products, (iii) families of mor-
phisms defined by term instantiation, e.g., all instances of $ ∗ z : C → C as
group homomorphisms from C+ to C+ . We may also have variables in the sets that
we do not want to instantiate, e.g., coming from background assumptions. What
we will want to include in parametrized will be families of morphisms parametrized
by their second argument, such as b : R → N → R. A suitable representation
of each of these sets is therefore as a list of terms, which we will call the unary,
binary and parametrized operators together with a list of term variables that are
subject to instantiation. (The term variables not in the list of instantiable variables
will effectively be treated as constants by the proof procedure).
   The rules of the rewrite system are all instances of higher-order equations that
we can prove in advance. We call such preproved theorems that capture the validity
of a step in a proof procedure template theorems. Typically, template theorems are
instantiated as necessary and used as rewrite rules. For example, the rule for binary
is justified by the following template theorem.
           ` ∀f s t• (λx •f (s x ) (t x )) = Uncurry f o Pair (s, t)
Now the left-hand side of this template theorem is not a linear pattern, since f has
the application s x for its first argument. Fortunately, when we instantiate f to a
constant (or to a constant applied to one or more linear patterns), the left-hand
side becomes a linear pattern. For example, when we instantiate f to +, we get:
           ` ∀s t• (λx •(s x ) + (t x )) = Uncurry $+ o Pair (s, t)
  Thus the instantiation of the template theorem is a two-stage process: it is
instantiated once for each binary operator resulting in a form that is suitable for
our higher-order matcher, which we then use repeatedly to find the instantiations
needed to process any given input goal. Similarly, the template theorem justifying
the rule for unary is:
           ` ∀f t• (λx •f (t x )) = f o t
The instantiation of this to represent the family of homomorphisms from C+ to C+
given by left-multiplication is as follows:
           ` ∀t• (λx • $∗ z (t x )) = $∗ z o t
The rewrite rules for unary, binary and parametrized can therefore be implemented
by instantiating the template theorem to the various operators and then arranging

6 Inparticular, the ground terms λx• h x j are the only λ-abstractions in t0 . A case could be made
for replacing λx• h x j in the rewrite rules by switch h p where switch f x y = f y x, so there would
be no λ-abstractions at all. The description here matches what has actually been implemented.
                                                 Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
46       ·    R.D. Arthan

for instantiation to be enabled during rewriting for the instantiable variables only
(in ProofPower this may be achieved just by forming the universal closure with
respect to the instantiable variables).
   Thus we can arrange for all the instances of the rewrite rules that we need to
be expressed as linear patterns. In order to use the Miller-Nipkow higher-order
matching algorithm [Nip93], we also need to transform the abstraction over a
pattern p into abstraction over a plain variable7 . This is straightforward, e.g.,
(λ(x , y) • x + y) can be preprocessed into λxy • Fst xy + Snd xy. using a con-
version provided as part of the ProofPower proof infrastructure.
3.2      Proving the combinator form is a morphism
We now consider the problem of proving that the combinator form produced by
the first phase of our proof procedure is actually a morphism in the category C.
We can assume that the goal now has the form ?`(λx• t) ∈ MorC (X, Y ), where t is
formed from given morphisms using composition ◦ and pairing h , i and where
X and Y are formed from given objects of C using binary products. We assume we
have proved theorems asserting that that given morphisms are indeed morphisms,
that that the given objects are indeed objects together with the following theorems
allowing us to construct new objects and morphisms from old:
      ` ∀X Y •X ∈ ObjC ∧ Y ∈ ObjC ⇒ X ×C Y ∈ ObjC

      ` ∀X Y Z f g•
          X ∈ ObjC ∧ Y ∈ ObjC ∧ Z ∈ ObjC ∧ f ∈ MorC (X, Y ) ∧ g ∈ MorC (X, Z)
       ⇒ hf, gi ∈ MorC (X, Y ×C Z)

      ` ∀X Y Z f g•
          X ∈ ObjC ∧ Y ∈ ObjC ∧ Z ∈ ObjC ∧ f ∈ MorC (X, Y ) ∧ g ∈ MorC (Y, Z)
       ⇒ g ◦ f ∈ MorC (X, Z)
Backchaining with first-order matching, e.g., as implemented in the ProofPower
tactic bc tac is exactly what we need to use these theorems. However, backchaining
with the theorem about ◦ will produce a subgoal of the form:
      ?` ∃Y •X ∈ ObjC ∧ Y ∈ ObjC ∧ Z ∈ ObjC ∧ f ∈ MorC (X, Y ) ∧ g ∈ MorC (Y, Z)
We need some way of choosing the right intermediate object Y . A simple but
effective heuristic for this is to use the type of the term Y to decide what object to
use. Typically, we will only have a finite number of relevant objects of C of a given
HOL type, so we can use the type to select a list of possibilities.
   If we want to package the proof procedure as a decision procedure, then we can
do a search with backtracking for the right choice of objects. However, we may
also want to package the proof procedure as a heuristic for interactive use that
may make useful progress on a goal without solving it completely. For example,
if A and B are topological spaces, the function K x does not define a continuous

7 This  would be unnecessary given an implementation of the matching algorithm of Fettig and
Löchner which handles paired abstractions and projections [FL96]. However, the special case that
is of interest here does not require the full generality.

Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
                                             Now f is continuous (exercise!)        ·     47

function from A to B unless x ∈ B, and this might require a proof that is outside
the scope of our morphismhood proof procedure. A backtracking approach would
be inappropriate when the proof procedure is used in this way.
  In practice, at least when working with abstract topological spaces, the proof
procedure has proved very useful just using the naive heuristic of picking the first
known topology that has the right type. As an example where this heuristic fails,
consider the following problem about group homomorphisms:
         ?` (λx • Exp(x ) ) ∈ Homomorphism(C+ , C∗ )
  Here the postfix operator written z denotes conjugation of complex numbers
(which is a homomorphism on both C+ and C∗ ). It turns out that our implemen-
tation of the naive heuristic will lead to the false subgoals:
         ?` $ ∈ Homomorphism (C+ , C∗ )
         ?` Exp ∈ Homomorphism (C+ , C+ )
  The one-object-per-type approach has picked the wrong intermediate group. A
backtracking implementation of the proof procedure as a decision procedure will
try again and find the correct intermediate subgoals:
         ?` $ ∈ Homomorphism (C∗ , C∗ )
         ?` Exp ∈ Homomorphism (C+ , C∗ )
and so solve the goal. Since proofs in which there are many different group struc-
tures on the same underlying set are rare, a naive backtracking approach should be
relatively efficient in most cases.

4.   IMPLEMENTATION AND APPLICATIONS
A prototype of the generic proof procedure described in section 3 has been im-
plemented and applied in the ProofPower-HOL mathematical case studies [Art14].
A reader who downloads the case study source will find the implementation of the
generic procedure (basic morphism tac) in the file wrk083.doc and instantiations
(basic continuity tac, R continuity tac) in the file wrk067.doc.
   A design goal was to make good use of the existing matching, rewriting and
backchaining tools and we believe this was achieved: the implementation of the ba-
sic proof procedure is less than 100 lines of Standard ML code. This is augmented
by about 30 lines of interface code which automates the process of deriving the sets
unary, binary and parametrized by analysing a set of theorems asserting the neces-
sary categorical properties of some collection of objects, morphisms and operators
thereon.
   The generic proof procedure is implemented as a tactic that can make partial
progress and then hand the problem back to the user. However, the interface code
is relatively simplistic and, in particular, does not currently handle arbitrary side-
conditions in these theorems. This means that, in practice, when the procedure
fails it tends to be because a necessary assumption is missing and the solution is to
provide that assumption and then try again.
   The proof procedure has been found to be a very convenient tool in the formal-
isation of some of the basics of abstract topology, metric spaces, homotopy theory


                                         Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
48     ·     R.D. Arthan

and group theory and in putting this theory to work on some of the standard ex-
amples of functions on the complex plane with interesting topological and algebraic
properties.
   Here, for example, are the definitions of the notion of homotopy and a homotopy
class used in the case studies. As a technical convenience, a homotopy between
functions f, g : S → T relative to a subspace X of S is taken to be a continuous
function from S × R → T that agrees with f (resp. g) when restricted to S × {0}
(resp. T × {1}). (This is equivalent to the standard definition of a homotopy as a
continuous function on S × [0, 1], because such a function can always be extended
to S × R.)
            $Homotopy : 0 a P P × 0 a P × 0 b P P → (0 a × R → 0 b) P


            ∀σ X τ • (σ, X , τ ) Homotopy =
               {f
               |   f ∈ ((σ ×T O R ), τ ) Continuous
               ∧ ∀x s t•x ∈ X ⇒ f (x , s) = f (x , t)}

            $HomotopyClass : 0 a P P × 0 a P × 0 b P P → (0 a → 0 b) → (0 a → 0 b) P


            ∀σ X τ f • ((σ, X , τ ) HomotopyClass) f =
               {g
               | ∃H • H ∈ (σ, X , τ ) Homotopy
               ∧ (∀x • H (x , NR 0 ) = f x ) ∧ (∀x • H (x , NR 1 ) = g x )}
   The case studies include proofs of basic facts about these notions, e.g. the proofs
of the following theorem, whcih stat that the homotopy classes are the equivalence
classes of an equivalence relation:
           `∀σ X τ f        •
                 σ ∈        Topology ∧ τ ∈ Topology
             ∧ f ∈          (σ, τ ) Continuous
             ⇒ f ∈          ((σ, X , τ ) HomotopyClass) f

           `∀σ X τ f        g •
                 σ ∈        Topology ∧ τ ∈ Topology
             ∧ g ∈          ((σ, X , τ ) HomotopyClass) f
             ⇒ f ∈          ((σ, X , τ ) HomotopyClass) g

           `∀σ X τ f        g h •
                 σ ∈        Topology ∧ τ ∈ Topology
             ∧ g ∈          ((σ, X , τ ) HomotopyClass) f
             ∧ h ∈          ((σ, X , τ ) HomotopyClass) g
             ⇒ h ∈          ((σ, X , τ ) HomotopyClass) f
Let us look at the goal resulting from expanding the definition of HomotopyClass
in the proof that the homotopy relation is symmetric (the second of the above three
Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
                                             Now f is continuous (exercise!)         ·     49

theorems). The goal is printed by ProofPower as a sequent with 6 assumptions in
the context and a single conclusion:
         (∗   6   ∗)pσ ∈ Topologyq
         (∗   5   ∗)pτ ∈ Topologyq
         (∗   4   ∗)pH ∈ (σ ×T O R , τ ) Continuousq
         (∗   3   ∗)p∀ x s t• x ∈ X ⇒ H (x , s) = H (x , t)q
         (∗   2   ∗)p∀ x • H (x , 0 .) = f x q
         (∗   1   ∗)p∀ x • H (x , 1 .) = g x q

         (∗ ?` ∗)p∃ H
             • (H ∈ (σ ×T O R , τ ) Continuous
                  ∧ (∀ x s t• x ∈ X ⇒ H (x , s) = H (x , t)))
                  ∧ (∀ x • H (x , 0 .) = g x )
                  ∧ (∀ x • H (x , 1 .) = f x )q
The 6 assumptions give us that H is a homotopy from f to g relative to X with
respect to the topology σ on the domain of f and g and the topology τ on their
range. We are asked to provide a homotopy from g to f . We supply the witness
λ xt • H (Fst xt, NR 1 − Snd xt) and a rewriting tactic then does standard al-
gebraic simplifications using the assumptions to give us the same list of assumptions
and the following conclusion left to prove:
         (∗ ?` ∗)p(λ xt• H (Fst xt, 1 . + ∼ (Snd xt)))
                          ∈ (σ ×T O R , τ ) Continuousq
An application of R continuity tac concludes the proof.
  Deeper topological properties in the case studies include the unique lifting prop-
erty and the homotopy lifting property for covering projections. The proof are
based on proofs given in [May99] and [Spa95].
  The exponential mapping from the real line, R, to the unit circle S 1 in the
complex plane is formally defined in the case studies as follows:
           ExpS1 : R → C


           ∀t• ExpS1 t = (Cos t, Sin t)
   The proof that this is a group homomorphism from R+ to C× follows by easy
algebra from the laws for sines and cosines of sums and does not need the machinery
of this paper. However the proof that it is a covering projection makes extensive
use of the proof procedure for proving continuity and would have been tedious to
find without that. In total (at the time of writing), the proof procedure is used
5 times in the proofs about abstract topology, 22 times in proofs about homotopy
and 13 times in the proofs about topological properties of the complex numbers.

5.   CONCLUDING REMARKS
We believe that success in mechanizing a large corpus of mathematics is crucially
dependent on a powerful array of tools to automate common proof tasks in an in-
teractive theorem proving system. Proving morphismhood in typical formalisations
of specific concrete categories like the categories of topological spaces, groups, etc.
                                          Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
50     ·     R.D. Arthan

is a very common task. We have presented a proof procedure to assist with this
problem that has been implemented in ProofPower and has proved very useful. The
basic ingredients of the proof procedure are the well-known Miller-Nipkow higher-
order matching for linear patterns and backchaining with Horn clauses. The proce-
dure will therefore admit a straightforward implementation in many programmable
theorem-proving systems, for example, the various HOL systems or other members
of the LCF family.
   It is noteworthy that the categories of interest in this paper have a different
flavour from the ones more commonly considered in computer science. Our proof
procedure uses a rewrite system to convert a λ-term into a combinator form. The
rewrite system is similar in spirit to bracket abstraction [Tur79]. However bracket
abstraction makes essential use of the S combinator, which in a typed setting has
polymorphic type (α → β → γ) → (α → β) → α → γ. In a concrete category
that is not cartesian closed, the first parameter of S will not in general be the
type of any morphism in the category. Of the usual categories in which pure
mathematics is conducted, very few (apart from Set) are cartesian closed. Non-
trivial algebraic categories like Grp that have an initial object that is also terminal
cannot be cartesian closed. Top comes closer to being cartesian closed, but while
there are many ways of deriving a topology on X → Y from topologies on X and
Y , pathological cases prevent any such topology from making Top into a cartesian
closed category with respect to the usual product topology [EH02].
   I believe an achievable goal in the not too distant future is a synthesis of ideas
from automated and interactive theorem-proving, computation logic and computa-
tional algebra to provide the computational power and ease of use computer algebra
systems combined with the assurance of machine-checked proof in a framework that
is adequate for modern research-level mathematics. Related work that one hopes
is leading in this direction includes work on constructing a hierarchy of algebraic
structures in Coq using type classes [SvdW11] or canonical structures [Gar11] as
well as work on infrastructure for analysis and geometry [HIH13, Har13].

Acknowledgments
My thanks are due to the referees for their constructive and helpful remarks.

References
[AJ 1]  Rob Arthan and Roger Bishop Jones. Z in HOL in ProofPower. BCS FACS
        FACTS, 2005-1. http://www.lemma-one.com/ProofPower/index/.
[Art14] R.D. Arthan. Product mathematical case studies, 2004-2014. http://
        www.lemma-one.com/ProofPower/examples/examples.html.
[BLM12] Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Improving real
        analysis in coq: A user-friendly approach to integrals and derivatives. In
        Chris Hawblitzel and Dale Miller, editors, Certified Programs and Proofs -
        Second International Conference, CPP 2012, Kyoto, Japan, December 13-
        15, 2012. Proceedings, volume 7679 of Lecture Notes in Computer Science,
        pages 289–304. Springer, 2012.
[CF02] Luis Cruz-Filipe. Formalizing real calculus in Coq. In Victor Carreño,
        César A. Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher
Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
                                             Now f is continuous (exercise!)         ·     51

          Order Logics, Proceedings of the Workshop on Formalising Continuous
          Mathematics, Hampton, VA, USA, August 19, 2002, pages 158–166.
          NASA Technical Report NASA/CP-2002-211736, 2002.
[EH02]    Martı́n Escardó and Reinhold Heckmann. Topologies on spaces of contin-
          uous functions. Topol. Proc., 26(2):545–564, 2002.
[FL96]    Roland Fettig and Bernd Löchner. Unification of higher-order patterns in
          a simply typed lambda-calculus with finite products and terminal type.
          In Harald Ganzinger, editor, Rewriting Techniques and Applications, 7th
          International Conference, RTA-96, New Brunswick, NJ, USA, July 27-
          30, 1996, Proceedings, volume 1103 of Lecture Notes in Computer Science,
          pages 347–361. Springer, 1996.
[Fle00]   Jacques D. Fleuriot. On the mechanization of real analysis in Is-
          abelle/HOL. In Harrison and Aagaard [HA00], pages 145–161.
[Fre70]   Peter Freyd. On the concreteness of certain categories. Sympos. Math.,
          Roma 4, Teoria Numeri, Dic. 1968, e Algebra, Marzo 1969, 431-456
          (1970)., 1970.
[Fre04]   Peter Freyd. Homotopy is not concrete. Repr. Theory Appl. Categ.,
          2004(6):1–10, 2004. http://www.tac.mta.ca/tac/reprints/.
[Gar11]   François Garillot. Generic Proof Tools and Finite Group Theory. Theses,
          Ecole Polytechnique X, December 2011.
[Gor00]   Mike Gordon. From LCF to HOL: a short history. In Gordon D. Plotkin,
          Colin Stirling, and Mads Tofte, editors, Proof, Language, and Interaction,
          Essays in Honour of Robin Milner, pages 169–186. The MIT Press, 2000.
[Got00]   Hanne Gottliebsen. Transcendental functions and continuity checking in
          PVS. In Harrison and Aagaard [HA00], pages 198–215.
[HA00]    John Harrison and Mark Aagaard, editors. Theorem Proving in Higher
          Order Logics: 13th International Conference, TPHOLs 2000, volume 1869
          of Lecture Notes in Computer Science. Berlin: Springer-Verlag, 2000.
[Har98]   John Harrison. Theorem Proving with the Real Numbers. Berlin: Springer-
          Verlag, 1998.
[Har13]   John Harrison. The HOL light theory of euclidean space. J. Autom.
          Reasoning, 50(2):173–190, 2013.
[HIH13]   Johannes Hölzl, Fabian Immler, and Brian Huffman. Type classes and
          filters for mathematical analysis in isabelle/hol. In Sandrine Blazy, Chris-
          tine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem
          Proving - 4th International Conference, ITP 2013, Rennes, France, July
          22-26, 2013. Proceedings, volume 7998 of Lecture Notes in Computer Sci-
          ence, pages 279–294. Springer, 2013.
[Hod93]   Wilfrid Hodges. Model theory. Cambridge: Cambridge University Press,
          1993.
[Mac98]   Saunders Mac Lane. Categories for the Working Mathematician. 2nd ed.
          New York, NY: Springer, 2nd ed edition, 1998.
[May99]   J.P. May. A Concise Course in Algebraic Topology. Chicago, IL: Univer-
          sity of Chicago Press, 1999.

                                          Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
52     ·     R.D. Arthan

[Mil91] Dale Miller. A logic programming language with lambda-abstraction, func-
        tion variables, and simple unification. J. Log. Comput., 1(4):497–536, 1991.
[Nip93] Tobias Nipkow. Functional unification of higher-order patterns. In Pro-
        ceedings, Eighth Annual IEEE Symposium on Logic in Computer Science,
        19-23 June 1993, Montreal, Canada, pages 64–74. IEEE Computer Soci-
        ety, 1993.
[Spa95] Edwin H. Spanier. Algebraic Topology. Berlin: Springer-Verlag, 1995.
[Spi92] J. Michael Spivey. Z Notation - a reference manual (2. ed.). Prentice Hall
        International Series in Computer Science. Prentice Hall, 1992.
[Sti09] Colin Stirling. Decidability of higher-order matching. Logical Methods in
        Computer Science, 5(3), 2009.
[SvdW11] Bas Spitters and Eelis van der Weegen. Type classes for mathematics in
        type theory. Mathematical Structures in Computer Science, 21(4):795–825,
        2011.
[Tur79] D.A. Turner. Another algorithm for bracket abstraction. J. Symb. Log.,
        44:267–271, 1979.




Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
