override_interface ("-->",`(tends_num_real)`);;
prioritize_real();;

(* ---------------------------------------------------------------------- *)
(*  properites of num sequences                                           *)
(* ---------------------------------------------------------------------- *)

let LIM_INV_1N = 
prove_by_refinement( `(\n. &1 / &n) --> &0`,
(* {{{ Proof *) [ REWRITE_TAC[SEQ;real_sub;REAL_ADD_RID;REAL_NEG_0;real_gt;real_ge;GT;GE]; REPEAT STRIP_TAC; MP_TAC (ISPEC `&2 / e` REAL_ARCH_SIMPLE); STRIP_TAC; EXISTS_TAC `n`; REPEAT STRIP_TAC; CLAIM `&0 < &2 / e`; ASM_MESON_TAC[REAL_LT_RDIV_0;REAL_ARITH `&0 < &2`]; STRIP_TAC; CLAIM `&0 < &n`; ASM_MESON_TAC[REAL_LTE_TRANS;REAL_LE]; STRIP_TAC; CLAIM `&0 < &n'`; ASM_MESON_TAC[REAL_LTE_TRANS;REAL_LE]; STRIP_TAC; CLAIM `~(&n' = &0)`; ASM_MESON_TAC[REAL_LT_IMP_NZ]; STRIP_TAC; ASM_SIMP_TAC[ABS_DIV]; REWRITE_TAC[REAL_ABS_NUM]; ASM_SIMP_TAC[REAL_LT_LDIV_EQ]; CLAIM `&2 <= e * &n`; ASM_MESON_TAC[REAL_LE_LDIV_EQ;REAL_MUL_SYM]; STRIP_TAC; CLAIM `e * &n <= e * &n'`; MATCH_MP_TAC REAL_LE_LMUL; ASM_MESON_TAC [REAL_LT_LE;REAL_LE]; STRIP_TAC; ASM_MESON_TAC[REAL_LTE_TRANS;REAL_LE_TRANS;REAL_ARITH `&1 < &2`]; ]);;
(* }}} *)
let LIM_INV_CONST = 
prove_by_refinement( `!c. (\n. c / &n) --> &0`,
(* {{{ Proof *) [ ONCE_REWRITE_TAC[REAL_ARITH `c / &n = c * &1 / &n`]; STRIP_TAC; CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV[REAL_ARITH `&0 = c * &0`])); MATCH_MP_TAC SEQ_MUL; CONJ_TAC THENL [MATCH_ACCEPT_TAC SEQ_CONST;MATCH_ACCEPT_TAC LIM_INV_1N]; ]);;
(* }}} *)
let LIM_INV_1NP = 
prove_by_refinement( `!c k. 0 < k ==> (\n. c / &n pow k) --> &0`,
(* {{{ Proof *) [ STRIP_TAC; INDUCT_TAC; REWRITE_TAC[ARITH_RULE `~(0 < 0)`]; REWRITE_TAC[real_pow;REAL_DIV_DISTRIB_R]; STRIP_TAC; CASES_ON `k = 0`; ASM_REWRITE_TAC[real_pow;GSYM REAL_DIV_DISTRIB_R;REAL_MUL_RID]; MATCH_ACCEPT_TAC LIM_INV_CONST; CLAIM `(\n. c / &n pow k) --> &0`; FIRST_ASSUM MATCH_MP_TAC; EVERY_ASSUM MP_TAC THEN ARITH_TAC; STRIP_TAC; ONCE_REWRITE_TAC[REAL_ARITH `&0 = &0 * &0`]; MATCH_MP_TAC SEQ_MUL; CONJ_TAC THENL [MATCH_ACCEPT_TAC LIM_INV_1N;FIRST_ASSUM MATCH_ACCEPT_TAC]; ]);;
(* }}} *)
let LIM_INV_CON = 
prove_by_refinement( `!c d k. 0 < k ==> (\n. c / (d * &n pow k)) --> &0`,
(* {{{ Proof *) [ REWRITE_TAC[REAL_DIV_DISTRIB_R]; REPEAT STRIP_TAC; ONCE_REWRITE_TAC[REAL_ARITH `&0 = (&1 / d) * &0`]; MATCH_MP_TAC SEQ_MUL; CONJ_TAC; MATCH_ACCEPT_TAC SEQ_CONST; POP_ASSUM MP_TAC THEN MATCH_ACCEPT_TAC LIM_INV_1NP; ]);;
(* }}} *)
let LIM_NN = 
prove_by_refinement( `(\n. &n / &n) --> &1`,
(* {{{ Proof *) [ REWRITE_TAC[SEQ]; REPEAT STRIP_TAC; EXISTS_TAC `1`; REWRITE_TAC[GT;GE]; REPEAT STRIP_TAC; CLAIM `~(&n = &0)`; MATCH_MP_TAC REAL_LT_IMP_NZ; ASM_MESON_TAC[REAL_LE;REAL_ARITH `&0 < &1`;REAL_LTE_TRANS]; STRIP_TAC; ASM_SIMP_TAC[REAL_DIV_REFL;real_sub;REAL_ADD_RINV;ABS_0]; ]);;
(* }}} *)
let LIM_NNC = 
prove_by_refinement( `~(k = &0) ==> (\n. (k * &n) / (k * &n)) --> &1`,
(* {{{ Proof *) [ REWRITE_TAC[REAL_DIV_DISTRIB_2]; ONCE_REWRITE_TAC[REAL_ARITH `&1 = &1 * &1`]; STRIP_TAC; MATCH_MP_TAC SEQ_MUL; CONJ_TAC; ASM_SIMP_TAC[real_div;REAL_MUL_RINV]; MATCH_ACCEPT_TAC SEQ_CONST; MATCH_ACCEPT_TAC LIM_NN; ]);;
(* }}} *)
let LIM_MONO = 
prove_by_refinement( `!c d a b. ~(d = &0) /\ a < b ==> (\n. (c * &n pow a) / (d * &n pow b)) --> &0`,
(* {{{ Proof *) [ STRIP_TAC THEN STRIP_TAC; INDUCT_TAC; REPEAT STRIP_TAC; REWRITE_TAC[real_pow;REAL_MUL_RID]; POP_ASSUM MP_TAC THEN MATCH_ACCEPT_TAC LIM_INV_CON; REPEAT STRIP_TAC; REWRITE_TAC[real_pow]; CLAIM `(b = SUC(PRE b))`; POP_ASSUM MP_TAC THEN ARITH_TAC; STRIP_TAC; ONCE_ASM_REWRITE_TAC[]; REWRITE_TAC[real_pow]; ONCE_REWRITE_TAC[ARITH_RULE `a * b * c = b * a * c`]; ONCE_REWRITE_TAC[REAL_DIV_DISTRIB_2]; ONCE_REWRITE_TAC[REAL_ARITH `&0 = &1 * &0`]; MATCH_MP_TAC SEQ_MUL; CONJ_TAC; MATCH_ACCEPT_TAC LIM_NN; FIRST_ASSUM MATCH_MP_TAC; ASM_REWRITE_TAC[]; LABEL_ALL_TAC; USE_THEN "Z-1" MP_TAC; ARITH_TAC; ]);;
(* }}} *)
let LIM_POLY_LT = 
prove_by_refinement( `!p k. LENGTH p <= k ==> (\n. poly p (&n) / &n pow k) --> &0`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; REWRITE_TAC[poly;LENGTH]; REPEAT STRIP_TAC; REWRITE_TAC[REAL_DIV_LZERO;SEQ_CONST]; REWRITE_TAC[poly;LENGTH]; REPEAT STRIP_TAC; CLAIM `~(k = 0)`; POP_ASSUM MP_TAC THEN ARITH_TAC; STRIP_TAC; LABEL_ALL_TAC; CLAIM `LENGTH t <= PRE k`; USE_THEN "Z-1" MP_TAC THEN ARITH_TAC; DISCH_THEN (fun x -> FIRST_ASSUM (fun y -> MP_TAC (MATCH_MP y x))); STRIP_TAC; REWRITE_TAC[REAL_DIV_ADD_DISTRIB]; ONCE_REWRITE_TAC[REAL_ARITH `&0 = &0 + &0`]; MATCH_MP_TAC SEQ_ADD; CONJ_TAC; ONCE_REWRITE_TAC[ARITH_RULE `n pow k = &1 * n pow k`]; MATCH_MP_TAC LIM_INV_CON; USE_THEN "Z-0" MP_TAC THEN ARITH_TAC; CLAIM `k = SUC (PRE k)`; USE_THEN "Z-0" MP_TAC THEN ARITH_TAC; STRIP_TAC; ONCE_ASM_REWRITE_TAC[]; REWRITE_TAC[real_pow]; REWRITE_TAC[REAL_DIV_DISTRIB_2]; ONCE_REWRITE_TAC[REAL_ARITH `&0 = &1 * &0`]; MATCH_MP_TAC SEQ_MUL; CONJ_TAC; MATCH_ACCEPT_TAC LIM_NN; FIRST_ASSUM MATCH_MP_TAC; USE_THEN "Z-1" MP_TAC THEN ARITH_TAC; ]);;
(* }}} *)
let LIM_POLY = 
prove_by_refinement( `!p. (0 < LENGTH p /\ ~(LAST p = &0)) ==> (\n. poly p (&n) / (LAST p * &n pow PRE (LENGTH p))) --> &1`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; REWRITE_TAC[LENGTH;LT]; ASM_REWRITE_TAC[LENGTH;poly]; REPEAT STRIP_TAC; CASES_ON `t = []`; ASM_REWRITE_TAC[PRE;real_pow;REAL_POW_1;LAST;poly;REAL_MUL_RZERO;REAL_ADD_RID;LENGTH;REAL_DIV_DISTRIB_L]; CLAIM `~(h = &0)`; ASM_MESON_TAC[LAST]; STRIP_TAC; CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV[REAL_ARITH `&1 = &1 * &1`])); MATCH_MP_TAC SEQ_MUL; CONJ_TAC; ASM_SIMP_TAC[DIV_ID]; MATCH_ACCEPT_TAC SEQ_CONST; ASM_SIMP_TAC[DIV_ID;REAL_10]; MATCH_ACCEPT_TAC SEQ_CONST; CLAIM `LAST (CONS h t) = LAST t`; ASM_REWRITE_TAC[LAST]; STRIP_TAC; ASM_REWRITE_TAC[LAST;PRE]; REWRITE_TAC[REAL_DIV_ADD_DISTRIB]; ONCE_REWRITE_TAC [REAL_ARITH `&1 = &0 + &1`]; MATCH_MP_TAC SEQ_ADD; CLAIM `~(LENGTH t = 0)`; ASM_MESON_TAC[LENGTH_0]; STRIP_TAC; CONJ_TAC; MATCH_MP_TAC LIM_INV_CON; POP_ASSUM MP_TAC THEN ARITH_TAC; CLAIM `(LENGTH t = SUC (PRE (LENGTH t)))`; POP_ASSUM MP_TAC THEN ARITH_TAC; STRIP_TAC; ONCE_ASM_REWRITE_TAC[]; REWRITE_TAC[real_pow]; ONCE_REWRITE_TAC[ARITH_RULE `a * b * c = b * a * c`]; REWRITE_TAC[REAL_DIV_DISTRIB_2]; ONCE_REWRITE_TAC [REAL_ARITH `&1 = &1 * &1`]; MATCH_MP_TAC SEQ_MUL; CONJ_TAC; MATCH_ACCEPT_TAC LIM_NN; FIRST_ASSUM MATCH_MP_TAC; CONJ_TAC; LABEL_ALL_TAC; USE_THEN "Z-1" MP_TAC THEN ARITH_TAC; ASM_MESON_TAC[]; ]);;
(* }}} *)
let mono_inc = new_definition(
  `mono_inc (f:num -> real) = !(m:num) n. m <= n ==> f m <= f n`);;
let mono_dec = new_definition(
  `mono_dec (f:num -> real) = !(m:num) n. m <= n ==> f n <= f m`);;
let mono_inc_dec = 
prove_by_refinement( `!f. mono f <=> mono_inc f \/ mono_dec f`,
(* {{{ Proof *) [ REWRITE_TAC[mono_inc;mono_dec;mono;real_ge] ]);;
(* }}} *)
let mono_inc_pow = 
prove_by_refinement( `!k. mono_inc (\n. &n pow k)`,
(* {{{ Proof *) [ REWRITE_TAC[mono_inc]; INDUCT_TAC THEN REWRITE_TAC[real_pow;REAL_LE_REFL]; GEN_TAC THEN GEN_TAC; DISCH_THEN (fun x -> (RULE_ASSUM_TAC (fun y -> MATCH_MP y x)) THEN ASSUME_TAC x); MATCH_MP_TAC REAL_LE_MUL2; REPEAT STRIP_TAC; MATCH_ACCEPT_TAC REAL_NUM_LE_0; ASM_REWRITE_TAC[REAL_LE]; MATCH_MP_TAC REAL_POW_LE; MATCH_ACCEPT_TAC REAL_NUM_LE_0; FIRST_ASSUM MATCH_ACCEPT_TAC; ]);;
(* }}} *)
let mono_inc_pow_const = 
prove_by_refinement( `!k c. &0 < c ==> mono_inc (\n. c * &n pow k)`,
(* {{{ Proof *) [ REWRITE_TAC[mono_inc]; REPEAT STRIP_TAC; MATCH_MP_TAC REAL_LE_MUL2; REPEAT STRIP_TAC; ASM_MESON_TAC[REAL_LT_LE]; REAL_ARITH_TAC; MATCH_MP_TAC REAL_POW_LE; MATCH_ACCEPT_TAC REAL_NUM_LE_0; ASM_MESON_TAC[mono_inc_pow;mono_inc] ]);;
(* }}} *) (* ---------------------------------------------------------------------- *) (* Unbounded sequences *) (* ---------------------------------------------------------------------- *)
let mono_unbounded_above = new_definition(
 `mono_unbounded_above (f:num -> real) = !c. ?N. !n. N <= n ==> c < f n`);;
let mono_unbounded_below = new_definition(
 `mono_unbounded_below (f:num -> real) = !c. ?N. !n. N <= n ==> f n < c`);;
