simplify proof of coeff_mult_degree_sum
authorhuffman
Tue, 13 Jan 2009 07:40:05 -0800
changeset 29471 6a46a13ce1f9
parent 29470 1851088a1f87
child 29472 a63a2e46cec9
simplify proof of coeff_mult_degree_sum
src/HOL/Polynomial.thy
--- a/src/HOL/Polynomial.thy	Tue Jan 13 06:57:08 2009 -0800
+++ b/src/HOL/Polynomial.thy	Tue Jan 13 07:40:05 2009 -0800
@@ -662,17 +662,7 @@
 lemma coeff_mult_degree_sum:
   "coeff (p * q) (degree p + degree q) =
    coeff p (degree p) * coeff q (degree q)"
- apply (simp add: coeff_mult)
- apply (subst setsum_diff1' [where a="degree p"])
-   apply simp
-  apply simp
- apply (subst setsum_0' [rule_format])
-  apply clarsimp
-  apply (subgoal_tac "degree p < a \<or> degree q < degree p + degree q - a")
-   apply (force simp add: coeff_eq_0)
-  apply arith
- apply simp
-done
+  by (induct p, simp, simp add: coeff_eq_0)
 
 instance poly :: (idom) idom
 proof