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

Remarks:

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 = …
begin

…

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

…

end

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

subclass (semi)ring_gcd
  …

end

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 = …
begin

…

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

…

end

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

subclass (semi)ring_gcd
  …

end

> 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.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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