--- a/src/HOL/Algebra/poly/PolyHomo.thy Mon Mar 25 19:53:44 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,187 +0,0 @@
-(* Author: Clemens Ballarin, started 15 April 1997
-
-Universal property and evaluation homomorphism of univariate polynomials.
-*)
-
-theory PolyHomo
-imports UnivPoly2
-begin
-
-definition
- EVAL2 :: "['a::ring => 'b, 'b, 'a up] => 'b::ring" where
- "EVAL2 phi a p = setsum (%i. phi (coeff p i) * a ^ i) {..deg p}"
-
-definition
- EVAL :: "['a::ring, 'a up] => 'a" where
- "EVAL = EVAL2 (%x. x)"
-
-lemma SUM_shrink_lemma:
- "!! f::(nat=>'a::ring).
- m <= n & (ALL i. m < i & i <= n --> f i = 0) -->
- setsum f {..m} = setsum f {..n}"
- apply (induct_tac n)
- (* Base case *)
- apply (simp (no_asm))
- (* Induction step *)
- apply (case_tac "m <= n")
- apply auto
- apply (subgoal_tac "m = Suc n")
- apply (simp (no_asm_simp))
- apply arith
- done
-
-lemma SUM_shrink:
- "!! f::(nat=>'a::ring).
- [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..n}) |]
- ==> P (setsum f {..m})"
- apply (cut_tac m = m and n = n and f = f in SUM_shrink_lemma)
- apply simp
- done
-
-lemma SUM_extend:
- "!! f::(nat=>'a::ring).
- [| m <= n; !!i. [| m < i; i <= n |] ==> f i = 0; P (setsum f {..m}) |]
- ==> P (setsum f {..n})"
- apply (cut_tac m = m and n = n and f = f in SUM_shrink_lemma)
- apply simp
- done
-
-lemma DiagSum_lemma:
- "!!f::nat=>'a::ring. j <= n + m -->
- setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..j} =
- setsum (%k. setsum (%i. f k * g i) {..j - k}) {..j}"
- apply (induct_tac j)
- (* Base case *)
- apply (simp (no_asm))
- (* Induction step *)
- apply (simp (no_asm) add: Suc_diff_le natsum_add)
- apply (simp (no_asm_simp))
- done
-
-lemma DiagSum:
- "!!f::nat=>'a::ring.
- setsum (%k. setsum (%i. f i * g (k - i)) {..k}) {..n + m} =
- setsum (%k. setsum (%i. f k * g i) {..n + m - k}) {..n + m}"
- apply (rule DiagSum_lemma [THEN mp])
- apply (rule le_refl)
- done
-
-lemma CauchySum:
- "!! f::nat=>'a::ring. [| bound n f; bound m g|] ==>
- setsum (%k. setsum (%i. f i * g (k-i)) {..k}) {..n + m} =
- setsum f {..n} * setsum g {..m}"
- apply (simp (no_asm) add: natsum_ldistr DiagSum)
- (* SUM_rdistr must be applied after SUM_ldistr ! *)
- apply (simp (no_asm) add: natsum_rdistr)
- apply (rule_tac m = n and n = "n + m" in SUM_extend)
- apply (rule le_add1)
- apply force
- apply (rule natsum_cong)
- apply (rule refl)
- apply (rule_tac m = m and n = "n +m - i" in SUM_shrink)
- apply (simp (no_asm_simp) add: le_add_diff)
- apply auto
- done
-
-(* Evaluation homomorphism *)
-
-lemma EVAL2_homo:
- "!! phi::('a::ring=>'b::ring). homo phi ==> homo (EVAL2 phi a)"
- apply (rule homoI)
- apply (unfold EVAL2_def)
- (* + commutes *)
- (* degree estimations:
- bound of all sums can be extended to max (deg aa) (deg b) *)
- apply (rule_tac m = "deg (aa + b) " and n = "max (deg aa) (deg b)" in SUM_shrink)
- apply (rule deg_add)
- apply (simp (no_asm_simp) del: coeff_add add: deg_aboveD)
- apply (rule_tac m = "deg aa" and n = "max (deg aa) (deg b)" in SUM_shrink)
- apply (rule le_maxI1)
- apply (simp (no_asm_simp) add: deg_aboveD)
- apply (rule_tac m = "deg b" and n = "max (deg aa) (deg b) " in SUM_shrink)
- apply (rule le_maxI2)
- apply (simp (no_asm_simp) add: deg_aboveD)
- (* actual homom property + *)
- apply (simp (no_asm_simp) add: l_distr natsum_add)
-
- (* * commutes *)
- apply (rule_tac m = "deg (aa * b) " and n = "deg aa + deg b" in SUM_shrink)
- apply (rule deg_mult_ring)
- apply (simp (no_asm_simp) del: coeff_mult add: deg_aboveD)
- apply (rule trans)
- apply (rule_tac [2] CauchySum)
- prefer 2
- apply (simp add: boundI deg_aboveD)
- prefer 2
- apply (simp add: boundI deg_aboveD)
- (* getting a^i and a^(k-i) together is difficult, so we do it manually *)
- apply (rule_tac s = "setsum (%k. setsum (%i. phi (coeff aa i) * (phi (coeff b (k - i)) * (a ^ i * a ^ (k - i)))) {..k}) {..deg aa + deg b}" in trans)
- apply (simp (no_asm_simp) add: power_mult leD [THEN add_diff_inverse] natsum_ldistr)
- apply (simp (no_asm))
- (* 1 commutes *)
- apply (simp (no_asm_simp))
- done
-
-lemma EVAL2_const:
- "!!phi::'a::ring=>'b::ring. EVAL2 phi a (monom b 0) = phi b"
- by (simp add: EVAL2_def)
-
-lemma EVAL2_monom1:
- "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 1) = a"
- by (simp add: EVAL2_def)
- (* Must be able to distinguish 0 from 1, hence 'a::domain *)
-
-lemma EVAL2_monom:
- "!! phi::'a::domain=>'b::ring. homo phi ==> EVAL2 phi a (monom 1 n) = a ^ n"
- apply (unfold EVAL2_def)
- apply (simp (no_asm))
- apply (case_tac n)
- apply auto
- done
-
-lemma EVAL2_smult:
- "!!phi::'a::ring=>'b::ring.
- homo phi ==> EVAL2 phi a (b *s p) = phi b * EVAL2 phi a p"
- by (simp (no_asm_simp) add: monom_mult_is_smult [symmetric] EVAL2_homo EVAL2_const)
-
-lemma monom_decomp: "monom (a::'a::ring) n = monom a 0 * monom 1 n"
- apply (simp (no_asm) add: monom_mult_is_smult)
- apply (rule up_eqI)
- apply (simp (no_asm))
- done
-
-lemma EVAL2_monom_n:
- "!! phi::'a::domain=>'b::ring.
- homo phi ==> EVAL2 phi a (monom b n) = phi b * a ^ n"
- apply (subst monom_decomp)
- apply (simp (no_asm_simp) add: EVAL2_homo EVAL2_const EVAL2_monom)
- done
-
-lemma EVAL_homo: "!!a::'a::ring. homo (EVAL a)"
- by (simp add: EVAL_def EVAL2_homo)
-
-lemma EVAL_const: "!!a::'a::ring. EVAL a (monom b 0) = b"
- by (simp add: EVAL_def EVAL2_const)
-
-lemma EVAL_monom: "!!a::'a::domain. EVAL a (monom 1 n) = a ^ n"
- by (simp add: EVAL_def EVAL2_monom)
-
-lemma EVAL_smult: "!!a::'a::ring. EVAL a (b *s p) = b * EVAL a p"
- by (simp add: EVAL_def EVAL2_smult)
-
-lemma EVAL_monom_n: "!!a::'a::domain. EVAL a (monom b n) = b * a ^ n"
- by (simp add: EVAL_def EVAL2_monom_n)
-
-
-(* Examples *)
-
-lemma "EVAL (x::'a::domain) (a*X^2 + b*X^1 + c*X^0) = a * x ^ 2 + b * x ^ 1 + c"
- by (simp del: power_Suc add: EVAL_homo EVAL_monom EVAL_monom_n)
-
-lemma
- "EVAL (y::'a::domain)
- (EVAL (monom x 0) (monom 1 1 + monom (a*X^2 + b*X^1 + c*X^0) 0)) =
- x ^ 1 + (a * y ^ 2 + b * y ^ 1 + c)"
- by (simp del: add: EVAL_homo EVAL_monom EVAL_monom_n EVAL_const)
-
-end