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