1 (* ========================================================================= *)
2 (* Calculation with real numbers (Boehm-style but by inference). *)
3 (* ========================================================================= *)
5 needs "Library/transc.ml";;
7 let REAL_SUB_SUM0 = prove
8 (`!x y m. sum(0,m) x - sum(0,m) y = sum(0,m) (\i. x i - y i)`,
9 CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN
10 GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN
11 ASM_REWRITE_TAC[sum] THEN
14 let REAL_MUL_RSUM0 = prove
15 (`!m c x. c * sum(0,m) x = sum(0,m) (\i. c * x(i))`,
17 ASM_REWRITE_TAC[sum; REAL_MUL_RZERO; REAL_ADD_LDISTRIB]);;
19 let REAL_ABS_LEMMA = prove
20 (`!a b n. (&a pow n) * abs b = abs((&a pow n) * b)`,
21 REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_POW; REAL_ABS_NUM]);;
23 let REAL_ABS_LEMMA1 = prove
24 (`!a b. &a * abs b = abs(&a * b)`,
25 REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_NUM]);;
27 let REAL_ABS_TRIANGLE_LEMMA = prove
28 (`!u x y z. abs(x - y) + abs(z - x) < u ==> abs(z - y) < u`,
30 let REAL_MONO_POW2 = prove
31 (`!m n. m <= n ==> &2 pow m <= &2 pow n`,
32 REPEAT GEN_TAC THEN REWRITE_TAC[LE_EXISTS] THEN
33 DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN
34 SPEC_TAC(`d:num`,`d:num`) THEN INDUCT_TAC THEN
35 REWRITE_TAC[ADD_CLAUSES; real_pow; REAL_LE_REFL] THEN
36 POP_ASSUM MP_TAC THEN MP_TAC(SPEC `m:num` REAL_LT_POW2) THEN
39 let REAL_LE_SUC_POW2 = prove
40 (`!m. &2 pow m + &1 <= &2 pow (SUC m)`,
41 GEN_TAC THEN REWRITE_TAC[real_pow; REAL_MUL_2; REAL_LE_LADD; REAL_LE_POW2]);;
43 let REAL_OPPSIGN_LEMMA = prove
44 (`!x y. (x * y < &0) <=> (x < &0 /\ &0 < y) \/ (&0 < x /\ y < &0)`,
46 REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC (SPEC `x:real` REAL_LT_NEGTOTAL) THEN
47 REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC (SPEC `y:real` REAL_LT_NEGTOTAL) THEN
48 ASM_REWRITE_TAC[REAL_MUL_LZERO; REAL_MUL_RZERO; REAL_LT_REFL] THEN
49 POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
50 DISCH_THEN(fun th -> MP_TAC(MATCH_MP REAL_LT_MUL th) THEN MP_TAC th) THEN
51 REWRITE_TAC[REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_NEG_NEG] THEN
54 let REAL_OPPSIGN = prove
55 (`(&0 < x ==> &0 <= y) /\ (x < &0 ==> y <= &0) <=> &0 <= x * y`,
56 REWRITE_TAC[GSYM REAL_NOT_LT; REAL_OPPSIGN_LEMMA] THEN
59 let REAL_NDIV_LEMMA1a = prove
60 (`!a m n. &2 * abs(&2 pow m * &a - &2 pow (m + n)) <= &2 pow m
62 REPEAT GEN_TAC THEN REWRITE_TAC[REAL_POW_ADD; GSYM REAL_SUB_LDISTRIB] THEN
63 REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_POW; REAL_ABS_NUM] THEN
64 REWRITE_TAC[REAL_OF_NUM_POW] THEN
65 REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
66 (SPECL [`a:num`; `2 EXP n`] LT_CASES) THEN
67 ASM_REWRITE_TAC[] THEN
68 CONV_TAC CONTRAPOS_CONV THEN DISCH_THEN(K ALL_TAC) THEN
69 POP_ASSUM(X_CHOOSE_THEN `d:num` SUBST1_TAC o REWRITE_RULE[LT_EXISTS]) THEN
70 REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN
71 REWRITE_TAC[REAL_ARITH `((a + b) - a = b) /\ (a - (a + b) = --b)`] THEN
72 REWRITE_TAC[REAL_ABS_NEG; REAL_NOT_LE; REAL_ABS_NUM] THEN
73 REWRITE_TAC[ADD1; GSYM REAL_OF_NUM_ADD] THEN
74 REWRITE_TAC[REAL_MUL_2; REAL_ADD_LDISTRIB; REAL_ADD_RDISTRIB] THEN
75 REWRITE_TAC[REAL_MUL_RID; REAL_ADD_ASSOC; REAL_LT_ADDL] THEN
76 MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&(2 EXP m)` THEN
77 REWRITE_TAC[REAL_LT_POW2; GSYM REAL_OF_NUM_POW] THEN
78 ONCE_REWRITE_TAC[AC REAL_ADD_AC `(a + b) + c = b + (a + c)`] THEN
79 REWRITE_TAC[GSYM REAL_MUL_2; REAL_LE_ADDR] THEN
80 MATCH_MP_TAC REAL_LE_MUL THEN REWRITE_TAC[REAL_POS] THEN
81 MATCH_MP_TAC REAL_LE_MUL THEN REWRITE_TAC[REAL_POS] THEN
82 MATCH_MP_TAC REAL_LT_IMP_LE THEN REWRITE_TAC[REAL_LT_POW2]);;
84 let REAL_NDIV_LEMMA1b = prove
85 (`!a m n. ~(&2 * abs(-- (&2 pow m * &a) - &2 pow (m + n)) <= &2 pow m)`,
86 REPEAT GEN_TAC THEN REWRITE_TAC[real_sub; GSYM REAL_NEG_ADD] THEN
87 REWRITE_TAC[REAL_ABS_NEG; REAL_POW_ADD] THEN
88 REWRITE_TAC[REAL_ABS_MUL; GSYM REAL_ADD_LDISTRIB] THEN
89 SUBGOAL_THEN `&0 <= &a + &2 pow n` ASSUME_TAC THENL
90 [MATCH_MP_TAC REAL_LE_ADD THEN REWRITE_TAC[REAL_POS] THEN
91 MATCH_MP_TAC REAL_POW_LE THEN REWRITE_TAC[REAL_POS];
92 REWRITE_TAC[REAL_ABS_POW; REAL_ABS_NUM] THEN
93 ASM_REWRITE_TAC[real_abs; REAL_NOT_LE] THEN
94 MATCH_MP_TAC REAL_LTE_TRANS THEN
95 EXISTS_TAC `(&2 * &2 pow m) * &1` THEN CONJ_TAC THENL
96 [REWRITE_TAC[REAL_MUL_RID; REAL_MUL_2] THEN
97 REWRITE_TAC[REAL_LT_ADDR; REAL_LT_POW2];
98 REWRITE_TAC[REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LE_LMUL THEN
100 [MATCH_MP_TAC REAL_LE_MUL THEN REWRITE_TAC[REAL_POS] THEN
101 MATCH_MP_TAC REAL_POW_LE THEN REWRITE_TAC[REAL_POS];
102 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 pow n` THEN
103 REWRITE_TAC[REAL_LE_POW2; REAL_LE_ADDL; REAL_POS]]]]);;
105 let REAL_NDIV_LEMMA2 = prove
106 (`!a b m n. (?k. (b = &k) \/ (b = --(&k))) /\
107 (abs(a) = &2 pow m) /\
108 &2 * abs(a * b - &2 pow (m + n)) <= abs(a)
109 ==> (a * b = &2 pow (m + n))`,
111 DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
112 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
113 DISJ_CASES_THEN SUBST1_TAC (REAL_ARITH `(a = abs a) \/ (a = --(abs a))`) THEN
114 ASM_REWRITE_TAC[REAL_MUL_LNEG; REAL_MUL_RNEG] THEN
115 REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_POW; REAL_ABS_NUM; REAL_NEG_NEG] THEN
116 REWRITE_TAC[REAL_NDIV_LEMMA1b] THEN
117 DISCH_THEN(SUBST1_TAC o MATCH_MP REAL_NDIV_LEMMA1a) THEN
118 REWRITE_TAC[REAL_POW_ADD]);;
120 let REAL_NDIV_LEMMA3 = prove
121 (`!a b m n. m <= n /\
122 (?k. (b = &k) \/ (b = --(&k))) /\
123 (abs(a) = &2 pow m) /\
124 &2 * abs(a * b - &2 pow n) <= abs(a)
125 ==> (a * b = &2 pow n)`,
127 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
128 POP_ASSUM(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[LE_EXISTS]) THEN
129 REWRITE_TAC[REAL_NDIV_LEMMA2]);;
131 (* ------------------------------------------------------------------------- *)
132 (* Surely there is already an efficient way to do this... *)
133 (* ------------------------------------------------------------------------- *)
135 let log2 = (*** least p >= 0 with x <= 2^p ***)
138 else log2 (quo_num x (Int 2)) (y +/ Int 1) in
139 fun x -> log2 (x -/ Int 1) (Int 0);;
141 (* ------------------------------------------------------------------------- *)
142 (* Theorems justifying the steps. *)
143 (* ------------------------------------------------------------------------- *)
145 let REALCALC_DOWNGRADE = prove
148 abs(a - &2 pow n0 * x) < &1 ==>
149 abs((&2 pow d) * b - a) <= &2 pow d0 ==>
150 abs(b - &2 pow n * x) < &1`,
151 DISCH_THEN(SUBST1_TAC o SYM) THEN
152 DISCH_THEN(SUBST1_TAC o SYM) THEN
153 REPEAT DISCH_TAC THEN
154 MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN EXISTS_TAC `&2 pow (SUC d0)` THEN
156 [MATCH_MP_TAC REAL_POW_LT THEN REAL_ARITH_TAC;
157 REWRITE_TAC[REAL_ABS_LEMMA; REAL_MUL_RID; REAL_SUB_LDISTRIB] THEN
158 MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&2 pow d0 + &2 pow d0` THEN
160 [MATCH_MP_TAC REAL_ABS_TRIANGLE_LEMMA THEN EXISTS_TAC `a:real` THEN
161 MATCH_MP_TAC REAL_LTE_ADD2 THEN ASM_REWRITE_TAC[] THEN
162 MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&1` THEN
163 REWRITE_TAC[REAL_MUL_ASSOC; GSYM REAL_POW_ADD] THEN
164 ONCE_REWRITE_TAC[ADD_SYM] THEN ASM_REWRITE_TAC[] THEN
165 SPEC_TAC(`d0:num`,`d0:num`) THEN INDUCT_TAC THEN
166 REWRITE_TAC[real_pow; REAL_LE_REFL] THEN
167 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&1 + &1` THEN
168 REWRITE_TAC[REAL_MUL_2] THEN CONJ_TAC THENL
170 MATCH_MP_TAC REAL_LE_ADD2 THEN ASM_REWRITE_TAC[]];
171 REWRITE_TAC[real_pow; GSYM REAL_MUL_2; REAL_LE_REFL]]]);;
173 let REALCALC_INT = prove
174 (`abs((&2 pow n) * a - (&2 pow n) * a) < &1`,
175 REWRITE_TAC[REAL_SUB_REFL; REAL_ABS_0; REAL_LT_01]);;
177 let REALCALC_NEG = prove
178 (`abs(a - (&2 pow n) * x) < &1
179 ==> abs(--a - (&2 pow n) * --x) < &1`,
180 REWRITE_TAC[real_sub; GSYM REAL_NEG_ADD] THEN
181 REWRITE_TAC[REAL_ABS_NEG; REAL_MUL_RNEG]);;
183 let REALCALC_ABS = prove
184 (`abs(a - &2 pow n * x) < &1
185 ==> abs(abs(a) - &2 pow n * abs(x)) < &1`,
186 DISCH_TAC THEN REWRITE_TAC[REAL_ABS_LEMMA] THEN
187 MATCH_MP_TAC REAL_LET_TRANS THEN
188 EXISTS_TAC `abs(a - (&2 pow n) * x)` THEN
189 ASM_REWRITE_TAC[REAL_ABS_SUB_ABS]);;
191 let REALCALC_INV_LEMMA = prove
192 (`(?m. (b = &m) \/ (b = --(&m))) /\
193 (?m. (a = &m) \/ (a = --(&m))) /\
194 SUC(n + k) <= (2 * e) /\
195 &2 pow e <= abs(a) /\
196 abs(a - &2 pow k * x) < &1 /\
197 &2 * abs(a * b - &2 pow (n + k)) <= abs(a)
198 ==> abs(b - &2 pow n * inv(x)) < &1`,
199 let lemma1 = REAL_ARITH
200 `!x y z b. &2 * abs(x - y) <= b /\ &2 * abs(y - z) < b
201 ==> &2 * abs(x - z) < &2 * b` in
202 let lemma2 = REAL_ARITH
203 `!x y z. x + &1 <= abs(z) /\ abs(z - y) < &1 ==> x <= abs(y)` in
204 let lemma3 = REAL_ARITH
205 `(abs(x) <= &1 /\ &0 < abs(y) /\ abs(y) < &1) /\
206 (&0 < x ==> &0 <= y) /\ (x < &0 ==> y <= &0)
207 ==> abs(x - y) < &1` in
208 let lemma4 = REAL_ARITH
209 `!a b c. c <= abs(a) + abs(b) /\ abs(a - b) < c ==>
210 (&0 < a ==> &0 <= b) /\ (a < &0 ==> b <= &0)` in
211 DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
212 SUBGOAL_THEN `~(a = &0)` ASSUME_TAC THENL
213 [DISCH_THEN SUBST_ALL_TAC THEN UNDISCH_TAC `&2 pow e <= abs(&0)` THEN
214 REWRITE_TAC[REAL_ABS_0; GSYM REAL_NOT_LT; REAL_LT_POW2]; ALL_TAC] THEN
215 SUBGOAL_THEN `~(x = &0)` ASSUME_TAC THENL
216 [DISCH_THEN SUBST_ALL_TAC THEN
217 UNDISCH_TAC `abs(a - &2 pow k * &0) < &1` THEN
218 REWRITE_TAC[REAL_MUL_RZERO; REAL_SUB_RZERO; REAL_NOT_LT] THEN
219 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 pow e` THEN
220 ASM_REWRITE_TAC[REAL_LE_POW2]; ALL_TAC] THEN
221 SUBGOAL_THEN `(&2 pow e + &1 <= abs(a)) \/ (&2 pow e = abs(a))` MP_TAC THENL
222 [REWRITE_TAC[REAL_OF_NUM_POW] THEN
223 FIRST_ASSUM(CHOOSE_THEN(DISJ_CASES_THEN SUBST_ALL_TAC)) THEN
224 REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_NUM] THEN
225 RULE_ASSUM_TAC(REWRITE_RULE[REAL_ABS_NEG; REAL_ABS_NUM]) THEN
226 REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_LE; REAL_OF_NUM_EQ] THEN
227 REWRITE_TAC[GSYM ADD1; LE_SUC_LT; GSYM LE_LT] THEN
228 ASM_REWRITE_TAC[GSYM REAL_OF_NUM_LE; GSYM REAL_OF_NUM_POW];
229 UNDISCH_TAC `&2 pow e <= abs(a)` THEN DISCH_THEN(K ALL_TAC)] THEN
230 DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL
231 [DISCH_TAC THEN MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN
232 EXISTS_TAC `&2 * abs(a)` THEN CONJ_TAC THENL
233 [MATCH_MP_TAC REAL_LT_MUL THEN
234 ASM_REWRITE_TAC[GSYM REAL_ABS_NZ] THEN REAL_ARITH_TAC;
235 REWRITE_TAC[GSYM REAL_MUL_ASSOC; GSYM REAL_ABS_MUL] THEN
236 REWRITE_TAC[REAL_SUB_LDISTRIB; REAL_MUL_RID] THEN
237 MATCH_MP_TAC lemma1 THEN EXISTS_TAC `&2 pow (n + k)` THEN
238 ASM_REWRITE_TAC[]] THEN
239 GEN_REWRITE_TAC (LAND_CONV o funpow 3 RAND_CONV) [REAL_MUL_SYM] THEN
240 REWRITE_TAC[REAL_POW_ADD; GSYM REAL_MUL_ASSOC] THEN
241 REWRITE_TAC[GSYM REAL_SUB_LDISTRIB; REAL_ABS_MUL] THEN
242 MATCH_MP_TAC REAL_LT_RCANCEL_IMP THEN
243 EXISTS_TAC `abs(x)` THEN ASM_REWRITE_TAC[GSYM REAL_ABS_NZ] THEN
244 REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
245 ONCE_REWRITE_TAC[GSYM REAL_ABS_MUL] THEN
246 MATCH_MP_TAC REAL_LTE_TRANS THEN
247 EXISTS_TAC `&2 * abs(&2 pow n) * &1` THEN CONJ_TAC THENL
248 [MATCH_MP_TAC REAL_LT_LMUL THEN
249 CONJ_TAC THENL [REAL_ARITH_TAC; ALL_TAC] THEN
250 MATCH_MP_TAC REAL_LT_LMUL THEN CONJ_TAC THENL
251 [REWRITE_TAC[GSYM REAL_ABS_NZ; REAL_POW_EQ_0] THEN
252 CONV_TAC(RAND_CONV(LAND_CONV REAL_INT_EQ_CONV)) THEN REWRITE_TAC[];
253 REWRITE_TAC[REAL_SUB_RDISTRIB] THEN
254 ONCE_REWRITE_TAC[REAL_ABS_SUB] THEN
255 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o LAND_CONV) [REAL_MUL_SYM] THEN
256 REWRITE_TAC[REAL_MUL_ASSOC] THEN
257 FIRST_ASSUM(fun th -> REWRITE_TAC[MATCH_MP REAL_MUL_RINV th]) THEN
258 ASM_REWRITE_TAC[REAL_MUL_LID]];
260 MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN EXISTS_TAC `&2 pow k` THEN
261 REWRITE_TAC[REAL_LT_POW2; REAL_MUL_RID; REAL_ABS_LEMMA] THEN
263 [AC REAL_MUL_AC `a * b * c = (a * c) * b`] THEN
264 REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_POW; REAL_ABS_NUM] THEN
265 MATCH_MP_TAC REAL_LE_TRANS THEN
266 EXISTS_TAC `&2 pow e * &2 pow e` THEN CONJ_TAC THENL
268 [AC REAL_MUL_AC `(a * b) * c = c * b * a`] THEN
269 REWRITE_TAC[GSYM REAL_POW_ADD; GSYM(CONJUNCT2 real_pow)] THEN
270 MATCH_MP_TAC REAL_MONO_POW2 THEN ASM_REWRITE_TAC[GSYM MULT_2];
271 MATCH_MP_TAC REAL_LE_MUL2 THEN REPEAT CONJ_TAC THENL
272 [MATCH_MP_TAC REAL_LT_IMP_LE THEN REWRITE_TAC[REAL_LT_POW2];
273 REWRITE_TAC[REAL_ABS_LEMMA] THEN MATCH_MP_TAC lemma2 THEN
274 EXISTS_TAC `a:real` THEN ASM_REWRITE_TAC[];
275 MATCH_MP_TAC REAL_LT_IMP_LE THEN REWRITE_TAC[REAL_LT_POW2];
276 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 pow e + &1` THEN
277 ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC]];
280 DISJ_CASES_TAC (SPECL [`e:num`; `n + k:num`] LET_CASES) THENL
281 [SUBGOAL_THEN `a * b = &2 pow (n + k)` ASSUME_TAC THENL
282 [MATCH_MP_TAC REAL_NDIV_LEMMA3 THEN
283 EXISTS_TAC `e:num` THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
284 MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN EXISTS_TAC `abs(a)` THEN
285 ASM_REWRITE_TAC[GSYM REAL_ABS_NZ; GSYM REAL_ABS_MUL] THEN
286 ASM_REWRITE_TAC[REAL_SUB_LDISTRIB] THEN
287 ONCE_REWRITE_TAC[AC REAL_MUL_AC `a * b * c = b * a * c`] THEN
288 REWRITE_TAC[REAL_POW_ADD; GSYM REAL_SUB_LDISTRIB] THEN
289 REWRITE_TAC[REAL_ABS_MUL; REAL_MUL_RID] THEN
290 MATCH_MP_TAC REAL_LT_RCANCEL_IMP THEN EXISTS_TAC `abs(x)` THEN
291 ASM_REWRITE_TAC[GSYM REAL_ABS_NZ; GSYM REAL_MUL_ASSOC] THEN
292 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM REAL_ABS_MUL] THEN
293 REWRITE_TAC[REAL_SUB_RDISTRIB; GSYM REAL_MUL_ASSOC] THEN
294 REWRITE_TAC[MATCH_MP REAL_MUL_LINV (ASSUME `~(x = &0)`)] THEN
295 ONCE_REWRITE_TAC[REAL_ABS_SUB] THEN
296 MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&2 pow n * &1` THEN
298 [REWRITE_TAC[REAL_ABS_POW; REAL_ABS_NUM] THEN
299 MATCH_MP_TAC REAL_LT_LMUL THEN
300 ASM_REWRITE_TAC[REAL_LT_POW2; REAL_MUL_RID];
301 MATCH_MP_TAC REAL_LE_RCANCEL_IMP THEN EXISTS_TAC `&2 pow (SUC k)` THEN
302 REWRITE_TAC[REAL_MUL_RID; REAL_LT_POW2]] THEN
303 MATCH_MP_TAC REAL_LE_TRANS THEN
304 EXISTS_TAC `&2 pow (2 * e)` THEN CONJ_TAC THENL
305 [REWRITE_TAC[GSYM REAL_POW_ADD; ADD_CLAUSES] THEN
306 MATCH_MP_TAC REAL_MONO_POW2 THEN ASM_REWRITE_TAC[];
307 SUBST1_TAC(SYM(ASSUME `&2 pow e = abs(a)`)) THEN
308 REWRITE_TAC[MULT_2; REAL_POW_ADD; GSYM REAL_MUL_ASSOC] THEN
309 MATCH_MP_TAC REAL_LE_LMUL THEN
310 REWRITE_TAC[MATCH_MP REAL_LT_IMP_LE (SPEC_ALL REAL_LT_POW2)]] THEN
311 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[real_pow] THEN
312 SUBGOAL_THEN `?d. e = SUC d` (CHOOSE_THEN SUBST_ALL_TAC) THENL
313 [UNDISCH_TAC `SUC (n + k) <= (2 * e)` THEN
314 SPEC_TAC(`e:num`,`e:num`) THEN INDUCT_TAC THEN
315 REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES; LE; NOT_SUC] THEN
316 REWRITE_TAC[SUC_INJ; GSYM EXISTS_REFL];
317 REWRITE_TAC[real_pow; GSYM REAL_MUL_ASSOC] THEN
318 MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_POS] THEN
319 MATCH_MP_TAC REAL_LE_TRANS THEN
320 EXISTS_TAC `&2 pow (SUC d) - &1` THEN
321 REWRITE_TAC[REAL_LE_SUB_RADD; REAL_LE_SUB_LADD] THEN
322 REWRITE_TAC[REAL_LE_SUC_POW2] THEN
323 SUBGOAL_THEN `abs(abs a - &2 pow k * abs(x)) < &1` MP_TAC THENL
324 [REWRITE_TAC[REAL_ABS_LEMMA] THEN
325 MATCH_MP_TAC(REAL_LET_IMP REAL_ABS_SUB_ABS) THEN
327 ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC]];
329 SUBGOAL_THEN `abs(b) <= &1 /\ &0 <= a * b` STRIP_ASSUME_TAC THENL
330 [ASM_CASES_TAC `b = &0` THEN
331 ASM_REWRITE_TAC[REAL_ABS_0; REAL_MUL_RZERO; REAL_POS] THEN
332 SUBGOAL_THEN `abs(a) <= abs(a * b)` ASSUME_TAC THENL
333 [GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM REAL_MUL_RID] THEN
334 REWRITE_TAC[REAL_ABS_MUL] THEN MATCH_MP_TAC REAL_LE_LMUL THEN
335 REWRITE_TAC[REAL_ABS_POS] THEN
336 SUBGOAL_THEN `?q. abs(b) = &q` CHOOSE_TAC THENL
337 [UNDISCH_TAC `?m. (b = &m) \/ (b = --(&m))` THEN
338 DISCH_THEN(X_CHOOSE_THEN `p:num` DISJ_CASES_TAC) THEN
339 EXISTS_TAC `p:num` THEN
340 ASM_REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_NUM];
341 UNDISCH_TAC `~(b = &0)` THEN ASM_REWRITE_TAC[REAL_ABS_NZ] THEN
342 REWRITE_TAC[REAL_ABS_NUM; REAL_OF_NUM_LE; REAL_OF_NUM_LT] THEN
343 REWRITE_TAC[SYM(REWRITE_CONV[ARITH_SUC] `SUC 0`)] THEN
344 REWRITE_TAC[LE_SUC_LT]];
346 SUBGOAL_THEN `abs(a * b) <= abs(a) /\ &0 <= a * b` ASSUME_TAC THENL
347 [MP_TAC(SPEC `(n:num) + k` REAL_LT_POW2) THEN
348 UNDISCH_TAC `&2 * abs(a * b - &2 pow (n + k)) <= abs a` THEN
349 UNDISCH_TAC `abs(a) <= abs(a * b)` THEN
350 SUBGOAL_THEN `~(a * b = &0)` MP_TAC THENL
351 [ASM_REWRITE_TAC[REAL_ENTIRE]; ALL_TAC] THEN
352 SUBGOAL_THEN `&2 * &2 pow (n + k) <= abs(a)` MP_TAC THENL
353 [REWRITE_TAC[GSYM(CONJUNCT2 real_pow)] THEN
354 FIRST_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [SYM th]) THEN
355 MATCH_MP_TAC REAL_MONO_POW2 THEN ASM_REWRITE_TAC[LE_SUC_LT];
357 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN
358 EXISTS_TAC `abs(a)` THEN ASM_REWRITE_TAC
359 [GSYM REAL_ABS_NZ; GSYM REAL_ABS_MUL; REAL_MUL_RID]];
361 MATCH_MP_TAC lemma3 THEN CONJ_TAC THENL
362 [ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
363 [ASM_REWRITE_TAC[GSYM REAL_ABS_NZ; REAL_ENTIRE; REAL_INV_EQ_0] THEN
364 MATCH_MP_TAC REAL_LT_IMP_NZ THEN REWRITE_TAC[REAL_LT_POW2];
365 MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN EXISTS_TAC `abs(x)` THEN
366 ASM_REWRITE_TAC[GSYM REAL_ABS_NZ; GSYM REAL_ABS_MUL] THEN
367 ONCE_REWRITE_TAC[AC REAL_MUL_AC `a * b * c = b * c * a`] THEN
368 SUBGOAL_THEN `inv(x) * x = &1` SUBST1_TAC THENL
369 [MATCH_MP_TAC REAL_MUL_LINV THEN ASM_REWRITE_TAC[];
370 REWRITE_TAC[REAL_MUL_RID] THEN
371 MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN EXISTS_TAC `&2 pow k` THEN
372 REWRITE_TAC[REAL_LT_POW2; REAL_ABS_LEMMA] THEN
373 MATCH_MP_TAC REAL_LET_TRANS THEN
374 EXISTS_TAC `&2 pow (SUC(n + k)) - &1` THEN
375 REWRITE_TAC[REAL_LT_SUB_RADD; REAL_LE_SUB_LADD] THEN
376 ONCE_REWRITE_TAC[ADD_SYM] THEN
377 REWRITE_TAC[GSYM REAL_POW_ADD] THEN
378 ONCE_REWRITE_TAC[ADD_SYM] THEN
379 REWRITE_TAC[REAL_LE_SUC_POW2; REAL_ABS_POW; REAL_ABS_NUM] THEN
380 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `&2 pow e` THEN
382 [MATCH_MP_TAC REAL_MONO_POW2 THEN
383 ASM_REWRITE_TAC[LE_SUC_LT];
384 UNDISCH_TAC `abs(a - &2 pow k * x) < &1` THEN
385 ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC]]];
386 SUBGOAL_THEN `&0 <= b * (&2 pow n * inv x)` MP_TAC THENL
387 [MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN
388 EXISTS_TAC `a * a` THEN ASM_REWRITE_TAC[REAL_LT_SQUARE] THEN
389 REWRITE_TAC[REAL_MUL_RZERO] THEN
390 ONCE_REWRITE_TAC[AC REAL_MUL_AC
391 `(a * b) * c * d = (a * c) * (b * d)`] THEN
392 MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[] THEN
393 MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN
394 EXISTS_TAC `x * x` THEN ASM_REWRITE_TAC[REAL_LT_SQUARE] THEN
395 REWRITE_TAC[REAL_MUL_RZERO] THEN
396 ONCE_REWRITE_TAC[AC REAL_MUL_AC
397 `(a * b) * c * d * e = d * (e * a) * c * b`] THEN
398 MATCH_MP_TAC REAL_LE_MUL THEN
399 REWRITE_TAC[MATCH_MP REAL_LT_IMP_LE (SPEC_ALL REAL_LT_POW2)] THEN
400 FIRST_ASSUM(fun th -> GEN_REWRITE_TAC (RAND_CONV o LAND_CONV)
401 [MATCH_MP REAL_MUL_LINV th]) THEN
402 MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN EXISTS_TAC `&2 pow k` THEN
403 REWRITE_TAC[REAL_LT_POW2; REAL_MUL_RZERO; REAL_MUL_LID] THEN
404 ONCE_REWRITE_TAC[AC REAL_MUL_AC `a * b * c = b * (a * c)`] THEN
405 ONCE_REWRITE_TAC[GSYM REAL_OPPSIGN] THEN
406 MATCH_MP_TAC lemma4 THEN EXISTS_TAC `&1` THEN
407 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_TRANS THEN
408 EXISTS_TAC `abs(a)` THEN CONJ_TAC THENL
409 [UNDISCH_TAC `?m. (a = & m) \/ (a = -- (& m))` THEN
410 DISCH_THEN(CHOOSE_THEN(DISJ_CASES_THEN SUBST_ALL_TAC)) THEN
411 ASM_REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_NUM] THEN
412 REWRITE_TAC[REAL_OF_NUM_LE] THEN
413 REWRITE_TAC[SYM(REWRITE_CONV[ARITH_SUC] `SUC 0`)] THEN
414 REWRITE_TAC[LE_SUC_LT] THEN RULE_ASSUM_TAC
415 (REWRITE_RULE[REAL_ARITH `(--x = &0) = (x = &0)`]) THEN
416 UNDISCH_TAC `~(&m = &0)` THEN REWRITE_TAC[REAL_OF_NUM_EQ] THEN
417 CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[NOT_LT; LE];
418 REWRITE_TAC[REAL_LE_ADDR; REAL_ABS_POS]];
419 REWRITE_TAC[REAL_OPPSIGN]]]]]);;
421 let REALCALC_INV = prove
422 (`abs(a - &2 pow k * x) < &1 ==>
423 (?m. (a = &m) \/ (a = --(&m))) ==>
424 (?m. (b = &m) \/ (b = --(&m))) ==>
425 SUC(n + k) <= (2 * e) ==>
426 &2 pow e <= abs(a) ==>
427 &2 * abs(a * b - &2 pow (n + k)) <= abs(a)
428 ==> abs(b - &2 pow n * inv(x)) < &1`,
429 REPEAT DISCH_TAC THEN MATCH_MP_TAC REALCALC_INV_LEMMA THEN
432 let REALCALC_ADD = prove
434 abs(a - &2 pow n' * x) < &1 ==>
435 abs(b - &2 pow n' * y) < &1 ==>
436 abs(&4 * c - (a + b)) <= &2
437 ==> abs(c - &2 pow n * (x + y)) < &1`,
438 DISCH_THEN(SUBST_ALL_TAC o SYM) THEN REPEAT DISCH_TAC THEN
439 MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN
440 EXISTS_TAC `&2 pow 2` THEN
441 CONV_TAC(LAND_CONV REAL_INT_REDUCE_CONV) THEN
442 REWRITE_TAC[REAL_ABS_LEMMA; REAL_SUB_LDISTRIB; REAL_MUL_RID] THEN
443 REWRITE_TAC[REAL_MUL_ASSOC; GSYM REAL_POW_ADD] THEN
444 ONCE_REWRITE_TAC[ADD_SYM] THEN
445 SUBST1_TAC(REAL_INT_REDUCE_CONV `&2 pow 2`) THEN
446 MATCH_MP_TAC REAL_ABS_TRIANGLE_LEMMA THEN
447 EXISTS_TAC `a + b` THEN
448 GEN_REWRITE_TAC RAND_CONV [SYM(REAL_INT_REDUCE_CONV `&2 + &2`)] THEN
449 MATCH_MP_TAC REAL_LTE_ADD2 THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC
450 [REAL_ARITH `(x + y) - a * (u + v) = (x - a * u) + (y - a * v)`] THEN
451 GEN_REWRITE_TAC RAND_CONV [SYM(REAL_INT_REDUCE_CONV `&1 + &1`)] THEN
452 MATCH_MP_TAC(REAL_LET_IMP REAL_ABS_TRIANGLE) THEN
453 MATCH_MP_TAC REAL_LT_ADD2 THEN ASM_REWRITE_TAC[]);;
455 let REALCALC_MUL = prove
456 (`abs(a - &2 pow k * x) < &1 ==>
457 abs(b - &2 pow l * y) < &1 ==>
459 &2 * (abs(a) + abs(b) + &1) <= &2 pow m ==>
460 &2 * abs(&2 pow m * c - a * b) <= &2 pow m
461 ==> abs(c - &2 pow n * (x * y)) < &1`,
462 REPEAT STRIP_TAC THEN
463 MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN EXISTS_TAC `&2 pow m` THEN
464 REWRITE_TAC[REAL_LT_POW2; REAL_ABS_LEMMA; REAL_SUB_LDISTRIB] THEN
465 MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN EXISTS_TAC `&2` THEN
466 CONV_TAC(LAND_CONV (EQT_INTRO o REAL_ARITH)) THEN
467 REWRITE_TAC[REAL_MUL_RID] THEN
468 GEN_REWRITE_TAC RAND_CONV [REAL_MUL_2] THEN
469 MATCH_MP_TAC REAL_LET_TRANS THEN
470 EXISTS_TAC `&2 * abs(&2 pow m * c - a * b) +
471 &2 * abs(a * b - &2 pow m * &2 pow n * x * y)` THEN
472 CONV_TAC(LAND_CONV (EQT_INTRO o REAL_ARITH)) THEN REWRITE_TAC[] THEN
473 MATCH_MP_TAC REAL_LET_ADD2 THEN ASM_REWRITE_TAC[] THEN
474 REWRITE_TAC[REAL_MUL_ASSOC; GSYM REAL_POW_ADD] THEN
475 ONCE_REWRITE_TAC[ADD_SYM] THEN ASM_REWRITE_TAC[] THEN
476 REWRITE_TAC[REAL_POW_ADD] THEN
477 ONCE_REWRITE_TAC[AC REAL_MUL_AC `((a * b) * c) * d = (a * c) * (b * d)`] THEN
478 SUBGOAL_THEN `?d. abs(d) < &1 /\ (&2 pow k * x = a + d)` MP_TAC THENL
479 [EXISTS_TAC `&2 pow k * x - a` THEN
480 UNDISCH_TAC `abs(a - &2 pow k * x) < &1` THEN REAL_ARITH_TAC;
481 DISCH_THEN(CHOOSE_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST1_TAC))] THEN
482 SUBGOAL_THEN `?e. abs(e) < &1 /\ (&2 pow l * y = b + e)` MP_TAC THENL
483 [EXISTS_TAC `&2 pow l * y - b` THEN
484 UNDISCH_TAC `abs(b - &2 pow l * y) < &1` THEN REAL_ARITH_TAC;
485 DISCH_THEN(CHOOSE_THEN(CONJUNCTS_THEN2 ASSUME_TAC SUBST1_TAC))] THEN
486 MATCH_MP_TAC REAL_LTE_TRANS THEN
487 EXISTS_TAC `&2 * (abs(a) * &1 + abs(b) * &1 + &1 * &1)` THEN CONJ_TAC THENL
488 [MATCH_MP_TAC REAL_LT_LMUL THEN
489 CONV_TAC(LAND_CONV (EQT_INTRO o REAL_ARITH)) THEN REWRITE_TAC[] THEN
490 MATCH_MP_TAC REAL_LET_TRANS THEN
491 EXISTS_TAC `abs(a) * abs(e) + abs(b) * abs(d) + abs(d) * abs(e)` THEN
493 [REWRITE_TAC[GSYM REAL_ABS_MUL] THEN REAL_ARITH_TAC;
494 MATCH_MP_TAC REAL_LET_ADD2 THEN CONJ_TAC THENL
495 [MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN
496 MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[];
497 MATCH_MP_TAC REAL_LET_ADD2 THEN CONJ_TAC THENL
498 [MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN
499 MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[];
500 MATCH_MP_TAC REAL_LT_MUL2 THEN ASM_REWRITE_TAC[REAL_ABS_POS]]]];
501 ASM_REWRITE_TAC[REAL_MUL_RID]]);;
503 (* ------------------------------------------------------------------------- *)
505 (* ------------------------------------------------------------------------- *)
507 let REALCALC_SQRT = prove
508 (`abs(a - &2 pow n * x) < &1
510 ==> abs(b pow 2 - &2 pow n * a) <= b
511 ==> abs(b - &2 pow n * sqrt(x)) < &1`,
512 REPEAT STRIP_TAC THEN
513 MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN
514 EXISTS_TAC `abs(b + &2 pow n * sqrt(x))` THEN CONJ_TAC THENL
515 [MATCH_MP_TAC(REAL_ARITH
516 `!z. abs(z) <= b /\ &0 < c ==> &0 < abs(b + c)`) THEN
517 EXISTS_TAC `b pow 2 - &2 pow n * a` THEN ASM_REWRITE_TAC[] THEN
518 ASM_SIMP_TAC[REAL_POW_LT; REAL_OF_NUM_LT; ARITH; REAL_LT_MUL;
519 SQRT_POS_LT; REAL_ARITH `&1 <= x ==> &0 < x`]; ALL_TAC] THEN
520 REWRITE_TAC[GSYM REAL_ABS_MUL; REAL_MUL_RID] THEN
521 ONCE_REWRITE_TAC[REAL_ARITH
522 `(a + b) * (a - b) = a * a - b * b`] THEN
523 MATCH_MP_TAC(REAL_ARITH
524 `!c d. abs(b - c) <= d /\ abs(c - a) < e - d
525 ==> abs(b - a) < e`) THEN
526 MAP_EVERY EXISTS_TAC [`&2 pow n * a`; `b:real`] THEN
527 ASM_REWRITE_TAC[GSYM REAL_POW_2] THEN
528 REWRITE_TAC[REAL_POW_2; GSYM REAL_MUL_ASSOC] THEN
529 REWRITE_TAC[GSYM REAL_SUB_LDISTRIB; REAL_ABS_MUL] THEN
530 MATCH_MP_TAC(REAL_ARITH `a < c ==> a < abs(b + c) - b`) THEN
531 REWRITE_TAC[REAL_ABS_POW; REAL_ABS_NUM] THEN
532 MATCH_MP_TAC REAL_LT_LMUL THEN
533 SIMP_TAC[REAL_POW_LT; REAL_OF_NUM_LT; ARITH] THEN
534 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
535 MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&1` THEN
536 ASM_SIMP_TAC[GSYM REAL_MUL_ASSOC; GSYM POW_2; SQRT_POW_2;
537 REAL_ARITH `&1 <= x ==> &0 <= x`] THEN
538 FIRST_ASSUM(ASSUME_TAC o MATCH_MP(REAL_ARITH `&1 <= x ==> &0 <= x`)) THEN
539 UNDISCH_TAC `&1 <= x` THEN CONV_TAC CONTRAPOS_CONV THEN
540 REWRITE_TAC[REAL_NOT_LE] THEN DISCH_TAC THEN
541 SUBGOAL_THEN `x = sqrt(x) pow 2` SUBST1_TAC THENL
542 [CONV_TAC SYM_CONV THEN ASM_REWRITE_TAC[SQRT_POW2];
543 GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
544 REWRITE_TAC[POW_2] THEN MATCH_MP_TAC REAL_LT_MUL2 THEN
545 ASM_SIMP_TAC[SQRT_POS_LE]]);;
547 (* ------------------------------------------------------------------------- *)
548 (* Lemmas common to all the Taylor series error analyses. *)
549 (* ------------------------------------------------------------------------- *)
551 let STEP_LEMMA1 = prove
553 abs(a - c) <= x /\ abs(b - d) <= y
554 ==> abs(a * b - c * d) <= abs(c) * y + abs(d) * x + x * y`,
556 ABBREV_TAC `u = a - c` THEN ABBREV_TAC `v = b - d` THEN
557 SUBGOAL_THEN `a = c + u` SUBST1_TAC THENL
558 [POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN REAL_ARITH_TAC; ALL_TAC] THEN
559 SUBGOAL_THEN `b = d + v` SUBST1_TAC THENL
560 [POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN REAL_ARITH_TAC; ALL_TAC] THEN
561 STRIP_TAC THEN SUBST1_TAC
562 (REAL_ARITH `(c + u) * (d + v) - c * d = c * v + d * u + u * v`) THEN
563 REPEAT(MATCH_MP_TAC (REAL_LE_IMP REAL_ABS_TRIANGLE) THEN
564 MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC) THEN
565 REWRITE_TAC[REAL_ABS_MUL] THENL
566 [MATCH_MP_TAC REAL_LE_LMUL;
567 MATCH_MP_TAC REAL_LE_LMUL;
568 MATCH_MP_TAC REAL_LE_MUL2] THEN
569 ASM_REWRITE_TAC[REAL_ABS_POS]);;
571 let STEP_LEMMA2 = prove
572 (`!n s t u x y k l a d.
575 abs(s - &2 pow n * x) <= k /\
576 abs(t - &2 pow n * y) <= l /\
577 &2 * abs(u * &2 pow n * d - a * s * t) <= &2 pow n * d
578 ==> abs(u - &2 pow n * (a / d) * (x * y)) <=
579 (a / d) * (abs(x) + k / (&2 pow n)) * l +
580 ((a / d) * k * abs(y) + &1 / &2)`,
581 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
582 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
583 ONCE_REWRITE_TAC[CONJ_ASSOC] THEN DISCH_THEN
584 (CONJUNCTS_THEN2 (ASSUME_TAC o MATCH_MP STEP_LEMMA1) ASSUME_TAC) THEN
585 SUBGOAL_THEN `&0 < &2 * &2 pow n * d` ASSUME_TAC THENL
586 [REPEAT(MATCH_MP_TAC REAL_LT_MUL THEN CONJ_TAC) THEN
587 ASM_REWRITE_TAC[REAL_LT_POW2] THEN REAL_ARITH_TAC; ALL_TAC] THEN
588 MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN
589 EXISTS_TAC `&2 * &2 pow n * d` THEN ASM_REWRITE_TAC[] THEN
590 REWRITE_TAC[real_div; REAL_ADD_LDISTRIB; REAL_ADD_RDISTRIB] THEN
592 `!z. (&2 * &2 pow n * d) * abs(z) = abs((&2 * &2 pow n * d) * z)`
593 (fun th -> REWRITE_TAC[th])
595 [GEN_TAC THEN ONCE_REWRITE_TAC[REAL_ABS_MUL] THEN AP_THM_TAC THEN
596 AP_TERM_TAC THEN UNDISCH_TAC `&0 < &2 * &2 pow n * d` THEN
597 REAL_ARITH_TAC; ALL_TAC] THEN
598 REWRITE_TAC[REAL_SUB_LDISTRIB] THEN
599 (MATCH_MP_TAC o GEN_ALL o REAL_ARITH)
600 `abs(a - b) + abs(b - c) <= d ==> abs(a - c) <= d` THEN
601 EXISTS_TAC `&2 * a * s * t` THEN
602 REWRITE_TAC[GSYM REAL_MUL_ASSOC; REAL_ADD_ASSOC] THEN
603 GEN_REWRITE_TAC RAND_CONV [REAL_ADD_SYM] THEN
604 SUBGOAL_THEN `(inv(&2) * &2 = &1) /\
605 (inv(&2 pow n) * &2 pow n = &1) /\
607 STRIP_ASSUME_TAC THENL
608 [REPEAT CONJ_TAC THEN MATCH_MP_TAC REAL_MUL_LINV THEN
609 REWRITE_TAC[REAL_POW_EQ_0] THEN
610 UNDISCH_TAC `&0 < d` THEN REAL_ARITH_TAC; ALL_TAC] THEN
611 MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL
612 [GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN
613 ASM_REWRITE_TAC[GSYM REAL_MUL_ASSOC; REAL_MUL_RID] THEN
614 REWRITE_TAC[GSYM REAL_SUB_LDISTRIB; GSYM REAL_ABS_LEMMA1] THEN
615 REWRITE_TAC[REAL_MUL_ASSOC] THEN
616 GEN_REWRITE_TAC (LAND_CONV o funpow 2 RAND_CONV o LAND_CONV)
617 [REAL_MUL_SYM] THEN ASM_REWRITE_TAC[GSYM REAL_MUL_ASSOC];
619 REWRITE_TAC(map (GSYM o SPEC `&2`)
620 [REAL_SUB_LDISTRIB; REAL_ADD_LDISTRIB]) THEN
621 REWRITE_TAC[GSYM REAL_ABS_LEMMA1] THEN MATCH_MP_TAC REAL_LE_LMUL THEN
622 CONV_TAC(LAND_CONV (EQT_INTRO o REAL_ARITH)) THEN REWRITE_TAC[] THEN
623 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
625 `a * b * c * d * e * f * g = d * (a * f) * (c * g) * (e * b)`] THEN
626 GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o LAND_CONV)
628 `a * b * c * d * e * f = c * (a * e) * f * (d * b)`] THEN
629 GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o RAND_CONV)
631 `a * b * c * d * e * f * g = c * (e * g) * (f * a) * (d * b)`] THEN
632 GEN_REWRITE_TAC (RAND_CONV o RAND_CONV)
634 `a * b * c * d * e * f = c * (a * f) * e * (d * b)`] THEN
635 GEN_REWRITE_TAC RAND_CONV
636 [AC REAL_ADD_AC `(a + b) + c = a + c + b`] THEN
637 ASM_REWRITE_TAC[REAL_MUL_RID] THEN
638 REWRITE_TAC[GSYM REAL_ADD_LDISTRIB; GSYM REAL_SUB_LDISTRIB] THEN
639 REWRITE_TAC[REAL_ABS_MUL] THEN
640 SUBGOAL_THEN `abs(a) = a` SUBST1_TAC THENL
641 [UNDISCH_TAC `&0 < a` THEN REAL_ARITH_TAC;
642 MATCH_MP_TAC REAL_LE_LMUL THEN ASM_REWRITE_TAC[REAL_ABS_LEMMA] THEN
643 MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[]]]);;
645 (* ------------------------------------------------------------------------- *)
646 (* Now specific instances. *)
647 (* ------------------------------------------------------------------------- *)
651 abs(s - &2 pow n * x) <= &1 /\
652 abs(t - &2 pow n * (x pow i / &(FACT i))) <= k /\
653 &2 * abs(u * &2 pow n * &(SUC i) - s * t) <= &2 pow n * &(SUC i)
654 ==> abs(u - &2 pow n * (x pow (SUC i)) / &(FACT(SUC i))) <=
655 (&2 / &(SUC i)) * k + &1 / &(FACT(SUC i)) + &1 / &2`,
657 MP_TAC(SPECL [`n:num`; `s:real`; `t:real`; `u:real`;
658 `x:real`; `x pow i / &(FACT i)`;
659 `&1`; `k:real`; `&1`; `&(SUC i)`] STEP_LEMMA2) THEN
660 ASM_REWRITE_TAC[REAL_LT_01; REAL_MUL_LID] THEN
661 REWRITE_TAC[REAL_OF_NUM_LT; LT_0] THEN
662 REWRITE_TAC[FACT; real_div; GSYM REAL_OF_NUM_MUL; real_pow] THEN
663 REWRITE_TAC[REAL_MUL_LID; REAL_INV_MUL] THEN
664 MATCH_MP_TAC(REAL_ARITH `(a = b) /\ c <= d ==> a <= c ==> b <= d`) THEN
666 [REWRITE_TAC[REAL_MUL_AC];
667 REWRITE_TAC[REAL_ADD_ASSOC; REAL_LE_RADD] THEN
668 GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o LAND_CONV) [REAL_MUL_SYM] THEN
669 REWRITE_TAC[GSYM REAL_ADD_LDISTRIB; GSYM REAL_MUL_ASSOC] THEN
670 MATCH_MP_TAC REAL_LE_LMUL THEN CONJ_TAC THENL
671 [MATCH_MP_TAC REAL_LE_INV THEN REWRITE_TAC[REAL_OF_NUM_LE; LE_0];
672 MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL
673 [MATCH_MP_TAC REAL_LE_RMUL THEN CONJ_TAC THENL
674 [GEN_REWRITE_TAC RAND_CONV [REAL_ARITH `&2 = &1 + &1`] THEN
675 MATCH_MP_TAC REAL_LE_ADD2 THEN ASM_REWRITE_TAC[] THEN
676 MATCH_MP_TAC REAL_INV_LE_1 THEN REWRITE_TAC[REAL_LE_POW2];
677 MATCH_MP_TAC REAL_LE_TRANS THEN
678 EXISTS_TAC `abs(t - &2 pow n * (x pow i / &(FACT i)))` THEN
679 ASM_REWRITE_TAC[REAL_ABS_POS]];
680 REWRITE_TAC[REAL_ABS_MUL] THEN
681 GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
682 MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[REAL_ABS_POS] THEN
684 [REWRITE_TAC[REAL_ABS_POW] THEN MATCH_MP_TAC REAL_POW_1_LE THEN
685 ASM_REWRITE_TAC[REAL_ABS_POS];
686 MATCH_MP_TAC(REAL_ARITH `&0 <= a ==> abs(a) <= a`) THEN
687 MATCH_MP_TAC REAL_LE_INV THEN
688 REWRITE_TAC[REAL_OF_NUM_LE; LE_0]]]]]);;
692 abs(s - &2 pow n * --(x pow 2)) <= &1 /\
694 x pow (2 * i + 1) / &(FACT (2 * i + 1)))
696 &2 * abs(u * &2 pow n * &(2 * i + 2) * &(2 * i + 3)
698 <= &2 pow n * &(2 * i + 2) * &(2 * i + 3)
699 ==> abs(u - &2 pow n *
700 --(x pow (2 * (SUC i) + 1)) /
701 &(FACT (2 * (SUC i) + 1))) <= &1`,
703 MP_TAC(SPECL [`n:num`; `s:real`; `t:real`; `u:real`;
708 `&(2 * i + 2) * &(2 * i + 3)`]
710 ASM_REWRITE_TAC[REAL_LT_01; REAL_MUL_LID] THEN W(C SUBGOAL_THEN
711 (fun th -> REWRITE_TAC[th]) o funpow 2 (fst o dest_imp) o snd) THENL
712 [REWRITE_TAC(map num_CONV [`3`; `2`; `1`]) THEN
713 REWRITE_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_LT] THEN
714 REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES; LT_0]; ALL_TAC] THEN
715 MATCH_MP_TAC(REAL_ARITH `(a = b) /\ c <= d ==> a <= c ==> b <= d`) THEN
717 [AP_TERM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN SUBGOAL_THEN
718 `2 * (SUC i) + 1 = SUC(SUC(2 * i + 1))`
720 [GEN_REWRITE_TAC I [GSYM REAL_OF_NUM_EQ] THEN
721 REWRITE_TAC[ADD1; GSYM REAL_OF_NUM_MUL; GSYM REAL_OF_NUM_ADD] THEN
723 REWRITE_TAC[real_pow; FACT] THEN
724 REWRITE_TAC[ADD1; GSYM ADD_ASSOC] THEN
725 REWRITE_TAC[ARITH] THEN
726 REWRITE_TAC[real_div; REAL_INV_MUL; GSYM REAL_OF_NUM_MUL;
727 GSYM REAL_OF_NUM_ADD] THEN
728 REWRITE_TAC[REAL_MUL_LID; REAL_MUL_RNEG; REAL_MUL_LNEG] THEN
729 REWRITE_TAC[REAL_POW_2; REAL_MUL_AC]];
730 GEN_REWRITE_TAC RAND_CONV
731 [SYM(REAL_RAT_REDUCE_CONV `&1 / &3 + &1 / &6 + &1 / &2`)] THEN
732 REWRITE_TAC[REAL_ADD_ASSOC; REAL_LE_RADD] THEN
733 SUBGOAL_THEN `&1 / (&(2 * i + 2) * &(2 * i + 3))
734 <= &1 / &6` ASSUME_TAC THENL
735 [REWRITE_TAC[real_div; REAL_MUL_LID] THEN
736 MATCH_MP_TAC REAL_LE_INV2 THEN
737 CONV_TAC(LAND_CONV (EQT_INTRO o REAL_ARITH)) THEN REWRITE_TAC[] THEN
738 REWRITE_TAC[REAL_ARITH `&6 = &2 * &3`] THEN
739 REWRITE_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_LE] THEN
740 MATCH_MP_TAC LE_MULT2 THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
741 REWRITE_TAC[LE_ADD]; ALL_TAC] THEN
742 REWRITE_TAC[SYM(REAL_RAT_REDUCE_CONV `&1 / &6 * &2`)] THEN
743 GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM REAL_MUL_RID] THEN
744 REWRITE_TAC[GSYM REAL_ADD_LDISTRIB] THEN
745 MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_REWRITE_TAC[] THEN
746 REPEAT CONJ_TAC THENL
747 [REWRITE_TAC[real_div; REAL_MUL_LID; REAL_LE_INV_EQ] THEN
748 REWRITE_TAC[REAL_OF_NUM_MUL; REAL_POS];
749 MATCH_MP_TAC REAL_LE_ADD THEN
750 REWRITE_TAC[REAL_MUL_RID; REAL_ABS_POS] THEN
751 MATCH_MP_TAC REAL_LE_ADD THEN
752 REWRITE_TAC[real_div; REAL_MUL_LID; REAL_LE_INV_EQ; REAL_ABS_POS] THEN
753 MATCH_MP_TAC REAL_LT_IMP_LE THEN REWRITE_TAC[REAL_LT_POW2];
754 REWRITE_TAC[REAL_MUL_RID]] THEN
755 MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL
756 [GEN_REWRITE_TAC RAND_CONV [REAL_ARITH `&2 = &1 + &1`] THEN
757 MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL
758 [REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_POW] THEN
759 MATCH_MP_TAC REAL_POW_1_LE THEN ASM_REWRITE_TAC[REAL_ABS_POS];
760 REWRITE_TAC[real_div; REAL_MUL_LID] THEN
761 MATCH_MP_TAC REAL_INV_LE_1 THEN REWRITE_TAC[REAL_LE_POW2]];
762 REWRITE_TAC[real_div; REAL_ABS_MUL] THEN
763 GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN
764 MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[REAL_ABS_POS] THEN
766 [REWRITE_TAC[REAL_ABS_POW] THEN MATCH_MP_TAC REAL_POW_1_LE THEN
767 ASM_REWRITE_TAC[REAL_ABS_POS];
768 REWRITE_TAC[REAL_ABS_INV; REAL_ABS_NUM] THEN
769 MATCH_MP_TAC REAL_INV_LE_1 THEN
770 REWRITE_TAC[REAL_OF_NUM_LE; FACT_LE]]]]);;
774 abs(s - &2 pow n * --(x pow 2)) <= &1 /\
776 x pow (2 * i) / &(FACT (2 * i)))
778 &2 * abs(u * &2 pow n * &(2 * i + 1) * &(2 * i + 2)
780 <= &2 pow n * &(2 * i + 1) * &(2 * i + 2)
781 ==> abs(u - &2 pow n *
782 --(x pow (2 * (SUC i))) /
783 &(FACT (2 * (SUC i))))
784 <= (&2 * inv(&(2 * i + 1) * &(2 * i + 2))) * k
785 + inv(&(FACT(2 * i + 2))) + &1 / &2`,
787 MP_TAC(SPECL [`n:num`; `s:real`; `t:real`; `u:real`;
791 `&1`; `k:real`; `&1`;
792 `&(2 * i + 1) * &(2 * i + 2)`]
794 ASM_REWRITE_TAC[REAL_LT_01; REAL_MUL_LID] THEN W(C SUBGOAL_THEN
795 (fun th -> REWRITE_TAC[th]) o funpow 2 (fst o dest_imp) o snd) THENL
796 [REWRITE_TAC(map num_CONV [`3`; `2`; `1`]) THEN
797 REWRITE_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_LT] THEN
798 REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES; LT_0]; ALL_TAC] THEN
799 MATCH_MP_TAC(REAL_ARITH `(a = b) /\ c <= d ==> a <= c ==> b <= d`) THEN
801 [AP_TERM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN SUBGOAL_THEN
802 `2 * (SUC i) = SUC(SUC(2 * i))`
804 [GEN_REWRITE_TAC I [GSYM REAL_OF_NUM_EQ] THEN
805 REWRITE_TAC[ADD1; GSYM REAL_OF_NUM_MUL; GSYM REAL_OF_NUM_ADD] THEN
807 REWRITE_TAC[real_pow; FACT] THEN
808 REWRITE_TAC[ADD1; GSYM ADD_ASSOC] THEN
809 REWRITE_TAC[ARITH] THEN
810 REWRITE_TAC[real_div; REAL_INV_MUL; GSYM REAL_OF_NUM_MUL;
811 GSYM REAL_OF_NUM_ADD] THEN
812 REWRITE_TAC[REAL_MUL_LID; REAL_MUL_RNEG; REAL_MUL_LNEG] THEN
813 REWRITE_TAC[REAL_POW_2; REAL_MUL_AC]];
815 REWRITE_TAC[REAL_ADD_ASSOC; REAL_LE_RADD] THEN
816 MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL
817 [REWRITE_TAC[REAL_MUL_ASSOC] THEN
818 MATCH_MP_TAC REAL_LE_RMUL THEN CONJ_TAC THENL
819 [REWRITE_TAC[real_div; REAL_MUL_LID] THEN
820 GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_SYM] THEN
821 MATCH_MP_TAC REAL_LE_LMUL THEN CONJ_TAC THENL
822 [MATCH_MP_TAC REAL_LE_INV THEN
823 REWRITE_TAC[REAL_OF_NUM_MUL; REAL_POS];
824 GEN_REWRITE_TAC RAND_CONV [REAL_ARITH `&2 = &1 + &1`] THEN
825 MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL
826 [REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_POW] THEN
827 MATCH_MP_TAC REAL_POW_1_LE THEN
828 ASM_REWRITE_TAC[REAL_ABS_POS];
829 MATCH_MP_TAC REAL_INV_LE_1 THEN REWRITE_TAC[REAL_LE_POW2]]];
830 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC
831 `abs(t - &2 pow n * x pow (2 * i) / &(FACT (2 * i)))` THEN
832 ASM_REWRITE_TAC[REAL_ABS_POS]];
833 REWRITE_TAC[real_div; REAL_MUL_LID; REAL_INV_MUL; REAL_ABS_MUL] THEN
834 GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN
835 ONCE_REWRITE_TAC[AC REAL_MUL_AC
836 `(a * b) * c * d = (d * a * b) * c`] THEN
837 MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[REAL_ABS_POS] THEN
838 REPEAT CONJ_TAC THENL
839 [REPEAT(MATCH_MP_TAC REAL_LE_MUL THEN CONJ_TAC) THEN
840 REWRITE_TAC[REAL_POS; REAL_ABS_POS; REAL_LE_INV_EQ];
841 REWRITE_TAC[REAL_ABS_INV] THEN
842 REWRITE_TAC[GSYM REAL_INV_MUL; REAL_ABS_NUM] THEN
843 MATCH_MP_TAC REAL_EQ_IMP_LE THEN AP_TERM_TAC THEN
844 REWRITE_TAC[num_CONV `2`; num_CONV `1`; ADD_CLAUSES] THEN
845 REWRITE_TAC[SYM(num_CONV `2`); SYM(num_CONV `1`)] THEN
846 REWRITE_TAC[FACT; REAL_OF_NUM_MUL] THEN
847 REWRITE_TAC[MULT_AC];
848 REWRITE_TAC[REAL_ABS_POW] THEN MATCH_MP_TAC REAL_POW_1_LE THEN
849 ASM_REWRITE_TAC[REAL_ABS_POS]]]]);;
854 abs(s - &2 pow n * --x) <= &1 /\
855 abs(t - &2 pow n * -- ((--x) pow (SUC i) / &(SUC i))) <= &3 /\
856 &2 * abs(u * &2 pow n * &(SUC(SUC i)) - &(SUC i) * s * t)
857 <= &2 pow n * &(SUC(SUC i))
858 ==> abs(u - &2 pow n * -- ((--x) pow (SUC(SUC i)) / &(SUC(SUC i)))) <= &3`,
860 MP_TAC(SPECL [`n:num`; `s:real`; `t:real`; `u:real`;
862 `-- (--x pow (SUC i) / &(SUC i))`;
867 ASM_REWRITE_TAC[REAL_LT_01; REAL_MUL_LID] THEN
868 REWRITE_TAC[REAL_OF_NUM_LT; LT_0] THEN
869 MATCH_MP_TAC(REAL_ARITH `(a = b) /\ c <= d ==> a <= c ==> b <= d`) THEN
871 [AP_TERM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
872 REWRITE_TAC[real_pow; real_div; REAL_INV_MUL] THEN
873 REWRITE_TAC[REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_NEG_NEG] THEN
874 AP_TERM_TAC THEN REWRITE_TAC[REAL_MUL_ASSOC] THEN
875 GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] THEN
876 SUBGOAL_THEN `inv(&(SUC i)) * &(SUC i) = &1` ASSUME_TAC THENL
877 [MATCH_MP_TAC REAL_MUL_LINV THEN
878 REWRITE_TAC[REAL_OF_NUM_EQ; NOT_SUC];
879 ASM_REWRITE_TAC[REAL_MUL_ASSOC; REAL_MUL_LID] THEN
880 REWRITE_TAC[REAL_MUL_AC]];
881 GEN_REWRITE_TAC RAND_CONV [SYM(REAL_RAT_REDUCE_CONV
882 `(&1 / &2 + &1 / &4) * &3 + &1 / &4 + &1 / &2`)] THEN
883 REWRITE_TAC[REAL_ADD_ASSOC; REAL_LE_RADD] THEN
884 MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL
885 [REWRITE_TAC[REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LE_RMUL THEN
886 CONV_TAC(RAND_CONV (EQT_INTRO o REAL_ARITH)) THEN REWRITE_TAC[] THEN
887 GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
888 MATCH_MP_TAC REAL_LE_MUL2 THEN REPEAT CONJ_TAC THENL
889 [MATCH_MP_TAC REAL_LE_RCANCEL_IMP THEN
890 EXISTS_TAC `&(SUC(SUC i))` THEN
891 REWRITE_TAC[REAL_MUL_LZERO; REAL_OF_NUM_LT; LT_0] THEN
892 REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC] THEN
893 MATCH_MP_TAC REAL_LE_MUL THEN REWRITE_TAC[REAL_POS] THEN
894 MATCH_MP_TAC(REAL_ARITH `(x = &1) ==> &0 <= x`) THEN
895 MATCH_MP_TAC REAL_MUL_LINV THEN
896 REWRITE_TAC[REAL_OF_NUM_EQ; NOT_SUC];
897 MATCH_MP_TAC REAL_LE_RCANCEL_IMP THEN
898 EXISTS_TAC `&(SUC(SUC i))` THEN
899 REWRITE_TAC[REAL_OF_NUM_LT; LT_0] THEN
900 REWRITE_TAC[real_div; REAL_MUL_LID; GSYM REAL_MUL_ASSOC] THEN
901 GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN
902 MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[REAL_POS] THEN
903 REWRITE_TAC[REAL_OF_NUM_LE; LE] THEN
904 MATCH_MP_TAC(REAL_ARITH `(x = &1) ==> &0 <= x /\ x <= &1`) THEN
905 MATCH_MP_TAC REAL_MUL_LINV THEN
906 REWRITE_TAC[REAL_OF_NUM_EQ; NOT_SUC];
907 MATCH_MP_TAC REAL_LE_ADD THEN REWRITE_TAC[REAL_ABS_POS] THEN
908 REWRITE_TAC[real_div; REAL_MUL_LID; REAL_LE_INV_EQ] THEN
909 MATCH_MP_TAC REAL_LT_IMP_LE THEN REWRITE_TAC[REAL_LT_POW2];
910 MATCH_MP_TAC REAL_LE_ADD2 THEN ASM_REWRITE_TAC[REAL_ABS_NEG] THEN
911 REWRITE_TAC[real_div; REAL_MUL_LID] THEN
912 MATCH_MP_TAC REAL_LE_INV2 THEN
913 CONV_TAC(LAND_CONV (EQT_INTRO o REAL_ARITH)) THEN REWRITE_TAC[] THEN
914 SUBST1_TAC(SYM(REAL_INT_REDUCE_CONV `&2 pow 2`)) THEN
915 MATCH_MP_TAC REAL_MONO_POW2 THEN ASM_REWRITE_TAC[]];
916 REWRITE_TAC[real_div; REAL_ABS_MUL; REAL_ABS_NEG; REAL_ABS_INV] THEN
917 REWRITE_TAC[REAL_ABS_POW; REAL_ABS_NEG; REAL_MUL_LID] THEN
918 REWRITE_TAC[REAL_ABS_NUM] THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
919 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[REAL_MUL_ASSOC] THEN
920 SUBGOAL_THEN `inv(&(SUC i)) * &(SUC i) = &1` ASSUME_TAC THENL
921 [MATCH_MP_TAC REAL_MUL_LINV THEN REWRITE_TAC[REAL_OF_NUM_EQ; NOT_SUC];
922 GEN_REWRITE_TAC RAND_CONV
923 [EQT_ELIM(REAL_RAT_REDUCE_CONV `inv(&4) = inv(&2) * inv(&2)`)] THEN
924 ASM_REWRITE_TAC[REAL_MUL_RID; GSYM REAL_MUL_ASSOC] THEN
925 MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC
926 [REAL_POS; REAL_ABS_POS; REAL_LE_INV_EQ; GSYM REAL_ABS_POW] THEN
928 [MATCH_MP_TAC REAL_LE_INV2 THEN REWRITE_TAC[REAL_POS] THEN
929 REWRITE_TAC[ADD1; GSYM REAL_OF_NUM_ADD] THEN
930 MP_TAC(SPEC `i:num` REAL_POS) THEN REAL_ARITH_TAC;
931 REWRITE_TAC[real_pow; REAL_ABS_POW] THEN
932 GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN
933 MATCH_MP_TAC REAL_LE_MUL2 THEN
934 REWRITE_TAC[REAL_LE_INV_EQ; REAL_ABS_POS] THEN
935 REPEAT CONJ_TAC THENL
936 [CONV_TAC(RAND_CONV REAL_RAT_REDUCE_CONV) THEN ASM_REWRITE_TAC[];
937 MATCH_MP_TAC REAL_POW_LE THEN REWRITE_TAC[REAL_ABS_POS];
938 MATCH_MP_TAC REAL_POW_1_LE THEN REWRITE_TAC[REAL_ABS_POS] THEN
939 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&1 / &2` THEN
940 ASM_REWRITE_TAC[] THEN CONV_TAC REAL_RAT_REDUCE_CONV]]]]]);;
942 (* ------------------------------------------------------------------------- *)
943 (* Expand the "!k. SUC k < r ==> P k" term for given numeral r. *)
944 (* ------------------------------------------------------------------------- *)
946 let EXPAND_RANGE_CONV =
948 (`(!k. SUC k < 0 ==> P k) <=> T`,
951 (`(!k. k < (SUC m) ==> P k) <=>
952 (!k. k < m ==> P k) /\ P m`,
953 REWRITE_TAC[LT] THEN MESON_TAC[])
955 (`(!k. k < 0 ==> P k) <=> T`,
957 let triv_conv = GEN_REWRITE_CONV I [pth0]
958 and trivial_conv = GEN_REWRITE_CONV I [pth2]
959 and nontrivial_conv = GEN_REWRITE_CONV I [pth1] in
962 and n_tm = `n:num` in
963 let rec expand_conv tm =
966 let mth = num_CONV(rand(lhand(body(rand tm)))) in
967 let th1 = BINDER_CONV(LAND_CONV(RAND_CONV(K mth))) tm in
968 let th2 = TRANS th1 (nontrivial_conv (rand(concl th1))) in
969 let th3 = COMB2_CONV (RAND_CONV expand_conv) (SUBS_CONV[SYM mth])
974 (BINDER_CONV (LAND_CONV
975 ((RAND_CONV num_CONV) THENC REWR_CONV LT_SUC)) THENC
979 (* ------------------------------------------------------------------------- *)
980 (* Lemmas leading to iterative versions. *)
981 (* ------------------------------------------------------------------------- *)
983 let STEP_EXP_THM = prove
985 abs(s - &2 pow n * x) < &1 /\
986 abs(t(i) - &2 pow n * (x pow i / &(FACT i))) <= k ==>
987 &2 * abs(t(SUC i) * &2 pow n * &(SUC i) - s * t(i)) <= &2 pow n * &(SUC i)
988 ==> abs(t(SUC i) - &2 pow n * (x pow (SUC i)) / &(FACT(SUC i))) <=
989 (&2 / &(SUC i)) * k + &1 / &(FACT(SUC i)) + &1 / &2`,
990 REPEAT STRIP_TAC THEN MATCH_MP_TAC(GEN_ALL STEP_EXP) THEN
991 MAP_EVERY EXISTS_TAC [`s:real`; `t(i:num):real`] THEN
992 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN
995 let STEP_EXP_RULE th =
996 let th1 = MATCH_MP STEP_EXP_THM th in
997 let th2 = UNDISCH(PURE_REWRITE_RULE[ARITH_SUC] th1) in
998 let th3 = CONV_RULE(RAND_CONV(ONCE_DEPTH_CONV NUM_FACT_CONV)) th2 in
999 let th4 = CONV_RULE(RAND_CONV REAL_RAT_REDUCE_CONV) th3 in
1000 let th5 = ASSUME(find is_conj (hyp th)) in
1001 let th6a,th6b = (I F_F CONJUNCT1) (CONJ_PAIR th5) in
1002 CONJ th6a (CONJ th6b th4);;
1004 let STEP_EXP_0 = (UNDISCH o prove)
1006 abs(s - &2 pow n * x) < &1 /\
1007 (t(0) = &2 pow n) ==>
1009 abs(s - &2 pow n * x) < &1 /\
1010 abs(t(0) - &2 pow n * (x pow 0 / &(FACT 0))) <= &0`,
1011 STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
1012 REWRITE_TAC[real_pow; FACT; real_div; REAL_INV_1; REAL_MUL_RID] THEN
1013 REWRITE_TAC[REAL_SUB_REFL; REAL_ABS_0; REAL_LE_REFL]);;
1015 let STEP_EXP_1 = STEP_EXP_RULE STEP_EXP_0;; (* e(1) = 3/2 *)
1016 let STEP_EXP_2 = STEP_EXP_RULE STEP_EXP_1;; (* e(2) = 5/2 *)
1017 let STEP_EXP_3 = STEP_EXP_RULE STEP_EXP_2;; (* e(3) = 7/3 *)
1018 let STEP_EXP_4 = STEP_EXP_RULE STEP_EXP_3;; (* e(4) = 41/24 *)
1019 let STEP_EXP_5 = STEP_EXP_RULE STEP_EXP_4;; (* e(5) = 143/120 *)
1021 let STEP_EXP_4_PLUS = prove
1024 abs(s - &2 pow n * x) < &1 /\
1025 (t(0) = &2 pow n) /\
1026 (!k. SUC k < SUC m ==>
1027 &2 * abs(t(SUC k) * &2 pow n * &(SUC k) - s * t(k))
1028 <= &2 pow n * &(SUC k))
1029 ==> abs(t m - &2 pow n * x pow m / &(FACT m)) <= &2`,
1031 (`(!k. k < (SUC m) ==> P k) <=>
1032 (!k. k < m ==> P k) /\ P m`,
1033 REWRITE_TAC[LT] THEN MESON_TAC[]) in
1034 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1035 POP_ASSUM(X_CHOOSE_THEN `d:num` SUBST1_TAC o REWRITE_RULE[LE_EXISTS]) THEN
1036 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1037 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1038 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1039 REWRITE_TAC[LT_SUC] THEN SPEC_TAC(`d:num`,`d:num`) THEN
1041 [REWRITE_TAC[ADD_CLAUSES] THEN
1042 SUBST1_TAC(TOP_DEPTH_CONV num_CONV `4`) THEN
1043 REWRITE_TAC[lemma] THEN REWRITE_TAC[ARITH_SUC] THEN
1044 REWRITE_TAC[LT] THEN STRIP_TAC THEN
1045 MP_TAC (DISCH_ALL STEP_EXP_4) THEN ASM_REWRITE_TAC[] THEN
1046 MATCH_MP_TAC(REAL_ARITH `b <= c ==> a <= b ==> a <= c`) THEN
1047 CONV_TAC REAL_RAT_REDUCE_CONV;
1048 REWRITE_TAC[ADD_CLAUSES; lemma] THEN STRIP_TAC THEN
1049 MATCH_MP_TAC REAL_LE_TRANS THEN
1050 EXISTS_TAC `&2 / &(SUC(4 + d)) * &2 +
1051 &1 / &(FACT(SUC(4 + d))) + &1 / &2` THEN
1053 [MATCH_MP_TAC(GEN_ALL STEP_EXP) THEN ASM_REWRITE_TAC[] THEN
1054 EXISTS_TAC `s:real` THEN EXISTS_TAC `t(4 + d):real` THEN
1055 ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
1056 [MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[];
1057 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]];
1058 GEN_REWRITE_TAC RAND_CONV
1059 [SYM(REAL_RAT_REDUCE_CONV `&3 / &2 + &1 / &2`)] THEN
1060 REWRITE_TAC[REAL_LE_RADD; REAL_ADD_ASSOC] THEN
1061 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&4 / &5 + &1 / &120` THEN
1062 CONV_TAC(RAND_CONV REAL_RAT_REDUCE_CONV) THEN REWRITE_TAC[] THEN
1063 MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL
1064 [ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
1065 REWRITE_TAC[real_div; REAL_MUL_ASSOC] THEN
1066 REWRITE_TAC[REAL_ARITH `&2 * &2 = &4`] THEN
1067 MATCH_MP_TAC REAL_LE_LMUL THEN
1068 REWRITE_TAC[REAL_ARITH `&0 <= &4`] THEN
1069 MATCH_MP_TAC REAL_LE_INV2 THEN
1070 REWRITE_TAC[ADD1; GSYM REAL_OF_NUM_ADD] THEN
1071 MP_TAC(SPEC `d':num` REAL_POS) THEN REAL_ARITH_TAC;
1072 REWRITE_TAC[real_div; REAL_MUL_LID] THEN
1073 MATCH_MP_TAC REAL_LE_INV2 THEN
1074 CONV_TAC(LAND_CONV (EQT_INTRO o REAL_ARITH)) THEN REWRITE_TAC[] THEN
1075 SUBST1_TAC(SYM(NUM_FACT_CONV `FACT 5`)) THEN
1076 REWRITE_TAC[REAL_OF_NUM_LE] THEN MATCH_MP_TAC FACT_MONO THEN
1077 REWRITE_TAC[num_CONV `5`; LE_SUC; LE_ADD]]]]);;
1079 let STEPS_EXP_0 = prove
1081 abs(s - &2 pow n * x) < &1 /\
1082 (t(0) = &2 pow n) /\
1084 &2 * abs(t(SUC k) * &2 pow n * &(SUC k) - s * t(k))
1085 <= &2 pow n * &(SUC k))
1086 ==> abs(sum(0,0) t -
1087 &2 pow n * sum(0,0) (\i. x pow i / &(FACT i))) <= &2 * &0`,
1088 STRIP_TAC THEN ASM_REWRITE_TAC[sum] THEN
1089 REWRITE_TAC[REAL_MUL_RZERO; REAL_ABS_0; REAL_SUB_REFL; REAL_LE_REFL]);;
1091 let STEPS_EXP_1 = prove
1093 abs(s - &2 pow n * x) < &1 /\
1094 (t(0) = &2 pow n) /\
1096 &2 * abs(t(SUC k) * &2 pow n * &(SUC k) - s * t(k))
1097 <= &2 pow n * &(SUC k))
1098 ==> abs(sum(0,1) t - &2 pow n * sum(0,1)(\i. x pow i / &(FACT i)))
1100 CONV_TAC(ONCE_DEPTH_CONV EXPAND_RANGE_CONV) THEN REWRITE_TAC[] THEN
1101 STRIP_TAC THEN CONV_TAC(ONCE_DEPTH_CONV REAL_SUM_CONV) THEN
1102 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&0` THEN
1103 CONV_TAC(RAND_CONV REAL_RAT_REDUCE_CONV) THEN REWRITE_TAC[] THEN
1104 MP_TAC (DISCH_ALL STEP_EXP_0) THEN ASM_REWRITE_TAC[]);;
1106 let STEPS_EXP_2 = prove
1108 abs(s - &2 pow n * x) < &1 /\
1109 (t(0) = &2 pow n) /\
1111 &2 * abs(t(SUC k) * &2 pow n * &(SUC k) - s * t(k))
1112 <= &2 pow n * &(SUC k))
1113 ==> abs(sum(0,2) t - &2 pow n * sum(0,2) (\i. x pow i / &(FACT i)))
1115 CONV_TAC(ONCE_DEPTH_CONV EXPAND_RANGE_CONV) THEN REWRITE_TAC[] THEN
1116 STRIP_TAC THEN CONV_TAC(ONCE_DEPTH_CONV REAL_SUM_CONV) THEN
1117 REWRITE_TAC[REAL_ADD_LDISTRIB] THEN
1118 REWRITE_TAC[REAL_ARITH `(a + b) - (c + d) = (a - c) + (b - d)`] THEN
1119 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&0 + &3 / &2` THEN
1120 CONV_TAC(RAND_CONV REAL_RAT_REDUCE_CONV) THEN REWRITE_TAC[] THEN
1121 MATCH_MP_TAC(REAL_LE_IMP(REAL_ARITH `abs(a + b) <= abs(a) + abs(b)`)) THEN
1122 MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL
1123 [MP_TAC (DISCH_ALL STEP_EXP_0) THEN ASM_REWRITE_TAC[];
1124 MP_TAC (DISCH_ALL STEP_EXP_1) THEN
1125 ASM_REWRITE_TAC[ADD_CLAUSES]]);;
1127 let STEPS_EXP_3 = prove
1129 abs(s - &2 pow n * x) < &1 /\
1130 (t(0) = &2 pow n) /\
1132 &2 * abs(t(SUC k) * &2 pow n * &(SUC k) - s * t(k))
1133 <= &2 pow n * &(SUC k))
1134 ==> abs(sum(0,3) t - &2 pow n * sum(0,3) (\i. x pow i / &(FACT i)))
1136 CONV_TAC(ONCE_DEPTH_CONV EXPAND_RANGE_CONV) THEN REWRITE_TAC[] THEN
1137 STRIP_TAC THEN CONV_TAC(ONCE_DEPTH_CONV REAL_SUM_CONV) THEN
1138 REWRITE_TAC[REAL_ADD_LDISTRIB] THEN
1139 REWRITE_TAC[REAL_ARITH `(a + b) - (c + d) = (a - c) + (b - d)`] THEN
1140 REWRITE_TAC[GSYM REAL_ADD_ASSOC] THEN
1141 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&0 + &3 / &2 + &5 / &2` THEN
1142 CONV_TAC(RAND_CONV REAL_RAT_REDUCE_CONV) THEN REWRITE_TAC[] THEN
1144 (MATCH_MP_TAC(REAL_LE_IMP(REAL_ARITH `abs(a + b) <= abs(a) + abs(b)`)) THEN
1145 MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC)
1147 [MP_TAC (DISCH_ALL STEP_EXP_0) THEN ASM_REWRITE_TAC[];
1148 MP_TAC (DISCH_ALL STEP_EXP_1) THEN ASM_REWRITE_TAC[ADD_CLAUSES];
1149 MP_TAC (DISCH_ALL STEP_EXP_2) THEN ASM_REWRITE_TAC[ADD_CLAUSES]]);;
1151 let STEPS_EXP_4 = prove
1153 abs(s - &2 pow n * x) < &1 /\
1154 (t(0) = &2 pow n) /\
1156 &2 * abs(t(SUC k) * &2 pow n * &(SUC k) - s * t(k))
1157 <= &2 pow n * &(SUC k))
1158 ==> abs(sum(0,4) t - &2 pow n * sum(0,4) (\i. x pow i / &(FACT i)))
1160 CONV_TAC(ONCE_DEPTH_CONV EXPAND_RANGE_CONV) THEN REWRITE_TAC[] THEN
1161 STRIP_TAC THEN CONV_TAC(ONCE_DEPTH_CONV REAL_SUM_CONV) THEN
1162 REWRITE_TAC[REAL_ADD_LDISTRIB] THEN
1163 REWRITE_TAC[REAL_ARITH `(a + b) - (c + d) = (a - c) + (b - d)`] THEN
1164 REWRITE_TAC[GSYM REAL_ADD_ASSOC] THEN
1165 MATCH_MP_TAC REAL_LE_TRANS THEN
1166 EXISTS_TAC `&0 + &3 / &2 + &5 / &2 + &7 / &3` THEN
1167 CONV_TAC(RAND_CONV REAL_RAT_REDUCE_CONV) THEN REWRITE_TAC[] THEN
1169 (MATCH_MP_TAC(REAL_LE_IMP(REAL_ARITH `abs(a + b) <= abs(a) + abs(b)`)) THEN
1170 MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC)
1172 [MP_TAC (DISCH_ALL STEP_EXP_0) THEN ASM_REWRITE_TAC[];
1173 MP_TAC (DISCH_ALL STEP_EXP_1) THEN ASM_REWRITE_TAC[ADD_CLAUSES];
1174 MP_TAC (DISCH_ALL STEP_EXP_2) THEN ASM_REWRITE_TAC[ADD_CLAUSES];
1175 MP_TAC (DISCH_ALL STEP_EXP_3) THEN ASM_REWRITE_TAC[ADD_CLAUSES]]);;
1177 (* ------------------------------------------------------------------------- *)
1178 (* Iterated versions. *)
1179 (* ------------------------------------------------------------------------- *)
1181 let STEPS_EXP_LEMMA = prove
1182 (`(!k. P(SUC k) ==> P(k)) /\
1183 (P(0) ==> (abs(sum(0,0) z) <= &2 * &0)) /\
1184 (P(1) ==> (abs(sum(0,1) z) <= &2 * &1)) /\
1185 (P(2) ==> (abs(sum(0,2) z) <= &2 * &2)) /\
1186 (P(3) ==> (abs(sum(0,3) z) <= &2 * &3)) /\
1187 (P(4) ==> (abs(sum(0,4) z) <= &2 * &4)) /\
1188 (!m. 4 <= m /\ P(SUC m) ==> (abs(z m) <= &2))
1189 ==> !m. P(m) ==> (abs(sum(0,m) z) <= &2 * &m)`,
1190 STRIP_TAC THEN SUBGOAL_THEN
1192 abs(sum(0,d + 4) z) <= &2 * &(d + 4)`
1194 [INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN
1195 DISCH_TAC THEN REWRITE_TAC[sum; ADD1] THEN
1196 ONCE_REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN
1197 REWRITE_TAC[REAL_ADD_LDISTRIB] THEN
1198 MATCH_MP_TAC(REAL_LE_IMP(REAL_ARITH `abs(a + b) <= abs(a) + abs(b)`)) THEN
1199 MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL
1200 [FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
1201 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
1202 REWRITE_TAC[REAL_MUL_RID] THEN FIRST_ASSUM MATCH_MP_TAC THEN
1203 ASM_REWRITE_TAC[ADD_CLAUSES] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
1204 REWRITE_TAC[LE_ADD]];
1206 DISJ_CASES_THEN MP_TAC (SPECL [`4`; `m:num`] LE_CASES) THENL
1207 [DISCH_THEN(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[LE_EXISTS]) THEN
1208 ONCE_REWRITE_TAC[ADD_SYM] THEN ASM_REWRITE_TAC[];
1209 SUBST1_TAC(TOP_DEPTH_CONV num_CONV `4`) THEN
1210 REWRITE_TAC[LE] THEN REWRITE_TAC[ARITH_SUC] THEN
1211 DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN SUBST1_TAC) THEN
1212 ASM_REWRITE_TAC[]]]);;
1214 let STEPS_EXP = prove
1216 abs(s - &2 pow n * x) < &1 /\
1217 (t(0) = &2 pow n) /\
1219 &2 * abs(t(SUC k) * &2 pow n * &(SUC k) - s * t(k))
1220 <= &2 pow n * &(SUC k))
1221 ==> abs(sum(0,m) t - &2 pow n * sum(0,m) (\i. x pow i / &(FACT i)))
1223 REWRITE_TAC[REAL_MUL_RSUM0; REAL_SUB_SUM0] THEN
1224 SPEC_TAC(`m:num`,`m:num`) THEN MATCH_MP_TAC STEPS_EXP_LEMMA THEN
1225 REWRITE_TAC[GSYM REAL_SUB_SUM0; GSYM REAL_MUL_RSUM0] THEN
1226 REWRITE_TAC[STEPS_EXP_0; STEPS_EXP_1; STEPS_EXP_2; STEPS_EXP_3] THEN
1227 REWRITE_TAC[STEPS_EXP_4; STEP_EXP_4_PLUS] THEN
1228 GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
1229 GEN_TAC THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
1230 MATCH_MP_TAC LT_TRANS THEN EXISTS_TAC `k:num` THEN
1231 ASM_REWRITE_TAC[] THEN REWRITE_TAC[LT]);;
1233 let STEPS_LN = prove
1235 abs(x) <= &1 / &2 /\
1236 abs(s - &2 pow n * --x) < &1 /\
1239 &2 * abs(t(SUC k) * &2 pow n * &(SUC(SUC k))
1240 - &(SUC k) * s * t(k))
1241 <= &2 pow n * &(SUC(SUC k)))
1242 ==> abs(sum(0,m) t - &2 pow n * sum(0,m)
1243 (\i. (--(&1)) pow i * x pow (SUC i) / &(SUC i))) <= &3 * &m`,
1244 REWRITE_TAC[REAL_MUL_RSUM0; REAL_SUB_SUM0] THEN
1245 STRIP_TAC THEN GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN
1246 MATCH_MP_TAC (REAL_LE_IMP SUM_ABS_LE) THEN
1247 MATCH_MP_TAC SUM_BOUND THEN REWRITE_TAC[ADD_CLAUSES; LE_0] THEN
1249 [REWRITE_TAC[real_pow; ARITH; REAL_DIV_1; REAL_MUL_LID; REAL_MUL_RID] THEN
1250 DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
1251 REWRITE_TAC[REAL_ARITH `-- a - b * c = --(a - b * --c)`] THEN
1252 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&1` THEN
1253 ASM_SIMP_TAC[REAL_ABS_NEG; REAL_LT_IMP_LE; REAL_OF_NUM_LE; ARITH];
1255 DISCH_THEN(fun th -> ASSUME_TAC th THEN MP_TAC th) THEN
1256 DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
1257 SUBGOAL_THEN `p:num < m` (ANTE_RES_THEN MP_TAC) THENL
1258 [UNDISCH_TAC `SUC p < m` THEN ARITH_TAC; ALL_TAC] THEN
1259 DISCH_TAC THEN DISCH_TAC THEN
1260 MATCH_MP_TAC(REAL_ARITH
1261 `!y. abs(x - y) + abs(y - z) <= e ==> abs(x - z) <= e`) THEN
1262 EXISTS_TAC `&(SUC p) * s * t p / (&2 pow n * &(SUC(SUC p)))` THEN
1263 ONCE_REWRITE_TAC [SYM(REAL_RAT_REDUCE_CONV `&1 / &2 + &5 / &2`)] THEN
1264 MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL
1265 [MATCH_MP_TAC REAL_LE_RCANCEL_IMP THEN
1266 EXISTS_TAC `&2 pow n * &(SUC(SUC p))` THEN
1267 SUBGOAL_THEN `&0 < &2 pow n * &(SUC(SUC p))` ASSUME_TAC THENL
1268 [MATCH_MP_TAC REAL_LT_MUL THEN
1269 SIMP_TAC[REAL_POW_LT; REAL_OF_NUM_LT; LT_0; ARITH]; ALL_TAC] THEN
1270 ASM_REWRITE_TAC[] THEN
1271 SUBGOAL_THEN `!x y. &0 < y ==> (abs(x) * y = abs(x * y))`
1272 (fun th -> ASM_SIMP_TAC[th]) THENL
1273 [REPEAT STRIP_TAC THEN REWRITE_TAC[REAL_ABS_MUL] THEN
1274 AP_TERM_TAC THEN ASM_SIMP_TAC[real_abs; REAL_LT_IMP_LE]; ALL_TAC] THEN
1275 MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN EXISTS_TAC `&2` THEN
1276 REWRITE_TAC[REAL_MUL_ASSOC] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
1277 REWRITE_TAC[GSYM REAL_MUL_ASSOC; REAL_MUL_LID] THEN
1278 REWRITE_TAC[REAL_SUB_RDISTRIB] THEN
1279 SUBGOAL_THEN `!a b c d. &0 < a ==> ((b * c * d / a) * a = b * c * d)`
1280 (fun th -> ASM_SIMP_TAC[th]) THEN
1281 SIMP_TAC[real_div; GSYM REAL_MUL_ASSOC; REAL_MUL_LINV; REAL_MUL_RID;
1284 MATCH_MP_TAC(REAL_ARITH
1285 `!y. abs(x - y) + abs(y - z) <= e ==> abs(x - z) <= e`) THEN
1286 EXISTS_TAC `--(&1) pow p * s * x pow (SUC p) / &(SUC(SUC p))` THEN
1287 ONCE_REWRITE_TAC [SYM(REAL_RAT_REDUCE_CONV `&9 / &4 + &1 / &4`)] THEN
1288 MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL
1289 [SUBGOAL_THEN `--(&1) pow p * s * x pow (SUC p) / &(SUC(SUC p)) =
1291 (&2 pow n * --(&1) pow p * x pow SUC p / &(SUC p)) /
1292 (&2 pow n * &(SUC (SUC p)))`
1294 [REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC; REAL_INV_MUL] THEN
1295 ONCE_REWRITE_TAC[AC REAL_MUL_AC
1296 `a * b * c * d * e * f * g * h =
1297 d * b * e * h * (g * c) * (f * a)`] THEN
1298 SIMP_TAC[REAL_MUL_LINV; REAL_POW_EQ_0; REAL_OF_NUM_EQ;
1299 ARITH; NOT_SUC] THEN
1300 REWRITE_TAC[REAL_MUL_RID]; ALL_TAC] THEN
1301 REWRITE_TAC[GSYM REAL_SUB_LDISTRIB; REAL_ABS_MUL] THEN
1302 REWRITE_TAC[real_div; REAL_MUL_ASSOC; GSYM REAL_SUB_RDISTRIB] THEN
1303 REWRITE_TAC[REAL_ABS_MUL; GSYM REAL_MUL_ASSOC] THEN
1304 REWRITE_TAC[GSYM real_div] THEN
1305 ONCE_REWRITE_TAC[AC REAL_MUL_AC `a * b * c * d = (a * b * d) * c`] THEN
1306 GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o REDEPTH_CONV)
1307 [GSYM REAL_ABS_MUL] THEN
1308 MATCH_MP_TAC REAL_LE_TRANS THEN
1309 EXISTS_TAC `abs (&(SUC p) * s * inv (&2 pow n * &(SUC (SUC p)))) * &3` THEN
1310 ASM_SIMP_TAC[REAL_LE_LMUL; REAL_ABS_POS] THEN
1311 REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_NUM; REAL_ABS_INV; REAL_ABS_POW] THEN
1312 REWRITE_TAC[REAL_INV_MUL] THEN
1313 REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
1314 ONCE_REWRITE_TAC[AC REAL_MUL_AC `a * b * c * d * e =
1315 (d * a) * (b * c) * e`] THEN
1316 MATCH_MP_TAC REAL_LE_TRANS THEN
1317 EXISTS_TAC `inv(&1) * &3 / &4 * &3` THEN
1318 CONV_TAC(RAND_CONV REAL_RAT_REDUCE_CONV) THEN REWRITE_TAC[] THEN
1319 REWRITE_TAC[REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LE_RMUL THEN
1320 REWRITE_TAC[REAL_OF_NUM_LE; ARITH] THEN
1321 ONCE_REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
1322 MATCH_MP_TAC REAL_LE_MUL2 THEN
1323 SIMP_TAC[REAL_LE_MUL; REAL_LE_INV_EQ; REAL_POS;
1324 REAL_POW_LE; REAL_ABS_POS] THEN
1326 [MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN
1327 EXISTS_TAC `&(SUC(SUC p))` THEN
1328 SIMP_TAC[REAL_MUL_ASSOC; REAL_MUL_RINV; REAL_OF_NUM_EQ; NOT_SUC] THEN
1329 REWRITE_TAC[REAL_INV_1; REAL_MUL_LID; REAL_MUL_RID] THEN
1330 REWRITE_TAC[REAL_OF_NUM_LT; REAL_OF_NUM_LE] THEN ARITH_TAC;
1331 MATCH_MP_TAC REAL_LE_RCANCEL_IMP THEN
1332 EXISTS_TAC `&2 pow n` THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
1333 SIMP_TAC[REAL_MUL_LINV; REAL_POW_EQ_0; REAL_OF_NUM_EQ; ARITH_EQ] THEN
1334 SIMP_TAC[REAL_POW_LT; REAL_OF_NUM_LT; ARITH; REAL_MUL_RID] THEN
1335 MATCH_MP_TAC(REAL_ARITH
1336 `!y. abs(x - y) < &1 /\ abs(y) <= d - &1 ==> abs(x) <= d`) THEN
1337 EXISTS_TAC `&2 pow n * --x` THEN ASM_REWRITE_TAC[] THEN
1338 MATCH_MP_TAC REAL_LE_RCANCEL_IMP THEN EXISTS_TAC `inv(&2 pow n)` THEN
1339 SIMP_TAC[REAL_LT_INV_EQ; REAL_POW_LT; REAL_OF_NUM_LT; ARITH] THEN
1340 REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_NEG; REAL_ABS_POW; REAL_ABS_NUM] THEN
1341 GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] THEN
1342 SIMP_TAC[REAL_MUL_ASSOC; REAL_MUL_LINV; REAL_POW_EQ_0; REAL_OF_NUM_EQ;
1344 REWRITE_TAC[REAL_MUL_LID] THEN MATCH_MP_TAC REAL_LE_TRANS THEN
1345 EXISTS_TAC `&1 / &2` THEN ASM_REWRITE_TAC[] THEN
1346 REWRITE_TAC[real_div; REAL_SUB_RDISTRIB; GSYM REAL_MUL_ASSOC] THEN
1347 SIMP_TAC[REAL_MUL_RINV; REAL_POW_EQ_0; REAL_OF_NUM_EQ; ARITH_EQ] THEN
1348 REWRITE_TAC[REAL_MUL_LID; REAL_MUL_RID] THEN
1349 REWRITE_TAC[REAL_LE_SUB_LADD] THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
1350 REWRITE_TAC[GSYM REAL_LE_SUB_LADD] THEN
1351 CONV_TAC REAL_RAT_REDUCE_CONV THEN
1352 REWRITE_TAC[real_div; REAL_MUL_LID] THEN
1353 MATCH_MP_TAC REAL_LE_INV2 THEN
1354 REWRITE_TAC[REAL_OF_NUM_LT; ARITH] THEN
1355 SUBST1_TAC(SYM(REAL_INT_REDUCE_CONV `&2 pow 2`)) THEN
1356 MATCH_MP_TAC REAL_POW_MONO THEN
1357 ASM_REWRITE_TAC[REAL_OF_NUM_LE; ARITH]];
1360 `--(&1) pow p * s * x pow (SUC p) / &(SUC(SUC p)) -
1361 &2 pow n * --(&1) pow (SUC p) * x pow (SUC(SUC p)) / &(SUC(SUC p)) =
1362 (--(&1) pow p * x pow (SUC p) / &(SUC(SUC p))) *
1363 (s - &2 pow n * --x)`
1365 [REWRITE_TAC[real_pow; real_div; GSYM REAL_OF_NUM_SUC] THEN
1366 REWRITE_TAC[REAL_SUB_LDISTRIB; GSYM REAL_MUL_ASSOC] THEN
1367 REWRITE_TAC[REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_MUL_LID] THEN
1368 REWRITE_TAC[REAL_NEG_NEG; REAL_MUL_AC]; ALL_TAC] THEN
1369 ONCE_REWRITE_TAC[REAL_ABS_MUL] THEN
1370 MATCH_MP_TAC REAL_LE_TRANS THEN
1371 EXISTS_TAC `abs (-- (&1) pow p * x pow SUC p / &(SUC (SUC p))) * &1` THEN
1372 ASM_SIMP_TAC[REAL_LE_LMUL; REAL_ABS_POS; REAL_LT_IMP_LE] THEN
1373 REWRITE_TAC[REAL_MUL_RID; real_div; REAL_ABS_MUL; REAL_ABS_POW;
1374 REAL_ABS_NEG; REAL_ABS_NUM; REAL_ABS_INV] THEN
1375 REWRITE_TAC[REAL_POW_ONE; REAL_MUL_LID] THEN
1376 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `inv(&2) pow 1 * inv(&2)` THEN
1377 CONJ_TAC THENL [ALL_TAC; CONV_TAC REAL_RAT_REDUCE_CONV] THEN
1378 MATCH_MP_TAC REAL_LE_MUL2 THEN
1379 SIMP_TAC[REAL_ABS_POS; REAL_POW_LE;
1380 REAL_LE_INV_EQ; LE_0; REAL_OF_NUM_LE] THEN
1382 [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `inv(&2) pow (SUC p)` THEN
1384 [MATCH_MP_TAC REAL_POW_LE2 THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
1385 ASM_REWRITE_TAC[REAL_ABS_POS];
1386 REWRITE_TAC[REAL_POW_INV] THEN MATCH_MP_TAC REAL_LE_INV2 THEN
1387 CONJ_TAC THENL [CONV_TAC REAL_RAT_REDUCE_CONV; ALL_TAC] THEN
1388 MATCH_MP_TAC REAL_POW_MONO THEN
1389 REWRITE_TAC[REAL_OF_NUM_LE; ARITH] THEN ARITH_TAC];
1390 MATCH_MP_TAC REAL_LE_INV2 THEN
1391 REWRITE_TAC[REAL_OF_NUM_LT; ARITH; REAL_OF_NUM_LE] THEN ARITH_TAC]);;
1393 (* ------------------------------------------------------------------------- *)
1394 (* Special version of Taylor series for exponential in limited range. *)
1395 (* ------------------------------------------------------------------------- *)
1397 let MCLAURIN_EXP_LE1 = prove
1398 (`!x n. abs(x) <= &1
1399 ==> ?t. abs(t) <= &1 /\
1400 (exp(x) = sum(0,n) (\m. x pow m / &(FACT m)) +
1401 (exp(t) / &(FACT n)) * x pow n)`,
1402 REPEAT STRIP_TAC THEN
1403 MP_TAC(SPECL [`x:real`; `n:num`] MCLAURIN_EXP_LE) THEN
1404 DISCH_THEN(X_CHOOSE_THEN `t:real` STRIP_ASSUME_TAC) THEN
1405 EXISTS_TAC `t:real` THEN ASM_REWRITE_TAC[] THEN
1406 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `abs(x)` THEN
1407 ASM_REWRITE_TAC[]);;
1409 let REAL_EXP_15 = prove
1411 SUBST1_TAC(SYM(REAL_RAT_REDUCE_CONV `inv(&2) + inv(&2)`)) THEN
1412 REWRITE_TAC[REAL_EXP_ADD] THEN
1413 MATCH_MP_TAC REAL_LET_TRANS THEN
1414 EXISTS_TAC `(&1 + &2 * inv(&2)) * (&1 + &2 * inv(&2))` THEN
1415 CONV_TAC(RAND_CONV REAL_RAT_REDUCE_CONV) THEN
1417 MATCH_MP_TAC REAL_LE_MUL2 THEN
1418 REWRITE_TAC[REAL_EXP_POS_LE] THEN
1419 MATCH_MP_TAC REAL_EXP_BOUND_LEMMA THEN
1420 CONV_TAC REAL_RAT_REDUCE_CONV);;
1422 let TAYLOR_EXP_WEAK = prove
1424 abs(exp(x) - sum(0,m) (\i. x pow i / &(FACT i))) < &5 * inv(&(FACT m))`,
1426 FIRST_ASSUM(MP_TAC o SPEC `m:num` o MATCH_MP MCLAURIN_EXP_LE1) THEN
1427 DISCH_THEN(X_CHOOSE_THEN `t:real` STRIP_ASSUME_TAC) THEN
1428 ASM_REWRITE_TAC[REAL_ARITH `abs((x + y) - x) = abs(y)`] THEN
1429 REWRITE_TAC[real_div; REAL_ABS_MUL; GSYM REAL_MUL_ASSOC] THEN
1430 ASM_CASES_TAC `x = &0` THENL
1431 [ASM_REWRITE_TAC[] THEN
1432 SPEC_TAC(`m:num`,`m:num`) THEN INDUCT_TAC THENL
1433 [REWRITE_TAC[real_pow; FACT; ABS_N; REAL_INV_1; REAL_MUL_RID] THEN
1434 ASM_REWRITE_TAC[real_abs; REAL_EXP_POS_LE] THEN
1435 MATCH_MP_TAC REAL_LET_TRANS THEN
1436 EXISTS_TAC `exp(&1)` THEN REWRITE_TAC[REAL_EXP_15] THEN
1437 REWRITE_TAC[REAL_EXP_MONO_LE] THEN
1438 UNDISCH_TAC `abs(t) <= &1` THEN REAL_ARITH_TAC;
1439 REWRITE_TAC[POW_0; REAL_ABS_0; REAL_MUL_RZERO] THEN
1440 MATCH_MP_TAC REAL_LT_MUL THEN REWRITE_TAC[REAL_OF_NUM_LT; ARITH] THEN
1441 MATCH_MP_TAC REAL_INV_POS THEN
1442 REWRITE_TAC[REAL_OF_NUM_LT; FACT_LT]];
1443 MATCH_MP_TAC REAL_LTE_TRANS THEN
1444 EXISTS_TAC `&5 * abs(inv(&(FACT m))) * abs(x pow m)` THEN CONJ_TAC THENL
1445 [MATCH_MP_TAC REAL_LT_RMUL_IMP THEN CONJ_TAC THENL
1446 [MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `abs(exp(&1))` THEN
1447 ASM_REWRITE_TAC[real_abs; REAL_EXP_POS_LE; REAL_EXP_MONO_LE;
1449 UNDISCH_TAC `abs(t) <= &1` THEN REAL_ARITH_TAC;
1450 MATCH_MP_TAC REAL_LT_MUL THEN
1451 ASM_REWRITE_TAC[GSYM ABS_NZ; REAL_POW_EQ_0] THEN
1452 REWRITE_TAC[REAL_INV_EQ_0; REAL_OF_NUM_EQ] THEN
1453 MP_TAC(SPEC `m:num` FACT_LT) THEN ARITH_TAC];
1454 MATCH_MP_TAC REAL_LE_LMUL_IMP THEN
1455 REWRITE_TAC[REAL_OF_NUM_LE; ARITH] THEN
1456 GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN
1457 MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[REAL_ABS_POS] THEN
1458 REWRITE_TAC[REAL_ABS_INV; ABS_N; REAL_LE_REFL] THEN
1459 REWRITE_TAC[REAL_ABS_POW] THEN
1460 MATCH_MP_TAC REAL_POW_1_LE THEN
1461 ASM_REWRITE_TAC[REAL_ABS_POS]]]);;
1463 let REAL_EXP_13 = prove
1465 MP_TAC(INST [`&1`,`x:real`; `5`,`m:num`] TAYLOR_EXP_WEAK) THEN
1466 CONV_TAC(ONCE_DEPTH_CONV REAL_SUM_CONV) THEN
1467 REWRITE_TAC[ADD_CLAUSES] THEN
1468 CONV_TAC(ONCE_DEPTH_CONV NUM_FACT_CONV) THEN
1469 CONV_TAC REAL_RAT_REDUCE_CONV THEN
1470 MATCH_MP_TAC(REAL_ARITH
1471 `b + e <= c ==> abs(a - b) < e ==> a < c`) THEN
1472 CONV_TAC REAL_RAT_REDUCE_CONV);;
1474 let TAYLOR_EXP = prove
1476 abs(exp(x) - sum(0,m) (\i. x pow i / &(FACT i))) < &3 * inv(&(FACT m))`,
1478 FIRST_ASSUM(MP_TAC o SPEC `m:num` o MATCH_MP MCLAURIN_EXP_LE1) THEN
1479 DISCH_THEN(X_CHOOSE_THEN `t:real` STRIP_ASSUME_TAC) THEN
1480 ASM_REWRITE_TAC[REAL_ARITH `abs((x + y) - x) = abs(y)`] THEN
1481 REWRITE_TAC[real_div; REAL_ABS_MUL; GSYM REAL_MUL_ASSOC] THEN
1482 ASM_CASES_TAC `x = &0` THENL
1483 [ASM_REWRITE_TAC[] THEN
1484 SPEC_TAC(`m:num`,`m:num`) THEN INDUCT_TAC THENL
1485 [REWRITE_TAC[real_pow; FACT; ABS_N; REAL_INV_1; REAL_MUL_RID] THEN
1486 ASM_REWRITE_TAC[real_abs; REAL_EXP_POS_LE] THEN
1487 MATCH_MP_TAC REAL_LET_TRANS THEN
1488 EXISTS_TAC `exp(&1)` THEN REWRITE_TAC[REAL_EXP_13] THEN
1489 REWRITE_TAC[REAL_EXP_MONO_LE] THEN
1490 UNDISCH_TAC `abs(t) <= &1` THEN REAL_ARITH_TAC;
1491 REWRITE_TAC[POW_0; REAL_ABS_0; REAL_MUL_RZERO] THEN
1492 MATCH_MP_TAC REAL_LT_MUL THEN REWRITE_TAC[REAL_OF_NUM_LT; ARITH] THEN
1493 MATCH_MP_TAC REAL_INV_POS THEN
1494 REWRITE_TAC[REAL_OF_NUM_LT; FACT_LT]];
1495 MATCH_MP_TAC REAL_LTE_TRANS THEN
1496 EXISTS_TAC `&3 * abs(inv(&(FACT m))) * abs(x pow m)` THEN CONJ_TAC THENL
1497 [MATCH_MP_TAC REAL_LT_RMUL_IMP THEN CONJ_TAC THENL
1498 [MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `abs(exp(&1))` THEN
1499 ASM_REWRITE_TAC[real_abs; REAL_EXP_POS_LE; REAL_EXP_MONO_LE;
1501 UNDISCH_TAC `abs(t) <= &1` THEN REAL_ARITH_TAC;
1502 MATCH_MP_TAC REAL_LT_MUL THEN
1503 ASM_REWRITE_TAC[GSYM ABS_NZ; REAL_POW_EQ_0] THEN
1504 REWRITE_TAC[REAL_INV_EQ_0; REAL_OF_NUM_EQ] THEN
1505 MP_TAC(SPEC `m:num` FACT_LT) THEN ARITH_TAC];
1506 MATCH_MP_TAC REAL_LE_LMUL_IMP THEN
1507 REWRITE_TAC[REAL_OF_NUM_LE; ARITH] THEN
1508 GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN
1509 MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[REAL_ABS_POS] THEN
1510 REWRITE_TAC[REAL_ABS_INV; ABS_N; REAL_LE_REFL] THEN
1511 REWRITE_TAC[REAL_ABS_POW] THEN
1512 MATCH_MP_TAC REAL_POW_1_LE THEN
1513 ASM_REWRITE_TAC[REAL_ABS_POS]]]);;
1515 let TAYLOR_LN = prove
1516 (`&0 <= x /\ x <= inv(&2 pow k) ==>
1517 abs(ln(&1 + x) - sum(0,m) (\i. --(&1) pow i * x pow SUC i / & (SUC i)))
1518 < inv(&2 pow (k * SUC m) * &(SUC m))`,
1519 let lemma = INST [`1`,`k:num`] (SYM(SPEC_ALL SUM_REINDEX)) in
1521 UNDISCH_TAC `&0 <= x` THEN REWRITE_TAC[REAL_LE_LT] THEN
1522 DISCH_THEN(DISJ_CASES_THEN2 ASSUME_TAC (SUBST1_TAC o SYM)) THENL
1524 REWRITE_TAC[real_pow; REAL_MUL_LZERO; REAL_MUL_RZERO; real_div] THEN
1525 REWRITE_TAC[SUM_0; REAL_ADD_RID; REAL_SUB_LZERO; LN_1] THEN
1526 REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_0] THEN
1527 SIMP_TAC[REAL_LT_INV_EQ; REAL_LT_MUL; REAL_POW_LT; REAL_OF_NUM_LT;
1529 SUBGOAL_THEN `!i. --(&1) pow i = --(&1) pow (SUC(SUC i))`
1530 (fun th -> ONCE_REWRITE_TAC[th]) THENL
1531 [REWRITE_TAC[real_pow; REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_NEG_NEG] THEN
1532 REWRITE_TAC[REAL_MUL_LID]; ALL_TAC] THEN
1533 REWRITE_TAC[ADD1; lemma] THEN
1534 REWRITE_TAC[ADD_CLAUSES] THEN
1535 ONCE_REWRITE_TAC[SUM_DIFF] THEN
1536 CONV_TAC(ONCE_DEPTH_CONV REAL_SUM_CONV) THEN
1537 REWRITE_TAC[real_div; REAL_INV_0; REAL_MUL_RZERO] THEN
1538 REWRITE_TAC[GSYM ADD1] THEN
1539 MP_TAC(SPECL [`x:real`; `SUC m`] MCLAURIN_LN_POS) THEN
1540 ASM_REWRITE_TAC[LT_0] THEN
1541 ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[GSYM ADD1] THEN
1542 REWRITE_TAC[GSYM real_div] THEN
1543 DISCH_THEN(X_CHOOSE_THEN `t:real` STRIP_ASSUME_TAC) THEN
1544 ASM_REWRITE_TAC[REAL_SUB_RZERO; REAL_ARITH `(a + b) - a = b`] THEN
1545 REWRITE_TAC[real_div; REAL_ABS_MUL; REAL_ABS_INV; REAL_ABS_POW] THEN
1546 REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_NUM; REAL_POW_ONE] THEN
1547 REWRITE_TAC[REAL_MUL_LID; REAL_INV_MUL; GSYM REAL_MUL_ASSOC] THEN
1548 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC
1549 `inv (&2 pow (k * SUC m)) * inv (&(SUC m)) * inv(abs(&1 + t) pow SUC m)` THEN
1551 [REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
1552 MATCH_MP_TAC REAL_LE_RMUL THEN
1553 SIMP_TAC[REAL_LE_MUL; REAL_LE_INV_EQ; REAL_POS; REAL_ABS_POS;
1555 REWRITE_TAC[GSYM REAL_POW_INV] THEN
1556 REWRITE_TAC[GSYM REAL_POW_POW] THEN
1557 MATCH_MP_TAC REAL_POW_LE2 THEN
1558 ASM_SIMP_TAC[REAL_POW_INV; real_abs; REAL_LT_IMP_LE];
1559 GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN
1560 REWRITE_TAC[REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LT_LMUL THEN
1561 SIMP_TAC[REAL_LT_MUL; REAL_LT_INV_EQ; REAL_OF_NUM_LT; LT_0; REAL_POW_LT;
1563 REWRITE_TAC[GSYM REAL_POW_INV; GSYM REAL_ABS_INV] THEN
1564 SUBGOAL_THEN `abs(inv(&1 + t)) < &1` ASSUME_TAC THENL
1565 [REWRITE_TAC[REAL_ABS_INV] THEN
1566 GEN_REWRITE_TAC RAND_CONV [GSYM REAL_INV_1] THEN
1567 MATCH_MP_TAC REAL_LT_INV2 THEN
1568 UNDISCH_TAC `&0 < t` THEN REAL_ARITH_TAC;
1569 SUBST1_TAC(SYM(SPEC `SUC m` REAL_POW_ONE)) THEN
1570 MATCH_MP_TAC REAL_POW_LT2 THEN
1571 ASM_REWRITE_TAC[REAL_POW_ONE; NOT_SUC; REAL_ABS_POS]]]);;
1573 (* ------------------------------------------------------------------------- *)
1574 (* Leading from the summation to the actual function. *)
1575 (* ------------------------------------------------------------------------- *)
1577 let APPROX_LEMMA1 = prove
1578 (`abs(f(x:real) - sum(0,m) (\i. P i x)) < inv(&2 pow (n + 2)) /\
1579 abs(u - &2 pow (n + e + 2) * sum(0,m) (\i. P i x)) <= &k * &m /\
1580 &k * &m <= &2 pow e /\
1581 abs(s * &2 pow (e + 2) - u) <= &2 pow (e + 1)
1582 ==> abs(s - &2 pow n * f(x)) < &1`,
1583 STRIP_TAC THEN MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN
1584 EXISTS_TAC `&2 pow (n + e + 2)` THEN
1585 REWRITE_TAC[REAL_LT_POW2] THEN
1586 REWRITE_TAC[REAL_ABS_LEMMA; REAL_SUB_LDISTRIB; REAL_MUL_RID] THEN
1587 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN (MATCH_MP_TAC o GEN_ALL)
1588 (REAL_ARITH `abs(a - b) + abs(b - c) < d ==> abs(a - c) < d`) THEN
1589 EXISTS_TAC `&2 pow n * u` THEN
1590 CONV_TAC(funpow 4 RAND_CONV num_CONV) THEN
1591 REWRITE_TAC[ADD_CLAUSES; real_pow; REAL_MUL_2] THEN
1592 MATCH_MP_TAC REAL_LET_ADD2 THEN CONJ_TAC THENL
1593 [ONCE_REWRITE_TAC[REAL_POW_ADD] THEN
1594 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o LAND_CONV) [REAL_MUL_SYM] THEN
1595 REWRITE_TAC[GSYM REAL_MUL_ASSOC; GSYM REAL_SUB_LDISTRIB] THEN
1596 REWRITE_TAC[GSYM REAL_ABS_LEMMA] THEN
1597 MATCH_MP_TAC REAL_LE_LMUL THEN
1598 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN ASM_REWRITE_TAC[] THEN
1599 MATCH_MP_TAC REAL_LT_IMP_LE THEN REWRITE_TAC[REAL_LT_POW2];
1600 REWRITE_TAC[GSYM REAL_MUL_ASSOC; GSYM REAL_SUB_LDISTRIB] THEN
1601 GEN_REWRITE_TAC RAND_CONV [REAL_POW_ADD] THEN
1602 REWRITE_TAC[GSYM REAL_ABS_LEMMA] THEN
1603 MATCH_MP_TAC REAL_LT_LMUL THEN REWRITE_TAC[REAL_LT_POW2] THEN
1604 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN (MATCH_MP_TAC o GEN_ALL)
1605 (REAL_ARITH `abs(a - b) + abs(b - c) < d ==> abs(a - c) < d`) THEN
1607 `&2 pow (n + e + 2) * sum(0,m) (\i. P i (x:real))` THEN
1608 GEN_REWRITE_TAC RAND_CONV [REAL_POW_ADD] THEN
1609 GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN
1610 REWRITE_TAC[REAL_POW_1; REAL_MUL_2] THEN
1611 MATCH_MP_TAC REAL_LET_ADD2 THEN CONJ_TAC THENL
1612 [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&k * &m` THEN
1614 REWRITE_TAC[GSYM REAL_SUB_LDISTRIB; GSYM REAL_ABS_LEMMA] THEN
1615 ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[GSYM ADD_ASSOC] THEN
1616 ONCE_REWRITE_TAC[REAL_POW_ADD] THEN
1617 REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
1618 GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN
1619 MATCH_MP_TAC REAL_LT_LMUL THEN
1620 REWRITE_TAC[REAL_LT_POW2] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
1621 MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN
1622 EXISTS_TAC `inv(&2 pow (n + 2))` THEN
1623 REWRITE_TAC[REAL_LT_INV_EQ; REAL_LT_POW2] THEN
1624 REWRITE_TAC[REAL_MUL_RID; REAL_MUL_ASSOC] THEN
1625 ONCE_REWRITE_TAC[REAL_ABS_SUB] THEN
1626 SUBGOAL_THEN `inv(&2 pow (n + 2)) * &2 pow (n + 2) = &1`
1627 (fun th -> ASM_REWRITE_TAC[th; REAL_MUL_LID]) THEN
1628 MATCH_MP_TAC REAL_MUL_LINV THEN REWRITE_TAC[REAL_POW_EQ_0] THEN
1629 REWRITE_TAC[DE_MORGAN_THM] THEN DISJ1_TAC THEN REAL_ARITH_TAC]]);;
1631 (* ------------------------------------------------------------------------- *)
1632 (* Approximation theorems. *)
1633 (* ------------------------------------------------------------------------- *)
1635 let APPROX_EXP = prove
1636 (`(n + e + 2 = p) /\
1637 &3 * &2 pow (n + 2) <= &(FACT m) /\
1638 &2 * &m <= &2 pow e /\
1640 abs(s - &2 pow p * x) < &1 /\
1641 (t(0) = &2 pow p) /\
1643 &2 * abs(t(SUC k) * &2 pow p * &(SUC k) - s * t(k))
1644 <= &2 pow p * &(SUC k)) /\
1645 abs(u * &2 pow (e + 2) - sum(0,m) t) <= &2 pow (e + 1)
1646 ==> abs(u - &2 pow n * exp(x)) < &1`,
1647 STRIP_TAC THEN MATCH_MP_TAC(GEN_ALL APPROX_LEMMA1) THEN
1648 MAP_EVERY EXISTS_TAC
1649 [`\i x. x pow i / &(FACT i)`; `2`; `m:num`; `sum(0,m) t`; `e:num`] THEN
1650 ASM_REWRITE_TAC[BETA_THM] THEN CONJ_TAC THENL
1651 [MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&3 * inv(&(FACT m))` THEN
1653 [MATCH_MP_TAC TAYLOR_EXP THEN ASM_REWRITE_TAC[];
1654 SUBST1_TAC(SYM(SPEC `&3` REAL_INV_INV)) THEN
1655 REWRITE_TAC[GSYM REAL_INV_MUL] THEN
1656 MATCH_MP_TAC REAL_LE_INV2 THEN ASM_REWRITE_TAC[REAL_LT_POW2] THEN
1657 MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN EXISTS_TAC `&3` THEN
1658 REWRITE_TAC[REAL_MUL_ASSOC] THEN
1659 REWRITE_TAC[MATCH_MP REAL_MUL_RINV (REAL_ARITH `~(&3 = &0)`)] THEN
1660 ASM_REWRITE_TAC[REAL_MUL_LID] THEN REAL_ARITH_TAC];
1661 MATCH_MP_TAC STEPS_EXP THEN ASM_REWRITE_TAC[]]);;
1663 let APPROX_LN = prove
1666 &2 pow (n + 2) <= &2 pow (k * SUC m) * &(SUC m) /\
1667 &3 * &m <= &2 pow e /\
1668 (&0 <= x /\ x <= inv(&2 pow k)) /\
1669 abs(s - &2 pow p * --x) < &1 /\
1672 &2 * abs(t(SUC k) * &2 pow p * &(SUC(SUC k)) -
1673 &(SUC k) * s * t(k))
1674 <= &2 pow p * &(SUC(SUC k))) /\
1675 abs(u * &2 pow (e + 2) - sum(0,m) t) <= &2 pow (e + 1)
1676 ==> abs(u - &2 pow n * ln(&1 + x)) < &1`,
1678 (MATCH_MP_TAC o GEN_ALL o BETA_RULE)
1679 (INST [`\x. ln(&1 + x):real`,`f:real->real`] APPROX_LEMMA1) THEN
1680 MAP_EVERY EXISTS_TAC
1681 [`\i x. (--(&1)) pow i * x pow (SUC i) / &(SUC i)`;
1682 `3`; `m:num`; `sum(0,m) t`; `e:num`] THEN
1683 ASM_REWRITE_TAC[BETA_THM] THEN CONJ_TAC THENL
1684 [MATCH_MP_TAC REAL_LTE_TRANS THEN
1685 EXISTS_TAC `inv(&2 pow (k * SUC m) * &(SUC m))` THEN CONJ_TAC THENL
1686 [MATCH_MP_TAC TAYLOR_LN THEN ASM_REWRITE_TAC[];
1687 MATCH_MP_TAC REAL_LE_INV2 THEN ASM_REWRITE_TAC[REAL_LT_POW2]];
1688 MATCH_MP_TAC STEPS_LN THEN ASM_REWRITE_TAC[] THEN
1689 SUBGOAL_THEN `2 <= (n + e + 2)` MP_TAC THENL
1690 [REWRITE_TAC[ADD_ASSOC] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
1691 REWRITE_TAC[LE_ADD];
1692 SUBGOAL_THEN `abs(x) <= &1 / &2` (fun th -> ASM_REWRITE_TAC[th]) THEN
1693 ASM_REWRITE_TAC[real_abs] THEN MATCH_MP_TAC REAL_LE_TRANS THEN
1694 EXISTS_TAC `inv(&2 pow k)` THEN ASM_REWRITE_TAC[] THEN
1695 REWRITE_TAC[real_div; REAL_MUL_LID] THEN
1696 GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM REAL_POW_1] THEN
1697 MATCH_MP_TAC REAL_LE_INV2 THEN REWRITE_TAC[REAL_LT_POW2] THEN
1698 MATCH_MP_TAC REAL_POW_MONO THEN
1699 REWRITE_TAC[REAL_OF_NUM_LE; ARITH] THEN
1700 UNDISCH_TAC `~(k = 0)` THEN ARITH_TAC]]);;
1702 (* ------------------------------------------------------------------------- *)
1703 (* Eliminate trivial definitions. *)
1704 (* ------------------------------------------------------------------------- *)
1709 and sconv = REWRITE_CONV[ARITH] in
1711 if tdefs = [] then th else
1713 itlist (fun tm acc ->
1714 let l,r = (rand F_F I) (dest_eq tm) in
1715 mk_cond(mk_eq(x_tm,l),r,acc)) tdefs a_tm in
1716 let atm = mk_abs(x_tm,ctm) in
1717 let ttm = rator(lhs(hd tdefs)) in
1718 let tth = ASSUME(mk_eq(ttm,atm)) in
1720 (EQT_ELIM o CONV_RULE(RAND_CONV sconv) o SUBS_CONV[tth]) tdefs in
1721 let dth = PROVE_HYP (end_itlist CONJ ths) th in
1722 MP (INST [atm,ttm] (DISCH_ALL dth)) (REFL atm);;
1724 (* ------------------------------------------------------------------------- *)
1725 (* Overall conversion. *)
1726 (* ------------------------------------------------------------------------- *)
1728 let realcalc_cache = ref [];;
1730 let REALCALC_CONV,thm_eval,raw_eval,thm_wrap =
1731 let a_tm = `a:real` and n_tm = `n:num` and n'_tm = `n':num`
1735 and b_tm = `b:real` and e_tm = `e:num`
1741 and sqrt_tm = `sqrt`
1745 and exp_tm = `exp:real->real`
1746 and ln_tm = `ln:real->real`
1747 and add1_tm = `(+) (&1)`
1748 and pow2_tm = `(pow) (&2)`
1750 and lt_tm = `(<)` in
1753 EQT_ELIM o REWRITE_CONV[REAL_EQ_NEG2; GSYM EXISTS_REFL;
1754 EXISTS_OR_THM; REAL_OF_NUM_EQ] in
1757 let q = quo_num x y in
1758 let r = x -/ (q */ y) in
1759 if le_num (abs_num(Int 2 */ r)) (abs_num y) then q
1760 else if le_num (abs_num(Int 2 */ (r -/ y))) (abs_num y) then q +/ Int 1
1761 else if le_num (abs_num(Int 2 */ (r +/ y))) (abs_num y) then q -/ Int 1
1762 else let s = (string_of_num x)^" and "^(string_of_num y) in
1763 failwith ("ndiv: "^s) in
1765 let raw_wrap (f:num->num) = (ref(Int(-1),Int 0),f) in
1767 let raw_eval(r,(f:num->num)) n =
1769 if le_num n n0 then ndiv y0 (power_num (Int 2) (n0 -/ n))
1770 else let y = f n in (r := (n,y); y) in
1774 and mk_add = mk_binop `(+):num->num->num` in
1775 fun (r,(f:num->thm)) n ->
1776 let (n0,y0th) = !r in
1778 if n =/ n0 then y0th else
1779 let th1 = NUM_SUC_CONV
1780 (mk_comb(SUC_tm,mk_numeral(n0 -/ (n +/ Int 1)))) in
1781 let th2 = MATCH_MP REALCALC_DOWNGRADE th1 in
1782 let th3 = NUM_ADD_CONV(mk_add(mk_numeral(n)) (mk_numeral(n0 -/ n))) in
1783 let th4 = MATCH_MP th2 th3 in
1784 let th5 = MATCH_MP th4 y0th in
1785 let tm5 = fst(dest_imp(concl th5)) in
1786 let tm5a,tm5b = dest_comb tm5 in
1787 let th6 = REAL_INT_POW_CONV tm5b in
1788 let tm5c = rand(rand tm5a) in
1789 let tm5d,tm5e = dest_comb tm5c in
1790 let tm5f,tm5g = dest_comb(rand tm5d) in
1791 let tm5h = rand(rand tm5f) in
1792 let bin = mk_realintconst
1793 (ndiv (dest_realintconst tm5e) (power_num (Int 2) (dest_numeral tm5h))) in
1794 let th7 = AP_TERM (rator(rand tm5f)) th1 in
1795 let th8 = GEN_REWRITE_RULE LAND_CONV [CONJUNCT2 real_pow] th7 in
1796 let th9 = SYM(GEN_REWRITE_RULE (LAND_CONV o RAND_CONV) [th6] th8) in
1797 let th10 = TRANS th9 (REAL_INT_MUL_CONV (rand(concl th9))) in
1798 let th11 = AP_THM (AP_TERM (rator tm5f) th10) bin in
1799 let th12 = TRANS th11 (REAL_INT_MUL_CONV (rand(concl th11))) in
1800 let th13 = AP_THM (AP_TERM (rator tm5d) th12) tm5e in
1801 let th14 = TRANS th13 (REAL_INT_SUB_CONV (rand(concl th13))) in
1802 let th15 = AP_TERM (rator(rand tm5a)) th14 in
1803 let th16 = TRANS th15 (REAL_INT_ABS_CONV (rand(concl th15))) in
1804 let th17 = MK_COMB(AP_TERM (rator tm5a) th16,th6) in
1805 let th18 = TRANS th17 (REAL_INT_LE_CONV (rand(concl th17))) in
1806 MATCH_MP th5 (EQT_ELIM th18)
1807 else let yth = f n in (r := (n,yth); yth) in
1809 let thm_wrap (f:num->thm) = (ref(Int(-1),TRUTH),f) in
1812 let rec find_msd n f =
1813 if Int 1 </ abs_num(raw_eval f n) then n
1814 else find_msd (n +/ Int 1) f in
1818 let rec find_msd n f =
1819 if Int 32 </ abs_num(raw_eval f n) then n
1820 else find_msd (n +/ Int 1) f in
1824 let k = find_acc f in
1825 let a = abs_num(raw_eval f k) in
1826 k -/ log2 (a +/ Int 1) in
1828 let REALCALC_EXP_CONV =
1829 let t_tm = `t:num->real`
1836 and x_tm = `x:real` in
1837 let rec calculate_m acc i r =
1838 if acc >=/ r then i else
1839 let i' = i +/ Int 1 in
1840 calculate_m (i' */ acc) i' r in
1841 let calculate_exp_sequence =
1842 let rec calculate_exp_sequence p2 s i =
1843 if i </ Int 0 then []
1844 else if i =/ Int 0 then [p2] else
1845 let acc = calculate_exp_sequence p2 s (i -/ Int 1) in
1847 let t' = ndiv (s */ t) (p2 */ i) in
1849 fun p s m -> let p2 = power_num (Int 2) p in
1850 rev(calculate_exp_sequence p2 s (m -/ Int 1)) in
1853 abs(s - &2 pow p * x) < &1 ==>
1855 &3 * &2 pow (n + 2) <= &(FACT m) /\
1856 &2 * &m <= &2 pow e /\
1857 (t(0) = &2 pow p) /\
1859 &2 * abs(t(SUC k) * &2 pow p * &(SUC k) - s * t(k))
1860 <= &2 pow p * &(SUC k)) /\
1861 abs(u * &2 pow (e + 2) - sum(0,m) t) <= &2 pow (e + 1)
1862 ==> abs(u - &2 pow n * exp(x)) < &1`,
1863 REPEAT STRIP_TAC THEN MATCH_MP_TAC APPROX_EXP THEN
1864 ASM_REWRITE_TAC[]) in
1865 let LEFT_ZERO_RULE =
1866 ONCE_REWRITE_RULE[prove(`0 + n = n`,REWRITE_TAC[ADD_CLAUSES])] in
1869 let m = calculate_m (Int 1) (Int 0)
1870 (Int 3 */ (power_num (Int 2) (n +/ Int 2))) in
1871 let e = log2 (Int 2 */ m) in
1872 let p = n +/ e +/ Int 2 in
1873 let s = raw_eval fn1 p in
1874 let seq = calculate_exp_sequence p s m in
1875 let u0 = itlist (+/) seq (Int 0) in
1876 ndiv u0 (power_num (Int 2) (e +/ Int 2))
1878 let m = calculate_m (Int 1) (Int 0)
1879 (Int 3 */ (power_num (Int 2) (n +/ Int 2))) in
1880 let e = log2 (Int 2 */ m) in
1881 let p = n +/ e +/ Int 2 in
1882 let sth = thm_eval fn2 p in
1883 let tm1 = rand(lhand(concl sth)) in
1884 let s_num = lhand tm1 in
1885 let x_num = rand(rand tm1) in
1886 let s = dest_realintconst s_num in
1887 let seq = calculate_exp_sequence p s m in
1888 let u0 = itlist (+/) seq (Int 0) in
1889 let u = ndiv u0 (power_num (Int 2) (e +/ Int 2)) in
1890 let m_num = mk_numeral m
1891 and n_num = mk_numeral n
1892 and e_num = mk_numeral e
1893 and p_num = mk_numeral p
1894 and u_num = mk_realintconst u in
1895 let tdefs = map2 (fun a b -> mk_eq(mk_comb(t_tm,mk_small_numeral a),
1896 mk_realintconst b)) (0--(length seq - 1)) seq in
1897 let p2th = REAL_INT_POW_CONV (mk_comb(pow2_tm,p_num)) in
1898 let th0 = INST [m_num,m_tm; n_num,n_tm; e_num,e_tm;
1899 x_num,x_tm; p_num,p_tm; s_num,s_tm; u_num,u_tm] pth in
1900 let th0' = MP th0 (EQT_ELIM(REAL_RAT_REDUCE_CONV(lhand(concl th0)))) in
1901 let th1 = MP th0' sth in
1902 let th2 = CONV_RULE (ONCE_DEPTH_CONV EXPAND_RANGE_CONV) th1 in
1903 let th3 = LEFT_ZERO_RULE
1904 (CONV_RULE (ONCE_DEPTH_CONV REAL_SUM_CONV) th2) in
1905 let ths = try CONJUNCTS(ASSUME(list_mk_conj tdefs))
1906 with Failure _ -> [] in
1907 let th4 = SUBS (p2th::ths) th3 in
1908 let th5 = CONV_RULE (LAND_CONV
1909 (DEPTH_CONV NUM_ADD_CONV THENC
1910 ONCE_DEPTH_CONV NUM_FACT_CONV THENC
1911 REAL_INT_REDUCE_CONV)) th4 in
1912 MP (ELIMINATE_DEF tdefs th5) TRUTH in
1913 raw_wrap raw_fn,thm_wrap thm_fn in
1915 let REALCALC_LN_CONV =
1916 let t_tm = `t:num->real`
1924 and x_tm = `x:real` in
1925 let rec calculate_m acc k2 m r =
1926 if acc */ (m +/ Int 1) >=/ r then m else
1927 calculate_m (k2 */ acc) k2 (m +/ Int 1) r in
1928 let calculate_ln_sequence =
1929 let rec calculate_ln_sequence p2 s i =
1930 if i </ Int 0 then []
1931 else if i =/ Int 0 then [s] else
1932 let acc = calculate_ln_sequence p2 s (i -/ Int 1) in
1934 let t' = ndiv (Int(-1) */ s */ t */ i) (p2 */ (i +/ Int 1)) in
1936 fun p s m -> let p2 = power_num (Int 2) p in
1937 rev(calculate_ln_sequence p2 s (m -/ Int 1)) in
1939 (`&0 <= x /\ x <= inv(&2 pow k) ==>
1940 abs(s - &2 pow p * x) < &1 ==>
1943 &2 pow (n + 2) <= &2 pow (k * SUC m) * &(SUC m) /\
1944 &3 * &m <= &2 pow e /\
1947 &2 * abs(t(SUC k) * &2 pow p * &(SUC(SUC k)) -
1948 &(SUC k) * --s * t(k))
1949 <= &2 pow p * &(SUC(SUC k))) /\
1950 abs(u * &2 pow (e + 2) - sum(0,m) t) <= &2 pow (e + 1)
1951 ==> abs(u - &2 pow n * ln(&1 + x)) < &1`,
1952 REPEAT STRIP_TAC THEN MATCH_MP_TAC(INST [`--s`,`s:real`] APPROX_LN) THEN
1953 ASM_REWRITE_TAC[REAL_NEG_NEG] THEN
1954 REWRITE_TAC[REAL_MUL_RNEG] THEN
1955 REWRITE_TAC[REAL_ARITH `abs(--a - --b) = abs(a - b)`] THEN
1956 ASM_REWRITE_TAC[]) in
1957 let LEFT_ZERO_RULE =
1958 ONCE_REWRITE_RULE[prove(`0 + n = n`,REWRITE_TAC[ADD_CLAUSES])] in
1959 let pow2_tm = `(pow) (&2)` in
1960 let default_tdefs = [`t 0 = &0`] in
1963 let k = find_ubound fn1 in
1964 if k </ Int 1 then failwith "ln of number not provably <= 1/2" else
1965 let k2 = power_num (Int 2) k in
1966 let m = calculate_m k2 k2 (Int 0) (power_num (Int 2) (n +/ Int 2)) in
1967 let e = log2 (Int 3 */ m) in
1968 let p = n +/ e +/ Int 2 in
1969 let s = raw_eval fn1 p in
1970 let seq = calculate_ln_sequence p s m in
1971 let u0 = itlist (+/) seq (Int 0) in
1972 ndiv u0 (power_num (Int 2) (e +/ Int 2))
1974 let k = find_ubound fn1 in
1975 if k </ Int 1 then failwith "ln of number not provably <= 1/2" else
1976 let k2 = power_num (Int 2) k in
1977 let m = calculate_m k2 k2 (Int 0) (power_num (Int 2) (n +/ Int 2)) in
1978 let e = log2 (Int 3 */ m) in
1979 let p = n +/ e +/ Int 2 in
1980 let sth = thm_eval fn2 p in
1981 let tm1 = rand(lhand(concl sth)) in
1982 let s_num = lhand tm1 in
1983 let x_num = rand(rand tm1) in
1984 let s = dest_realintconst s_num in
1985 let seq = calculate_ln_sequence p s m in
1986 let u0 = itlist (+/) seq (Int 0) in
1987 let u = ndiv u0 (power_num (Int 2) (e +/ Int 2)) in
1988 let m_num = mk_numeral m
1989 and n_num = mk_numeral n
1990 and e_num = mk_numeral e
1991 and p_num = mk_numeral p
1992 and k_num = mk_numeral k
1993 and u_num = mk_realintconst u in
1994 let tdefs0 = map2 (fun a b -> mk_eq(mk_comb(t_tm,mk_small_numeral a),
1995 mk_realintconst b)) (0--(length seq - 1)) seq in
1996 let tdefs = if tdefs0 = [] then default_tdefs else tdefs0 in
1997 let p2th = REAL_INT_POW_CONV (mk_comb(pow2_tm,p_num)) in
1998 let th0 = INST [m_num,m_tm; n_num,n_tm; e_num,e_tm; k_num,k_tm;
1999 x_num,x_tm; p_num,p_tm; s_num,s_tm; u_num,u_tm] pth in
2000 let th0' = MP th0 (EQT_ELIM(REAL_RAT_REDUCE_CONV(lhand(concl th0)))) in
2001 let th1 = MP th0' sth in
2002 let th2 = CONV_RULE (ONCE_DEPTH_CONV EXPAND_RANGE_CONV) th1 in
2003 let th3 = LEFT_ZERO_RULE
2004 (CONV_RULE (ONCE_DEPTH_CONV REAL_SUM_CONV) th2) in
2005 let ths = try CONJUNCTS(ASSUME(list_mk_conj tdefs))
2006 with Failure _ -> [] in
2007 let th4 = SUBS (p2th::ths) th3 in
2008 let th5 = CONV_RULE (LAND_CONV
2009 (NUM_REDUCE_CONV THENC
2010 REAL_INT_REDUCE_CONV)) th4 in
2011 MP (ELIMINATE_DEF tdefs th5) TRUTH in
2012 raw_wrap raw_fn,thm_wrap thm_fn in
2014 let REALCALC_SQRT_CONV =
2016 let rec isolate_sqrt (a,b) y =
2017 if abs_num(a -/ b) <=/ Int 1 then
2018 if abs_num(a */ a -/ y) <=/ a then a else b
2020 let c = quo_num (a +/ b) (Int 2) in
2021 if c */ c <=/ y then isolate_sqrt (c,b) y
2022 else isolate_sqrt (a,c) y in
2023 fun n -> isolate_sqrt (Int 0,n) n in
2024 let MATCH_pth = MATCH_MP REALCALC_SQRT in
2025 let b_tm = `b:real` in
2026 let PROVE_1_LE_SQRT =
2028 (`&1 <= x ==> &1 <= sqrt(x)`,
2029 DISCH_THEN(fun th ->
2030 ASSUME_TAC(MATCH_MP (REAL_ARITH `&1 <= x ==> &0 <= x`) th) THEN
2032 CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[REAL_NOT_LE] THEN
2034 SUBGOAL_THEN `x = sqrt(x) pow 2` SUBST1_TAC THENL
2035 [CONV_TAC SYM_CONV THEN ASM_REWRITE_TAC[SQRT_POW2];
2036 GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
2037 REWRITE_TAC[POW_2] THEN MATCH_MP_TAC REAL_LT_MUL2 THEN
2038 ASM_SIMP_TAC[SQRT_POS_LE]]) in
2039 let tac = REPEAT(MATCH_MP_TAC pth) THEN CONV_TAC REAL_RAT_LE_CONV in
2040 fun tm -> try prove(tm,tac)
2041 with Failure _ -> failwith "Need root body >= &1" in
2044 num_sqrt(power_num (Int 2) n */ raw_eval fn1 n)
2046 let th1 = MATCH_pth(thm_eval fn2 n) in
2047 let th2 = MP th1 (PROVE_1_LE_SQRT(lhand(concl th1))) in
2048 let th3 = CONV_RULE(funpow 2 LAND_CONV
2049 (funpow 2 RAND_CONV REAL_RAT_REDUCE_CONV)) th2 in
2050 let k = dest_realintconst(rand(rand(lhand(lhand(concl th3))))) in
2051 let th4 = INST [mk_realintconst(num_sqrt k),b_tm] th3 in
2052 MP th4 (EQT_ELIM(REAL_RAT_REDUCE_CONV(lhand(concl th4)))) in
2053 raw_wrap raw_fn,thm_wrap thm_fn in
2055 let rec REALCALC_CONV tm =
2056 try assoc tm (!realcalc_cache) with Failure _ ->
2057 if is_ratconst tm then
2058 let x = rat_of_term tm in
2060 floor_num ((power_num (Int 2) acc) */ x)
2062 let a = floor_num ((power_num (Int 2) acc) */ x) in
2063 let atm = mk_realintconst a in
2064 let rtm = mk_comb(mk_comb(mul_tm,mk_comb(pow2_tm,mk_numeral acc)),tm) in
2065 let btm = mk_comb(abs_tm,mk_comb(mk_comb(sub_tm,atm),rtm)) in
2066 let ftm = mk_comb(mk_comb(lt_tm,btm),one_tm) in
2067 EQT_ELIM(REAL_RAT_REDUCE_CONV ftm) in
2068 raw_wrap raw_fn,thm_wrap thm_fn else
2069 let lop,r = dest_comb tm in
2070 if lop = neg_tm then
2071 let rfn,tfn = REALCALC_CONV r in
2073 minus_num (raw_eval rfn acc)
2075 let th1 = thm_eval tfn acc in
2076 let th2 = MATCH_MP REALCALC_NEG th1 in
2077 try EQ_MP (LAND_CONV(RAND_CONV(LAND_CONV REAL_INT_NEG_CONV)) (concl th2))
2079 with Failure _ -> th2 in
2080 raw_wrap raw_fn,thm_wrap thm_fn
2081 else if lop = abs_tm then
2082 let rfn,tfn = REALCALC_CONV r in
2084 abs_num (raw_eval rfn acc)
2086 let th1 = thm_eval tfn acc in
2087 let th2 = MATCH_MP REALCALC_ABS th1 in
2088 CONV_RULE (LAND_CONV(RAND_CONV(LAND_CONV REAL_INT_ABS_CONV))) th2 in
2089 raw_wrap raw_fn,thm_wrap thm_fn
2090 else if lop = sqrt_tm then
2091 REALCALC_SQRT_CONV(REALCALC_CONV r)
2092 else if lop = inv_tm then
2093 let rfn,tfn = REALCALC_CONV r in
2094 let x0 = raw_eval rfn (Int 0) in
2095 let ax0 = abs_num x0 in
2096 let r = log2(ax0) -/ Int 1 in
2099 let p = find_msd rfn in
2100 let e = acc +/ p +/ Int 1 in
2101 let k = e +/ p in e,k
2103 let k = let k0 = acc +/ Int 1 -/ (Int 2 */ r) in
2104 if k0 </ Int 0 then Int 0 else k0 in
2105 let e = r +/ k in e,k in
2107 let _,k = get_ek(acc) in
2108 let nk2 = power_num (Int 2) (acc +/ k) in
2109 ndiv nk2 (raw_eval rfn k) in
2111 let e,k = get_ek(acc) in
2112 let nk2 = power_num (Int 2) (acc +/ k) in
2113 let th1 = thm_eval tfn k in
2114 let atm = lhand(rand(lhand(concl th1))) in
2115 let a = dest_realintconst atm in
2116 let b = ndiv nk2 a in
2117 let btm = mk_realintconst b in
2118 let etm = mk_numeral e in
2119 let ntm = mk_numeral acc in
2120 let th2 = MATCH_MP REALCALC_INV th1 in
2121 let th3 = INST [btm,b_tm; etm,e_tm; ntm,n_tm] th2 in
2122 let th4 = MP th3 (INTEGER_PROVE(lhand(concl th3))) in
2123 let th5 = MP th4 (INTEGER_PROVE(lhand(concl th4))) in
2124 let th6 = MP th5 (EQT_ELIM(NUM_REDUCE_CONV(lhand(concl th5)))) in
2125 let th7 = MP th6 (EQT_ELIM(REAL_INT_REDUCE_CONV(lhand(concl th6)))) in
2127 (EQT_ELIM(((LAND_CONV (funpow 4 RAND_CONV NUM_ADD_CONV) THENC
2128 REAL_INT_REDUCE_CONV) (lhand(concl th7))))) in
2129 raw_wrap raw_fn,thm_wrap thm_fn
2130 else if lop = exp_tm then
2131 let rfn,tfn = REALCALC_CONV r in
2132 REALCALC_EXP_CONV (rfn,tfn)
2133 else if lop = ln_tm then
2134 let r1,r2 = dest_comb r in
2135 if r1 = add1_tm then
2136 let rfn,tfn = REALCALC_CONV r2 in
2137 REALCALC_LN_CONV (rfn,tfn)
2139 failwith "Can only do logs like ln(&1 + x) for small rational x" else
2140 let op,l = dest_comb lop in
2142 let rfn1,tfn1 = REALCALC_CONV l
2143 and rfn2,tfn2 = REALCALC_CONV r in
2145 let acc' = acc +/ Int 2 in
2146 ndiv (raw_eval rfn1 acc' +/ raw_eval rfn2 acc') (Int 4)
2148 let acc' = acc +/ Int 2 in
2149 let th1 = INST [mk_numeral acc,n_tm] REALCALC_ADD in
2150 let th2 = MATCH_MP th1 (NUM_ADD_CONV (lhand(lhand(concl th1)))) in
2151 let th3 = thm_eval tfn1 acc' in
2152 let th4 = MATCH_MP th2 th3 in
2153 let th5 = thm_eval tfn2 acc' in
2154 let th6 = MATCH_MP th4 th5 in
2155 let n1 = dest_realintconst(lhand(rand(lhand(concl th3))))
2156 and n2 = dest_realintconst(lhand(rand(lhand(concl th5)))) in
2157 let ci = mk_realintconst(ndiv (n1 +/ n2) (Int 4)) in
2158 let th7 = INST [ci,c_tm] th6 in
2159 let th8 = EQT_ELIM(REAL_INT_REDUCE_CONV(lhand(concl th7))) in
2161 raw_wrap raw_fn,thm_wrap thm_fn
2162 else if op = mul_tm then
2163 let rfn1,tfn1 = REALCALC_CONV l
2164 and rfn2,tfn2 = REALCALC_CONV r in
2166 let n' = acc +/ Int 2 in
2167 let r = quo_num n' (Int 2) in
2169 let p = log2(abs_num(raw_eval rfn1 r))
2170 and q = log2(abs_num(raw_eval rfn2 s)) in
2171 let k = q +/ r +/ Int 1
2172 and l = p +/ s +/ Int 1 in
2173 if p =/ Int 0 & q = Int 0 then
2174 if k </ l then k +/ Int 1,l else k,l +/ Int 1
2177 let k,l = get_kl acc in
2178 let m = (k +/ l) -/ acc in
2179 ndiv (raw_eval rfn1 k */ raw_eval rfn2 l) (power_num (Int 2) m) in
2181 let k,l = get_kl acc in
2182 let m = (k +/ l) -/ acc in
2183 let th1a = thm_eval tfn1 k
2184 and th1b = thm_eval tfn2 l in
2185 let a = dest_realintconst(lhand(rand(lhand(concl th1a))))
2186 and b = dest_realintconst(lhand(rand(lhand(concl th1b)))) in
2187 let c = ndiv (a */ b) (power_num (Int 2) m) in
2188 let ntm = mk_numeral acc
2189 and mtm = mk_numeral m
2190 and ctm = mk_realintconst c in
2191 let th1 = MATCH_MP REALCALC_MUL th1a in
2192 let th2 = MATCH_MP th1 th1b in
2193 let th3 = INST [ntm,n_tm; mtm,m_tm; ctm,c_tm] th2 in
2194 let th4 = MP th3 (EQT_ELIM(NUM_REDUCE_CONV(lhand(concl th3)))) in
2195 let th5 = MP th4 (EQT_ELIM(REAL_INT_REDUCE_CONV(lhand(concl th4)))) in
2196 MP th5 (EQT_ELIM(REAL_INT_REDUCE_CONV(lhand(concl th5)))) in
2197 raw_wrap raw_fn,thm_wrap thm_fn
2198 else failwith "No other operators work yet, sorry!" in
2199 REALCALC_CONV,thm_eval,raw_eval,thm_wrap;;
2201 (* ------------------------------------------------------------------------- *)
2202 (* Apply some conversion before doing approximation. *)
2203 (* ------------------------------------------------------------------------- *)
2205 let REALCALC_PRECONV conv tm =
2207 let rfn,tfn = REALCALC_CONV (rand(concl th)) in
2210 let th1 = thm_eval tfn n in
2211 GEN_REWRITE_RULE (LAND_CONV o funpow 3 RAND_CONV) [SYM th] th1);;
2213 (* ------------------------------------------------------------------------- *)
2214 (* Calculate ordering relation between two expressions. *)
2215 (* ------------------------------------------------------------------------- *)
2217 let REALCALC_LT = prove
2218 (`abs(a - &2 pow n * x) < &1 /\ abs(b - &2 pow n * y) < &1
2219 ==> &2 <= abs(a - b) ==> (x < y <=> a < b)`,
2220 REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
2221 EXISTS_TAC `&2 pow n * x < &2 pow n * y` THEN CONJ_TAC THENL
2222 [SIMP_TAC[REAL_LT_LMUL_EQ; REAL_POW_LT; REAL_OF_NUM_LT; ARITH];
2223 POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN REAL_ARITH_TAC]);;
2225 let REALCALC_LE = prove
2226 (`abs(a - &2 pow n * x) < &1 /\ abs(b - &2 pow n * y) < &1
2227 ==> &2 <= abs(a - b) ==> (x <= y <=> a <= b)`,
2228 REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
2229 EXISTS_TAC `&2 pow n * x <= &2 pow n * y` THEN CONJ_TAC THENL
2230 [SIMP_TAC[REAL_LE_LMUL_EQ; REAL_POW_LT; REAL_OF_NUM_LT; ARITH];
2231 POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN REAL_ARITH_TAC]);;
2233 let REALCALC_GT = prove
2234 (`abs(a - &2 pow n * x) < &1 /\ abs(b - &2 pow n * y) < &1
2235 ==> &2 <= abs(a - b) ==> (x > y <=> a > b)`,
2236 ONCE_REWRITE_TAC[CONJ_SYM; REAL_ABS_SUB] THEN
2237 REWRITE_TAC[real_gt; REALCALC_LT]);;
2239 let REALCALC_GE = prove
2240 (`abs(a - &2 pow n * x) < &1 /\ abs(b - &2 pow n * y) < &1
2241 ==> &2 <= abs(a - b) ==> (x >= y <=> a >= b)`,
2242 ONCE_REWRITE_TAC[CONJ_SYM; REAL_ABS_SUB] THEN
2243 REWRITE_TAC[real_ge; REALCALC_LE]);;
2245 let REALCALC_EQ = prove
2246 (`abs(a - &2 pow n * x) < &1 /\ abs(b - &2 pow n * y) < &1
2247 ==> &2 <= abs(a - b) ==> ((x = y) <=> F)`,
2248 ASM_CASES_TAC `x:real = y` THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
2250 let realcalc_rel_conv =
2252 [`(<)`,(</); `(<=)`,(<=/);
2253 `(>)`,(>/); `(>=)`,(>=/);
2254 `(=):real->real->bool`,(=/)] in
2255 let rec find_n rfn1 rfn2 n =
2256 if n >/ Int 1000 then
2257 failwith "realcalc_rel_conv: too close to discriminate" else
2258 if abs_num(raw_eval rfn1 n -/ raw_eval rfn2 n) >=/ Int 4 then n
2259 else find_n rfn1 rfn2 (n +/ Int 1) in
2261 let lop,r = dest_comb tm in
2262 let op,l = dest_comb lop in
2265 with Failure _ -> failwith "realcalc_rel_conv: unknown operator" in
2266 let rfn1,tfn1 = REALCALC_CONV l
2267 and rfn2,tfn2 = REALCALC_CONV r in
2268 let n = find_n rfn1 rfn2 (Int 1) in
2269 pop (raw_eval rfn1 n) (raw_eval rfn2 n);;
2271 let REALCALC_REL_CONV =
2273 [`(<)`,REALCALC_LT; `(<=)`,REALCALC_LE;
2274 `(>)`,REALCALC_GT; `(>=)`,REALCALC_GE;
2275 `(=):real->real->bool`,REALCALC_EQ] in
2276 let rec find_n rfn1 rfn2 n =
2277 if n >/ Int 1000 then
2278 failwith "realcalc_rel_conv: too close to discriminate" else
2279 if abs_num(raw_eval rfn1 n -/ raw_eval rfn2 n) >=/ Int 4 then n
2280 else find_n rfn1 rfn2 (n +/ Int 1) in
2282 let lop,r = dest_comb tm in
2283 let op,l = dest_comb lop in
2284 let pth = try assoc op pths
2285 with Failure _ -> failwith "realcalc_rel_conv: unknown operator" in
2286 let rfn1,tfn1 = REALCALC_CONV l
2287 and rfn2,tfn2 = REALCALC_CONV r in
2288 let n = find_n rfn1 rfn2 (Int 1) in
2289 let th1 = thm_eval tfn1 n
2290 and th2 = thm_eval tfn2 n in
2291 let th3 = MATCH_MP pth (CONJ th1 th2) in
2292 let th4 = MP th3 (EQT_ELIM(REAL_INT_REDUCE_CONV(lhand(concl th3)))) in
2293 CONV_RULE(RAND_CONV REAL_RAT_REDUCE_CONV) th4;;
git://colo12-c703.uibk.ac.at / hl193./.git / blob