*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] HOL/Library/Polynomial pcompose*From*: Walther Neuper <wneuper at ist.tugraz.at>*Date*: Thu, 28 Nov 2013 16:06:16 +0100*In-reply-to*: <5296FD2A.9060700@informatik.tu-muenchen.de>*References*: <5290BAB4.6020108@ist.tugraz.at> <5296FD2A.9060700@informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.1.0

On 11/28/2013 09:22 AM, Florian Haftmann wrote:

Hi Walther, Am 23.11.2013 15:24, schrieb Walther Neuper:the definition definition pcompose :: "'a::comm_semiring_0 poly => 'a poly => 'a poly" where "pcompose p q = fold_coeffs (λa c. [:a:] + q * c) p 0" is not yet used --- what is the purpose of it ?The english Wikipedia defines composition of polynomials as follows: »A composition of two polynomials is a polynomial, which is obtained by substituting a variable of the first polynomial by the second polynomial.« I did not try do match that definition mentally against the Isabelle definition above, but maybe that's it. You might want to check it for your own.

value "pcompose [:1,1,1::int:] [:1,1::int:]" --"Poly [3, 3, 1]" (*substitute for x in (1+x+x^2) by (1+x) = 1 + (1+x) + (1+x)^2 = 3 + 3x + x^2 *)

Cheers, Florian

questions is on the way ;-) Walther

**References**:**[isabelle] HOL/Library/Polynomial pcompose***From:*Walther Neuper

**Re: [isabelle] HOL/Library/Polynomial pcompose***From:*Florian Haftmann

- Previous by Date: [isabelle] feature request: defining tuples
- Next by Date: Re: [isabelle] Isabelle2013-2-RC2 available for testing
- Previous by Thread: Re: [isabelle] HOL/Library/Polynomial pcompose
- Next by Thread: Re: [isabelle] efficient code for ('a, 'b) map (as opposed to ('a, 'b) mapping
- Cl-isabelle-users November 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list