*To*: Wenda Li <wl302 at cam.ac.uk>, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] Code setup for Fraction_Field*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Thu, 10 Sep 2015 12:16:11 +0200*Cc*: Manuel Eberl <eberlm at in.tum.de>, prathamesh at imsc.res.in, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <6dac9d570b17350fd14f5226d3b52b1c@cam.ac.uk>*Organization*: TU Munich*References*: <55DED10F.5030507@inf.ethz.ch> <55DEDF86.3010508@in.tum.de> <55E02EAA.506@inf.ethz.ch> <6dac9d570b17350fd14f5226d3b52b1c@cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:38.0) Gecko/20100101 Thunderbird/38.2.0

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!? Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

- Previous by Date: Re: [isabelle] Expansion of let-bindings in proofs
- Next by Date: Re: [isabelle] Code setup for Fraction_Field
- Previous by Thread: Re: [isabelle] Code setup for Fraction_Field
- Next by Thread: [isabelle] New AFP entry: Converting LTL to Deterministic (Generalised) Rabin Automata
- Cl-isabelle-users September 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list