[isabelle-dev] Isabelle2016-RC0: potential changes

Thiemann, Rene Rene.Thiemann at uibk.ac.at
Tue Jan 12 09:21:42 CET 2016

```Hi Manuel,

> I added the efficient code equations for fact and binomial, and similar ones for pochhammer and gbinomial.
>
> I also adapted everything from Square_Free_Factorization and Missing_Polynomial that seemed to be of general interest to me (especially the generalisation of the type of pderiv).

thanks a lot; in the meantime, I deleted this material from the AFP-entries.

>
> I also noticed the ring_gcd instance for polynomials. Finalising the changes to the GCD class hierarchy and updating the AFP entries that rely on half-finished versions of this change (such as Echelon_Form) is something that I should probably take care of soon, but definitely not before the 2016 release – hopefully before the 2017 one.

The absence of the ring_gcd instance for polynomials is strange from my perspective: In Isabelle 2015 we had

instantiation poly :: (field) gcd

where the gcd-class contained the important properties of a gcd.

In Isabelle 2016-RC0 there also is

instantiation poly :: (field) gcd

but now the gcd-class is purely syntactic. Here, to get the same properties of a gcd (and more), the corresponding instance would be

instantiation poly :: (field) semiring_gcd   (or ring_gcd)

So why should the small proof below be not integrated for the 2016 release? Otherwise, there
is no class-based gcd for polynomials available for 2016, in contrast to 2015.

instance poly :: (field) ring_gcd
proof
fix a b :: "'a poly"
show "normalize (gcd a b) = gcd a b" by (simp add: normalize_poly_def poly_gcd_monic)
show "lcm a b = normalize (a * b) div gcd a b"
proof (cases "a * b = 0")
case False
show ?thesis unfolding lcm_poly_def normalize_poly_def
by (subst div_smult_right, insert False, auto simp: div_smult_left)
(metis coeff_degree_mult divide_divide_eq_left divide_inverse_commute inverse_eq_divide)
next
case True
thus ?thesis by (metis div_0 lcm_poly_def normalize_0)
qed
qed auto

Cheers,
René
```