# HG changeset patch # User huffman # Date 1231861205 28800 # Node ID 6a46a13ce1f9cb4e1bf8c65236fedb801f639d56 # Parent 1851088a1f87c5b8392861debe7c78ab38276419 simplify proof of coeff_mult_degree_sum diff -r 1851088a1f87 -r 6a46a13ce1f9 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 \ 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