[isabelle-dev] Isabelle2016-RC0: potential changes

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 836 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160114/21666047/attachment.sig>