let mono_unbounded_above_pos = 
prove_by_refinement( `mono_unbounded_above (f:num -> real) = !c. &0 <= c ==> ?N. !n. N <= n ==> c < f n`,
(* {{{ Proof *) [ REWRITE_TAC[mono_unbounded_above]; EQ_TAC THENL [ASM_MESON_TAC[];ALL_TAC]; REPEAT STRIP_TAC; POP_ASSUM (ASSUME_TAC o ISPEC `abs c`); POP_ASSUM (MP_TAC o (C MATCH_MP) (ISPEC `c:real` ABS_POS)); STRIP_TAC; EXISTS_TAC `N`; GEN_TAC; DISCH_THEN (fun x -> POP_ASSUM (fun y -> ASSUME_TAC (MATCH_MP y x))); ASM_MESON_TAC[ABS_LE;REAL_LET_TRANS]; ]);;
(* }}} *)
let mono_unbounded_below_neg = 
prove_by_refinement( `mono_unbounded_below (f:num -> real) = !c. c <= &0 ==> ?N. !n. N <= n ==> f n < c`,
(* {{{ Proof *) [ REWRITE_TAC[mono_unbounded_below]; EQ_TAC THENL [ASM_MESON_TAC[];ALL_TAC]; REPEAT STRIP_TAC; POP_ASSUM (ASSUME_TAC o ISPEC `-- (abs c)`); POP_ASSUM (MP_TAC o (C MATCH_MP) (ISPEC `c:real` NEG_ABS)); STRIP_TAC; EXISTS_TAC `N`; GEN_TAC; DISCH_THEN (fun x -> POP_ASSUM (fun y -> ASSUME_TAC (MATCH_MP y x))); POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ]);;
(* }}} *)
let mua_quotient_limit = 
prove_by_refinement( `!k f g. &0 < k /\ (\n. f n / g n) --> k /\ mono_unbounded_above g ==> mono_unbounded_above f`,
(* {{{ Proof *) [ REWRITE_TAC[SEQ;mono_unbounded_above_pos;AND_IMP_THM]; REPEAT GEN_TAC; STRIP_TAC; CLAIM `&0 < k / &2`; POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; DISCH_THEN (fun x -> DISCH_THEN (fun y -> (ASSUME_TAC (MATCH_MP (ISPEC `k / &2` y) x)))); POP_ASSUM (X_CHOOSE_TAC `M:num`); STRIP_TAC; X_GEN_TAC `d:real`; STRIP_TAC; CLAIM `&0 <= &2 * d / k`; MATCH_MP_TAC REAL_LE_MUL; CONJ_TAC THENL [REAL_ARITH_TAC;ALL_TAC]; MATCH_MP_TAC REAL_LE_DIV; CONJ_TAC THENL [FIRST_ASSUM MATCH_ACCEPT_TAC;ASM_MESON_TAC[REAL_LT_LE]]; STRIP_TAC; LABEL_ALL_TAC; MOVE_TO_FRONT "Z-2";
POP_ASSUM (fun x -> USE_THEN "Z-0" (fun y -> MP_TAC (MATCH_MP x y))); DISCH_THEN (X_CHOOSE_TAC `K:num`); EXISTS_TAC `nmax M K`; REPEAT STRIP_TAC; CLAIM `M <= n /\ K <= (n:num)`; POP_ASSUM MP_TAC THEN REWRITE_TAC[nmax] THEN COND_CASES_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC; STRIP_TAC; RULE_ASSUM_TAC (REWRITE_RULE[GE]); FIRST_X_ASSUM (fun x -> FIRST_X_ASSUM (fun y -> ASSUME_TAC (MATCH_MP y x))); FIRST_X_ASSUM (fun x -> FIRST_X_ASSUM (fun y -> ASSUME_TAC (MATCH_MP y x))); RULE_ASSUM_TAC (REWRITE_RULE[real_div]); CASES_ON `k <= f n * inv (g n)`; MATCH_MP_TAC (prove(`d <= &2 * d /\ &2 * d < k * (g n) /\ k * (g n) <= f n ==> d < f n`,MESON_TAC !REAL_REWRITES)); REPEAT STRIP_TAC; USE_THEN "Z-1" MP_TAC THEN REAL_ARITH_TAC; FIRST_ASSUM (fun x -> ASSUME_TAC (MATCH_MP (REWRITE_RULE[AND_IMP_THM] REAL_LT_LMUL) x)); LABEL_ALL_TAC; POP_ASSUM (fun y -> USE_THEN "Z-6" (fun x -> ASSUME_TAC (MATCH_MP y x))); CLAIM `k * &2 * d * inv k = (k * inv k) * &2 * d`; REAL_ARITH_TAC; CLAIM `k * inv k = &1`; ASM_MESON_TAC[REAL_MUL_RINV;REAL_LT_NZ]; STRIP_TAC; ASM_REWRITE_TAC[REAL_MUL_LID]; ASM_MESON_TAC[]; (* *) MATCH_MP_TAC REAL_LE_RCANCEL_IMP; EXISTS_TAC `inv (g n)`; REWRITE_TAC[GSYM REAL_MUL_ASSOC]; CLAIM `&0 < inv (g n)`; CLAIM `&0 < inv k`; MATCH_MP_TAC REAL_LT_INV THEN FIRST_ASSUM MATCH_ACCEPT_TAC; STRIP_TAC; CLAIM `&0 < g n`; ASM_MESON_TAC !REAL_REWRITES; STRIP_TAC; ASM_MESON_TAC[REAL_LT_INV]; STRIP_TAC; ASM_REWRITE_TAC[]; CLAIM `g n * inv (g n) = &1`; ASM_MESON_TAC[REAL_MUL_RINV;REAL_LT_NZ;REAL_LT_INV_EQ]; DISCH_THEN SUBST1_TAC; REWRITE_TAC[REAL_MUL_RID]; FIRST_ASSUM MATCH_ACCEPT_TAC; (* *) RULE_ASSUM_TAC (REWRITE_RULE[REAL_NOT_LE]); CLAIM `f n * inv (g n) - k < &0`; POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; STRIP_TAC; CLAIM `abs (f n * inv (g n) - k) = k - (f n * inv (g n))`; POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; DISCH_THEN (RULE_ASSUM_TAC o REWRITE_RULE o list); CLAIM `k * inv(&2) < f n * inv (g n)`; LABEL_ALL_TAC; USE_THEN "Z-5" MP_TAC THEN REAL_ARITH_TAC; STRIP_TAC; CLAIM `k * g n < &2 * f n`; CLAIM `&0 < g n`; LABEL_ALL_TAC; MATCH_MP_TAC REAL_LET_TRANS; EXISTS_TAC `&2 * d * inv k`; CONJ_TAC THEN FIRST_ASSUM MATCH_ACCEPT_TAC; STRIP_TAC; MATCH_MP_TAC REAL_LT_LCANCEL_IMP; EXISTS_TAC `inv(&2)`; CONJ_TAC THENL [REAL_ARITH_TAC;ALL_TAC]; REWRITE_TAC[ARITH_RULE `inv(&2) * &2 = &1`;REAL_MUL_LID;REAL_MUL_ASSOC]; MATCH_MP_TAC REAL_LT_LCANCEL_IMP; EXISTS_TAC `inv(g n)`; CONJ_TAC; ASM_MESON_TAC[REAL_LT_INV]; ONCE_REWRITE_TAC[ARITH_RULE `a * (b * c) * d = c * b * (d * a)`]; CLAIM `g n * inv (g n) = &1`; POP_ASSUM MP_TAC THEN ASM_MESON_TAC[REAL_MUL_RINV;REAL_POS_NZ]; DISCH_THEN SUBST1_TAC; ASM_MESON_TAC[REAL_MUL_RID;REAL_MUL_SYM]; STRIP_TAC; CLAIM `&2 * d < k * g n`; MATCH_MP_TAC REAL_LT_RCANCEL_IMP; EXISTS_TAC `inv k`; STRIP_TAC; ASM_MESON_TAC[REAL_LT_INV]; MATCH_MP_TAC REAL_LTE_TRANS; EXISTS_TAC `g n`; CONJ_TAC; REWRITE_TAC[GSYM REAL_MUL_ASSOC]; FIRST_ASSUM MATCH_ACCEPT_TAC; LABEL_ALL_TAC; ONCE_REWRITE_TAC[ARITH_RULE `(a * b) * c = b * (a * c)`]; CLAIM `k * inv k = &1`; ASM_MESON_TAC[REAL_MUL_RINV;REAL_POS_NZ]; DISCH_THEN SUBST1_TAC; REAL_ARITH_TAC; STRIP_TAC; CLAIM `&2 * d < &2 * f n`; POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; REAL_ARITH_TAC; ]);; (* }}} *)
let mua_neg = 
prove_by_refinement( `!f. mono_unbounded_above f = mono_unbounded_below (\n. -- (f n))`,
(* {{{ Proof *) [ MESON_TAC[mono_unbounded_above;mono_unbounded_below;REAL_ARITH `x < y ==> --y < -- x`;REAL_ARITH `-- (-- x) = x`]; ]);;
(* }}} *)
let mua_neg2 = 
prove_by_refinement( `!f. mono_unbounded_below f = mono_unbounded_above (\n. -- (f n))`,
(* {{{ Proof *) [ MESON_TAC[mono_unbounded_above;mono_unbounded_below;REAL_ARITH `x < y ==> --y < -- x`;REAL_ARITH `-- (-- x) = x`]; ]);;
(* }}} *)
let mua_quotient_limit_neg = 
prove_by_refinement( `!k f g. &0 < k /\ (\n. f n / g n) --> k /\ mono_unbounded_below g ==> mono_unbounded_below f`,
(* {{{ Proof *) [ REWRITE_TAC[mua_neg2]; REPEAT STRIP_TAC; MATCH_MP_TAC (mua_quotient_limit); EXISTS_TAC `k`; EXISTS_TAC `\n. -- g n`; ASM_REWRITE_TAC[]; POP_ASSUM (fun x -> ALL_TAC); POP_ASSUM MP_TAC; REWRITE_TAC[SEQ]; DISCH_THEN (fun x -> REPEAT STRIP_TAC THEN MP_TAC x); DISCH_THEN (MP_TAC o ISPEC `e:real`); ANTS_TAC; FIRST_ASSUM MATCH_ACCEPT_TAC; STRIP_TAC; EXISTS_TAC `N`; REPEAT STRIP_TAC; REWRITE_TAC[real_div;REAL_NEG_MUL2;REAL_INV_NEG]; ASM_MESON_TAC[real_div]; ]);;
(* }}} *) (* ---------------------------------------------------------------------- *) (* Polynomial properties *) (* ---------------------------------------------------------------------- *)
let normal = new_definition(
 `normal p <=> ((normalize p = p) /\ ~(p = []))`);;
let nonconstant = new_definition(
 `nonconstant p <=> normal p /\ (!x. ~(p = [x]))`);;
