(*
Title: Univariate Polynomials
Id: $Id$
Author: Clemens Ballarin, started 9 December 1996
Copyright: Clemens Ballarin
*)
header {* Univariate Polynomials *}
theory UnivPoly2
imports "../abstract/Abstract"
begin
(* 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 *}
definition
bound :: "[nat, nat => 'a::zero] => bool" where
"bound n f = (ALL i. n < i --> f i = 0)"
lemma boundI [intro!]: "[| !! m. n < m ==> f m = 0 |] ==> bound n f"
unfolding bound_def by blast
lemma boundE [elim?]: "[| bound n f; (!! m. n < m ==> f m = 0) ==> P |] ==> P"
unfolding bound_def by blast
lemma boundD [dest]: "[| bound n f; n < m |] ==> f m = 0"
unfolding bound_def by blast
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 *}
definition
coeff :: "['a up, nat] => ('a::zero)" where
"coeff p n = Rep_UP p n"
definition
monom :: "['a::zero, nat] => 'a up" ("(3_*X^/_)" [71, 71] 70) where
"monom a n = Abs_UP (%i. if i=n then a else 0)"
definition
smult :: "['a::{zero, times}, 'a up] => 'a up" (infixl "*s" 70) where
"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 *}
definition
deg :: "('a::zero) up => nat" where
"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)
(* Divisibility and degree *)
lemma "!! p::'a::domain up. [| p dvd q; q ~= 0 |] ==> deg p <= deg q"
apply (unfold dvd_def)
apply (erule exE)
apply hypsubst
apply (case_tac "p = 0")
apply (case_tac [2] "k = 0")
apply auto
done
end