[isabelle-dev] Isabelle2016-RC0: potential changes

[Thiemann, Rene]

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é