let NORMALIZE_SING = 
prove_by_refinement( `!x. (normalize [x] = [x]) <=> ~(x = &0)`,
(* {{{ Proof *) [ MESON_TAC[NOT_CONS_NIL;normalize]; ]);;
(* }}} *)
let NORMALIZE_PAIR = 
prove_by_refinement( `!x y. ~(y = &0) <=> (normalize [x; y] = [x; y])`,
(* {{{ Proof *) [ REWRITE_TAC[normalize;NOT_CONS_NIL]; REPEAT GEN_TAC; COND_CASES_TAC; CLAIM `y = &0`; ASM_MESON_TAC !LIST_REWRITES; DISCH_THEN SUBST1_TAC; ASM_MESON_TAC !LIST_REWRITES; ASM_MESON_TAC !LIST_REWRITES; ]);;
(* }}} *)
let POLY_NORMALIZE = 
prove (`!p. poly (normalize p) = poly p`,
(* {{{ Proof *) LIST_INDUCT_TAC THEN REWRITE_TAC[normalize; poly] THEN ASM_CASES_TAC `h = &0` THEN ASM_REWRITE_TAC[] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[poly; FUN_EQ_THM] THEN UNDISCH_TAC `poly (normalize t) = poly t` THEN DISCH_THEN(SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC[poly] THEN REWRITE_TAC[REAL_MUL_RZERO; REAL_ADD_LID]);;
(* }}} *)
let NORMAL_CONS = 
prove_by_refinement( `!h t. normal t ==> normal (CONS h t)`,
(* {{{ Proof *) [ REWRITE_TAC[normal;normalize]; REPEAT STRIP_TAC; ASM_REWRITE_TAC[]; ASM_MESON_TAC[NOT_CONS_NIL]; ]);;
(* }}} *)
let NORMAL_TAIL = 
prove_by_refinement( `!h t. ~(t = []) /\ normal (CONS h t) ==> normal t`,
(* {{{ Proof *) [ REWRITE_TAC[normal;normalize]; REPEAT STRIP_TAC THENL [ALL_TAC;ASM_MESON_TAC[]]; CASES_ON `normalize t = []`; ASM_MESON_TAC[NOT_CONS_NIL;CONS_11]; ASM_MESON_TAC[NOT_CONS_NIL;CONS_11]; ]);;
(* }}} *)
let NORMAL_LAST_NONZERO = 
prove_by_refinement( `!p. normal p ==> ~(LAST p = &0)`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; ASM_MESON_TAC[normal]; CASES_ON `t = []`; ASM_REWRITE_TAC[normal;normalize;NOT_CONS_NIL;LAST]; MESON_TAC[NOT_CONS_NIL]; ASM_SIMP_TAC[GSYM LAST_CONS]; ASM_REWRITE_TAC[LAST;NOT_CONS_NIL;]; STRIP_TAC; FIRST_ASSUM MATCH_MP_TAC; MATCH_MP_TAC NORMAL_TAIL; ASM_MESON_TAC[]; ]);;
(* }}} *)
let NORMAL_LENGTH = 
prove_by_refinement( `!p. normal p ==> 0 < LENGTH p`,
(* {{{ Proof *) [ MESON_TAC[normal;LENGTH_0;ARITH_RULE `~(n = 0) <=> 0 < n`] ]);;
(* }}} *)
let NORMAL_LAST_LENGTH = 
prove_by_refinement( `!p. 0 < LENGTH p /\ ~(LAST p = &0) ==> normal p`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; MESON_TAC[LENGTH;LT_REFL]; STRIP_TAC; CASES_ON `t = []`; ASM_REWRITE_TAC[normal;NORMALIZE_SING;NOT_CONS_NIL;]; ASM_MESON_TAC[LAST]; MATCH_MP_TAC NORMAL_CONS; FIRST_ASSUM MATCH_MP_TAC; STRIP_TAC; ASM_MESON_TAC[LENGTH_0;ARITH_RULE `~(n = 0) <=> 0 < n`]; ASM_MESON_TAC[LAST_CONS]; ]);;
(* }}} *)
let NORMAL_ID = 
prove_by_refinement( `!p. normal p <=> 0 < LENGTH p /\ ~(LAST p = &0)`,
(* {{{ Proof *) [ MESON_TAC[NORMAL_LAST_LENGTH;NORMAL_LENGTH;NORMAL_LAST_NONZERO]; ]);;
(* }}} *)
let LIM_POLY2 = 
prove_by_refinement( `!p. normal p ==> (\n. poly p (&n) / (LAST p * &n pow (degree p))) --> &1`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; REWRITE_TAC[degree]; CLAIM `normalize p = p`; ASM_MESON_TAC[normal]; DISCH_THEN SUBST1_TAC; MATCH_MP_TAC LIM_POLY; ASM_MESON_TAC[NORMAL_ID]; ]);;
(* }}} *)
let POW_UNB = 
prove_by_refinement( `!k. 0 < k ==> mono_unbounded_above (\n. (&n) pow k)`,
(* {{{ Proof *) [ REWRITE_TAC[mono_unbounded_above]; REPEAT STRIP_TAC; MP_TAC (ISPEC `max (&1) c` REAL_ARCH_SIMPLE_LT); STRIP_TAC; EXISTS_TAC `n`; REPEAT STRIP_TAC; MATCH_MP_TAC REAL_LTE_TRANS; EXISTS_TAC `&n`; CONJ_TAC; MATCH_MP_TAC REAL_LET_TRANS; EXISTS_TAC `max (&1) c`; ASM_MESON_TAC[REAL_MAX_MAX]; MATCH_MP_TAC REAL_LE_TRANS; EXISTS_TAC `&n'`; STRIP_TAC; ASM_MESON_TAC[REAL_LE]; CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV[REAL_ARITH `x = x pow 1`])); MATCH_MP_TAC REAL_POW_MONO; STRIP_TAC; MATCH_MP_TAC REAL_LE_TRANS; EXISTS_TAC `max (&1) c`; CONJ_TAC THENL [ASM_MESON_TAC[REAL_MAX_MAX];ALL_TAC]; MATCH_MP_TAC REAL_LE_TRANS; EXISTS_TAC `&n`; ASM_MESON_TAC (!REAL_REWRITES @ [REAL_LE;REAL_LT_LE]); EVERY_ASSUM MP_TAC THEN ARITH_TAC; ]);;
(* }}} *)
let POW_UNB_CON = 
prove_by_refinement( `!k a. 0 < k /\ &0 < a ==> mono_unbounded_above (\n. a * (&n) pow k)`,
(* {{{ Proof *) [ REWRITE_TAC[mono_unbounded_above;AND_IMP_THM;]; REPEAT STRIP_TAC; LABEL_ALL_TAC; MOVE_TO_FRONT "Z-1";
POP_ASSUM (fun x -> MP_TAC (MATCH_MP POW_UNB x)); REWRITE_TAC[mono_unbounded_above]; DISCH_THEN (MP_TAC o ISPEC `inv a * c`); STRIP_TAC; EXISTS_TAC `N`; STRIP_TAC; DISCH_THEN (fun x -> POP_ASSUM (fun y -> ASSUME_TAC (MATCH_MP y x))); CLAIM `inv a * a = &1`; MATCH_MP_TAC REAL_MUL_LINV; EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC; STRIP_TAC; MATCH_MP_TAC REAL_LT_LCANCEL_IMP; EXISTS_TAC `inv a`; CONJ_TAC; ASM_MESON_TAC[REAL_LT_INV]; ASM_REWRITE_TAC[REAL_MUL_ASSOC;REAL_MUL_LID]; ]);; (* }}} *)
let POW_UNBB_CON = 
prove_by_refinement( `!k a. 0 < k /\ a < &0 ==> mono_unbounded_below (\n. a * (&n) pow k)`,
(* {{{ Proof *) [ REWRITE_TAC[mua_neg2;ARITH_RULE `--(x * y) = -- x * y`]; REPEAT STRIP_TAC; MATCH_MP_TAC POW_UNB_CON; STRIP_TAC; FIRST_ASSUM MATCH_ACCEPT_TAC; POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ]);;
(* }}} *)
let POLY_SING = 
prove_by_refinement( `!x y. poly [x] y = x`,
(* {{{ Proof *) [ REWRITE_TAC[poly]; REAL_ARITH_TAC; ]);;
(* }}} *)
let POLY_LAST_GT = 
prove_by_refinement( `!p. normal p /\ (?X. !x. X < x ==> &0 < poly p x) ==> &0 < LAST p`,
(* {{{ Proof *) [ GEN_TAC; CASES_ON `LENGTH p = 1`; RULE_ASSUM_TAC (REWRITE_RULE[LENGTH_1]); POP_ASSUM MP_TAC THEN STRIP_TAC; ASM_REWRITE_TAC[LAST_SING;POLY_SING]; REPEAT STRIP_TAC; FIRST_ASSUM MATCH_MP_TAC; EXISTS_TAC `X + &1`; REAL_ARITH_TAC; (* *) REWRITE_TAC[AND_IMP_THM;]; DISCH_THEN (fun x -> MP_TAC (MATCH_MP LIM_POLY2 x) THEN ASSUME_TAC x); REPEAT STRIP_TAC; DISJ_CASES_TAC (ISPECL [`&0`;`LAST (p:real list)`] REAL_LT_TOTAL); ASM_MESON_TAC[NORMAL_ID]; POP_ASSUM DISJ_CASES_TAC; FIRST_ASSUM MATCH_ACCEPT_TAC; (* save *) CLAIM `mono_unbounded_below (\n. LAST p * &n pow degree p)`; MATCH_MP_TAC POW_UNBB_CON; REWRITE_TAC[degree]; CONJ_TAC THENL [ALL_TAC;FIRST_ASSUM MATCH_ACCEPT_TAC]; CLAIM `normalize p = p`; ASM_MESON_TAC[normal]; DISCH_THEN SUBST1_TAC; CLAIM `~(LENGTH p = 0)`; ASM_MESON_TAC[normal;LENGTH_EQ_NIL]; LABEL_ALL_TAC; USE_THEN "Z-4" MP_TAC; ARITH_TAC; (* save *) STRIP_TAC; CLAIM `mono_unbounded_below (\n. poly p (&n))`; MATCH_MP_TAC mua_quotient_limit_neg; BETA_TAC; EXISTS_TAC `&1`; EXISTS_TAC `(\n. LAST p * &n pow degree p)`; REPEAT STRIP_TAC; REAL_ARITH_TAC; BETA_TAC; FIRST_ASSUM MATCH_ACCEPT_TAC; FIRST_ASSUM MATCH_ACCEPT_TAC; REWRITE_TAC[mono_unbounded_below]; DISCH_THEN (MP_TAC o ISPEC `&0`); STRIP_TAC; LABEL_ALL_TAC; USE_THEN "Z-3" MP_TAC; POP_ASSUM MP_TAC; POP_ASSUM_LIST (fun x -> ALL_TAC); MP_TAC (ISPEC `X:real` REAL_ARCH_SIMPLE); STRIP_TAC; DISCH_THEN (ASSUME_TAC o ISPEC `1 + nmax N n`); DISCH_THEN (ASSUME_TAC o ISPEC `&1 + &(nmax N n)`); POP_ASSUM MP_TAC THEN ANTS_TAC; REWRITE_TAC[nmax]; COND_CASES_TAC; EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC; RULE_ASSUM_TAC (REWRITE_RULE[NOT_LE;GSYM REAL_LT]); EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN ANTS_TAC; REWRITE_TAC[nmax]; ARITH_TAC; ASM_MESON_TAC[ARITH_RULE `~(x < y /\ y < x)`;GSYM REAL_OF_NUM_ADD]; ]);;
(* }}} *)
let POLY_LAST_LT = 
prove_by_refinement( `!p. normal p /\ (?X. !x. X < x ==> poly p x < &0) ==> LAST p < &0`,
(* {{{ Proof *) [ GEN_TAC; CASES_ON `LENGTH p = 1`; RULE_ASSUM_TAC (REWRITE_RULE[LENGTH_1]); POP_ASSUM MP_TAC THEN STRIP_TAC; ASM_REWRITE_TAC[LAST_SING;POLY_SING]; REPEAT STRIP_TAC; FIRST_ASSUM MATCH_MP_TAC; EXISTS_TAC `X + &1`; REAL_ARITH_TAC; (* *) REWRITE_TAC[AND_IMP_THM;]; DISCH_THEN (fun x -> MP_TAC (MATCH_MP LIM_POLY2 x) THEN ASSUME_TAC x); REPEAT STRIP_TAC; DISJ_CASES_TAC (ISPECL [`&0`;`LAST (p:real list)`] REAL_LT_TOTAL); ASM_MESON_TAC[NORMAL_ID]; POP_ASSUM DISJ_CASES_TAC THENL [ALL_TAC;FIRST_ASSUM MATCH_ACCEPT_TAC]; (* save *) CLAIM `mono_unbounded_above (\n. LAST p * &n pow degree p)`; MATCH_MP_TAC POW_UNB_CON; REWRITE_TAC[degree]; CONJ_TAC THENL [ALL_TAC;FIRST_ASSUM MATCH_ACCEPT_TAC]; CLAIM `normalize p = p`; ASM_MESON_TAC[normal]; DISCH_THEN SUBST1_TAC; CLAIM `~(LENGTH p = 0)`; ASM_MESON_TAC[normal;LENGTH_EQ_NIL]; LABEL_ALL_TAC; USE_THEN "Z-4" MP_TAC; ARITH_TAC; (* save *) STRIP_TAC; CLAIM `mono_unbounded_above (\n. poly p (&n))`; MATCH_MP_TAC mua_quotient_limit; BETA_TAC; EXISTS_TAC `&1`; EXISTS_TAC `(\n. LAST p * &n pow degree p)`; REPEAT STRIP_TAC; REAL_ARITH_TAC; BETA_TAC; FIRST_ASSUM MATCH_ACCEPT_TAC; FIRST_ASSUM MATCH_ACCEPT_TAC; REWRITE_TAC[mono_unbounded_above]; DISCH_THEN (MP_TAC o ISPEC `&0`); STRIP_TAC; LABEL_ALL_TAC; USE_THEN "Z-3" MP_TAC; POP_ASSUM MP_TAC; POP_ASSUM_LIST (fun x -> ALL_TAC); MP_TAC (ISPEC `X:real` REAL_ARCH_SIMPLE); STRIP_TAC; DISCH_THEN (ASSUME_TAC o ISPEC `1 + nmax N n`); DISCH_THEN (ASSUME_TAC o ISPEC `&1 + &(nmax N n)`); POP_ASSUM MP_TAC THEN ANTS_TAC; REWRITE_TAC[nmax]; COND_CASES_TAC; EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC; RULE_ASSUM_TAC (REWRITE_RULE[NOT_LE;GSYM REAL_LT]); EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN ANTS_TAC; REWRITE_TAC[nmax]; ARITH_TAC; ASM_MESON_TAC[ARITH_RULE `~(x < y /\ y < x)`;GSYM REAL_OF_NUM_ADD]; ]);;
(* }}} *)
let NORMALIZE_LENGTH_MONO = 
prove_by_refinement( `!l. LENGTH (normalize l) <= LENGTH l`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; MESON_TAC[normalize;LE_REFL]; REWRITE_TAC[LENGTH;normalize]; REPEAT COND_CASES_TAC THEN REWRITE_TAC[LENGTH] THEN EVERY_ASSUM MP_TAC THEN ARITH_TAC; ]);;
(* }}} *)
let DEGREE_SING = 
prove_by_refinement( `!x. (degree [x] = 0)`,
(* {{{ Proof *) [ REWRITE_TAC[degree]; STRIP_TAC; CASES_ON `x = &0`; ASM_REWRITE_TAC[normalize;LENGTH]; ARITH_TAC; CLAIM `normalize [x] = [x]`; ASM_MESON_TAC[NORMALIZE_SING]; DISCH_THEN SUBST1_TAC; REWRITE_TAC[LENGTH]; ARITH_TAC; ]);;
(* }}} *)
let DEGREE_CONS = 
prove_by_refinement( `!h t. normal t ==> (degree (CONS h t) = 1 + degree t)`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; CLAIM `normal (CONS h t)`; ASM_MESON_TAC[NORMAL_CONS]; REWRITE_TAC[normal;degree]; STRIP_TAC; ASM_REWRITE_TAC[]; RULE_ASSUM_TAC (REWRITE_RULE[normal]); CLAIM `~(LENGTH t = 0)`; ASM_MESON_TAC[LENGTH_0]; STRIP_TAC; ASM_REWRITE_TAC[LENGTH]; POP_ASSUM MP_TAC THEN ARITH_TAC; ]);;
(* }}} *) (* ---------------------------------------------------------------------- *) (* Now the derivative *) (* ---------------------------------------------------------------------- *)
let PDA_LENGTH = 
prove_by_refinement( `!p n. ~(p = []) ==> (LENGTH(poly_diff_aux n p) = LENGTH p)`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; REWRITE_TAC[]; GEN_TAC THEN DISCH_THEN IGNORE; REWRITE_TAC[LENGTH;poly_diff_aux;]; CASES_ON `t = []`; ASM_REWRITE_TAC[LENGTH;poly_diff_aux;]; ASM_MESON_TAC[]; ]);;
(* }}} *)
let POLY_DIFF_LENGTH = 
prove_by_refinement( `!p. LENGTH (poly_diff p) = PRE (LENGTH p)`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; REWRITE_TAC[poly_diff;LENGTH;PRE]; CASES_ON `t = []`; ASM_REWRITE_TAC[LENGTH;PRE]; REWRITE_TAC[poly_diff;NOT_CONS_NIL;TL;PRE;poly_diff_aux;LENGTH;]; REWRITE_TAC[poly_diff;TL;LENGTH;PRE;NOT_CONS_NIL;]; MATCH_MP_TAC PDA_LENGTH; FIRST_ASSUM MATCH_ACCEPT_TAC; ]);;
(* }}} *)
let POLY_DIFF_SING = 
prove_by_refinement( `!p h. (poly_diff p = [h]) <=> ?x. p = [x; h]`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; DISJ_CASES_TAC (ISPEC `LENGTH (p:real list)` (ARITH_RULE `!n. (n = 0) \/ (n = 1) \/ (n = 2) \/ 2 < n`)); ASM_MESON_TAC[poly_diff;LENGTH_0;NOT_CONS_NIL;]; POP_ASSUM DISJ_CASES_TAC; RULE_ASSUM_TAC (REWRITE_RULE[LENGTH_1]); POP_ASSUM MP_TAC THEN STRIP_TAC THEN POP_ASSUM SUBST1_TAC; REWRITE_TAC[poly_diff;NOT_CONS_NIL;TL;poly_diff_aux;]; ASM_MESON_TAC !LIST_REWRITES; POP_ASSUM DISJ_CASES_TAC; RULE_ASSUM_TAC (MATCH_EQ_MP LENGTH_PAIR); POP_ASSUM MP_TAC THEN STRIP_TAC; ASM_REWRITE_TAC[poly_diff;NOT_CONS_NIL;TL;poly_diff_aux;REAL_MUL_LID;]; ASM_MESON_TAC[CONS_11]; EQ_TAC; STRIP_TAC; POP_ASSUM (ASSUME_TAC o (AP_TERM `LENGTH:((real) list) -> num`)); RULE_ASSUM_TAC(REWRITE_RULE[LENGTH]); CLAIM `PRE (LENGTH p) = 1`; ASM_MESON_TAC[POLY_DIFF_LENGTH;ARITH_RULE `SUC 0 = 1`]; STRIP_TAC; CLAIM `LENGTH p = 2`; POP_ASSUM MP_TAC THEN ARITH_TAC; ASM_MESON_TAC[LT_REFL]; REPEAT STRIP_TAC; ASM_REWRITE_TAC[]; REWRITE_TAC[poly_diff;NOT_CONS_NIL;TL;poly_diff_aux;REAL_MUL_LID;]; ]);;
(* }}} *)
let lem = 
prove_by_refinement( `!p n. ~(p = []) ==> (LAST (poly_diff_aux n p) = LAST p * &(PRE(LENGTH p) + n))`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; REWRITE_TAC[]; REPEAT STRIP_TAC; POP_ASSUM IGNORE; REWRITE_TAC[LENGTH;poly_diff_aux;]; CASES_ON `t = []`; ASM_REWRITE_TAC[poly_diff_aux;LAST;LENGTH;GSYM REAL_OF_NUM_ADD]; CLAIM `((SUC 0) - 1) + n = n`; ARITH_TAC; DISCH_THEN SUBST1_TAC; REWRITE_TAC[PRE]; REAL_ARITH_TAC; POP_ASSUM (fun x -> FIRST_ASSUM (fun y -> MP_TAC (MATCH_MP y x)) THEN ASSUME_TAC x); STRIP_TAC; ASM_REWRITE_TAC[]; LIST_SIMP_TAC; ASM_REWRITE_TAC[]; COND_CASES_TAC; REWRITE_TAC[PRE]; ASM_MESON_TAC[PDA_LENGTH;LENGTH;LENGTH_0]; REWRITE_TAC[PRE]; MATCH_EQ_MP_TAC (GSYM REAL_EQ_MUL_LCANCEL); DISJ2_TAC; AP_TERM_TAC; CLAIM `~(LENGTH t = 0)`; ASM_MESON_TAC[LENGTH_0]; ARITH_TAC; ]);;
(* }}} *)
let NONCONSTANT_LENGTH = 
prove_by_refinement( `!p. nonconstant p ==> 1 < LENGTH p`,
(* {{{ Proof *) [ REWRITE_TAC[nonconstant;normal]; ASM_MESON_TAC[LENGTH_0;LENGTH_1;ARITH_RULE `(x = 0) \/ (x = 1) \/ 1 < x`]; ]);;
(* }}} *)
let NONCONSTANT_DIFF_NIL = 
prove_by_refinement( `!p. nonconstant p ==> ~(poly_diff p = [])`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; CLAIM `1 < LENGTH p`; ASM_MESON_TAC[NONCONSTANT_LENGTH]; STRIP_TAC; CLAIM `0 < LENGTH (poly_diff p)`; REWRITE_TAC[POLY_DIFF_LENGTH]; POP_ASSUM MP_TAC THEN ARITH_TAC; ASM_REWRITE_TAC[LENGTH]; ARITH_TAC; ]);;
(* }}} *)
let NONCONSTANT_DEGREE = 
prove_by_refinement( `!p. nonconstant p ==> 0 < degree p`,
(* {{{ Proof *) [ GEN_TAC; DISCH_THEN (fun x -> ASSUME_TAC x THEN MP_TAC x); REWRITE_TAC[nonconstant;degree]; REPEAT STRIP_TAC; CLAIM `normalize p = p`; ASM_MESON_TAC[normal]; STRIP_TAC; ASM_REWRITE_TAC[]; CLAIM `1 < LENGTH p`; ASM_MESON_TAC[NONCONSTANT_LENGTH]; ARITH_TAC; ]);;
(* }}} *)
let POLY_DIFF_LAST_LEM = 
prove_by_refinement( `!p. nonconstant p ==> (LAST (poly_diff p) = LAST p * &(degree p))`,
(* {{{ Proof *) [ REWRITE_TAC[nonconstant;poly_diff;]; REPEAT STRIP_TAC; COND_CASES_TAC; ASM_MESON_TAC[normal]; CLAIM `~(TL p = [])`; ASM_MESON_TAC[TL;NOT_CONS_NIL;list_CASES;TL_NIL]; DISCH_THEN (fun x -> MP_TAC (MATCH_MP lem x) THEN ASSUME_TAC x); DISCH_THEN (ASSUME_TAC o ISPEC `1`); ASM_REWRITE_TAC[]; CLAIM `LAST (TL p) = LAST p`; ASM_MESON_TAC[LAST_TL]; DISCH_THEN SUBST1_TAC; REWRITE_TAC[degree]; CLAIM `normalize p = p`; ASM_MESON_TAC[normal]; DISCH_THEN SUBST1_TAC; MATCH_EQ_MP_TAC (GSYM REAL_EQ_MUL_LCANCEL); DISJ2_TAC; AP_TERM_TAC; ASM_SIMP_TAC[LENGTH_TL]; CLAIM `~(LENGTH p = 0)`; ASM_MESON_TAC[LENGTH_0]; CLAIM `~(LENGTH p = 1)`; ASM_MESON_TAC[LENGTH_1]; ARITH_TAC; ]);;
(* }}} *)
let NONCONSTANT_DIFF_0 = 
prove_by_refinement( `!p. nonconstant p ==> ~(poly_diff p = [&0])`,
(* {{{ Proof *) [ STRIP_TAC; DISCH_THEN (fun x -> MP_TAC x THEN ASSUME_TAC x); REWRITE_TAC[nonconstant]; REPEAT STRIP_TAC; CLAIM `~(p = [])`; ASM_MESON_TAC[normal]; DISCH_THEN (fun x -> RULE_ASSUM_TAC (REWRITE_RULE[x]) THEN ASSUME_TAC x); CLAIM `~(LAST p = &0)`; MATCH_MP_TAC NORMAL_LAST_NONZERO; FIRST_ASSUM MATCH_ACCEPT_TAC; STRIP_TAC; CLAIM `LAST p * &(degree p) = &0`; ASM_SIMP_TAC[GSYM POLY_DIFF_LAST_LEM]; REWRITE_TAC[LAST]; STRIP_TAC; CLAIM `(LAST p = &0) \/ (&(degree p) = &0)`; ASM_MESON_TAC[REAL_ENTIRE]; STRIP_TAC; ASM_MESON_TAC[]; CLAIM `?h t. p = CONS h t`; ASM_MESON_TAC[list_CASES]; STRIP_TAC; CLAIM `normal t`; ASM_MESON_TAC[NORMAL_TAIL]; STRIP_TAC; FIRST_ASSUM (MP_TAC o (MATCH_MP (ISPECL [`h:real`;`t:real list`] DEGREE_CONS))); STRIP_TAC; CLAIM `degree p = 0`; ASM_MESON_TAC [REAL_OF_NUM_EQ]; ASM_REWRITE_TAC[]; ARITH_TAC; ]);;
(* }}} *)
let POLY_DIFF_LAST_LT = 
prove_by_refinement( `!p. nonconstant p ==> (LAST (poly_diff p) < &0 <=> LAST p < &0)`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; ASM_SIMP_TAC[POLY_DIFF_LAST_LEM]; CLAIM `&0 <= &(degree p)`; REAL_ARITH_TAC; STRIP_TAC; EQ_TAC; ASM_MESON_TAC([REAL_MUL_LT] @ !REAL_REWRITES); STRIP_TAC; CLAIM `0 < degree p`; ASM_MESON_TAC[NONCONSTANT_DEGREE]; STRIP_TAC; CLAIM `&0 < &(degree p)`; REAL_SIMP_TAC; FIRST_ASSUM MATCH_ACCEPT_TAC; STRIP_TAC; MATCH_EQ_MP_TAC (GSYM REAL_MUL_LT); ASM_REWRITE_TAC[]; ]);;
(* }}} *)
let POLY_DIFF_LAST_GT = 
prove_by_refinement( `!p. nonconstant p ==> (&0 < LAST (poly_diff p) <=> &0 < LAST p)`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; ASM_SIMP_TAC[POLY_DIFF_LAST_LEM]; CLAIM `&0 < &(degree p)`; ASM_MESON_TAC[NONCONSTANT_DEGREE;REAL_OF_NUM_LT]; STRIP_TAC; EQ_TAC; REWRITE_TAC[REAL_MUL_GT]; STRIP_TAC; EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC; STRIP_TAC; ONCE_REWRITE_TAC [ARITH_RULE `&0 = &0 * &0`]; MATCH_MP_TAC REAL_LT_MUL2; EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC; ]);;
(* }}} *)
let NONCONSTANT_DIFF_NORMAL = 
prove_by_refinement( `!p. nonconstant p ==> normal (poly_diff p)`,
(* {{{ Proof *) [ GEN_TAC; DISCH_THEN (fun x -> ASSUME_TAC x THEN MP_TAC x); REWRITE_TAC[nonconstant]; REPEAT STRIP_TAC; MATCH_MP_TAC NORMAL_LAST_LENGTH; STRIP_TAC; CLAIM `1 < LENGTH p`; ASM_MESON_TAC[NONCONSTANT_LENGTH]; STRIP_TAC; CLAIM `LENGTH (poly_diff p) = PRE (LENGTH p)`; ASM_MESON_TAC[POLY_DIFF_LENGTH]; POP_ASSUM MP_TAC THEN ARITH_TAC; STRIP_TAC; CASES_ON `LAST p < &0`; CLAIM `LAST (poly_diff p) < &0`; ASM_MESON_TAC[POLY_DIFF_LAST_LT]; ASM_REWRITE_TAC[]; REAL_ARITH_TAC; REWRITE_ASSUMS !REAL_REWRITES; REWRITE_ASSUMS[REAL_LE_LT]; POP_ASSUM MP_TAC THEN STRIP_TAC; CLAIM `&0 < LAST (poly_diff p)`; ASM_MESON_TAC[POLY_DIFF_LAST_GT]; ASM_REWRITE_TAC[]; REAL_ARITH_TAC; ASM_MESON_TAC[NORMAL_ID]; ]);;
(* }}} *)
let PDIFF_POS_LAST = 
prove_by_refinement( `!p. nonconstant p /\ (?X. !x. X < x ==> &0 < poly (poly_diff p) x) ==> &0 < LAST p`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; CLAIM `&0 < LAST (poly_diff p)`; MATCH_MP_TAC POLY_LAST_GT; ASM_SIMP_TAC[NONCONSTANT_DIFF_NORMAL]; ASM_MESON_TAC[]; STRIP_TAC; ASM_SIMP_TAC[GSYM POLY_DIFF_LAST_GT]; ]);;
(* }}} *)
let LAST_UNB = 
prove_by_refinement( `!p. nonconstant p /\ &0 < LAST p ==> mono_unbounded_above (\n. poly p (&n))`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; MATCH_MP_TAC mua_quotient_limit; EXISTS_TAC `&1`; EXISTS_TAC `(\n. (LAST p) * (&n) pow (degree p))`; BETA_TAC; STRIP_TAC; REAL_ARITH_TAC; STRIP_TAC; MATCH_MP_TAC LIM_POLY2; ASM_MESON_TAC[nonconstant]; MATCH_MP_TAC POW_UNB_CON; ASM_REWRITE_TAC[]; ASM_MESON_TAC[NONCONSTANT_DEGREE]; ]);;
(* }}} *) (* ---------------------------------------------------------------------- *) (* Finally, the positive theorems *) (* ---------------------------------------------------------------------- *)
let POLY_DIFF_UP_RIGHT = 
prove_by_refinement( `nonconstant p /\ (?X. !x. X < x ==> &0 < poly (poly_diff p) x) ==> (?Y. !y. Y < y ==> &0 < poly p y)`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; CLAIM `mono_unbounded_above (\n. poly p (&n))`; MATCH_MP_TAC LAST_UNB; ASM_MESON_TAC[PDIFF_POS_LAST]; REWRITE_TAC[mono_unbounded_above]; DISCH_THEN (MP_TAC o (ISPEC `&0`)); STRIP_TAC; CLAIM `?K. max X (&N) < &K`; ASM_MESON_TAC[REAL_ARCH_SIMPLE_LT]; STRIP_TAC; EXISTS_TAC `&K`; REPEAT STRIP_TAC; CCONTR_TAC; REWRITE_ASSUMS[REAL_NOT_LT]; CLAIM `&N < y /\ X < y`; ASM_MESON_TAC([REAL_MAX_MAX] @ !REAL_REWRITES); REPEAT STRIP_TAC; MP_TAC (ISPECL [`p:real list`;`&K`;`y:real`] POLY_MVT); ANTS_TAC; FIRST_ASSUM MATCH_ACCEPT_TAC; STRIP_TAC; CLAIM `poly p y - poly p (&K) <= &0`; MATCH_MP_TAC (REAL_ARITH `x <= &0 /\ &0 < y ==> x - y <= &0`); ASM_REWRITE_TAC[]; FIRST_ASSUM MATCH_MP_TAC; CLAIM `&N < &K`; ASM_MESON_TAC [REAL_MAX_MAX;REAL_LET_TRANS]; STRIP_TAC; CLAIM `N:num < K`; ASM_MESON_TAC [REAL_OF_NUM_LT]; ARITH_TAC; STRIP_TAC; CLAIM `&0 < y - &K`; LABEL_ALL_TAC; USE_THEN "Z-7" MP_TAC; REAL_ARITH_TAC; STRIP_TAC; CLAIM `&0 < poly (poly_diff p) x`; FIRST_ASSUM MATCH_MP_TAC; ASM_MESON_TAC[REAL_MAX_MAX;REAL_LET_TRANS;REAL_LT_TRANS]; STRIP_TAC; CLAIM `&0 < (y - &K) * poly (poly_diff p) x`; ONCE_REWRITE_TAC [ARITH_RULE `&0 = &0 * &0`]; MATCH_MP_TAC REAL_LT_MUL2 THEN REPEAT STRIP_TAC THEN TRY REAL_ARITH_TAC THEN FIRST_ASSUM MATCH_ACCEPT_TAC; STRIP_TAC; REAL_SOLVE_TAC; ]);;
(* }}} *)
let PDIFF_NEG_LAST = 
prove_by_refinement( `!p. nonconstant p /\ (?X. !x. X < x ==> poly (poly_diff p) x < &0) ==> LAST p < &0`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; CLAIM `LAST (poly_diff p) < &0`; MATCH_MP_TAC POLY_LAST_LT; ASM_SIMP_TAC[NONCONSTANT_DIFF_NORMAL]; ASM_MESON_TAC[]; STRIP_TAC; ASM_SIMP_TAC[GSYM POLY_DIFF_LAST_LT]; ]);;
(* }}} *)
let LAST_UNB_NEG = 
prove_by_refinement( `!p. nonconstant p /\ LAST p < &0 ==> mono_unbounded_below (\n. poly p (&n))`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; MATCH_MP_TAC mua_quotient_limit_neg; EXISTS_TAC `&1`; EXISTS_TAC `(\n. (LAST p) * (&n) pow (degree p))`; BETA_TAC; STRIP_TAC; REAL_ARITH_TAC; STRIP_TAC; MATCH_MP_TAC LIM_POLY2; ASM_MESON_TAC[nonconstant]; MATCH_MP_TAC POW_UNBB_CON; ASM_REWRITE_TAC[]; ASM_MESON_TAC[NONCONSTANT_DEGREE]; ]);;
(* }}} *)
let POLY_DIFF_DOWN_RIGHT = 
prove_by_refinement( `nonconstant p /\ (?X. !x. X < x ==> poly (poly_diff p) x < &0) ==> (?Y. !y. Y < y ==> poly p y < &0)`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; CLAIM `mono_unbounded_below (\n. poly p (&n))`; MATCH_MP_TAC LAST_UNB_NEG; ASM_MESON_TAC[PDIFF_NEG_LAST]; REWRITE_TAC[mono_unbounded_below]; DISCH_THEN (MP_TAC o (ISPEC `&0`)); STRIP_TAC; CLAIM `?K. max X (&N) < &K`; ASM_MESON_TAC[REAL_ARCH_SIMPLE_LT]; STRIP_TAC; EXISTS_TAC `&K`; REPEAT STRIP_TAC; CCONTR_TAC; REWRITE_ASSUMS[REAL_NOT_LT]; CLAIM `&N < y /\ X < y`; ASM_MESON_TAC([REAL_MAX_MAX] @ !REAL_REWRITES); REPEAT STRIP_TAC; MP_TAC (ISPECL [`p:real list`;`&K`;`y:real`] POLY_MVT); ANTS_TAC; FIRST_ASSUM MATCH_ACCEPT_TAC; STRIP_TAC; CLAIM `&0 <= poly p y - poly p (&K)`; MATCH_MP_TAC (REAL_ARITH `&0 <= x /\ y < &0 ==> &0 <= x - y`); ASM_REWRITE_TAC[]; FIRST_ASSUM MATCH_MP_TAC; CLAIM `&N < &K`; ASM_MESON_TAC (!REAL_REWRITES @ !NUM_REWRITES); STRIP_TAC; CLAIM `N:num < K`; ASM_MESON_TAC [REAL_OF_NUM_LT]; ARITH_TAC; STRIP_TAC; CLAIM `&0 < y - &K`; LABEL_ALL_TAC; USE_THEN "Z-7" MP_TAC; REAL_ARITH_TAC; STRIP_TAC; CLAIM `poly (poly_diff p) x < &0`; FIRST_ASSUM MATCH_MP_TAC; REAL_SOLVE_TAC; STRIP_TAC; CLAIM `(y - &K) * poly (poly_diff p) x < &0`; ASM_MESON_TAC[REAL_MUL_LT]; REPEAT STRIP_TAC; REAL_SOLVE_TAC; ]);;
(* }}} *) (* ---------------------------------------------------------------------- *) (* Now the negative ones *) (* ---------------------------------------------------------------------- *)
let UNB_LEFT_EVEN = 
prove_by_refinement( `!k. 0 < k /\ EVEN k ==> mono_unbounded_above (\n. (-- &n) pow k)`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; ASM_REWRITE_TAC[REAL_POW_NEG]; MATCH_MP_TAC POW_UNB; FIRST_ASSUM MATCH_ACCEPT_TAC; ]);;
(* }}} *)
let UNB_LEFT_ODD = 
prove_by_refinement( `!k. 0 < k /\ ODD k ==> mono_unbounded_below (\n. (-- &n) pow k)`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; REWRITE_ASSUMS[GSYM NOT_EVEN]; ASM_REWRITE_TAC[REAL_POW_NEG]; MATCH_EQ_MP_TAC mua_neg; MATCH_MP_TAC POW_UNB; FIRST_ASSUM MATCH_ACCEPT_TAC; ]);;
(* }}} *)
let EVEN_CONS = 
prove_by_refinement( `!t h. ODD (LENGTH (CONS h t)) = EVEN (LENGTH t)`,
(* {{{ Proof *) [ LIST_INDUCT_TAC THEN ASM_MESON_TAC[LENGTH_SING;LENGTH;EVEN;ODD;ONE]; ]);;
(* }}} *)
let ODD_CONS = 
prove_by_refinement( `!t h. EVEN (LENGTH (CONS h t)) = ODD (LENGTH t)`,
(* {{{ Proof *) [ LIST_INDUCT_TAC THEN ASM_MESON_TAC[LENGTH_SING;LENGTH;EVEN;ODD;ONE]; ]);;
(* }}} *)
let MUA_DIV_CONST = 
prove_by_refinement( `!a b p. mono_unbounded_above (\n. p n) ==> (\n. a / (b + p n)) --> &0`,
(* {{{ Proof *) [ REWRITE_TAC[mono_unbounded_above;SEQ]; REPEAT STRIP_TAC; REAL_SIMP_TAC; CASES_ON `a = &0`; ASM_REWRITE_TAC[real_div;REAL_MUL_LZERO;ABS_0]; ABBREV_TAC `k = (max (&1) (abs a / e - b))`; FIRST_ASSUM (MP_TAC o (ISPEC `k:real`)); STRIP_TAC; EXISTS_TAC `N`; REPEAT STRIP_TAC; REWRITE_ASSUMS (!REAL_REWRITES @ !NUM_REWRITES); POP_ASSUM (fun x -> POP_ASSUM (fun y -> ASSUME_TAC (MATCH_MP y x))); REWRITE_TAC[REAL_ABS_DIV]; MATCH_MP_TAC REAL_LTE_TRANS; EXISTS_TAC `abs a / (b + k)`; STRIP_TAC; MATCH_MP_TAC REAL_DIV_DENOM_LT; REPEAT STRIP_TAC; ASM_MESON_TAC[REAL_ABS_NZ]; LABEL_ALL_TAC; CLAIM `(abs a / e - b) <= k`; ASM_MESON_TAC[REAL_MAX_MAX]; STRIP_TAC; CLAIM `&0 < abs a / e`; REWRITE_TAC[real_div]; MATCH_MP_TAC REAL_LT_MUL; ASM_MESON_TAC[REAL_INV_POS;REAL_ABS_NZ]; STRIP_TAC; POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; CLAIM `-- b < p n`; MATCH_MP_TAC REAL_LET_TRANS; EXISTS_TAC `k`; ASM_REWRITE_TAC[]; CLAIM `(abs a / e - b) <= k`; ASM_MESON_TAC[REAL_MAX_MAX]; STRIP_TAC; CLAIM `&0 < abs a / e`; REWRITE_TAC[real_div]; MATCH_MP_TAC REAL_LT_MUL; ASM_MESON_TAC[REAL_INV_POS;REAL_ABS_NZ]; STRIP_TAC; POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; STRIP_TAC; CLAIM `abs (b + p n) = b + p n`; MATCH_EQ_MP_TAC REAL_ABS_REFL; POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; DISCH_THEN SUBST1_TAC; POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; CLAIM `(abs a / e - b) <= k`; ASM_MESON_TAC[REAL_MAX_MAX]; STRIP_TAC; CLAIM `&0 < abs a / e`; REWRITE_TAC[real_div]; MATCH_MP_TAC REAL_LT_MUL; ASM_MESON_TAC[REAL_INV_POS;REAL_ABS_NZ]; STRIP_TAC; LABEL_ALL_TAC; CLAIM `abs a / e <= b + k`; USE_THEN "Z-1" MP_TAC THEN REAL_ARITH_TAC; STRIP_TAC; CASES_ON `&1 <= abs a / e - b`; CLAIM `k = abs a / e - b`; USE_THEN "Z-3" (SUBST1_TAC o GSYM); ASM_REWRITE_TAC[real_max]; ASM_MESON_TAC[real_max]; DISCH_THEN SUBST1_TAC; REWRITE_TAC[ARITH_RULE `b + a - b = a`]; REWRITE_TAC[real_div;]; REAL_SIMP_TAC; REWRITE_TAC[REAL_MUL_ASSOC]; CLAIM `~(abs a = &0)`; ASM_MESON_TAC[REAL_ABS_NZ;REAL_LT_LE]; STRIP_TAC; ASM_SIMP_TAC[REAL_MUL_RINV]; REAL_SIMP_TAC; (* save *) REWRITE_ASSUMS !REAL_REWRITES; CLAIM `k = &1`; ASM_MESON_TAC([real_max] @ !REAL_REWRITES); STRIP_TAC; CLAIM `&0 < b + k`; MATCH_MP_TAC REAL_LTE_TRANS; EXISTS_TAC `abs a / e`; ASM_MESON_TAC[]; STRIP_TAC; MATCH_MP_TAC REAL_LE_RCANCEL_IMP; EXISTS_TAC `b + k`; ASM_REWRITE_TAC[]; REWRITE_TAC[real_div]; REWRITE_TAC[GSYM REAL_MUL_ASSOC]; CLAIM `inv (b + &1) * (b + &1) = &1`; LABEL_ALL_TAC; POP_ASSUM MP_TAC; ASM_REWRITE_TAC[]; STRIP_TAC; ASM_MESON_TAC[REAL_MUL_LINV;REAL_LT_LE]; DISCH_THEN SUBST1_TAC; REWRITE_TAC[REAL_MUL_RID]; MATCH_MP_TAC REAL_LE_LCANCEL_IMP; EXISTS_TAC `inv e`; REPEAT STRIP_TAC; USE_THEN "Z-5" MP_TAC; MESON_TAC[REAL_INV_POS;REAL_LT_LE]; REWRITE_TAC[REAL_MUL_ASSOC]; CLAIM `~(e = &0)`; ASM_MESON_TAC[REAL_INV_NZ;REAL_LT_LE]; STRIP_TAC; ASM_SIMP_TAC[REAL_MUL_LINV]; REAL_SIMP_TAC; ASM_MESON_TAC[real_div;REAL_MUL_SYM] ]);;
(* }}} *)
let SEQ_0_NEG = 
prove_by_refinement( `!p. (\n. p n) --> &0 <=> (\n. -- p n) --> &0`,
(* {{{ Proof *) [ REWRITE_TAC[SEQ]; GEN_TAC THEN EQ_TAC; REPEAT STRIP_TAC; LABEL_ALL_TAC; USE_THEN "Z-0" (fun x -> FIRST_ASSUM (fun y -> MP_TAC (MATCH_MP y x))); STRIP_TAC; EXISTS_TAC `N`; REPEAT STRIP_TAC; POP_ASSUM (fun x -> FIRST_ASSUM (fun y -> MP_TAC (MATCH_MP y x))); REAL_SIMP_TAC; STRIP_TAC; ASM_MESON_TAC[REAL_ABS_NEG]; REPEAT STRIP_TAC; LABEL_ALL_TAC; USE_THEN "Z-0" (fun x -> FIRST_ASSUM (fun y -> MP_TAC (MATCH_MP y x))); STRIP_TAC; EXISTS_TAC `N`; REPEAT STRIP_TAC; POP_ASSUM (fun x -> FIRST_ASSUM (fun y -> MP_TAC (MATCH_MP y x))); REAL_SIMP_TAC; STRIP_TAC; ASM_MESON_TAC[REAL_ABS_NEG]; ]);;
(* }}} *)
let lem = 
prove_by_refinement( `!x y z. --(x / (y + z)) = x / (-- y + -- z)`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; REWRITE_TAC[real_div]; REWRITE_TAC[ARITH_RULE `--(x * y) = x * -- y`]; REWRITE_TAC[ARITH_RULE `-- y + -- z = --(y + z)`]; REWRITE_TAC[REAL_INV_NEG]; ]);;
(* }}} *)
let MUB_DIV_CONST = 
prove_by_refinement( `!a b p. mono_unbounded_below (\n. p n) ==> (\n. a / (b + p n)) --> &0`,
(* {{{ Proof *) [ REWRITE_TAC[mua_neg2]; REPEAT STRIP_TAC; ONCE_REWRITE_TAC[SEQ_0_NEG]; REWRITE_TAC[lem]; MATCH_MP_TAC MUA_DIV_CONST; FIRST_ASSUM MATCH_ACCEPT_TAC; ]);;
(* }}} *)
let mono_unbounded = new_definition(
  `mono_unbounded p <=> mono_unbounded_above p \/ mono_unbounded_below p`);;
