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

lemma (in ring) property three: assumes d ∈ carrier R and h ∈ carrier R

and h ∗ h =0 and h ∗ d ∗ h = h and p = d ∗ h + h ∗ d

shows (1 h =0

proof - from prems show ?thesis by algebra qed

− p ) ∗

Some comments on this proof: firstly, regarding the accuracy of the statement
and, again, the abstraction process mentioned before, it should be pointed out
that from the comparison of the proposed lemma in Isabelle and the prop-
erty stated in Lemma 2 one difference is observed; namely, Lemma 2 says
(id D ∗ −

p ) h =0 hom D ∗ ker p whereas the Isabelle proof corresponds exactly to

(id D ∗ − p ) h =0 hom D ∗ D ∗ since there is only one ring involved in the Isabelle con-

text. This is not a problem in this concrete equality since the value of 0 hom D ∗ ker p
and 0 hom D ∗ D ∗ is equal at every point (because ker p is a graded subgroup of
D ∗ ); so far, the proof implemented in Isabelle, although having a formal differ-
ence with the original proof, can be considered to be an exact implementation
of the mathematical proof. Nevertheless, this kind of situation is the one that
will lead us to seek a more appropriate environment where the different domains
and algebraic structures can be represented.
It is also worth to emphasize the tool support for this style of reasoning:

1. use of locales is of advantage since it clarifies the syntax, shortens the proof
and creates contexts with local assumptions; in our case just by adding (in
ring) in our lemma a specific context is built where R is a generic ring and
all the theorems proved in the existing ring locale appear like facts.
2. the algebra tactic valid for rings automates proofs looking for a normal form
of the given expression (0, in this case).

This approach has some advantages. First of all, it is quite simple and intuitive,
which has the consequence that proofs are quite close to the mathematical proofs
obtained and can be easily understood. As will be seen in Section 4, when more
elaborate approaches are discussed, it is also possible that the size of the proofs
turns them into something unfeasible. Moreover, Isabelle has among its stan-
dard libraries enough theories to produce proofs in the context of the symbolic
approach in a completely automatic way; these generic proofs can be used where
only equational reasoning is required. In addition to this, the basic idea of this
approach will be useful in Sections 5 and 6.
There are also some drawbacks of this method. Firstly, we cannot prove the
other properties needed to complete the implementation the proof of the lemma.
They can not be proved, since information about the domain of the homomor-
phisms or about the concrete definition of the homomorphisms in such domains is
required. For instance, it is not possible to derive with the tools of this framework

that p ker p

x = 0. A second disadvantage observed is the high level of abstraction
required to pass from the mathematical context to the given context in Isabelle.
The type assigned to homomorphisms in this framework, where they are consid-
ered ring elements, is just a generic type α , whereas something more similar to
the mathematical definition of homomorphism would be at least desirable (for
instance, α → β ). In particular, neither the differential group ( D ,d D ∗ )northe

∗