Theory: poly

Parents

• list
• pred_set
• lim

Types

Constants

• ##  :real -> real list -> real list
• poly_order  :real -> real list -> num
• poly_diff_aux  :num -> real list -> real list
• poly_divides  :real list -> real list -> bool
• poly_add  :real list -> real list -> real list
• diff  :real list -> real list
• poly_exp  :real list -> num -> real list
• poly_neg  :real list -> real list
• poly_mul  :real list -> real list -> real list
• normalize  :real list -> real list
• degree  :real list -> num
• rsquarefree  :real list -> bool
• poly  :real list -> real -> real

Definitions

degree

|- !p. degree p = PRE (LENGTH (normalize p))

normalize

|- (normalize [] = []) /\
   !h t.
     normalize (h::t) =
     (if normalize t = [] then
        (if h = 0 then [] else [h])
      else
        h::normalize t)

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_def

|- (!x. poly [] x = 0) /\ !h t x. poly (h::t) x = h + x * poly t x

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_exp_def

|- (!p. p poly_exp 0 = [1]) /\ !p n. p poly_exp SUC n = p * p poly_exp n

poly_mul_def

|- (!l2. [] * l2 = []) /\
   !h t l2. (h::t) * l2 = (if t = [] then h ## l2 else h ## l2 + (0::t * l2))

poly_neg_def

|- $~ = $## ~1

rsquarefree

|- !p.
     rsquarefree p =
     ~(poly p = poly []) /\ !a. (poly_order a p = 0) \/ (poly_order a p = 1)

Theorems

DEGREE_ZERO

|- !p. (poly p = poly []) ==> (degree p = 0)

FINITE_LEMMA

|- !i N P. (!x. P x ==> ?n. n < N /\ (x = i n)) ==> ?a. !x. P x ==> x < a

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_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_DIFF

|- !p a.
     ~(poly (diff p) = poly []) /\ ~(poly_order a p = 0) ==>
     (poly_order a p = SUC (poly_order a (diff p)))

ORDER_DIVIDES

|- !p a n.
     [~a; 1] poly_exp n poly_divides p =
     (poly p = poly []) \/ n <= poly_order a p

ORDER_MUL

|- !a p q.
     ~(poly (p * q) = poly []) ==>
     (poly_order a (p * q) = poly_order a p + poly_order a q)

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_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)

POLY_ADD

|- !p1 p2 x. poly (p1 + p2) x = poly p1 x + poly p2 x

POLY_ADD_CLAUSES

|- ([] + p2 = p2) /\ (p1 + [] = p1) /\
   ((h1::t1) + (h2::t2) = h1 + h2::t1 + t2)

POLY_ADD_RZERO

|- !p. poly (p + []) = poly p

POLY_CMUL