let MU_DIV_CONST = 
prove_by_refinement( `!a b p. mono_unbounded p ==> (\n. a / (b + p n)) --> &0`,
(* {{{ Proof *) [ REWRITE_TAC[mono_unbounded]; REPEAT STRIP_TAC; MATCH_MP_TAC MUA_DIV_CONST; REWRITE_TAC[ETA_AX]; POP_ASSUM MATCH_ACCEPT_TAC; MATCH_MP_TAC MUB_DIV_CONST; REWRITE_TAC[ETA_AX]; POP_ASSUM MATCH_ACCEPT_TAC; ]);;
(* }}} *)
let MUA_MUA = 
prove_by_refinement( `!p q. mono_unbounded_above (\n. p n) /\ mono_unbounded_above (\n. q n) ==> mono_unbounded_above (\n. p n * q n)`,
(* {{{ Proof *) [ REWRITE_TAC[mono_unbounded_above_pos]; REPEAT STRIP_TAC; CLAIM `&0 <= max c (&1)`; REWRITE_TAC[real_max]; COND_CASES_TAC; REAL_ARITH_TAC; ASM_REWRITE_TAC[]; DISCH_THEN (fun y -> POP_ASSUM (fun x -> RULE_ASSUM_TAC (C MATCH_MP y) THEN ASSUME_TAC x)); EVERY_ASSUM MP_TAC THEN REPEAT STRIP_TAC; EXISTS_TAC `nmax N N'`; REPEAT STRIP_TAC; MATCH_MP_TAC REAL_LET_TRANS; EXISTS_TAC `max c (&1)`; ASM_REWRITE_TAC[REAL_MAX_MAX]; MATCH_MP_TAC REAL_LET_TRANS; EXISTS_TAC `max c (&1) * max c (&1)`; REPEAT STRIP_TAC; CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [GSYM REAL_MUL_RID])); MATCH_MP_TAC REAL_LE_MUL2; REPEAT STRIP_TAC; REAL_SOLVE_TAC; REAL_SIMP_TAC; REAL_ARITH_TAC; REAL_SOLVE_TAC; MATCH_MP_TAC REAL_LT_MUL2; REPEAT STRIP_TAC; REAL_SOLVE_TAC; CLAIM `N <= n /\ N' <= (n:num)`; POP_ASSUM MP_TAC; REWRITE_TAC[nmax]; COND_CASES_TAC; REPEAT STRIP_TAC; POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC; FIRST_ASSUM MATCH_ACCEPT_TAC; REPEAT STRIP_TAC; FIRST_ASSUM MATCH_ACCEPT_TAC; POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC; REPEAT STRIP_TAC; FIRST_ASSUM MATCH_MP_TAC; FIRST_ASSUM MATCH_ACCEPT_TAC; REAL_SOLVE_TAC; FIRST_ASSUM MATCH_MP_TAC; POP_ASSUM MP_TAC THEN REWRITE_TAC[nmax] THEN ARITH_TAC; ]);;
(* }}} *)
let MUA_MUB = 
prove_by_refinement( `!p q. mono_unbounded_above (\n. p n) /\ mono_unbounded_below (\n. q n) ==> mono_unbounded_below (\n. p n * q n)`,
(* {{{ Proof *) [ REWRITE_TAC[mua_neg2]; REWRITE_TAC[ARITH_RULE `--(x * y) = x * -- y`]; REPEAT STRIP_TAC; MATCH_MP_TAC MUA_MUA; ASM_REWRITE_TAC[]; ]);;
(* }}} *)
let MUB_MUA = 
prove_by_refinement( `!p q. mono_unbounded_below (\n. p n) /\ mono_unbounded_above (\n. q n) ==> mono_unbounded_below (\n. p n * q n)`,
(* {{{ Proof *) [ REWRITE_TAC[mua_neg2]; REWRITE_TAC[ARITH_RULE `--(x * y) = -- x * y`]; REPEAT STRIP_TAC; MATCH_MP_TAC MUA_MUA; ASM_REWRITE_TAC[]; ]);;
(* }}} *)
let MUB_MUB = 
prove_by_refinement( `!p q. mono_unbounded_below (\n. p n) /\ mono_unbounded_below (\n. q n) ==> mono_unbounded_above (\n. p n * q n)`,
(* {{{ Proof *) [ REWRITE_TAC[mua_neg2]; ONCE_REWRITE_TAC[ARITH_RULE `(x * y) = -- x * -- y`]; REPEAT STRIP_TAC; MATCH_MP_TAC MUA_MUA; ASM_REWRITE_TAC[]; ]);;
(* }}} *)
let MU_PROD = 
prove_by_refinement( `!p q. mono_unbounded (\n. p n) /\ mono_unbounded (\n. q n) ==> mono_unbounded (\n. p n * q n)`,
(* {{{ Proof *) [ REWRITE_TAC[mono_unbounded]; ASM_MESON_TAC[MUA_MUA;MUA_MUB;MUB_MUA;MUB_MUB]; ]);;
(* }}} *)
let mub_quotient_limit = 
prove_by_refinement( `!k f g. &0 < k /\ (\n. f n / g n) --> k /\ mono_unbounded_below g ==> mono_unbounded_below f`,
(* {{{ Proof *) [ REWRITE_TAC[mua_neg2]; REPEAT STRIP_TAC; MATCH_MP_TAC mua_quotient_limit; EXISTS_TAC `k`; EXISTS_TAC `\n. -- g n`; REPEAT STRIP_TAC; FIRST_ASSUM MATCH_ACCEPT_TAC; BETA_TAC; REWRITE_TAC[REAL_NEG_DIV]; FIRST_ASSUM MATCH_ACCEPT_TAC; FIRST_ASSUM MATCH_ACCEPT_TAC; ]);;
(* }}} *)
let POLY_UB = 
prove_by_refinement( `!p. nonconstant p ==> mono_unbounded (\n. poly p (&n))`,
(* {{{ Proof *) [ GEN_TAC; DISCH_THEN (fun x -> ASSUME_TAC x THEN MP_TAC x); REWRITE_TAC[nonconstant]; REPEAT STRIP_TAC; FIRST_ASSUM (fun x -> ASSUME_TAC (MATCH_MP LIM_POLY2 x)); CASES_ON `LAST p < &0`; REWRITE_TAC[mono_unbounded]; DISJ2_TAC; MATCH_MP_TAC mub_quotient_limit; EXISTS_TAC `&1`; EXISTS_TAC `(\n. LAST p * &n pow degree p)`; REPEAT STRIP_TAC; REAL_ARITH_TAC; BETA_TAC; MATCH_MP_TAC LIM_POLY2; FIRST_ASSUM MATCH_ACCEPT_TAC; MATCH_MP_TAC POW_UNBB_CON; ASM_REWRITE_TAC[]; MATCH_MP_TAC NONCONSTANT_DEGREE; FIRST_ASSUM MATCH_ACCEPT_TAC; REWRITE_ASSUMS !REAL_REWRITES; REWRITE_ASSUMS[REAL_LE_LT]; POP_ASSUM MP_TAC THEN STRIP_TAC; (* save *) REWRITE_TAC[mono_unbounded]; DISJ1_TAC; MATCH_MP_TAC mua_quotient_limit; EXISTS_TAC `&1`; EXISTS_TAC `(\n. LAST p * &n pow degree p)`; REPEAT STRIP_TAC; REAL_ARITH_TAC; BETA_TAC; MATCH_MP_TAC LIM_POLY2; FIRST_ASSUM MATCH_ACCEPT_TAC; MATCH_MP_TAC POW_UNB_CON; ASM_REWRITE_TAC[]; MATCH_MP_TAC NONCONSTANT_DEGREE; FIRST_ASSUM MATCH_ACCEPT_TAC; ASM_MESON_TAC[NORMAL_LAST_NONZERO]; ]);;
(* }}} *) (* ---------------------------------------------------------------------- *) (* A polynomial applied to a negative argument *) (* ---------------------------------------------------------------------- *)
let pneg_aux = new_recursive_definition list_RECURSION
 `(pneg_aux n [] = []) /\
  (pneg_aux n (CONS h t) = CONS (--(&1) pow n * h) (pneg_aux (SUC n) t))`;;
