Hi all, > 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.
I have already some post-release patches in the pipeline which would add
this instance anyway. So, there is no demand for action here at the moment.
Note that the classes (semi)ring_gcd in Isabelle2015 had no lemmas and
thus very hardly different from syntactic classes, so there is no loss
of generality here.
Cheers,
Florian
>
>
> 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é
>>
--
PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
