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

homomorphismsasrecordssometimes slows down the interactive proof steps. A
likely cause for this loss of performance are ineciencies in the record package
of Isabelle2003 5 . A record encoding a homomorphism is a rather large data
structure and contains a lot of redundant information. For instance, in f : D

∗ →

D itself is already

a quite large record. It appears that when several homomorphism are involved
in a proof, the redundancies cause a slowed response time of the interactive
environment.

, the corresponding record contains four copies of D ,and D

∗ ∗ ∗

6 Instantiating Locales

A final method based on the instantiation of locales (see [1]), a tool recently
implemented in Isabelle that could be of great help for this kind of problems,
is also considered. Locales, which are light-weight modules, define local scopes
for Isabelle; some fixed assumptions are made and theorems can be proved from
these assumptions in the context of the locale.
With the instantiation of locales it is not possible to define generic frame-
works, but the method has a great expressiveness for concrete problems. The ap-
proach presented in this section is based to some extent on the ideas introduced
in the first approach, considering homomorphisms embedded in an algebraic
structure, but with the clear advantage that now several algebraic structures
can be defined at the same time (this will allow us to introduce rings R and R ,
abelian groups A and A , and so on) and the elements of these structures can
be instantiated with their real components. For instance, R could be instanti-
ated with hom( D ,d D ∗ )( D ,d D ∗ ) as carrier set and the usual composition ◦ as

∗ ∗

product, R with carrier hom(ker p, d D ∗ )(ker p, d D ∗ ) and operation ◦ as product,

A with carrier hom( D ) and so on. This permits to work with

homomorphisms at two different levels. In a first one, they can be considered
as elements of the algebraic structures and the computations between the ele-
ments of these algebraic structures are identified with the steps of the proofs. In
the second level, the operations of the algebraic structures can be instantiated
to their definition (for instance, “mult =

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

∗

∗ D gx ”) as
well as the structures (in our case, the differential groups or chain complexes),
in order to complete the proof steps requiring this information (for instance,

◦ ”or“sum= λf g.λx.f x

p ker p x = 0). The structure of the locale needed to implement the proofs of

Lemma 2 in Isabelle would now look as follows:

locale hom completion environment = comm group G +commgroup K +
ring R +ring R 0 +commgroup A +commgroup A 0 +varp+
assumes R = (carrier = hom complection GG ,mult=op

◦

, one = ...)

and R = ...
defines K = ker p

5 These have been removed in the latest release, Isabelle2004, but we have not yet
ported our proofs.