# Theory PolyHomo

Up to index of Isabelle/HOL/HOL-Algebra

theory PolyHomo
imports UnivPoly2
uses [PolyHomo.ML]
begin

    (*
        Universal property and evaluation homomorphism of univariate polynomials
        $Id: PolyHomo.thy,v 1.7 2005/09/17 18:49:15 wenzelm Exp $
        Author: Clemens Ballarin, started 15 April 1997
    *)

    theory PolyHomo imports UnivPoly2 begin

    consts
      EVAL2 :: "['a::ring => 'b, 'b, 'a up] => 'b::ring"
      EVAL  :: "['a::ring, 'a up] => 'a"

    defs
      EVAL2_def:    "EVAL2 phi a p ==
                     setsum (%i. phi (coeff p i) * a ^ i) {..deg p}"
      EVAL_def:     "EVAL == EVAL2 (%x. x)"

    end

theorem SUM_shrink:

      [| m ≤ n; !!i. [| m < i; i ≤ n |] ==> f i = (0::'a); P (setsum f {..n}) |]
      ==> P (setsum f {..m})

theorem SUM_extend:

      [| m ≤ n; !!i. [| m < i; i ≤ n |] ==> f i = (0::'a); P (setsum f {..m}) |]
      ==> P (setsum f {..n})

theorem DiagSum:

      (∑k≤n + m. ∑i≤k. f i * g (k - i)) = (∑k≤n + m. ∑i≤n + m - k. f k * g i)

theorem CauchySum:

      [| bound n f; bound m g |]
      ==> (∑k≤n + m. ∑i≤k. f i * g (k - i)) = setsum f {..n} * setsum g {..m}

theorem EVAL2_homo:

      homo phi ==> homo (EVAL2 phi a)

theorem EVAL2_const:

      EVAL2 phi a (b*X^0) = phi b

theorem EVAL2_monom1:

      homo phi ==> EVAL2 phi a ((1::'a)*X^1) = a

theorem EVAL2_monom:

      homo phi ==> EVAL2 phi a ((1::'a)*X^n) = a ^ n

theorem EVAL2_smult:

      homo phi ==> EVAL2 phi a (b *s p) = phi b * EVAL2 phi a p

theorem monom_decomp:

      a*X^n = a*X^0 * ((1::'a)*X^n)

theorem EVAL2_monom_n:

      homo phi ==> EVAL2 phi a (b*X^n) = phi b * a ^ n

theorem EVAL_homo:

      homo (EVAL a)

theorem EVAL_const:

      EVAL a (b*X^0) = b

theorem EVAL_monom:

      EVAL a ((1::'a)*X^n) = a ^ n

theorem EVAL_smult:

      EVAL a (b *s p) = b * EVAL a p

theorem EVAL_monom_n:

      EVAL a (b*X^n) = b * a ^ n