Re: [isabelle] Rational functions

Also in HOL/Library you will find Fraction_Field.thy, which defines a
type constructor 'a fract that gives the field of fractions over any
integral domain 'a. You can combine this with the polynomial type from
Polynomial.thy to get a type of rational functions: e.g. "real poly
fract" would be the type of rational functions with real coefficients.

Fraction_Field.thy seems to be a bit spartan at the moment, not
providing a lot of operations or theorems beyond basic arithmetic
stuff. Please let us know about any suggestions for
additions/improvements you'd like to see, so we can make the libraries

Hope this helps,

- Brian

On Tue, May 27, 2014 at 2:46 AM, Johannes Hölzl <hoelzl at> wrote:
> Hi Prathamesh,
> I'm not aware of a formalization of rational functions, but there is a
> polynomial libraries in Isabelle:
>   ~~/src/HOL/Library/Polynomial:
>     Defines a type: 'a poly, the evaluation function is also called
> "poly".
>     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.