Re: [isabelle] Code setup for Fraction_Field

Hi all,

>> 3. For fraction fields over polynomials over rings (rather than
>> fields), one can use subresultants, but I have not been able to find
>> them formalised in Isabelle. Are they hidden somewhere? If not, are
>> there any plans to formalise them?
> Are subresultants really necessary for this?
> definition ppdivmod_rel :: "'a::idom poly â 'a poly â 'a poly â 'a poly
> â 'a â bool"
> where
>   "ppdivmod_rel x y q r m â (
>       smult m x = q * y + r â (if y = 0 then q = 0 else r = 0 â degree r
> < degree y)
>       â  ( m= (if x=0 â y=0 then 1 else (lead_coeff y) ^ (degree x + 1 -
> degree y))))"

I am somehow lost how the Âalgebraic stack is supposed to look like in
the whole example.  Something like Fraction over Poly over Int?
Since Poly over Int forms a factorial ring but not an euclidean ring,
the question is how to generalize normalization of quotients a / b
accordingly.  It won't work naturally with type classes:

	Poly over Rat --> normalization via gcd / eucl
	Poly over Poly over Rat --> somehow different

Hence, some type class magic would be needed to detect whether to use
the rather efficient euclidean algorithm or something different â or
even refrain from normalization at all!?



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.