[isabelle-dev] Polynomial theory

[Amine Chaieb]

Hi,


This looks like a nice version of Clemen's Algebra/poly/Univ_Poly2.thy.
I guess it is "justified" to add code-axioms here to implement 'a poly
with a list, or better once one proves the relation to the executable
version, I think Florian has a fancy mechanism to make it work?


We have many polynomials in Isabelle and we need some serious work to
unify the approaches. There is still the locale based (maybe the most
abstract version Algebra/Univ_Poly.thy). I also have a reflective
formalization of Multivariate polynomials which I have not committed.
When we add the Vectors theory (the finite Cartesian product
construction) we could formalize multivariate polynomials appropriately,
then Univariate polynomials will become again an instance of that
general theory. I don't know what is the best way to go...


I recently developed (and still developing) a theory of (univariate)
formal power series (infinite polynomials, if we like) and was
originally also hoping to deduce everything about polynomials from it.
It introduces a type constructor 'a fps which is isomorphic to nat => 'a.


Unfortunately the class mechanism can only constrain the range 'a and
hence we can not recover the polynomials from that formalization. But if
you happen to see a way to do it, then please let me know.


Best wishes,

Amine.


Tobias Nipkow wrote:

> The theory is certainly welcome. Ideally both concrete and abstract
> polynomials should be in the same place and should reference each other,
> to facilitate choice between the theories.
>
> What is the main advantage of abstract polynomials? That "=" is what you
> want it to be? And the main drawback? Non-executability?
>
> Thanks a lot!
> Tobias
>
> Brian Huffman schrieb:
>   
>> Hi all,
>>
>> Recently I was inspired by Mark Janney's comments on the Isabelle users
>> list to finish up the polynomial theory that started working on a while
>> ago. Basically, it is a heavily-reworked version of Clemens Ballarin's
>> theories from HOL/Abstract/poly in the distribution. It includes most of
>> the same operations: coefficients, monomials, degree, scalar
>> multiplication, and all the ring operations. It also includes
>> definitions for div and mod, and is fully integrated with the HOL
>> algebraic type class hierarchy.
>>
>> If there are no objections, I would like to add this theory to the main
>> Isabelle/HOL source directory. Since the main HOL image already includes
>> a list-based formalization of polynomials (Univ_Poly.thy), I think that
>> a formalization using a real type constructor would be an improvement;
>> it probably wouldn't be too hard to adapt the other theories to use the
>> new polynomial type instead.
>>
>> The source file is attached (it will probably only work with the
>> development snapshot).
>>
>> - Brian
>>
>>
>> ------------------------------------------------------------------------
>>
>> _______________________________________________
>> Isabelle-dev mailing list
>> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>     
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>