[isabelle-dev] Isabelle2016-RC0: potential changes

[Manuel Eberl]

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

Ironically, quite a few of those facts were already proven independently 
in other AFP entries by Wenda Li and/or me. (e.g. the ones about pcompose)


 > So why should the small proof below be not integrated for the 2016 
release?

This is probably a question for Florian. I introduced Euclidean rings to 
allow a more systematic derivation of (constructive) GCDs about two 
years ago or so.

Since then, Florian cleaned this up and improved it a lot, but from what 
I gathered, there is much to be done yet. I should probably have taken 
care of this already, but I never quite found the time; I shall attempt 
to do that this year.

As for the release, perhaps Florian can comment on whether anything 
speaks against moving this instance into the Polynomial theory.


Cheers,

Manuel


On 12/01/16 09:21, Thiemann, Rene wrote:
> 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é
>