(* ========================================================================= *)
(* Calculation with real numbers (Boehm-style but by inference).             *)
(* ========================================================================= *)

needs "Library/transc.ml";;

let REAL_SUB_SUM0 = 
prove (`!x y m. sum(0,m) x - sum(0,m) y = sum(0,m) (\i. x i - y i)`,
CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[sum] THEN REAL_ARITH_TAC);;
let REAL_MUL_RSUM0 = 
prove (`!m c x. c * sum(0,m) x = sum(0,m) (\i. c * x(i))`,
INDUCT_TAC THEN ASM_REWRITE_TAC[sum; REAL_MUL_RZERO; REAL_ADD_LDISTRIB]);;
let REAL_ABS_LEMMA = 
prove (`!a b n. (&a pow n) * abs b = abs((&a pow n) * b)`,
let REAL_ABS_LEMMA1 = 
prove (`!a b. &a * abs b = abs(&a * b)`,
REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_NUM]);;
let REAL_ABS_TRIANGLE_LEMMA = 
prove (`!u x y z. abs(x - y) + abs(z - x) < u ==> abs(z - y) < u`,
REAL_ARITH_TAC);;
let REAL_MONO_POW2 = 
prove (`!m n. m <= n ==> &2 pow m <= &2 pow n`,
REPEAT GEN_TAC THEN REWRITE_TAC[LE_EXISTS] THEN DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN SPEC_TAC(`d:num`,`d:num`) THEN INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; real_pow; REAL_LE_REFL] THEN POP_ASSUM MP_TAC THEN MP_TAC(SPEC `m:num` REAL_LT_POW2) THEN REAL_ARITH_TAC);;
let REAL_LE_SUC_POW2 = 
prove (`!m. &2 pow m + &1 <= &2 pow (SUC m)`,
GEN_TAC THEN REWRITE_TAC[real_pow; REAL_MUL_2; REAL_LE_LADD; REAL_LE_POW2]);;
let REAL_OPPSIGN_LEMMA = 
prove (`!x y. (x * y < &0) <=> (x < &0 /\ &0 < y) \/ (&0 < x /\ y < &0)`,
REPEAT GEN_TAC THEN REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC (SPEC `x:real` REAL_LT_NEGTOTAL) THEN REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC (SPEC `y:real` REAL_LT_NEGTOTAL) THEN ASM_REWRITE_TAC[REAL_MUL_LZERO; REAL_MUL_RZERO; REAL_LT_REFL] THEN POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN DISCH_THEN(fun th -> MP_TAC(MATCH_MP REAL_LT_MUL th) THEN MP_TAC th) THEN REWRITE_TAC[REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_NEG_NEG] THEN REAL_ARITH_TAC);;
let REAL_OPPSIGN = 
prove (`(&0 < x ==> &0 <= y) /\ (x < &0 ==> y <= &0) <=> &0 <= x * y`,
REWRITE_TAC[GSYM REAL_NOT_LT; REAL_OPPSIGN_LEMMA] THEN REAL_ARITH_TAC);;
let REAL_NDIV_LEMMA1a = 
prove (`!a m n. &2 * abs(&2 pow m * &a - &2 pow (m + n)) <= &2 pow m ==> (&a = &2 pow n)`,
REPEAT GEN_TAC THEN REWRITE_TAC[REAL_POW_ADD; GSYM REAL_SUB_LDISTRIB] THEN REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_POW; REAL_ABS_NUM] THEN REWRITE_TAC[REAL_OF_NUM_POW] THEN REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC (SPECL [`a:num`; `2 EXP n`] LT_CASES) THEN ASM_REWRITE_TAC[] THEN CONV_TAC CONTRAPOS_CONV THEN DISCH_THEN(K ALL_TAC) THEN POP_ASSUM(X_CHOOSE_THEN `d:num` SUBST1_TAC o REWRITE_RULE[LT_EXISTS]) THEN REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN REWRITE_TAC[REAL_ARITH `((a + b) - a = b) /\ (a - (a + b) = --b)`] THEN REWRITE_TAC[REAL_ABS_NEG; REAL_NOT_LE; REAL_ABS_NUM] THEN REWRITE_TAC[ADD1; GSYM REAL_OF_NUM_ADD] THEN REWRITE_TAC[REAL_MUL_2; REAL_ADD_LDISTRIB; REAL_ADD_RDISTRIB] THEN REWRITE_TAC[REAL_MUL_RID; REAL_ADD_ASSOC; REAL_LT_ADDL] THEN MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&(2 EXP m)` THEN REWRITE_TAC[REAL_LT_POW2; GSYM REAL_OF_NUM_POW] THEN ONCE_REWRITE_TAC[AC REAL_ADD_AC `(a + b) + c = b + (a + c)`] THEN REWRITE_TAC[GSYM REAL_MUL_2; REAL_LE_ADDR] THEN MATCH_MP_TAC REAL_LE_MUL THEN REWRITE_TAC[REAL_POS] THEN MATCH_MP_TAC REAL_LE_MUL THEN REWRITE_TAC[REAL_POS] THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN REWRITE_TAC[REAL_LT_POW2]);;
let REAL_NDIV_LEMMA1b = 
prove (`!a m n. ~(&2 * abs(-- (&2 pow m * &a) - &2 pow (m + n)) <= &2 pow m)`,
REPEAT GEN_TAC THEN REWRITE_TAC[real_sub; GSYM REAL_NEG_ADD] THEN REWRITE_TAC[REAL_ABS_NEG; REAL_POW_ADD] THEN REWRITE_TAC[REAL_ABS_MUL; GSYM REAL_ADD_LDISTRIB] THEN SUBGOAL_THEN `&0 <= &a + &2 pow n` ASSUME_TAC THENL [MATCH_MP_TAC REAL_LE_ADD THEN REWRITE_TAC[REAL_POS] THEN MATCH_MP_TAC REAL_POW_LE THEN REWRITE_TAC[REAL_POS]; REWRITE_TAC[REAL_ABS_POW; REAL_ABS_NUM] THEN ASM_REWRITE_TAC[real_abs; REAL_NOT_LE] THEN MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `(&2 * &2 pow m) * &1` THEN CONJ_TAC THENL [REWRITE_TAC[REAL_MUL_RID; REAL_MUL_2] THEN REWRITE_TAC[REAL_LT_ADDR; REAL_LT_POW2]; REWRITE_TAC[REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LE_LMUL THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LE_MUL THEN REWRITE_TAC[REAL_POS] THEN MATCH_MP_TAC REAL_POW_LE THEN REWRITE_TAC[REAL_POS]; MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 pow n` THEN REWRITE_TAC[REAL_LE_POW2; REAL_LE_ADDL; REAL_POS]]]]);;
let REAL_NDIV_LEMMA2 = 
prove (`!a b m n. (?k. (b = &k) \/ (b = --(&k))) /\ (abs(a) = &2 pow m) /\ &2 * abs(a * b - &2 pow (m + n)) <= abs(a) ==> (a * b = &2 pow (m + n))`,
REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN DISJ_CASES_THEN SUBST1_TAC (REAL_ARITH `(a = abs a) \/ (a = --(abs a))`) THEN ASM_REWRITE_TAC[REAL_MUL_LNEG; REAL_MUL_RNEG] THEN REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_POW; REAL_ABS_NUM; REAL_NEG_NEG] THEN REWRITE_TAC[REAL_NDIV_LEMMA1b] THEN DISCH_THEN(SUBST1_TAC o MATCH_MP REAL_NDIV_LEMMA1a) THEN REWRITE_TAC[REAL_POW_ADD]);;
let REAL_NDIV_LEMMA3 = 
prove (`!a b m n. m <= n /\ (?k. (b = &k) \/ (b = --(&k))) /\ (abs(a) = &2 pow m) /\ &2 * abs(a * b - &2 pow n) <= abs(a) ==> (a * b = &2 pow n)`,
REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN POP_ASSUM(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[LE_EXISTS]) THEN REWRITE_TAC[REAL_NDIV_LEMMA2]);;
(* ------------------------------------------------------------------------- *) (* Surely there is already an efficient way to do this... *) (* ------------------------------------------------------------------------- *) let log2 = (*** least p >= 0 with x <= 2^p ***) let rec log2 x y = if x </ Int 1 then y else log2 (quo_num x (Int 2)) (y +/ Int 1) in fun x -> log2 (x -/ Int 1) (Int 0);; (* ------------------------------------------------------------------------- *) (* Theorems justifying the steps. *) (* ------------------------------------------------------------------------- *)
let REALCALC_DOWNGRADE = 
prove (`(SUC d0 = d) ==> (n + d = n0) ==> abs(a - &2 pow n0 * x) < &1 ==> abs((&2 pow d) * b - a) <= &2 pow d0 ==> abs(b - &2 pow n * x) < &1`,
DISCH_THEN(SUBST1_TAC o SYM) THEN DISCH_THEN(SUBST1_TAC o SYM) THEN REPEAT DISCH_TAC THEN MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN EXISTS_TAC `&2 pow (SUC d0)` THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_POW_LT THEN REAL_ARITH_TAC; REWRITE_TAC[REAL_ABS_LEMMA; REAL_MUL_RID; REAL_SUB_LDISTRIB] THEN MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&2 pow d0 + &2 pow d0` THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_ABS_TRIANGLE_LEMMA THEN EXISTS_TAC `a:real` THEN MATCH_MP_TAC REAL_LTE_ADD2 THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&1` THEN REWRITE_TAC[REAL_MUL_ASSOC; GSYM REAL_POW_ADD] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN ASM_REWRITE_TAC[] THEN SPEC_TAC(`d0:num`,`d0:num`) THEN INDUCT_TAC THEN REWRITE_TAC[real_pow; REAL_LE_REFL] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&1 + &1` THEN REWRITE_TAC[REAL_MUL_2] THEN CONJ_TAC THENL [REAL_ARITH_TAC; MATCH_MP_TAC REAL_LE_ADD2 THEN ASM_REWRITE_TAC[]]; REWRITE_TAC[real_pow; GSYM REAL_MUL_2; REAL_LE_REFL]]]);;
let REALCALC_INT = 
prove (`abs((&2 pow n) * a - (&2 pow n) * a) < &1`,
let REALCALC_NEG = 
prove (`abs(a - (&2 pow n) * x) < &1 ==> abs(--a - (&2 pow n) * --x) < &1`,
REWRITE_TAC[real_sub; GSYM REAL_NEG_ADD] THEN REWRITE_TAC[REAL_ABS_NEG; REAL_MUL_RNEG]);;
let REALCALC_ABS = 
prove (`abs(a - &2 pow n * x) < &1 ==> abs(abs(a) - &2 pow n * abs(x)) < &1`,
DISCH_TAC THEN REWRITE_TAC[REAL_ABS_LEMMA] THEN MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `abs(a - (&2 pow n) * x)` THEN ASM_REWRITE_TAC[REAL_ABS_SUB_ABS]);;
let REALCALC_INV_LEMMA = 
prove (`(?m. (b = &m) \/ (b = --(&m))) /\ (?m. (a = &m) \/ (a = --(&m))) /\ SUC(n + k) <= (2 * e) /\ &2 pow e <= abs(a) /\ abs(a - &2 pow k * x) < &1 /\ &2 * abs(a * b - &2 pow (n + k)) <= abs(a) ==> abs(b - &2 pow n * inv(x)) < &1`,
let lemma1 = REAL_ARITH `!x y z b. &2 * abs(x - y) <= b /\ &2 * abs(y - z) < b ==> &2 * abs(x - z) < &2 * b` in let lemma2 = REAL_ARITH `!x y z. x + &1 <= abs(z) /\ abs(z - y) < &1 ==> x <= abs(y)` in let lemma3 = REAL_ARITH `(abs(x) <= &1 /\ &0 < abs(y) /\ abs(y) < &1) /\ (&0 < x ==> &0 <= y) /\ (x < &0 ==> y <= &0) ==> abs(x - y) < &1` in let lemma4 = REAL_ARITH `!a b c. c <= abs(a) + abs(b) /\ abs(a - b) < c ==> (&0 < a ==> &0 <= b) /\ (a < &0 ==> b <= &0)` in DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN SUBGOAL_THEN `~(a = &0)` ASSUME_TAC THENL [DISCH_THEN SUBST_ALL_TAC THEN UNDISCH_TAC `&2 pow e <= abs(&0)` THEN REWRITE_TAC[REAL_ABS_0; GSYM REAL_NOT_LT; REAL_LT_POW2]; ALL_TAC] THEN SUBGOAL_THEN `~(x = &0)` ASSUME_TAC THENL [DISCH_THEN SUBST_ALL_TAC THEN UNDISCH_TAC `abs(a - &2 pow k * &0) < &1` THEN REWRITE_TAC[REAL_MUL_RZERO; REAL_SUB_RZERO; REAL_NOT_LT] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 pow e` THEN ASM_REWRITE_TAC[REAL_LE_POW2]; ALL_TAC] THEN SUBGOAL_THEN `(&2 pow e + &1 <= abs(a)) \/ (&2 pow e = abs(a))` MP_TAC THENL [REWRITE_TAC[REAL_OF_NUM_POW] THEN FIRST_ASSUM(CHOOSE_THEN(DISJ_CASES_THEN SUBST_ALL_TAC)) THEN REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_NUM] THEN RULE_ASSUM_TAC(REWRITE_RULE[REAL_ABS_NEG; REAL_ABS_NUM]) THEN REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_LE; REAL_OF_NUM_EQ] THEN REWRITE_TAC[GSYM ADD1; LE_SUC_LT; GSYM LE_LT] THEN ASM_REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_POW]; UNDISCH_TAC `&2 pow e <= abs(a)` THEN DISCH_THEN(K ALL_TAC)] THEN DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL [DISCH_TAC THEN MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN EXISTS_TAC `&2 * abs(a)` THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[GSYM REAL_ABS_NZ] THEN REAL_ARITH_TAC; REWRITE_TAC[GSYM REAL_MUL_ASSOC; GSYM REAL_ABS_MUL] THEN REWRITE_TAC[REAL_SUB_LDISTRIB; REAL_MUL_RID] THEN MATCH_MP_TAC lemma1 THEN EXISTS_TAC `&2 pow (n + k)` THEN ASM_REWRITE_TAC[]] THEN GEN_REWRITE_TAC (LAND_CONV o funpow 3 RAND_CONV) [REAL_MUL_SYM] THEN REWRITE_TAC[REAL_POW_ADD; GSYM REAL_MUL_ASSOC] THEN REWRITE_TAC[GSYM REAL_SUB_LDISTRIB; REAL_ABS_MUL] THEN MATCH_MP_TAC REAL_LT_RCANCEL_IMP THEN EXISTS_TAC `abs(x)` THEN ASM_REWRITE_TAC[GSYM REAL_ABS_NZ] THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN ONCE_REWRITE_TAC[GSYM REAL_ABS_MUL] THEN MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&2 * abs(&2 pow n) * &1` THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LT_LMUL THEN CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC] THEN MATCH_MP_TAC REAL_LT_LMUL THEN CONJ_TAC THENL [REWRITE_TAC[GSYM REAL_ABS_NZ; REAL_POW_EQ_0] THEN CONV_TAC(RAND_CONV(LAND_CONV REAL_INT_EQ_CONV)) THEN REWRITE_TAC[]; REWRITE_TAC[REAL_SUB_RDISTRIB] THEN ONCE_REWRITE_TAC[REAL_ABS_SUB] THEN GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o LAND_CONV) [REAL_MUL_SYM] THEN REWRITE_TAC[REAL_MUL_ASSOC] THEN FIRST_ASSUM(fun th -> REWRITE_TAC[MATCH_MP REAL_MUL_RINV th]) THEN ASM_REWRITE_TAC[REAL_MUL_LID]]; ALL_TAC] THEN MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN EXISTS_TAC `&2 pow k` THEN REWRITE_TAC[REAL_LT_POW2; REAL_MUL_RID; REAL_ABS_LEMMA] THEN ONCE_REWRITE_TAC [AC REAL_MUL_AC `a * b * c = (a * c) * b`] THEN REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_POW; REAL_ABS_NUM] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 pow e * &2 pow e` THEN CONJ_TAC THENL [ONCE_REWRITE_TAC [AC REAL_MUL_AC `(a * b) * c = c * b * a`] THEN REWRITE_TAC[GSYM REAL_POW_ADD; GSYM(CONJUNCT2 real_pow)] THEN MATCH_MP_TAC REAL_MONO_POW2 THEN ASM_REWRITE_TAC[GSYM MULT_2]; MATCH_MP_TAC REAL_LE_MUL2 THEN REPEAT CONJ_TAC THENL [MATCH_MP_TAC REAL_LT_IMP_LE THEN REWRITE_TAC[REAL_LT_POW2]; REWRITE_TAC[REAL_ABS_LEMMA] THEN MATCH_MP_TAC lemma2 THEN EXISTS_TAC `a:real` THEN ASM_REWRITE_TAC[]; MATCH_MP_TAC REAL_LT_IMP_LE THEN REWRITE_TAC[REAL_LT_POW2]; MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 pow e + &1` THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC]]; DISCH_TAC THEN DISJ_CASES_TAC (SPECL [`e:num`; `n + k:num`] LET_CASES) THENL [SUBGOAL_THEN `a * b = &2 pow (n + k)` ASSUME_TAC THENL [MATCH_MP_TAC REAL_NDIV_LEMMA3 THEN EXISTS_TAC `e:num` THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN EXISTS_TAC `abs(a)` THEN ASM_REWRITE_TAC[GSYM REAL_ABS_NZ; GSYM REAL_ABS_MUL] THEN ASM_REWRITE_TAC[REAL_SUB_LDISTRIB] THEN ONCE_REWRITE_TAC[AC REAL_MUL_AC `a * b * c = b * a * c`] THEN REWRITE_TAC[REAL_POW_ADD; GSYM REAL_SUB_LDISTRIB] THEN REWRITE_TAC[REAL_ABS_MUL; REAL_MUL_RID] THEN MATCH_MP_TAC REAL_LT_RCANCEL_IMP THEN EXISTS_TAC `abs(x)` THEN ASM_REWRITE_TAC[GSYM REAL_ABS_NZ; GSYM REAL_MUL_ASSOC] THEN GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM REAL_ABS_MUL] THEN REWRITE_TAC[REAL_SUB_RDISTRIB; GSYM REAL_MUL_ASSOC] THEN REWRITE_TAC[MATCH_MP REAL_MUL_LINV (ASSUME `~(x = &0)`)] THEN ONCE_REWRITE_TAC[REAL_ABS_SUB] THEN MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&2 pow n * &1` THEN CONJ_TAC THENL [REWRITE_TAC[REAL_ABS_POW; REAL_ABS_NUM] THEN MATCH_MP_TAC REAL_LT_LMUL THEN ASM_REWRITE_TAC[REAL_LT_POW2; REAL_MUL_RID]; MATCH_MP_TAC REAL_LE_RCANCEL_IMP THEN EXISTS_TAC `&2 pow (SUC k)` THEN REWRITE_TAC[REAL_MUL_RID; REAL_LT_POW2]] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 pow (2 * e)` THEN CONJ_TAC THENL [REWRITE_TAC[GSYM REAL_POW_ADD; ADD_CLAUSES] THEN MATCH_MP_TAC REAL_MONO_POW2 THEN ASM_REWRITE_TAC[]; SUBST1_TAC(SYM(ASSUME `&2 pow e = abs(a)`)) THEN REWRITE_TAC[MULT_2; REAL_POW_ADD; GSYM REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[MATCH_MP REAL_LT_IMP_LE (SPEC_ALL REAL_LT_POW2)]] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[real_pow] THEN SUBGOAL_THEN `?d. e = SUC d` (CHOOSE_THEN SUBST_ALL_TAC) THENL [UNDISCH_TAC `SUC (n + k) <= (2 * e)` THEN SPEC_TAC(`e:num`,`e:num`) THEN INDUCT_TAC THEN REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES; LE; NOT_SUC] THEN REWRITE_TAC[SUC_INJ; GSYM EXISTS_REFL]; REWRITE_TAC[real_pow; GSYM REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_POS] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 pow (SUC d) - &1` THEN REWRITE_TAC[REAL_LE_SUB_RADD; REAL_LE_SUB_LADD] THEN REWRITE_TAC[REAL_LE_SUC_POW2] THEN SUBGOAL_THEN `abs(abs a - &2 pow k * abs(x)) < &1` MP_TAC THENL [REWRITE_TAC[REAL_ABS_LEMMA] THEN MATCH_MP_TAC(REAL_LET_IMP REAL_ABS_SUB_ABS) THEN ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC]]; SUBGOAL_THEN `abs(b) <= &1 /\ &0 <= a * b` STRIP_ASSUME_TAC THENL [ASM_CASES_TAC `b = &0` THEN ASM_REWRITE_TAC[REAL_ABS_0; REAL_MUL_RZERO; REAL_POS] THEN SUBGOAL_THEN `abs(a) <= abs(a * b)` ASSUME_TAC THENL [GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM REAL_MUL_RID] THEN REWRITE_TAC[REAL_ABS_MUL] THEN MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN SUBGOAL_THEN `?q. abs(b) = &q` CHOOSE_TAC THENL [UNDISCH_TAC `?m. (b = &m) \/ (b = --(&m))` THEN DISCH_THEN(X_CHOOSE_THEN `p:num` DISJ_CASES_TAC) THEN EXISTS_TAC `p:num` THEN ASM_REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_NUM]; UNDISCH_TAC `~(b = &0)` THEN ASM_REWRITE_TAC[REAL_ABS_NZ] THEN REWRITE_TAC[REAL_ABS_NUM; REAL_OF_NUM_LE; REAL_OF_NUM_LT] THEN REWRITE_TAC[SYM(REWRITE_CONV[ARITH_SUC] `SUC 0`)] THEN REWRITE_TAC[LE_SUC_LT]]; ALL_TAC] THEN SUBGOAL_THEN `abs(a * b) <= abs(a) /\ &0 <= a * b` ASSUME_TAC THENL [MP_TAC(SPEC `(n:num) + k` REAL_LT_POW2) THEN UNDISCH_TAC `&2 * abs(a * b - &2 pow (n + k)) <= abs a` THEN UNDISCH_TAC `abs(a) <= abs(a * b)` THEN SUBGOAL_THEN `~(a * b = &0)` MP_TAC THENL [ASM_REWRITE_TAC[REAL_ENTIRE]; ALL_TAC] THEN SUBGOAL_THEN `&2 * &2 pow (n + k) <= abs(a)` MP_TAC THENL [REWRITE_TAC[GSYM(CONJUNCT2 real_pow)] THEN FIRST_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [SYM th]) THEN MATCH_MP_TAC REAL_MONO_POW2 THEN ASM_REWRITE_TAC[LE_SUC_LT]; REAL_ARITH_TAC]; ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN EXISTS_TAC `abs(a)` THEN ASM_REWRITE_TAC [GSYM REAL_ABS_NZ; GSYM REAL_ABS_MUL; REAL_MUL_RID]]; ALL_TAC] THEN MATCH_MP_TAC lemma3 THEN CONJ_TAC THENL [ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [ASM_REWRITE_TAC[GSYM REAL_ABS_NZ; REAL_ENTIRE; REAL_INV_EQ_0] THEN MATCH_MP_TAC REAL_LT_IMP_NZ THEN REWRITE_TAC[REAL_LT_POW2]; MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN EXISTS_TAC `abs(x)` THEN ASM_REWRITE_TAC[GSYM REAL_ABS_NZ; GSYM REAL_ABS_MUL] THEN ONCE_REWRITE_TAC[AC REAL_MUL_AC `a * b * c = b * c * a`] THEN SUBGOAL_THEN `inv(x) * x = &1` SUBST1_TAC THENL [MATCH_MP_TAC REAL_MUL_LINV THEN ASM_REWRITE_TAC[]; REWRITE_TAC[REAL_MUL_RID] THEN MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN EXISTS_TAC `&2 pow k` THEN REWRITE_TAC[REAL_LT_POW2; REAL_ABS_LEMMA] THEN MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `&2 pow (SUC(n + k)) - &1` THEN REWRITE_TAC[REAL_LT_SUB_RADD; REAL_LE_SUB_LADD] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[GSYM REAL_POW_ADD] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[REAL_LE_SUC_POW2; REAL_ABS_POW; REAL_ABS_NUM] THEN MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `&2 pow e` THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_MONO_POW2 THEN ASM_REWRITE_TAC[LE_SUC_LT]; UNDISCH_TAC `abs(a - &2 pow k * x) < &1` THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC]]]; SUBGOAL_THEN `&0 <= b * (&2 pow n * inv x)` MP_TAC THENL [MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN EXISTS_TAC `a * a` THEN ASM_REWRITE_TAC[REAL_LT_SQUARE] THEN REWRITE_TAC[REAL_MUL_RZERO] THEN ONCE_REWRITE_TAC[AC REAL_MUL_AC `(a * b) * c * d = (a * c) * (b * d)`] THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN EXISTS_TAC `x * x` THEN ASM_REWRITE_TAC[REAL_LT_SQUARE] THEN REWRITE_TAC[REAL_MUL_RZERO] THEN ONCE_REWRITE_TAC[AC REAL_MUL_AC `(a * b) * c * d * e = d * (e * a) * c * b`] THEN MATCH_MP_TAC REAL_LE_MUL THEN REWRITE_TAC[MATCH_MP REAL_LT_IMP_LE (SPEC_ALL REAL_LT_POW2)] THEN FIRST_ASSUM(fun th -> GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) [MATCH_MP REAL_MUL_LINV th]) THEN MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN EXISTS_TAC `&2 pow k` THEN REWRITE_TAC[REAL_LT_POW2; REAL_MUL_RZERO; REAL_MUL_LID] THEN ONCE_REWRITE_TAC[AC REAL_MUL_AC `a * b * c = b * (a * c)`] THEN ONCE_REWRITE_TAC[GSYM REAL_OPPSIGN] THEN MATCH_MP_TAC lemma4 THEN EXISTS_TAC `&1` THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `abs(a)` THEN CONJ_TAC THENL [UNDISCH_TAC `?m. (a = & m) \/ (a = -- (& m))` THEN DISCH_THEN(CHOOSE_THEN(DISJ_CASES_THEN SUBST_ALL_TAC)) THEN ASM_REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_NUM] THEN REWRITE_TAC[REAL_OF_NUM_LE] THEN REWRITE_TAC[SYM(REWRITE_CONV[ARITH_SUC] `SUC 0`)] THEN REWRITE_TAC[LE_SUC_LT] THEN RULE_ASSUM_TAC (REWRITE_RULE[REAL_ARITH `(--x = &0) = (x = &0)`]) THEN UNDISCH_TAC `~(&m = &0)` THEN REWRITE_TAC[REAL_OF_NUM_EQ] THEN CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[NOT_LT; LE]; REWRITE_TAC[REAL_LE_ADDR; REAL_ABS_POS]]; REWRITE_TAC[REAL_OPPSIGN]]]]]);;
let REALCALC_INV = 
prove (`abs(a - &2 pow k * x) < &1 ==> (?m. (a = &m) \/ (a = --(&m))) ==> (?m. (b = &m) \/ (b = --(&m))) ==> SUC(n + k) <= (2 * e) ==> &2 pow e <= abs(a) ==> &2 * abs(a * b - &2 pow (n + k)) <= abs(a) ==> abs(b - &2 pow n * inv(x)) < &1`,
REPEAT DISCH_TAC THEN MATCH_MP_TAC REALCALC_INV_LEMMA THEN ASM_REWRITE_TAC[]);;
let REALCALC_ADD = 
prove (`(n + 2 = n') ==> abs(a - &2 pow n' * x) < &1 ==> abs(b - &2 pow n' * y) < &1 ==> abs(&4 * c - (a + b)) <= &2 ==> abs(c - &2 pow n * (x + y)) < &1`,
DISCH_THEN(SUBST_ALL_TAC o SYM) THEN REPEAT DISCH_TAC THEN MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN EXISTS_TAC `&2 pow 2` THEN CONV_TAC(LAND_CONV REAL_INT_REDUCE_CONV) THEN REWRITE_TAC[REAL_ABS_LEMMA; REAL_SUB_LDISTRIB; REAL_MUL_RID] THEN REWRITE_TAC[REAL_MUL_ASSOC; GSYM REAL_POW_ADD] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN SUBST1_TAC(REAL_INT_REDUCE_CONV `&2 pow 2`) THEN MATCH_MP_TAC REAL_ABS_TRIANGLE_LEMMA THEN EXISTS_TAC `a + b` THEN GEN_REWRITE_TAC RAND_CONV [SYM(REAL_INT_REDUCE_CONV `&2 + &2`)] THEN MATCH_MP_TAC REAL_LTE_ADD2 THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC [REAL_ARITH `(x + y) - a * (u + v) = (x - a * u) + (y - a * v)`] THEN GEN_REWRITE_TAC RAND_CONV [SYM(REAL_INT_REDUCE_CONV `&1 + &1`)] THEN MATCH_MP_TAC(REAL_LET_IMP REAL_ABS_TRIANGLE) THEN MATCH_MP_TAC REAL_LT_ADD2 THEN ASM_REWRITE_TAC[]);;
let REALCALC_MUL = 
prove (`abs(a - &2 pow k * x) < &1 ==> abs(b - &2 pow l * y) < &1 ==> (n + m = k + l) ==> &2 * (abs(a) + abs(b) + &1) <= &2 pow m ==> &2 * abs(&2 pow m * c - a * b) <= &2 pow m ==> abs(c - &2 pow n * (x * y)) < &1`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN EXISTS_TAC `&2 pow m` THEN REWRITE_TAC[REAL_LT_POW2; REAL_ABS_LEMMA; REAL_SUB_LDISTRIB] THEN MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN EXISTS_TAC `&2` THEN CONV_TAC(LAND_CONV (EQT_INTRO o REAL_ARITH)) THEN REWRITE_TAC[REAL_MUL_RID] THEN GEN_REWRITE_TAC RAND_CONV [REAL_MUL_2] THEN MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `&2 * abs(&2 pow m * c - a * b) + &2 * abs(a * b - &2 pow m * &2 pow n * x * y)` THEN CONV_TAC(LAND_CONV (EQT_INTRO o REAL_ARITH)) THEN REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LET_ADD2 THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_MUL_ASSOC; GSYM REAL_POW_ADD] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_POW_ADD] THEN ONCE_REWRITE_TAC[AC REAL_MUL_AC `((a * b) * c) * d = (a * c) * (b * d)`] THEN SUBGOAL_THEN `?d. abs(d) < &1 /\ (&2 pow k * x = a + d)` MP_TAC THENL [EXISTS_TAC `&2 pow k * x - a` THEN UNDISCH_TAC `abs(a - &2 pow k * x) < &1` THEN REAL_ARITH_TAC; DISCH_THEN(CHOOSE_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST1_TAC))] THEN SUBGOAL_THEN `?e. abs(e) < &1 /\ (&2 pow l * y = b + e)` MP_TAC THENL [EXISTS_TAC `&2 pow l * y - b` THEN UNDISCH_TAC `abs(b - &2 pow l * y) < &1` THEN REAL_ARITH_TAC; DISCH_THEN(CHOOSE_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST1_TAC))] THEN MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&2 * (abs(a) * &1 + abs(b) * &1 + &1 * &1)` THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LT_LMUL THEN CONV_TAC(LAND_CONV (EQT_INTRO o REAL_ARITH)) THEN REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `abs(a) * abs(e) + abs(b) * abs(d) + abs(d) * abs(e)` THEN CONJ_TAC THENL [REWRITE_TAC[GSYM REAL_ABS_MUL] THEN REAL_ARITH_TAC; MATCH_MP_TAC REAL_LET_ADD2 THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[]; MATCH_MP_TAC REAL_LET_ADD2 THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[]; MATCH_MP_TAC REAL_LT_MUL2 THEN ASM_REWRITE_TAC[REAL_ABS_POS]]]]; ASM_REWRITE_TAC[REAL_MUL_RID]]);;
(* ------------------------------------------------------------------------- *) (* Square root. *) (* ------------------------------------------------------------------------- *)
let REALCALC_SQRT = 
prove (`abs(a - &2 pow n * x) < &1 ==> &1 <= x ==> abs(b pow 2 - &2 pow n * a) <= b ==> abs(b - &2 pow n * sqrt(x)) < &1`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN EXISTS_TAC `abs(b + &2 pow n * sqrt(x))` THEN CONJ_TAC THENL [MATCH_MP_TAC(REAL_ARITH `!z. abs(z) <= b /\ &0 < c ==> &0 < abs(b + c)`) THEN EXISTS_TAC `b pow 2 - &2 pow n * a` THEN ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[REAL_POW_LT; REAL_OF_NUM_LT; ARITH; REAL_LT_MUL; SQRT_POS_LT; REAL_ARITH `&1 <= x ==> &0 < x`]; ALL_TAC] THEN REWRITE_TAC[GSYM REAL_ABS_MUL; REAL_MUL_RID] THEN ONCE_REWRITE_TAC[REAL_ARITH `(a + b) * (a - b) = a * a - b * b`] THEN MATCH_MP_TAC(REAL_ARITH `!c d. abs(b - c) <= d /\ abs(c - a) < e - d ==> abs(b - a) < e`) THEN MAP_EVERY EXISTS_TAC [`&2 pow n * a`; `b:real`] THEN ASM_REWRITE_TAC[GSYM REAL_POW_2] THEN REWRITE_TAC[REAL_POW_2; GSYM REAL_MUL_ASSOC] THEN REWRITE_TAC[GSYM REAL_SUB_LDISTRIB; REAL_ABS_MUL] THEN MATCH_MP_TAC(REAL_ARITH `a < c ==> a < abs(b + c) - b`) THEN REWRITE_TAC[REAL_ABS_POW; REAL_ABS_NUM] THEN MATCH_MP_TAC REAL_LT_LMUL THEN SIMP_TAC[REAL_POW_LT; REAL_OF_NUM_LT; ARITH] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&1` THEN ASM_SIMP_TAC[GSYM REAL_MUL_ASSOC; GSYM POW_2; SQRT_POW_2; REAL_ARITH `&1 <= x ==> &0 <= x`] THEN FIRST_ASSUM(ASSUME_TAC o MATCH_MP(REAL_ARITH `&1 <= x ==> &0 <= x`)) THEN UNDISCH_TAC `&1 <= x` THEN CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[REAL_NOT_LE] THEN DISCH_TAC THEN SUBGOAL_THEN `x = sqrt(x) pow 2` SUBST1_TAC THENL [CONV_TAC SYM_CONV THEN ASM_REWRITE_TAC[SQRT_POW2]; GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN REWRITE_TAC[POW_2] THEN MATCH_MP_TAC REAL_LT_MUL2 THEN ASM_SIMP_TAC[SQRT_POS_LE]]);;
(* ------------------------------------------------------------------------- *) (* Lemmas common to all the Taylor series error analyses. *) (* ------------------------------------------------------------------------- *)
let STEP_LEMMA1 = 
prove (`!a b c d x y. abs(a - c) <= x /\ abs(b - d) <= y ==> abs(a * b - c * d) <= abs(c) * y + abs(d) * x + x * y`,
REPEAT GEN_TAC THEN ABBREV_TAC `u = a - c` THEN ABBREV_TAC `v = b - d` THEN SUBGOAL_THEN `a = c + u` SUBST1_TAC THENL [POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN REAL_ARITH_TAC; ALL_TAC] THEN SUBGOAL_THEN `b = d + v` SUBST1_TAC THENL [POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN REAL_ARITH_TAC; ALL_TAC] THEN STRIP_TAC THEN SUBST1_TAC (REAL_ARITH `(c + u) * (d + v) - c * d = c * v + d * u + u * v`) THEN REPEAT(MATCH_MP_TAC (REAL_LE_IMP REAL_ABS_TRIANGLE) THEN MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC) THEN REWRITE_TAC[REAL_ABS_MUL] THENL [MATCH_MP_TAC REAL_LE_LMUL; MATCH_MP_TAC REAL_LE_LMUL; MATCH_MP_TAC REAL_LE_MUL2] THEN ASM_REWRITE_TAC[REAL_ABS_POS]);;
let STEP_LEMMA2 = 
prove (`!n s t u x y k l a d. &0 < a /\ &0 < d /\ abs(s - &2 pow n * x) <= k /\ abs(t - &2 pow n * y) <= l /\ &2 * abs(u * &2 pow n * d - a * s * t) <= &2 pow n * d ==> abs(u - &2 pow n * (a / d) * (x * y)) <= (a / d) * (abs(x) + k / (&2 pow n)) * l + ((a / d) * k * abs(y) + &1 / &2)`,
REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN ONCE_REWRITE_TAC[CONJ_ASSOC] THEN DISCH_THEN (CONJUNCTS_THEN2 (ASSUME_TAC o MATCH_MP STEP_LEMMA1) ASSUME_TAC) THEN SUBGOAL_THEN `&0 < &2 * &2 pow n * d` ASSUME_TAC THENL [REPEAT(MATCH_MP_TAC REAL_LT_MUL THEN CONJ_TAC) THEN ASM_REWRITE_TAC[REAL_LT_POW2] THEN REAL_ARITH_TAC; ALL_TAC] THEN MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN EXISTS_TAC `&2 * &2 pow n * d` THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[real_div; REAL_ADD_LDISTRIB; REAL_ADD_RDISTRIB] THEN SUBGOAL_THEN `!z. (&2 * &2 pow n * d) * abs(z) = abs((&2 * &2 pow n * d) * z)` (fun th -> REWRITE_TAC[th]) THENL [GEN_TAC THEN ONCE_REWRITE_TAC[REAL_ABS_MUL] THEN AP_THM_TAC THEN AP_TERM_TAC THEN UNDISCH_TAC `&0 < &2 * &2 pow n * d` THEN REAL_ARITH_TAC; ALL_TAC] THEN REWRITE_TAC[REAL_SUB_LDISTRIB] THEN (MATCH_MP_TAC o GEN_ALL o REAL_ARITH) `abs(a - b) + abs(b - c) <= d ==> abs(a - c) <= d` THEN EXISTS_TAC `&2 * a * s * t` THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC; REAL_ADD_ASSOC] THEN GEN_REWRITE_TAC RAND_CONV [REAL_ADD_SYM] THEN SUBGOAL_THEN `(inv(&2) * &2 = &1) /\ (inv(&2 pow n) * &2 pow n = &1) /\ (inv(d) * d = &1)` STRIP_ASSUME_TAC THENL [REPEAT CONJ_TAC THEN MATCH_MP_TAC REAL_MUL_LINV THEN REWRITE_TAC[REAL_POW_EQ_0] THEN UNDISCH_TAC `&0 < d` THEN REAL_ARITH_TAC; ALL_TAC] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL [GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN ASM_REWRITE_TAC[GSYM REAL_MUL_ASSOC; REAL_MUL_RID] THEN REWRITE_TAC[GSYM REAL_SUB_LDISTRIB; GSYM REAL_ABS_LEMMA1] THEN REWRITE_TAC[REAL_MUL_ASSOC] THEN GEN_REWRITE_TAC (LAND_CONV o funpow 2 RAND_CONV o LAND_CONV) [REAL_MUL_SYM] THEN ASM_REWRITE_TAC[GSYM REAL_MUL_ASSOC]; REWRITE_TAC(map (GSYM o SPEC `&2`) [REAL_SUB_LDISTRIB; REAL_ADD_LDISTRIB]) THEN REWRITE_TAC[GSYM REAL_ABS_LEMMA1] THEN MATCH_MP_TAC REAL_LE_LMUL THEN CONV_TAC(LAND_CONV (EQT_INTRO o REAL_ARITH)) THEN REWRITE_TAC[] THEN GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [AC REAL_MUL_AC `a * b * c * d * e * f * g = d * (a * f) * (c * g) * (e * b)`] THEN GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o LAND_CONV) [AC REAL_MUL_AC `a * b * c * d * e * f = c * (a * e) * f * (d * b)`] THEN GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o RAND_CONV) [AC REAL_MUL_AC `a * b * c * d * e * f * g = c * (e * g) * (f * a) * (d * b)`] THEN GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [AC REAL_MUL_AC `a * b * c * d * e * f = c * (a * f) * e * (d * b)`] THEN GEN_REWRITE_TAC RAND_CONV [AC REAL_ADD_AC `(a + b) + c = a + c + b`] THEN ASM_REWRITE_TAC[REAL_MUL_RID] THEN REWRITE_TAC[GSYM REAL_ADD_LDISTRIB; GSYM REAL_SUB_LDISTRIB] THEN REWRITE_TAC[REAL_ABS_MUL] THEN SUBGOAL_THEN `abs(a) = a` SUBST1_TAC THENL [UNDISCH_TAC `&0 < a` THEN REAL_ARITH_TAC; MATCH_MP_TAC REAL_LE_LMUL THEN ASM_REWRITE_TAC[REAL_ABS_LEMMA] THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[]]]);;
(* ------------------------------------------------------------------------- *) (* Now specific instances. *) (* ------------------------------------------------------------------------- *)
let STEP_EXP = 
prove (`abs(x) <= &1 /\ abs(s - &2 pow n * x) <= &1 /\ abs(t - &2 pow n * (x pow i / &(FACT i))) <= k /\ &2 * abs(u * &2 pow n * &(SUC i) - s * t) <= &2 pow n * &(SUC i) ==> abs(u - &2 pow n * (x pow (SUC i)) / &(FACT(SUC i))) <= (&2 / &(SUC i)) * k + &1 / &(FACT(SUC i)) + &1 / &2`,
STRIP_TAC THEN MP_TAC(SPECL [`n:num`; `s:real`; `t:real`; `u:real`; `x:real`; `x pow i / &(FACT i)`; `&1`; `k:real`; `&1`; `&(SUC i)`] STEP_LEMMA2) THEN ASM_REWRITE_TAC[REAL_LT_01; REAL_MUL_LID] THEN REWRITE_TAC[REAL_OF_NUM_LT; LT_0] THEN REWRITE_TAC[FACT; real_div; GSYM REAL_OF_NUM_MUL; real_pow] THEN REWRITE_TAC[REAL_MUL_LID; REAL_INV_MUL] THEN MATCH_MP_TAC(REAL_ARITH `(a = b) /\ c <= d ==> a <= c ==> b <= d`) THEN CONJ_TAC THENL [REWRITE_TAC[REAL_MUL_AC]; REWRITE_TAC[REAL_ADD_ASSOC; REAL_LE_RADD] THEN GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o LAND_CONV) [REAL_MUL_SYM] THEN REWRITE_TAC[GSYM REAL_ADD_LDISTRIB; GSYM REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LE_LMUL THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LE_INV THEN REWRITE_TAC[REAL_OF_NUM_LE; LE_0]; MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LE_RMUL THEN CONJ_TAC THENL [GEN_REWRITE_TAC RAND_CONV [REAL_ARITH `&2 = &1 + &1`] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_INV_LE_1 THEN REWRITE_TAC[REAL_LE_POW2]; MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `abs(t - &2 pow n * (x pow i / &(FACT i)))` THEN ASM_REWRITE_TAC[REAL_ABS_POS]]; REWRITE_TAC[REAL_ABS_MUL] THEN GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL [REWRITE_TAC[REAL_ABS_POW] THEN MATCH_MP_TAC REAL_POW_1_LE THEN ASM_REWRITE_TAC[REAL_ABS_POS]; MATCH_MP_TAC(REAL_ARITH `&0 <= a ==> abs(a) <= a`) THEN MATCH_MP_TAC REAL_LE_INV THEN REWRITE_TAC[REAL_OF_NUM_LE; LE_0]]]]]);;
let STEP_SIN = 
prove (`abs(x) <= &1 /\ abs(s - &2 pow n * --(x pow 2)) <= &1 /\ abs(t - &2 pow n * x pow (2 * i + 1) / &(FACT (2 * i + 1))) <= &1 /\ &2 * abs(u * &2 pow n * &(2 * i + 2) * &(2 * i + 3) - s * t) <= &2 pow n * &(2 * i + 2) * &(2 * i + 3) ==> abs(u - &2 pow n * --(x pow (2 * (SUC i) + 1)) / &(FACT (2 * (SUC i) + 1))) <= &1`,
STRIP_TAC THEN MP_TAC(SPECL [`n:num`; `s:real`; `t:real`; `u:real`; `--(x pow 2)`; `x pow (2 * i + 1) / &(FACT(2 * i + 1))`; `&1`; `&1`; `&1`; `&(2 * i + 2) * &(2 * i + 3)`] STEP_LEMMA2) THEN ASM_REWRITE_TAC[REAL_LT_01; REAL_MUL_LID] THEN W(C SUBGOAL_THEN (fun th -> REWRITE_TAC[th]) o funpow 2 (fst o dest_imp) o snd) THENL [REWRITE_TAC(map num_CONV [`3`; `2`; `1`]) THEN REWRITE_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_LT] THEN REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES; LT_0]; ALL_TAC] THEN MATCH_MP_TAC(REAL_ARITH `(a = b) /\ c <= d ==> a <= c ==> b <= d`) THEN CONJ_TAC THENL [AP_TERM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN SUBGOAL_THEN `2 * (SUC i) + 1 = SUC(SUC(2 * i + 1))` SUBST1_TAC THENL [GEN_REWRITE_TAC I [GSYM REAL_OF_NUM_EQ] THEN REWRITE_TAC[ADD1; GSYM REAL_OF_NUM_MUL; GSYM REAL_OF_NUM_ADD] THEN REAL_ARITH_TAC; REWRITE_TAC[real_pow; FACT] THEN REWRITE_TAC[ADD1; GSYM ADD_ASSOC] THEN REWRITE_TAC[ARITH] THEN REWRITE_TAC[real_div; REAL_INV_MUL; GSYM REAL_OF_NUM_MUL; GSYM REAL_OF_NUM_ADD] THEN REWRITE_TAC[REAL_MUL_LID; REAL_MUL_RNEG; REAL_MUL_LNEG] THEN REWRITE_TAC[REAL_POW_2; REAL_MUL_AC]]; GEN_REWRITE_TAC RAND_CONV [SYM(REAL_RAT_REDUCE_CONV `&1 / &3 + &1 / &6 + &1 / &2`)] THEN REWRITE_TAC[REAL_ADD_ASSOC; REAL_LE_RADD] THEN SUBGOAL_THEN `&1 / (&(2 * i + 2) * &(2 * i + 3)) <= &1 / &6` ASSUME_TAC THENL [REWRITE_TAC[real_div; REAL_MUL_LID] THEN MATCH_MP_TAC REAL_LE_INV2 THEN CONV_TAC(LAND_CONV (EQT_INTRO o REAL_ARITH)) THEN REWRITE_TAC[] THEN REWRITE_TAC[REAL_ARITH `&6 = &2 * &3`] THEN REWRITE_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_LE] THEN MATCH_MP_TAC LE_MULT2 THEN ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[LE_ADD]; ALL_TAC] THEN REWRITE_TAC[SYM(REAL_RAT_REDUCE_CONV `&1 / &6 * &2`)] THEN GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM REAL_MUL_RID] THEN REWRITE_TAC[GSYM REAL_ADD_LDISTRIB] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL [REWRITE_TAC[real_div; REAL_MUL_LID; REAL_LE_INV_EQ] THEN REWRITE_TAC[REAL_OF_NUM_MUL; REAL_POS]; MATCH_MP_TAC REAL_LE_ADD THEN REWRITE_TAC[REAL_MUL_RID; REAL_ABS_POS] THEN MATCH_MP_TAC REAL_LE_ADD THEN REWRITE_TAC[real_div; REAL_MUL_LID; REAL_LE_INV_EQ; REAL_ABS_POS] THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN REWRITE_TAC[REAL_LT_POW2]; REWRITE_TAC[REAL_MUL_RID]] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL [GEN_REWRITE_TAC RAND_CONV [REAL_ARITH `&2 = &1 + &1`] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL [REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_POW] THEN MATCH_MP_TAC REAL_POW_1_LE THEN ASM_REWRITE_TAC[REAL_ABS_POS]; REWRITE_TAC[real_div; REAL_MUL_LID] THEN MATCH_MP_TAC REAL_INV_LE_1 THEN REWRITE_TAC[REAL_LE_POW2]]; REWRITE_TAC[real_div; REAL_ABS_MUL] THEN GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL [REWRITE_TAC[REAL_ABS_POW] THEN MATCH_MP_TAC REAL_POW_1_LE THEN ASM_REWRITE_TAC[REAL_ABS_POS]; REWRITE_TAC[REAL_ABS_INV; REAL_ABS_NUM] THEN MATCH_MP_TAC REAL_INV_LE_1 THEN REWRITE_TAC[REAL_OF_NUM_LE; FACT_LE]]]]);;
let STEP_COS = 
prove (`abs(x) <= &1 /\ abs(s - &2 pow n * --(x pow 2)) <= &1 /\ abs(t - &2 pow n * x pow (2 * i) / &(FACT (2 * i))) <= k /\ &2 * abs(u * &2 pow n * &(2 * i + 1) * &(2 * i + 2) - s * t) <= &2 pow n * &(2 * i + 1) * &(2 * i + 2) ==> abs(u - &2 pow n * --(x pow (2 * (SUC i))) / &(FACT (2 * (SUC i)))) <= (&2 * inv(&(2 * i + 1) * &(2 * i + 2))) * k + inv(&(FACT(2 * i + 2))) + &1 / &2`,
STRIP_TAC THEN MP_TAC(SPECL [`n:num`; `s:real`; `t:real`; `u:real`; `--(x pow 2)`; `x pow (2 * i) / &(FACT(2 * i))`; `&1`; `k:real`; `&1`; `&(2 * i + 1) * &(2 * i + 2)`] STEP_LEMMA2) THEN ASM_REWRITE_TAC[REAL_LT_01; REAL_MUL_LID] THEN W(C SUBGOAL_THEN (fun th -> REWRITE_TAC[th]) o funpow 2 (fst o dest_imp) o snd) THENL [REWRITE_TAC(map num_CONV [`3`; `2`; `1`]) THEN REWRITE_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_LT] THEN REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES; LT_0]; ALL_TAC] THEN MATCH_MP_TAC(REAL_ARITH `(a = b) /\ c <= d ==> a <= c ==> b <= d`) THEN CONJ_TAC THENL [AP_TERM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN SUBGOAL_THEN `2 * (SUC i) = SUC(SUC(2 * i))` SUBST1_TAC THENL [GEN_REWRITE_TAC I [GSYM REAL_OF_NUM_EQ] THEN REWRITE_TAC[ADD1; GSYM REAL_OF_NUM_MUL; GSYM REAL_OF_NUM_ADD] THEN REAL_ARITH_TAC; REWRITE_TAC[real_pow; FACT] THEN REWRITE_TAC[ADD1; GSYM ADD_ASSOC] THEN REWRITE_TAC[ARITH] THEN REWRITE_TAC[real_div; REAL_INV_MUL; GSYM REAL_OF_NUM_MUL; GSYM REAL_OF_NUM_ADD] THEN REWRITE_TAC[REAL_MUL_LID; REAL_MUL_RNEG; REAL_MUL_LNEG] THEN REWRITE_TAC[REAL_POW_2; REAL_MUL_AC]]; REWRITE_TAC[REAL_ADD_ASSOC; REAL_LE_RADD] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL [REWRITE_TAC[REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LE_RMUL THEN CONJ_TAC THENL [REWRITE_TAC[real_div; REAL_MUL_LID] THEN GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_SYM] THEN MATCH_MP_TAC REAL_LE_LMUL THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LE_INV THEN REWRITE_TAC[REAL_OF_NUM_MUL; REAL_POS]; GEN_REWRITE_TAC RAND_CONV [REAL_ARITH `&2 = &1 + &1`] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL [REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_POW] THEN MATCH_MP_TAC REAL_POW_1_LE THEN ASM_REWRITE_TAC[REAL_ABS_POS]; MATCH_MP_TAC REAL_INV_LE_1 THEN REWRITE_TAC[REAL_LE_POW2]]]; MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `abs(t - &2 pow n * x pow (2 * i) / &(FACT (2 * i)))` THEN ASM_REWRITE_TAC[REAL_ABS_POS]]; REWRITE_TAC[real_div; REAL_MUL_LID; REAL_INV_MUL; REAL_ABS_MUL] THEN GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN ONCE_REWRITE_TAC[AC REAL_MUL_AC `(a * b) * c * d = (d * a * b) * c`] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[REAL_ABS_POS] THEN REPEAT CONJ_TAC THENL [REPEAT(MATCH_MP_TAC REAL_LE_MUL THEN CONJ_TAC) THEN REWRITE_TAC[REAL_POS; REAL_ABS_POS; REAL_LE_INV_EQ]; REWRITE_TAC[REAL_ABS_INV] THEN REWRITE_TAC[GSYM REAL_INV_MUL; REAL_ABS_NUM] THEN MATCH_MP_TAC REAL_EQ_IMP_LE THEN AP_TERM_TAC THEN REWRITE_TAC[num_CONV `2`; num_CONV `1`; ADD_CLAUSES] THEN REWRITE_TAC[SYM(num_CONV `2`); SYM(num_CONV `1`)] THEN REWRITE_TAC[FACT; REAL_OF_NUM_MUL] THEN REWRITE_TAC[MULT_AC]; REWRITE_TAC[REAL_ABS_POW] THEN MATCH_MP_TAC REAL_POW_1_LE THEN ASM_REWRITE_TAC[REAL_ABS_POS]]]]);;
let STEP_LN = 
prove (`2 <= n /\ abs(x) <= &1 / &2 /\ abs(s - &2 pow n * --x) <= &1 /\ abs(t - &2 pow n * -- ((--x) pow (SUC i) / &(SUC i))) <= &3 /\ &2 * abs(u * &2 pow n * &(SUC(SUC i)) - &(SUC i) * s * t) <= &2 pow n * &(SUC(SUC i)) ==> abs(u - &2 pow n * -- ((--x) pow (SUC(SUC i)) / &(SUC(SUC i)))) <= &3`,
STRIP_TAC THEN MP_TAC(SPECL [`n:num`; `s:real`; `t:real`; `u:real`; `--x`; `-- (--x pow (SUC i) / &(SUC i))`; `&1`; `&3`; `&(SUC i)`; `&(SUC(SUC i))`] STEP_LEMMA2) THEN ASM_REWRITE_TAC[REAL_LT_01; REAL_MUL_LID] THEN REWRITE_TAC[REAL_OF_NUM_LT; LT_0] THEN MATCH_MP_TAC(REAL_ARITH `(a = b) /\ c <= d ==> a <= c ==> b <= d`) THEN CONJ_TAC THENL [AP_TERM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[real_pow; real_div; REAL_INV_MUL] THEN REWRITE_TAC[REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_NEG_NEG] THEN AP_TERM_TAC THEN REWRITE_TAC[REAL_MUL_ASSOC] THEN GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] THEN SUBGOAL_THEN `inv(&(SUC i)) * &(SUC i) = &1` ASSUME_TAC THENL [MATCH_MP_TAC REAL_MUL_LINV THEN REWRITE_TAC[REAL_OF_NUM_EQ; NOT_SUC]; ASM_REWRITE_TAC[REAL_MUL_ASSOC; REAL_MUL_LID] THEN REWRITE_TAC[REAL_MUL_AC]]; GEN_REWRITE_TAC RAND_CONV [SYM(REAL_RAT_REDUCE_CONV `(&1 / &2 + &1 / &4) * &3 + &1 / &4 + &1 / &2`)] THEN REWRITE_TAC[REAL_ADD_ASSOC; REAL_LE_RADD] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL [REWRITE_TAC[REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LE_RMUL THEN CONV_TAC(RAND_CONV (EQT_INTRO o REAL_ARITH)) THEN REWRITE_TAC[] THEN GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN REPEAT CONJ_TAC THENL [MATCH_MP_TAC REAL_LE_RCANCEL_IMP THEN EXISTS_TAC `&(SUC(SUC i))` THEN REWRITE_TAC[REAL_MUL_LZERO; REAL_OF_NUM_LT; LT_0] THEN REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LE_MUL THEN REWRITE_TAC[REAL_POS] THEN MATCH_MP_TAC(REAL_ARITH `(x = &1) ==> &0 <= x`) THEN MATCH_MP_TAC REAL_MUL_LINV THEN REWRITE_TAC[REAL_OF_NUM_EQ; NOT_SUC]; MATCH_MP_TAC REAL_LE_RCANCEL_IMP THEN EXISTS_TAC `&(SUC(SUC i))` THEN REWRITE_TAC[REAL_OF_NUM_LT; LT_0] THEN REWRITE_TAC[real_div; REAL_MUL_LID; GSYM REAL_MUL_ASSOC] THEN GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[REAL_POS] THEN REWRITE_TAC[REAL_OF_NUM_LE; LE] THEN MATCH_MP_TAC(REAL_ARITH `(x = &1) ==> &0 <= x /\ x <= &1`) THEN MATCH_MP_TAC REAL_MUL_LINV THEN REWRITE_TAC[REAL_OF_NUM_EQ; NOT_SUC]; MATCH_MP_TAC REAL_LE_ADD THEN REWRITE_TAC[REAL_ABS_POS] THEN REWRITE_TAC[real_div; REAL_MUL_LID; REAL_LE_INV_EQ] THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN REWRITE_TAC[REAL_LT_POW2]; MATCH_MP_TAC REAL_LE_ADD2 THEN ASM_REWRITE_TAC[REAL_ABS_NEG] THEN REWRITE_TAC[real_div; REAL_MUL_LID] THEN MATCH_MP_TAC REAL_LE_INV2 THEN CONV_TAC(LAND_CONV (EQT_INTRO o REAL_ARITH)) THEN REWRITE_TAC[] THEN SUBST1_TAC(SYM(REAL_INT_REDUCE_CONV `&2 pow 2`)) THEN MATCH_MP_TAC REAL_MONO_POW2 THEN ASM_REWRITE_TAC[]]; REWRITE_TAC[real_div; REAL_ABS_MUL; REAL_ABS_NEG; REAL_ABS_INV] THEN REWRITE_TAC[REAL_ABS_POW; REAL_ABS_NEG; REAL_MUL_LID] THEN REWRITE_TAC[REAL_ABS_NUM] THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[REAL_MUL_ASSOC] THEN SUBGOAL_THEN `inv(&(SUC i)) * &(SUC i) = &1` ASSUME_TAC THENL [MATCH_MP_TAC REAL_MUL_LINV THEN REWRITE_TAC[REAL_OF_NUM_EQ; NOT_SUC]; GEN_REWRITE_TAC RAND_CONV [EQT_ELIM(REAL_RAT_REDUCE_CONV `inv(&4) = inv(&2) * inv(&2)`)] THEN ASM_REWRITE_TAC[REAL_MUL_RID; GSYM REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC [REAL_POS; REAL_ABS_POS; REAL_LE_INV_EQ; GSYM REAL_ABS_POW] THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LE_INV2 THEN REWRITE_TAC[REAL_POS] THEN REWRITE_TAC[ADD1; GSYM REAL_OF_NUM_ADD] THEN MP_TAC(SPEC `i:num` REAL_POS) THEN REAL_ARITH_TAC; REWRITE_TAC[real_pow; REAL_ABS_POW] THEN GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[REAL_LE_INV_EQ; REAL_ABS_POS] THEN REPEAT CONJ_TAC THENL [CONV_TAC(RAND_CONV REAL_RAT_REDUCE_CONV) THEN ASM_REWRITE_TAC[]; MATCH_MP_TAC REAL_POW_LE THEN REWRITE_TAC[REAL_ABS_POS]; MATCH_MP_TAC REAL_POW_1_LE THEN REWRITE_TAC[REAL_ABS_POS] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&1 / &2` THEN ASM_REWRITE_TAC[] THEN CONV_TAC REAL_RAT_REDUCE_CONV]]]]]);;
(* ------------------------------------------------------------------------- *) (* Expand the "!k. SUC k < r ==> P k" term for given numeral r. *) (* ------------------------------------------------------------------------- *) let EXPAND_RANGE_CONV =
let pth0 = 
prove (`(!k. SUC k < 0 ==> P k) <=> T`,
REWRITE_TAC[LT]) and pth1 = prove (`(!k. k < (SUC m) ==> P k) <=> (!k. k < m ==> P k) /\ P m`, REWRITE_TAC[LT] THEN MESON_TAC[]) and pth2 = prove (`(!k. k < 0 ==> P k) <=> T`, REWRITE_TAC[LT]) in let triv_conv = GEN_REWRITE_CONV I [pth0] and trivial_conv = GEN_REWRITE_CONV I [pth2] and nontrivial_conv = GEN_REWRITE_CONV I [pth1] in let s_tm = `s:real` and m_tm = `m:num` and n_tm = `n:num` in let rec expand_conv tm = try trivial_conv tm with Failure _ -> let mth = num_CONV(rand(lhand(body(rand tm)))) in let th1 = BINDER_CONV(LAND_CONV(RAND_CONV(K mth))) tm in let th2 = TRANS th1 (nontrivial_conv (rand(concl th1))) in let th3 = COMB2_CONV (RAND_CONV expand_conv) (SUBS_CONV[SYM mth]) (rand(concl th2)) in TRANS th2 th3 in let hack_conv = triv_conv ORELSEC (BINDER_CONV (LAND_CONV ((RAND_CONV num_CONV) THENC REWR_CONV LT_SUC)) THENC expand_conv) in hack_conv;;
(* ------------------------------------------------------------------------- *) (* Lemmas leading to iterative versions. *) (* ------------------------------------------------------------------------- *)
let STEP_EXP_THM = 
prove (`abs(x) <= &1 /\ abs(s - &2 pow n * x) < &1 /\ abs(t(i) - &2 pow n * (x pow i / &(FACT i))) <= k ==> &2 * abs(t(SUC i) * &2 pow n * &(SUC i) - s * t(i)) <= &2 pow n * &(SUC i) ==> abs(t(SUC i) - &2 pow n * (x pow (SUC i)) / &(FACT(SUC i))) <= (&2 / &(SUC i)) * k + &1 / &(FACT(SUC i)) + &1 / &2`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC(GEN_ALL STEP_EXP) THEN MAP_EVERY EXISTS_TAC [`s:real`; `t(i:num):real`] THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[]);;
let STEP_EXP_RULE th = let th1 = MATCH_MP STEP_EXP_THM th in let th2 = UNDISCH(PURE_REWRITE_RULE[ARITH_SUC] th1) in let th3 = CONV_RULE(RAND_CONV(ONCE_DEPTH_CONV NUM_FACT_CONV)) th2 in let th4 = CONV_RULE(RAND_CONV REAL_RAT_REDUCE_CONV) th3 in let th5 = ASSUME(find is_conj (hyp th)) in let th6a,th6b = (I F_F CONJUNCT1) (CONJ_PAIR th5) in CONJ th6a (CONJ th6b th4);; let STEP_EXP_0 = (UNDISCH o prove) (`abs(x) <= &1 /\ abs(s - &2 pow n * x) < &1 /\ (t(0) = &2 pow n) ==> abs(x) <= &1 /\ abs(s - &2 pow n * x) < &1 /\ abs(t(0) - &2 pow n * (x pow 0 / &(FACT 0))) <= &0`, STRIP_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[real_pow; FACT; real_div; REAL_INV_1; REAL_MUL_RID] THEN REWRITE_TAC[REAL_SUB_REFL; REAL_ABS_0; REAL_LE_REFL]);; let STEP_EXP_1 = STEP_EXP_RULE STEP_EXP_0;; (* e(1) = 3/2 *) let STEP_EXP_2 = STEP_EXP_RULE STEP_EXP_1;; (* e(2) = 5/2 *) let STEP_EXP_3 = STEP_EXP_RULE STEP_EXP_2;; (* e(3) = 7/3 *) let STEP_EXP_4 = STEP_EXP_RULE STEP_EXP_3;; (* e(4) = 41/24 *) let STEP_EXP_5 = STEP_EXP_RULE STEP_EXP_4;; (* e(5) = 143/120 *)
let STEP_EXP_4_PLUS = 
prove (`4 <= m /\ abs(x) <= &1 /\ abs(s - &2 pow n * x) < &1 /\ (t(0) = &2 pow n) /\ (!k. SUC k < SUC m ==> &2 * abs(t(SUC k) * &2 pow n * &(SUC k) - s * t(k)) <= &2 pow n * &(SUC k)) ==> abs(t m - &2 pow n * x pow m / &(FACT m)) <= &2`,
let lemma = prove
   (`(!k. k < (SUC m) ==> P k) <=>
     (!k. k < m ==> P k) /\ P m`,
    REWRITE_TAC[LT] THEN MESON_TAC[]) in
  DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
  POP_ASSUM(X_CHOOSE_THEN `d:num` SUBST1_TAC o REWRITE_RULE[LE_EXISTS]) THEN
  DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
  DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
  DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
  REWRITE_TAC[LT_SUC] THEN SPEC_TAC(`d:num`,`d:num`) THEN
  INDUCT_TAC THENL
   [REWRITE_TAC[ADD_CLAUSES] THEN
    SUBST1_TAC(TOP_DEPTH_CONV num_CONV `4`) THEN
    REWRITE_TAC[lemma] THEN REWRITE_TAC[ARITH_SUC] THEN
    REWRITE_TAC[LT] THEN STRIP_TAC THEN
    MP_TAC (DISCH_ALL STEP_EXP_4) THEN ASM_REWRITE_TAC[] THEN
    MATCH_MP_TAC(REAL_ARITH `b <= c ==> a <= b ==> a <= c`) THEN
    CONV_TAC REAL_RAT_REDUCE_CONV;
    REWRITE_TAC[ADD_CLAUSES; lemma] THEN STRIP_TAC THEN
    MATCH_MP_TAC REAL_LE_TRANS THEN
    EXISTS_TAC `&2 / &(SUC(4 + d)) * &2 +
                &1 / &(FACT(SUC(4 + d))) + &1 / &2` THEN
    CONJ_TAC THENL
     [MATCH_MP_TAC(GEN_ALL STEP_EXP) THEN ASM_REWRITE_TAC[] THEN
      EXISTS_TAC `s:real` THEN EXISTS_TAC `t(4 + d):real` THEN
      ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
       [MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[];
        FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]];
      GEN_REWRITE_TAC RAND_CONV
        [SYM(REAL_RAT_REDUCE_CONV `&3 / &2 + &1 / &2`)] THEN
      REWRITE_TAC[REAL_LE_RADD; REAL_ADD_ASSOC] THEN
      MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&4 / &5 + &1 / &120` THEN
      CONV_TAC(RAND_CONV REAL_RAT_REDUCE_CONV) THEN REWRITE_TAC[] THEN
      MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL
       [ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
        REWRITE_TAC[real_div; REAL_MUL_ASSOC] THEN
        REWRITE_TAC[REAL_ARITH `&2 * &2 = &4`] THEN
        MATCH_MP_TAC REAL_LE_LMUL THEN
        REWRITE_TAC[REAL_ARITH `&0 <= &4`] THEN
        MATCH_MP_TAC REAL_LE_INV2 THEN
        REWRITE_TAC[ADD1; GSYM REAL_OF_NUM_ADD] THEN
        MP_TAC(SPEC `d':num` REAL_POS) THEN REAL_ARITH_TAC;
        REWRITE_TAC[real_div; REAL_MUL_LID] THEN
        MATCH_MP_TAC REAL_LE_INV2 THEN
        CONV_TAC(LAND_CONV (EQT_INTRO o REAL_ARITH)) THEN REWRITE_TAC[] THEN
        SUBST1_TAC(SYM(NUM_FACT_CONV `FACT 5`)) THEN
        REWRITE_TAC[REAL_OF_NUM_LE] THEN MATCH_MP_TAC FACT_MONO THEN
        REWRITE_TAC[num_CONV `5`; LE_SUC; LE_ADD]]]]);;
let STEPS_EXP_0 = 
prove (`abs(x) <= &1 /\ abs(s - &2 pow n * x) < &1 /\ (t(0) = &2 pow n) /\ (!k. SUC k < 0 ==> &2 * abs(t(SUC k) * &2 pow n * &(SUC k) - s * t(k)) <= &2 pow n * &(SUC k)) ==> abs(sum(0,0) t - &2 pow n * sum(0,0) (\i. x pow i / &(FACT i))) <= &2 * &0`,
STRIP_TAC THEN ASM_REWRITE_TAC[sum] THEN REWRITE_TAC[REAL_MUL_RZERO; REAL_ABS_0; REAL_SUB_REFL; REAL_LE_REFL]);;
let STEPS_EXP_1 = 
prove (`abs(x) <= &1 /\ abs(s - &2 pow n * x) < &1 /\ (t(0) = &2 pow n) /\ (!k. SUC k < 1 ==> &2 * abs(t(SUC k) * &2 pow n * &(SUC k) - s * t(k)) <= &2 pow n * &(SUC k)) ==> abs(sum(0,1) t - &2 pow n * sum(0,1)(\i. x pow i / &(FACT i))) <= &2 * &1`,
CONV_TAC(ONCE_DEPTH_CONV EXPAND_RANGE_CONV) THEN REWRITE_TAC[] THEN STRIP_TAC THEN CONV_TAC(ONCE_DEPTH_CONV REAL_SUM_CONV) THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&0` THEN CONV_TAC(RAND_CONV REAL_RAT_REDUCE_CONV) THEN REWRITE_TAC[] THEN MP_TAC (DISCH_ALL STEP_EXP_0) THEN ASM_REWRITE_TAC[]);;
let STEPS_EXP_2 = 
prove (`abs(x) <= &1 /\ abs(s - &2 pow n * x) < &1 /\ (t(0) = &2 pow n) /\ (!k. SUC k < 2 ==> &2 * abs(t(SUC k) * &2 pow n * &(SUC k) - s * t(k)) <= &2 pow n * &(SUC k)) ==> abs(sum(0,2) t - &2 pow n * sum(0,2) (\i. x pow i / &(FACT i))) <= &2 * &2`,
CONV_TAC(ONCE_DEPTH_CONV EXPAND_RANGE_CONV) THEN REWRITE_TAC[] THEN STRIP_TAC THEN CONV_TAC(ONCE_DEPTH_CONV REAL_SUM_CONV) THEN REWRITE_TAC[REAL_ADD_LDISTRIB] THEN REWRITE_TAC[REAL_ARITH `(a + b) - (c + d) = (a - c) + (b - d)`] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&0 + &3 / &2` THEN CONV_TAC(RAND_CONV REAL_RAT_REDUCE_CONV) THEN REWRITE_TAC[] THEN MATCH_MP_TAC(REAL_LE_IMP(REAL_ARITH `abs(a + b) <= abs(a) + abs(b)`)) THEN MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL [MP_TAC (DISCH_ALL STEP_EXP_0) THEN ASM_REWRITE_TAC[]; MP_TAC (DISCH_ALL STEP_EXP_1) THEN ASM_REWRITE_TAC[ADD_CLAUSES]]);;
let STEPS_EXP_3 = 
prove (`abs(x) <= &1 /\ abs(s - &2 pow n * x) < &1 /\ (t(0) = &2 pow n) /\ (!k. SUC k < 3 ==> &2 * abs(t(SUC k) * &2 pow n * &(SUC k) - s * t(k)) <= &2 pow n * &(SUC k)) ==> abs(sum(0,3) t - &2 pow n * sum(0,3) (\i. x pow i / &(FACT i))) <= &2 * &3`,
CONV_TAC(ONCE_DEPTH_CONV EXPAND_RANGE_CONV) THEN REWRITE_TAC[] THEN STRIP_TAC THEN CONV_TAC(ONCE_DEPTH_CONV REAL_SUM_CONV) THEN REWRITE_TAC[REAL_ADD_LDISTRIB] THEN REWRITE_TAC[REAL_ARITH `(a + b) - (c + d) = (a - c) + (b - d)`] THEN REWRITE_TAC[GSYM REAL_ADD_ASSOC] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&0 + &3 / &2 + &5 / &2` THEN CONV_TAC(RAND_CONV REAL_RAT_REDUCE_CONV) THEN REWRITE_TAC[] THEN REPEAT (MATCH_MP_TAC(REAL_LE_IMP(REAL_ARITH `abs(a + b) <= abs(a) + abs(b)`)) THEN MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC) THENL [MP_TAC (DISCH_ALL STEP_EXP_0) THEN ASM_REWRITE_TAC[]; MP_TAC (DISCH_ALL STEP_EXP_1) THEN ASM_REWRITE_TAC[ADD_CLAUSES]; MP_TAC (DISCH_ALL STEP_EXP_2) THEN ASM_REWRITE_TAC[ADD_CLAUSES]]);;
let STEPS_EXP_4 = 
prove (`abs(x) <= &1 /\ abs(s - &2 pow n * x) < &1 /\ (t(0) = &2 pow n) /\ (!k. SUC k < 4 ==> &2 * abs(t(SUC k) * &2 pow n * &(SUC k) - s * t(k)) <= &2 pow n * &(SUC k)) ==> abs(sum(0,4) t - &2 pow n * sum(0,4) (\i. x pow i / &(FACT i))) <= &2 * &4`,
CONV_TAC(ONCE_DEPTH_CONV EXPAND_RANGE_CONV) THEN REWRITE_TAC[] THEN STRIP_TAC THEN CONV_TAC(ONCE_DEPTH_CONV REAL_SUM_CONV) THEN REWRITE_TAC[REAL_ADD_LDISTRIB] THEN REWRITE_TAC[REAL_ARITH `(a + b) - (c + d) = (a - c) + (b - d)`] THEN REWRITE_TAC[GSYM REAL_ADD_ASSOC] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&0 + &3 / &2 + &5 / &2 + &7 / &3` THEN CONV_TAC(RAND_CONV REAL_RAT_REDUCE_CONV) THEN REWRITE_TAC[] THEN REPEAT (MATCH_MP_TAC(REAL_LE_IMP(REAL_ARITH `abs(a + b) <= abs(a) + abs(b)`)) THEN MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC) THENL [MP_TAC (DISCH_ALL STEP_EXP_0) THEN ASM_REWRITE_TAC[]; MP_TAC (DISCH_ALL STEP_EXP_1) THEN ASM_REWRITE_TAC[ADD_CLAUSES]; MP_TAC (DISCH_ALL STEP_EXP_2) THEN ASM_REWRITE_TAC[ADD_CLAUSES]; MP_TAC (DISCH_ALL STEP_EXP_3) THEN ASM_REWRITE_TAC[ADD_CLAUSES]]);;
(* ------------------------------------------------------------------------- *) (* Iterated versions. *) (* ------------------------------------------------------------------------- *)
let STEPS_EXP_LEMMA = 
prove (`(!k. P(SUC k) ==> P(k)) /\ (P(0) ==> (abs(sum(0,0) z) <= &2 * &0)) /\ (P(1) ==> (abs(sum(0,1) z) <= &2 * &1)) /\ (P(2) ==> (abs(sum(0,2) z) <= &2 * &2)) /\ (P(3) ==> (abs(sum(0,3) z) <= &2 * &3)) /\ (P(4) ==> (abs(sum(0,4) z) <= &2 * &4)) /\ (!m. 4 <= m /\ P(SUC m) ==> (abs(z m) <= &2)) ==> !m. P(m) ==> (abs(sum(0,m) z) <= &2 * &m)`,
STRIP_TAC THEN SUBGOAL_THEN `!d. P(d + 4) ==> abs(sum(0,d + 4) z) <= &2 * &(d + 4)` ASSUME_TAC THENL [INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN DISCH_TAC THEN REWRITE_TAC[sum; ADD1] THEN ONCE_REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN REWRITE_TAC[REAL_ADD_LDISTRIB] THEN MATCH_MP_TAC(REAL_LE_IMP(REAL_ARITH `abs(a + b) <= abs(a) + abs(b)`)) THEN MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL [FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]; REWRITE_TAC[REAL_MUL_RID] THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[LE_ADD]]; GEN_TAC THEN DISJ_CASES_THEN MP_TAC (SPECL [`4`; `m:num`] LE_CASES) THENL [DISCH_THEN(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[LE_EXISTS]) THEN ONCE_REWRITE_TAC[ADD_SYM] THEN ASM_REWRITE_TAC[]; SUBST1_TAC(TOP_DEPTH_CONV num_CONV `4`) THEN REWRITE_TAC[LE] THEN REWRITE_TAC[ARITH_SUC] THEN DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN SUBST1_TAC) THEN ASM_REWRITE_TAC[]]]);;
let STEPS_EXP = 
prove (`abs(x) <= &1 /\ abs(s - &2 pow n * x) < &1 /\ (t(0) = &2 pow n) /\ (!k. SUC k < m ==> &2 * abs(t(SUC k) * &2 pow n * &(SUC k) - s * t(k)) <= &2 pow n * &(SUC k)) ==> abs(sum(0,m) t - &2 pow n * sum(0,m) (\i. x pow i / &(FACT i))) <= &2 * &m`,
REWRITE_TAC[REAL_MUL_RSUM0; REAL_SUB_SUM0] THEN SPEC_TAC(`m:num`,`m:num`) THEN MATCH_MP_TAC STEPS_EXP_LEMMA THEN REWRITE_TAC[GSYM REAL_SUB_SUM0; GSYM REAL_MUL_RSUM0] THEN REWRITE_TAC[STEPS_EXP_0; STEPS_EXP_1; STEPS_EXP_2; STEPS_EXP_3] THEN REWRITE_TAC[STEPS_EXP_4; STEP_EXP_4_PLUS] THEN GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN GEN_TAC THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN MATCH_MP_TAC LT_TRANS THEN EXISTS_TAC `k:num` THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[LT]);;
let STEPS_LN = 
prove (`2 <= n /\ abs(x) <= &1 / &2 /\ abs(s - &2 pow n * --x) < &1 /\ (t(0) = --s) /\ (!k. SUC k < m ==> &2 * abs(t(SUC k) * &2 pow n * &(SUC(SUC k)) - &(SUC k) * s * t(k)) <= &2 pow n * &(SUC(SUC k))) ==> abs(sum(0,m) t - &2 pow n * sum(0,m) (\i. (--(&1)) pow i * x pow (SUC i) / &(SUC i))) <= &3 * &m`,
REWRITE_TAC[REAL_MUL_RSUM0; REAL_SUB_SUM0] THEN STRIP_TAC THEN GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN MATCH_MP_TAC (REAL_LE_IMP SUM_ABS_LE) THEN MATCH_MP_TAC SUM_BOUND THEN REWRITE_TAC[ADD_CLAUSES; LE_0] THEN INDUCT_TAC THENL [REWRITE_TAC[real_pow; ARITH; REAL_DIV_1; REAL_MUL_LID; REAL_MUL_RID] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_ARITH `-- a - b * c = --(a - b * --c)`] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&1` THEN ASM_SIMP_TAC[REAL_ABS_NEG; REAL_LT_IMP_LE; REAL_OF_NUM_LE; ARITH]; ALL_TAC] THEN DISCH_THEN(fun th -> ASSUME_TAC th THEN MP_TAC th) THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN SUBGOAL_THEN `p:num < m` (ANTE_RES_THEN MP_TAC) THENL [UNDISCH_TAC `SUC p < m` THEN ARITH_TAC; ALL_TAC] THEN DISCH_TAC THEN DISCH_TAC THEN MATCH_MP_TAC(REAL_ARITH `!y. abs(x - y) + abs(y - z) <= e ==> abs(x - z) <= e`) THEN EXISTS_TAC `&(SUC p) * s * t p / (&2 pow n * &(SUC(SUC p)))` THEN ONCE_REWRITE_TAC [SYM(REAL_RAT_REDUCE_CONV `&1 / &2 + &5 / &2`)] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LE_RCANCEL_IMP THEN EXISTS_TAC `&2 pow n * &(SUC(SUC p))` THEN SUBGOAL_THEN `&0 < &2 pow n * &(SUC(SUC p))` ASSUME_TAC THENL [MATCH_MP_TAC REAL_LT_MUL THEN SIMP_TAC[REAL_POW_LT; REAL_OF_NUM_LT; LT_0; ARITH]; ALL_TAC] THEN ASM_REWRITE_TAC[] THEN SUBGOAL_THEN `!x y. &0 < y ==> (abs(x) * y = abs(x * y))` (fun th -> ASM_SIMP_TAC[th]) THENL [REPEAT STRIP_TAC THEN REWRITE_TAC[REAL_ABS_MUL] THEN AP_TERM_TAC THEN ASM_SIMP_TAC[real_abs; REAL_LT_IMP_LE]; ALL_TAC] THEN MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN EXISTS_TAC `&2` THEN REWRITE_TAC[REAL_MUL_ASSOC] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC; REAL_MUL_LID] THEN REWRITE_TAC[REAL_SUB_RDISTRIB] THEN SUBGOAL_THEN `!a b c d. &0 < a ==> ((b * c * d / a) * a = b * c * d)` (fun th -> ASM_SIMP_TAC[th]) THEN SIMP_TAC[real_div; GSYM REAL_MUL_ASSOC; REAL_MUL_LINV; REAL_MUL_RID; REAL_LT_IMP_NZ]; ALL_TAC] THEN MATCH_MP_TAC(REAL_ARITH `!y. abs(x - y) + abs(y - z) <= e ==> abs(x - z) <= e`) THEN EXISTS_TAC `--(&1) pow p * s * x pow (SUC p) / &(SUC(SUC p))` THEN ONCE_REWRITE_TAC [SYM(REAL_RAT_REDUCE_CONV `&9 / &4 + &1 / &4`)] THEN MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL [SUBGOAL_THEN `--(&1) pow p * s * x pow (SUC p) / &(SUC(SUC p)) = &(SUC p) * s * (&2 pow n * --(&1) pow p * x pow SUC p / &(SUC p)) / (&2 pow n * &(SUC (SUC p)))` SUBST1_TAC THENL [REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC; REAL_INV_MUL] THEN ONCE_REWRITE_TAC[AC REAL_MUL_AC `a * b * c * d * e * f * g * h = d * b * e * h * (g * c) * (f * a)`] THEN SIMP_TAC[REAL_MUL_LINV; REAL_POW_EQ_0; REAL_OF_NUM_EQ; ARITH; NOT_SUC] THEN REWRITE_TAC[REAL_MUL_RID]; ALL_TAC] THEN REWRITE_TAC[GSYM REAL_SUB_LDISTRIB; REAL_ABS_MUL] THEN REWRITE_TAC[real_div; REAL_MUL_ASSOC; GSYM REAL_SUB_RDISTRIB] THEN REWRITE_TAC[REAL_ABS_MUL; GSYM REAL_MUL_ASSOC] THEN REWRITE_TAC[GSYM real_div] THEN ONCE_REWRITE_TAC[AC REAL_MUL_AC `a * b * c * d = (a * b * d) * c`] THEN GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o REDEPTH_CONV) [GSYM REAL_ABS_MUL] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `abs (&(SUC p) * s * inv (&2 pow n * &(SUC (SUC p)))) * &3` THEN ASM_SIMP_TAC[REAL_LE_LMUL; REAL_ABS_POS] THEN REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_NUM; REAL_ABS_INV; REAL_ABS_POW] THEN REWRITE_TAC[REAL_INV_MUL] THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN ONCE_REWRITE_TAC[AC REAL_MUL_AC `a * b * c * d * e = (d * a) * (b * c) * e`] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `inv(&1) * &3 / &4 * &3` THEN CONV_TAC(RAND_CONV REAL_RAT_REDUCE_CONV) THEN REWRITE_TAC[] THEN REWRITE_TAC[REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[REAL_OF_NUM_LE; ARITH] THEN ONCE_REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_LE_MUL; REAL_LE_INV_EQ; REAL_POS; REAL_POW_LE; REAL_ABS_POS] THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN EXISTS_TAC `&(SUC(SUC p))` THEN SIMP_TAC[REAL_MUL_ASSOC; REAL_MUL_RINV; REAL_OF_NUM_EQ; NOT_SUC] THEN REWRITE_TAC[REAL_INV_1; REAL_MUL_LID; REAL_MUL_RID] THEN REWRITE_TAC[REAL_OF_NUM_LT; REAL_OF_NUM_LE] THEN ARITH_TAC; MATCH_MP_TAC REAL_LE_RCANCEL_IMP THEN EXISTS_TAC `&2 pow n` THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN SIMP_TAC[REAL_MUL_LINV; REAL_POW_EQ_0; REAL_OF_NUM_EQ; ARITH_EQ] THEN SIMP_TAC[REAL_POW_LT; REAL_OF_NUM_LT; ARITH; REAL_MUL_RID] THEN MATCH_MP_TAC(REAL_ARITH `!y. abs(x - y) < &1 /\ abs(y) <= d - &1 ==> abs(x) <= d`) THEN EXISTS_TAC `&2 pow n * --x` THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_RCANCEL_IMP THEN EXISTS_TAC `inv(&2 pow n)` THEN SIMP_TAC[REAL_LT_INV_EQ; REAL_POW_LT; REAL_OF_NUM_LT; ARITH] THEN REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_NEG; REAL_ABS_POW; REAL_ABS_NUM] THEN GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] THEN SIMP_TAC[REAL_MUL_ASSOC; REAL_MUL_LINV; REAL_POW_EQ_0; REAL_OF_NUM_EQ; ARITH_EQ] THEN REWRITE_TAC[REAL_MUL_LID] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&1 / &2` THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[real_div; REAL_SUB_RDISTRIB; GSYM REAL_MUL_ASSOC] THEN SIMP_TAC[REAL_MUL_RINV; REAL_POW_EQ_0; REAL_OF_NUM_EQ; ARITH_EQ] THEN REWRITE_TAC[REAL_MUL_LID; REAL_MUL_RID] THEN REWRITE_TAC[REAL_LE_SUB_LADD] THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN REWRITE_TAC[GSYM REAL_LE_SUB_LADD] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[real_div; REAL_MUL_LID] THEN MATCH_MP_TAC REAL_LE_INV2 THEN REWRITE_TAC[REAL_OF_NUM_LT; ARITH] THEN SUBST1_TAC(SYM(REAL_INT_REDUCE_CONV `&2 pow 2`)) THEN MATCH_MP_TAC REAL_POW_MONO THEN ASM_REWRITE_TAC[REAL_OF_NUM_LE; ARITH]]; ALL_TAC] THEN SUBGOAL_THEN `--(&1) pow p * s * x pow (SUC p) / &(SUC(SUC p)) - &2 pow n * --(&1) pow (SUC p) * x pow (SUC(SUC p)) / &(SUC(SUC p)) = (--(&1) pow p * x pow (SUC p) / &(SUC(SUC p))) * (s - &2 pow n * --x)` SUBST1_TAC THENL [REWRITE_TAC[real_pow; real_div; GSYM REAL_OF_NUM_SUC] THEN REWRITE_TAC[REAL_SUB_LDISTRIB; GSYM REAL_MUL_ASSOC] THEN REWRITE_TAC[REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_MUL_LID] THEN REWRITE_TAC[REAL_NEG_NEG; REAL_MUL_AC]; ALL_TAC] THEN ONCE_REWRITE_TAC[REAL_ABS_MUL] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `abs (-- (&1) pow p * x pow SUC p / &(SUC (SUC p))) * &1` THEN ASM_SIMP_TAC[REAL_LE_LMUL; REAL_ABS_POS; REAL_LT_IMP_LE] THEN REWRITE_TAC[REAL_MUL_RID; real_div; REAL_ABS_MUL; REAL_ABS_POW; REAL_ABS_NEG; REAL_ABS_NUM; REAL_ABS_INV] THEN REWRITE_TAC[REAL_POW_ONE; REAL_MUL_LID] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `inv(&2) pow 1 * inv(&2)` THEN CONJ_TAC THENL [ALL_TAC; CONV_TAC REAL_RAT_REDUCE_CONV] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_ABS_POS; REAL_POW_LE; REAL_LE_INV_EQ; LE_0; REAL_OF_NUM_LE] THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `inv(&2) pow (SUC p)` THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_POW_LE2 THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN ASM_REWRITE_TAC[REAL_ABS_POS]; REWRITE_TAC[REAL_POW_INV] THEN MATCH_MP_TAC REAL_LE_INV2 THEN CONJ_TAC THENL [CONV_TAC REAL_RAT_REDUCE_CONV; ALL_TAC] THEN MATCH_MP_TAC REAL_POW_MONO THEN REWRITE_TAC[REAL_OF_NUM_LE; ARITH] THEN ARITH_TAC]; MATCH_MP_TAC REAL_LE_INV2 THEN REWRITE_TAC[REAL_OF_NUM_LT; ARITH; REAL_OF_NUM_LE] THEN ARITH_TAC]);;
(* ------------------------------------------------------------------------- *) (* Special version of Taylor series for exponential in limited range. *) (* ------------------------------------------------------------------------- *)
let MCLAURIN_EXP_LE1 = 
prove (`!x n. abs(x) <= &1 ==> ?t. abs(t) <= &1 /\ (exp(x) = sum(0,n) (\m. x pow m / &(FACT m)) + (exp(t) / &(FACT n)) * x pow n)`,
REPEAT STRIP_TAC THEN MP_TAC(SPECL [`x:real`; `n:num`] MCLAURIN_EXP_LE) THEN DISCH_THEN(X_CHOOSE_THEN `t:real` STRIP_ASSUME_TAC) THEN EXISTS_TAC `t:real` THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `abs(x)` THEN ASM_REWRITE_TAC[]);;
let REAL_EXP_15 = 
prove (`exp(&1) < &5`,
SUBST1_TAC(SYM(REAL_RAT_REDUCE_CONV `inv(&2) + inv(&2)`)) THEN REWRITE_TAC[REAL_EXP_ADD] THEN MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `(&1 + &2 * inv(&2)) * (&1 + &2 * inv(&2))` THEN CONV_TAC(RAND_CONV REAL_RAT_REDUCE_CONV) THEN REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[REAL_EXP_POS_LE] THEN MATCH_MP_TAC REAL_EXP_BOUND_LEMMA THEN CONV_TAC REAL_RAT_REDUCE_CONV);;
let TAYLOR_EXP_WEAK = 
prove (`abs(x) <= &1 ==> abs(exp(x) - sum(0,m) (\i. x pow i / &(FACT i))) < &5 * inv(&(FACT m))`,
DISCH_TAC THEN FIRST_ASSUM(MP_TAC o SPEC `m:num` o MATCH_MP MCLAURIN_EXP_LE1) THEN DISCH_THEN(X_CHOOSE_THEN `t:real` STRIP_ASSUME_TAC) THEN ASM_REWRITE_TAC[REAL_ARITH `abs((x + y) - x) = abs(y)`] THEN REWRITE_TAC[real_div; REAL_ABS_MUL; GSYM REAL_MUL_ASSOC] THEN ASM_CASES_TAC `x = &0` THENL [ASM_REWRITE_TAC[] THEN SPEC_TAC(`m:num`,`m:num`) THEN INDUCT_TAC THENL [REWRITE_TAC[real_pow; FACT; ABS_N; REAL_INV_1; REAL_MUL_RID] THEN ASM_REWRITE_TAC[real_abs; REAL_EXP_POS_LE] THEN MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `exp(&1)` THEN REWRITE_TAC[REAL_EXP_15] THEN REWRITE_TAC[REAL_EXP_MONO_LE] THEN UNDISCH_TAC `abs(t) <= &1` THEN REAL_ARITH_TAC; REWRITE_TAC[POW_0; REAL_ABS_0; REAL_MUL_RZERO] THEN MATCH_MP_TAC REAL_LT_MUL THEN REWRITE_TAC[REAL_OF_NUM_LT; ARITH] THEN MATCH_MP_TAC REAL_INV_POS THEN REWRITE_TAC[REAL_OF_NUM_LT; FACT_LT]]; MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&5 * abs(inv(&(FACT m))) * abs(x pow m)` THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LT_RMUL_IMP THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `abs(exp(&1))` THEN ASM_REWRITE_TAC[real_abs; REAL_EXP_POS_LE; REAL_EXP_MONO_LE; REAL_EXP_15] THEN UNDISCH_TAC `abs(t) <= &1` THEN REAL_ARITH_TAC; MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[GSYM ABS_NZ; REAL_POW_EQ_0] THEN REWRITE_TAC[REAL_INV_EQ_0; REAL_OF_NUM_EQ] THEN MP_TAC(SPEC `m:num` FACT_LT) THEN ARITH_TAC]; MATCH_MP_TAC REAL_LE_LMUL_IMP THEN REWRITE_TAC[REAL_OF_NUM_LE; ARITH] THEN GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[REAL_ABS_POS] THEN REWRITE_TAC[REAL_ABS_INV; ABS_N; REAL_LE_REFL] THEN REWRITE_TAC[REAL_ABS_POW] THEN MATCH_MP_TAC REAL_POW_1_LE THEN ASM_REWRITE_TAC[REAL_ABS_POS]]]);;
let REAL_EXP_13 = 
prove (`exp(&1) < &3`,
MP_TAC(INST [`&1`,`x:real`; `5`,`m:num`] TAYLOR_EXP_WEAK) THEN CONV_TAC(ONCE_DEPTH_CONV REAL_SUM_CONV) THEN REWRITE_TAC[ADD_CLAUSES] THEN CONV_TAC(ONCE_DEPTH_CONV NUM_FACT_CONV) THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN MATCH_MP_TAC(REAL_ARITH `b + e <= c ==> abs(a - b) < e ==> a < c`) THEN CONV_TAC REAL_RAT_REDUCE_CONV);;
let TAYLOR_EXP = 
prove (`abs(x) <= &1 ==> abs(exp(x) - sum(0,m) (\i. x pow i / &(FACT i))) < &3 * inv(&(FACT m))`,
DISCH_TAC THEN FIRST_ASSUM(MP_TAC o SPEC `m:num` o MATCH_MP MCLAURIN_EXP_LE1) THEN DISCH_THEN(X_CHOOSE_THEN `t:real` STRIP_ASSUME_TAC) THEN ASM_REWRITE_TAC[REAL_ARITH `abs((x + y) - x) = abs(y)`] THEN REWRITE_TAC[real_div; REAL_ABS_MUL; GSYM REAL_MUL_ASSOC] THEN ASM_CASES_TAC `x = &0` THENL [ASM_REWRITE_TAC[] THEN SPEC_TAC(`m:num`,`m:num`) THEN INDUCT_TAC THENL [REWRITE_TAC[real_pow; FACT; ABS_N; REAL_INV_1; REAL_MUL_RID] THEN ASM_REWRITE_TAC[real_abs; REAL_EXP_POS_LE] THEN MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `exp(&1)` THEN REWRITE_TAC[REAL_EXP_13] THEN REWRITE_TAC[REAL_EXP_MONO_LE] THEN UNDISCH_TAC `abs(t) <= &1` THEN REAL_ARITH_TAC; REWRITE_TAC[POW_0; REAL_ABS_0; REAL_MUL_RZERO] THEN MATCH_MP_TAC REAL_LT_MUL THEN REWRITE_TAC[REAL_OF_NUM_LT; ARITH] THEN MATCH_MP_TAC REAL_INV_POS THEN REWRITE_TAC[REAL_OF_NUM_LT; FACT_LT]]; MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&3 * abs(inv(&(FACT m))) * abs(x pow m)` THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LT_RMUL_IMP THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `abs(exp(&1))` THEN ASM_REWRITE_TAC[real_abs; REAL_EXP_POS_LE; REAL_EXP_MONO_LE; REAL_EXP_13] THEN UNDISCH_TAC `abs(t) <= &1` THEN REAL_ARITH_TAC; MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[GSYM ABS_NZ; REAL_POW_EQ_0] THEN REWRITE_TAC[REAL_INV_EQ_0; REAL_OF_NUM_EQ] THEN MP_TAC(SPEC `m:num` FACT_LT) THEN ARITH_TAC]; MATCH_MP_TAC REAL_LE_LMUL_IMP THEN REWRITE_TAC[REAL_OF_NUM_LE; ARITH] THEN GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[REAL_ABS_POS] THEN REWRITE_TAC[REAL_ABS_INV; ABS_N; REAL_LE_REFL] THEN REWRITE_TAC[REAL_ABS_POW] THEN MATCH_MP_TAC REAL_POW_1_LE THEN ASM_REWRITE_TAC[REAL_ABS_POS]]]);;
let TAYLOR_LN = 
prove (`&0 <= x /\ x <= inv(&2 pow k) ==> abs(ln(&1 + x) - sum(0,m) (\i. --(&1) pow i * x pow SUC i / & (SUC i))) < inv(&2 pow (k * SUC m) * &(SUC m))`,
let lemma = INST [`1`,`k:num`] (SYM(SPEC_ALL SUM_REINDEX)) in STRIP_TAC THEN UNDISCH_TAC `&0 <= x` THEN REWRITE_TAC[REAL_LE_LT] THEN DISCH_THEN(DISJ_CASES_THEN2 ASSUME_TAC (SUBST1_TAC o SYM)) THENL [ALL_TAC; REWRITE_TAC[real_pow; REAL_MUL_LZERO; REAL_MUL_RZERO; real_div] THEN REWRITE_TAC[SUM_0; REAL_ADD_RID; REAL_SUB_LZERO; LN_1] THEN REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_0] THEN SIMP_TAC[REAL_LT_INV_EQ; REAL_LT_MUL; REAL_POW_LT; REAL_OF_NUM_LT; LT_0; ARITH]] THEN SUBGOAL_THEN `!i. --(&1) pow i = --(&1) pow (SUC(SUC i))` (fun th -> ONCE_REWRITE_TAC[th]) THENL [REWRITE_TAC[real_pow; REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_NEG_NEG] THEN REWRITE_TAC[REAL_MUL_LID]; ALL_TAC] THEN REWRITE_TAC[ADD1; lemma] THEN REWRITE_TAC[ADD_CLAUSES] THEN ONCE_REWRITE_TAC[SUM_DIFF] THEN CONV_TAC(ONCE_DEPTH_CONV REAL_SUM_CONV) THEN REWRITE_TAC[real_div; REAL_INV_0; REAL_MUL_RZERO] THEN REWRITE_TAC[GSYM ADD1] THEN MP_TAC(SPECL [`x:real`; `SUC m`] MCLAURIN_LN_POS) THEN ASM_REWRITE_TAC[LT_0] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[GSYM ADD1] THEN REWRITE_TAC[GSYM real_div] THEN DISCH_THEN(X_CHOOSE_THEN `t:real` STRIP_ASSUME_TAC) THEN ASM_REWRITE_TAC[REAL_SUB_RZERO; REAL_ARITH `(a + b) - a = b`] THEN REWRITE_TAC[real_div; REAL_ABS_MUL; REAL_ABS_INV; REAL_ABS_POW] THEN REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_NUM; REAL_POW_ONE] THEN REWRITE_TAC[REAL_MUL_LID; REAL_INV_MUL; GSYM REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `inv (&2 pow (k * SUC m)) * inv (&(SUC m)) * inv(abs(&1 + t) pow SUC m)` THEN CONJ_TAC THENL [REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LE_RMUL THEN SIMP_TAC[REAL_LE_MUL; REAL_LE_INV_EQ; REAL_POS; REAL_ABS_POS; REAL_POW_LE] THEN REWRITE_TAC[GSYM REAL_POW_INV] THEN REWRITE_TAC[GSYM REAL_POW_POW] THEN MATCH_MP_TAC REAL_POW_LE2 THEN ASM_SIMP_TAC[REAL_POW_INV; real_abs; REAL_LT_IMP_LE]; GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN REWRITE_TAC[REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LT_LMUL THEN SIMP_TAC[REAL_LT_MUL; REAL_LT_INV_EQ; REAL_OF_NUM_LT; LT_0; REAL_POW_LT; ARITH] THEN REWRITE_TAC[GSYM REAL_POW_INV; GSYM REAL_ABS_INV] THEN SUBGOAL_THEN `abs(inv(&1 + t)) < &1` ASSUME_TAC THENL [REWRITE_TAC[REAL_ABS_INV] THEN GEN_REWRITE_TAC RAND_CONV [GSYM REAL_INV_1] THEN MATCH_MP_TAC REAL_LT_INV2 THEN UNDISCH_TAC `&0 < t` THEN REAL_ARITH_TAC; SUBST1_TAC(SYM(SPEC `SUC m` REAL_POW_ONE)) THEN MATCH_MP_TAC REAL_POW_LT2 THEN ASM_REWRITE_TAC[REAL_POW_ONE; NOT_SUC; REAL_ABS_POS]]]);;
(* ------------------------------------------------------------------------- *) (* Leading from the summation to the actual function. *) (* ------------------------------------------------------------------------- *)
let APPROX_LEMMA1 = 
prove (`abs(f(x:real) - sum(0,m) (\i. P i x)) < inv(&2 pow (n + 2)) /\ abs(u - &2 pow (n + e + 2) * sum(0,m) (\i. P i x)) <= &k * &m /\ &k * &m <= &2 pow e /\ abs(s * &2 pow (e + 2) - u) <= &2 pow (e + 1) ==> abs(s - &2 pow n * f(x)) < &1`,
STRIP_TAC THEN MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN EXISTS_TAC `&2 pow (n + e + 2)` THEN REWRITE_TAC[REAL_LT_POW2] THEN REWRITE_TAC[REAL_ABS_LEMMA; REAL_SUB_LDISTRIB; REAL_MUL_RID] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN (MATCH_MP_TAC o GEN_ALL) (REAL_ARITH `abs(a - b) + abs(b - c) < d ==> abs(a - c) < d`) THEN EXISTS_TAC `&2 pow n * u` THEN CONV_TAC(funpow 4 RAND_CONV num_CONV) THEN REWRITE_TAC[ADD_CLAUSES; real_pow; REAL_MUL_2] THEN MATCH_MP_TAC REAL_LET_ADD2 THEN CONJ_TAC THENL [ONCE_REWRITE_TAC[REAL_POW_ADD] THEN GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o LAND_CONV) [REAL_MUL_SYM] THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC; GSYM REAL_SUB_LDISTRIB] THEN REWRITE_TAC[GSYM REAL_ABS_LEMMA] THEN MATCH_MP_TAC REAL_LE_LMUL THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN REWRITE_TAC[REAL_LT_POW2]; REWRITE_TAC[GSYM REAL_MUL_ASSOC; GSYM REAL_SUB_LDISTRIB] THEN GEN_REWRITE_TAC RAND_CONV [REAL_POW_ADD] THEN REWRITE_TAC[GSYM REAL_ABS_LEMMA] THEN MATCH_MP_TAC REAL_LT_LMUL THEN REWRITE_TAC[REAL_LT_POW2] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN (MATCH_MP_TAC o GEN_ALL) (REAL_ARITH `abs(a - b) + abs(b - c) < d ==> abs(a - c) < d`) THEN EXISTS_TAC `&2 pow (n + e + 2) * sum(0,m) (\i. P i (x:real))` THEN GEN_REWRITE_TAC RAND_CONV [REAL_POW_ADD] THEN GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN REWRITE_TAC[REAL_POW_1; REAL_MUL_2] THEN MATCH_MP_TAC REAL_LET_ADD2 THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&k * &m` THEN ASM_REWRITE_TAC[]; REWRITE_TAC[GSYM REAL_SUB_LDISTRIB; GSYM REAL_ABS_LEMMA] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[GSYM ADD_ASSOC] THEN ONCE_REWRITE_TAC[REAL_POW_ADD] THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN MATCH_MP_TAC REAL_LT_LMUL THEN REWRITE_TAC[REAL_LT_POW2] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN EXISTS_TAC `inv(&2 pow (n + 2))` THEN REWRITE_TAC[REAL_LT_INV_EQ; REAL_LT_POW2] THEN REWRITE_TAC[REAL_MUL_RID; REAL_MUL_ASSOC] THEN ONCE_REWRITE_TAC[REAL_ABS_SUB] THEN SUBGOAL_THEN `inv(&2 pow (n + 2)) * &2 pow (n + 2) = &1` (fun th -> ASM_REWRITE_TAC[th; REAL_MUL_LID]) THEN MATCH_MP_TAC REAL_MUL_LINV THEN REWRITE_TAC[REAL_POW_EQ_0] THEN REWRITE_TAC[DE_MORGAN_THM] THEN DISJ1_TAC THEN REAL_ARITH_TAC]]);;
(* ------------------------------------------------------------------------- *) (* Approximation theorems. *) (* ------------------------------------------------------------------------- *)
let APPROX_EXP = 
prove (`(n + e + 2 = p) /\ &3 * &2 pow (n + 2) <= &(FACT m) /\ &2 * &m <= &2 pow e /\ abs(x) <= &1 /\ abs(s - &2 pow p * x) < &1 /\ (t(0) = &2 pow p) /\ (!k. SUC k < m ==> &2 * abs(t(SUC k) * &2 pow p * &(SUC k) - s * t(k)) <= &2 pow p * &(SUC k)) /\ abs(u * &2 pow (e + 2) - sum(0,m) t) <= &2 pow (e + 1) ==> abs(u - &2 pow n * exp(x)) < &1`,
STRIP_TAC THEN MATCH_MP_TAC(GEN_ALL APPROX_LEMMA1) THEN MAP_EVERY EXISTS_TAC [`\i x. x pow i / &(FACT i)`; `2`; `m:num`; `sum(0,m) t`; `e:num`] THEN ASM_REWRITE_TAC[BETA_THM] THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&3 * inv(&(FACT m))` THEN CONJ_TAC THENL [MATCH_MP_TAC TAYLOR_EXP THEN ASM_REWRITE_TAC[]; SUBST1_TAC(SYM(SPEC `&3` REAL_INV_INV)) THEN REWRITE_TAC[GSYM REAL_INV_MUL] THEN MATCH_MP_TAC REAL_LE_INV2 THEN ASM_REWRITE_TAC[REAL_LT_POW2] THEN MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN EXISTS_TAC `&3` THEN REWRITE_TAC[REAL_MUL_ASSOC] THEN REWRITE_TAC[MATCH_MP REAL_MUL_RINV (REAL_ARITH `~(&3 = &0)`)] THEN ASM_REWRITE_TAC[REAL_MUL_LID] THEN REAL_ARITH_TAC]; MATCH_MP_TAC STEPS_EXP THEN ASM_REWRITE_TAC[]]);;
let APPROX_LN = 
prove (`~(k = 0) /\ (n + e + 2 = p) /\ &2 pow (n + 2) <= &2 pow (k * SUC m) * &(SUC m) /\ &3 * &m <= &2 pow e /\ (&0 <= x /\ x <= inv(&2 pow k)) /\ abs(s - &2 pow p * --x) < &1 /\ (t(0) = --s) /\ (!k. SUC k < m ==> &2 * abs(t(SUC k) * &2 pow p * &(SUC(SUC k)) - &(SUC k) * s * t(k)) <= &2 pow p * &(SUC(SUC k))) /\ abs(u * &2 pow (e + 2) - sum(0,m) t) <= &2 pow (e + 1) ==> abs(u - &2 pow n * ln(&1 + x)) < &1`,
STRIP_TAC THEN (MATCH_MP_TAC o GEN_ALL o BETA_RULE) (INST [`\x. ln(&1 + x):real`,`f:real->real`] APPROX_LEMMA1) THEN MAP_EVERY EXISTS_TAC [`\i x. (--(&1)) pow i * x pow (SUC i) / &(SUC i)`; `3`; `m:num`; `sum(0,m) t`; `e:num`] THEN ASM_REWRITE_TAC[BETA_THM] THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `inv(&2 pow (k * SUC m) * &(SUC m))` THEN CONJ_TAC THENL [MATCH_MP_TAC TAYLOR_LN THEN ASM_REWRITE_TAC[]; MATCH_MP_TAC REAL_LE_INV2 THEN ASM_REWRITE_TAC[REAL_LT_POW2]]; MATCH_MP_TAC STEPS_LN THEN ASM_REWRITE_TAC[] THEN SUBGOAL_THEN `2 <= (n + e + 2)` MP_TAC THENL [REWRITE_TAC[ADD_ASSOC] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[LE_ADD]; SUBGOAL_THEN `abs(x) <= &1 / &2` (fun th -> ASM_REWRITE_TAC[th]) THEN ASM_REWRITE_TAC[real_abs] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `inv(&2 pow k)` THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[real_div; REAL_MUL_LID] THEN GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM REAL_POW_1] THEN MATCH_MP_TAC REAL_LE_INV2 THEN REWRITE_TAC[REAL_LT_POW2] THEN MATCH_MP_TAC REAL_POW_MONO THEN REWRITE_TAC[REAL_OF_NUM_LE; ARITH] THEN UNDISCH_TAC `~(k = 0)` THEN ARITH_TAC]]);;
(* ------------------------------------------------------------------------- *) (* Eliminate trivial definitions. *) (* ------------------------------------------------------------------------- *) let ELIMINATE_DEF = let x_tm = `x:num` and a_tm = `&0` and sconv = REWRITE_CONV[ARITH] in fun tdefs th -> if tdefs = [] then th else let ctm = itlist (fun tm acc -> let l,r = (rand F_F I) (dest_eq tm) in mk_cond(mk_eq(x_tm,l),r,acc)) tdefs a_tm in let atm = mk_abs(x_tm,ctm) in let ttm = rator(lhs(hd tdefs)) in let tth = ASSUME(mk_eq(ttm,atm)) in let ths = map (EQT_ELIM o CONV_RULE(RAND_CONV sconv) o SUBS_CONV[tth]) tdefs in let dth = PROVE_HYP (end_itlist CONJ ths) th in MP (INST [atm,ttm] (DISCH_ALL dth)) (REFL atm);; (* ------------------------------------------------------------------------- *) (* Overall conversion. *) (* ------------------------------------------------------------------------- *) let realcalc_cache = ref [];; let REALCALC_CONV,thm_eval,raw_eval,thm_wrap = let a_tm = `a:real` and n_tm = `n:num` and n'_tm = `n':num` and m_tm = `m:num` and b_tm = `b:real` and e_tm = `e:num` and c_tm = `c:real` and neg_tm = `(--)` and abs_tm = `abs` and inv_tm = `inv` and sqrt_tm = `sqrt` and add_tm = `(+)` and mul_tm = `(*)` and sub_tm = `(-)` and exp_tm = `exp:real->real` and ln_tm = `ln:real->real` and add1_tm = `(+) (&1)` and pow2_tm = `(pow) (&2)` and one_tm = `&1` and lt_tm = `(<)` in let INTEGER_PROVE = EQT_ELIM o REWRITE_CONV[REAL_EQ_NEG2; GSYM EXISTS_REFL; EXISTS_OR_THM; REAL_OF_NUM_EQ] in let ndiv x y = let q = quo_num x y in let r = x -/ (q */ y) in if le_num (abs_num(Int 2 */ r)) (abs_num y) then q else if le_num (abs_num(Int 2 */ (r -/ y))) (abs_num y) then q +/ Int 1 else if le_num (abs_num(Int 2 */ (r +/ y))) (abs_num y) then q -/ Int 1 else let s = (string_of_num x)^" and "^(string_of_num y) in failwith ("ndiv: "^s) in let raw_wrap (f:num->num) = (ref(Int(-1),Int 0),f) in let raw_eval(r,(f:num->num)) n = let (n0,y0) = !r in if le_num n n0 then ndiv y0 (power_num (Int 2) (n0 -/ n)) else let y = f n in (r := (n,y); y) in let thm_eval = let SUC_tm = `SUC` and mk_add = mk_binop `(+):num->num->num` in fun (r,(f:num->thm)) n -> let (n0,y0th) = !r in if le_num n n0 then if n =/ n0 then y0th else let th1 = NUM_SUC_CONV (mk_comb(SUC_tm,mk_numeral(n0 -/ (n +/ Int 1)))) in let th2 = MATCH_MP REALCALC_DOWNGRADE th1 in let th3 = NUM_ADD_CONV(mk_add(mk_numeral(n)) (mk_numeral(n0 -/ n))) in let th4 = MATCH_MP th2 th3 in let th5 = MATCH_MP th4 y0th in let tm5 = fst(dest_imp(concl th5)) in let tm5a,tm5b = dest_comb tm5 in let th6 = REAL_INT_POW_CONV tm5b in let tm5c = rand(rand tm5a) in let tm5d,tm5e = dest_comb tm5c in let tm5f,tm5g = dest_comb(rand tm5d) in let tm5h = rand(rand tm5f) in let bin = mk_realintconst (ndiv (dest_realintconst tm5e) (power_num (Int 2) (dest_numeral tm5h))) in let th7 = AP_TERM (rator(rand tm5f)) th1 in let th8 = GEN_REWRITE_RULE LAND_CONV [CONJUNCT2 real_pow] th7 in let th9 = SYM(GEN_REWRITE_RULE (LAND_CONV o RAND_CONV) [th6] th8) in let th10 = TRANS th9 (REAL_INT_MUL_CONV (rand(concl th9))) in let th11 = AP_THM (AP_TERM (rator tm5f) th10) bin in let th12 = TRANS th11 (REAL_INT_MUL_CONV (rand(concl th11))) in let th13 = AP_THM (AP_TERM (rator tm5d) th12) tm5e in let th14 = TRANS th13 (REAL_INT_SUB_CONV (rand(concl th13))) in let th15 = AP_TERM (rator(rand tm5a)) th14 in let th16 = TRANS th15 (REAL_INT_ABS_CONV (rand(concl th15))) in let th17 = MK_COMB(AP_TERM (rator tm5a) th16,th6) in let th18 = TRANS th17 (REAL_INT_LE_CONV (rand(concl th17))) in MATCH_MP th5 (EQT_ELIM th18) else let yth = f n in (r := (n,yth); yth) in let thm_wrap (f:num->thm) = (ref(Int(-1),TRUTH),f) in let find_msd = let rec find_msd n f = if Int 1 </ abs_num(raw_eval f n) then n else find_msd (n +/ Int 1) f in find_msd (Int 0) in let find_acc = let rec find_msd n f = if Int 32 </ abs_num(raw_eval f n) then n else find_msd (n +/ Int 1) f in find_msd (Int 0) in let find_ubound f = let k = find_acc f in let a = abs_num(raw_eval f k) in k -/ log2 (a +/ Int 1) in let REALCALC_EXP_CONV = let t_tm = `t:num->real` and n_tm = `n:num` and m_tm = `m:num` and e_tm = `e:num` and p_tm = `p:num` and s_tm = `s:real` and u_tm = `u:real` and x_tm = `x:real` in let rec calculate_m acc i r = if acc >=/ r then i else let i' = i +/ Int 1 in calculate_m (i' */ acc) i' r in let calculate_exp_sequence = let rec calculate_exp_sequence p2 s i = if i </ Int 0 then [] else if i =/ Int 0 then [p2] else let acc = calculate_exp_sequence p2 s (i -/ Int 1) in let t = hd acc in let t' = ndiv (s */ t) (p2 */ i) in t'::acc in fun p s m -> let p2 = power_num (Int 2) p in rev(calculate_exp_sequence p2 s (m -/ Int 1)) in let pth = prove (`abs(x) <= &1 ==> abs(s - &2 pow p * x) < &1 ==> (n + e + 2 = p) /\ &3 * &2 pow (n + 2) <= &(FACT m) /\ &2 * &m <= &2 pow e /\ (t(0) = &2 pow p) /\ (!k. SUC k < m ==> &2 * abs(t(SUC k) * &2 pow p * &(SUC k) - s * t(k)) <= &2 pow p * &(SUC k)) /\ abs(u * &2 pow (e + 2) - sum(0,m) t) <= &2 pow (e + 1) ==> abs(u - &2 pow n * exp(x)) < &1`, REPEAT STRIP_TAC THEN MATCH_MP_TAC APPROX_EXP THEN ASM_REWRITE_TAC[]) in let LEFT_ZERO_RULE = ONCE_REWRITE_RULE[prove(`0 + n = n`,REWRITE_TAC[ADD_CLAUSES])] in fun (fn1,fn2) -> let raw_fn n = let m = calculate_m (Int 1) (Int 0) (Int 3 */ (power_num (Int 2) (n +/ Int 2))) in let e = log2 (Int 2 */ m) in let p = n +/ e +/ Int 2 in let s = raw_eval fn1 p in let seq = calculate_exp_sequence p s m in let u0 = itlist (+/) seq (Int 0) in ndiv u0 (power_num (Int 2) (e +/ Int 2)) and thm_fn n = let m = calculate_m (Int 1) (Int 0) (Int 3 */ (power_num (Int 2) (n +/ Int 2))) in let e = log2 (Int 2 */ m) in let p = n +/ e +/ Int 2 in let sth = thm_eval fn2 p in let tm1 = rand(lhand(concl sth)) in let s_num = lhand tm1 in let x_num = rand(rand tm1) in let s = dest_realintconst s_num in let seq = calculate_exp_sequence p s m in let u0 = itlist (+/) seq (Int 0) in let u = ndiv u0 (power_num (Int 2) (e +/ Int 2)) in let m_num = mk_numeral m and n_num = mk_numeral n and e_num = mk_numeral e and p_num = mk_numeral p and u_num = mk_realintconst u in let tdefs = map2 (fun a b -> mk_eq(mk_comb(t_tm,mk_small_numeral a), mk_realintconst b)) (0--(length seq - 1)) seq in let p2th = REAL_INT_POW_CONV (mk_comb(pow2_tm,p_num)) in let th0 = INST [m_num,m_tm; n_num,n_tm; e_num,e_tm; x_num,x_tm; p_num,p_tm; s_num,s_tm; u_num,u_tm] pth in let th0' = MP th0 (EQT_ELIM(REAL_RAT_REDUCE_CONV(lhand(concl th0)))) in let th1 = MP th0' sth in let th2 = CONV_RULE (ONCE_DEPTH_CONV EXPAND_RANGE_CONV) th1 in let th3 = LEFT_ZERO_RULE (CONV_RULE (ONCE_DEPTH_CONV REAL_SUM_CONV) th2) in let ths = try CONJUNCTS(ASSUME(list_mk_conj tdefs)) with Failure _ -> [] in let th4 = SUBS (p2th::ths) th3 in let th5 = CONV_RULE (LAND_CONV (DEPTH_CONV NUM_ADD_CONV THENC ONCE_DEPTH_CONV NUM_FACT_CONV THENC REAL_INT_REDUCE_CONV)) th4 in MP (ELIMINATE_DEF tdefs th5) TRUTH in raw_wrap raw_fn,thm_wrap thm_fn in let REALCALC_LN_CONV = let t_tm = `t:num->real` and n_tm = `n:num` and m_tm = `m:num` and e_tm = `e:num` and p_tm = `p:num` and s_tm = `s:real` and u_tm = `u:real` and k_tm = `k:num` and x_tm = `x:real` in let rec calculate_m acc k2 m r = if acc */ (m +/ Int 1) >=/ r then m else calculate_m (k2 */ acc) k2 (m +/ Int 1) r in let calculate_ln_sequence = let rec calculate_ln_sequence p2 s i = if i </ Int 0 then [] else if i =/ Int 0 then [s] else let acc = calculate_ln_sequence p2 s (i -/ Int 1) in let t = hd acc in let t' = ndiv (Int(-1) */ s */ t */ i) (p2 */ (i +/ Int 1)) in t'::acc in fun p s m -> let p2 = power_num (Int 2) p in rev(calculate_ln_sequence p2 s (m -/ Int 1)) in let pth = prove (`&0 <= x /\ x <= inv(&2 pow k) ==> abs(s - &2 pow p * x) < &1 ==> ~(k = 0) /\ (n + e + 2 = p) /\ &2 pow (n + 2) <= &2 pow (k * SUC m) * &(SUC m) /\ &3 * &m <= &2 pow e /\ (t(0) = s) /\ (!k. SUC k < m ==> &2 * abs(t(SUC k) * &2 pow p * &(SUC(SUC k)) - &(SUC k) * --s * t(k)) <= &2 pow p * &(SUC(SUC k))) /\ abs(u * &2 pow (e + 2) - sum(0,m) t) <= &2 pow (e + 1) ==> abs(u - &2 pow n * ln(&1 + x)) < &1`, REPEAT STRIP_TAC THEN MATCH_MP_TAC(INST [`--s`,`s:real`] APPROX_LN) THEN ASM_REWRITE_TAC[REAL_NEG_NEG] THEN REWRITE_TAC[REAL_MUL_RNEG] THEN REWRITE_TAC[REAL_ARITH `abs(--a - --b) = abs(a - b)`] THEN ASM_REWRITE_TAC[]) in let LEFT_ZERO_RULE = ONCE_REWRITE_RULE[prove(`0 + n = n`,REWRITE_TAC[ADD_CLAUSES])] in let pow2_tm = `(pow) (&2)` in let default_tdefs = [`t 0 = &0`] in fun (fn1,fn2) -> let raw_fn n = let k = find_ubound fn1 in if k </ Int 1 then failwith "ln of number not provably <= 1/2" else let k2 = power_num (Int 2) k in let m = calculate_m k2 k2 (Int 0) (power_num (Int 2) (n +/ Int 2)) in let e = log2 (Int 3 */ m) in let p = n +/ e +/ Int 2 in let s = raw_eval fn1 p in let seq = calculate_ln_sequence p s m in let u0 = itlist (+/) seq (Int 0) in ndiv u0 (power_num (Int 2) (e +/ Int 2)) and thm_fn n = let k = find_ubound fn1 in if k </ Int 1 then failwith "ln of number not provably <= 1/2" else let k2 = power_num (Int 2) k in let m = calculate_m k2 k2 (Int 0) (power_num (Int 2) (n +/ Int 2)) in let e = log2 (Int 3 */ m) in let p = n +/ e +/ Int 2 in let sth = thm_eval fn2 p in let tm1 = rand(lhand(concl sth)) in let s_num = lhand tm1 in let x_num = rand(rand tm1) in let s = dest_realintconst s_num in let seq = calculate_ln_sequence p s m in let u0 = itlist (+/) seq (Int 0) in let u = ndiv u0 (power_num (Int 2) (e +/ Int 2)) in let m_num = mk_numeral m and n_num = mk_numeral n and e_num = mk_numeral e and p_num = mk_numeral p and k_num = mk_numeral k and u_num = mk_realintconst u in let tdefs0 = map2 (fun a b -> mk_eq(mk_comb(t_tm,mk_small_numeral a), mk_realintconst b)) (0--(length seq - 1)) seq in let tdefs = if tdefs0 = [] then default_tdefs else tdefs0 in let p2th = REAL_INT_POW_CONV (mk_comb(pow2_tm,p_num)) in let th0 = INST [m_num,m_tm; n_num,n_tm; e_num,e_tm; k_num,k_tm; x_num,x_tm; p_num,p_tm; s_num,s_tm; u_num,u_tm] pth in let th0' = MP th0 (EQT_ELIM(REAL_RAT_REDUCE_CONV(lhand(concl th0)))) in let th1 = MP th0' sth in let th2 = CONV_RULE (ONCE_DEPTH_CONV EXPAND_RANGE_CONV) th1 in let th3 = LEFT_ZERO_RULE (CONV_RULE (ONCE_DEPTH_CONV REAL_SUM_CONV) th2) in let ths = try CONJUNCTS(ASSUME(list_mk_conj tdefs)) with Failure _ -> [] in let th4 = SUBS (p2th::ths) th3 in let th5 = CONV_RULE (LAND_CONV (NUM_REDUCE_CONV THENC REAL_INT_REDUCE_CONV)) th4 in MP (ELIMINATE_DEF tdefs th5) TRUTH in raw_wrap raw_fn,thm_wrap thm_fn in let REALCALC_SQRT_CONV = let num_sqrt = let rec isolate_sqrt (a,b) y = if abs_num(a -/ b) <=/ Int 1 then if abs_num(a */ a -/ y) <=/ a then a else b else let c = quo_num (a +/ b) (Int 2) in if c */ c <=/ y then isolate_sqrt (c,b) y else isolate_sqrt (a,c) y in fun n -> isolate_sqrt (Int 0,n) n in let MATCH_pth = MATCH_MP REALCALC_SQRT in let b_tm = `b:real` in let PROVE_1_LE_SQRT = let pth = prove (`&1 <= x ==> &1 <= sqrt(x)`, DISCH_THEN(fun th -> ASSUME_TAC(MATCH_MP (REAL_ARITH `&1 <= x ==> &0 <= x`) th) THEN MP_TAC th) THEN CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[REAL_NOT_LE] THEN DISCH_TAC THEN SUBGOAL_THEN `x = sqrt(x) pow 2` SUBST1_TAC THENL [CONV_TAC SYM_CONV THEN ASM_REWRITE_TAC[SQRT_POW2]; GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN REWRITE_TAC[POW_2] THEN MATCH_MP_TAC REAL_LT_MUL2 THEN ASM_SIMP_TAC[SQRT_POS_LE]]) in let tac = REPEAT(MATCH_MP_TAC pth) THEN CONV_TAC REAL_RAT_LE_CONV in fun tm -> try prove(tm,tac) with Failure _ -> failwith "Need root body >= &1" in fun (fn1,fn2) -> let raw_fn n = num_sqrt(power_num (Int 2) n */ raw_eval fn1 n) and thm_fn n = let th1 = MATCH_pth(thm_eval fn2 n) in let th2 = MP th1 (PROVE_1_LE_SQRT(lhand(concl th1))) in let th3 = CONV_RULE(funpow 2 LAND_CONV (funpow 2 RAND_CONV REAL_RAT_REDUCE_CONV)) th2 in let k = dest_realintconst(rand(rand(lhand(lhand(concl th3))))) in let th4 = INST [mk_realintconst(num_sqrt k),b_tm] th3 in MP th4 (EQT_ELIM(REAL_RAT_REDUCE_CONV(lhand(concl th4)))) in raw_wrap raw_fn,thm_wrap thm_fn in let rec REALCALC_CONV tm = try assoc tm (!realcalc_cache) with Failure _ -> if is_ratconst tm then let x = rat_of_term tm in let raw_fn acc = floor_num ((power_num (Int 2) acc) */ x) and thm_fn acc = let a = floor_num ((power_num (Int 2) acc) */ x) in let atm = mk_realintconst a in let rtm = mk_comb(mk_comb(mul_tm,mk_comb(pow2_tm,mk_numeral acc)),tm) in let btm = mk_comb(abs_tm,mk_comb(mk_comb(sub_tm,atm),rtm)) in let ftm = mk_comb(mk_comb(lt_tm,btm),one_tm) in EQT_ELIM(REAL_RAT_REDUCE_CONV ftm) in raw_wrap raw_fn,thm_wrap thm_fn else let lop,r = dest_comb tm in if lop = neg_tm then let rfn,tfn = REALCALC_CONV r in let raw_fn acc = minus_num (raw_eval rfn acc) and thm_fn acc = let th1 = thm_eval tfn acc in let th2 = MATCH_MP REALCALC_NEG th1 in try EQ_MP (LAND_CONV(RAND_CONV(LAND_CONV REAL_INT_NEG_CONV)) (concl th2)) th2 with Failure _ -> th2 in raw_wrap raw_fn,thm_wrap thm_fn else if lop = abs_tm then let rfn,tfn = REALCALC_CONV r in let raw_fn acc = abs_num (raw_eval rfn acc) and thm_fn acc = let th1 = thm_eval tfn acc in let th2 = MATCH_MP REALCALC_ABS th1 in CONV_RULE (LAND_CONV(RAND_CONV(LAND_CONV REAL_INT_ABS_CONV))) th2 in raw_wrap raw_fn,thm_wrap thm_fn else if lop = sqrt_tm then REALCALC_SQRT_CONV(REALCALC_CONV r) else if lop = inv_tm then let rfn,tfn = REALCALC_CONV r in let x0 = raw_eval rfn (Int 0) in let ax0 = abs_num x0 in let r = log2(ax0) -/ Int 1 in let get_ek(acc) = if r < Int 0 then let p = find_msd rfn in let e = acc +/ p +/ Int 1 in let k = e +/ p in e,k else let k = let k0 = acc +/ Int 1 -/ (Int 2 */ r) in if k0 </ Int 0 then Int 0 else k0 in let e = r +/ k in e,k in let raw_fn acc = let _,k = get_ek(acc) in let nk2 = power_num (Int 2) (acc +/ k) in ndiv nk2 (raw_eval rfn k) in let thm_fn acc = let e,k = get_ek(acc) in let nk2 = power_num (Int 2) (acc +/ k) in let th1 = thm_eval tfn k in let atm = lhand(rand(lhand(concl th1))) in let a = dest_realintconst atm in let b = ndiv nk2 a in let btm = mk_realintconst b in let etm = mk_numeral e in let ntm = mk_numeral acc in let th2 = MATCH_MP REALCALC_INV th1 in let th3 = INST [btm,b_tm; etm,e_tm; ntm,n_tm] th2 in let th4 = MP th3 (INTEGER_PROVE(lhand(concl th3))) in let th5 = MP th4 (INTEGER_PROVE(lhand(concl th4))) in let th6 = MP th5 (EQT_ELIM(NUM_REDUCE_CONV(lhand(concl th5)))) in let th7 = MP th6 (EQT_ELIM(REAL_INT_REDUCE_CONV(lhand(concl th6)))) in MP th7 (EQT_ELIM(((LAND_CONV (funpow 4 RAND_CONV NUM_ADD_CONV) THENC REAL_INT_REDUCE_CONV) (lhand(concl th7))))) in raw_wrap raw_fn,thm_wrap thm_fn else if lop = exp_tm then let rfn,tfn = REALCALC_CONV r in REALCALC_EXP_CONV (rfn,tfn) else if lop = ln_tm then let r1,r2 = dest_comb r in if r1 = add1_tm then let rfn,tfn = REALCALC_CONV r2 in REALCALC_LN_CONV (rfn,tfn) else failwith "Can only do logs like ln(&1 + x) for small rational x" else let op,l = dest_comb lop in if op = add_tm then let rfn1,tfn1 = REALCALC_CONV l and rfn2,tfn2 = REALCALC_CONV r in let raw_fn acc = let acc' = acc +/ Int 2 in ndiv (raw_eval rfn1 acc' +/ raw_eval rfn2 acc') (Int 4) and thm_fn acc = let acc' = acc +/ Int 2 in let th1 = INST [mk_numeral acc,n_tm] REALCALC_ADD in let th2 = MATCH_MP th1 (NUM_ADD_CONV (lhand(lhand(concl th1)))) in let th3 = thm_eval tfn1 acc' in let th4 = MATCH_MP th2 th3 in let th5 = thm_eval tfn2 acc' in let th6 = MATCH_MP th4 th5 in let n1 = dest_realintconst(lhand(rand(lhand(concl th3)))) and n2 = dest_realintconst(lhand(rand(lhand(concl th5)))) in let ci = mk_realintconst(ndiv (n1 +/ n2) (Int 4)) in let th7 = INST [ci,c_tm] th6 in let th8 = EQT_ELIM(REAL_INT_REDUCE_CONV(lhand(concl th7))) in MP th7 th8 in raw_wrap raw_fn,thm_wrap thm_fn else if op = mul_tm then let rfn1,tfn1 = REALCALC_CONV l and rfn2,tfn2 = REALCALC_CONV r in let get_kl(acc) = let n' = acc +/ Int 2 in let r = quo_num n' (Int 2) in let s = n' -/ r in let p = log2(abs_num(raw_eval rfn1 r)) and q = log2(abs_num(raw_eval rfn2 s)) in let k = q +/ r +/ Int 1 and l = p +/ s +/ Int 1 in if p =/ Int 0 & q = Int 0 then if k </ l then k +/ Int 1,l else k,l +/ Int 1 else k,l in let raw_fn acc = let k,l = get_kl acc in let m = (k +/ l) -/ acc in ndiv (raw_eval rfn1 k */ raw_eval rfn2 l) (power_num (Int 2) m) in let thm_fn acc = let k,l = get_kl acc in let m = (k +/ l) -/ acc in let th1a = thm_eval tfn1 k and th1b = thm_eval tfn2 l in let a = dest_realintconst(lhand(rand(lhand(concl th1a)))) and b = dest_realintconst(lhand(rand(lhand(concl th1b)))) in let c = ndiv (a */ b) (power_num (Int 2) m) in let ntm = mk_numeral acc and mtm = mk_numeral m and ctm = mk_realintconst c in let th1 = MATCH_MP REALCALC_MUL th1a in let th2 = MATCH_MP th1 th1b in let th3 = INST [ntm,n_tm; mtm,m_tm; ctm,c_tm] th2 in let th4 = MP th3 (EQT_ELIM(NUM_REDUCE_CONV(lhand(concl th3)))) in let th5 = MP th4 (EQT_ELIM(REAL_INT_REDUCE_CONV(lhand(concl th4)))) in MP th5 (EQT_ELIM(REAL_INT_REDUCE_CONV(lhand(concl th5)))) in raw_wrap raw_fn,thm_wrap thm_fn else failwith "No other operators work yet, sorry!" in REALCALC_CONV,thm_eval,raw_eval,thm_wrap;; (* ------------------------------------------------------------------------- *) (* Apply some conversion before doing approximation. *) (* ------------------------------------------------------------------------- *) let REALCALC_PRECONV conv tm = let th = conv tm in let rfn,tfn = REALCALC_CONV (rand(concl th)) in rfn, thm_wrap(fun n -> let th1 = thm_eval tfn n in GEN_REWRITE_RULE (LAND_CONV o funpow 3 RAND_CONV) [SYM th] th1);; (* ------------------------------------------------------------------------- *) (* Calculate ordering relation between two expressions. *) (* ------------------------------------------------------------------------- *)
let REALCALC_LT = 
prove (`abs(a - &2 pow n * x) < &1 /\ abs(b - &2 pow n * y) < &1 ==> &2 <= abs(a - b) ==> (x < y <=> a < b)`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `&2 pow n * x < &2 pow n * y` THEN CONJ_TAC THENL [SIMP_TAC[REAL_LT_LMUL_EQ; REAL_POW_LT; REAL_OF_NUM_LT; ARITH]; POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN REAL_ARITH_TAC]);;
let REALCALC_LE = 
prove (`abs(a - &2 pow n * x) < &1 /\ abs(b - &2 pow n * y) < &1 ==> &2 <= abs(a - b) ==> (x <= y <=> a <= b)`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `&2 pow n * x <= &2 pow n * y` THEN CONJ_TAC THENL [SIMP_TAC[REAL_LE_LMUL_EQ; REAL_POW_LT; REAL_OF_NUM_LT; ARITH]; POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN REAL_ARITH_TAC]);;
let REALCALC_GT = 
prove (`abs(a - &2 pow n * x) < &1 /\ abs(b - &2 pow n * y) < &1 ==> &2 <= abs(a - b) ==> (x > y <=> a > b)`,
ONCE_REWRITE_TAC[CONJ_SYM; REAL_ABS_SUB] THEN REWRITE_TAC[real_gt; REALCALC_LT]);;
let REALCALC_GE = 
prove (`abs(a - &2 pow n * x) < &1 /\ abs(b - &2 pow n * y) < &1 ==> &2 <= abs(a - b) ==> (x >= y <=> a >= b)`,
ONCE_REWRITE_TAC[CONJ_SYM; REAL_ABS_SUB] THEN REWRITE_TAC[real_ge; REALCALC_LE]);;
let REALCALC_EQ = 
prove (`abs(a - &2 pow n * x) < &1 /\ abs(b - &2 pow n * y) < &1 ==> &2 <= abs(a - b) ==> ((x = y) <=> F)`,
ASM_CASES_TAC `x:real = y` THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
let realcalc_rel_conv = let pops = [`(<)`,(</); `(<=)`,(<=/); `(>)`,(>/); `(>=)`,(>=/); `(=):real->real->bool`,(=/)] in let rec find_n rfn1 rfn2 n = if n >/ Int 1000 then failwith "realcalc_rel_conv: too close to discriminate" else if abs_num(raw_eval rfn1 n -/ raw_eval rfn2 n) >=/ Int 4 then n else find_n rfn1 rfn2 (n +/ Int 1) in fun tm -> let lop,r = dest_comb tm in let op,l = dest_comb lop in let pop = try assoc op pops with Failure _ -> failwith "realcalc_rel_conv: unknown operator" in let rfn1,tfn1 = REALCALC_CONV l and rfn2,tfn2 = REALCALC_CONV r in let n = find_n rfn1 rfn2 (Int 1) in pop (raw_eval rfn1 n) (raw_eval rfn2 n);; let REALCALC_REL_CONV = let pths = [`(<)`,REALCALC_LT; `(<=)`,REALCALC_LE; `(>)`,REALCALC_GT; `(>=)`,REALCALC_GE; `(=):real->real->bool`,REALCALC_EQ] in let rec find_n rfn1 rfn2 n = if n >/ Int 1000 then failwith "realcalc_rel_conv: too close to discriminate" else if abs_num(raw_eval rfn1 n -/ raw_eval rfn2 n) >=/ Int 4 then n else find_n rfn1 rfn2 (n +/ Int 1) in fun tm -> let lop,r = dest_comb tm in let op,l = dest_comb lop in let pth = try assoc op pths with Failure _ -> failwith "realcalc_rel_conv: unknown operator" in let rfn1,tfn1 = REALCALC_CONV l and rfn2,tfn2 = REALCALC_CONV r in let n = find_n rfn1 rfn2 (Int 1) in let th1 = thm_eval tfn1 n and th2 = thm_eval tfn2 n in let th3 = MATCH_MP pth (CONJ th1 th2) in let th4 = MP th3 (EQT_ELIM(REAL_INT_REDUCE_CONV(lhand(concl th3)))) in CONV_RULE(RAND_CONV REAL_RAT_REDUCE_CONV) th4;;