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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev