# HG changeset patch # User wenzelm # Date 1231881904 -3600 # Node ID b834f95c2532d0c11170ff386bd63cdbdfc6d19d # Parent 68e88293708f1cfe25f3a457eb4bd901c5fa100e# Parent c9bb4e06d1730f66ec414af7a91947b60f8509df merged diff -r c9bb4e06d173 -r b834f95c2532 src/HOL/Deriv.thy --- a/src/HOL/Deriv.thy Tue Jan 13 22:20:49 2009 +0100 +++ b/src/HOL/Deriv.thy Tue Jan 13 22:25:04 2009 +0100 @@ -9,7 +9,7 @@ header{* Differentiation *} theory Deriv -imports Lim Univ_Poly +imports Lim Polynomial begin text{*Standard Definitions*} @@ -1412,34 +1412,71 @@ lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E" by auto + subsection {* Derivatives of univariate polynomials *} - - -primrec pderiv_aux :: "nat => real list => real list" where - pderiv_aux_Nil: "pderiv_aux n [] = []" -| pderiv_aux_Cons: "pderiv_aux n (h#t) = - (real n * h)#(pderiv_aux (Suc n) t)" - definition - pderiv :: "real list => real list" where - "pderiv p = (if p = [] then [] else pderiv_aux 1 (tl p))" + pderiv :: "'a::real_normed_field poly \ 'a poly" where + "pderiv = poly_rec 0 (\a p p'. p + pCons 0 p')" + +lemma pderiv_0 [simp]: "pderiv 0 = 0" + unfolding pderiv_def by (simp add: poly_rec_0) +lemma pderiv_pCons: "pderiv (pCons a p) = p + pCons 0 (pderiv p)" + unfolding pderiv_def by (simp add: poly_rec_pCons) + +lemma coeff_pderiv: "coeff (pderiv p) n = of_nat (Suc n) * coeff p (Suc n)" + apply (induct p arbitrary: n, simp) + apply (simp add: pderiv_pCons coeff_pCons ring_simps split: nat.split) + done -text{*The derivative*} +lemma pderiv_eq_0_iff: "pderiv p = 0 \ degree p = 0" + apply (rule iffI) + apply (cases p, simp) + apply (simp add: expand_poly_eq coeff_pderiv del: of_nat_Suc) + apply (simp add: expand_poly_eq coeff_pderiv coeff_eq_0) + done -lemma pderiv_Nil: "pderiv [] = []" +lemma degree_pderiv: "degree (pderiv p) = degree p - 1" + apply (rule order_antisym [OF degree_le]) + apply (simp add: coeff_pderiv coeff_eq_0) + apply (cases "degree p", simp) + apply (rule le_degree) + apply (simp add: coeff_pderiv del: of_nat_Suc) + apply (rule subst, assumption) + apply (rule leading_coeff_neq_0, clarsimp) + done -apply (simp add: pderiv_def) -done -declare pderiv_Nil [simp] +lemma pderiv_singleton [simp]: "pderiv [:a:] = 0" +by (simp add: pderiv_pCons) + +lemma pderiv_add: "pderiv (p + q) = pderiv p + pderiv q" +by (rule poly_ext, simp add: coeff_pderiv ring_simps) + +lemma pderiv_minus: "pderiv (- p) = - pderiv p" +by (rule poly_ext, simp add: coeff_pderiv) + +lemma pderiv_diff: "pderiv (p - q) = pderiv p - pderiv q" +by (rule poly_ext, simp add: coeff_pderiv ring_simps) + +lemma pderiv_smult: "pderiv (smult a p) = smult a (pderiv p)" +by (rule poly_ext, simp add: coeff_pderiv ring_simps) -lemma pderiv_singleton: "pderiv [c] = []" -by (simp add: pderiv_def) -declare pderiv_singleton [simp] +lemma pderiv_mult: "pderiv (p * q) = p * pderiv q + q * pderiv p" +apply (induct p) +apply simp +apply (simp add: pderiv_add pderiv_smult pderiv_pCons ring_simps) +done -lemma pderiv_Cons: "pderiv (h#t) = pderiv_aux 1 t" -by (simp add: pderiv_def) +lemma pderiv_power_Suc: + "pderiv (p ^ Suc n) = smult (of_nat (Suc n)) (p ^ n) * pderiv p" +apply (induct n) +apply simp +apply (subst power_Suc) +apply (subst pderiv_mult) +apply (erule ssubst) +apply (simp add: smult_add_left ring_simps) +done lemma DERIV_cmult2: "DERIV f x :> D ==> DERIV (%x. (f x) * c :: real) x :> D * c" by (simp add: DERIV_cmult mult_commute [of _ c]) @@ -1448,33 +1485,18 @@ by (rule lemma_DERIV_subst, rule DERIV_pow, simp) declare DERIV_pow2 [simp] DERIV_pow [simp] -lemma lemma_DERIV_poly1: "\n. DERIV (%x. (x ^ (Suc n) * poly p x)) x :> - x ^ n * poly (pderiv_aux (Suc n) p) x " -apply (induct "p") -apply (auto intro!: DERIV_add DERIV_cmult2 - simp add: pderiv_def right_distrib real_mult_assoc [symmetric] - simp del: realpow_Suc) -apply (subst mult_commute) -apply (simp del: realpow_Suc) -apply (simp add: mult_commute realpow_Suc [symmetric] del: realpow_Suc) -done - -lemma lemma_DERIV_poly: "DERIV (%x. (x ^ (Suc n) * poly p x)) x :> - x ^ n * poly (pderiv_aux (Suc n) p) x " -by (simp add: lemma_DERIV_poly1 del: realpow_Suc) - -lemma DERIV_add_const: "DERIV f x :> D ==> DERIV (%x. a + f x :: real) x :> D" +lemma DERIV_add_const: "DERIV f x :> D ==> DERIV (%x. a + f x :: 'a::real_normed_field) x :> D" by (rule lemma_DERIV_subst, rule DERIV_add, auto) lemma poly_DERIV[simp]: "DERIV (%x. poly p x) x :> poly (pderiv p) x" -apply (induct "p") -apply (auto simp add: pderiv_Cons) -apply (rule DERIV_add_const) +apply (induct p) +apply simp +apply (simp add: pderiv_pCons) apply (rule lemma_DERIV_subst) -apply (rule lemma_DERIV_poly [where n=0, simplified], simp) +apply (rule DERIV_add DERIV_mult DERIV_const DERIV_ident | assumption)+ +apply simp done - text{* Consequences of the derivative theorem above*} lemma poly_differentiable[simp]: "(%x. poly p x) differentiable (x::real)" @@ -1493,11 +1515,9 @@ lemma poly_IVT_neg: "[| (a::real) < b; 0 < poly p a; poly p b < 0 |] ==> \x. a < x & x < b & (poly p x = 0)" -apply (insert poly_IVT_pos [where p = "-- p" ]) -apply (simp add: poly_minus neg_less_0_iff_less) -done +by (insert poly_IVT_pos [where p = "- p" ]) simp -lemma poly_MVT: "a < b ==> +lemma poly_MVT: "(a::real) < b ==> \x. a < x & x < b & (poly p b - poly p a = (b - a) * poly (pderiv p) x)" apply (drule_tac f = "poly p" in MVT, auto) apply (rule_tac x = z in exI) @@ -1506,136 +1526,7 @@ text{*Lemmas for Derivatives*} -lemma lemma_poly_pderiv_aux_add: "\p2 n. poly (pderiv_aux n (p1 +++ p2)) x = - poly (pderiv_aux n p1 +++ pderiv_aux n p2) x" -apply (induct "p1", simp, clarify) -apply (case_tac "p2") -apply (auto simp add: right_distrib) -done - -lemma poly_pderiv_aux_add: "poly (pderiv_aux n (p1 +++ p2)) x = - poly (pderiv_aux n p1 +++ pderiv_aux n p2) x" -apply (simp add: lemma_poly_pderiv_aux_add) -done - -lemma lemma_poly_pderiv_aux_cmult: "\n. poly (pderiv_aux n (c %* p)) x = poly (c %* pderiv_aux n p) x" -apply (induct "p") -apply (auto simp add: poly_cmult mult_ac) -done - -lemma poly_pderiv_aux_cmult: "poly (pderiv_aux n (c %* p)) x = poly (c %* pderiv_aux n p) x" -by (simp add: lemma_poly_pderiv_aux_cmult) - -lemma poly_pderiv_aux_minus: - "poly (pderiv_aux n (-- p)) x = poly (-- pderiv_aux n p) x" -apply (simp add: poly_minus_def poly_pderiv_aux_cmult) -done - -lemma lemma_poly_pderiv_aux_mult1: "\n. poly (pderiv_aux (Suc n) p) x = poly ((pderiv_aux n p) +++ p) x" -apply (induct "p") -apply (auto simp add: real_of_nat_Suc left_distrib) -done - -lemma lemma_poly_pderiv_aux_mult: "poly (pderiv_aux (Suc n) p) x = poly ((pderiv_aux n p) +++ p) x" -by (simp add: lemma_poly_pderiv_aux_mult1) - -lemma lemma_poly_pderiv_add: "\q. poly (pderiv (p +++ q)) x = poly (pderiv p +++ pderiv q) x" -apply (induct "p", simp, clarify) -apply (case_tac "q") -apply (auto simp add: poly_pderiv_aux_add poly_add pderiv_def) -done - -lemma poly_pderiv_add: "poly (pderiv (p +++ q)) x = poly (pderiv p +++ pderiv q) x" -by (simp add: lemma_poly_pderiv_add) - -lemma poly_pderiv_cmult: "poly (pderiv (c %* p)) x = poly (c %* (pderiv p)) x" -apply (induct "p") -apply (auto simp add: poly_pderiv_aux_cmult poly_cmult pderiv_def) -done - -lemma poly_pderiv_minus: "poly (pderiv (--p)) x = poly (--(pderiv p)) x" -by (simp add: poly_minus_def poly_pderiv_cmult) - -lemma lemma_poly_mult_pderiv: - "poly (pderiv (h#t)) x = poly ((0 # (pderiv t)) +++ t) x" -apply (simp add: pderiv_def) -apply (induct "t") -apply (auto simp add: poly_add lemma_poly_pderiv_aux_mult) -done - -lemma poly_pderiv_mult: "\q. poly (pderiv (p *** q)) x = - poly (p *** (pderiv q) +++ q *** (pderiv p)) x" -apply (induct "p") -apply (auto simp add: poly_add poly_cmult poly_pderiv_cmult poly_pderiv_add poly_mult) -apply (rule lemma_poly_mult_pderiv [THEN ssubst]) -apply (rule lemma_poly_mult_pderiv [THEN ssubst]) -apply (rule poly_add [THEN ssubst]) -apply (rule poly_add [THEN ssubst]) -apply (simp (no_asm_simp) add: poly_mult right_distrib add_ac mult_ac) -done - -lemma poly_pderiv_exp: "poly (pderiv (p %^ (Suc n))) x = - poly ((real (Suc n)) %* (p %^ n) *** pderiv p) x" -apply (induct "n") -apply (auto simp add: poly_add poly_pderiv_cmult poly_cmult poly_pderiv_mult - real_of_nat_zero poly_mult real_of_nat_Suc - right_distrib left_distrib mult_ac) -done - -lemma poly_pderiv_exp_prime: "poly (pderiv ([-a, 1] %^ (Suc n))) x = - poly (real (Suc n) %* ([-a, 1] %^ n)) x" -apply (simp add: poly_pderiv_exp poly_mult del: pexp_Suc) -apply (simp add: poly_cmult pderiv_def) -done - - -lemma real_mult_zero_disj_iff[simp]: "(x * y = 0) = (x = (0::real) | y = 0)" -by simp - -lemma pderiv_aux_iszero [rule_format, simp]: - "\n. list_all (%c. c = 0) (pderiv_aux (Suc n) p) = list_all (%c. c = 0) p" -by (induct "p", auto) - -lemma pderiv_aux_iszero_num: "(number_of n :: nat) \ 0 - ==> (list_all (%c. c = 0) (pderiv_aux (number_of n) p) = - list_all (%c. c = 0) p)" -unfolding neq0_conv -apply (rule_tac n1 = "number_of n" and m1 = 0 in less_imp_Suc_add [THEN exE], force) -apply (rule_tac n1 = "0 + x" in pderiv_aux_iszero [THEN subst]) -apply (simp (no_asm_simp) del: pderiv_aux_iszero) -done - -instance real:: idom_char_0 -apply (intro_classes) -done - -instance real:: recpower_idom_char_0 -apply (intro_classes) -done - -lemma pderiv_iszero [rule_format]: - "poly (pderiv p) = poly [] --> (\h. poly p = poly [h])" -apply (simp add: poly_zero) -apply (induct "p", force) -apply (simp add: pderiv_Cons pderiv_aux_iszero_num del: poly_Cons) -apply (auto simp add: poly_zero [symmetric]) -done - -lemma pderiv_zero_obj: "poly p = poly [] --> (poly (pderiv p) = poly [])" -apply (simp add: poly_zero) -apply (induct "p", force) -apply (simp add: pderiv_Cons pderiv_aux_iszero_num del: poly_Cons) -done - -lemma pderiv_zero: "poly p = poly [] ==> (poly (pderiv p) = poly [])" -by (blast elim: pderiv_zero_obj [THEN impE]) -declare pderiv_zero [simp] - -lemma poly_pderiv_welldef: "poly p = poly q ==> (poly (pderiv p) = poly (pderiv q))" -apply (cut_tac p = "p +++ --q" in pderiv_zero_obj) -apply (simp add: fun_eq poly_add poly_minus poly_pderiv_add poly_pderiv_minus del: pderiv_zero) -done - +(* FIXME lemma lemma_order_pderiv [rule_format]: "\p q a. 0 < n & poly (pderiv p) \ poly [] & @@ -1756,7 +1647,7 @@ apply (simp (no_asm) add: rsquarefree_def order_root del: pmult_Cons) apply (simp add: poly_entire del: pmult_Cons) done - +*) subsection {* Theorems about Limits *} diff -r c9bb4e06d173 -r b834f95c2532 src/HOL/Fundamental_Theorem_Algebra.thy --- a/src/HOL/Fundamental_Theorem_Algebra.thy Tue Jan 13 22:20:49 2009 +0100 +++ b/src/HOL/Fundamental_Theorem_Algebra.thy Tue Jan 13 22:25:04 2009 +0100 @@ -6,9 +6,6 @@ imports Polynomial Dense_Linear_Order Complex begin -hide (open) const Univ_Poly.poly -hide (open) const Univ_Poly.degree - subsection {* Square root of complex numbers *} definition csqrt :: "complex \ complex" where "csqrt z = (if Im z = 0 then @@ -137,7 +134,7 @@ apply (simp add: offset_poly_eq_0_iff) done -definition +definition [code del]: "plength p = (if p = 0 then 0 else Suc (degree p))" lemma plength_eq_0_iff [simp]: "plength p = 0 \ p = 0" @@ -827,7 +824,7 @@ by simp let ?r = "smult (inverse ?a0) q" have lgqr: "plength q = plength ?r" - using a00 unfolding plength_def Polynomial.degree_def + using a00 unfolding plength_def degree_def by (simp add: expand_poly_eq) {assume h: "\x y. poly ?r x = poly ?r y" {fix x y @@ -1064,7 +1061,7 @@ fixes p :: "'a::{idom,ring_char_0} poly" shows "poly p = poly 0 \ p = 0" apply (cases "p = 0", simp_all) -apply (drule Polynomial.poly_roots_finite) +apply (drule poly_roots_finite) apply (auto simp add: UNIV_char_0_infinite) done @@ -1118,8 +1115,7 @@ from k oop [of a] have "q ^ n = p * ?w" apply - apply (subst r, subst s, subst kpn) - apply (subst power_mult_distrib) - apply (simp add: mult_smult_left mult_smult_right smult_smult) + apply (subst power_mult_distrib, simp) apply (subst power_add [symmetric], simp) done hence ?ths unfolding dvd_def by blast} @@ -1147,7 +1143,7 @@ have "s dvd (r ^ (degree s))" by blast then obtain u where u: "r ^ (degree s) = s * u" .. hence u': "\x. poly s x * poly u x = poly r x ^ degree s" - by (simp only: Polynomial.poly_mult[symmetric] poly_power[symmetric]) + by (simp only: poly_mult[symmetric] poly_power[symmetric]) let ?w = "(u * ([:-a,1:] ^ (n - ?op))) * (r ^ (n - degree s))" from oop[of a] dsn have "q ^ n = p * ?w" apply - @@ -1207,7 +1203,7 @@ then obtain u where u: "q ^ (Suc n) = p * u" .. {fix x assume h: "poly p x = 0" "poly q x \ 0" hence "poly (q ^ (Suc n)) x \ 0" by simp - hence False using u h(1) by (simp only: poly_mult poly_exp) simp}} + hence False using u h(1) by (simp only: poly_mult) simp}} with n nullstellensatz_lemma[of p q "degree p"] dp have ?thesis by auto} ultimately have ?thesis by blast} @@ -1258,7 +1254,6 @@ lemma resolve_eq_raw: "poly 0 x \ 0" "poly [:c:] x \ (c::complex)" by auto lemma resolve_eq_then: "(P \ (Q \ Q1)) \ (\P \ (Q \ Q2)) \ Q \ P \ Q1 \ \P\ Q2" apply (atomize (full)) by blast -lemma expand_ex_beta_conv: "list_ex P [c] \ P c" by simp lemma poly_divides_pad_rule: fixes p q :: "complex poly" @@ -1382,8 +1377,6 @@ lemma elim_neg_conv: "- z \ (-1) * (z::complex)" by simp lemma eqT_intr: "PROP P \ (True \ PROP P )" "PROP P \ True" by blast+ lemma negate_negate_rule: "Trueprop P \ \ P \ False" by (atomize (full), auto) -lemma last_simps: "last [x] = x" "last (x#y#ys) = last (y#ys)" by simp_all -lemma length_simps: "length [] = 0" "length (x#y#xs) = length xs + 2" "length [x] = 1" by simp_all lemma complex_entire: "(z::complex) \ 0 \ w \ 0 \ z*w \ 0" by simp lemma resolve_eq_ne: "(P \ True) \ (\P \ False)" "(P \ False) \ (\P \ True)" diff -r c9bb4e06d173 -r b834f95c2532 src/HOL/Integration.thy --- a/src/HOL/Integration.thy Tue Jan 13 22:20:49 2009 +0100 +++ b/src/HOL/Integration.thy Tue Jan 13 22:25:04 2009 +0100 @@ -6,7 +6,7 @@ header{*Theory of Integration*} theory Integration -imports Deriv +imports Deriv ATP_Linkup begin text{*We follow John Harrison in formalizing the Gauge integral.*} diff -r c9bb4e06d173 -r b834f95c2532 src/HOL/Polynomial.thy --- a/src/HOL/Polynomial.thy Tue Jan 13 22:20:49 2009 +0100 +++ b/src/HOL/Polynomial.thy Tue Jan 13 22:25:04 2009 +0100 @@ -208,7 +208,7 @@ function poly_rec :: "'b \ ('a::zero \ 'a poly \ 'b \ 'b) \ 'a poly \ 'b" where - poly_rec_pCons_eq_if [simp del]: + poly_rec_pCons_eq_if [simp del, code del]: "poly_rec z f (pCons a p) = f a p (if p = 0 then z else poly_rec z f p)" by (case_tac x, rename_tac q, case_tac q, auto) @@ -413,7 +413,7 @@ lemma degree_smult_le: "degree (smult a p) \ degree p" by (rule degree_le, simp add: coeff_eq_0) -lemma smult_smult: "smult a (smult b p) = smult (a * b) p" +lemma smult_smult [simp]: "smult a (smult b p) = smult (a * b) p" by (rule poly_ext, simp add: mult_assoc) lemma smult_0_right [simp]: "smult a 0 = 0" @@ -449,6 +449,10 @@ "smult (a - b::'a::comm_ring) p = smult a p - smult b p" by (rule poly_ext, simp add: ring_simps) +lemmas smult_distribs = + smult_add_left smult_add_right + smult_diff_left smult_diff_right + lemma smult_pCons [simp]: "smult a (pCons b p) = pCons (a * b) (smult a p)" by (rule poly_ext, simp add: coeff_pCons split: nat.split) @@ -459,57 +463,7 @@ subsection {* Multiplication of polynomials *} -lemma Poly_mult_lemma: - fixes f g :: "nat \ 'a::comm_semiring_0" and m n :: nat - assumes "\i>m. f i = 0" - assumes "\j>n. g j = 0" - shows "\k>m+n. (\i\k. f i * g (k-i)) = 0" -proof (clarify) - fix k :: nat - assume "m + n < k" - show "(\i\k. f i * g (k - i)) = 0" - proof (rule setsum_0' [rule_format]) - fix i :: nat - assume "i \ {..k}" hence "i \ k" by simp - with `m + n < k` have "m < i \ n < k - i" by arith - thus "f i * g (k - i) = 0" - using prems by auto - qed -qed - -lemma Poly_mult: - fixes f g :: "nat \ 'a::comm_semiring_0" - shows "\f \ Poly; g \ Poly\ \ (\n. \i\n. f i * g (n-i)) \ Poly" - unfolding Poly_def - by (safe, rule exI, rule Poly_mult_lemma) - -lemma poly_mult_assoc_lemma: - fixes k :: nat and f :: "nat \ nat \ nat \ 'a::comm_monoid_add" - shows "(\j\k. \i\j. f i (j - i) (n - j)) = - (\j\k. \i\k - j. f j i (n - j - i))" -proof (induct k) - case 0 show ?case by simp -next - case (Suc k) thus ?case - by (simp add: Suc_diff_le setsum_addf add_assoc - cong: strong_setsum_cong) -qed - -lemma poly_mult_commute_lemma: - fixes n :: nat and f :: "nat \ nat \ 'a::comm_monoid_add" - shows "(\i\n. f i (n - i)) = (\i\n. f (n - i) i)" -proof (rule setsum_reindex_cong) - show "inj_on (\i. n - i) {..n}" - by (rule inj_onI) simp - show "{..n} = (\i. n - i) ` {..n}" - by (auto, rule_tac x="n - x" in image_eqI, simp_all) -next - fix i assume "i \ {..n}" - hence "n - (n - i) = i" by simp - thus "f (n - i) i = f (n - i) (n - (n - i))" by simp -qed - -text {* TODO: move to appropriate theory *} +text {* TODO: move to SetInterval.thy *} lemma setsum_atMost_Suc_shift: fixes f :: "nat \ 'a::comm_monoid_add" shows "(\i\Suc n. f i) = f 0 + (\i\n. f (Suc i))" @@ -533,70 +487,70 @@ begin definition - times_poly_def: - "p * q = Abs_poly (\n. \i\n. coeff p i * coeff q (n-i))" + times_poly_def [code del]: + "p * q = poly_rec 0 (\a p pq. smult a q + pCons 0 pq) p" + +lemma mult_poly_0_left: "(0::'a poly) * q = 0" + unfolding times_poly_def by (simp add: poly_rec_0) + +lemma mult_pCons_left [simp]: + "pCons a p * q = smult a q + pCons 0 (p * q)" + unfolding times_poly_def by (simp add: poly_rec_pCons) + +lemma mult_poly_0_right: "p * (0::'a poly) = 0" + by (induct p, simp add: mult_poly_0_left, simp) -lemma coeff_mult: - "coeff (p * q) n = (\i\n. coeff p i * coeff q (n-i))" - unfolding times_poly_def - by (simp add: Abs_poly_inverse coeff Poly_mult) +lemma mult_pCons_right [simp]: + "p * pCons a q = smult a p + pCons 0 (p * q)" + by (induct p, simp add: mult_poly_0_left, simp add: ring_simps) + +lemmas mult_poly_0 = mult_poly_0_left mult_poly_0_right + +lemma mult_smult_left [simp]: "smult a p * q = smult a (p * q)" + by (induct p, simp add: mult_poly_0, simp add: smult_add_right) + +lemma mult_smult_right [simp]: "p * smult a q = smult a (p * q)" + by (induct q, simp add: mult_poly_0, simp add: smult_add_right) + +lemma mult_poly_add_left: + fixes p q r :: "'a poly" + shows "(p + q) * r = p * r + q * r" + by (induct r, simp add: mult_poly_0, + simp add: smult_distribs group_simps) instance proof fix p q r :: "'a poly" show 0: "0 * p = 0" - by (simp add: expand_poly_eq coeff_mult) + by (rule mult_poly_0_left) show "p * 0 = 0" - by (simp add: expand_poly_eq coeff_mult) + by (rule mult_poly_0_right) show "(p + q) * r = p * r + q * r" - by (simp add: expand_poly_eq coeff_mult left_distrib setsum_addf) + by (rule mult_poly_add_left) show "(p * q) * r = p * (q * r)" - proof (rule poly_ext) - fix n :: nat - have "(\j\n. \i\j. coeff p i * coeff q (j - i) * coeff r (n - j)) = - (\j\n. \i\n - j. coeff p j * coeff q i * coeff r (n - j - i))" - by (rule poly_mult_assoc_lemma) - thus "coeff ((p * q) * r) n = coeff (p * (q * r)) n" - by (simp add: coeff_mult setsum_right_distrib - setsum_left_distrib mult_assoc) - qed + by (induct p, simp add: mult_poly_0, simp add: mult_poly_add_left) show "p * q = q * p" - proof (rule poly_ext) - fix n :: nat - have "(\i\n. coeff p i * coeff q (n - i)) = - (\i\n. coeff p (n - i) * coeff q i)" - by (rule poly_mult_commute_lemma) - thus "coeff (p * q) n = coeff (q * p) n" - by (simp add: coeff_mult mult_commute) - qed + by (induct p, simp add: mult_poly_0, simp) qed end -lemma degree_mult_le: "degree (p * q) \ degree p + degree q" -apply (rule degree_le, simp add: coeff_mult) -apply (rule Poly_mult_lemma) -apply (simp_all add: coeff_eq_0) -done +lemma coeff_mult: + "coeff (p * q) n = (\i\n. coeff p i * coeff q (n-i))" +proof (induct p arbitrary: n) + case 0 show ?case by simp +next + case (pCons a p n) thus ?case + by (cases n, simp, simp add: setsum_atMost_Suc_shift + del: setsum_atMost_Suc) +qed -lemma mult_pCons_left [simp]: - "pCons a p * q = smult a q + pCons 0 (p * q)" -apply (rule poly_ext) -apply (case_tac n) -apply (simp add: coeff_mult) -apply (simp add: coeff_mult setsum_atMost_Suc_shift - del: setsum_atMost_Suc) +lemma degree_mult_le: "degree (p * q) \ degree p + degree q" +apply (rule degree_le) +apply (induct p) +apply simp +apply (simp add: coeff_eq_0 coeff_pCons split: nat.split) done -lemma mult_pCons_right [simp]: - "p * pCons a q = smult a p + pCons 0 (p * q)" - using mult_pCons_left [of a q p] by (simp add: mult_commute) - -lemma mult_smult_left: "smult a p * q = smult a (p * q)" - by (induct p, simp, simp add: smult_add_right smult_smult) - -lemma mult_smult_right: "p * smult a q = smult a (p * q)" - using mult_smult_left [of a q p] by (simp add: mult_commute) - lemma mult_monom: "monom a m * monom b n = monom (a * b) (m + n)" by (induct m, simp add: monom_0 smult_monom, simp add: monom_Suc) @@ -662,17 +616,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 @@ -705,6 +649,7 @@ definition divmod_poly_rel :: "'a::field poly \ 'a poly \ 'a poly \ 'a poly \ bool" where + [code del]: "divmod_poly_rel x y q r \ x = q * y + r \ (if y = 0 then q = 0 else r = 0 \ degree r < degree y)"