Re: [isabelle] HOL/Library/Polynomial pcompose



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

Thank you very much -- suppose, this was the last simple question, a new round of
questions is on the way ;-)

Walther




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