Up to index of Isabelle/HOL/HOL-Algebra
theory UnivPoly2(* Title: Univariate Polynomials Id: $Id: UnivPoly2.thy,v 1.7 2005/07/01 12:05:41 berghofe Exp $ Author: Clemens Ballarin, started 9 December 1996 Copyright: Clemens Ballarin *) header {* Univariate Polynomials *} theory UnivPoly2 imports "../abstract/Abstract" begin (* already proved in Finite_Set.thy lemma setsum_cong: "[| A = B; !!i. i : B ==> f i = g i |] ==> setsum f A = setsum g B" proof - assume prems: "A = B" "!!i. i : B ==> f i = g i" show ?thesis proof (cases "finite B") case True then have "!!A. [| A = B; !!i. i : B ==> f i = g i |] ==> setsum f A = setsum g B" proof induct case empty thus ?case by simp next case insert thus ?case by simp qed with prems show ?thesis by simp next case False with prems show ?thesis by (simp add: setsum_def) qed qed *) (* With this variant of setsum_cong, assumptions like i:{m..n} get simplified (to m <= i & i <= n). *) declare strong_setsum_cong [cong] section {* Definition of type up *} constdefs bound :: "[nat, nat => 'a::zero] => bool" "bound n f == (ALL i. n < i --> f i = 0)" lemma boundI [intro!]: "[| !! m. n < m ==> f m = 0 |] ==> bound n f" proof (unfold bound_def) qed fast lemma boundE [elim?]: "[| bound n f; (!! m. n < m ==> f m = 0) ==> P |] ==> P" proof (unfold bound_def) qed fast lemma boundD [dest]: "[| bound n f; n < m |] ==> f m = 0" proof (unfold bound_def) qed fast lemma bound_below: assumes bound: "bound m f" and nonzero: "f n ~= 0" shows "n <= m" proof (rule classical) assume "~ ?thesis" then have "m < n" by arith with bound have "f n = 0" .. with nonzero show ?thesis by contradiction qed typedef (UP) ('a) up = "{f :: nat => 'a::zero. EX n. bound n f}" by (rule+) (* Question: what does trace_rule show??? *) section {* Constants *} consts coeff :: "['a up, nat] => ('a::zero)" monom :: "['a::zero, nat] => 'a up" ("(3_*X^/_)" [71, 71] 70) "*s" :: "['a::{zero, times}, 'a up] => 'a up" (infixl 70) defs coeff_def: "coeff p n == Rep_UP p n" monom_def: "monom a n == Abs_UP (%i. if i=n then a else 0)" smult_def: "a *s p == Abs_UP (%i. a * Rep_UP p i)" lemma coeff_bound_ex: "EX n. bound n (coeff p)" proof - have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP) then obtain n where "bound n (coeff p)" by (unfold UP_def) fast then show ?thesis .. qed lemma bound_coeff_obtain: assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P" proof - have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP) then obtain n where "bound n (coeff p)" by (unfold UP_def) fast with prem show P . qed text {* Ring operations *} instance up :: (zero) zero .. instance up :: (one) one .. instance up :: (plus) plus .. instance up :: (minus) minus .. instance up :: (times) times .. instance up :: (inverse) inverse .. instance up :: (power) power .. defs up_add_def: "p + q == Abs_UP (%n. Rep_UP p n + Rep_UP q n)" up_mult_def: "p * q == Abs_UP (%n::nat. setsum (%i. Rep_UP p i * Rep_UP q (n-i)) {..n})" up_zero_def: "0 == monom 0 0" up_one_def: "1 == monom 1 0" up_uminus_def:"- p == (- 1) *s p" (* easier to use than "Abs_UP (%i. - Rep_UP p i)" *) (* note: - 1 is different from -1; latter is of class number *) up_minus_def: "(a::'a::{plus, minus} up) - b == a + (-b)" up_inverse_def: "inverse (a::'a::{zero, one, times, inverse} up) == (if a dvd 1 then THE x. a*x = 1 else 0)" up_divide_def: "(a::'a::{times, inverse} up) / b == a * inverse b" up_power_def: "(a::'a::{one, times, power} up) ^ n == nat_rec 1 (%u b. b * a) n" subsection {* Effect of operations on coefficients *} lemma coeff_monom [simp]: "coeff (monom a m) n = (if m=n then a else 0)" proof - have "(%n. if n = m then a else 0) : UP" using UP_def by force from this show ?thesis by (simp add: coeff_def monom_def Abs_UP_inverse Rep_UP) qed lemma coeff_zero [simp]: "coeff 0 n = 0" proof (unfold up_zero_def) qed simp lemma coeff_one [simp]: "coeff 1 n = (if n=0 then 1 else 0)" proof (unfold up_one_def) qed simp (* term order lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n" proof - have "!!f. f : UP ==> (%n. a * f n) : UP" by (unfold UP_def) (force simp add: ring_simps) *) (* this force step is slow *) (* then show ?thesis apply (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP) qed *) lemma coeff_smult [simp]: "coeff (a *s p) n = (a::'a::ring) * coeff p n" proof - have "Rep_UP p : UP ==> (%n. a * Rep_UP p n) : UP" by (unfold UP_def) (force simp add: ring_simps) (* this force step is slow *) then show ?thesis by (simp add: coeff_def smult_def Abs_UP_inverse Rep_UP) qed lemma coeff_add [simp]: "coeff (p+q) n = (coeff p n + coeff q n::'a::ring)" proof - { fix f g assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP" have "(%i. f i + g i) : UP" proof - from fup obtain n where boundn: "bound n f" by (unfold UP_def) fast from gup obtain m where boundm: "bound m g" by (unfold UP_def) fast have "bound (max n m) (%i. (f i + g i))" proof fix i assume "max n m < i" with boundn and boundm show "f i + g i = 0" by (fastsimp simp add: ring_simps) qed then show "(%i. (f i + g i)) : UP" by (unfold UP_def) fast qed } then show ?thesis by (simp add: coeff_def up_add_def Abs_UP_inverse Rep_UP) qed lemma coeff_mult [simp]: "coeff (p * q) n = (setsum (%i. coeff p i * coeff q (n-i)) {..n}::'a::ring)" proof - { fix f g assume fup: "(f::nat=>'a::ring) : UP" and gup: "(g::nat=>'a::ring) : UP" have "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP" proof - from fup obtain n where "bound n f" by (unfold UP_def) fast from gup obtain m where "bound m g" by (unfold UP_def) fast have "bound (n + m) (%n. setsum (%i. f i * g (n-i)) {..n})" proof fix k assume bound: "n + m < k" { fix i have "f i * g (k-i) = 0" proof cases assume "n < i" show ?thesis by (auto! simp add: ring_simps) next assume "~ (n < i)" with bound have "m < k-i" by arith then show ?thesis by (auto! simp add: ring_simps) qed } then show "setsum (%i. f i * g (k-i)) {..k} = 0" by (simp add: ring_simps) qed then show "(%n. setsum (%i. f i * g (n-i)) {..n}) : UP" by (unfold UP_def) fast qed } then show ?thesis by (simp add: coeff_def up_mult_def Abs_UP_inverse Rep_UP) qed lemma coeff_uminus [simp]: "coeff (-p) n = (-coeff p n::'a::ring)" by (unfold up_uminus_def) (simp add: ring_simps) (* Other lemmas *) lemma up_eqI: assumes prem: "(!! n. coeff p n = coeff q n)" shows "p = q" proof - have "p = Abs_UP (%u. Rep_UP p u)" by (simp add: Rep_UP_inverse) also from prem have "... = Abs_UP (Rep_UP q)" by (simp only: coeff_def) also have "... = q" by (simp add: Rep_UP_inverse) finally show ?thesis . qed (* ML_setup {* Addsimprocs [ring_simproc] *} *) instance up :: (ring) ring proof fix p q r :: "'a::ring up" show "(p + q) + r = p + (q + r)" by (rule up_eqI) simp show "0 + p = p" by (rule up_eqI) simp show "(-p) + p = 0" by (rule up_eqI) simp show "p + q = q + p" by (rule up_eqI) simp show "(p * q) * r = p * (q * r)" proof (rule up_eqI) fix n { fix k and a b c :: "nat=>'a::ring" have "k <= n ==> setsum (%j. setsum (%i. a i * b (j-i)) {..j} * c (n-j)) {..k} = setsum (%j. a j * setsum (%i. b i * c (n-j-i)) {..k-j}) {..k}" (is "_ ==> ?eq k") proof (induct k) case 0 show ?case by simp next case (Suc k) then have "k <= n" by arith then have "?eq k" by (rule Suc) then show ?case by (simp add: Suc_diff_le natsum_ldistr) qed } then show "coeff ((p * q) * r) n = coeff (p * (q * r)) n" by simp qed show "1 * p = p" proof (rule up_eqI) fix n show "coeff (1 * p) n = coeff p n" proof (cases n) case 0 then show ?thesis by simp next case Suc then show ?thesis by (simp del: setsum_atMost_Suc add: natsum_Suc2) qed qed show "(p + q) * r = p * r + q * r" by (rule up_eqI) simp show "p * q = q * p" proof (rule up_eqI) fix n { fix k fix a b :: "nat=>'a::ring" have "k <= n ==> setsum (%i. a i * b (n-i)) {..k} = setsum (%i. a (k-i) * b (i+n-k)) {..k}" (is "_ ==> ?eq k") proof (induct k) case 0 show ?case by simp next case (Suc k) then show ?case by (subst natsum_Suc2) simp qed } then show "coeff (p * q) n = coeff (q * p) n" by simp qed show "p - q = p + (-q)" by (simp add: up_minus_def) show "inverse p = (if p dvd 1 then THE x. p*x = 1 else 0)" by (simp add: up_inverse_def) show "p / q = p * inverse q" by (simp add: up_divide_def) fix n show "p ^ n = nat_rec 1 (%u b. b * p) n" by (simp add: up_power_def) qed (* Further properties of monom *) lemma monom_zero [simp]: "monom 0 n = 0" by (simp add: monom_def up_zero_def) (* term order: application of coeff_mult goes wrong: rule not symmetric lemma monom_mult_is_smult: "monom (a::'a::ring) 0 * p = a *s p" proof (rule up_eqI) fix k show "coeff (monom a 0 * p) k = coeff (a *s p) k" proof (cases k) case 0 then show ?thesis by simp next case Suc then show ?thesis by simp qed qed *) ML_setup {* Delsimprocs [ring_simproc] *} lemma monom_mult_is_smult: "monom (a::'a::ring) 0 * p = a *s p" proof (rule up_eqI) fix k have "coeff (p * monom a 0) k = coeff (a *s p) k" proof (cases k) case 0 then show ?thesis by simp ring next case Suc then show ?thesis by (simp add: ring_simps) ring qed then show "coeff (monom a 0 * p) k = coeff (a *s p) k" by ring qed ML_setup {* Addsimprocs [ring_simproc] *} lemma monom_add [simp]: "monom (a + b) n = monom (a::'a::ring) n + monom b n" by (rule up_eqI) simp lemma monom_mult_smult: "monom (a * b) n = a *s monom (b::'a::ring) n" by (rule up_eqI) simp lemma monom_uminus [simp]: "monom (-a) n = - monom (a::'a::ring) n" by (rule up_eqI) simp lemma monom_one [simp]: "monom 1 0 = 1" by (simp add: up_one_def) lemma monom_inj: "(monom a n = monom b n) = (a = b)" proof assume "monom a n = monom b n" then have "coeff (monom a n) n = coeff (monom b n) n" by simp then show "a = b" by simp next assume "a = b" then show "monom a n = monom b n" by simp qed (* Properties of *s: Polynomials form a module *) lemma smult_l_distr: "(a + b::'a::ring) *s p = a *s p + b *s p" by (rule up_eqI) simp lemma smult_r_distr: "(a::'a::ring) *s (p + q) = a *s p + a *s q" by (rule up_eqI) simp lemma smult_assoc1: "(a * b::'a::ring) *s p = a *s (b *s p)" by (rule up_eqI) simp lemma smult_one [simp]: "(1::'a::ring) *s p = p" by (rule up_eqI) simp (* Polynomials form an algebra *) ML_setup {* Delsimprocs [ring_simproc] *} lemma smult_assoc2: "(a *s p) * q = (a::'a::ring) *s (p * q)" by (rule up_eqI) (simp add: natsum_rdistr m_assoc) (* Simproc fails. *) ML_setup {* Addsimprocs [ring_simproc] *} (* the following can be derived from the above ones, for generality reasons, it is therefore done *) lemma smult_l_null [simp]: "(0::'a::ring) *s p = 0" proof - fix a have "0 *s p = (0 *s p + a *s p) + - (a *s p)" by simp also have "... = (0 + a) *s p + - (a *s p)" by (simp only: smult_l_distr) also have "... = 0" by simp finally show ?thesis . qed lemma smult_r_null [simp]: "(a::'a::ring) *s 0 = 0"; proof - fix p have "a *s 0 = (a *s 0 + a *s p) + - (a *s p)" by simp also have "... = a *s (0 + p) + - (a *s p)" by (simp only: smult_r_distr) also have "... = 0" by simp finally show ?thesis . qed lemma smult_l_minus: "(-a::'a::ring) *s p = - (a *s p)" proof - have "(-a) *s p = (-a *s p + a *s p) + -(a *s p)" by simp also have "... = (-a + a) *s p + -(a *s p)" by (simp only: smult_l_distr) also have "... = -(a *s p)" by simp finally show ?thesis . qed lemma smult_r_minus: "(a::'a::ring) *s (-p) = - (a *s p)" proof - have "a *s (-p) = (a *s -p + a *s p) + -(a *s p)" by simp also have "... = a *s (-p + p) + -(a *s p)" by (simp only: smult_r_distr) also have "... = -(a *s p)" by simp finally show ?thesis . qed section {* The degree function *} constdefs deg :: "('a::zero) up => nat" "deg p == LEAST n. bound n (coeff p)" lemma deg_aboveI: "(!!m. n < m ==> coeff p m = 0) ==> deg p <= n" by (unfold deg_def) (fast intro: Least_le) lemma deg_aboveD: assumes prem: "deg p < m" shows "coeff p m = 0" proof - obtain n where "bound n (coeff p)" by (rule bound_coeff_obtain) then have "bound (deg p) (coeff p)" by (unfold deg_def, rule LeastI) then show "coeff p m = 0" by (rule boundD) qed lemma deg_belowI: assumes prem: "n ~= 0 ==> coeff p n ~= 0" shows "n <= deg p" (* logically, this is a slightly stronger version of deg_aboveD *) proof (cases "n=0") case True then show ?thesis by simp next case False then have "coeff p n ~= 0" by (rule prem) then have "~ deg p < n" by (fast dest: deg_aboveD) then show ?thesis by arith qed lemma lcoeff_nonzero_deg: assumes deg: "deg p ~= 0" shows "coeff p (deg p) ~= 0" proof - obtain m where "deg p <= m" and m_coeff: "coeff p m ~= 0" proof - have minus: "!!(n::nat) m. n ~= 0 ==> (n - Suc 0 < m) = (n <= m)" by arith (* make public?, why does proof not work with "1" *) from deg have "deg p - 1 < (LEAST n. bound n (coeff p))" by (unfold deg_def) arith then have "~ bound (deg p - 1) (coeff p)" by (rule not_less_Least) then have "EX m. deg p - 1 < m & coeff p m ~= 0" by (unfold bound_def) fast then have "EX m. deg p <= m & coeff p m ~= 0" by (simp add: deg minus) then show ?thesis by auto qed with deg_belowI have "deg p = m" by fastsimp with m_coeff show ?thesis by simp qed lemma lcoeff_nonzero_nonzero: assumes deg: "deg p = 0" and nonzero: "p ~= 0" shows "coeff p 0 ~= 0" proof - have "EX m. coeff p m ~= 0" proof (rule classical) assume "~ ?thesis" then have "p = 0" by (auto intro: up_eqI) with nonzero show ?thesis by contradiction qed then obtain m where coeff: "coeff p m ~= 0" .. then have "m <= deg p" by (rule deg_belowI) then have "m = 0" by (simp add: deg) with coeff show ?thesis by simp qed lemma lcoeff_nonzero: "p ~= 0 ==> coeff p (deg p) ~= 0" proof (cases "deg p = 0") case True assume "p ~= 0" with True show ?thesis by (simp add: lcoeff_nonzero_nonzero) next case False assume "p ~= 0" with False show ?thesis by (simp add: lcoeff_nonzero_deg) qed lemma deg_eqI: "[| !!m. n < m ==> coeff p m = 0; !!n. n ~= 0 ==> coeff p n ~= 0|] ==> deg p = n" by (fast intro: le_anti_sym deg_aboveI deg_belowI) (* Degree and polynomial operations *) lemma deg_add [simp]: "deg ((p::'a::ring up) + q) <= max (deg p) (deg q)" proof (cases "deg p <= deg q") case True show ?thesis by (rule deg_aboveI) (simp add: True deg_aboveD) next case False show ?thesis by (rule deg_aboveI) (simp add: False deg_aboveD) qed lemma deg_monom_ring: "deg (monom a n::'a::ring up) <= n" by (rule deg_aboveI) simp lemma deg_monom [simp]: "a ~= 0 ==> deg (monom a n::'a::ring up) = n" by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI) lemma deg_const [simp]: "deg (monom (a::'a::ring) 0) = 0" proof (rule le_anti_sym) show "deg (monom a 0) <= 0" by (rule deg_aboveI) simp next show "0 <= deg (monom a 0)" by (rule deg_belowI) simp qed lemma deg_zero [simp]: "deg 0 = 0" proof (rule le_anti_sym) show "deg 0 <= 0" by (rule deg_aboveI) simp next show "0 <= deg 0" by (rule deg_belowI) simp qed lemma deg_one [simp]: "deg 1 = 0" proof (rule le_anti_sym) show "deg 1 <= 0" by (rule deg_aboveI) simp next show "0 <= deg 1" by (rule deg_belowI) simp qed lemma uminus_monom: "!!a::'a::ring. (-a = 0) = (a = 0)" proof fix a::"'a::ring" assume "a = 0" then show "-a = 0" by simp next fix a::"'a::ring" assume "- a = 0" then have "-(- a) = 0" by simp then show "a = 0" by simp qed lemma deg_uminus [simp]: "deg (-p::('a::ring) up) = deg p" proof (rule le_anti_sym) show "deg (- p) <= deg p" by (simp add: deg_aboveI deg_aboveD) next show "deg p <= deg (- p)" by (simp add: deg_belowI lcoeff_nonzero_deg uminus_monom) qed lemma deg_smult_ring: "deg ((a::'a::ring) *s p) <= (if a = 0 then 0 else deg p)" proof (cases "a = 0") qed (simp add: deg_aboveI deg_aboveD)+ lemma deg_smult [simp]: "deg ((a::'a::domain) *s p) = (if a = 0 then 0 else deg p)" proof (rule le_anti_sym) show "deg (a *s p) <= (if a = 0 then 0 else deg p)" by (rule deg_smult_ring) next show "(if a = 0 then 0 else deg p) <= deg (a *s p)" proof (cases "a = 0") qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff) qed lemma deg_mult_ring: "deg (p * q::'a::ring up) <= deg p + deg q" proof (rule deg_aboveI) fix m assume boundm: "deg p + deg q < m" { fix k i assume boundk: "deg p + deg q < k" then have "coeff p i * coeff q (k - i) = 0" proof (cases "deg p < i") case True then show ?thesis by (simp add: deg_aboveD) next case False with boundk have "deg q < k - i" by arith then show ?thesis by (simp add: deg_aboveD) qed } (* This is similar to bound_mult_zero and deg_above_mult_zero in the old proofs. *) with boundm show "coeff (p * q) m = 0" by simp qed lemma deg_mult [simp]: "[| (p::'a::domain up) ~= 0; q ~= 0|] ==> deg (p * q) = deg p + deg q" proof (rule le_anti_sym) show "deg (p * q) <= deg p + deg q" by (rule deg_mult_ring) next let ?s = "(%i. coeff p i * coeff q (deg p + deg q - i))" assume nz: "p ~= 0" "q ~= 0" have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m - k" by arith show "deg p + deg q <= deg (p * q)" proof (rule deg_belowI, simp) have "setsum ?s {.. deg p + deg q} = setsum ?s ({..< deg p} Un {deg p .. deg p + deg q})" by (simp only: ivl_disj_un_one) also have "... = setsum ?s {deg p .. deg p + deg q}" by (simp add: setsum_Un_disjoint ivl_disj_int_one setsum_0 deg_aboveD less_add_diff) also have "... = setsum ?s ({deg p} Un {deg p <.. deg p + deg q})" by (simp only: ivl_disj_un_singleton) also have "... = coeff p (deg p) * coeff q (deg q)" by (simp add: setsum_Un_disjoint ivl_disj_int_singleton setsum_0 deg_aboveD) finally have "setsum ?s {.. deg p + deg q} = coeff p (deg p) * coeff q (deg q)" . with nz show "setsum ?s {.. deg p + deg q} ~= 0" by (simp add: integral_iff lcoeff_nonzero) qed qed lemma coeff_natsum: "((coeff (setsum p A) k)::'a::ring) = setsum (%i. coeff (p i) k) A" proof (cases "finite A") case True then show ?thesis by induct auto next case False then show ?thesis by (simp add: setsum_def) qed (* Instance of a more general result!!! *) (* lemma coeff_natsum: "((coeff (setsum p {..n::nat}) k)::'a::ring) = setsum (%i. coeff (p i) k) {..n}" by (induct n) auto *) lemma up_repr: "setsum (%i. monom (coeff p i) i) {..deg (p::'a::ring up)} = p" proof (rule up_eqI) let ?s = "(%i. monom (coeff p i) i)" fix k show "coeff (setsum ?s {..deg p}) k = coeff p k" proof (cases "k <= deg p") case True hence "coeff (setsum ?s {..deg p}) k = coeff (setsum ?s ({..k} Un {k<..deg p})) k" by (simp only: ivl_disj_un_one) also from True have "... = coeff (setsum ?s {..k}) k" by (simp add: setsum_Un_disjoint ivl_disj_int_one order_less_imp_not_eq2 setsum_0 coeff_natsum ) also have "... = coeff (setsum ?s ({..<k} Un {k})) k" by (simp only: ivl_disj_un_singleton) also have "... = coeff p k" by (simp add: setsum_Un_disjoint ivl_disj_int_singleton setsum_0 coeff_natsum deg_aboveD) finally show ?thesis . next case False hence "coeff (setsum ?s {..deg p}) k = coeff (setsum ?s ({..<deg p} Un {deg p})) k" by (simp only: ivl_disj_un_singleton) also from False have "... = coeff p k" by (simp add: setsum_Un_disjoint ivl_disj_int_singleton setsum_0 coeff_natsum deg_aboveD) finally show ?thesis . qed qed lemma up_repr_le: "deg (p::'a::ring up) <= n ==> setsum (%i. monom (coeff p i) i) {..n} = p" proof - let ?s = "(%i. monom (coeff p i) i)" assume "deg p <= n" then have "setsum ?s {..n} = setsum ?s ({..deg p} Un {deg p<..n})" by (simp only: ivl_disj_un_one) also have "... = setsum ?s {..deg p}" by (simp add: setsum_Un_disjoint ivl_disj_int_one setsum_0 deg_aboveD) also have "... = p" by (rule up_repr) finally show ?thesis . qed instance up :: ("domain") "domain" proof show "1 ~= (0::'a up)" proof (* notI is applied here *) assume "1 = (0::'a up)" hence "coeff 1 0 = (coeff 0 0::'a)" by simp hence "1 = (0::'a)" by simp with one_not_zero show "False" by contradiction qed next fix p q :: "'a::domain up" assume pq: "p * q = 0" show "p = 0 | q = 0" proof (rule classical) assume c: "~ (p = 0 | q = 0)" then have "deg p + deg q = deg (p * q)" by simp also from pq have "... = 0" by simp finally have "deg p + deg q = 0" . then have f1: "deg p = 0 & deg q = 0" by simp from f1 have "p = setsum (%i. (monom (coeff p i) i)) {..0}" by (simp only: up_repr_le) also have "... = monom (coeff p 0) 0" by simp finally have p: "p = monom (coeff p 0) 0" . from f1 have "q = setsum (%i. (monom (coeff q i) i)) {..0}" by (simp only: up_repr_le) also have "... = monom (coeff q 0) 0" by simp finally have q: "q = monom (coeff q 0) 0" . have "coeff p 0 * coeff q 0 = coeff (p * q) 0" by simp also from pq have "... = 0" by simp finally have "coeff p 0 * coeff q 0 = 0" . then have "coeff p 0 = 0 | coeff q 0 = 0" by (simp only: integral_iff) with p q show "p = 0 | q = 0" by fastsimp qed qed lemma monom_inj_zero: "(monom a n = 0) = (a = 0)" proof - have "(monom a n = 0) = (monom a n = monom 0 n)" by simp also have "... = (a = 0)" by (simp add: monom_inj del: monom_zero) finally show ?thesis . qed (* term order: makes this simpler!!! lemma smult_integral: "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0" by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero) fast *) lemma smult_integral: "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0" by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero) end
lemma boundI:
(!!m. n < m ==> f m = (0::'a)) ==> bound n f
lemma boundE:
[| bound n f; (!!m. n < m ==> f m = (0::'a)) ==> P |] ==> P
lemma boundD:
[| bound n f; n < m |] ==> f m = (0::'a)
lemma bound_below:
[| bound m f; f n ≠ (0::'a) |] ==> n ≤ m
lemma coeff_bound_ex:
∃n. bound n (coeff p)
lemma bound_coeff_obtain:
(!!n. bound n (coeff p) ==> P) ==> P
lemma coeff_monom:
coeff (a*X^m) n = (if m = n then a else 0::'a)
lemma coeff_zero:
coeff 0 n = (0::'a)
lemma coeff_one:
coeff 1 n = (if n = 0 then 1::'a else 0::'a)
lemma coeff_smult:
coeff (a *s p) n = a * coeff p n
lemma coeff_add:
coeff (p + q) n = coeff p n + coeff q n
lemma coeff_mult:
coeff (p * q) n = (∑i≤n. coeff p i * coeff q (n - i))
lemma coeff_uminus:
coeff (- p) n = - coeff p n
lemma up_eqI:
(!!n. coeff p n = coeff q n) ==> p = q
lemma monom_zero:
(0::'a)*X^n = 0
lemma monom_mult_is_smult:
a*X^0 * p = a *s p
lemma monom_add:
(a + b)*X^n = a*X^n + b*X^n
lemma monom_mult_smult:
(a * b)*X^n = a *s (b*X^n)
lemma monom_uminus:
- a*X^n = - (a*X^n)
lemma monom_one:
(1::'a)*X^0 = 1
lemma monom_inj:
(a*X^n = b*X^n) = (a = b)
lemma smult_l_distr:
(a + b) *s p = a *s p + b *s p
lemma smult_r_distr:
a *s (p + q) = a *s p + a *s q
lemma smult_assoc1:
a * b *s p = a *s (b *s p)
lemma smult_one:
(1::'a) *s p = p
lemma smult_assoc2:
a *s p * q = a *s (p * q)
lemma smult_l_null:
(0::'a) *s p = 0
lemma smult_r_null:
a *s 0 = 0
lemma smult_l_minus:
- a *s p = - (a *s p)
lemma smult_r_minus:
a *s - p = - (a *s p)
lemma deg_aboveI:
(!!m. n < m ==> coeff p m = (0::'a)) ==> deg p ≤ n
lemma deg_aboveD:
deg p < m ==> coeff p m = (0::'a)
lemma deg_belowI:
(n ≠ 0 ==> coeff p n ≠ (0::'a)) ==> n ≤ deg p
lemma lcoeff_nonzero_deg:
deg p ≠ 0 ==> coeff p (deg p) ≠ (0::'a)
lemma lcoeff_nonzero_nonzero:
[| deg p = 0; p ≠ 0 |] ==> coeff p 0 ≠ (0::'a)
lemma lcoeff_nonzero:
p ≠ 0 ==> coeff p (deg p) ≠ (0::'a)
lemma deg_eqI:
[| !!m. n < m ==> coeff p m = (0::'a); !!n. n ≠ 0 ==> coeff p n ≠ (0::'a) |] ==> deg p = n
lemma deg_add:
deg (p + q) ≤ max (deg p) (deg q)
lemma deg_monom_ring:
deg (a*X^n) ≤ n
lemma deg_monom:
a ≠ (0::'a) ==> deg (a*X^n) = n
lemma deg_const:
deg (a*X^0) = 0
lemma deg_zero:
deg 0 = 0
lemma deg_one:
deg 1 = 0
lemma uminus_monom:
(- a = (0::'a)) = (a = (0::'a))
lemma deg_uminus:
deg (- p) = deg p
lemma deg_smult_ring:
deg (a *s p) ≤ (if a = (0::'a) then 0 else deg p)
lemma deg_smult:
deg (a *s p) = (if a = (0::'a) then 0 else deg p)
lemma deg_mult_ring:
deg (p * q) ≤ deg p + deg q
lemma deg_mult:
[| p ≠ 0; q ≠ 0 |] ==> deg (p * q) = deg p + deg q
lemma coeff_natsum:
coeff (setsum p A) k = (∑i∈A. coeff (p i) k)
lemma up_repr:
(∑i≤deg p. coeff p i*X^i) = p
lemma up_repr_le:
deg p ≤ n ==> (∑i≤n. coeff p i*X^i) = p
lemma monom_inj_zero:
(a*X^n = 0) = (a = (0::'a))
lemma smult_integral:
a *s p = 0 ==> a = (0::'a) ∨ p = 0
theorem dvd_imp_deg:
[| p dvd q; q ≠ 0 |] ==> deg p ≤ deg q