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

First the structures (the variables) needed for the local scope are fixed and then
their components are defined. Once all these assumptions have been made, the
statement of lemmas will have the following appearance 6 :

lemma (in hom complection environment) reduction property one:
assumes p

∈ carrier R

carrier ker p then id x else one ker p )=one R show (one R 3 p) ◦ ( λx .if x ∈

By specifying (in hom complection environment) we introduce all the facts
present in the locale hom complection environment and then they can be used as
theorems in our lemma. The previous statement corresponds to property (2) of
Def. 2 specialized for Lemma 2. Using these tools, we get a framework very close
to the one in the mathematical lemmas. Moreover, proofs can be mechanized in
a readable style quite similar to the mathematical proofs, and only some repeti-
tive steps have to be added to explicitly obtain the value of the fields of the fixed
algebraic structures when needed; proofs are easy to read and similar to the ones
made “by hand”. All these features make this framework quite satisfactory. On
the other hand, from the formal point of view there is also a drawback. The
operation appearing in the statement of the lemma can not be identified with

any of the operations of the framework. It composes elements of different alge-
braic structures such as hom(ker p, d D ∗

◦

)
but whose relation has not been made explicit at any point inside the locale. The
composition

)(ker p, d D ∗ ), hom( D ,d D ∗ )(ker p, d D ∗

∗

is valid in this case since all the elements of the carrier sets are im-
plemented trough functions, and therefore they can be composed. Even in other
cases, the operation relating the different structures could be implemented, but
there is no mathematical correspondence for this external op

◦

; this produces a
gap in the abstraction function that permits to identify mathematical objects
with their representation in the theorem prover.

◦

7 Conclusions and Further Work

A design “from bottom to top” has been used to implement the proof of the BPL
in Isabelle. Instead of considering algebraic topology as a whole and formalizing
generic concepts of this theory, our approach started from a very concrete (and
relevant) lemma (the BPL) in this area that could allow to estimate the real
capabilities from Isabelle to work with differential structures and their homo-
morphisms. We also started from a simple attempt (in Section 3) that gave us
helpful ideas for the following approaches about what tools were directly avail-
able in Isabelle and those other tools that should be supplied to the system.
The Isabelle tools introduced in Section 4 were not enough to produce readable
proofs. Then, in Section 5, an original framework where several computations
with homomorphisms can be carried out was suggested. The implementation of
these tools led us to the problem of what changes must be made into partial

6 In Isabelle syntax, 3 is a reference to the “minus” operation in the third structure
of our locale definition, ring R .