[isabelle] Gcd and algebraic structures



Dear all,

I would like to formalise some linear algebra structures, such as principal
ideal rings, principal ideal domains, unique factorization domains and so
on.

As part of those structures, there exist some basic operations over rings
such as gcd and div, which are already implemented in the Isabelle library.
For instance, there is a class gcd in the library which has been
instantiated by int and nat:

class gcd = zero + one + dvd +
  fixes gcd :: "'a => 'a => 'a"
    and lcm :: "'a => 'a => 'a"

begin



Nevertheless, this class seems to me somehow strange, because it doesn’t
fix any property about gcd and lcm, so it could be instantiated by almost
anything.

Moreover, the notion of greatest common divisor can be properly defined in
commutative rings, and also in principal ideal rings, although in general
there need not exist just one for every pair of elements.

My doubt is how to include that concept in the principal ideal ring class
that I’m formalising.

I think that there are (at least) three options:

1.- “Forget” the gcd class that exists in the library and define gcd inside
my class:

class pir = comm_ring_1 + assumes all_ideal_is_principal: "∀I. ideal I ⟶
principal_ideal I"

begin

definition "gcd_pir a b = ....."

end

2.- Define a class called “pir_gcd”, extending gcd and assuming what gcd
must satisfy.

class pir_gcd = comm_ring_1 + gcd + assumes all_ideal_is_principal: "∀I.
ideal I ⟶ principal_ideal I"  and "∀a b. gcd a b = ..." and "∀a b. lcm a b
= ..."

3.- Option 1 + interpretations/sublocales.

class pir = comm_ring_1 + assumes all_ideal_is_principal: "∀I. ideal I ⟶
principal_ideal I"

begin

definition "gcd_pir a b = ....."

definition "lcm_pir a b = ....."

interpretation gcd "0::'a" 1 "times::'a=>'a=>'a" "gcd_pir" "lcm_pir" .

sublocale gcd "0::'a" 1 "times::'a=>'a=>'a" "gcd_pir" "lcm_pir" .

end

By the way, what is the difference between interpretation and sublocale in
this context?

Which is the recommended option? At first I though that it was the last
one, but then I wondered why the second one has been used in the library
(there are two classes: semiring and semiring_div in the library instead of
only one of them).

Thanks,
Jose



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.