1(* ========================================================================= *) 2(* Properties of real polynomials (not canonically represented). *) 3(* ========================================================================= *) 4 5(* 6app load ["numLib", 7 "mesonLib", 8 "tautLib", 9 "numLib", 10 "simpLib", 11 "boolSimps", 12 "arithSimps", 13 "pairSimps", 14 "Ho_Rewrite", 15 "jrhUtils", 16 "limTheory", 17 "listTheory", 18 "pred_setTheory", 19 "realSimps", "RealArith"]; 20*) 21 22open HolKernel Parse boolLib hol88Lib reduceLib pairLib numLib 23 mesonLib tautLib simpLib boolSimps numSimps realSimps 24 pairTheory numTheory prim_recTheory arithmeticTheory listTheory 25 Ho_Rewrite jrhUtils Canon_Port AC realTheory limTheory listTheory 26 pred_setTheory RealArith; 27 28infix THEN THENL ORELSE ORELSEC ## THENC ORELSE_TCL; 29 30val _ = new_theory "poly"; 31val _ = ParseExtras.temp_loose_equality() 32 33 34(* ------------------------------------------------------------------------- *) 35(* Extras needed to port polyTheory to hol98. *) 36(* ------------------------------------------------------------------------- *) 37 38fun LIST_INDUCT_TAC g = 39 let 40 val v = (fst o dest_forall o snd) g 41 val v' = mk_var ("t", type_of v) 42 val tac = 43 CONV_TAC (GEN_ALPHA_CONV v') 44 THEN INDUCT_THEN list_INDUCT ASSUME_TAC 45 THENL [ALL_TAC,GEN_TAC] 46 in 47 tac g 48 end; 49 50val ARITH_TAC = CONV_TAC ARITH_CONV; 51fun ARITH_RULE tm = prove (tm, ARITH_TAC); 52 53val FORALL = LIST_CONJ (map SPEC_ALL (CONJUNCTS EVERY_DEF)); 54 55(* Basic extra theorems *) 56 57val FUN_EQ_THM = prove (Term`!f g. (f = g) = (!x. f x = g x)`, 58 REPEAT GEN_TAC THEN EQ_TAC THENL 59 [DISCH_THEN SUBST1_TAC THEN GEN_TAC THEN REFL_TAC, 60 MATCH_ACCEPT_TAC EQ_EXT]); 61 62val RIGHT_IMP_EXISTS_THM = prove ( 63 Term`!P Q. P ==> (?x. Q x) = (?x. P ==> Q x)`, 64 MESON_TAC []); 65 66val LEFT_IMP_EXISTS_THM = prove ( 67 Term`!P Q. (?x. P x) ==> Q = (!x. P x ==> Q)`, 68 MESON_TAC []); 69 70(* Extra theorems needed about the naturals *) 71 72val NOT_LE = arithmeticTheory.NOT_LESS_EQUAL; 73val SUC_INJ = prim_recTheory.INV_SUC_EQ 74 75val LT_SUC_LE = prove (Term`!m n. m < SUC n = m <= n`, ARITH_TAC); 76 77val LT = prove( 78 Term`(!m:num. m < 0 = F) /\ (!m n. m < SUC n = (m = n) \/ m < n)`, 79 ARITH_TAC); 80 81val LT_ADD_LCANCEL = prove ( 82 Term`!m n p:num. m + n < m + p = n < p`, 83 ARITH_TAC); 84 85val LE_EXISTS = prove ( 86 Term`!m n:num. m <= n = (?d. n = m + d)`, 87 REPEAT (STRIP_TAC ORELSE EQ_TAC) 88 THENL [ 89 EXISTS_TAC (Term`n - m:num`), 90 ALL_TAC 91 ] 92 THEN POP_ASSUM (MP_TAC) 93 THEN ARITH_TAC); 94 95val LE_SUC_LT = prove ( 96 Term`!m n. SUC m <= n = m < n`, 97 ARITH_TAC); 98 99val LT_CASES = prove ( 100 Term`!m n:num. m < n \/ n < m \/ (m = n)`, 101 ARITH_TAC); 102 103val LE_REFL = prove (Term`!n:num. n <= n`, ARITH_TAC); 104 105(* Extra theorems needed about sets *) 106 107val FINITE_SUBSET = prove (Term`!s t. FINITE t /\ s SUBSET t ==> FINITE s`, 108 MESON_TAC [SUBSET_FINITE]); 109 110val FINITE_RULES = prove ( 111 Term`FINITE {} /\ (!x s. FINITE s ==> FINITE (x INSERT s))`, 112 MESON_TAC [FINITE_EMPTY, FINITE_INSERT]); 113 114val GSPEC_DEF = prove (Term`!f. GSPEC f = \v. ?z. f z = (v,T)`, 115GEN_TAC THEN CONV_TAC FUN_EQ_CONV THEN BETA_TAC THEN GEN_TAC 116 THEN ONCE_REWRITE_TAC[BETA_RULE 117 (ONCE_REWRITE_CONV[GSYM SPECIFICATION](Term`(\x. GSPEC f x) x`))] 118 THEN CONV_TAC (ONCE_DEPTH_CONV ETA_CONV) 119 THEN REWRITE_TAC[GSPECIFICATION] 120 THEN MESON_TAC[]); 121 122(* ------------------------------------------------------------------------- *) 123(* Application of polynomial as a real function. *) 124(* ------------------------------------------------------------------------- *) 125 126fun new_recursive_definition ax name def = 127 Prim_rec.new_recursive_definition 128 {name=name, def=def, rec_axiom=ax}; 129 130val poly = new_recursive_definition list_Axiom "poly_def" 131 (Term`(poly [] x = 0r) /\ 132 (poly (h::t) x = h + x * poly t x)`); 133 134 135(* ------------------------------------------------------------------------- *) 136(* Arithmetic operations on polynomials. Overloaded (not sure this is wise). *) 137(* ------------------------------------------------------------------------- *) 138 139val poly_add = new_recursive_definition list_Axiom "poly_add_def" 140 (Term`(poly_add [] l2 = l2) /\ 141 (poly_add (h::t) l2 = if (l2 = []) then h::t 142 else ((h:real) + HD l2)::poly_add t (TL l2))`); 143 144val _ = overload_on ("+", Term`poly_add`); 145 146val _ = Parse.hide "##"; 147 148val poly_cmul = new_recursive_definition list_Axiom "poly_cmul_def" 149 (Term`($## c [] = []) /\ 150 ($## c (h::t) = (c:real * h) :: ($## c t))`); 151val _ = set_fixity "##" (Infixl 600); 152 153val poly_neg = new_definition ("poly_neg_def", Term`poly_neg = $## (~(&1))`); 154 155val _ = overload_on ("~", Term`poly_neg`); 156 157val poly_mul = new_recursive_definition list_Axiom "poly_mul_def" 158 (Term`(poly_mul [] l2 = []) /\ 159 (poly_mul (h::t) l2 = if (t = []) then h ## l2 160 else (h ## l2) + (0r :: poly_mul t l2))`); 161 162val _ = overload_on ("*", Term`poly_mul`); 163 164val poly_exp = new_recursive_definition num_Axiom "poly_exp_def" 165 (Term`(poly_exp p 0 = [1r]) /\ 166 (poly_exp p (SUC n) = poly_mul p (poly_exp p n))`); 167 168val _ = set_fixity "poly_exp" (Infixr 700) ; 169 170 171(* ------------------------------------------------------------------------- *) 172(* Differentiation of polynomials (needs an auxiliary function). *) 173(* ------------------------------------------------------------------------- *) 174 175val poly_diff_aux = new_recursive_definition list_Axiom 176 "poly_diff_aux_def" 177 (Term`(poly_diff_aux n [] = []) /\ 178 (poly_diff_aux n (h::t) = (&n * h) :: poly_diff_aux (SUC n) t)`); 179 180val poly_diff = new_definition ("poly_diff_def", 181 Term`diff l = if l = [] then [] else poly_diff_aux 1 (TL l)`); 182 183 184(* ------------------------------------------------------------------------- *) 185(* Useful clausifications. *) 186(* ------------------------------------------------------------------------- *) 187 188val POLY_ADD_CLAUSES = store_thm("POLY_ADD_CLAUSES", 189 Term`([] + p2 = p2) /\ 190 (p1 + [] = p1) /\ 191 ((h1::t1) + (h2::t2) = (h1 + h2) :: (t1 + t2))`, 192 REWRITE_TAC[poly_add, NOT_CONS_NIL, HD, TL] THEN 193 SPEC_TAC(Term`p1:real list`,Term`p1:real list`) THEN 194 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[poly_add]); 195 196val POLY_CMUL_CLAUSES = store_thm("POLY_CMUL_CLAUSES", 197 Term`(c ## [] = []) /\ 198 (c ## (h::t) = (c * h) :: (c ## t))`, 199 REWRITE_TAC[poly_cmul]); 200 201val POLY_NEG_CLAUSES = store_thm("POLY_NEG_CLAUSES", 202 Term`(poly_neg [] = []) /\ 203 (poly_neg (h::t) = ~h::poly_neg t)`, 204 REWRITE_TAC[poly_neg, POLY_CMUL_CLAUSES, REAL_MUL_LNEG, REAL_MUL_LID]); 205 206val POLY_MUL_CLAUSES = store_thm("POLY_MUL_CLAUSES", 207 Term`([] * p2 = []) /\ 208 ([h1] * p2 = h1 ## p2) /\ 209 ((h1::k1::t1) * p2 = (h1 ## p2) + (&0 :: ((k1::t1) * p2)))`, 210 REWRITE_TAC[poly_mul, NOT_CONS_NIL]); 211 212val POLY_DIFF_CLAUSES = store_thm("POLY_DIFF_CLAUSES", 213 Term`(diff [] = []) /\ 214 (diff [c] = []) /\ 215 (diff (h::t) = poly_diff_aux 1 t)`, 216 REWRITE_TAC[poly_diff, NOT_CONS_NIL, HD, TL, poly_diff_aux]); 217 218(* ------------------------------------------------------------------------- *) 219(* Various natural consequences of syntactic definitions. *) 220(* ------------------------------------------------------------------------- *) 221 222val POLY_ADD = store_thm("POLY_ADD", 223 Term`!p1 p2 x. poly (p1 + p2) x = poly p1 x + poly p2 x`, 224 LIST_INDUCT_TAC THEN REWRITE_TAC[poly_add, poly, REAL_ADD_LID] THEN 225 LIST_INDUCT_TAC THEN 226 ASM_REWRITE_TAC[NOT_CONS_NIL, HD, TL, poly, REAL_ADD_RID] THEN 227 REAL_ARITH_TAC); 228 229val POLY_CMUL = store_thm("POLY_CMUL", 230 Term`!p c x. poly (c ## p) x = c * poly p x`, 231 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[poly, poly_cmul] THEN 232 REAL_ARITH_TAC); 233 234val POLY_NEG = store_thm("POLY_NEG", 235 Term`!p x. poly (poly_neg p) x = ~(poly p x)`, 236 REWRITE_TAC[poly_neg, POLY_CMUL] THEN 237 REAL_ARITH_TAC); 238 239val POLY_MUL = store_thm("POLY_MUL", 240 Term`!x p1 p2. poly (p1 * p2) x = poly p1 x * poly p2 x`, 241 GEN_TAC THEN LIST_INDUCT_TAC THEN 242 REWRITE_TAC[poly_mul, poly, REAL_MUL_LZERO, POLY_CMUL, POLY_ADD] THEN 243 SPEC_TAC(Term`h:real`,Term`h:real`) THEN 244 SPEC_TAC(Term`t:real list`,Term`t:real list`) THEN 245 LIST_INDUCT_TAC THEN 246 REWRITE_TAC[poly_mul, POLY_CMUL, POLY_ADD, poly, POLY_CMUL, 247 REAL_MUL_RZERO, REAL_ADD_RID, NOT_CONS_NIL] THEN 248 ASM_REWRITE_TAC[POLY_ADD, POLY_CMUL, poly] THEN 249 REAL_ARITH_TAC); 250 251val POLY_EXP = store_thm("POLY_EXP", 252 Term`!p n (x:real). poly (p poly_exp n) x = (poly p x) pow n`, 253 GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[poly_exp, pow, POLY_MUL] THEN 254 REWRITE_TAC[poly] THEN REAL_ARITH_TAC); 255 256(* ------------------------------------------------------------------------- *) 257(* The derivative is a bit more complicated. *) 258(* ------------------------------------------------------------------------- *) 259 260val POLY_DIFF_LEMMA = store_thm("POLY_DIFF_LEMMA", 261 (Term`!l n x. ((\x. (x pow (SUC n)) * poly l x) diffl 262 ((x pow n) * poly (poly_diff_aux (SUC n) l) x))(x)`), 263 LIST_INDUCT_TAC THEN 264 REWRITE_TAC[poly, poly_diff_aux, REAL_MUL_RZERO, DIFF_CONST] THEN 265 MAP_EVERY X_GEN_TAC [(Term`n:num`), (Term`x:real`)] THEN 266 REWRITE_TAC[REAL_LDISTRIB, REAL_MUL_ASSOC] THEN 267 ONCE_REWRITE_TAC[GSYM(ONCE_REWRITE_RULE[REAL_MUL_SYM] (CONJUNCT2 pow))] THEN 268 POP_ASSUM(MP_TAC o SPECL [(Term`SUC n`), (Term`x:real`)]) THEN 269 SUBGOAL_THEN ((Term`(((\x. (x pow (SUC n)) * h)) diffl 270 ((x pow n) * &(SUC n) * h))(x)`)) 271 (fn th => DISCH_THEN(MP_TAC o CONJ th)) THENL 272 [REWRITE_TAC[REAL_MUL_ASSOC] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN 273 MP_TAC(SPEC ((Term`\x. x pow (SUC n)`)) DIFF_CMUL) THEN BETA_TAC THEN 274 DISCH_THEN MATCH_MP_TAC THEN 275 MP_TAC(SPEC ((Term`SUC n`)) DIFF_POW) THEN REWRITE_TAC[SUC_SUB1] THEN 276 DISCH_THEN(MATCH_ACCEPT_TAC o ONCE_REWRITE_RULE[REAL_MUL_SYM]), 277 DISCH_THEN(MP_TAC o MATCH_MP DIFF_ADD) THEN BETA_TAC THEN 278 REWRITE_TAC[REAL_MUL_ASSOC]]); 279 280val POLY_DIFF = store_thm("POLY_DIFF", 281 (Term`!l x. ((\x. poly l x) diffl (poly (diff l) x))(x)`), 282 LIST_INDUCT_TAC THEN REWRITE_TAC[POLY_DIFF_CLAUSES] THEN 283 ONCE_REWRITE_TAC[SYM(ETA_CONV (Term`\x. poly l x`))] THEN 284 REWRITE_TAC[poly, DIFF_CONST] THEN 285 MAP_EVERY X_GEN_TAC [(Term`x:real`)] THEN 286 MP_TAC(SPECL [(Term`t:real list`), (Term`0:num`), (Term`x:real`)] 287 POLY_DIFF_LEMMA) THEN 288 REWRITE_TAC[SYM ONE] THEN REWRITE_TAC[pow, REAL_MUL_LID] THEN 289 REWRITE_TAC[POW_1] THEN 290 DISCH_THEN(MP_TAC o CONJ (SPECL [(Term`h:real`), (Term`x:real`)] DIFF_CONST)) 291 THEN DISCH_THEN(MP_TAC o MATCH_MP DIFF_ADD) THEN BETA_TAC THEN 292 REWRITE_TAC[REAL_ADD_LID]); 293 294(* ------------------------------------------------------------------------- *) 295(* Trivial consequences. *) 296(* ------------------------------------------------------------------------- *) 297 298val POLY_DIFFERENTIABLE = store_thm("POLY_DIFFERENTIABLE", 299 (Term`!l x. (\x. poly l x) differentiable x`), 300 REPEAT GEN_TAC THEN REWRITE_TAC[differentiable] THEN 301 EXISTS_TAC (Term`poly (diff l) x`) THEN 302 REWRITE_TAC[POLY_DIFF]); 303 304val POLY_CONT = store_thm("POLY_CONT", 305 (Term`!l x. (\x. poly l x) contl x`), 306 REPEAT GEN_TAC THEN MATCH_MP_TAC DIFF_CONT THEN 307 EXISTS_TAC (Term`poly (diff l) x`) THEN 308 MATCH_ACCEPT_TAC POLY_DIFF); 309 310val POLY_IVT_POS = store_thm("POLY_IVT_POS", 311 (Term`!p a b. a < b /\ poly p a < &0 /\ poly p b > &0 312 ==> ?x. a < x /\ x < b /\ (poly p x = &0)`), 313 REWRITE_TAC[real_gt] THEN REPEAT STRIP_TAC THEN 314 MP_TAC(SPECL [(Term`\x. poly p x`), (Term`a:real`), (Term`b:real`), (Term`&0`)] IVT) THEN 315 SIMP_TAC bool_ss [POLY_CONT] THEN 316 EVERY_ASSUM(fn th => REWRITE_TAC[MATCH_MP REAL_LT_IMP_LE th]) THEN 317 DISCH_THEN(X_CHOOSE_THEN (Term`x:real`) STRIP_ASSUME_TAC) THEN 318 EXISTS_TAC (Term`x:real`) THEN ASM_REWRITE_TAC[REAL_LT_LE] THEN 319 CONJ_TAC THEN DISCH_THEN SUBST_ALL_TAC THEN 320 FIRST_ASSUM SUBST_ALL_TAC THEN 321 RULE_ASSUM_TAC(REWRITE_RULE[REAL_LT_REFL]) THEN 322 FIRST_ASSUM CONTR_TAC); 323 324val POLY_IVT_NEG = store_thm("POLY_IVT_NEG", 325 (Term`!p a b. a < b /\ poly p a > &0 /\ poly p b < &0 326 ==> ?x. a < x /\ x < b /\ (poly p x = &0)`), 327 REPEAT STRIP_TAC THEN MP_TAC(SPEC (Term`poly_neg p`) POLY_IVT_POS) THEN 328 REWRITE_TAC[POLY_NEG, 329 REAL_ARITH (Term`(~x < &0 = x > &0) /\ (~x > &0 = x < &0)`)] THEN 330 DISCH_THEN(MP_TAC o SPECL [(Term`a:real`), (Term`b:real`)]) THEN 331 ASM_REWRITE_TAC[REAL_ARITH (Term`(~x = &0) = (x = &0)`)]); 332 333val POLY_MVT = store_thm("POLY_MVT", 334 (Term`!p a b. a < b ==> 335 ?x. a < x /\ x < b /\ 336 (poly p b - poly p a = (b - a) * poly (diff p) x)`), 337 REPEAT STRIP_TAC THEN 338 MP_TAC(SPECL [(Term`poly p`), (Term`a:real`), (Term`b:real`)] MVT) THEN 339 ASM_REWRITE_TAC[CONV_RULE(DEPTH_CONV ETA_CONV) (SPEC_ALL POLY_CONT), 340 CONV_RULE(DEPTH_CONV ETA_CONV) (SPEC_ALL POLY_DIFFERENTIABLE)] THEN 341 DISCH_THEN(X_CHOOSE_THEN (Term`l:real`) MP_TAC) THEN 342 DISCH_THEN(X_CHOOSE_THEN (Term`x:real`) STRIP_ASSUME_TAC) THEN 343 EXISTS_TAC (Term`x:real`) THEN ASM_REWRITE_TAC[] THEN 344 AP_TERM_TAC THEN MATCH_MP_TAC DIFF_UNIQ THEN 345 EXISTS_TAC (Term`poly p`) THEN EXISTS_TAC (Term`x:real`) THEN 346 ASM_REWRITE_TAC[CONV_RULE(DEPTH_CONV ETA_CONV) (SPEC_ALL POLY_DIFF)]); 347 348(* ------------------------------------------------------------------------- *) 349(* Lemmas. *) 350(* ------------------------------------------------------------------------- *) 351 352val POLY_ADD_RZERO = store_thm("POLY_ADD_RZERO", 353 (Term`!p. poly (p + []) = poly p`), 354 REWRITE_TAC[FUN_EQ_THM, POLY_ADD, poly, REAL_ADD_RID]); 355 356val POLY_MUL_ASSOC = store_thm("POLY_MUL_ASSOC", 357 (Term`!p q r. poly (p * (q * r)) = poly ((p * q) * r)`), 358 REWRITE_TAC[FUN_EQ_THM, POLY_MUL, REAL_MUL_ASSOC]); 359 360val POLY_EXP_ADD = store_thm("POLY_EXP_ADD", 361 (Term`!d n p. poly(p poly_exp (n + d)) = poly(p poly_exp n * p poly_exp d)`), 362 REWRITE_TAC[FUN_EQ_THM, POLY_MUL] THEN 363 INDUCT_TAC THEN ASM_REWRITE_TAC[POLY_MUL, ADD_CLAUSES, poly_exp, poly] THEN 364 REAL_ARITH_TAC); 365 366(* ------------------------------------------------------------------------- *) 367(* Lemmas for derivatives. *) 368(* ------------------------------------------------------------------------- *) 369 370val POLY_DIFF_AUX_ADD = store_thm("POLY_DIFF_AUX_ADD", 371(Term`!p1 p2 n. poly (poly_diff_aux n (p1 + p2)) = 372 poly (poly_diff_aux n p1 + poly_diff_aux n p2)`), 373 REPEAT(LIST_INDUCT_TAC THEN REWRITE_TAC[poly_diff_aux, poly_add]) THEN 374 ASM_REWRITE_TAC[poly_diff_aux, FUN_EQ_THM, poly, NOT_CONS_NIL, HD, TL] THEN 375 REAL_ARITH_TAC); 376 377val POLY_DIFF_AUX_CMUL = store_thm("POLY_DIFF_AUX_CMUL", 378 (Term`!p c n. poly (poly_diff_aux n (c ## p)) = 379 poly (c ## poly_diff_aux n p)`), 380 LIST_INDUCT_TAC THEN 381 ASM_SIMP_TAC real_ac_ss [FUN_EQ_THM, poly, poly_diff_aux, poly_cmul]); 382 383val POLY_DIFF_AUX_NEG = store_thm("POLY_DIFF_AUX_NEG", 384 (Term`!p n. poly (poly_diff_aux n (poly_neg p)) = 385 poly (poly_neg (poly_diff_aux n p))`), 386 REWRITE_TAC[poly_neg, POLY_DIFF_AUX_CMUL]); 387 388val POLY_DIFF_AUX_MUL_LEMMA = store_thm("POLY_DIFF_AUX_MUL_LEMMA", 389 (Term`!p n. poly (poly_diff_aux (SUC n) p) = poly (poly_diff_aux n p + p)`), 390 LIST_INDUCT_TAC THEN REWRITE_TAC[poly_diff_aux, poly_add, NOT_CONS_NIL] THEN 391 ASM_REWRITE_TAC[HD, TL, poly, FUN_EQ_THM] THEN 392 REWRITE_TAC[GSYM REAL_OF_NUM_SUC, REAL_ADD_RDISTRIB, REAL_MUL_LID]); 393 394(* ------------------------------------------------------------------------- *) 395(* Final results for derivatives. *) 396(* ------------------------------------------------------------------------- *) 397 398val POLY_DIFF_ADD = store_thm("POLY_DIFF_ADD", 399 (Term`!p1 p2. poly (diff (p1 + p2)) = 400 poly (diff p1 + diff p2)`), 401 REPEAT LIST_INDUCT_TAC THEN 402 REWRITE_TAC[poly_add, poly_diff, NOT_CONS_NIL, POLY_ADD_RZERO] THEN 403 ASM_REWRITE_TAC[HD, TL, POLY_DIFF_AUX_ADD]); 404 405val POLY_DIFF_CMUL = store_thm("POLY_DIFF_CMUL", 406 (Term`!p c. poly (diff (c ## p)) = poly (c ## diff p)`), 407 LIST_INDUCT_TAC THEN REWRITE_TAC[poly_diff, poly_cmul] THEN 408 REWRITE_TAC[NOT_CONS_NIL, HD, TL, POLY_DIFF_AUX_CMUL]); 409 410val POLY_DIFF_NEG = store_thm("POLY_DIFF_NEG", 411 (Term`!p. poly (diff (poly_neg p)) = poly (poly_neg (diff p))`), 412 REWRITE_TAC[poly_neg, POLY_DIFF_CMUL]); 413 414val POLY_DIFF_MUL_LEMMA = store_thm("POLY_DIFF_MUL_LEMMA", 415 (Term`!t h. poly (diff (CONS h t)) = 416 poly (CONS (&0) (diff t) + t)`), 417 REWRITE_TAC[poly_diff, NOT_CONS_NIL] THEN 418 LIST_INDUCT_TAC THEN REWRITE_TAC[poly_diff_aux, NOT_CONS_NIL, HD, TL] THENL 419 [REWRITE_TAC[FUN_EQ_THM, poly, poly_add, REAL_MUL_RZERO, REAL_ADD_LID], 420 REWRITE_TAC[FUN_EQ_THM, poly, POLY_DIFF_AUX_MUL_LEMMA, POLY_ADD] THEN 421 REAL_ARITH_TAC]); 422 423val POLY_DIFF_MUL = store_thm("POLY_DIFF_MUL", 424 (Term`!p1 p2. poly (diff (p1 * p2)) = 425 poly (p1 * diff p2 + diff p1 * p2)`), 426 LIST_INDUCT_TAC THEN REWRITE_TAC[poly_mul] THENL 427 [REWRITE_TAC[poly_diff, poly_add, poly_mul], ALL_TAC] THEN 428 GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL 429 [REWRITE_TAC[POLY_DIFF_CLAUSES] THEN 430 REWRITE_TAC[poly_add, poly_mul, POLY_ADD_RZERO, POLY_DIFF_CMUL], 431 ALL_TAC] THEN 432 REWRITE_TAC[FUN_EQ_THM, POLY_DIFF_ADD, POLY_ADD] THEN 433 REWRITE_TAC[poly, POLY_ADD, POLY_DIFF_MUL_LEMMA, POLY_MUL] THEN 434 ASM_REWRITE_TAC[POLY_DIFF_CMUL, POLY_ADD, POLY_MUL] THEN 435 REAL_ARITH_TAC); 436 437val POLY_DIFF_EXP = store_thm("POLY_DIFF_EXP", 438 (Term`!p n. poly (diff (p poly_exp (SUC n))) = 439 poly (&(SUC n) ## (p poly_exp n) * diff p)`), 440 GEN_TAC THEN INDUCT_TAC THEN ONCE_REWRITE_TAC[poly_exp] THENL 441 [REWRITE_TAC[poly_exp, POLY_DIFF_MUL] THEN 442 REWRITE_TAC[FUN_EQ_THM, POLY_MUL, POLY_ADD, POLY_CMUL] THEN 443 REWRITE_TAC[poly, POLY_DIFF_CLAUSES, ADD1, ADD_CLAUSES] THEN 444 REAL_ARITH_TAC, 445 REWRITE_TAC[POLY_DIFF_MUL] THEN 446 ASM_REWRITE_TAC[POLY_MUL, POLY_ADD, FUN_EQ_THM, POLY_CMUL] THEN 447 REWRITE_TAC[poly_exp, POLY_MUL] THEN 448 REWRITE_TAC[ADD1, GSYM REAL_OF_NUM_ADD] THEN 449 REAL_ARITH_TAC]); 450 451val POLY_DIFF_EXP_PRIME = store_thm("POLY_DIFF_EXP_PRIME", 452 (Term`!n a. poly (diff ([~a; &1] poly_exp (SUC n))) = 453 poly (&(SUC n) ## ([~a; &1] poly_exp n))`), 454 REPEAT GEN_TAC THEN SIMP_TAC real_ac_ss [POLY_DIFF_EXP] THEN 455 SIMP_TAC real_ac_ss [FUN_EQ_THM, POLY_CMUL, POLY_MUL] THEN 456 SIMP_TAC real_ac_ss [poly_diff, poly_diff_aux, TL, NOT_CONS_NIL] THEN 457 SIMP_TAC real_ac_ss [poly] THEN REAL_ARITH_TAC); 458 459(* ------------------------------------------------------------------------- *) 460(* Key property that f(a) = 0 ==> (x - a) divides p(x). Very delicate! *) 461(* ------------------------------------------------------------------------- *) 462 463val POLY_LINEAR_REM = store_thm("POLY_LINEAR_REM", 464 (Term`!t h. ?q r. h::t = [r] + [~a; &1] * q`), 465 LIST_INDUCT_TAC THEN REWRITE_TAC[] THENL 466 [GEN_TAC THEN EXISTS_TAC (Term`[]:real list`) THEN 467 EXISTS_TAC (Term`h:real`) THEN 468 REWRITE_TAC[poly_add, poly_mul, poly_cmul, NOT_CONS_NIL] THEN 469 REWRITE_TAC[HD, TL, REAL_ADD_RID], 470 X_GEN_TAC (Term`k:real`) THEN 471 POP_ASSUM(STRIP_ASSUME_TAC o SPEC (Term`h:real`)) THEN 472 EXISTS_TAC (Term`CONS (r:real) q`) THEN 473 EXISTS_TAC (Term`r * a + k:real`) THEN 474 ASM_REWRITE_TAC[POLY_ADD_CLAUSES, POLY_MUL_CLAUSES, poly_cmul] THEN 475 REWRITE_TAC[CONS_11] THEN CONJ_TAC THENL 476 [REAL_ARITH_TAC, ALL_TAC] THEN 477 SPEC_TAC((Term`q:real list`),(Term`q:real list`)) THEN 478 LIST_INDUCT_TAC THEN 479 REWRITE_TAC[POLY_ADD_CLAUSES, POLY_MUL_CLAUSES, poly_cmul] THEN 480 REWRITE_TAC[REAL_ADD_RID, REAL_MUL_LID] THEN 481 SIMP_TAC real_ac_ss []]); 482 483val POLY_LINEAR_DIVIDES = store_thm("POLY_LINEAR_DIVIDES", 484 (Term`!a p. (poly p a = &0) = (p = []) \/ ?q. p = [~a; &1] * q`), 485 GEN_TAC THEN LIST_INDUCT_TAC THENL 486 [REWRITE_TAC[poly], ALL_TAC] THEN 487 EQ_TAC THEN STRIP_TAC THENL 488 [DISJ2_TAC THEN STRIP_ASSUME_TAC(SPEC_ALL POLY_LINEAR_REM) THEN 489 EXISTS_TAC (Term`q:real list`) THEN ASM_REWRITE_TAC[] THEN 490 SUBGOAL_THEN (Term`r = &0`) SUBST_ALL_TAC THENL 491 [UNDISCH_TAC (Term`poly (CONS h t) a = &0`) THEN 492 ASM_REWRITE_TAC[] THEN REWRITE_TAC[POLY_ADD, POLY_MUL] THEN 493 REWRITE_TAC[poly, REAL_MUL_RZERO, REAL_ADD_RID, REAL_MUL_RID] THEN 494 REWRITE_TAC[REAL_ARITH (Term`~a + a = &0`)] THEN REAL_ARITH_TAC, 495 REWRITE_TAC[poly_mul] THEN REWRITE_TAC[NOT_CONS_NIL] THEN 496 SPEC_TAC((Term`q:real list`),(Term`q:real list`)) THEN LIST_INDUCT_TAC THENL 497 [REWRITE_TAC[poly_cmul, poly_add, NOT_CONS_NIL, HD, TL, REAL_ADD_LID], 498 REWRITE_TAC[poly_cmul, poly_add, NOT_CONS_NIL, HD, TL, REAL_ADD_LID]]], 499 ASM_REWRITE_TAC[] THEN REWRITE_TAC[poly], 500 ASM_REWRITE_TAC[] THEN REWRITE_TAC[poly] THEN 501 REWRITE_TAC[POLY_MUL] THEN REWRITE_TAC[poly] THEN 502 REWRITE_TAC[poly, REAL_MUL_RZERO, REAL_ADD_RID, REAL_MUL_RID] THEN 503 REWRITE_TAC[REAL_ARITH (Term`~a + a = &0`)] THEN REAL_ARITH_TAC]); 504 505(* ------------------------------------------------------------------------- *) 506(* Thanks to the finesse of the above, we can use length rather than degree. *) 507(* ------------------------------------------------------------------------- *) 508 509val POLY_LENGTH_MUL = store_thm("POLY_LENGTH_MUL", 510 (Term`!q. LENGTH([~a; &1] * q) = SUC(LENGTH q)`), 511 let 512 val lemma = prove 513 ((Term`!p h k a. LENGTH (k ## p + CONS h (a ## p)) = SUC(LENGTH p)`), 514 LIST_INDUCT_TAC THEN 515 ASM_REWRITE_TAC[poly_cmul, POLY_ADD_CLAUSES, LENGTH]) 516 in 517 REWRITE_TAC[poly_mul, NOT_CONS_NIL, lemma] 518 end); 519 520(* ------------------------------------------------------------------------- *) 521(* Thus a nontrivial polynomial of degree n has no more than n roots. *) 522(* ------------------------------------------------------------------------- *) 523 524val POLY_ROOTS_INDEX_LEMMA = store_thm("POLY_ROOTS_INDEX_LEMMA", 525 (Term`!n. !p. ~(poly p = poly []) /\ (LENGTH p = n) 526 ==> ?i. !x. (poly p (x) = &0) ==> ?m. m <= n /\ (x = i m)`), 527 INDUCT_TAC THENL 528 [SIMP_TAC real_ac_ss [LENGTH_NIL], 529 REPEAT STRIP_TAC THEN ASM_CASES_TAC (Term`?a. poly p a = &0`) THENL 530 [UNDISCH_TAC (Term`?a. poly p a = &0`) THEN DISCH_THEN(CHOOSE_THEN MP_TAC) THEN 531 GEN_REWRITE_TAC LAND_CONV [POLY_LINEAR_DIVIDES] THEN 532 DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL [ASM_MESON_TAC[], ALL_TAC] THEN 533 DISCH_THEN(X_CHOOSE_THEN (Term`q:real list`) SUBST_ALL_TAC) THEN 534 FIRST_ASSUM(UNDISCH_TAC o assert is_forall o concl) THEN 535 UNDISCH_TAC (Term`~(poly ([~a; &1] * q) = poly [])`) THEN 536 POP_ASSUM MP_TAC THEN REWRITE_TAC[POLY_LENGTH_MUL, SUC_INJ] THEN 537 DISCH_TAC THEN ASM_CASES_TAC (Term`poly q = poly []`) THENL 538 [ASM_REWRITE_TAC[POLY_MUL, poly, REAL_MUL_RZERO, FUN_EQ_THM], 539 DISCH_THEN(K ALL_TAC)] THEN 540 DISCH_THEN(MP_TAC o SPEC (Term`q:real list`)) THEN ASM_REWRITE_TAC[] THEN 541 DISCH_THEN(X_CHOOSE_TAC (Term`i:num->real`)) THEN 542 EXISTS_TAC (Term`\m. if m = SUC n then (a:real) else i m`) THEN 543 REWRITE_TAC[POLY_MUL, LE, REAL_ENTIRE] THEN 544 X_GEN_TAC (Term`x:real`) THEN DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL 545 [DISCH_THEN(fn th => EXISTS_TAC (Term`SUC n`) THEN MP_TAC th) THEN 546 SIMP_TAC real_ac_ss [] THEN REWRITE_TAC[poly] THEN REAL_ARITH_TAC, 547 DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN 548 DISCH_THEN(X_CHOOSE_THEN (Term`m:num`) STRIP_ASSUME_TAC) THEN 549 EXISTS_TAC (Term`m:num`) THEN ASM_SIMP_TAC real_ac_ss [] THEN 550 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN 551 UNDISCH_TAC (Term`m:num <= n`) THEN ASM_SIMP_TAC real_ac_ss []], 552 UNDISCH_TAC (Term`~(?a. poly p a = &0)`) THEN 553 REWRITE_TAC[NOT_EXISTS_THM] THEN DISCH_TAC 554 THEN ASM_SIMP_TAC bool_ss []]]); 555 556val POLY_ROOTS_INDEX_LENGTH = store_thm("POLY_ROOTS_INDEX_LENGTH", 557 (Term`!p. ~(poly p = poly []) 558 ==> ?i. !x. (poly p(x) = &0) ==> ?n. n <= LENGTH p /\ (x = i n)`), 559 MESON_TAC[POLY_ROOTS_INDEX_LEMMA]); 560 561val POLY_ROOTS_FINITE_LEMMA = store_thm("POLY_ROOTS_FINITE_LEMMA", 562 (Term`!p. ~(poly p = poly []) 563 ==> ?N i. !x. (poly p(x) = &0) ==> ?n:num. n < N /\ (x = i n)`), 564 MESON_TAC[POLY_ROOTS_INDEX_LENGTH, LT_SUC_LE]); 565 566val FINITE_LEMMA = store_thm("FINITE_LEMMA", 567 (Term`!i N P. (!x. P x ==> ?n:num. n < N /\ (x = i n)) 568 ==> ?a. !x. P x ==> x < a`), 569 GEN_TAC THEN ONCE_REWRITE_TAC[RIGHT_IMP_EXISTS_THM] THEN INDUCT_TAC THENL 570 [REWRITE_TAC[LT] THEN MESON_TAC[], ALL_TAC] THEN 571 X_GEN_TAC (Term`P:real->bool`) THEN 572 POP_ASSUM(MP_TAC o SPEC (Term`\z. P z /\ ~(z = (i:num->real) N)`)) THEN 573 DISCH_THEN(X_CHOOSE_TAC (Term`a:real`)) THEN 574 EXISTS_TAC (Term`abs(a) + abs(i(N:num)) + &1`) THEN 575 POP_ASSUM MP_TAC THEN REWRITE_TAC[LT] THEN 576 MP_TAC(REAL_ARITH (Term`!x v. x < abs(v) + abs(x) + &1`)) THEN 577 MP_TAC(REAL_ARITH (Term`!u v x. x < v ==> x < abs(v) + abs(u) + &1`)) THEN 578 MESON_TAC[]); 579 580val POLY_ROOTS_FINITE = store_thm("POLY_ROOTS_FINITE", 581 (Term`!p. ~(poly p = poly []) = 582 ?N i. !x. (poly p(x) = &0) ==> ?n:num. n < N /\ (x = i n)`), 583 GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[POLY_ROOTS_FINITE_LEMMA] THEN 584 REWRITE_TAC[FUN_EQ_THM, LEFT_IMP_EXISTS_THM, NOT_FORALL_THM, poly] THEN 585 MP_TAC(GENL [(Term`i:num->real`), (Term`N:num`)] 586 (SPECL [(Term`i:num->real`), (Term`N:num`), (Term`\x. poly p x = &0`)] FINITE_LEMMA)) THEN 587 REWRITE_TAC[] THEN MESON_TAC[REAL_LT_REFL]); 588 589(* ------------------------------------------------------------------------- *) 590(* Hence get entirety and cancellation for polynomials. *) 591(* ------------------------------------------------------------------------- *) 592 593val POLY_ENTIRE_LEMMA = store_thm("POLY_ENTIRE_LEMMA", 594 (Term`!p q. ~(poly p = poly []) /\ ~(poly q = poly []) 595 ==> ~(poly (p * q) = poly [])`), 596 REPEAT GEN_TAC THEN REWRITE_TAC[POLY_ROOTS_FINITE] THEN 597 DISCH_THEN(CONJUNCTS_THEN MP_TAC) THEN 598 DISCH_THEN(X_CHOOSE_THEN (Term`N2:num`) (X_CHOOSE_TAC (Term`i2:num->real`))) THEN 599 DISCH_THEN(X_CHOOSE_THEN (Term`N1:num`) (X_CHOOSE_TAC (Term`i1:num->real`))) THEN 600 EXISTS_TAC (Term`N1 + N2:num`) THEN 601 EXISTS_TAC (Term`\n:num. if n < N1 then i1(n):real else i2(n - N1)`) THEN 602 X_GEN_TAC (Term`x:real`) THEN REWRITE_TAC[REAL_ENTIRE, POLY_MUL] THEN 603 DISCH_THEN(DISJ_CASES_THEN (ANTE_RES_THEN (X_CHOOSE_TAC (Term`n:num`)))) THENL 604 [EXISTS_TAC (Term`n:num`) THEN ASM_SIMP_TAC real_ac_ss [], 605 EXISTS_TAC (Term`N1 + n:num`) THEN ASM_SIMP_TAC real_ac_ss [LT_ADD_LCANCEL]]); 606 607val POLY_ENTIRE = store_thm("POLY_ENTIRE", 608 (Term`!p q. (poly (p * q) = poly []) = (poly p = poly []) \/ (poly q = poly [])`), 609 REPEAT GEN_TAC THEN EQ_TAC THENL 610 [MESON_TAC[POLY_ENTIRE_LEMMA], 611 REWRITE_TAC[FUN_EQ_THM, POLY_MUL] THEN 612 STRIP_TAC THEN ASM_REWRITE_TAC[REAL_MUL_RZERO, REAL_MUL_LZERO, poly]]); 613 614val POLY_MUL_LCANCEL = store_thm("POLY_MUL_LCANCEL", 615 (Term`!p q r. (poly (p * q) = poly (p * r)) = 616 (poly p = poly []) \/ (poly q = poly r)`), 617 let 618 val lemma1 = prove 619 ((Term`!p q. (poly (p + poly_neg q) = poly []) = (poly p = poly q)`), 620 REWRITE_TAC[FUN_EQ_THM, POLY_ADD, POLY_NEG, poly] THEN 621 REWRITE_TAC[REAL_ARITH (Term`(p + ~q = &0) = (p = q)`)]) 622 val lemma2 = prove 623 ((Term`!p q r. poly (p * q + poly_neg(p * r)) = poly (p * (q + poly_neg(r)))`), 624 REWRITE_TAC[FUN_EQ_THM, POLY_ADD, POLY_NEG, POLY_MUL] THEN 625 REAL_ARITH_TAC) 626 in 627 ONCE_REWRITE_TAC[GSYM lemma1] THEN 628 REWRITE_TAC[lemma2, POLY_ENTIRE] THEN 629 REWRITE_TAC[lemma1] 630 end); 631 632val POLY_EXP_EQ_0 = store_thm("POLY_EXP_EQ_0", 633 (Term`!p n. (poly (p poly_exp n) = poly []) = (poly p = poly []) /\ ~(n = 0)`), 634 REPEAT GEN_TAC THEN REWRITE_TAC[FUN_EQ_THM, poly] THEN 635 REWRITE_TAC [LEFT_AND_FORALL_THM] THEN AP_TERM_TAC THEN ABS_TAC THEN 636 SPEC_TAC((Term`n:num`),(Term`n:num`)) THEN INDUCT_TAC THEN 637 SIMP_TAC real_ac_ss [poly_exp, poly, REAL_MUL_RZERO, REAL_ADD_RID, 638 REAL_OF_NUM_EQ, NOT_SUC] THEN 639 ASM_REWRITE_TAC[POLY_MUL, poly, REAL_ENTIRE] THEN 640 MESON_TAC []); 641 642val POLY_PRIME_EQ_0 = store_thm("POLY_PRIME_EQ_0", 643 (Term`!a. ~(poly [a; &1] = poly [])`), 644 GEN_TAC THEN REWRITE_TAC[FUN_EQ_THM, poly] THEN 645 DISCH_THEN(MP_TAC o SPEC (Term`&1 - a`)) THEN 646 REAL_ARITH_TAC); 647 648val POLY_EXP_PRIME_EQ_0 = store_thm("POLY_EXP_PRIME_EQ_0", 649 (Term`!a n. ~(poly ([a; &1] poly_exp n) = poly [])`), 650 MESON_TAC[POLY_EXP_EQ_0, POLY_PRIME_EQ_0]); 651 652(* ------------------------------------------------------------------------- *) 653(* Can also prove a more "constructive" notion of polynomial being trivial. *) 654(* ------------------------------------------------------------------------- *) 655 656val POLY_ZERO_LEMMA = store_thm("POLY_ZERO_LEMMA", 657 (Term`!h t. (poly (CONS h t) = poly []) ==> (h = &0) /\ (poly t = poly [])`), 658 let 659 val lemma = REWRITE_RULE[FUN_EQ_THM, poly] POLY_ROOTS_FINITE 660 in 661 REPEAT GEN_TAC 662 THEN SIMP_TAC real_ac_ss [FUN_EQ_THM, poly] 663 THEN ASM_CASES_TAC (Term`h = &0`) 664 THEN ASM_SIMP_TAC real_ac_ss [] 665 THENL [ 666 SIMP_TAC real_ac_ss [REAL_ADD_LID] 667 THEN CONV_TAC CONTRAPOS_CONV 668 THEN DISCH_THEN(MP_TAC o REWRITE_RULE[lemma]) 669 THEN DISCH_THEN(X_CHOOSE_THEN (Term`N:num`) (X_CHOOSE_TAC (Term`i:num->real`))) 670 THEN MP_TAC 671 (SPECL [(Term`i:num->real`), (Term`N:num`), (Term`\x. poly t x = &0`)] FINITE_LEMMA) 672 THEN ASM_SIMP_TAC real_ac_ss [] 673 THEN DISCH_THEN(X_CHOOSE_TAC (Term`a:real`)) 674 THEN EXISTS_TAC (Term`abs(a) + &1`) 675 THEN POP_ASSUM (MP_TAC o SPEC (Term`abs(a) + &1`)) 676 THEN REWRITE_TAC [REAL_ENTIRE] 677 THEN REAL_ARITH_TAC, 678 EXISTS_TAC (Term`&0`) 679 THEN ASM_SIMP_TAC real_ac_ss [] 680 ] 681 end); 682 683val POLY_ZERO = store_thm("POLY_ZERO", 684 (Term`!p. (poly p = poly []) = EVERY (\c. c = &0) p`), 685 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[FORALL] THEN EQ_TAC THENL 686 [DISCH_THEN(MP_TAC o MATCH_MP POLY_ZERO_LEMMA) THEN ASM_REWRITE_TAC[], 687 POP_ASSUM(SUBST1_TAC o SYM) THEN STRIP_TAC THEN 688 ASM_REWRITE_TAC[FUN_EQ_THM, poly] THEN REAL_ARITH_TAC]); 689 690(* ------------------------------------------------------------------------- *) 691(* Useful triviality. *) 692(* ------------------------------------------------------------------------- *) 693 694val POLY_DIFF_AUX_ISZERO = store_thm("POLY_DIFF_AUX_ISZERO", 695 (Term`!p n. EVERY (\c. c = &0) (poly_diff_aux (SUC n) p) = 696 EVERY (\c. c = &0) p`), 697 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC 698 [FORALL, poly_diff_aux, REAL_ENTIRE, REAL_OF_NUM_EQ, NOT_SUC]); 699 700 701val POLY_DIFF_ISZERO = store_thm("POLY_DIFF_ISZERO", 702 (Term`!p. (poly (diff p) = poly []) ==> ?h. poly p = poly [h]`), 703 REWRITE_TAC[POLY_ZERO] THEN 704 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[POLY_DIFF_CLAUSES, FORALL] THENL 705 [EXISTS_TAC (Term`&0`) THEN REWRITE_TAC[FUN_EQ_THM, poly] THEN REAL_ARITH_TAC, 706 REWRITE_TAC[ONE, POLY_DIFF_AUX_ISZERO] THEN 707 REWRITE_TAC[GSYM POLY_ZERO] THEN DISCH_TAC THEN 708 EXISTS_TAC (Term`h:real`) THEN ASM_REWRITE_TAC[poly, FUN_EQ_THM]]); 709 710val POLY_DIFF_ZERO = store_thm("POLY_DIFF_ZERO", 711 (Term`!p. (poly p = poly []) ==> (poly (diff p) = poly [])`), 712 REWRITE_TAC[POLY_ZERO] THEN 713 LIST_INDUCT_TAC THEN REWRITE_TAC[poly_diff, NOT_CONS_NIL] THEN 714 REWRITE_TAC[FORALL, TL] THEN 715 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN 716 SPEC_TAC((Term`1:num`),(Term`n:num`)) THEN POP_ASSUM_LIST(K ALL_TAC) THEN 717 SPEC_TAC((Term`t:real list`),(Term`t:real list`)) THEN 718 LIST_INDUCT_TAC THEN REWRITE_TAC[FORALL, poly_diff_aux] THEN 719 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[REAL_MUL_RZERO] THEN 720 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]); 721 722val POLY_DIFF_WELLDEF = store_thm("POLY_DIFF_WELLDEF", 723 (Term`!p q. (poly p = poly q) ==> (poly (diff p) = poly (diff q))`), 724 REPEAT STRIP_TAC THEN MP_TAC(SPEC (Term`p + poly_neg(q)`) POLY_DIFF_ZERO) THEN 725 REWRITE_TAC[FUN_EQ_THM, POLY_DIFF_ADD, POLY_DIFF_NEG, POLY_ADD] THEN 726 ASM_REWRITE_TAC[POLY_NEG, poly, REAL_ARITH (Term`a + ~a = &0`)] THEN 727 REWRITE_TAC[REAL_ARITH (Term`(a + ~b = &0) = (a = b)`)]); 728 729(* ------------------------------------------------------------------------- *) 730(* Basics of divisibility. *) 731(* ------------------------------------------------------------------------- *) 732 733val poly_divides = new_infixl_definition ("poly_divides", 734 (Term`$poly_divides p1 p2 = ?q. poly p2 = poly (p1 * q)`), 475); 735 736val POLY_PRIMES = store_thm("POLY_PRIMES", 737 (Term`!a p q. [a; &1] poly_divides (p * q) 738 = 739 [a; &1] poly_divides p \/ [a; &1] poly_divides q`), 740 REPEAT GEN_TAC THEN REWRITE_TAC[poly_divides, POLY_MUL, FUN_EQ_THM, poly] THEN 741 REWRITE_TAC[REAL_MUL_RZERO, REAL_ADD_RID, REAL_MUL_RID] THEN EQ_TAC THENL 742 [DISCH_THEN(X_CHOOSE_THEN (Term`r:real list`) 743 (MP_TAC o SPEC (Term`~a:real`))) THEN 744 REWRITE_TAC[REAL_ENTIRE, GSYM real_sub, REAL_SUB_REFL, REAL_MUL_LZERO] THEN 745 DISCH_THEN DISJ_CASES_TAC THENL [DISJ1_TAC, DISJ2_TAC] THEN 746 (POP_ASSUM(MP_TAC o REWRITE_RULE[POLY_LINEAR_DIVIDES]) THEN 747 REWRITE_TAC[REAL_NEG_NEG] THEN 748 DISCH_THEN(DISJ_CASES_THEN2 SUBST_ALL_TAC 749 (X_CHOOSE_THEN (Term`s:real list`) SUBST_ALL_TAC)) THENL 750 [EXISTS_TAC (Term`[]:real list`) THEN REWRITE_TAC[poly, REAL_MUL_RZERO], 751 EXISTS_TAC (Term`s:real list`) THEN GEN_TAC THEN 752 REWRITE_TAC[POLY_MUL, poly] THEN REAL_ARITH_TAC]), 753 DISCH_THEN(DISJ_CASES_THEN(X_CHOOSE_TAC (Term`s:real list`))) THEN 754 ASM_REWRITE_TAC[] THENL 755 [EXISTS_TAC (Term`s * q`), EXISTS_TAC (Term`p * s`)] THEN 756 GEN_TAC THEN REWRITE_TAC[POLY_MUL] THEN REAL_ARITH_TAC]); 757 758val POLY_DIVIDES_REFL = store_thm("POLY_DIVIDES_REFL", 759 (Term`!p. p poly_divides p`), 760 GEN_TAC THEN REWRITE_TAC[poly_divides] THEN EXISTS_TAC (Term`[&1]`) THEN 761 REWRITE_TAC[FUN_EQ_THM, POLY_MUL, poly] THEN REAL_ARITH_TAC); 762 763val POLY_DIVIDES_TRANS = store_thm("POLY_DIVIDES_TRANS", 764 (Term`!p q r. p poly_divides q /\ q poly_divides r ==> p poly_divides r`), 765 REPEAT GEN_TAC THEN REWRITE_TAC[poly_divides] THEN 766 DISCH_THEN(CONJUNCTS_THEN MP_TAC) THEN 767 DISCH_THEN(X_CHOOSE_THEN (Term`s:real list`) ASSUME_TAC) THEN 768 DISCH_THEN(X_CHOOSE_THEN (Term`t:real list`) ASSUME_TAC) THEN 769 EXISTS_TAC (Term`t * s`) THEN 770 ASM_REWRITE_TAC[FUN_EQ_THM, POLY_MUL, REAL_MUL_ASSOC]); 771 772val POLY_DIVIDES_EXP = store_thm("POLY_DIVIDES_EXP", 773 (Term`!p m n. m <= n ==> (p poly_exp m) poly_divides (p poly_exp n)`), 774 REPEAT GEN_TAC THEN REWRITE_TAC[LE_EXISTS] THEN 775 DISCH_THEN(X_CHOOSE_THEN (Term`d:num`) SUBST1_TAC) THEN 776 SPEC_TAC((Term`d:num`),(Term`d:num`)) THEN INDUCT_TAC THEN 777 REWRITE_TAC[ADD_CLAUSES, POLY_DIVIDES_REFL] THEN 778 MATCH_MP_TAC POLY_DIVIDES_TRANS THEN 779 EXISTS_TAC (Term`p poly_exp (m + d)`) THEN ASM_REWRITE_TAC[] THEN 780 REWRITE_TAC[poly_divides] THEN EXISTS_TAC (Term`p:real list`) THEN 781 REWRITE_TAC[poly_exp, FUN_EQ_THM, POLY_MUL] THEN 782 REAL_ARITH_TAC); 783 784val POLY_EXP_DIVIDES = store_thm("POLY_EXP_DIVIDES", 785 (Term`!p q m n. 786 (p poly_exp n) poly_divides q /\ m <= n ==> (p poly_exp m) poly_divides q`), 787 MESON_TAC[POLY_DIVIDES_TRANS, POLY_DIVIDES_EXP]); 788 789val POLY_DIVIDES_ADD = store_thm("POLY_DIVIDES_ADD", 790 (Term`!p q r. p poly_divides q /\ p poly_divides r ==> p poly_divides (q + r)`), 791 REPEAT GEN_TAC THEN REWRITE_TAC[poly_divides] THEN 792 DISCH_THEN(CONJUNCTS_THEN MP_TAC) THEN 793 DISCH_THEN(X_CHOOSE_THEN (Term`s:real list`) ASSUME_TAC) THEN 794 DISCH_THEN(X_CHOOSE_THEN (Term`t:real list`) ASSUME_TAC) THEN 795 EXISTS_TAC (Term`t + s`) THEN 796 ASM_REWRITE_TAC[FUN_EQ_THM, POLY_ADD, POLY_MUL] THEN 797 REAL_ARITH_TAC); 798 799val POLY_DIVIDES_SUB = store_thm("POLY_DIVIDES_SUB", 800 (Term`!p q r. p poly_divides q /\ p poly_divides (q + r) ==> p poly_divides r`), 801 REPEAT GEN_TAC THEN REWRITE_TAC[poly_divides] THEN 802 DISCH_THEN(CONJUNCTS_THEN MP_TAC) THEN 803 DISCH_THEN(X_CHOOSE_THEN (Term`s:real list`) ASSUME_TAC) THEN 804 DISCH_THEN(X_CHOOSE_THEN (Term`t:real list`) ASSUME_TAC) THEN 805 EXISTS_TAC (Term`s + poly_neg(t)`) THEN 806 POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN 807 REWRITE_TAC[FUN_EQ_THM, POLY_ADD, POLY_MUL, POLY_NEG] THEN 808 DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN 809 REWRITE_TAC[REAL_ADD_LDISTRIB, REAL_MUL_RNEG] THEN 810 ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC); 811 812val POLY_DIVIDES_SUB2 = store_thm("POLY_DIVIDES_SUB2", 813 (Term`!p q r. p poly_divides r /\ p poly_divides (q + r) ==> p poly_divides q`), 814 REPEAT STRIP_TAC THEN MATCH_MP_TAC POLY_DIVIDES_SUB THEN 815 EXISTS_TAC (Term`r:real list`) THEN ASM_REWRITE_TAC[] THEN 816 UNDISCH_TAC (Term`p poly_divides (q + r)`) THEN 817 REWRITE_TAC[poly_divides, POLY_ADD, FUN_EQ_THM, POLY_MUL] THEN 818 DISCH_THEN(X_CHOOSE_TAC (Term`s:real list`)) THEN 819 EXISTS_TAC (Term`s:real list`) THEN 820 X_GEN_TAC (Term`x:real`) THEN POP_ASSUM(MP_TAC o SPEC (Term`x:real`)) THEN 821 REAL_ARITH_TAC); 822 823val POLY_DIVIDES_ZERO = store_thm("POLY_DIVIDES_ZERO", 824 (Term`!p q. (poly p = poly []) ==> q poly_divides p`), 825 REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[poly_divides] THEN 826 EXISTS_TAC (Term`[]:real list`) THEN 827 ASM_REWRITE_TAC[FUN_EQ_THM, POLY_MUL, poly, REAL_MUL_RZERO]); 828 829(* ------------------------------------------------------------------------- *) 830(* At last, we can consider the order of a root. *) 831(* ------------------------------------------------------------------------- *) 832 833val POLY_ORDER_EXISTS = store_thm("POLY_ORDER_EXISTS", 834 (Term`!a d. !p. (LENGTH p = d) /\ ~(poly p = poly []) 835 ==> ?n. ([~a; &1] poly_exp n) poly_divides p /\ 836 ~(([~a; &1] poly_exp (SUC n)) poly_divides p)`), 837 GEN_TAC 838 THEN (STRIP_ASSUME_TAC o prove_rec_fn_exists num_Axiom) 839 (Term`(!p q. mulexp 0 p q = q) /\ 840 (!p q n. mulexp (SUC n) p q = p * (mulexp n p q))`) 841 THEN SUBGOAL_THEN 842 (Term`!d. !p. (LENGTH p = d) /\ ~(poly p = poly []) 843 ==> ?n q. (p = mulexp (n:num) [~a; &1] q) /\ 844 ~(poly q a = &0)`) MP_TAC 845 THENL [ INDUCT_TAC THENL [SIMP_TAC real_ac_ss [LENGTH_NIL], ALL_TAC] 846 THEN X_GEN_TAC (Term`p:real list`) 847 THEN ASM_CASES_TAC (Term`poly p a = &0`) 848 THENL [ 849 STRIP_TAC 850 THEN UNDISCH_TAC (Term`poly p a = &0`) 851 THEN DISCH_THEN(MP_TAC o REWRITE_RULE[POLY_LINEAR_DIVIDES]) 852 THEN DISCH_THEN(DISJ_CASES_THEN MP_TAC) 853 THENL [ 854 ASM_MESON_TAC[], 855 ALL_TAC 856 ] 857 THEN DISCH_THEN(X_CHOOSE_THEN (Term`q:real list`) SUBST_ALL_TAC) 858 THEN UNDISCH_TAC 859 (Term`!p. (LENGTH p = d) /\ ~(poly p = poly []) 860 ==> ?n q. (p = mulexp (n:num) [~a; &1] q) /\ 861 ~(poly q a = &0)`) 862 THEN DISCH_THEN(MP_TAC o SPEC (Term`q:real list`)) 863 THEN RULE_ASSUM_TAC(REWRITE_RULE[POLY_LENGTH_MUL, POLY_ENTIRE, 864 DE_MORGAN_THM, SUC_INJ]) 865 THEN ASM_REWRITE_TAC[] 866 THEN DISCH_THEN(X_CHOOSE_THEN (Term`n:num`) 867 (X_CHOOSE_THEN (Term`s:real list`) STRIP_ASSUME_TAC)) 868 THEN EXISTS_TAC (Term`SUC n`) 869 THEN EXISTS_TAC (Term`s:real list`) 870 THEN ASM_REWRITE_TAC[], 871 STRIP_TAC 872 THEN EXISTS_TAC (Term`0:num`) 873 THEN EXISTS_TAC (Term`p:real list`) 874 THEN ASM_REWRITE_TAC[] 875 ], 876 DISCH_TAC 877 THEN REPEAT GEN_TAC 878 THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) 879 THEN DISCH_THEN(X_CHOOSE_THEN (Term`n:num`) 880 (X_CHOOSE_THEN (Term`s:real list`) STRIP_ASSUME_TAC)) 881 THEN EXISTS_TAC (Term`n:num`) 882 THEN ASM_REWRITE_TAC[] 883 THEN REWRITE_TAC[poly_divides] 884 THEN CONJ_TAC 885 THENL [ 886 EXISTS_TAC (Term`s:real list`) 887 THEN SPEC_TAC((Term`n:num`),(Term`n:num`)) 888 THEN INDUCT_TAC 889 THEN ASM_REWRITE_TAC[poly_exp, FUN_EQ_THM, POLY_MUL, poly] 890 THEN REAL_ARITH_TAC, 891 DISCH_THEN(X_CHOOSE_THEN (Term`r:real list`) MP_TAC) 892 THEN SPEC_TAC((Term`n:num`),(Term`n:num`)) 893 THEN INDUCT_TAC 894 THEN ASM_SIMP_TAC bool_ss [] 895 THENL [ 896 UNDISCH_TAC (Term`~(poly s a = &0)`) 897 THEN CONV_TAC CONTRAPOS_CONV 898 THEN REWRITE_TAC[] 899 THEN DISCH_THEN SUBST1_TAC 900 THEN REWRITE_TAC[poly, poly_exp, POLY_MUL] 901 THEN REAL_ARITH_TAC, 902 REWRITE_TAC[] 903 THEN ONCE_ASM_REWRITE_TAC[] 904 THEN ONCE_REWRITE_TAC[poly_exp] 905 THEN REWRITE_TAC[GSYM POLY_MUL_ASSOC, POLY_MUL_LCANCEL] 906 THEN REWRITE_TAC[DE_MORGAN_THM] 907 THEN CONJ_TAC 908 THENL [ 909 REWRITE_TAC[FUN_EQ_THM] 910 THEN DISCH_THEN(MP_TAC o SPEC (Term`a + &1`)) 911 THEN REWRITE_TAC[poly] 912 THEN REAL_ARITH_TAC, 913 DISCH_THEN(ANTE_RES_THEN MP_TAC) 914 THEN REWRITE_TAC[] 915 ] 916 ] 917 ] 918 ]); 919 920val POLY_ORDER = store_thm("POLY_ORDER", 921 (Term`!p a. ~(poly p = poly []) 922 ==> ?!n. ([~a; &1] poly_exp n) poly_divides p /\ 923 ~(([~a; &1] poly_exp (SUC n)) poly_divides p)`), 924 MESON_TAC[POLY_ORDER_EXISTS, POLY_EXP_DIVIDES, LE_SUC_LT, LT_CASES]); 925 926(* ------------------------------------------------------------------------- *) 927(* Definition of order. *) 928(* ------------------------------------------------------------------------- *) 929 930val poly_order = new_definition ("poly_order", 931 (Term`poly_order a p = @n. ([~a; &1] poly_exp n) poly_divides p /\ 932 ~(([~a; &1] poly_exp (SUC n)) poly_divides p)`)); 933 934val ORDER = store_thm("ORDER", 935 (Term`!p a n. ([~a; &1] poly_exp n) poly_divides p /\ 936 ~(([~a; &1] poly_exp (SUC n)) poly_divides p) = 937 (n = poly_order a p) /\ 938 ~(poly p = poly [])`), 939 REPEAT GEN_TAC THEN REWRITE_TAC[poly_order] THEN 940 EQ_TAC THEN STRIP_TAC THENL 941 [SUBGOAL_THEN (Term`~(poly p = poly [])`) ASSUME_TAC THENL 942 [FIRST_ASSUM(UNDISCH_TAC o assert is_neg o concl) THEN 943 CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[poly_divides] THEN 944 DISCH_THEN SUBST1_TAC THEN EXISTS_TAC (Term`[]:real list`) THEN 945 REWRITE_TAC[FUN_EQ_THM, POLY_MUL, poly, REAL_MUL_RZERO], 946 ASM_REWRITE_TAC[] THEN CONV_TAC SYM_CONV THEN 947 MATCH_MP_TAC SELECT_UNIQUE THEN REWRITE_TAC[]], 948 ONCE_ASM_REWRITE_TAC[] THEN CONV_TAC SELECT_CONV] THEN 949 ASM_MESON_TAC[POLY_ORDER]); 950 951val ORDER_THM = store_thm("ORDER_THM", 952 (Term`!p a. ~(poly p = poly []) 953 ==> ([~a; &1] poly_exp (poly_order a p)) poly_divides p /\ 954 ~(([~a; &1] poly_exp (SUC(poly_order a p))) poly_divides p)`), 955 MESON_TAC[ORDER]); 956 957val ORDER_UNIQUE = store_thm("ORDER_UNIQUE", 958 (Term`!p a n. ~(poly p = poly []) /\ 959 ([~a; &1] poly_exp n) poly_divides p /\ 960 ~(([~a; &1] poly_exp (SUC n)) poly_divides p) 961 ==> (n = poly_order a p)`), 962 MESON_TAC[ORDER]); 963 964val ORDER_POLY = store_thm("ORDER_POLY", 965 (Term`!p q a. (poly p = poly q) ==> (poly_order a p = poly_order a q)`), 966 REPEAT STRIP_TAC THEN 967 ASM_REWRITE_TAC[poly_order, poly_divides, FUN_EQ_THM, POLY_MUL]); 968 969val ORDER_ROOT = store_thm("ORDER_ROOT", 970 (Term`!p a. (poly p a = &0) = (poly p = poly []) \/ ~(poly_order a p = 0)`), 971 REPEAT GEN_TAC THEN ASM_CASES_TAC (Term`poly p = poly []`) THEN 972 ASM_REWRITE_TAC[poly] THEN EQ_TAC THENL 973 [DISCH_THEN(MP_TAC o REWRITE_RULE[POLY_LINEAR_DIVIDES]) THEN 974 ASM_CASES_TAC (Term`p:real list = []`) THENL [ASM_MESON_TAC[], ALL_TAC] THEN 975 ASM_REWRITE_TAC[] THEN 976 DISCH_THEN(X_CHOOSE_THEN (Term`q:real list`) SUBST_ALL_TAC) THEN DISCH_TAC THEN 977 FIRST_ASSUM(MP_TAC o SPEC (Term`a:real`) o MATCH_MP ORDER_THM) THEN 978 ASM_REWRITE_TAC[poly_exp, DE_MORGAN_THM] THEN DISJ2_TAC THEN 979 REWRITE_TAC[poly_divides] THEN EXISTS_TAC (Term`q:real list`) THEN 980 REWRITE_TAC[FUN_EQ_THM, POLY_MUL, poly] THEN REAL_ARITH_TAC, 981 DISCH_TAC THEN 982 FIRST_ASSUM(MP_TAC o SPEC (Term`a:real`) o MATCH_MP ORDER_THM) THEN 983 UNDISCH_TAC (Term`~(poly_order a p = 0)`) THEN 984 SPEC_TAC((Term`poly_order a p`),(Term`n:num`)) THEN 985 INDUCT_TAC THEN ASM_REWRITE_TAC[poly_exp, NOT_SUC] THEN 986 DISCH_THEN(MP_TAC o CONJUNCT1) THEN REWRITE_TAC[poly_divides] THEN 987 DISCH_THEN(X_CHOOSE_THEN (Term`s:real list`) SUBST1_TAC) THEN 988 REWRITE_TAC[POLY_MUL, poly] THEN REAL_ARITH_TAC]); 989 990val ORDER_DIVIDES = store_thm("ORDER_DIVIDES", 991 (Term`!p a n. ([~a; &1] poly_exp n) poly_divides p = 992 (poly p = poly []) \/ n <= poly_order a p`), 993 REPEAT GEN_TAC THEN ASM_CASES_TAC (Term`poly p = poly []`) THEN 994 ASM_REWRITE_TAC[] THENL 995 [ASM_REWRITE_TAC[poly_divides] THEN EXISTS_TAC (Term`[]:real list`) THEN 996 REWRITE_TAC[FUN_EQ_THM, POLY_MUL, poly, REAL_MUL_RZERO], 997 ASM_MESON_TAC[ORDER_THM, POLY_EXP_DIVIDES, NOT_LE, LE_SUC_LT]]); 998 999val ORDER_DECOMP = store_thm("ORDER_DECOMP", 1000 (Term`!p a. ~(poly p = poly []) 1001 ==> ?q. (poly p = poly (([~a; &1] poly_exp (poly_order a p)) * q)) /\ 1002 ~([~a; &1] poly_divides q)`), 1003 REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP ORDER_THM) THEN 1004 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC o SPEC (Term`a:real`)) THEN 1005 DISCH_THEN(X_CHOOSE_TAC (Term`q:real list`) o REWRITE_RULE[poly_divides]) THEN 1006 EXISTS_TAC (Term`q:real list`) THEN ASM_REWRITE_TAC[] THEN 1007 DISCH_THEN(X_CHOOSE_TAC (Term`r: real list`) o REWRITE_RULE[poly_divides]) THEN 1008 UNDISCH_TAC (Term`~([~ a; &1] poly_exp SUC (poly_order a p) poly_divides p)`) THEN 1009 ASM_REWRITE_TAC[] THEN REWRITE_TAC[poly_divides] THEN 1010 EXISTS_TAC (Term`r:real list`) THEN 1011 ASM_REWRITE_TAC[POLY_MUL, FUN_EQ_THM, poly_exp] THEN 1012 REAL_ARITH_TAC); 1013 1014(* ------------------------------------------------------------------------- *) 1015(* Important composition properties of orders. *) 1016(* ------------------------------------------------------------------------- *) 1017 1018val ORDER_MUL = store_thm("ORDER_MUL", 1019 (Term`!a p q. ~(poly (p * q) = poly []) ==> 1020 (poly_order a (p * q) = poly_order a p + poly_order a q)`), 1021 REPEAT GEN_TAC 1022 THEN DISCH_THEN(fn th => ASSUME_TAC th THEN MP_TAC th) 1023 THEN REWRITE_TAC[POLY_ENTIRE, DE_MORGAN_THM] 1024 THEN STRIP_TAC 1025 THEN SUBGOAL_THEN (Term`(poly_order a p + poly_order a q 1026 = poly_order a (p * q)) /\ ~(poly (p * q) = poly [])`) MP_TAC 1027 THENL [ 1028 ALL_TAC, 1029 MESON_TAC[] 1030 ] 1031 THEN REWRITE_TAC[GSYM ORDER] 1032 THEN CONJ_TAC 1033 THENL [ 1034 MP_TAC(CONJUNCT1 (SPEC (Term`a:real`) 1035 (MATCH_MP ORDER_THM (ASSUME (Term`~(poly p = poly [])`))))) 1036 THEN DISCH_THEN(X_CHOOSE_TAC (Term`r: real list`) o REWRITE_RULE[poly_divides]) 1037 THEN MP_TAC(CONJUNCT1 (SPEC (Term`a:real`) 1038 (MATCH_MP ORDER_THM (ASSUME (Term`~(poly q = poly [])`))))) 1039 THEN DISCH_THEN(X_CHOOSE_TAC (Term`s: real list`) o REWRITE_RULE[poly_divides]) 1040 THEN REWRITE_TAC[poly_divides, FUN_EQ_THM] 1041 THEN EXISTS_TAC (Term`s * r`) 1042 THEN ASM_REWRITE_TAC[POLY_MUL, POLY_EXP_ADD] 1043 THEN REAL_ARITH_TAC, 1044 X_CHOOSE_THEN (Term`r: real list`) STRIP_ASSUME_TAC 1045 (SPEC (Term`a:real`) (MATCH_MP ORDER_DECOMP (ASSUME (Term`~(poly p = poly [])`)))) 1046 THEN X_CHOOSE_THEN (Term`s: real list`) STRIP_ASSUME_TAC 1047 (SPEC (Term`a:real`) (MATCH_MP ORDER_DECOMP (ASSUME (Term`~(poly q = poly [])`)))) 1048 THEN ASM_REWRITE_TAC[poly_divides, FUN_EQ_THM, POLY_EXP_ADD, POLY_MUL, poly_exp] 1049 THEN DISCH_THEN(X_CHOOSE_THEN (Term`t:real list`) STRIP_ASSUME_TAC) 1050 THEN SUBGOAL_THEN (Term`[~a; &1] poly_divides (r * s)`) MP_TAC 1051 THENL [ 1052 ALL_TAC, 1053 ASM_REWRITE_TAC[POLY_PRIMES] 1054 ] 1055 THEN REWRITE_TAC[poly_divides] 1056 THEN EXISTS_TAC (Term`t:real list`) 1057 THEN SUBGOAL_THEN (Term`poly ([~ a; &1] poly_exp (poly_order a p) * (r * s)) = 1058 poly ([~ a; &1] poly_exp (poly_order a p) * ([~ a; &1] * t))`) MP_TAC 1059 THENL [ 1060 ALL_TAC, 1061 MESON_TAC[POLY_MUL_LCANCEL, POLY_EXP_PRIME_EQ_0] 1062 ] 1063 THEN SUBGOAL_THEN (Term`poly ([~ a; &1] poly_exp (poly_order a q) * 1064 ([~ a; &1] poly_exp (poly_order a p) * (r * s))) = 1065 poly ([~ a; &1] poly_exp (poly_order a q) * 1066 ([~ a; &1] poly_exp (poly_order a p) * 1067 ([~ a; &1] * t)))`) MP_TAC 1068 THENL [ 1069 ALL_TAC, 1070 MESON_TAC[POLY_MUL_LCANCEL, POLY_EXP_PRIME_EQ_0] 1071 ] 1072 THEN REWRITE_TAC[FUN_EQ_THM, POLY_MUL, POLY_ADD] 1073 THEN FIRST_ASSUM(UNDISCH_TAC o assert is_forall o concl) 1074 THEN SIMP_TAC real_ac_ss [] 1075 ]); 1076 1077val ORDER_DIFF = store_thm("ORDER_DIFF", 1078 (Term`!p a. ~(poly (diff p) = poly []) /\ 1079 ~(poly_order a p = 0) 1080 ==> (poly_order a p = SUC (poly_order a (diff p)))`), 1081 REPEAT GEN_TAC THEN 1082 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN 1083 SUBGOAL_THEN (Term`~(poly p = poly [])`) MP_TAC THENL 1084 [ASM_MESON_TAC[POLY_DIFF_ZERO], ALL_TAC] THEN 1085 DISCH_THEN(X_CHOOSE_THEN (Term`q:real list`) MP_TAC o 1086 SPEC (Term`a:real`) o MATCH_MP ORDER_DECOMP) THEN 1087 SPEC_TAC((Term`poly_order a p`),(Term`n:num`)) THEN 1088 INDUCT_TAC THEN REWRITE_TAC[NOT_SUC, SUC_INJ] THEN 1089 STRIP_TAC THEN MATCH_MP_TAC ORDER_UNIQUE THEN 1090 ASM_REWRITE_TAC[] THEN 1091 SUBGOAL_THEN (Term`!r. r poly_divides (diff p) = 1092 r poly_divides (diff ([~ a; &1] poly_exp SUC n * q))`) 1093 (fn th => REWRITE_TAC[th]) THENL 1094 [GEN_TAC THEN REWRITE_TAC[poly_divides] THEN 1095 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP POLY_DIFF_WELLDEF th]), 1096 ALL_TAC] THEN 1097 CONJ_TAC THENL 1098 [REWRITE_TAC[poly_divides, FUN_EQ_THM] THEN 1099 EXISTS_TAC (Term`[~a; &1] * (diff q) + &(SUC n) ## q`) THEN 1100 REWRITE_TAC[POLY_DIFF_MUL, POLY_DIFF_EXP_PRIME, 1101 POLY_ADD, POLY_MUL, POLY_CMUL] THEN 1102 REWRITE_TAC[poly_exp, POLY_MUL] THEN REAL_ARITH_TAC, 1103 REWRITE_TAC[FUN_EQ_THM, poly_divides, POLY_DIFF_MUL, POLY_DIFF_EXP_PRIME, 1104 POLY_ADD, POLY_MUL, POLY_CMUL] THEN 1105 DISCH_THEN(X_CHOOSE_THEN (Term`r:real list`) ASSUME_TAC) THEN 1106 UNDISCH_TAC (Term`~([~ a; &1] poly_divides q)`) THEN 1107 REWRITE_TAC[poly_divides] THEN 1108 EXISTS_TAC (Term`inv(&(SUC n)) ## (r + poly_neg(diff q))`) THEN 1109 SUBGOAL_THEN 1110 (Term`poly ([~a; &1] poly_exp n * q) = 1111 poly ([~a; &1] poly_exp n * ([~ a; &1] * (inv (&(SUC n)) ## 1112 (r + poly_neg (diff q)))))`) 1113 MP_TAC THENL 1114 [ALL_TAC, MESON_TAC[POLY_MUL_LCANCEL, POLY_EXP_PRIME_EQ_0]] THEN 1115 REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC (Term`x:real`) THEN 1116 SUBGOAL_THEN 1117 (Term`!a b. (&(SUC n) * a = &(SUC n) * b) ==> (a = b)`) 1118 MATCH_MP_TAC THENL 1119 [REWRITE_TAC[REAL_EQ_MUL_LCANCEL, REAL_OF_NUM_EQ, NOT_SUC], ALL_TAC] THEN 1120 REWRITE_TAC[POLY_MUL, POLY_CMUL] THEN 1121 SUBGOAL_THEN (Term`!a b c. &(SUC n) * (a * (b * (inv(&(SUC n)) * c))) = 1122 a * (b * c)`) 1123 (fn th => REWRITE_TAC[th]) THENL 1124 [REPEAT GEN_TAC THEN 1125 GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] THEN 1126 REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN AP_TERM_TAC THEN 1127 AP_TERM_TAC THEN 1128 GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] THEN 1129 GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN 1130 REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN AP_TERM_TAC THEN 1131 MATCH_MP_TAC REAL_MUL_RINV THEN 1132 REWRITE_TAC[REAL_OF_NUM_EQ, NOT_SUC], ALL_TAC] THEN 1133 FIRST_ASSUM(MP_TAC o SPEC (Term`x:real`)) THEN 1134 REWRITE_TAC[poly_exp, POLY_MUL, POLY_ADD, POLY_NEG] THEN 1135 REAL_ARITH_TAC]); 1136 1137(* ------------------------------------------------------------------------- *) 1138(* Now justify the standard squarefree decomposition, i.e. f / gcd(f,f'). *) 1139(* ------------------------------------------------------------------------- *) 1140 1141val POLY_SQUAREFREE_DECOMP_ORDER = store_thm("POLY_SQUAREFREE_DECOMP_ORDER", 1142 (Term`!p q d e r s. 1143 ~(poly (diff p) = poly []) /\ 1144 (poly p = poly (q * d)) /\ 1145 (poly (diff p) = poly (e * d)) /\ 1146 (poly d = poly (r * p + s * diff p)) 1147 ==> !a. poly_order a q = (if (poly_order a p = 0) then 0 else 1)`), 1148 REPEAT STRIP_TAC THEN 1149 SUBGOAL_THEN (Term`poly_order a p = poly_order a q + poly_order a d`) MP_TAC THENL 1150 [MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC (Term`poly_order a (q * d)`) THEN 1151 CONJ_TAC THENL 1152 [MATCH_MP_TAC ORDER_POLY THEN ASM_REWRITE_TAC[], 1153 MATCH_MP_TAC ORDER_MUL THEN 1154 FIRST_ASSUM(fn th => 1155 GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) [SYM th]) THEN 1156 ASM_MESON_TAC[POLY_DIFF_ZERO]], ALL_TAC] THEN 1157 ASM_CASES_TAC (Term`poly_order a p = 0`) THEN ASM_REWRITE_TAC[] THENL 1158 [ARITH_TAC, ALL_TAC] THEN 1159 SUBGOAL_THEN (Term`poly_order a (diff p) = 1160 poly_order a e + poly_order a d`) MP_TAC THENL 1161 [MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC (Term`poly_order a (e * d)`) THEN 1162 CONJ_TAC THENL 1163 [ASM_MESON_TAC[ORDER_POLY], ASM_MESON_TAC[ORDER_MUL]], ALL_TAC] THEN 1164 SUBGOAL_THEN (Term`~(poly p = poly [])`) ASSUME_TAC THENL 1165 [ASM_MESON_TAC[POLY_DIFF_ZERO], ALL_TAC] THEN 1166 MP_TAC(SPECL [(Term`p:real list`), (Term`a:real`)] ORDER_DIFF) THEN 1167 ASM_REWRITE_TAC[] THEN 1168 DISCH_THEN(fn th => MP_TAC th THEN MP_TAC(AP_TERM (Term`PRE`) th)) THEN 1169 REWRITE_TAC[PRE] THEN DISCH_THEN(ASSUME_TAC o SYM) THEN 1170 SUBGOAL_THEN (Term`poly_order a (diff p) <= poly_order a d`) MP_TAC THENL 1171 [SUBGOAL_THEN (Term`([~a; &1] poly_exp (poly_order a (diff p))) poly_divides d`) 1172 MP_TAC THENL [ALL_TAC, ASM_MESON_TAC[POLY_ENTIRE, ORDER_DIVIDES]] THEN 1173 SUBGOAL_THEN 1174 (Term`([~a; &1] poly_exp (poly_order a (diff p))) poly_divides p /\ 1175 ([~a; &1] poly_exp (poly_order a (diff p))) poly_divides (diff p)`) 1176 MP_TAC THENL 1177 [REWRITE_TAC[ORDER_DIVIDES, LE_REFL] THEN DISJ2_TAC THEN 1178 REWRITE_TAC[ASSUME (Term`poly_order a (diff p) = PRE (poly_order a p)`)] THEN 1179 ARITH_TAC, 1180 DISCH_THEN(CONJUNCTS_THEN MP_TAC) THEN REWRITE_TAC[poly_divides] THEN 1181 REWRITE_TAC[ASSUME (Term`poly d = poly (r * p + s * diff p)`)] THEN 1182 POP_ASSUM_LIST(K ALL_TAC) THEN 1183 SIMP_TAC bool_ss [FUN_EQ_THM, POLY_MUL, POLY_ADD] THEN 1184 DISCH_THEN(X_CHOOSE_THEN (Term`f:real list`) ASSUME_TAC) THEN 1185 DISCH_THEN(X_CHOOSE_THEN (Term`g:real list`) ASSUME_TAC) THEN 1186 EXISTS_TAC (Term`r * g + s * f`) 1187 THEN GEN_TAC 1188 THEN SIMP_TAC real_ac_ss [POLY_MUL, POLY_ADD, REAL_LDISTRIB] 1189 THEN ASM_REWRITE_TAC [] THEN REAL_ARITH_TAC], 1190 ARITH_TAC]); 1191 1192(* ------------------------------------------------------------------------- *) 1193(* Define being "squarefree" --- NB with respect to real roots only. *) 1194(* ------------------------------------------------------------------------- *) 1195 1196val rsquarefree = new_definition ("rsquarefree", 1197 (Term`rsquarefree p = ~(poly p = poly []) /\ 1198 !a. (poly_order a p = 0) \/ (poly_order a p = 1)`)); 1199 1200(* ------------------------------------------------------------------------- *) 1201(* Standard squarefree criterion and rephasing of squarefree decomposition. *) 1202(* ------------------------------------------------------------------------- *) 1203 1204val RSQUAREFREE_ROOTS = store_thm("RSQUAREFREE_ROOTS", 1205 (Term`!p. rsquarefree p = !a. ~((poly p a = &0) /\ (poly (diff p) a = &0))`), 1206 GEN_TAC THEN REWRITE_TAC[rsquarefree] THEN 1207 ASM_CASES_TAC (Term`poly p = poly []`) THEN ASM_REWRITE_TAC[] THENL 1208 [FIRST_ASSUM(SUBST1_TAC o MATCH_MP POLY_DIFF_ZERO) THEN 1209 ASM_REWRITE_TAC[poly, NOT_FORALL_THM], 1210 ASM_CASES_TAC (Term`poly(diff p) = poly []`) THEN ASM_REWRITE_TAC[] THENL 1211 [FIRST_ASSUM(X_CHOOSE_THEN (Term`h:real`) MP_TAC o 1212 MATCH_MP POLY_DIFF_ISZERO) THEN 1213 DISCH_THEN(fn th => ASSUME_TAC th THEN MP_TAC th) THEN 1214 DISCH_THEN(fn th => REWRITE_TAC[MATCH_MP ORDER_POLY th]) THEN 1215 UNDISCH_TAC (Term`~(poly p = poly [])`) THEN ASM_REWRITE_TAC[poly] THEN 1216 REWRITE_TAC[FUN_EQ_THM, poly, REAL_MUL_RZERO, REAL_ADD_RID] THEN 1217 DISCH_TAC THEN ASM_REWRITE_TAC[] THEN 1218 X_GEN_TAC (Term`a:real`) THEN DISJ1_TAC THEN 1219 MP_TAC(SPECL [(Term`[h:real]`), (Term`a:real`)] ORDER_ROOT) THEN 1220 ASM_REWRITE_TAC[FUN_EQ_THM, poly, REAL_MUL_RZERO, REAL_ADD_RID], 1221 ASM_REWRITE_TAC[ORDER_ROOT, DE_MORGAN_THM, ONE] THEN 1222 ASM_MESON_TAC[ORDER_DIFF, SUC_INJ]]]); 1223 1224val RSQUAREFREE_DECOMP = store_thm("RSQUAREFREE_DECOMP", 1225 (Term`!p a. rsquarefree p /\ (poly p a = &0) 1226 ==> ?q. (poly p = poly ([~a; &1] * q)) /\ 1227 ~(poly q a = &0)`), 1228 REPEAT GEN_TAC THEN REWRITE_TAC[rsquarefree] THEN STRIP_TAC THEN 1229 FIRST_ASSUM(MP_TAC o MATCH_MP ORDER_DECOMP) THEN 1230 DISCH_THEN(X_CHOOSE_THEN (Term`q:real list`) MP_TAC o SPEC (Term`a:real`)) THEN 1231 FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [ORDER_ROOT]) THEN 1232 FIRST_ASSUM(DISJ_CASES_TAC o SPEC (Term`a:real`)) THEN 1233 ASM_SIMP_TAC real_ac_ss [] THEN 1234 DISCH_THEN(CONJUNCTS_THEN2 SUBST_ALL_TAC ASSUME_TAC) THEN 1235 EXISTS_TAC (Term`q:real list`) THEN CONJ_TAC THENL 1236 [REWRITE_TAC[FUN_EQ_THM, POLY_MUL] THEN GEN_TAC THEN 1237 AP_THM_TAC THEN AP_TERM_TAC THEN 1238 GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o RAND_CONV) [ONE] THEN 1239 REWRITE_TAC[poly_exp, POLY_MUL] THEN 1240 REWRITE_TAC[poly] THEN REAL_ARITH_TAC, 1241 DISCH_TAC THEN UNDISCH_TAC (Term`~([~a; &1] poly_divides q)`) THEN 1242 REWRITE_TAC[poly_divides] THEN 1243 UNDISCH_TAC (Term`poly q a = &0`) THEN 1244 GEN_REWRITE_TAC LAND_CONV [POLY_LINEAR_DIVIDES] THEN 1245 ASM_CASES_TAC (Term`q:real list = []`) THEN ASM_REWRITE_TAC[] THENL 1246 [EXISTS_TAC (Term`[] : real list`) THEN REWRITE_TAC[FUN_EQ_THM] THEN 1247 REWRITE_TAC[POLY_MUL, poly, REAL_MUL_RZERO], 1248 MESON_TAC[]]]); 1249 1250val POLY_SQUAREFREE_DECOMP = store_thm("POLY_SQUAREFREE_DECOMP", 1251 (Term`!p q d e r s. 1252 ~(poly (diff p) = poly []) /\ 1253 (poly p = poly (q * d)) /\ 1254 (poly (diff p) = poly (e * d)) /\ 1255 (poly d = poly (r * p + s * diff p)) 1256 ==> rsquarefree q /\ (!a. (poly q a = &0) = (poly p a = &0))`), 1257 REPEAT GEN_TAC THEN DISCH_THEN(fn th => MP_TAC th THEN 1258 ASSUME_TAC(MATCH_MP POLY_SQUAREFREE_DECOMP_ORDER th)) THEN 1259 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN 1260 SUBGOAL_THEN (Term`~(poly p = poly [])`) ASSUME_TAC THENL 1261 [ASM_MESON_TAC[POLY_DIFF_ZERO], ALL_TAC] THEN 1262 DISCH_THEN(ASSUME_TAC o CONJUNCT1) THEN 1263 UNDISCH_TAC (Term`~(poly p = poly [])`) THEN 1264 DISCH_THEN(fn th => MP_TAC th THEN MP_TAC th) THEN 1265 DISCH_THEN(fn th => ASM_REWRITE_TAC[] THEN ASSUME_TAC th) THEN 1266 ASM_REWRITE_TAC[] THEN 1267 REWRITE_TAC[POLY_ENTIRE, DE_MORGAN_THM] THEN STRIP_TAC THEN 1268 UNDISCH_TAC (Term`poly p = poly (q * d)`) THEN 1269 DISCH_THEN(SUBST_ALL_TAC o SYM) THEN 1270 ASM_REWRITE_TAC[rsquarefree, ORDER_ROOT] THEN 1271 CONJ_TAC THEN GEN_TAC THEN COND_CASES_TAC THEN ASM_SIMP_TAC real_ac_ss []); 1272 1273(* ------------------------------------------------------------------------- *) 1274(* Normalization of a polynomial. *) 1275(* ------------------------------------------------------------------------- *) 1276 1277val normalize = new_recursive_definition list_Axiom "normalize" 1278 (Term`(normalize [] = []) /\ 1279 (normalize (CONS h t) = (if (normalize t = []) then 1280 if (h = &0) then [] else [h] 1281 else CONS h (normalize t)))`); 1282 1283val POLY_NORMALIZE = store_thm("POLY_NORMALIZE", 1284 (Term`!p. poly (normalize p) = poly p`), 1285 LIST_INDUCT_TAC THEN REWRITE_TAC[normalize, poly] THEN 1286 ASM_CASES_TAC (Term`h = &0`) THEN ASM_REWRITE_TAC[] THEN 1287 COND_CASES_TAC THEN ASM_REWRITE_TAC[poly, FUN_EQ_THM] THEN 1288 UNDISCH_TAC (Term`poly (normalize t) = poly t`) THEN 1289 DISCH_THEN(SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC[poly] THEN 1290 REWRITE_TAC[REAL_MUL_RZERO, REAL_ADD_LID]); 1291 1292(* ------------------------------------------------------------------------- *) 1293(* The degree of a polynomial. *) 1294(* ------------------------------------------------------------------------- *) 1295 1296val degree = new_definition ("degree", 1297 (Term`degree p = PRE(LENGTH(normalize p))`)); 1298 1299val DEGREE_ZERO = store_thm("DEGREE_ZERO", 1300 (Term`!p. (poly p = poly []) ==> (degree p = 0)`), 1301 REPEAT STRIP_TAC THEN REWRITE_TAC[degree] THEN 1302 SUBGOAL_THEN (Term`normalize p = []`) SUBST1_TAC THENL 1303 [POP_ASSUM MP_TAC THEN SPEC_TAC((Term`p:real list`),(Term`p:real list`)) THEN 1304 REWRITE_TAC[POLY_ZERO] THEN 1305 LIST_INDUCT_TAC THEN REWRITE_TAC[normalize, FORALL] THEN 1306 STRIP_TAC THEN ASM_REWRITE_TAC[] THEN 1307 SUBGOAL_THEN (Term`normalize t = []`) (fn th => REWRITE_TAC[th]) THEN 1308 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[], 1309 REWRITE_TAC[LENGTH, PRE]]); 1310 1311(* ------------------------------------------------------------------------- *) 1312(* Tidier versions of finiteness of roots. *) 1313(* ------------------------------------------------------------------------- *) 1314 1315val POLY_ROOTS_FINITE_SET = store_thm("POLY_ROOTS_FINITE_SET", 1316 (Term`!p. ~(poly p = poly []) ==> FINITE {x | poly p x = &0}`), 1317 GEN_TAC THEN REWRITE_TAC[POLY_ROOTS_FINITE] THEN 1318 DISCH_THEN(X_CHOOSE_THEN (Term`N:num`) MP_TAC) THEN 1319 DISCH_THEN(X_CHOOSE_THEN (Term`i:num->real`) ASSUME_TAC) THEN 1320 MATCH_MP_TAC FINITE_SUBSET THEN 1321 EXISTS_TAC (Term`{x:real | ?n:num. n < N /\ (x = i n)}`) THEN 1322 CONJ_TAC THENL 1323 [SPEC_TAC((Term`N:num`),(Term`N:num`)) THEN POP_ASSUM_LIST(K ALL_TAC) THEN 1324 INDUCT_TAC THENL 1325 [SUBGOAL_THEN (Term`{x:real | ?n:num. n < 0 /\ (x = i n)} = {}`) 1326 (fn th => REWRITE_TAC[th, FINITE_RULES]) THEN 1327 SIMP_TAC bool_ss [GSPEC_DEF, EMPTY_DEF, pairTheory.CLOSED_PAIR_EQ, 1328 NOT_LESS, EQT_ELIM (ARITH_CONV (Term`!n:num. ~(n < 0)`))], 1329 SUBGOAL_THEN (Term`{x:real | ?n. n < SUC N /\ (x = i n)} = 1330 (i N) INSERT {x:real | ?n:num. n < N /\ (x = i n)}`) 1331 SUBST1_TAC THENL 1332 [SIMP_TAC bool_ss [LT, EXTENSION, IN_INSERT, SPECIFICATION, 1333 GSPEC_DEF,pairTheory.CLOSED_PAIR_EQ] 1334 THEN MESON_TAC[], 1335 MATCH_MP_TAC(CONJUNCT2 FINITE_RULES) THEN ASM_REWRITE_TAC[]]], 1336 ASM_SIMP_TAC bool_ss [SUBSET_DEF, SPECIFICATION, GSPEC_DEF, 1337 pairTheory.CLOSED_PAIR_EQ] 1338 THEN ASM_MESON_TAC[]]); 1339 1340(* ------------------------------------------------------------------------- *) 1341(* Crude bound for polynomial. *) 1342(* ------------------------------------------------------------------------- *) 1343 1344val POLY_MONO = store_thm("POLY_MONO", 1345 (Term`!x k p. abs(x) <= k ==> abs(poly p x) <= poly (MAP abs p) k`), 1346 GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN 1347 DISCH_TAC THEN LIST_INDUCT_TAC THEN 1348 REWRITE_TAC[poly, REAL_LE_REFL, MAP, REAL_ABS_0] THEN 1349 MATCH_MP_TAC REAL_LE_TRANS THEN 1350 EXISTS_TAC (Term`abs(h) + abs(x * poly t x)`) THEN 1351 REWRITE_TAC[REAL_ABS_TRIANGLE, REAL_LE_LADD] THEN 1352 REWRITE_TAC[REAL_ABS_MUL] THEN 1353 MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_REWRITE_TAC[REAL_ABS_POS]); 1354 1355(* ------------------------------------------------------------------------- *) 1356(* Conversions to perform operations if coefficients are rational constants. *) 1357(* ------------------------------------------------------------------------- *) 1358 1359(* 1360val POLY_DIFF_CONV = 1361 let 1362 val aux_conv0 = GEN_REWRITE_CONV I [CONJUNCT1 poly_diff_aux] 1363 val aux_conv1 = GEN_REWRITE_CONV I [CONJUNCT2 poly_diff_aux] 1364 val diff_conv0 = GEN_REWRITE_CONV I (butlast (CONJUNCTS POLY_DIFF_CLAUSES)) 1365 val diff_conv1 = GEN_REWRITE_CONV I [last (CONJUNCTS POLY_DIFF_CLAUSES)] 1366 fun POLY_DIFF_AUX_CONV tm = 1367 (aux_conv0 ORELSEC 1368 (aux_conv1 THENC 1369 LAND_CONV REAL_RAT_MUL_CONV THENC 1370 RAND_CONV (LAND_CONV NUM_SUC_CONV THENC POLY_DIFF_AUX_CONV))) tm 1371 in 1372 diff_conv0 ORELSEC (diff_conv1 THENC POLY_DIFF_AUX_CONV) 1373 end; 1374 1375val POLY_CMUL_CONV = 1376 let cmul_conv0 = GEN_REWRITE_CONV I [CONJUNCT1 poly_cmul] 1377 and cmul_conv1 = GEN_REWRITE_CONV I [CONJUNCT2 poly_cmul] in 1378 let rec POLY_CMUL_CONV tm = 1379 (cmul_conv0 ORELSEC 1380 (cmul_conv1 THENC 1381 LAND_CONV REAL_RAT_MUL_CONV THENC 1382 RAND_CONV POLY_CMUL_CONV)) tm in 1383 POLY_CMUL_CONV; 1384 1385val POLY_ADD_CONV = 1386 let add_conv0 = GEN_REWRITE_CONV I (butlast (CONJUNCTS POLY_ADD_CLAUSES)) 1387 and add_conv1 = GEN_REWRITE_CONV I [last (CONJUNCTS POLY_ADD_CLAUSES)] in 1388 let rec POLY_ADD_CONV tm = 1389 (add_conv0 ORELSEC 1390 (add_conv1 THENC 1391 LAND_CONV REAL_RAT_ADD_CONV THENC 1392 RAND_CONV POLY_ADD_CONV)) tm in 1393 POLY_ADD_CONV; 1394 1395val POLY_MUL_CONV = 1396 let mul_conv0 = GEN_REWRITE_CONV I [CONJUNCT1 POLY_MUL_CLAUSES] 1397 and mul_conv1 = GEN_REWRITE_CONV I [CONJUNCT1(CONJUNCT2 POLY_MUL_CLAUSES)] 1398 and mul_conv2 = GEN_REWRITE_CONV I [CONJUNCT2(CONJUNCT2 POLY_MUL_CLAUSES)] in 1399 let rec POLY_MUL_CONV tm = 1400 (mul_conv0 ORELSEC 1401 (mul_conv1 THENC POLY_CMUL_CONV) ORELSEC 1402 (mul_conv2 THENC 1403 LAND_CONV POLY_CMUL_CONV THENC 1404 RAND_CONV(RAND_CONV POLY_MUL_CONV) THENC 1405 POLY_ADD_CONV)) tm in 1406 POLY_MUL_CONV; 1407 1408val POLY_NORMALIZE_CONV = 1409 let pth = prove 1410 ((Term`normalize (CONS h t) = 1411 (\n. (n = []) => (h = &0) => [] | [h] | CONS h n) (normalize t)`), 1412 REWRITE_TAC[normalize]) in 1413 let norm_conv0 = GEN_REWRITE_CONV I [CONJUNCT1 normalize] 1414 and norm_conv1 = GEN_REWRITE_CONV I [pth] 1415 and norm_conv2 = GEN_REWRITE_CONV DEPTH_CONV 1416 [COND_CLAUSES, NOT_CONS_NIL, EQT_INTRO(SPEC_ALL EQ_REFL)] in 1417 let rec POLY_NORMALIZE_CONV tm = 1418 (norm_conv0 ORELSEC 1419 (norm_conv1 THENC 1420 RAND_CONV POLY_NORMALIZE_CONV THENC 1421 BETA_CONV THENC 1422 RATOR_CONV(RAND_CONV(RATOR_CONV(LAND_CONV REAL_RAT_EQ_CONV))) THENC 1423 norm_conv2)) tm in 1424 POLY_NORMALIZE_CONV; 1425*) 1426 1427val _ = export_theory (); 1428