Four Approaches to Automated Reasoning with Differential Algebraic Structures - Artificial Intelligence and Symbolic Computation - page 229

800 lines of Isabelle code were needed to both specify the required structures
and implement the proofs, and a readable proof was obtained.
We would like to point out the following about this approach:

1. A higher degree of accuracy (in comparison to the previous approach) has
been obtained; now the relationship between the objects implemented in the
proof assistant and the mathematical concepts present in the proof is much
clearer.
2. The representation of algebraic structures in Isabelle and Kenzo is performed
in the same way, using records where each field represents an operator. On
the other hand, homomorphisms have a simpler representation in Isabelle
since they are just elements of a functional type whereas in Kenzo they are
also records, allowing that way to keep explicit information over their domain
and codomain.
3. Converting homomorphisms into total functions by the use of “arbitrary”
makes things a bit more complex. From the formal point of view, it is dif-
ficult to identify a homomorphism containing an arbitrary element, i.e., a
conditional statement “if x G then fx else arbitrary”, with any mathemat-

ical object; there is a gap in the abstraction process that cannot be directly
filled. A solution to clarify this process by identifying the elements outside
the domain with a special element of the homomorphism's codomain will be
proposed in Section 5; with this idea are avoided the non defined values of
the total function representing a concrete homomorphism. This solution has
been proposed before and its disadvantages are well known, but making a
careful use of it can make mechanization easier.
4. Homomorphisms are represented by conditional statements, and working
with n homomorphisms at the same time one has to consider 2 n cases. There
are two solutions to this problem. The first one consists in enhancing the
homomorphisms with an algebraic structure allowing to reason with them
like elements of this structure in an equational way (for instance, an abelian
group or a ring). With this implementation, proofs can sometimes avoid to
get into the concrete details of the representation of homomorphisms in the
theorem prover. To some extent this can be understood as the development
of a new level of abstraction; some steps (or computations) are developed at
the level of the elements of the homomorphisms domains whereas some are
developed at the level of the structure where homomorphisms are embedded.
This forces to implement proof steps more carefully and also to make a
correct choice of the homomorphisms that can be provided with an algebraic
structure, and will be discussed in Section 5. A second possible solution not
implemented yet using equivalence classes will be mentioned as future work
in Section 7.

∈

5 A Homomorphism Approach

If we capitalize the advantages of both the symbolic approach and the set the-
oretic approach and we combine them carefully, it is possible to obtain a new