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