[isabelle-dev] Euclidean Ring

[Florian Haftmann]

Hi Manuel,

> On 27/06/15 09:06, Florian Haftmann wrote:
>> What about: »a = unit_factor a * normalize a«
> Sounds reasonable.

See now cb21b7022b00 ff.

After accepting that gcd must always target a normalized segment of the
underlying ring structure, it is quite obvious how the abstract
specification for lcm and gcd must look like.  See theory GCD.thy.

Using »normalize«, the propositions »a is associated to b« becomes
simply »normalize a = normalize b« – logically a little stronger since
an explicit normalization is required, but morally equal since such a
normalization can be easily provided for all typical candidates.

This insight seems to me the final breakthrough after spending approx.
10 years of thinking on gcd.

>> See (EF1) in https://en.wikipedia.org/wiki/Euclidean_domain#Definition –
>> note the »either r = 0 or f(r) < f(b)«.  Note »either r <--> a mod b = 0
>> <--> b dvd a«.  Without that termination condition, you cannot prove
>> that polynomials are an euclidean semiring.
> That is not entirely true. Your weaker assumption allows for a slightly
> simpler instantiation, but my previous instantiation for polynomials used
> 
> definition [simp]: "euclidean_size_poly p \<equiv>
>       (if p = 0 then 0 else degree p + 1)"

I see.  I turned to the original specification again.

> (see https://github.com/3of8/isabellehol_gcd/blob/master/Polynomial.thy
> and also the other files on that Github repository)

Having material in drawers is risky since, without mechanical connection
to the distribution, it gets rotten quite fast.
Is there anything from there still missing in the Isabelle repository?

What comes next?  The existing theorems on gcd/lcm/Gcd/Lcm on nat/int
must be generalized as far as possible, duplicates identified and
possibly thrown away.

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/20150710/bd7a90f5/attachment.asc>