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:

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

theorem SUM_extend:

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

theorem DiagSum:

  (∑kn + m. ∑ik. f i * g (k - i)) = (∑kn + m. ∑in + m - k. f k * g i)

theorem CauchySum:

  [| bound n f; bound m g |]
  ==> (∑kn + m. ∑ik. 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