Up to index of Isabelle/HOL/HOL-Algebra
theory PolyHomo(* 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