Re: [isabelle] Rational functions

Hi Prathamesh,

I'm not aware of a formalization of rational functions, but there is a
polynomial libraries in Isabelle:


    Defines a type: 'a poly, the evaluation function is also called
    A rational function would be a pair (rat poly * rat poly)
    and a evaluation of the function at x 
      rat_fun (n, d) x = poly n x / poly d x

You may also look into ~~/src/HOL/Library/Poly_Deriv and the AFP entry
about Sturm Sequences, here Lib/Misc_Polynomial contains lemmas about
divisibility of polynoms. (it is planned to merge Lib/Misc_Polynomial
into the Isabelle library).

 - Johannes

Am Dienstag, den 27.05.2014, 14:25 +0530 schrieb Prathamesh:
>  Hello,
>  Is there a theory or a construction of rational functions in any of the
> isabelle theories(either in the library or in one of the submitted
> theories). If not, is there a known or an easy way to construct it from any
> of the theories of polynomial functions?
> Regards,
> Prathamesh

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