Email Gateway (Aug 19 2022 at 14:24): Email Gateway (Aug 19 2022 at 14:24):From: Prathamesh <prathamesh.t@gmail.com>
Thanks for the help.
Prathamesh
Email Gateway (Aug 19 2022 at 14:33):From: Prathamesh <prathamesh.t@gmail.com>
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
Email Gateway (Aug 19 2022 at 14:33):From: Johannes Hölzl <hoelzl@in.tum.de>
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).
Email Gateway (Aug 19 2022 at 14:34):From: Brian Huffman <huffman.brian.c@gmail.com>
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
better!
Hope this helps,
Last updated: Apr 24 2024 at 20:16 UTC