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

elements of the domain D appear. Therefore, the conceptual distance between

Isabelle code and the mathematical content is too large. From a more practical
point of view, the previous discussion on types shows that the computational
content of homomorphisms (that is to say, their interpretation as functions) is
lost, which prevents code extraction.

∗

4 A Set Theoretic Approach

The previous approach offers a high level of abstraction but is insucient to
prove our theorems. In this section we present a framework where the algebraic
structures are again represented by records, but homomorphisms are now rep-
resented as functions.
There are two main components in this framework. One is the algebraic struc-
tures involved and the other one is the homomorphisms between these structures.
In Isabelle, declarations of constants (including algebraic structures or homo-
morphisms) consist of a type 2 and a defining axiom. Algebraic structures are
implemented over extensible record types (see [11]); this permits record subtyp-
ing and parametric polymorphism, and thus algebraic structures can be derived
using inheritance. As an example, a differential group can be defined in Isabelle
as

record α diff group = α monoid +
diff :: α

⇒ α

diff group C ≡ ab group C ∧ diff ∈ hom CC ∧

∀ x ∈ carrier C .diffdiffx=one C

For homomorphisms, again a type and a definition must be declared. In the
Isabelle type system all functions are total, and therefore homomorphisms (which
are partial functions over generic types) are implemented through total functions;
the homomorphisms between two given algebraic structures will be the set of all
total functions between two types, for which the homomorphism axioms hold 3

hom :: [( α , θ ) monoid scheme, ( β , γ ) monoid scheme] ⇒ ( α ⇒ β )set

hom AB ≡{ f . f ∈ carrier A → carrier B ∧ f ( x ∗ A y )=( fx ) ∗ B ( fy ) }

Since in Isabelle equality (=) is total on types, problems arise when comparing
homomorphisms (or partial functions, in general). A way of getting out of this
situation is to use “arbitrary”, which denotes (for every type) an arbitrary but
unknown value. Doing so is sound, because types are inhabited. Partial functions
can be simulated by assigning them to “arbitrary” outside of their domain.
With these definitions we have implemented the complete proof of Lemma 1.
This proof takes advantage of the above mentioned inheritance among algebraic
structures, starting from sets, with the definition of a bijection between sets, and
then introducing the inherited structures step by step. Following this scheme,

2 In Isabelle syntax, f :: α = >β denotes a total function from type α to type β .
3 In Isabelle syntax, {x.f ( x ) } denotes set comprehension.