Theory "poly"

Signature

Definitions

poly_def

⊢ (∀x. poly [] x = 0) ∧ ∀h t x. poly (h::t) x = h + x * poly t x

poly_add_def

⊢ (∀l2. [] + l2 = l2) ∧
  ∀h t l2. (h::t) + l2 = if l2 = [] then h::t else h + HD l2::t + TL l2

poly_cmul_def

⊢ (∀c. c ## [] = []) ∧ ∀c h t. c ## (h::t) = c * h::c ## t

poly_neg_def

⊢ $~ = $## (-1)

poly_mul_def

⊢ (∀l2. [] * l2 = []) ∧
  ∀h t l2. (h::t) * l2 = if t = [] then h ## l2 else h ## l2 + (0::t * l2)

poly_exp_def

⊢ (∀p. p poly_exp 0 = [1]) ∧ ∀p n. p poly_exp SUC n = p * p poly_exp n

poly_diff_aux_def

⊢ (∀n. poly_diff_aux n [] = []) ∧
  ∀n h t. poly_diff_aux n (h::t) = &n * h::poly_diff_aux (SUC n) t

poly_diff_def

⊢ ∀l. diff l = if l = [] then [] else poly_diff_aux 1 (TL l)

poly_divides

⊢ ∀p1 p2. p1 poly_divides p2 ⇔ ∃q. poly p2 = poly (p1 * q)

poly_order

⊢ ∀a p.
      poly_order a p =
      @n.
          [-a; 1] poly_exp n poly_divides p ∧
          ¬([-a; 1] poly_exp SUC n poly_divides p)

rsquarefree

⊢ ∀p.
      rsquarefree p ⇔
      poly p ≠ poly [] ∧ ∀a. poly_order a p = 0 ∨ poly_order a p = 1

normalize

⊢ normalize [] = [] ∧
  ∀h t.
      normalize (h::t) = if normalize t = [] then if h = 0 then [] else [h]
      else h::normalize t

degree

⊢ ∀p. degree p = PRE (LENGTH (normalize p))

Theorems

POLY_ADD_CLAUSES

⊢ [] + p2 = p2 ∧ p1 + [] = p1 ∧ (h1::t1) + (h2::t2) = h1 + h2::t1 + t2

POLY_CMUL_CLAUSES

⊢ c ## [] = [] ∧ c ## (h::t) = c * h::c ## t

POLY_NEG_CLAUSES

⊢ ¬[] = [] ∧ ¬(h::t) = -h::¬t

POLY_MUL_CLAUSES

⊢ [] * p2 = [] ∧ [h1] * p2 = h1 ## p2 ∧
  (h1::k1::t1) * p2 = h1 ## p2 + (0::(k1::t1) * p2)

POLY_DIFF_CLAUSES

⊢ diff [] = [] ∧ diff [c] = [] ∧ diff (h::t) = poly_diff_aux 1 t

POLY_ADD

⊢ ∀p1 p2 x. poly (p1 + p2) x = poly p1 x + poly p2 x

POLY_CMUL

⊢ ∀p c x. poly (c ## p) x = c * poly p x

POLY_NEG

⊢ ∀p x. poly (¬p) x = -poly p x

POLY_MUL

⊢ ∀x p1 p2. poly (p1 * p2) x = poly p1 x * poly p2 x

POLY_EXP

⊢ ∀p n x. poly (p poly_exp n) x = poly p x pow n

POLY_DIFF_LEMMA

⊢ ∀l n x.
      ((λx. x pow SUC n * poly l x) diffl
       (x pow n * poly (poly_diff_aux (SUC n) l) x)) x

POLY_DIFF

⊢ ∀l x. ((λx. poly l x) diffl poly (diff l) x) x

POLY_DIFFERENTIABLE

⊢ ∀l x. (λx. poly l x) differentiable x

POLY_CONT

⊢ ∀l x. (λx. poly l x) contl x

POLY_IVT_POS

⊢ ∀p a b.
      a < b ∧ poly p a < 0 ∧ poly p b > 0 ⇒ ∃x. a < x ∧ x < b ∧ poly p x = 0

POLY_IVT_NEG

⊢ ∀p a b.
      a < b ∧ poly p a > 0 ∧ poly p b < 0 ⇒ ∃x. a < x ∧ x < b ∧ poly p x = 0

POLY_MVT

⊢ ∀p a b.
      a < b ⇒
      ∃x. a < x ∧ x < b ∧ poly p b − poly p a = (b − a) * poly (diff p) x

POLY_ADD_RZERO

⊢ ∀p. poly (p + []) = poly p

POLY_MUL_ASSOC

⊢ ∀p q r. poly (p * (q * r)) = poly (p * q * r)

POLY_EXP_ADD

⊢ ∀d n p. poly (p poly_exp (n + d)) = poly (p poly_exp n * p poly_exp d)

POLY_DIFF_AUX_ADD

⊢ ∀p1 p2 n.
      poly (poly_diff_aux n (p1 + p2)) =
      poly (poly_diff_aux n p1 + poly_diff_aux n p2)

POLY_DIFF_AUX_CMUL

⊢ ∀p c n. poly (poly_diff_aux n (c ## p)) = poly (c ## poly_diff_aux n p)

POLY_DIFF_AUX_NEG

⊢ ∀p n. poly (poly_diff_aux n (¬p)) = poly (¬poly_diff_aux n p)

POLY_DIFF_AUX_MUL_LEMMA

⊢ ∀p n. poly (poly_diff_aux (SUC n) p) = poly (poly_diff_aux n p + p)

POLY_DIFF_ADD

⊢ ∀p1 p2. poly (diff (p1 + p2)) = poly (diff p1 + diff p2)

POLY_DIFF_CMUL

⊢ ∀p c. poly (diff (c ## p)) = poly (c ## diff p)

POLY_DIFF_NEG

⊢ ∀p. poly (diff (¬p)) = poly (¬diff p)

POLY_DIFF_MUL_LEMMA

⊢ ∀t h. poly (diff (h::t)) = poly ((0::diff t) + t)

POLY_DIFF_MUL

⊢ ∀p1 p2. poly (diff (p1 * p2)) = poly (p1 * diff p2 + diff p1 * p2)

POLY_DIFF_EXP

⊢ ∀p n.
      poly (diff (p poly_exp SUC n)) = poly (&SUC n ## p poly_exp n * diff p)

POLY_DIFF_EXP_PRIME

⊢ ∀n a.
      poly (diff ([-a; 1] poly_exp SUC n)) =
      poly (&SUC n ## [-a; 1] poly_exp n)

POLY_LINEAR_REM

⊢ ∀t h. ∃q r. h::t = [r] + [-a; 1] * q

POLY_LINEAR_DIVIDES

⊢ ∀a p. poly p a = 0 ⇔ p = [] ∨ ∃q. p = [-a; 1] * q

POLY_LENGTH_MUL

⊢ ∀q. LENGTH ([-a; 1] * q) = SUC (LENGTH q)

POLY_ROOTS_INDEX_LEMMA

⊢ ∀n p.
      poly p ≠ poly [] ∧ LENGTH p = n ⇒
      ∃i. ∀x. poly p x = 0 ⇒ ∃m. m ≤ n ∧ x = i m

POLY_ROOTS_INDEX_LENGTH

⊢ ∀p. poly p ≠ poly [] ⇒ ∃i. ∀x. poly p x = 0 ⇒ ∃n. n ≤ LENGTH p ∧ x = i n

POLY_ROOTS_FINITE_LEMMA

⊢ ∀p. poly p ≠ poly [] ⇒ ∃N i. ∀x. poly p x = 0 ⇒ ∃n. n < N ∧ x = i n

FINITE_LEMMA

⊢ ∀i N P. (∀x. P x ⇒ ∃n. n < N ∧ x = i n) ⇒ ∃a. ∀x. P x ⇒ x < a

POLY_ROOTS_FINITE

⊢ ∀p. poly p ≠ poly [] ⇔ ∃N i. ∀x. poly p x = 0 ⇒ ∃n. n < N ∧ x = i n

POLY_ENTIRE_LEMMA

⊢ ∀p q. poly p ≠ poly [] ∧ poly q ≠ poly [] ⇒ poly (p * q) ≠ poly []

POLY_ENTIRE

⊢ ∀p q. poly (p * q) = poly [] ⇔ poly p = poly [] ∨ poly q = poly []

POLY_MUL_LCANCEL

⊢ ∀p q r. poly (p * q) = poly (p * r) ⇔ poly p = poly [] ∨ poly q = poly r

POLY_EXP_EQ_0

⊢ ∀p n. poly (p poly_exp n) = poly [] ⇔ poly p = poly [] ∧ n ≠ 0

POLY_PRIME_EQ_0

⊢ ∀a. poly [a; 1] ≠ poly []

POLY_EXP_PRIME_EQ_0

⊢ ∀a n. poly ([a; 1] poly_exp n) ≠ poly []

POLY_ZERO_LEMMA

⊢ ∀h t. poly (h::t) = poly [] ⇒ h = 0 ∧ poly t = poly []

POLY_ZERO

⊢ ∀p. poly p = poly [] ⇔ EVERY (λc. c = 0) p

POLY_DIFF_AUX_ISZERO

⊢ ∀p n. EVERY (λc. c = 0) (poly_diff_aux (SUC n) p) ⇔ EVERY (λc. c = 0) p

POLY_DIFF_ISZERO

⊢ ∀p. poly (diff p) = poly [] ⇒ ∃h. poly p = poly [h]

POLY_DIFF_ZERO

⊢ ∀p. poly p = poly [] ⇒ poly (diff p) = poly []

POLY_DIFF_WELLDEF

⊢ ∀p q. poly p = poly q ⇒ poly (diff p) = poly (diff q)

POLY_PRIMES

⊢ ∀a p q.
      [a; 1] poly_divides p * q ⇔
      [a; 1] poly_divides p ∨ [a; 1] poly_divides q

POLY_DIVIDES_REFL

⊢ ∀p. p poly_divides p

POLY_DIVIDES_TRANS

⊢ ∀p q r. p poly_divides q ∧ q poly_divides r ⇒ p poly_divides r

POLY_DIVIDES_EXP

⊢ ∀p m n. m ≤ n ⇒ p poly_exp m poly_divides p poly_exp n

POLY_EXP_DIVIDES

⊢ ∀p q m n. p poly_exp n poly_divides q ∧ m ≤ n ⇒ p poly_exp m poly_divides q

POLY_DIVIDES_ADD

⊢ ∀p q r. p poly_divides q ∧ p poly_divides r ⇒ p poly_divides q + r

POLY_DIVIDES_SUB

⊢ ∀p q r. p poly_divides q ∧ p poly_divides q + r ⇒ p poly_divides r

POLY_DIVIDES_SUB2

⊢ ∀p q r. p poly_divides r ∧ p poly_divides q + r ⇒ p poly_divides q

POLY_DIVIDES_ZERO

⊢ ∀p q. poly p = poly [] ⇒ q poly_divides p

POLY_ORDER_EXISTS

⊢ ∀a d p.
      LENGTH p = d ∧ poly p ≠ poly [] ⇒
      ∃n.
          [-a; 1] poly_exp n poly_divides p ∧
          ¬([-a; 1] poly_exp SUC n poly_divides p)

POLY_ORDER

⊢ ∀p a.
      poly p ≠ poly [] ⇒
      ∃!n.
          [-a; 1] poly_exp n poly_divides p ∧
          ¬([-a; 1] poly_exp SUC n poly_divides p)

ORDER

⊢ ∀p a n.
      [-a; 1] poly_exp n poly_divides p ∧
      ¬([-a; 1] poly_exp SUC n poly_divides p) ⇔
      n = poly_order a p ∧ poly p ≠ poly []

ORDER_THM

⊢ ∀p a.
      poly p ≠ poly [] ⇒
      [-a; 1] poly_exp poly_order a p poly_divides p ∧
      ¬([-a; 1] poly_exp SUC (poly_order a p) poly_divides p)

ORDER_UNIQUE

⊢ ∀p a n.
      poly p ≠ poly [] ∧ [-a; 1] poly_exp n poly_divides p ∧
      ¬([-a; 1] poly_exp SUC n poly_divides p) ⇒
      n = poly_order a p

ORDER_POLY

⊢ ∀p q a. poly p = poly q ⇒ poly_order a p = poly_order a q

ORDER_ROOT

⊢ ∀p a. poly p a = 0 ⇔ poly p = poly [] ∨ poly_order a p ≠ 0

ORDER_DIVIDES

⊢ ∀p a n.
      [-a; 1] poly_exp n poly_divides p ⇔
      poly p = poly [] ∨ n ≤ poly_order a p

ORDER_DECOMP

⊢ ∀p a.
      poly p ≠ poly [] ⇒
      ∃q.
          poly p = poly ([-a; 1] poly_exp poly_order a p * q) ∧
          ¬([-a; 1] poly_divides q)

ORDER_MUL

⊢ ∀a p q.
      poly (p * q) ≠ poly [] ⇒
      poly_order a (p * q) = poly_order a p + poly_order a q

ORDER_DIFF

⊢ ∀p a.
      poly (diff p) ≠ poly [] ∧ poly_order a p ≠ 0 ⇒
      poly_order a p = SUC (poly_order a (diff p))

POLY_SQUAREFREE_DECOMP_ORDER

⊢ ∀p q d e r s.
      poly (diff p) ≠ poly [] ∧ poly p = poly (q * d) ∧
      poly (diff p) = poly (e * d) ∧ poly d = poly (r * p + s * diff p) ⇒
      ∀a. poly_order a q = if poly_order a p = 0 then 0 else 1

RSQUAREFREE_ROOTS

⊢ ∀p. rsquarefree p ⇔ ∀a. ¬(poly p a = 0 ∧ poly (diff p) a = 0)

RSQUAREFREE_DECOMP

⊢ ∀p a.
      rsquarefree p ∧ poly p a = 0 ⇒
      ∃q. poly p = poly ([-a; 1] * q) ∧ poly q a ≠ 0

POLY_SQUAREFREE_DECOMP

⊢ ∀p q d e r s.
      poly (diff p) ≠ poly [] ∧ poly p = poly (q * d) ∧
      poly (diff p) = poly (e * d) ∧ poly d = poly (r * p + s * diff p) ⇒
      rsquarefree q ∧ ∀a. poly q a = 0 ⇔ poly p a = 0

POLY_NORMALIZE

⊢ ∀p. poly (normalize p) = poly p

DEGREE_ZERO

⊢ ∀p. poly p = poly [] ⇒ degree p = 0

POLY_ROOTS_FINITE_SET

⊢ ∀p. poly p ≠ poly [] ⇒ FINITE {x | poly p x = 0}

POLY_MONO

⊢ ∀x k p. abs x ≤ k ⇒ abs (poly p x) ≤ poly (MAP abs p) k