let pneg = new_recursive_definition list_RECURSION
 `(pneg [] = []) /\
  (pneg (CONS h t) = pneg_aux 0 (CONS h t))`;;
let POLY_PNEG_AUX_SUC = 
prove_by_refinement( `!t n. pneg_aux (SUC (SUC n)) t = pneg_aux n t`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; STRIP_TAC; REWRITE_TAC[pneg_aux]; REWRITE_TAC[pneg_aux;pow]; REAL_SIMP_TAC; STRIP_TAC; AP_TERM_TAC; ASM_MESON_TAC[]; ]);;
(* }}} *)
let POLY_NEG_NEG = 
prove_by_refinement( `!p. poly_neg (poly_neg p) = p`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; REWRITE_TAC[poly_neg;poly_cmul]; REWRITE_TAC[poly_neg;poly_cmul]; REAL_SIMP_TAC; AP_TERM_TAC; ASM_MESON_TAC[poly_neg;poly_cmul]; ]);;
(* }}} *)
let POLY_PNEG_NEG = 
prove_by_refinement( `!p n. poly_neg (pneg_aux (SUC n) p) = pneg_aux n p`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; ASM_REWRITE_TAC[pneg_aux;poly_neg;poly_cmul]; REWRITE_TAC[pneg_aux]; REPEAT STRIP_TAC; REWRITE_TAC[POLY_PNEG_AUX_SUC]; REWRITE_TAC[poly_neg;poly_cmul]; REAL_SIMP_TAC; AP_TERM_TAC; REWRITE_TAC[GSYM poly_neg]; CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV[GSYM POLY_NEG_NEG])); POP_ASSUM (ONCE_REWRITE_TAC o list); REWRITE_TAC[]; ]);;
(* }}} *)
let POLY_PNEG_AUX = 
prove_by_refinement( `!k p n. EVEN n ==> (poly p (-- k) = poly (pneg_aux n p) k)`,
(* {{{ Proof *) [ STRIP_TAC; LIST_INDUCT_TAC; REPEAT STRIP_TAC; REWRITE_TAC[pneg_aux;poly]; REPEAT STRIP_TAC; POP_ASSUM (fun x -> RULE_ASSUM_TAC (fun y -> MATCH_MP y x) THEN ASSUME_TAC x); REWRITE_TAC[poly;pneg_aux]; REAL_SIMP_TAC; ASM_REWRITE_TAC[]; REAL_SIMP_TAC; CLAIM `-- &1 pow n = &1`; REWRITE_TAC[REAL_POW_NEG]; ASM_REWRITE_TAC[]; REAL_SIMP_TAC; DISCH_THEN SUBST1_TAC; REAL_SIMP_TAC; AP_TERM_TAC; CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV[GSYM POLY_PNEG_NEG])); REWRITE_TAC[POLY_NEG]; REAL_SIMP_TAC; ]);;
(* }}} *)
let POLY_PNEG = 
prove_by_refinement( `!p x. poly p (-- x) = poly (pneg p) x`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; REWRITE_TAC[pneg;poly]; REWRITE_TAC[pneg;poly]; REPEAT STRIP_TAC; CLAIM `poly (pneg_aux 0 (CONS h t)) x = poly (CONS h t) (--x)`; ASM_MESON_TAC[POLY_PNEG_AUX;EVEN]; DISCH_THEN SUBST1_TAC; REWRITE_TAC[poly]; ]);;
(* }}} *)
let DEGREE_0 = 
prove_by_refinement( `degree [] = 0 `,
(* {{{ Proof *) [ REWRITE_TAC[degree]; REWRITE_TAC[normalize;LENGTH]; ARITH_TAC; ]);;
(* }}} *)
let EVEN_ODD = 
prove_by_refinement( `!x. EVEN (SUC x) = ODD x`,
(* {{{ Proof *) [ REWRITE_TAC[EVEN;NOT_EVEN]; ]);;
(* }}} *)
let ODD_EVEN = 
prove_by_refinement( `!x. ODD (SUC x) = EVEN x`,
(* {{{ Proof *) [ REWRITE_TAC[ODD;NOT_ODD]; ]);;
(* }}} *)
let PNEG_CONS = 
prove_by_refinement( `!p. pneg (CONS h t) = CONS h (neg (pneg t))`,
(* {{{ Proof *) [ REWRITE_TAC[pneg;pneg_aux]; REAL_SIMP_TAC; ONCE_REWRITE_TAC[GSYM POLY_PNEG_NEG]; REWRITE_TAC[POLY_PNEG_AUX_SUC]; CASES_ON `t = []`; ASM_REWRITE_TAC[pneg;pneg_aux;]; REWRITE_ASSUMS !LIST_REWRITES; POP_ASSUM MP_TAC THEN STRIP_TAC; ASM_REWRITE_TAC[]; REWRITE_TAC[GSYM pneg]; ]);;
(* }}} *)
let PNEG_NIL = 
prove_by_refinement( `!p. (pneg p = []) <=> (p = [])`,
(* {{{ Proof *) [ LIST_INDUCT_TAC THEN MESON_TAC[pneg;NOT_CONS_NIL;pneg_aux]; ]);;
(* }}} *)
let PNEG_AUX_NIL = 
prove_by_refinement( `!p n. (pneg_aux n p = []) <=> (p = [])`,
(* {{{ Proof *) [ LIST_INDUCT_TAC THEN MESON_TAC[pneg;NOT_CONS_NIL;pneg_aux]; ]);;
(* }}} *)
let POLY_CMUL_NIL = 
prove_by_refinement( `!p. (c ## p = []) <=> (p = [])`,
(* {{{ Proof *) [ LIST_INDUCT_TAC THEN MESON_TAC[poly_cmul;NOT_CONS_NIL;pneg_aux]; ]);;
(* }}} *)
let POLY_NEG_NIL = 
prove_by_refinement( `!p. (poly_neg p = []) <=> (p = [])`,
(* {{{ Proof *) [ LIST_INDUCT_TAC THEN MESON_TAC[poly_neg;poly_cmul;NOT_CONS_NIL]; ]);;
(* }}} *)
let NEG_LAST = 
prove_by_refinement( `!p. ~(p = []) ==> (LAST (neg p) = -- LAST p)`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; REWRITE_TAC[]; DISCH_THEN IGNORE; CASES_ON `t = []`; ASM_REWRITE_TAC[poly_neg;poly_cmul;LAST;]; REAL_ARITH_TAC; POP_ASSUM (fun x -> REWRITE_ASSUMS[x] THEN ASSUME_TAC x); ASM_SIMP_TAC[LAST_CONS;poly_neg;poly_cmul;]; CLAIM `~(-- &1 ## t = [])`; ASM_MESON_TAC[POLY_CMUL_NIL]; STRIP_TAC; ASM_SIMP_TAC[LAST_CONS]; ASM_MESON_TAC[poly_neg;]; ]);;
(* }}} *)
let POLY_PNEG_LAST = 
prove_by_refinement( `!p. normal p ==> (EVEN (degree p) ==> (LAST p = LAST (pneg p))) /\ (ODD (degree p) ==> (LAST p = -- LAST (pneg p)))`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; REWRITE_TAC[normal]; STRIP_TAC; CASES_ON `t = []`; ASM_REWRITE_TAC[LAST;pneg;pneg_aux]; REAL_SIMP_TAC; ASM_MESON_TAC[DEGREE_SING;EVEN;NOT_EVEN]; CLAIM `normal t`; MATCH_MP_TAC NORMAL_TAIL; ASM_MESON_TAC[]; DISCH_THEN (fun x -> RULE_ASSUM_TAC (REWRITE_RULE [x]) THEN ASSUME_TAC x); STRIP_TAC; STRIP_TAC; CLAIM `ODD (degree t)`; MATCH_EQ_MP_TAC EVEN_ODD; ASM_MESON_TAC[DEGREE_CONS;ADD1;ADD_SYM]; DISCH_THEN (fun x -> RULE_ASSUM_TAC (REWRITE_RULE [x]) THEN ASSUME_TAC x); ASM_SIMP_TAC[LAST_CONS]; REWRITE_TAC[PNEG_CONS]; CLAIM `~(neg (pneg t) = [])`; ASM_MESON_TAC[POLY_NEG_NIL;PNEG_NIL]; STRIP_TAC; ASM_SIMP_TAC[LAST_CONS]; ASM_MESON_TAC[NEG_LAST;PNEG_NIL]; CLAIM `normal t`; MATCH_MP_TAC NORMAL_TAIL; ASM_MESON_TAC[]; REPEAT STRIP_TAC; CLAIM `EVEN (degree t)`; MATCH_EQ_MP_TAC ODD_EVEN; ASM_MESON_TAC[DEGREE_CONS;ADD1;ADD_SYM]; DISCH_THEN (fun x -> RULE_ASSUM_TAC (REWRITE_RULE [x]) THEN ASSUME_TAC x); ASM_SIMP_TAC[LAST_CONS]; REWRITE_TAC[PNEG_CONS]; CLAIM `~(neg (pneg t) = [])`; ASM_MESON_TAC[POLY_NEG_NIL;PNEG_NIL]; STRIP_TAC; ASM_SIMP_TAC[LAST_CONS]; ASM_SIMP_TAC[NEG_LAST;PNEG_NIL]; REAL_SIMP_TAC; ]);;
(* }}} *)
let PNEG_AUX_LENGTH = 
prove_by_refinement( `!p n. LENGTH (pneg_aux n p) = LENGTH p`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; REWRITE_TAC[LENGTH;pneg;pneg_aux;]; REWRITE_TAC[LENGTH;pneg;pneg_aux;]; ASM_MESON_TAC[]; ]);;
(* }}} *)
let PNEG_LENGTH = 
prove_by_refinement( `!p. LENGTH (pneg p) = LENGTH p`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; REWRITE_TAC[LENGTH;pneg;pneg_aux;]; REWRITE_TAC[LENGTH;pneg;pneg_aux;]; ASM_MESON_TAC[PNEG_AUX_LENGTH]; ]);;
(* }}} *)
let LAST_PNEG_AUX_0 = 
prove_by_refinement( `!p n. ~(p = []) ==> ((LAST p = &0) <=> (LAST (pneg_aux n p) = &0))`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; REWRITE_TAC[]; STRIP_TAC; DISCH_THEN IGNORE; CASES_ON `t = []`; ASM_REWRITE_TAC[LAST;pneg;pneg_aux;]; REAL_SIMP_TAC; ASM_SIMP_TAC[LAST_CONS;pneg;pneg_aux;]; REAL_SIMP_TAC; EQ_TAC; DISCH_THEN SUBST1_TAC; REAL_SIMP_TAC; STRIP_TAC; MP_TAC (ISPECL[`-- &1`;`n:num`] POW_NZ); REAL_SIMP_TAC; REWRITE_TAC[ARITH_RULE `~(-- &1 = &0)`]; STRIP_TAC; ASM_MESON_TAC[REAL_ENTIRE]; ASM_SIMP_TAC[LAST_CONS]; REWRITE_TAC[pneg_aux]; CLAIM `~(pneg_aux (SUC n) t = [])`; ASM_MESON_TAC[PNEG_AUX_NIL]; STRIP_TAC; ASM_SIMP_TAC[LAST_CONS]; ASM_MESON_TAC[]; ]);;
(* }}} *)
let LAST_PNEG_0 = 
prove_by_refinement( `!p n. ~(p = []) ==> ((LAST p = &0) = (LAST (pneg p) = &0))`,
(* {{{ Proof *) [ LIST_INDUCT_TAC THEN MESON_TAC[LAST_PNEG_AUX_0;pneg]; ]);;
(* }}} *)
let PNEG_LAST = 
prove_by_refinement( `!p. ~(p = []) ==> (LAST (pneg p) = LAST p) \/ (LAST (pneg p) = -- LAST p)`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; CASES_ON `normal p`; MP_TAC (ISPEC `p:real list` POLY_PNEG_LAST); ASM_REWRITE_TAC[]; STRIP_TAC; DISJ_CASES_TAC (ISPEC `degree p` EVEN_OR_ODD); ASM_MESON_TAC[]; ASM_MESON_TAC !REAL_REWRITES; REWRITE_ASSUMS[NORMAL_ID;DE_MORGAN_THM;]; POP_ASSUM MP_TAC THEN STRIP_TAC; CLAIM `LENGTH p = 0`; POP_ASSUM MP_TAC THEN ARITH_TAC; ASM_MESON_TAC[LENGTH_0]; ASM_REWRITE_TAC[]; DISJ1_TAC; ASM_MESON_TAC[LAST_PNEG_0]; ]);;
(* }}} *)
let NORMAL_PNEG = 
prove_by_refinement( `!p. normal p = normal (pneg p)`,
(* {{{ Proof *) [ REWRITE_TAC[NORMAL_ID]; REPEAT STRIP_TAC; EQ_TAC; REPEAT STRIP_TAC; ASM_MESON_TAC[PNEG_LENGTH]; MP_TAC (ISPEC `p:real list` PNEG_LAST); CLAIM `~(p = [])`; ASM_MESON_TAC[LENGTH_NZ]; STRIP_TAC; ASM_REWRITE_TAC[]; EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC; (* save *) REPEAT STRIP_TAC; ONCE_REWRITE_TAC[GSYM PNEG_LENGTH]; ASM_REWRITE_TAC[]; MP_TAC (ISPEC `p:real list` PNEG_LAST); CLAIM `~(p = [])`; ASM_MESON_TAC[LENGTH_NZ;PNEG_LENGTH]; STRIP_TAC; ASM_REWRITE_TAC[]; EVERY_ASSUM MP_TAC THEN REAL_ARITH_TAC; ]);;
(* }}} *)
let PNEG_AUX_NORMALIZE_LENGTH = 
prove_by_refinement( `!p n. LENGTH (normalize (pneg_aux n p)) = LENGTH (normalize p)`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; REWRITE_TAC[normalize;LENGTH;pneg_aux;]; REWRITE_TAC[normalize;LENGTH;pneg;pneg_aux;]; STRIP_TAC; REPEAT COND_CASES_TAC THEN TRY (ASM_SIMP_TAC !LIST_REWRITES); LABEL_ALL_TAC; KEEP ["Z-2";
"Z-0"]; CLAIM `~(-- &1 pow n = &0)`; MATCH_MP_TAC REAL_POW_NZ; REAL_ARITH_TAC; STRIP_TAC; ASM_MESON_TAC[REAL_ENTIRE]; ASM_MESON_TAC[LENGTH_0]; CLAIM `~(-- &1 pow n = &0)`; MATCH_MP_TAC REAL_POW_NZ; REAL_ARITH_TAC; STRIP_TAC; ASM_MESON_TAC[REAL_ENTIRE]; ASM_MESON_TAC[LENGTH_0]; ASM_MESON_TAC[LENGTH_0]; ]);; (* }}} *)
let PNEG_NORMALIZE_LENGTH = 
prove_by_refinement( `!p n. LENGTH (normalize (pneg p)) = LENGTH (normalize p)`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; REWRITE_TAC[pneg]; ASM_MESON_TAC[PNEG_AUX_NORMALIZE_LENGTH;pneg;pneg_aux;]; ]);;
(* }}} *)
let DEGREE_PNEG = 
prove_by_refinement( `!p. degree (pneg p) = degree p`,
(* {{{ Proof *) [ REWRITE_TAC[degree]; ASM_MESON_TAC[PNEG_NORMALIZE_LENGTH]; ]);;
(* }}} *)
let PNEG_SING = 
prove_by_refinement( `!p. (pneg p = [x]) <=> (p = [x])`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; REWRITE_TAC[pneg;pneg_aux]; EQ_TAC; REPEAT STRIP_TAC; LIST_SIMP_TAC; STRIP_TAC; REWRITE_ASSUMS[pneg;pneg_aux]; POP_ASSUM MP_TAC; REAL_SIMP_TAC; LIST_SIMP_TAC; MESON_TAC[]; POP_ASSUM MP_TAC; REWRITE_TAC[pneg;pneg_aux]; LIST_SIMP_TAC; ASM_MESON_TAC[PNEG_AUX_NIL]; REWRITE_TAC[pneg;pneg_aux]; REAL_SIMP_TAC; LIST_SIMP_TAC; STRIP_TAC; ASM_MESON_TAC[pneg_aux]; ]);;
(* }}} *)
let PNEG_NONCONSTANT = 
prove_by_refinement( `!p. nonconstant (pneg p) = nonconstant p`,
(* {{{ Proof *) [ REWRITE_TAC[nonconstant]; STRIP_TAC THEN EQ_TAC; REPEAT STRIP_TAC; ASM_MESON_TAC[NORMAL_PNEG]; POP_ASSUM (REWRITE_ASSUMS o list); REWRITE_ASSUMS[pneg;pneg_aux]; POP_ASSUM MP_TAC; REAL_SIMP_TAC; MESON_TAC[]; REPEAT STRIP_TAC; ASM_MESON_TAC[NORMAL_PNEG]; ASM_MESON_TAC[PNEG_SING]; ]);;
(* }}} *)
let LAST_UNBB_EVEN_NEG = 
prove_by_refinement( `!p. nonconstant p /\ EVEN (degree p) /\ LAST p < &0 ==> mono_unbounded_below (\n. poly p (-- &n))`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; REWRITE_TAC[POLY_PNEG]; MATCH_MP_TAC LAST_UNB_NEG; ASM_REWRITE_TAC[PNEG_NONCONSTANT]; ASM_MESON_TAC[POLY_PNEG_LAST;nonconstant;]; ]);;
(* }}} *)
let POLY_PNEG_LAST2 = 
prove_by_refinement( `!p. normal p ==> (EVEN (degree p) ==> (LAST (pneg p) = LAST p)) /\ (ODD (degree p) ==> (LAST (pneg p) = -- LAST p))`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; ASM_MESON_TAC[POLY_PNEG_LAST]; ASM_MESON_TAC([POLY_PNEG_LAST; ARITH_RULE `(--x = y) <=> (x = -- y)` ]); ]);;
(* }}} *)
let LAST_UNB_ODD_NEG = 
prove_by_refinement( `!p. nonconstant p /\ ODD (degree p) /\ LAST p < &0 ==> mono_unbounded_above (\n. poly p (-- &n))`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; REWRITE_TAC[POLY_PNEG]; MATCH_MP_TAC LAST_UNB; ASM_REWRITE_TAC[PNEG_NONCONSTANT]; CLAIM `LAST (pneg p) = -- LAST p`; ASM_MESON_TAC[POLY_PNEG_LAST2;nonconstant;]; DISCH_THEN SUBST1_TAC; POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ]);;
(* }}} *)
let LAST_UNB_EVEN_POS = 
prove_by_refinement( `!p. nonconstant p /\ EVEN (degree p) /\ &0 < LAST p ==> mono_unbounded_above (\n. poly p (-- &n))`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; REWRITE_TAC[POLY_PNEG]; MATCH_MP_TAC LAST_UNB; ASM_REWRITE_TAC[PNEG_NONCONSTANT]; ASM_MESON_TAC[POLY_PNEG_LAST2;nonconstant;]; ]);;
(* }}} *)
let LAST_UNB_ODD_POS = 
prove_by_refinement( `!p. nonconstant p /\ ODD (degree p) /\ &0 < LAST p ==> mono_unbounded_below (\n. poly p (-- &n))`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; REWRITE_TAC[POLY_PNEG]; MATCH_MP_TAC LAST_UNB_NEG; ASM_REWRITE_TAC[PNEG_NONCONSTANT]; CLAIM `LAST (pneg p) = -- LAST p`; ASM_MESON_TAC[POLY_PNEG_LAST2;nonconstant;]; DISCH_THEN SUBST1_TAC; POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ]);;
(* }}} *)
let PNEG_NORMALIZE_LENGTH = 
prove_by_refinement( `!p n. LENGTH (normalize (pneg p)) = LENGTH (normalize p)`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; REWRITE_TAC[pneg]; ASM_MESON_TAC[PNEG_AUX_NORMALIZE_LENGTH;pneg;pneg_aux;]; ]);;
(* }}} *)
let POLY_DIFF_AUX_NORMAL = 
prove_by_refinement( `!p n. ~(n = 0) ==> (normal p = normal (poly_diff_aux n p))`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; REWRITE_TAC[normal;poly_diff_aux;]; REPEAT STRIP_TAC; REWRITE_TAC[poly_diff_aux]; CASES_ON `t = []`; ASM_REWRITE_TAC[poly_diff_aux;]; REWRITE_TAC[normal]; EQ_TAC; REPEAT STRIP_TAC; REWRITE_TAC[normalize]; COND_CASES_TAC; CLAIM `~(h = &0)`; ASM_MESON_TAC[normal;normalize]; STRIP_TAC; ASM_MESON_TAC[REAL_ENTIRE;REAL_INJ]; ASM_REWRITE_TAC[]; ASM_MESON_TAC[NOT_CONS_NIL]; STRIP_TAC; ASM_REWRITE_TAC[NOT_CONS_NIL]; REWRITE_TAC[NORMALIZE_SING]; CLAIM `~(&n * h = &0)`; ASM_MESON_TAC[normalize]; ASM_MESON_TAC[REAL_ENTIRE;REAL_INJ;normalize]; EQ_TAC; REPEAT STRIP_TAC; CLAIM `normal t`; ASM_MESON_TAC[NORMAL_TAIL]; STRIP_TAC; MATCH_MP_TAC NORMAL_CONS; ASM_MESON_TAC[ARITH_RULE `~(SUC x = 0)`]; STRIP_TAC; MATCH_MP_TAC NORMAL_CONS; MP_TAC (ARITH_RULE `~(SUC n = 0)`); DISCH_THEN (fun x -> FIRST_ASSUM (fun y -> (MP_TAC (MATCH_MP y x)))); STRIP_TAC; ASM_REWRITE_TAC[]; MATCH_MP_TAC NORMAL_TAIL; EXISTS_TAC `&n * h`; ASM_REWRITE_TAC[]; ASM_MESON_TAC[poly_diff_aux;NOT_CONS_NIL;list_CASES]; ]);;
(* }}} *)
let POLY_DIFF_NORMAL = 
prove_by_refinement( `!p. nonconstant p ==> normal (poly_diff p)`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; ASM_MESON_TAC[normal;poly_diff;poly_diff_aux;POLY_DIFF_AUX_NORMAL;ARITH_RULE `~(1 = 0)`;nonconstant;]; REWRITE_TAC[poly_diff;NOT_CONS_NIL;TL]; REWRITE_TAC[nonconstant]; STRIP_TAC; CLAIM `normal t`; MATCH_MP_TAC NORMAL_TAIL; EXISTS_TAC `h:real`; ASM_MESON_TAC[normal]; STRIP_TAC; ASM_MESON_TAC[normal;poly_diff;poly_diff_aux;POLY_DIFF_AUX_NORMAL;ARITH_RULE `~(1 = 0)`]; ]);;
(* }}} *)
let POLY_DIFF_AUX_NORMAL2 = 
prove_by_refinement( `!p n. ~(n = 0) ==> (normal (poly_diff_aux n p) <=> normal p)`,
(* {{{ Proof *) [MESON_TAC[POLY_DIFF_AUX_NORMAL]]);;
(* }}} *)
let POLY_DIFF_AUX_DEGREE = 
prove_by_refinement( `!p m n. ~(n = 0) /\ ~(m = 0) /\ normal p ==> (degree (poly_diff_aux n p) = degree (poly_diff_aux m p))`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; REWRITE_TAC[poly_diff_aux]; REPEAT STRIP_TAC; REWRITE_TAC[poly_diff_aux]; CASES_ON `t = []`; ASM_REWRITE_TAC[poly_diff_aux;DEGREE_SING]; CLAIM `normal (poly_diff_aux (SUC n) t)`; ASM_SIMP_TAC[POLY_DIFF_AUX_NORMAL2;NOT_SUC]; MATCH_MP_TAC NORMAL_TAIL; ASM_REWRITE_TAC[]; EXISTS_TAC `h:real`; ASM_REWRITE_TAC[]; STRIP_TAC; CLAIM `normal (poly_diff_aux (SUC m) t)`; ASM_SIMP_TAC[POLY_DIFF_AUX_NORMAL2;NOT_SUC]; MATCH_MP_TAC NORMAL_TAIL; ASM_REWRITE_TAC[]; EXISTS_TAC `h:real`; ASM_REWRITE_TAC[]; STRIP_TAC; ASM_SIMP_TAC[DEGREE_CONS]; AP_TERM_TAC; FIRST_ASSUM MATCH_MP_TAC; STRIP_TAC; ARITH_TAC; STRIP_TAC; ARITH_TAC; MATCH_MP_TAC NORMAL_TAIL; ASM_MESON_TAC[]; ]);;
(* }}} *)
let poly_diff_aux_odd = 
prove_by_refinement( `!p n. nonconstant p ==> (EVEN (degree p) = EVEN (degree (poly_diff_aux n p))) /\ (ODD (degree p) = ODD (degree (poly_diff_aux n p)))`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; REWRITE_TAC[normal;nonconstant;]; STRIP_TAC; DISCH_THEN (fun x -> ASSUME_TAC x THEN MP_TAC x); REWRITE_TAC[nonconstant]; STRIP_TAC; CASES_ON `t = []`; ASM_MESON_TAC[nonconstant;normal]; REWRITE_TAC[poly_diff_aux]; CLAIM `normal t`; ASM_MESON_TAC[NORMAL_TAIL]; STRIP_TAC; CLAIM `normal (poly_diff_aux (SUC n) t)`; ASM_MESON_TAC[nonconstant;normal;POLY_DIFF_AUX_NORMAL;NOT_SUC]; STRIP_TAC; CASES_ON `?x. t = [x]`; POP_ASSUM MP_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[]; CLAIM `~(x = &0)`; ASM_MESON_TAC[normal;normalize]; STRIP_TAC; CLAIM `degree [h; x] = 1`; CLAIM `normalize [h; x] = [h; x]`; ASM_MESON_TAC[normal]; DISCH_THEN SUBST1_TAC; CLAIM `LENGTH [h; x] = 2`; ASM_MESON_TAC[LENGTH_PAIR]; STRIP_TAC; REWRITE_TAC[degree]; CLAIM `normal [h; x]`; ASM_MESON_TAC[normal;normalize]; DISCH_THEN (fun x -> ASSUME_TAC x THEN MP_TAC x); REWRITE_TAC[normal]; STRIP_TAC; ASM_REWRITE_TAC[]; ARITH_TAC; STRIP_TAC; ASM_REWRITE_TAC[poly_diff_aux;]; CLAIM `~(&(SUC n) * x = &0)`; ASM_MESON_TAC[normal;normalize;REAL_ENTIRE;ARITH_RULE `~(SUC n = 0)`;REAL_INJ]; STRIP_TAC; CLAIM `degree [&n * h; &(SUC n) * x] = 1`; REWRITE_TAC[degree]; ASM_REWRITE_TAC[normalize;NOT_CONS_NIL;LENGTH;]; ARITH_TAC; STRIP_TAC; ASM_REWRITE_TAC[]; ASM_SIMP_TAC[DEGREE_CONS]; CLAIM `nonconstant t`; ASM_MESON_TAC[nonconstant]; STRIP_TAC; ONCE_REWRITE_TAC[ADD_SYM]; REWRITE_TAC[GSYM ADD1]; ASM_SIMP_TAC[EVEN;ODD]; ASM_MESON_TAC[POLY_DIFF_AUX_DEGREE]; ]);;
(* }}} *)
let poly_diff_parity = 
prove_by_refinement( `!p n. nonconstant p ==> (EVEN (degree p) = ODD (degree (poly_diff p))) /\ (ODD (degree p) = EVEN (degree (poly_diff p)))`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; REWRITE_TAC[nonconstant;normal]; STRIP_TAC; DISCH_ASS; REWRITE_TAC[nonconstant]; STRIP_TAC; REWRITE_TAC[poly_diff]; LIST_SIMP_TAC; CLAIM `~(1 = 0)`; ARITH_TAC; STRIP_TAC; CLAIM `normal t`; MATCH_MP_TAC NORMAL_TAIL; ASM_MESON_TAC[nonconstant;normal]; STRIP_TAC; ASM_SIMP_TAC[DEGREE_CONS]; CASES_ON `?x. t = [x]`; POP_ASSUM MP_TAC THEN STRIP_TAC; CLAIM `~(x = &0)`; ASM_MESON_TAC[normal;normalize]; STRIP_TAC; ASM_REWRITE_TAC[poly_diff_aux;DEGREE_SING;degree;normalize;LENGTH;NOT_CONS_NIL;]; CLAIM `~(&1 * x = &0)`; ASM_MESON_TAC[REAL_ENTIRE;ARITH_RULE `~(&1 = &0)`]; STRIP_TAC; ASM_REWRITE_TAC[LENGTH]; REWRITE_TAC[ARITH_RULE `1 + x = SUC x`]; ASM_MESON_TAC[EVEN;ODD;NOT_EVEN;NOT_ODD;]; CLAIM `nonconstant t`; ASM_MESON_TAC[nonconstant]; DISCH_ASS; DISCH_THEN (fun x -> REWRITE_ASSUMS[x] THEN ASSUME_TAC x); ONCE_REWRITE_TAC[ADD_SYM]; REWRITE_TAC[GSYM ADD1;EVEN;ODD]; CLAIM `?h' t'. t = CONS h' t'`; ASM_MESON_TAC[nonconstant;normal;list_CASES]; STRIP_TAC; POP_ASSUM (fun x -> REWRITE_ASSUMS [x] THEN REWRITE_TAC[x] THEN ASSUME_TAC x); REWRITE_ASSUMS[poly_diff;NOT_CONS_NIL;TL]; REWRITE_TAC[poly_diff_aux]; CLAIM `normal t'`; ASM_MESON_TAC[nonconstant;NORMAL_TAIL;normal]; STRIP_TAC; CLAIM `normal (poly_diff_aux (SUC 1) t')`; ASM_MESON_TAC[POLY_DIFF_AUX_NORMAL2;NOT_SUC]; STRIP_TAC; ASM_SIMP_TAC[DEGREE_CONS]; ONCE_REWRITE_TAC[ADD_SYM]; REWRITE_TAC[GSYM ADD1;EVEN;ODD]; CLAIM `normal (poly_diff_aux 1 t')`; ASM_MESON_TAC[POLY_DIFF_AUX_NORMAL2;ONE;NOT_SUC]; STRIP_TAC; ASM_MESON_TAC[POLY_DIFF_AUX_DEGREE;ONE;NOT_SUC]; ]);;
(* }}} *)
let poly_diff_parity2 = 
prove_by_refinement( `!p n. nonconstant p ==> (ODD (degree (poly_diff p)) = EVEN (degree p)) /\ (EVEN (degree (poly_diff p)) = ODD (degree p))`,
(* {{{ Proof *) [MESON_TAC[poly_diff_parity]]);;
(* }}} *)
let normal_nonconstant = 
prove_by_refinement( `!p. normal p /\ 0 < degree p ==> nonconstant p`,
(* {{{ Proof *) [ REWRITE_TAC[nonconstant]; ASM_MESON_TAC[DEGREE_SING;LT_REFL]; ]);;
(* }}} *)
let nmax_le = 
prove_by_refinement( `!n m. n <= nmax n m /\ m <= nmax n m`,
(* {{{ Proof *) [ REWRITE_TAC[nmax]; REPEAT STRIP_TAC; COND_CASES_TAC; ARITH_TAC; ARITH_TAC; ]);;
(* }}} *)
let POLY_DIFF_UP_LEFT = 
prove_by_refinement( `!p. nonconstant p /\ (?X. !x. x < X ==> poly (poly_diff p) x < &0) ==> (?Y. !y. y < Y ==> &0 < poly p y)`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; CLAIM `mono_unbounded_above (\n. poly p (-- &n))`; REWRITE_TAC[POLY_PNEG]; DISJ_CASES_TAC (ISPEC `degree p` EVEN_OR_ODD); MATCH_MP_TAC mua_quotient_limit; EXISTS_TAC `&1`; EXISTS_TAC `(\n. LAST (pneg p) * &n pow degree (pneg p))`; REPEAT STRIP_TAC; REAL_ARITH_TAC; BETA_TAC; MATCH_MP_TAC LIM_POLY2; MATCH_EQ_MP_TAC NORMAL_PNEG; ASM_MESON_TAC[nonconstant]; MATCH_MP_TAC POW_UNB_CON; STRIP_TAC; REWRITE_TAC[DEGREE_PNEG]; REWRITE_TAC[degree]; CLAIM `normalize p = p`; ASM_MESON_TAC[nonconstant;normal]; DISCH_THEN SUBST1_TAC; CLAIM `~(LENGTH p = 0)`; ASM_MESON_TAC[nonconstant;normal;LENGTH_NZ;LENGTH_0;degree]; STRIP_TAC; CLAIM `~(LENGTH p = 1)`; ASM_MESON_TAC[nonconstant;normal;LENGTH_NZ;LENGTH_1;degree]; POP_ASSUM MP_TAC THEN ARITH_TAC; (* save *) CLAIM `LAST (pneg p) = LAST p`; ASM_MESON_TAC[GSYM POLY_PNEG_LAST;nonconstant;]; DISCH_THEN SUBST1_TAC; ONCE_REWRITE_TAC[REAL_ARITH `x < y <=> ~(x = y) /\ ~(y < x)`]; STRIP_TAC; ASM_MESON_TAC[NORMAL_ID;nonconstant]; STRIP_TAC; CLAIM `ODD (degree (poly_diff p))`; ASM_SIMP_TAC[poly_diff_parity2]; STRIP_TAC; CLAIM `nonconstant (poly_diff p)`; MATCH_MP_TAC normal_nonconstant; STRIP_TAC; MATCH_MP_TAC NONCONSTANT_DIFF_NORMAL; FIRST_ASSUM MATCH_ACCEPT_TAC; POP_ASSUM MP_TAC THEN ARITH_TAC; STRIP_TAC; CLAIM `mono_unbounded_above (\n. poly (poly_diff p) (-- &n))`; MATCH_MP_TAC LAST_UNB_ODD_NEG; ASM_REWRITE_TAC[]; ASM_MESON_TAC[POLY_DIFF_LAST_LT]; REWRITE_TAC[mono_unbounded_above]; DISCH_THEN (MP_TAC o ISPEC `&0`); STRIP_TAC; (* save *) MP_TAC (ISPEC `-- (X - &1)` REAL_ARCH_SIMPLE); DISCH_THEN (X_CHOOSE_TAC `M:num`); CLAIM `-- &M <= X - &1`; POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; STRIP_TAC; LABEL_ALL_TAC; USE_THEN "Z-2" (MP_TAC o ISPEC `nmax M N`); STRIP_TAC; CLAIM `N <= nmax M N`; REWRITE_TAC[nmax_le]; DISCH_THEN (REWRITE_ASSUMS o list); CLAIM `-- &(nmax M N) < X`; MATCH_MP_TAC REAL_LET_TRANS; EXISTS_TAC `-- &M`; STRIP_TAC; REWRITE_TAC[nmax]; REWRITE_TAC[REAL_LE_NEG2; REAL_OF_NUM_LE] THEN ARITH_TAC; USE_THEN "Z-0" MP_TAC THEN ARITH_TAC; STRIP_TAC; ASM_MESON_TAC[ARITH_RULE `~(x < &0 /\ &0 < x)`]; (* save *) REWRITE_TAC[GSYM POLY_PNEG]; MATCH_MP_TAC LAST_UNB_ODD_NEG; ASM_REWRITE_TAC[]; ASM_SIMP_TAC[GSYM POLY_DIFF_LAST_LT]; CASES_ON `?x. poly_diff p = [x]`; POP_ASSUM MP_TAC THEN STRIP_TAC; ASM_REWRITE_TAC[LAST]; LABEL_ALL_TAC; USE_THEN "Z-2" MP_TAC; POP_ASSUM (fun x -> REWRITE_TAC[x] THEN ASSUME_TAC x); REWRITE_TAC[poly]; REAL_SIMP_TAC; REPEAT STRIP_TAC; FIRST_ASSUM MATCH_MP_TAC; EXISTS_TAC `X - &1`; REAL_ARITH_TAC; CLAIM `nonconstant (poly_diff p)`; REWRITE_TAC[nonconstant]; STRIP_TAC; MATCH_MP_TAC POLY_DIFF_NORMAL; FIRST_ASSUM MATCH_ACCEPT_TAC; ASM_MESON_TAC[]; STRIP_TAC; CLAIM `EVEN (degree (poly_diff p))`; ASM_MESON_TAC[poly_diff_parity]; STRIP_TAC; ONCE_REWRITE_TAC[ARITH_RULE `x < y <=> ~(y < x) /\ ~(y = x)`]; REPEAT STRIP_TAC; CLAIM `mono_unbounded_above (\n. poly (poly_diff p) (-- (&n)))`; MATCH_MP_TAC LAST_UNB_EVEN_POS; ASM_REWRITE_TAC[]; REWRITE_TAC[mono_unbounded_above]; DISCH_THEN (MP_TAC o ISPEC `&0`); STRIP_TAC; (* save *) MP_TAC (ISPEC `-- (X - &1)` REAL_ARCH_SIMPLE); DISCH_THEN (X_CHOOSE_TAC `M:num`); CLAIM `-- &M <= X - &1`; POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; STRIP_TAC; LABEL_ALL_TAC; USE_THEN "Z-2" (MP_TAC o ISPEC `nmax M N`); STRIP_TAC; CLAIM `N <= nmax M N`; REWRITE_TAC[nmax_le]; DISCH_THEN (REWRITE_ASSUMS o list); CLAIM `-- &(nmax M N) < X`; MATCH_MP_TAC REAL_LET_TRANS; EXISTS_TAC `-- &M`; STRIP_TAC; REWRITE_TAC[nmax]; REWRITE_TAC[REAL_LE_NEG2; REAL_OF_NUM_LE] THEN ARITH_TAC; USE_THEN "Z-0" MP_TAC THEN ARITH_TAC; STRIP_TAC; ASM_MESON_TAC[ARITH_RULE `~(x < &0 /\ &0 < x)`]; ASM_MESON_TAC[nonconstant;NORMAL_ID]; (* save xxx *) REWRITE_TAC[mono_unbounded_above]; DISCH_THEN (MP_TAC o ISPEC `&0`); STRIP_TAC; MP_TAC (ISPEC `-- (X - &1)` REAL_ARCH_SIMPLE); DISCH_THEN (X_CHOOSE_TAC `M:num`); ABBREV_TAC `k = nmax N M`; EXISTS_TAC `-- &k`; REPEAT STRIP_TAC; REWRITE_TAC [ARITH_RULE `x < y <=> ~(y <= x)`]; STRIP_TAC; MP_TAC (ISPECL [`p:real list`;`y:real`;`-- &k`] POLY_MVT); ASM_REWRITE_TAC[]; STRIP_TAC; LABEL_ALL_TAC; CLAIM `&0 < (-- &k) - y`; USE_THEN "Z-4" MP_TAC THEN REAL_ARITH_TAC; STRIP_TAC; CLAIM `poly (poly_diff p) x < &0`; FIRST_ASSUM MATCH_MP_TAC; MATCH_MP_TAC REAL_LTE_TRANS; EXISTS_TAC `-- &k`; ASM_REWRITE_TAC[]; MATCH_MP_TAC REAL_LE_TRANS; EXISTS_TAC `-- &M`; STRIP_TAC; USE_THEN "Z-5" (SUBST1_TAC o GSYM); REWRITE_TAC[nmax]; REWRITE_TAC[REAL_LE_NEG2; REAL_OF_NUM_LE] THEN ARITH_TAC; USE_THEN "Z-6" MP_TAC THEN REAL_ARITH_TAC; STRIP_TAC; (* save *) CLAIM `N <= k:num`; USE_THEN "Z-5" (SUBST1_TAC o GSYM); REWRITE_TAC[nmax] THEN ARITH_TAC; STRIP_TAC; CLAIM `&0 < poly p (-- &k)`; ASM_MESON_TAC[]; STRIP_TAC; CLAIM `&0 < poly p (-- &k) - poly p y`; LABEL_ALL_TAC; USE_ASSUM_LIST ["Z-10";
"Z-3"] MP_TAC THEN REAL_ARITH_TAC; STRIP_TAC; CLAIM `(-- &k - y) * poly (poly_diff p) x < &0`; REWRITE_TAC[REAL_MUL_LT]; ASM_REWRITE_TAC[]; POP_ASSUM MP_TAC; USE_THEN "Z-0" MP_TAC; REAL_ARITH_TAC; ]);; (* }}} *)
let POLY_DIFF_DOWN_LEFT = 
prove_by_refinement( `!p. nonconstant p /\ (?X. !x. x < X ==> &0 < poly (poly_diff p) x) ==> (?Y. !y. y < Y ==> poly p y < &0)`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; CLAIM `mono_unbounded_below (\n. poly p (-- &n))`; REWRITE_TAC[POLY_PNEG]; DISJ_CASES_TAC (ISPEC `degree p` EVEN_OR_ODD); MATCH_MP_TAC mua_quotient_limit_neg; EXISTS_TAC `&1`; EXISTS_TAC `(\n. LAST (pneg p) * &n pow degree (pneg p))`; REPEAT STRIP_TAC; REAL_ARITH_TAC; BETA_TAC; MATCH_MP_TAC LIM_POLY2; MATCH_EQ_MP_TAC NORMAL_PNEG; ASM_MESON_TAC[nonconstant]; MATCH_MP_TAC POW_UNBB_CON; STRIP_TAC; REWRITE_TAC[DEGREE_PNEG]; REWRITE_TAC[degree]; CLAIM `normalize p = p`; ASM_MESON_TAC[nonconstant;normal]; DISCH_THEN SUBST1_TAC; CLAIM `~(LENGTH p = 0)`; ASM_MESON_TAC[nonconstant;normal;LENGTH_NZ;LENGTH_0;degree]; STRIP_TAC; CLAIM `~(LENGTH p = 1)`; ASM_MESON_TAC[nonconstant;normal;LENGTH_NZ;LENGTH_1;degree]; POP_ASSUM MP_TAC THEN ARITH_TAC; (* save *) CLAIM `LAST (pneg p) = LAST p`; ASM_MESON_TAC[GSYM POLY_PNEG_LAST;nonconstant;]; DISCH_THEN SUBST1_TAC; ONCE_REWRITE_TAC[REAL_ARITH `x < y <=> ~(x = y) /\ ~(y < x)`]; STRIP_TAC; ASM_MESON_TAC[NORMAL_ID;nonconstant]; STRIP_TAC; CLAIM `ODD (degree (poly_diff p))`; ASM_SIMP_TAC[poly_diff_parity2]; STRIP_TAC; CLAIM `nonconstant (poly_diff p)`; MATCH_MP_TAC normal_nonconstant; STRIP_TAC; MATCH_MP_TAC NONCONSTANT_DIFF_NORMAL; FIRST_ASSUM MATCH_ACCEPT_TAC; POP_ASSUM MP_TAC THEN ARITH_TAC; STRIP_TAC; CLAIM `mono_unbounded_below (\n. poly (poly_diff p) (-- &n))`; MATCH_MP_TAC LAST_UNB_ODD_POS; ASM_REWRITE_TAC[]; ASM_MESON_TAC[POLY_DIFF_LAST_GT]; REWRITE_TAC[mono_unbounded_below]; DISCH_THEN (MP_TAC o ISPEC `&0`); STRIP_TAC; (* save *) MP_TAC (ISPEC `-- (X - &1)` REAL_ARCH_SIMPLE); DISCH_THEN (X_CHOOSE_TAC `M:num`); CLAIM `-- &M <= X - &1`; POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; STRIP_TAC; LABEL_ALL_TAC; USE_THEN "Z-2" (MP_TAC o ISPEC `nmax M N`); STRIP_TAC; CLAIM `N <= nmax M N`; REWRITE_TAC[nmax_le]; DISCH_THEN (REWRITE_ASSUMS o list); CLAIM `-- &(nmax M N) < X`; MATCH_MP_TAC REAL_LET_TRANS; EXISTS_TAC `-- &M`; STRIP_TAC; REWRITE_TAC[nmax]; REWRITE_TAC[REAL_LE_NEG2; REAL_OF_NUM_LE] THEN ARITH_TAC; USE_THEN "Z-0" MP_TAC THEN ARITH_TAC; STRIP_TAC; ASM_MESON_TAC[ARITH_RULE `~(x < &0 /\ &0 < x)`]; (* save *) REWRITE_TAC[GSYM POLY_PNEG]; MATCH_MP_TAC LAST_UNB_ODD_POS; ASM_REWRITE_TAC[]; ASM_SIMP_TAC[GSYM POLY_DIFF_LAST_GT]; CASES_ON `?x. poly_diff p = [x]`; POP_ASSUM MP_TAC THEN STRIP_TAC; ASM_REWRITE_TAC[LAST]; LABEL_ALL_TAC; USE_THEN "Z-2" MP_TAC; POP_ASSUM (fun x -> REWRITE_TAC[x] THEN ASSUME_TAC x); REWRITE_TAC[poly]; REAL_SIMP_TAC; REPEAT STRIP_TAC; FIRST_ASSUM MATCH_MP_TAC; EXISTS_TAC `X - &1`; REAL_ARITH_TAC; CLAIM `nonconstant (poly_diff p)`; REWRITE_TAC[nonconstant]; STRIP_TAC; MATCH_MP_TAC POLY_DIFF_NORMAL; FIRST_ASSUM MATCH_ACCEPT_TAC; ASM_MESON_TAC[]; STRIP_TAC; CLAIM `EVEN (degree (poly_diff p))`; ASM_MESON_TAC[poly_diff_parity]; STRIP_TAC; ONCE_REWRITE_TAC[ARITH_RULE `x < y <=> ~(y < x) /\ ~(y = x)`]; REPEAT STRIP_TAC; CLAIM `mono_unbounded_below (\n. poly (poly_diff p) (-- (&n)))`; MATCH_MP_TAC LAST_UNBB_EVEN_NEG; ASM_REWRITE_TAC[]; REWRITE_TAC[mono_unbounded_below]; DISCH_THEN (MP_TAC o ISPEC `&0`); STRIP_TAC; (* save *) MP_TAC (ISPEC `-- (X - &1)` REAL_ARCH_SIMPLE); DISCH_THEN (X_CHOOSE_TAC `M:num`); CLAIM `-- &M <= X - &1`; POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; STRIP_TAC; LABEL_ALL_TAC; USE_THEN "Z-2" (MP_TAC o ISPEC `nmax M N`); STRIP_TAC; CLAIM `N <= nmax M N`; REWRITE_TAC[nmax_le]; DISCH_THEN (REWRITE_ASSUMS o list); CLAIM `-- &(nmax M N) < X`; MATCH_MP_TAC REAL_LET_TRANS; EXISTS_TAC `-- &M`; STRIP_TAC; REWRITE_TAC[nmax]; REWRITE_TAC[REAL_LE_NEG2; REAL_OF_NUM_LE] THEN ARITH_TAC; USE_THEN "Z-0" MP_TAC THEN ARITH_TAC; STRIP_TAC; ASM_MESON_TAC[ARITH_RULE `~(x < &0 /\ &0 < x)`]; ASM_MESON_TAC[nonconstant;NORMAL_ID]; (* save *) REWRITE_TAC[mono_unbounded_below]; DISCH_THEN (MP_TAC o ISPEC `&0`); STRIP_TAC; MP_TAC (ISPEC `-- (X - &1)` REAL_ARCH_SIMPLE); DISCH_THEN (X_CHOOSE_TAC `M:num`); ABBREV_TAC `k = nmax N M`; EXISTS_TAC `-- &k`; REPEAT STRIP_TAC; REWRITE_TAC [ARITH_RULE `x < y <=> ~(y <= x)`]; STRIP_TAC; MP_TAC (ISPECL [`p:real list`;`y:real`;`-- &k`] POLY_MVT); ASM_REWRITE_TAC[]; STRIP_TAC; LABEL_ALL_TAC; CLAIM `&0 < (-- &k) - y`; USE_THEN "Z-4" MP_TAC THEN REAL_ARITH_TAC; STRIP_TAC; CLAIM `&0 < poly (poly_diff p) x`; FIRST_ASSUM MATCH_MP_TAC; MATCH_MP_TAC REAL_LTE_TRANS; EXISTS_TAC `-- &k`; ASM_REWRITE_TAC[]; MATCH_MP_TAC REAL_LE_TRANS; EXISTS_TAC `-- &M`; STRIP_TAC; USE_THEN "Z-5" (SUBST1_TAC o GSYM); REWRITE_TAC[nmax]; REWRITE_TAC[REAL_LE_NEG2; REAL_OF_NUM_LE] THEN ARITH_TAC; USE_THEN "Z-6" MP_TAC THEN REAL_ARITH_TAC; STRIP_TAC; (* save *) CLAIM `N <= k:num`; USE_THEN "Z-5" (SUBST1_TAC o GSYM); REWRITE_TAC[nmax] THEN ARITH_TAC; STRIP_TAC; CLAIM `poly p (-- &k) < &0`; ASM_MESON_TAC[]; STRIP_TAC; CLAIM `poly p (-- &k) - poly p y < &0`; LABEL_ALL_TAC; USE_ASSUM_LIST ["Z-10";
"Z-3"] MP_TAC THEN REAL_ARITH_TAC; STRIP_TAC; CLAIM `&0 < (-- &k - y) * poly (poly_diff p) x`; REWRITE_TAC[REAL_MUL_GT]; ASM_REWRITE_TAC[]; POP_ASSUM MP_TAC; USE_THEN "Z-0" MP_TAC; REAL_ARITH_TAC; ]);; (* }}} *)
let POLY_DIFF_DOWN_LEFT2 = 
prove_by_refinement( `!p X. nonconstant p /\ (!x. x < X ==> &0 < poly (poly_diff p) x) ==> (?Y. Y < X /\ (!y. y < Y ==> poly p y < &0))`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; MP_TAC (ISPEC `p:real list` POLY_DIFF_DOWN_LEFT); ASM_REWRITE_TAC[]; ANTS_TAC; ASM_MESON_TAC[]; STRIP_TAC; EXISTS_TAC `min X Y - &1`; REPEAT STRIP_TAC; REAL_ARITH_TAC; FIRST_ASSUM MATCH_MP_TAC; POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ]);;
(* }}} *)
let POLY_DIFF_UP_LEFT2 = 
prove_by_refinement( `!p X. nonconstant p /\ (!x. x < X ==> poly (poly_diff p) x < &0) ==> (?Y. Y < X /\ (!y. y < Y ==> &0 < poly p y))`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; MP_TAC (ISPEC `p:real list` POLY_DIFF_UP_LEFT); ASM_REWRITE_TAC[]; ANTS_TAC; ASM_MESON_TAC[]; STRIP_TAC; EXISTS_TAC `min X Y - &1`; REPEAT STRIP_TAC; REAL_ARITH_TAC; FIRST_ASSUM MATCH_MP_TAC; POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ]);;
(* }}} *)
let POLY_DIFF_DOWN_LEFT3 = 
prove_by_refinement( `!p p' X. nonconstant p ==> (poly_diff p = p') ==> (!x. x < X ==> &0 < poly p' x) ==> (?Y. Y < X /\ (!y. y < Y ==> poly p y < &0))`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; MP_TAC (ISPEC `p:real list` POLY_DIFF_DOWN_LEFT); ASM_REWRITE_TAC[]; ANTS_TAC; ASM_MESON_TAC[]; STRIP_TAC; EXISTS_TAC `min X Y - &1`; REPEAT STRIP_TAC; REAL_ARITH_TAC; FIRST_ASSUM MATCH_MP_TAC; POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ]);;
(* }}} *)
let POLY_DIFF_UP_LEFT3 = 
prove_by_refinement( `!p p' X. nonconstant p ==> (poly_diff p = p') ==> (!x. x < X ==> poly p' x < &0) ==> (?Y. Y < X /\ (!y. y < Y ==> &0 < poly p y))`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; MP_TAC (ISPEC `p:real list` POLY_DIFF_UP_LEFT); ASM_REWRITE_TAC[]; ANTS_TAC; ASM_MESON_TAC[]; STRIP_TAC; EXISTS_TAC `min X Y - &1`; REPEAT STRIP_TAC; REAL_ARITH_TAC; FIRST_ASSUM MATCH_MP_TAC; POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ]);;
(* }}} *)
let POLY_DIFF_DOWN_LEFT4 = 
prove_by_refinement( `!p p' X. nonconstant p ==> (poly_diff p = p') ==> (!x. x < X ==> &0 < poly p' x) ==> (?Y. Y < X /\ (!y. y <= Y ==> poly p y < &0))`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; MP_TAC (ISPECL[ `p:real list`;`p':real list`;`X:real`] POLY_DIFF_DOWN_LEFT3); ASM_REWRITE_TAC[]; REPEAT STRIP_TAC; EXISTS_TAC `Y - &1`; STRIP_TAC; POP_ASSUM IGNORE; POP_ASSUM MP_TAC; REAL_ARITH_TAC; REPEAT STRIP_TAC; FIRST_ASSUM MATCH_MP_TAC; POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ]);;
(* }}} *)
let POLY_DIFF_UP_LEFT4 = 
prove_by_refinement( `!p p' X. nonconstant p ==> (poly_diff p = p') ==> (!x. x < X ==> poly p' x < &0) ==> (?Y. Y < X /\ (!y. y <= Y ==> &0 < poly p y))`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; MP_TAC (ISPECL[ `p:real list`;`p':real list`;`X:real`] POLY_DIFF_UP_LEFT3); ASM_REWRITE_TAC[]; REPEAT STRIP_TAC; EXISTS_TAC `Y - &1`; STRIP_TAC; POP_ASSUM IGNORE; POP_ASSUM MP_TAC; REAL_ARITH_TAC; REPEAT STRIP_TAC; FIRST_ASSUM MATCH_MP_TAC; POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ]);;
(* }}} *)
let POLY_DIFF_DOWN_LEFT5 = 
prove_by_refinement( `!p p' X. nonconstant p ==> (poly_diff p = p') ==> (!x. x < X ==> poly p' x > &0) ==> (?Y. Y < X /\ (!y. y <= Y ==> poly p y < &0))`,
(* {{{ Proof *) [ REWRITE_TAC[real_gt]; ASM_MESON_TAC[POLY_DIFF_DOWN_LEFT4]; ]);;
(* }}} *)
let POLY_DIFF_UP_LEFT5 = 
prove_by_refinement( `!p p' X. nonconstant p ==> (poly_diff p = p') ==> (!x. x < X ==> poly p' x < &0) ==> (?Y. Y < X /\ (!y. y <= Y ==> poly p y > &0))`,
(* {{{ Proof *) [ REWRITE_TAC[real_gt]; MESON_TAC[POLY_DIFF_UP_LEFT4]; ]);;
(* }}} *)
let NORMAL_PDIFF_LEM = 
prove_by_refinement( `!p. normal (poly_diff p) ==> nonconstant p`,
(* {{{ Proof *) [ LIST_INDUCT_TAC; REWRITE_TAC[normal;poly_diff;poly_diff_aux]; REWRITE_TAC[nonconstant]; REWRITE_TAC[poly_diff;poly_diff_aux;NOT_CONS_NIL;TL;]; REPEAT STRIP_TAC; MATCH_MP_TAC NORMAL_CONS; ASM_MESON_TAC[POLY_DIFF_AUX_NORMAL;ARITH_RULE `~(1 = 0)`]; CLAIM `t = []`; ASM_MESON_TAC !LIST_REWRITES; DISCH_THEN (REWRITE_ASSUMS o list); ASM_MESON_TAC[normal;poly_diff_aux]; ]);;
(* }}} *)
let NORMAL_PDIFF = 
prove_by_refinement( `!p. nonconstant p = normal (poly_diff p)`,
(* {{{ Proof *) [ MESON_TAC[NORMAL_PDIFF_LEM;POLY_DIFF_NORMAL]; ]);;
(* }}} *)
let POLY_DIFF_UP_RIGHT2 = 
prove_by_refinement( `!p p' X. nonconstant p ==> (poly_diff p = p') ==> (!x. X < x ==> &0 < poly p' x) ==> (?Y. X < Y /\ (!y. Y <= y ==> &0 < poly p y))`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; MP_TAC (ISPECL[ `p:real list`] (GEN_ALL POLY_DIFF_UP_RIGHT)); ASM_REWRITE_TAC[]; ANTS_TAC; ASM_MESON_TAC[]; REPEAT STRIP_TAC; EXISTS_TAC `(max X Y) + &1`; STRIP_TAC; REAL_ARITH_TAC; REPEAT STRIP_TAC; FIRST_ASSUM MATCH_MP_TAC; POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ]);;
(* }}} *)
let POLY_DIFF_DOWN_RIGHT2 = 
prove_by_refinement( `!p p' X. nonconstant p ==> (poly_diff p = p') ==> (!x. X < x ==> poly p' x < &0) ==> (?Y. X < Y /\ (!y. Y <= y ==> poly p y < &0))`,
(* {{{ Proof *) [ REPEAT STRIP_TAC; MP_TAC (ISPECL[ `p:real list`] (GEN_ALL POLY_DIFF_DOWN_RIGHT)); ASM_REWRITE_TAC[]; ANTS_TAC; ASM_MESON_TAC[]; REPEAT STRIP_TAC; EXISTS_TAC `(max X Y) + &1`; STRIP_TAC; REAL_ARITH_TAC; REPEAT STRIP_TAC; FIRST_ASSUM MATCH_MP_TAC; POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ]);;
(* }}} *)
let POLY_DIFF_UP_RIGHT3 = 
prove_by_refinement( `!p p' X. nonconstant p ==> (poly_diff p = p') ==> (!x. X < x ==> poly p' x > &0) ==> (?Y. X < Y /\ (!y. Y <= y ==> poly p y > &0))`,
(* {{{ Proof *) [ REWRITE_TAC[real_gt;real_ge]; MESON_TAC[POLY_DIFF_UP_RIGHT2]; ]);;
(* }}} *)
let POLY_DIFF_DOWN_RIGHT3 = 
prove_by_refinement( `!p p' X. nonconstant p ==> (poly_diff p = p') ==> (!x. X < x ==> poly p' x < &0) ==> (?Y. X < Y /\ (!y. Y <= y ==> poly p y < &0))`,
(* {{{ Proof *) [ REWRITE_TAC[real_gt;real_ge]; MESON_TAC[POLY_DIFF_DOWN_RIGHT2]; ]);;
(* }}} *)