# Re: [isabelle] Rational functions

```Thanks for the help.
Prathamesh

On Tue, May 27, 2014 at 8:47 PM, Brian Huffman <huffman.brian.c at gmail.com>wrote:

> 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
> additions/improvements you'd like to see, so we can make the libraries
> better!
>
> Hope this helps,
>
> - Brian
>
> On Tue, May 27, 2014 at 2:46 AM, Johannes Hölzl <hoelzl at in.tum.de> 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
> > 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
> >
> >
> >
>

--
"Men make their own history, but they do not make it as they please; they
do not make it under self-selected circumstances, but under circumstances
existing already, given and transmitted from the past. The tradition of all
dead generations weighs like a nightmare on the brains of the living."

The Eighteenth Brumaire of Louis Bonaparte, Karl Marx

```

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