|- !p c x. poly (c ## p) x = c * poly p x

POLY_CMUL_CLAUSES

|- (c ## [] = []) /\ (c ## (h::t) = c * h::c ## t)

POLY_CONT

|- !l x. (\x. poly l x) contl x

POLY_DIFF

|- !l x. ((\x. poly l x) diffl poly (diff l) x) x

POLY_DIFF_ADD

|- !p1 p2. poly (diff (p1 + p2)) = poly (diff p1 + diff p2)

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_ISZERO

|- !p n. EVERY (\c. c = 0) (poly_diff_aux (SUC n) p) = EVERY (\c. c = 0) p

POLY_DIFF_AUX_MUL_LEMMA

|- !p n. poly (poly_diff_aux (SUC n) p) = poly (poly_diff_aux n p + p)

POLY_DIFF_AUX_NEG

|- !p n. poly (poly_diff_aux n ~p) = poly ~poly_diff_aux n p

POLY_DIFF_CLAUSES

|- (diff [] = []) /\ (diff [c] = []) /\ (diff (h::t) = poly_diff_aux 1 t)

POLY_DIFF_CMUL

|- !p c. poly (diff (c ## p)) = poly (c ## diff p)

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_DIFF_ISZERO

|- !p. (poly (diff p) = poly []) ==> ?h. poly p = poly [h]

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_MUL

|- !p1 p2. poly (diff (p1 * p2)) = poly (p1 * diff p2 + diff p1 * p2)

POLY_DIFF_MUL_LEMMA

|- !t h. poly (diff (h::t)) = poly ((0::diff t) + t)

POLY_DIFF_NEG

|- !p. poly (diff ~p) = poly ~diff p

POLY_DIFF_WELLDEF

|- !p q. (poly p = poly q) ==> (poly (diff p) = poly (diff q))

POLY_DIFF_ZERO

|- !p. (poly p = poly []) ==> (poly (diff p) = poly [])

POLY_DIFFERENTIABLE

|- !l x. (\x. poly l x) differentiable x

POLY_DIVIDES_ADD

|- !p q r. p poly_divides q /\ p poly_divides r ==> p poly_divides q + r

POLY_DIVIDES_EXP

|- !p m n. m <= n ==> p poly_exp m poly_divides p poly_exp n

POLY_DIVIDES_REFL

|- !p. p poly_divides p

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_TRANS

|- !p q r. p poly_divides q /\ q poly_divides r ==> p poly_divides r

POLY_DIVIDES_ZERO

|- !p q. (poly p = poly []) ==> q poly_divides p

POLY_ENTIRE

|- !p q. (poly (p * q) = poly []) = (poly p = poly []) \/ (poly q = poly [])

POLY_ENTIRE_LEMMA

|- !p q.
     ~(poly p = poly []) /\ ~(poly q = poly []) ==> ~(poly (p * q) = poly [])

POLY_EXP

|- !p n x. poly (p poly_exp n) x = poly p x pow n

POLY_EXP_ADD

|- !d n p. poly (p poly_exp (n + d)) = poly (p poly_exp n * p poly_exp d)

POLY_EXP_DIVIDES

|- !p q m n.
     p poly_exp n poly_divides q /\ m <= n ==> p poly_exp m poly_divides q

POLY_EXP_EQ_0

|- !p n. (poly (p poly_exp n) = poly []) = (poly p = poly []) /\ ~(n = 0)

POLY_EXP_PRIME_EQ_0

|- !a n. ~(poly ([a; 1] poly_exp n) = poly [])

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_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_LENGTH_MUL

|- !q. LENGTH ([~a; 1] * q) = SUC (LENGTH q)

POLY_LINEAR_DIVIDES

|- !a p. (poly p a = 0) = (p = []) \/ ?q. p = [~a; 1] * q

POLY_LINEAR_REM

|- !t h. ?q r. h::t = [r] + [~a; 1] * q

POLY_MONO

|- !x k p. abs x <= k ==> abs (poly p x) <= poly (MAP abs p) k

POLY_MUL

|- !x p1 p2. poly (p1 * p2) x = poly p1 x * poly p2 x

POLY_MUL_ASSOC

|- !p q r. poly (p * (q * r)) = poly (p * q * r)

POLY_MUL_CLAUSES

|- ([] * p2 = []) /\ ([h1] * p2 = h1 ## p2) /\
   ((h1::k1::t1) * p2 = h1 ## p2 + (0::(k1::t1) * p2))

POLY_MUL_LCANCEL

|- !p q r.
     (poly (p * q) = poly (p * r)) = (poly p = poly []) \/ (poly q = poly r)

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_NEG

|- !p x. poly (~p) x = ~poly p x

POLY_NEG_CLAUSES

|- (~[] = []) /\ (~(h::t) = ~h::~t)

POLY_NORMALIZE

|- !p. poly (normalize p) = poly 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)

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_PRIME_EQ_0

|- !a. ~(poly [a; 1] = poly [])

POLY_PRIMES

|- !a p q.
     [a; 1] poly_divides p * q =
     [a; 1] poly_divides p \/ [a; 1] poly_divides q

POLY_ROOTS_FINITE

|- !p.
     ~(poly p = poly []) = ?N i. !x. (poly p x = 0) ==> ?n. n < N /\ (x = i n)

POLY_ROOTS_FINITE_LEMMA

|- !p.
     ~(poly p = poly []) ==>
     ?N i. !x. (poly p x = 0) ==> ?n. n < N /\ (x = i n)

POLY_ROOTS_FINITE_SET

|- !p. ~(poly p = poly []) ==> FINITE {x | poly p x = 0}

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_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_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)

POLY_ZERO

|- !p. (poly p = poly []) = EVERY (\c. c = 0) p

POLY_ZERO_LEMMA

|- !h t. (poly (h::t) = poly []) ==> (h = 0) /\ (poly t = poly [])

RSQUAREFREE_DECOMP

|- !p a.
     rsquarefree p /\ (poly p a = 0) ==>
     ?q. (poly p = poly ([~a; 1] * q)) /\ ~(poly q a = 0)

RSQUAREFREE_ROOTS

|- !p. rsquarefree p = !a. ~((poly p a = 0) /\ (poly (diff p) a = 0))