[isabelle-dev] Euclidean Ring

[Florian Haftmann]

Hi Manuel,

you may have noticed the recent developments concerning euclidean rings,
with the ultimate goal to include this into the main corpse of the HOL
theories.

Currently I have the following questions:

1. Normalization. Currently, there is normalization_factor such that a
div normalization_factor a yields the normalized elements. My impression
is that the latter should be an operation on its own, say normalize, and
that normalization_factor is a misleading name since it suggests that
actually a * normalization_factor a is the normalized element. Have we
any other plausible name, say »orientation«? The idea is that normalize
and orientation work on integers like abs and sgn.

2. A generic lcm definition. In ordinary lattices, inf and sup are dual
to each other and there is little reason to prefer one over that other.
Concerning gcd and lcm, I have the strong impression that gcd is the
more primitive one and lcm should be solely derived from it. This is
supported by the observation that instantiation proofs get horrible if
you have to derive the characteristic properties of gcd and lcm on, say,
nat, simultaneously. Hence I argue that the specification of
semiring_gcd should contain a plain definition of lcm. Since the plain
semiring_gcd is not supposed to know anything about normalization, this
would lead to a plain »lcm a b = a * b div gcd a b«, in contrast to the
current »lcm a b = a * b div gcd a b div normalization_factor (a * b)«.
Do you foresee any difficulties here?

3. Gcd/Lcm. In your Gcd/Lcm approach, Lcm is the »more primitive«
definition.  Did you just take this over from src/HOL/GCD.thy, or is
there a deeper reason to do it this way round?

A further observation concerns algebraic closedness of normalized
elements. The properties »normalization_factor 1 = 1« and
»normalization_factor (a * b) = normalization_factor a *
normalization_factor b« state that normalized elements form a
multiplicative group. I did not find a reasonable characterization for
the additive behaviour, i.e. a way to enforce that for int normalization
goes for positive elements only and not a funny mixture like 1, -2, 3,
4, 5, -6, 7, -8. The tempting option to demand closedness under addition
does not work for polynomials, since x + x = 2 * x is not normalized any
longer. On the other hand, the theory works without any such enforcement.

Any suggestions?
Cheers,
	Florian

-- 

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20150625/60525854/attachment.asc>