Re: [isabelle] Gcd and algebraic structures

Hi Jose,

your are actually stumbling over the issue that HOL so far does not
really provide a hierarchy of type classes for divisibility in rings
(say, factorial ring, euclidean ring etc.)

Here my thoughts of what can be done with reasonable effort at the moment

1) The syntactic gcd type class.

Cf. also Manuel's mail.  Syntactic type classes can also be seen as an
instance of the traditional »worse is better« philosophy of UNIX: if you
do not know how to provide the right policy, restrict yourself to
provide a mechanisms while leaving the user to provide its own policy on
his own.

2) A fundamental algebraic type class for GCD.

IMHO this could look like:

> class semiring_gcd = semiring + gcd +
>   assumes "gcd a b dvd a"
>   assumes "gcd a b dvd b"
>   assumes "c dvd a ⟹ c dvd b ⟹ c dvd gcd a b"
> class ring_gcd = ring + semiring_gcd


a) I strongly believe the assumptions capture the essence of gcd,
whatever the underlying structure is.

b) Whenever you develop type class hierarchies for ring structures, you
always have a semiring (the additive structure is a monoid, not a group)
and a ring.  The semiring part of the hierarchy is to accommodate the
natural numbers (which, in algebra, appear not be that natural after all).

c) Here I have chosen »semiring«/»ring« as a base point.  Maybe gcd
itself suggests are more specific entry point to start with already, but
I have found no argument to do so (maybe you would do after some rounds
of experimenting and thinking).

d) The specification implicitly states
  I. the a gcd exists
  II. that is is functional, i.e. normalising wrt. to units
But it does not assume anything how this normalisation actually looks
like, i.e. concrete instances are free to normalise in a specific way.

3) Specific instances for GCD in more specific algebraic structures

a) e.g. for euclidean rings

class euclidean_(semi)ring = …


definition gcd_eucl where … -- ‹definition via euclidean algorithm›



class euclidean_(semi)ring_gcd = euclidean_(semi)ring + gcd
  assumes "gcd = gcd_eucl"

subclass (semi)ring_gcd


Note that this work has already been done by Manuel, but is not yet part
of Isabelle2014.  If you want to build on that, we will find a suitable
way without need to participate in the ongoing Isabelle development.

b) e.g. for factorial rings

class factorial_(semi)ring = …


definition factorization :: "'a => 'a mulitset" where …



class factorial_(semi)ring_gcd = factorial_(semi)ring + gcd
  assumes "gcd a b = msetprod (factorization a + factorization b)"

subclass (semi)ring_gcd


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

»interpretation« pulls in facts into the current target context, which
is closed at the final »end« – »confined interpretation«.

»sublocale« establishes a permanent connection.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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