1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Author: Alexey Solovyev *)
6 (* ===========================================================================*)
9 (**********************************************)
10 (* Properties of the function arc (arclegnth) *)
11 (**********************************************)
14 (* Some auxiliary results *)
15 flyspeck_needs "trigonometry/trigonometry.hl";;
16 (* lmfun, h0 definitions *)
17 flyspeck_needs "packing/pack_defs.hl";;
20 module Arc_properties = struct
23 let REMOVE_ASSUM = POP_ASSUM (fun th -> ALL_TAC);;
26 (* Some general results *)
28 (* Limit is a local notion *)
29 let REALLIM_ATREAL_LOCAL = prove(`!f g x y. (g ---> y) (atreal x) /\
30 (?s. real_open s /\ x IN s /\ (!y. y IN s ==> f y = g y))
31 ==> (f ---> y) (atreal x)`,
32 REWRITE_TAC[REALLIM_ATREAL; real_open] THEN
34 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
35 FIRST_X_ASSUM (MP_TAC o SPEC `x:real`) THEN
36 ASM_REWRITE_TAC[] THEN
37 STRIP_TAC THEN POP_ASSUM MP_TAC THEN
38 FIRST_X_ASSUM (MP_TAC o SPEC `e:real`) THEN
40 FIRST_X_ASSUM (MP_TAC o check (is_imp o concl)) THEN
41 ASM_REWRITE_TAC[] THEN
43 EXISTS_TAC `min e' d` THEN
46 REWRITE_TAC[real_min] THEN
47 COND_CASES_TAC THEN ASM_REWRITE_TAC[];
52 SUBGOAL_THEN `(f:real->real) x' = (g:real->real) x'` (fun th -> REWRITE_TAC[th]) THENL
54 FIRST_X_ASSUM MATCH_MP_TAC THEN
55 FIRST_X_ASSUM MATCH_MP_TAC THEN
56 MATCH_MP_TAC REAL_LTE_TRANS THEN
57 EXISTS_TAC `min e' d` THEN
58 ASM_REWRITE_TAC[REAL_MIN_MIN];
61 FIRST_X_ASSUM MATCH_MP_TAC THEN
62 ASM_REWRITE_TAC[] THEN
63 MATCH_MP_TAC REAL_LTE_TRANS THEN
64 EXISTS_TAC `min e' d` THEN
65 ASM_REWRITE_TAC[REAL_MIN_MIN]);;
70 (* Derivative is a local notion *)
71 let HAS_REAL_DERIVATIVE_LOCAL = prove(`!f g x g'x. (g has_real_derivative g'x) (atreal x)
72 /\ (?s. real_open s /\ x IN s /\ (!y. y IN s ==> f y = g y))
73 ==> (f has_real_derivative g'x) (atreal x)`,
74 REWRITE_TAC[HAS_REAL_DERIVATIVE_ATREAL] THEN
76 MATCH_MP_TAC REALLIM_ATREAL_LOCAL THEN
77 EXISTS_TAC `\y. (g y - (g:real->real) x) / (y - x)` THEN
78 ASM_REWRITE_TAC[] THEN
79 EXISTS_TAC `s:real->bool` THEN
80 ASM_REWRITE_TAC[] THEN
82 FIRST_ASSUM (MP_TAC o SPEC `x:real`) THEN
83 FIRST_X_ASSUM (MP_TAC o SPEC `y:real`) THEN
89 let REAL_LT_ONE_LDIV = prove(`!a b. &0 < b /\ a < b ==> a / b < &1`,
91 ASM_SIMP_TAC[REAL_FIELD `&0 < b ==> (a / b < &1 <=> &0 < (b - a) / b)`] THEN
92 ASM_SIMP_TAC[Trigonometry2.REAL_LT_DIV_0] THEN
93 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
97 (****************************************************************)
100 (* The derivative of arc (x, b, 2) *)
102 let der0 = REAL_DIFF_CONV `((\x. acs ((x * x + b * b - &2 * &2) / (&2 * x * b))) has_real_derivative f) (atreal x)` in
103 let der1 = REWRITE_RULE [REAL_ADD_RID; REAL_SUB_RZERO; REAL_MUL_RID; REAL_MUL_LID] der0 in
104 let der2 = REWRITE_RULE [IMP_IMP] (DISCH_ALL der1) in
105 let der_tm = (rand o rator) (concl der1) in
106 let concl0 = list_mk_comb (`(has_real_derivative)`, [`\x. arclength x b (&2)`; der_tm; `atreal x within real_interval [&2,#2.52]`]) in
107 let goal0 = list_mk_forall ([`x:real`; `b:real`], (mk_imp (`(&2 <= x /\ x <= #2.52) /\ (&2 <= b /\ b <= #2.52)`, concl0))) in
109 REPEAT STRIP_TAC THEN
110 MATCH_MP_TAC HAS_REAL_DERIVATIVE_ATREAL_WITHIN THEN
111 MATCH_MP_TAC HAS_REAL_DERIVATIVE_LOCAL THEN
112 EXISTS_TAC `(\x. acs ((x * x + b * b - &2 * &2) / (&2 * x * b)))` THEN
115 MATCH_MP_TAC der2 THEN
118 MATCH_MP_TAC (REAL_ARITH `&0 <= a /\ a < &1 ==> abs a < &1`) THEN
121 MATCH_MP_TAC REAL_LE_DIV THEN
122 SUBGOAL_THEN `&2 * &2 <= x * x /\ &2 * &2 <= b * b` ASSUME_TAC THENL
124 REWRITE_TAC[GSYM REAL_POW_2] THEN
125 CONJ_TAC THEN MATCH_MP_TAC REAL_POW_LE2 THEN ASM_REWRITE_TAC[REAL_ARITH `&0 <= &2`];
130 POP_ASSUM MP_TAC THEN
132 MATCH_MP_TAC REAL_LE_MUL THEN
133 REWRITE_TAC[REAL_ARITH `&0 <= &2`] THEN
134 MATCH_MP_TAC REAL_LE_MUL THEN
135 ASM_SIMP_TAC[REAL_ARITH `&2 <= x ==> &0 <= x`]
140 MATCH_MP_TAC REAL_LT_ONE_LDIV THEN
143 MATCH_MP_TAC REAL_LT_MUL THEN
144 REWRITE_TAC[REAL_ARITH `&0 < &2`] THEN
145 MATCH_MP_TAC REAL_LT_MUL THEN
146 ASM_SIMP_TAC[REAL_ARITH `&2 <= x ==> &0 < x`];
150 REWRITE_TAC[REAL_ARITH `x * x + b * b - &2 * &2 < &2 * x * b <=> (x - b) * (x - b) < &2 * &2`] THEN
151 REWRITE_TAC[GSYM REAL_POW_2] THEN
152 REWRITE_TAC[GSYM REAL_LT_SQUARE_ABS] THEN
153 REPEAT (POP_ASSUM MP_TAC) THEN
157 REWRITE_TAC[Trigonometry2.NOT_MUL_EQ0_EQ] THEN
158 REPEAT (POP_ASSUM MP_TAC) THEN
163 EXISTS_TAC `real_interval (#1.9,#2.6)` THEN
164 REWRITE_TAC[REAL_OPEN_REAL_INTERVAL; IN_REAL_INTERVAL] THEN
167 REPEAT (POP_ASSUM MP_TAC) THEN
171 REPEAT STRIP_TAC THEN
172 MATCH_MP_TAC Trigonometry1.ACS_ARCLENGTH THEN
173 REPEAT (POP_ASSUM MP_TAC) THEN
178 (**************************************************************)
182 (* Numerical approximations for cos and acos *)
185 let COS_EQ_NEG_SIN = prove(`!x. cos (x + pi / &2) = --sin x`,
186 REWRITE_TAC[COS_SIN; REAL_ARITH `a - (b + a) = --b`; SIN_NEG]);;
191 let COS_DERIVATIVES = prove(`!x n. ((\x. cos (x + &n * pi / &2)) has_real_derivative cos (x + &(n + 1) * pi / &2)) (atreal x)`,
192 REPEAT GEN_TAC THEN REWRITE_TAC[] THEN
193 MP_TAC (REAL_DIFF_CONV `((\x. cos (x + &n * pi / &2)) has_real_derivative f) (atreal x)`) THEN
194 SUBGOAL_THEN `(&1 + &0) * --sin (x + &n * pi / &2) = cos (x + &(n + 1) * pi / &2)` (fun th -> REWRITE_TAC[th]) THEN
195 REWRITE_TAC[REAL_ARITH `(&1 + &0) * --a = --a`] THEN
196 REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN
197 REWRITE_TAC[REAL_ARITH `x + (a + &1) * t = (x + a * t) + t`] THEN
198 REWRITE_TAC[COS_EQ_NEG_SIN]);;
203 let REAL_TAYLOR_COS_RAW = prove(`!x n. abs (cos x - sum (0..n) (\k. if (EVEN k) then ((-- &1) pow (k DIV 2) * x pow k) / &(FACT k) else &0)) <=
204 abs x pow (n + 1) / &(FACT (n + 1))`,
206 MP_TAC (SPECL [`(\i x. cos (x + &i * pi / &2))`; `n:num`; `UNIV:real->bool`; `&1`] REAL_TAYLOR) THEN
209 REWRITE_TAC[is_realinterval; IN_UNIV; WITHINREAL_UNIV; COS_DERIVATIVES; COS_BOUND];
212 REWRITE_TAC[IN_UNIV] THEN
213 DISCH_THEN (MP_TAC o SPECL [`&0`; `x:real`]) THEN
214 REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_RID; REAL_ADD_LID; REAL_SUB_RZERO; REAL_MUL_LID] THEN
215 SUBGOAL_THEN `!i. cos (&i * pi / &2) * x pow i / &(FACT i) = if EVEN i then (-- &1 pow (i DIV 2) * x pow i) / &(FACT i) else &0` (fun th -> SIMP_TAC[th]) THEN
217 ASM_CASES_TAC `EVEN i` THEN ASM_REWRITE_TAC[] THENL
219 POP_ASSUM MP_TAC THEN
220 REWRITE_TAC[EVEN_EXISTS] THEN
221 STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
222 SUBGOAL_THEN `(2 * m) DIV 2 = m` (fun th -> REWRITE_TAC[th]) THENL
224 MATCH_MP_TAC DIV_MULT THEN
228 REWRITE_TAC[GSYM REAL_OF_NUM_MUL] THEN
229 REWRITE_TAC[REAL_ARITH `(&2 * a) * b / &2 = a * b`] THEN
230 REWRITE_TAC[COS_NPI] THEN
234 SUBGOAL_THEN `cos (&i * pi / &2) = &0` (fun th -> REWRITE_TAC[th]) THENL
236 REWRITE_TAC[COS_ZERO] THEN
237 DISJ1_TAC THEN EXISTS_TAC `i:num` THEN
241 REWRITE_TAC[REAL_MUL_LZERO]);;
244 let SUM_PAIR_0 = prove(`!f n. sum (0..2 * n + 1) f = sum(0..n) (\i. f (2 * i) + f (2 * i + 1))`,
246 MP_TAC (SPECL [`f:num->real`; `0`; `n:num`] SUM_PAIR) THEN
247 REWRITE_TAC[ARITH_RULE `2 * 0 = 0`]);;
250 let REAL_TAYLOR_COS = prove(`!x n. abs (cos x - sum (0..n) (\i. (-- &1) pow i * x pow (2 * i) / &(FACT (2 * i)))) <= abs x pow (2*n + 2) / &(FACT (2*n + 2))`,
252 MP_TAC (SPECL [`x:real`; `2 * n + 1`] REAL_TAYLOR_COS_RAW) THEN
253 REWRITE_TAC[SUM_PAIR_0; EVEN_DOUBLE; ARITH_RULE `(2 * n + 1) + 1 = 2 *n + 2`] THEN
254 SUBGOAL_THEN `!i. ~(EVEN (2 * i + 1))` MP_TAC THENL
256 GEN_TAC THEN REWRITE_TAC[NOT_EVEN] THEN
257 REWRITE_TAC[ARITH_ODD; ODD_ADD; ODD_MULT];
260 DISCH_THEN (fun th -> SIMP_TAC[th]) THEN
261 SUBGOAL_THEN `!i. (2 * i) DIV 2 = i` MP_TAC THENL
264 MATCH_MP_TAC DIV_MULT THEN
268 DISCH_THEN (fun th -> REWRITE_TAC[th; REAL_ADD_RID]) THEN
269 REWRITE_TAC[REAL_ARITH `(a * b) / c = a * b / c`]);;
277 let tm = list_mk_comb (`sum:(num->bool)->(num->real)->real`, [mk_comb (`(..) 0`, mk_small_numeral n); `f:num->real`]) in
278 let suc_th = REWRITE_RULE[EQ_CLAUSES] (REWRITE_CONV[ARITH] (mk_eq (mk_small_numeral n, mk_comb (`SUC`, mk_small_numeral (n - 1))))) in
279 let th1 = REWRITE_CONV[suc_th] tm in
280 REWRITE_RULE[SUM_CLAUSES_NUMSEG; ARITH] th1 in
281 let rec rewriter th n =
283 rewriter (REWRITE_RULE[SUM_lemma n; GSYM REAL_ADD_ASSOC] th) (n - 1)
286 GEN_ALL (rewriter (SUM_lemma n) (n - 1));;
290 (* Evaluates cos at a given point using n terms from the cosine Taylor series *)
292 let th1 = (SPECL [x; mk_small_numeral n] REAL_TAYLOR_COS) in
293 let th2 = REWRITE_RULE[gen_sum_thm n] th1 in
294 let th4 = CONV_RULE (NUM_REDUCE_CONV) th2 in
295 let th5 = CONV_RULE (DEPTH_CONV REAL_INT_POW_CONV) th4 in
296 CONV_RULE (REAL_RAT_REDUCE_CONV) th5;;
301 (************************************************************************)
305 (***************************)
306 (* Properties of arc a b c *)
307 (***************************)
310 (* arc a b 2 <= arc a b c *)
311 let arc_lemma1 = prove(`!a b c. &2 <= a /\ a <= #2.52 /\
312 &2 <= b /\ b <= #2.52 /\
313 &2 <= c /\ c <= #2.52
314 ==> arclength a b (&2) <= arclength a b c`,
315 REPEAT STRIP_TAC THEN
316 SUBGOAL_THEN `arclength a b (&2) = acs ((a * a + b * b - &2 * &2) / (&2 * a * b))` (fun th -> REWRITE_TAC[th]) THENL
318 MATCH_MP_TAC Trigonometry1.ACS_ARCLENGTH THEN
319 REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
322 SUBGOAL_THEN `arclength a b c = acs ((a * a + b * b - c * c) / (&2 * a * b))` (fun th -> REWRITE_TAC[th]) THENL
324 MATCH_MP_TAC Trigonometry1.ACS_ARCLENGTH THEN
325 REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
328 MATCH_MP_TAC ACS_MONO_LE THEN
330 ABBREV_TAC `a2:real = a * a` THEN
331 ABBREV_TAC `b2:real = b * b` THEN
332 ABBREV_TAC `c2:real = c * c` THEN
333 ABBREV_TAC `ab2:real = &2 * a * b` THEN
335 SUBGOAL_THEN `&4 <= a2 /\ a2 <= #6.3504 /\ &4 <= b2 /\ b2 <= #6.3504 /\ &4 <= c2 /\ c2 <= #6.3504` ASSUME_TAC THENL
338 REPLICATE_TAC 3 (POP_ASSUM (fun th -> REWRITE_TAC[SYM th])) THEN
339 REWRITE_TAC[REAL_ARITH `&4 = &2 * &2`; REAL_ARITH `#6.3504 = #2.52 * #2.52`] THEN
340 REWRITE_TAC[GSYM REAL_POW_2; GSYM REAL_LE_SQUARE_ABS] THEN
341 REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC;
345 SUBGOAL_THEN `&8 <= ab2 /\ ab2 <= #12.7008` ASSUME_TAC THENL
347 EXPAND_TAC "ab2" THEN
348 REWRITE_TAC[REAL_ARITH `&8 = &2 * &2 * &2`; REAL_ARITH `#12.7008 = &2 * #2.52 * #2.52`] THEN
349 CONJ_TAC THEN MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ARITH `&0 <= &2`] THENL
351 MATCH_MP_TAC REAL_LE_MUL2 THEN
352 ASM_REWRITE_TAC[REAL_ARITH `&0 <= &2`];
353 MATCH_MP_TAC REAL_LE_MUL2 THEN
354 ASM_SIMP_TAC[REAL_ARITH `&2 <= a ==> &0 <= a`]
359 SUBGOAL_THEN `&0 < ab2` ASSUME_TAC THENL
361 MATCH_MP_TAC REAL_LTE_TRANS THEN
362 EXISTS_TAC `&8` THEN ASM_REWRITE_TAC[REAL_ARITH `&0 < &8`];
366 REPEAT CONJ_TAC THENL
368 MATCH_MP_TAC REAL_LE_TRANS THEN
370 REWRITE_TAC[REAL_ARITH `-- &1 <= &0`] THEN
371 MATCH_MP_TAC REAL_LE_DIV THEN
372 REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN
375 ASM_SIMP_TAC[REAL_LE_DIV2_EQ] THEN
376 REMOVE_ASSUM THEN REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
379 MATCH_MP_TAC Trigonometry2.REAL_LE_LDIV THEN
380 ASM_REWRITE_TAC[] THEN
382 MAP_EVERY EXPAND_TAC ["a2"; "b2"; "ab2"] THEN
383 ONCE_REWRITE_TAC[REAL_ARITH `a + b - c <= d <=> a + b - d <= c`] THEN
384 REWRITE_TAC[REAL_RING `a * a + b * b - &2 * a * b = (a - b) * (a - b)`] THEN
385 REWRITE_TAC[GSYM REAL_POW_2; GSYM REAL_LE_SQUARE_ABS] THEN
386 REPLICATE_TAC 9 REMOVE_ASSUM THEN
387 REPEAT (POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC
391 (*************************************************************)
394 (* arc a b c = arc b a c *)
395 let ups_x_sym = prove(`!a b c. ups_x a b c = ups_x b a c`,
396 REWRITE_TAC[Sphere.ups_x] THEN REAL_ARITH_TAC);;
399 let arc_sym = prove(`!a b c. arclength a b c = arclength b a c`,
400 REWRITE_TAC[Sphere.arclength; ups_x_sym] THEN
401 REWRITE_TAC[REAL_ARITH `c - a - b = c - b - a`]);;
405 (*************************************************************)
407 (* arc x b 2 is concave *)
410 (* A corrected version of the theorem from realanalysis.ml *)
411 let REAL_CONVEX_ON_SECOND_DERIVATIVE = prove
413 is_realinterval s /\ ~(?a. s = {a}) /\
414 (!x. x IN s ==> (f has_real_derivative f'(x)) (atreal x within s)) /\
415 (!x. x IN s ==> (f' has_real_derivative f''(x)) (atreal x within s))
416 ==> (f real_convex_on s <=> !x. x IN s ==> &0 <= f''(x))`,
417 REPEAT STRIP_TAC THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC
418 `!x y. x IN s /\ y IN s /\ x <= y ==> (f':real->real)(x) <= f'(y)` THEN
420 [MATCH_MP_TAC REAL_CONVEX_ON_DERIVATIVE_INCREASING;
421 CONV_TAC SYM_CONV THEN MATCH_MP_TAC HAS_REAL_DERIVATIVE_INCREASING] THEN
426 (* arc is concave (-arc is convex) *)
428 let arc_concave = prove(`!b. &2 <= b /\ b <= #2.52 ==> (\x. -- arclength x b (&2)) real_convex_on (real_interval [&2, #2.52])`,
429 REPEAT STRIP_TAC THEN
430 MP_TAC (SPECL [`\x. --arclength x b (&2)`;
431 `\x. (x * x - (b * b - &4)) / x * inv (sqrt (&4 * (x * x) * (b * b) - (x * x + b * b - &4) pow 2))`;
432 `\x. inv (sqrt (&4 * (x * x) * (b * b) - (x * x + b * b - &4) pow 2)) * ((x * x + (b * b - &4)) / (x * x) - ((&2 * b * b - &2 * x * x + &8) * (x * x - (b * b - &4))) / (&4 * (x * x) * (b * b) - (x * x + b * b - &4) pow 2))`;
433 `real_interval [&2,#2.52]`
434 ] REAL_CONVEX_ON_SECOND_DERIVATIVE) THEN
437 REWRITE_TAC[IS_REALINTERVAL_INTERVAL] THEN
440 REWRITE_TAC[NOT_EXISTS_THM] THEN GEN_TAC THEN
442 SUBGOAL_THEN `&2 = a /\ #2.52 = a` MP_TAC THENL
444 REWRITE_TAC[GSYM IN_SING] THEN
445 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
446 REWRITE_TAC[IN_REAL_INTERVAL] THEN
456 REWRITE_TAC[IN_REAL_INTERVAL] THEN
457 GEN_TAC THEN DISCH_TAC THEN
458 REWRITE_TAC[REAL_ARITH `a * inv(b) = --(a * --inv(b))`] THEN
459 MATCH_MP_TAC HAS_REAL_DERIVATIVE_NEG THEN
460 MP_TAC (SPEC_ALL arc_derivative) THEN
461 ASM_REWRITE_TAC[] THEN
462 REWRITE_TAC[REAL_ARITH `(x + x) * &2 * x * b - (x * x + b * b - &2 * &2) * &2 * b = &2 * b * (x * x - (b * b - &4))`] THEN
463 SUBGOAL_THEN `&0 < &2 * x * b` ASSUME_TAC THENL
465 MATCH_MP_TAC REAL_LT_MUL THEN
466 REWRITE_TAC[REAL_ARITH `&0 < &2`] THEN
467 MATCH_MP_TAC REAL_LT_MUL THEN
468 ASM_SIMP_TAC[REAL_ARITH `&2 <= x ==> &0 < x`];
472 SUBGOAL_THEN `(&2 * b * (x * x - (b * b - &4))) / (&2 * x * b) pow 2 = (x * x - (b * b - &4)) / x * inv(&2 * x * b)` (fun th -> REWRITE_TAC[th]) THENL
474 POP_ASSUM MP_TAC THEN
479 SUBGOAL_THEN `!a b c. (c * inv(a)) * --inv(b) = c * --inv(a * b)` (fun th -> ONCE_REWRITE_TAC[th]) THENL
481 REWRITE_TAC[REAL_INV_MUL] THEN
486 SUBGOAL_THEN `&0 <= &1 - ((x * x + b * b - &2 * &2) / (&2 * x * b)) pow 2` ASSUME_TAC THENL
488 REWRITE_TAC[REAL_POW_DIV] THEN
489 REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`] THEN
490 MATCH_MP_TAC Trigonometry2.REAL_LE_LDIV THEN
493 REWRITE_TAC[REAL_POW_2] THEN
494 MATCH_MP_TAC REAL_LT_MUL THEN
498 MATCH_MP_TAC REAL_POW_LE2 THEN
501 SUBGOAL_THEN `&2 * &2 <= x * x /\ &2 * &2 <= b * b` MP_TAC THENL
503 REWRITE_TAC[GSYM REAL_POW_2] THEN
504 REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS] THEN
505 REPEAT (POP_ASSUM MP_TAC) THEN
512 REWRITE_TAC[REAL_ARITH `x * x + b * b - &2 * &2 <= &2 * x * b <=> (x - b) pow 2 <= &2 pow 2`] THEN
513 REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS] THEN
514 REPEAT (POP_ASSUM MP_TAC) THEN
519 FIRST_ASSUM (ASSUME_TAC o MATCH_MP REAL_LT_IMP_LE) THEN
520 ASM_SIMP_TAC[Trigonometry1.SQRT_MUL_L] THEN
521 SUBGOAL_THEN `(&2 * x * b) pow 2 * (&1 - ((x * x + b * b - &2 * &2) / (&2 * x * b)) pow 2) = &4 * (x * x) * b * b - (x * x + b * b - &4) pow 2` MP_TAC THENL
523 REWRITE_TAC[REAL_POW_DIV; REAL_ARITH `a * (&1 - c) = a - a * c`] THEN
524 FIRST_ASSUM (ASSUME_TAC o MATCH_MP REAL_POW_LT) THEN
525 ASM_SIMP_TAC[REAL_FIELD `&0 < a ==> a * c / a = c`] THEN
529 DISCH_THEN (fun th -> REWRITE_TAC[th]);
533 REWRITE_TAC[IN_REAL_INTERVAL] THEN
534 GEN_TAC THEN DISCH_TAC THEN
537 SUBGOAL_THEN `&0 < &4 * (x * x) * b * b - (x * x + b * b - &4) pow 2` ASSUME_TAC THENL
539 REWRITE_TAC[REAL_RING `&4 * (x * x) * b * b - (x * x + b * b - &4) pow 2 = (&2 pow 2 - (x - b) pow 2) * ((x + b) pow 2 - &2 pow 2)`] THEN
540 MATCH_MP_TAC REAL_LT_MUL THEN
541 ONCE_REWRITE_TAC[REAL_ARITH `&0 < a - b <=> b < a`] THEN
542 REWRITE_TAC[GSYM REAL_LT_SQUARE_ABS] THEN
543 REPEAT (POP_ASSUM MP_TAC) THEN
551 FIRST_X_ASSUM (ASSUME_TAC o MATCH_MP SQRT_POS_LT) THEN
552 ASM_SIMP_TAC[REAL_POS_NZ; REAL_ARITH `&2 <= x ==> ~(x = &0)`];
556 REWRITE_TAC[REAL_MUL_LID; REAL_MUL_RID; REAL_ADD_RID; ARITH_RULE `2 - 1 = 1`; REAL_POW_1; REAL_SUB_RZERO] THEN
557 REWRITE_TAC[REAL_INV_MUL] THEN
558 FIRST_ASSUM (ASSUME_TAC o MATCH_MP REAL_LT_IMP_LE) THEN
559 ASM_SIMP_TAC[SQRT_POW_2] THEN
560 REPEAT (POP_ASSUM MP_TAC) THEN
565 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
566 REWRITE_TAC[IN_REAL_INTERVAL] THEN
567 GEN_TAC THEN DISCH_TAC THEN
568 MATCH_MP_TAC REAL_LE_MUL THEN
570 SUBGOAL_THEN `&0 < &4 * (x * x) * b * b - (x * x + b * b - &4) pow 2` ASSUME_TAC THENL
572 REWRITE_TAC[REAL_RING `&4 * (x * x) * b * b - (x * x + b * b - &4) pow 2 = (&2 pow 2 - (x - b) pow 2) * ((x + b) pow 2 - &2 pow 2)`] THEN
573 MATCH_MP_TAC REAL_LT_MUL THEN
574 ONCE_REWRITE_TAC[REAL_ARITH `&0 < a - b <=> b < a`] THEN
575 REWRITE_TAC[GSYM REAL_LT_SQUARE_ABS] THEN
576 REPEAT (POP_ASSUM MP_TAC) THEN
583 MATCH_MP_TAC REAL_LE_INV THEN
584 MATCH_MP_TAC SQRT_POS_LE THEN
585 MATCH_MP_TAC REAL_LT_IMP_LE THEN
590 ABBREV_TAC `t:real = x * x` THEN
591 ABBREV_TAC `u:real = b * b` THEN
593 REWRITE_TAC[REAL_ARITH `&0 <= a - b <=> b <= a`] THEN
594 SUBGOAL_THEN `&0 < t` ASSUME_TAC THENL
597 MATCH_MP_TAC REAL_LT_MUL THEN
598 ASM_SIMP_TAC[REAL_ARITH `&2 <= x ==> &0 < x`];
602 ASM_SIMP_TAC[RAT_LEMMA4] THEN
603 ONCE_REWRITE_TAC[REAL_ARITH `a <= b <=> &0 <= b - a`] THEN
605 ABBREV_TAC `f = \t. (t + u - &4) * (&4 * t * u - (t + u - &4) pow 2) - ((&2 * u - &2 * t + &8) * (t - (u - &4))) * t` THEN
606 FIRST_ASSUM (MP_TAC o (fun th -> AP_THM th `t:real`)) THEN
608 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
609 ABBREV_TAC `f' = \t. &3 * (-- &2 * t * u + t * (t + &8) + u pow 2) + &8 * u - &80` THEN
610 ABBREV_TAC `f'' = \t. &6 * (t - u + &4)` THEN
612 SUBGOAL_THEN `&4 <= t /\ &4 <= u /\ t <= #6.3504 /\ u <= #6.3504` ASSUME_TAC THENL
614 REWRITE_TAC[REAL_ARITH `&4 = &2 * &2`; REAL_ARITH `#6.3504 = #2.52 * #2.52`] THEN
615 EXPAND_TAC "t" THEN EXPAND_TAC "u" THEN
616 REWRITE_TAC[GSYM REAL_POW_2] THEN
617 REWRITE_TAC[GSYM REAL_LE_SQUARE_ABS] THEN
618 FIRST_X_ASSUM (MP_TAC o check (is_conj o concl)) THEN
619 REPEAT (FIRST_X_ASSUM (MP_TAC o check (is_binop `(<=):real->real->bool` o concl))) THEN
623 SUBGOAL_THEN `&0 <= t /\ &0 <= u` ASSUME_TAC THENL
625 ASM_SIMP_TAC[REAL_ARITH `&4 <= t ==> &0 <= t`];
629 MATCH_MP_TAC REAL_LE_TRANS THEN
630 EXISTS_TAC `(f:real->real) (&4)` THEN
634 REWRITE_TAC[REAL_ARITH `&4 + u - &4 = u`] THEN
635 REWRITE_TAC[REAL_ARITH `a - &2 * &4 + &8 = a`] THEN
636 REWRITE_TAC[REAL_ARITH `u * (&4 * &4 * u - u pow 2) - ((&2 * u) * (&4 - (u - &4))) * &4 = u * (&24 * u - u * u - &64)`] THEN
637 MATCH_MP_TAC REAL_LE_MUL THEN
638 ASM_REWRITE_TAC[] THEN
639 ABBREV_TAC `g = \u. &24 * u - u * u - &64` THEN
640 FIRST_ASSUM (MP_TAC o (fun th -> AP_THM th `u:real`)) THEN
641 BETA_TAC THEN DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
642 MATCH_MP_TAC REAL_LE_TRANS THEN
643 EXISTS_TAC `(g:real->real) (&4)` THEN
650 MATCH_MP_TAC HAS_REAL_DERIVATIVE_INCREASING_IMP THEN
651 EXISTS_TAC `\u. &24 - &2 * u` THEN
652 EXISTS_TAC `real_interval [&4,#6.3504]` THEN
653 REWRITE_TAC[IS_REALINTERVAL_INTERVAL] THEN
656 REPEAT STRIP_TAC THEN
662 ASM_REWRITE_TAC[IN_REAL_INTERVAL; REAL_ARITH `&4 <= &4 /\ &4 <= #6.3504`] THEN
667 MATCH_MP_TAC HAS_REAL_DERIVATIVE_INCREASING_IMP THEN
668 MAP_EVERY EXISTS_TAC [`f':real->real`; `real_interval [&4,#6.3504]`] THEN
669 ASM_REWRITE_TAC[IN_REAL_INTERVAL; REAL_ARITH `&4 <= &4 /\ &4 <= #6.3504`] THEN
670 REWRITE_TAC[IS_REALINTERVAL_INTERVAL] THEN
673 REPEAT STRIP_TAC THEN
674 EXPAND_TAC "f" THEN EXPAND_TAC "f'" THEN
676 REWRITE_TAC[ARITH_RULE `2 - 1 = 1`] THEN
681 X_GEN_TAC `y:real` THEN DISCH_TAC THEN
682 MATCH_MP_TAC REAL_LE_TRANS THEN
683 EXISTS_TAC `(f':real->real) (&4)` THEN
687 REWRITE_TAC[REAL_ARITH `&3 * (-- &2 * &4 * u + &4 * (&4 + &8) + u pow 2) + &8 * u - &80 = &3 * (u - &8 / &3) pow 2 + &128 / &3`] THEN
688 MATCH_MP_TAC REAL_LE_ADD THEN
691 MATCH_MP_TAC REAL_LE_MUL THEN
692 REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE] THEN
699 MATCH_MP_TAC HAS_REAL_DERIVATIVE_INCREASING_IMP THEN
700 MAP_EVERY EXISTS_TAC [`f'':real->real`; `real_interval [&4,#6.3504]`] THEN
701 ASM_REWRITE_TAC[IN_REAL_INTERVAL; REAL_ARITH `&4 <= &4 /\ &4 <= #6.3504`] THEN
702 REWRITE_TAC[IS_REALINTERVAL_INTERVAL] THEN
705 REPEAT STRIP_TAC THEN
706 EXPAND_TAC "f'" THEN EXPAND_TAC "f''" THEN
712 EXPAND_TAC "f''" THEN
713 REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN
718 (* arc x b 2 >= arc (2 h0) b 2 + lmfun(x / 2) * (arc 2 b 2 - arc (2 h0) b 2) *)
720 let arc_lemma3 = prove(`!x b. (&2 <= x /\ x <= #2.52) /\ (&2 <= b /\ b <= #2.52)
721 ==> arclength x b (&2) >=
722 arclength (#2.52) b (&2) +
723 lmfun(x / &2) * (arclength (&2) b (&2) - arclength (#2.52) b (&2))`,
724 REPEAT STRIP_TAC THEN
725 MP_TAC (SPEC_ALL arc_concave) THEN
726 ASM_REWRITE_TAC[real_convex_on] THEN
727 DISCH_THEN (MP_TAC o SPECL [`&2`; `#2.52`; `lmfun (x / &2)`; `&1 - lmfun (x / &2)`]) THEN
728 REWRITE_TAC[IN_REAL_INTERVAL; REAL_LE_REFL; REAL_ARITH `&2 <= #2.52`; REAL_ARITH `a + &1 - a = &1`] THEN
729 SUBGOAL_THEN `&0 <= lmfun (x / &2) /\ &0 <= &1 - lmfun (x / &2)` ASSUME_TAC THENL
731 REWRITE_TAC[Pack_defs.lmfun; Pack_defs.h0] THEN
732 REPEAT (POP_ASSUM MP_TAC) THEN
736 ASM_REWRITE_TAC[] THEN
737 SUBGOAL_THEN `lmfun (x / &2) * &2 + (&1 - lmfun (x / &2)) * #2.52 = x` (fun th -> REWRITE_TAC[th]) THENL
739 REWRITE_TAC[Pack_defs.lmfun; Pack_defs.h0] THEN
740 REPEAT (POP_ASSUM MP_TAC) THEN
749 (********************************************************)
754 let ABS_LE_BOUNDS = prove(`!x a e. abs (x - a) <= e <=> a - e <= x /\ x <= a + e`,
760 (* Estimates for the proof of arc_lemma4 *)
762 let estimate0 = prove(`arclength (&2) #2.52 (&2) - arclength #2.52 #2.52 (&2) >= #0.073`,
763 SUBGOAL_THEN `arclength #2.52 #2.52 (&2) = acs ((#2.52 * #2.52 + #2.52 * #2.52 - (&2) * (&2)) / (&2 * #2.52 * #2.52))` (fun th -> REWRITE_TAC[th]) THENL
765 MATCH_MP_TAC Trigonometry1.ACS_ARCLENGTH THEN
769 SUBGOAL_THEN `arclength (&2) #2.52 (&2) = acs (((&2) * (&2) + #2.52 * #2.52 - (&2) * (&2)) / (&2 * (&2) * #2.52))` (fun th -> REWRITE_TAC[th]) THENL
771 MATCH_MP_TAC Trigonometry1.ACS_ARCLENGTH THEN
775 CONV_TAC REAL_RAT_REDUCE_CONV THEN
776 REWRITE_TAC[REAL_ARITH `#0.073 = #0.8892 - #0.8162`] THEN
777 MATCH_MP_TAC (REAL_ARITH `a >= b /\ c <= d ==> a - c >= b - d`) THEN
780 SUBGOAL_THEN `#0.8892 = acs (cos #0.8892)` (fun th -> ONCE_REWRITE_TAC[th]) THENL
782 MATCH_MP_TAC (GSYM ACS_COS) THEN
783 MP_TAC PI_APPROX_32 THEN
787 REWRITE_TAC[real_ge] THEN
788 MATCH_MP_TAC ACS_MONO_LE THEN
789 REWRITE_TAC[COS_BOUNDS] THEN
792 CONV_TAC REAL_RAT_LE_CONV;
793 MP_TAC (CONJUNCT1 (REWRITE_RULE[ABS_LE_BOUNDS] (cos_eval `#0.8892` 2))) THEN
797 SUBGOAL_THEN `#0.8162 = acs (cos #0.8162)` (fun th -> ONCE_REWRITE_TAC[th]) THENL
799 MATCH_MP_TAC (GSYM ACS_COS) THEN
800 MP_TAC PI_APPROX_32 THEN
804 MATCH_MP_TAC ACS_MONO_LE THEN
805 REWRITE_TAC[COS_BOUNDS] THEN
808 MP_TAC ((CONJUNCT2 o REWRITE_RULE[ABS_LE_BOUNDS]) (cos_eval `#0.8162` 3)) THEN
810 CONV_TAC REAL_RAT_LE_CONV
815 let estimate1 = prove(`!x. &2 <= x /\ x <= #2.52 ==> &1 / &4 * --inv (sqrt (&1 - (x / &4) pow 2)) <= -- #0.28`,
816 REPEAT STRIP_TAC THEN
817 REWRITE_TAC[REAL_ARITH `&1 / &4 * --a <= --b <=> &4 * b <= a`] THEN
818 ONCE_REWRITE_TAC[REAL_ARITH `&4 * #0.28 = inv (inv (&4 * #0.28))`] THEN
819 MATCH_MP_TAC REAL_LE_INV2 THEN
820 SUBGOAL_THEN `&0 < &1 - (x / &4) pow 2` ASSUME_TAC THENL
822 REWRITE_TAC[REAL_ARITH `&0 < &1 - a <=> a < &1`] THEN
823 ONCE_REWRITE_TAC[REAL_ARITH `&1 = &1 pow 2`] THEN
824 MATCH_MP_TAC REAL_POW_LT2 THEN
825 REWRITE_TAC[ARITH_RULE `~(2 = 0)`] THEN
826 REPEAT (POP_ASSUM MP_TAC) THEN
832 MATCH_MP_TAC SQRT_POS_LT THEN
836 MATCH_MP_TAC REAL_LE_LSQRT THEN
837 ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
843 ONCE_REWRITE_TAC[REAL_ARITH `&1 - a <= b <=> &1 - b <= a`] THEN
844 REWRITE_TAC[REAL_POW_2] THEN
845 REWRITE_TAC[REAL_ARITH `a <= x / &4 * x / &4 <=> &16 * a <= x * x`] THEN
846 CONV_TAC REAL_RAT_REDUCE_CONV THEN
847 MATCH_MP_TAC REAL_LE_TRANS THEN
848 EXISTS_TAC `&2 * &2` THEN
851 CONV_TAC REAL_RAT_REDUCE_CONV;
852 REWRITE_TAC[GSYM REAL_POW_2] THEN
853 MATCH_MP_TAC REAL_POW_LE2 THEN
854 ASM_REWRITE_TAC[REAL_ARITH `&0 <= &2`]
860 let estimate2 = prove(`!x. &2 <= x /\ x <= #2.52
861 ==> (&2 * &2 * #2.52 * x * x - (&3969 / &625 + x * x - &4) * &126 / &25) / (&2 * #2.52 * x) pow 2 <= #0.13 /\
862 &0 <= (&2 * &2 * #2.52 * x * x - (&3969 / &625 + x * x - &4) * &126 / &25) / (&2 * #2.52 * x) pow 2`,
863 GEN_TAC THEN DISCH_TAC THEN
864 SUBGOAL_THEN `&0 < (&2 * #2.52 * x) pow 2` ASSUME_TAC THENL
866 MATCH_MP_TAC REAL_POW_LT THEN
867 POP_ASSUM MP_TAC THEN
871 ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_LE_RDIV_EQ; REAL_MUL_LZERO] THEN
872 ABBREV_TAC `t:real = x * x` THEN
873 SUBGOAL_THEN `&2 * &2 <= t /\ t <= #2.52 * #2.52` MP_TAC THENL
876 REWRITE_TAC[GSYM REAL_POW_2] THEN
877 CONJ_TAC THEN MATCH_MP_TAC REAL_POW_LE2 THEN ASM_REWRITE_TAC[] THENL
880 MATCH_MP_TAC REAL_LE_TRANS THEN
882 ASM_REWRITE_TAC[REAL_ARITH `&0 <= &2`]
887 REWRITE_TAC[REAL_POW_2] THEN
888 ASM_REWRITE_TAC[REAL_ARITH `(a * b * x) * a * b * x = (a * b) * (a * b) * (x * x)`] THEN
893 let estimate3 = prove(`!x. &2 <= x /\ x <= #2.52 ==>
894 inv (sqrt (&1 - ((&3969 / &625 + x * x - &4) / (&2 * #2.52 * x)) pow 2)) <= &2 /\
895 &0 <= inv (sqrt (&1 - ((&3969 / &625 + x * x - &4) / (&2 * #2.52 * x)) pow 2))`,
896 GEN_TAC THEN DISCH_TAC THEN
897 SUBGOAL_THEN `inv (&2) <= sqrt (&1 - ((&3969 / &625 + x * x - &4) / (&2 * #2.52 * x)) pow 2)` ASSUME_TAC THENL
899 MATCH_MP_TAC REAL_LE_RSQRT THEN
900 REWRITE_TAC[REAL_ARITH `a <= &1 - c <=> c <= &1 - a`; REAL_INV_INV] THEN
901 REWRITE_TAC[REAL_POW_DIV; REAL_POW_2] THEN
902 REWRITE_TAC[REAL_ARITH `(a * b * x) * a * b * x = (a * b * a * b) * x * x`] THEN
903 ABBREV_TAC `t:real = x * x` THEN
904 SUBGOAL_THEN `&4 <= t /\ t <= #6.3504` ASSUME_TAC THENL
906 REWRITE_TAC[REAL_ARITH `&4 = &2 * &2`; REAL_ARITH `#6.3504 = #2.52 * #2.52`] THEN
908 REWRITE_TAC[GSYM REAL_POW_2] THEN
909 CONJ_TAC THEN MATCH_MP_TAC REAL_POW_LE2 THEN ASM_REWRITE_TAC[] THENL
912 REPEAT (POP_ASSUM MP_TAC) THEN
918 CONV_TAC (DEPTH_CONV REAL_RAT_MUL_CONV) THEN
919 SUBGOAL_THEN `&0 < &15876 / &625 * t` ASSUME_TAC THENL
921 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
924 ASM_SIMP_TAC[REAL_LE_LDIV_EQ] THEN
925 REWRITE_TAC[REAL_ARITH `a + t - b = (a - b) + t`; REAL_ARITH `a * b * t = (a * b) * t`] THEN
926 CONV_TAC REAL_RAT_REDUCE_CONV THEN
927 REWRITE_TAC[REAL_ARITH `(a + t) * (a + t) <= b * t <=> (b / &2 - a - t) * (b / &2 - a - t) <= b * b / &4 - a * b`] THEN
928 CONV_TAC REAL_RAT_REDUCE_CONV THEN
929 MATCH_MP_TAC REAL_LE_TRANS THEN
930 EXISTS_TAC `&4 * &4` THEN
933 REWRITE_TAC[GSYM REAL_POW_2] THEN
934 MATCH_MP_TAC REAL_POW_LE2 THEN
935 FIRST_X_ASSUM (MP_TAC o check (is_conj o concl)) THEN
945 ONCE_REWRITE_TAC[REAL_ARITH `&2 = inv (inv (&2))`] THEN
946 MATCH_MP_TAC REAL_LE_INV2 THEN
947 ASM_REWRITE_TAC[REAL_ARITH `&0 < inv (&2)`; REAL_INV_INV];
951 MATCH_MP_TAC REAL_LE_INV THEN
952 MATCH_MP_TAC REAL_LE_TRANS THEN
953 EXISTS_TAC `inv (&2)` THEN
954 ASM_REWRITE_TAC[REAL_ARITH `&0 <= inv (&2)`]);;
958 (* arc 2 x 2 - arc (2 h0) x 2 >= 0.073 *)
960 let arc_lemma4 = prove(`!x. &2 <= x /\ x <= #2.52
961 ==> arclength (&2) x (&2) - arclength (#2.52) x (&2) >= #0.073`,
962 REPEAT STRIP_TAC THEN
963 REWRITE_TAC[REAL_ARITH `a - b >= c <=> b - a <= --c`] THEN
964 MATCH_MP_TAC REAL_LE_TRANS THEN
965 EXISTS_TAC `arclength #2.52 #2.52 (&2) - arclength (&2) #2.52 (&2)` THEN
966 REWRITE_TAC[REWRITE_RULE [REAL_ARITH `a - b >= c <=> b - a <= --c`] estimate0] THEN
967 ONCE_REWRITE_TAC[arc_sym] THEN
968 MP_TAC (SPECL [`\x. arclength x #2.52 (&2) - arclength x (&2) (&2)`;
969 `\x. (&2 * &2 * #2.52 * x * x - (&3969 / &625 + x * x - &4) * &126 / &25) / (&2 * #2.52 * x) pow 2 *
970 --inv (sqrt (&1 - ((&3969 / &625 + x * x - &4) / (&2 * #2.52 * x)) pow 2)) -
971 &1 / &4 * --inv (sqrt (&1 - (x / &4) pow 2))`;
972 `real_interval [&2, #2.52]`]
973 HAS_REAL_DERIVATIVE_INCREASING) THEN
977 REWRITE_TAC[IS_REALINTERVAL_INTERVAL] THEN
980 REWRITE_TAC[NOT_EXISTS_THM] THEN GEN_TAC THEN
982 SUBGOAL_THEN `&2 = a /\ #2.52 = a` MP_TAC THENL
984 REWRITE_TAC[GSYM IN_SING] THEN
985 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
986 REWRITE_TAC[IN_REAL_INTERVAL] THEN
994 REWRITE_TAC[IN_REAL_INTERVAL] THEN
995 X_GEN_TAC `y:real` THEN DISCH_TAC THEN
996 MATCH_MP_TAC HAS_REAL_DERIVATIVE_SUB THEN
999 MP_TAC (SPECL [`y:real`; `#2.52`] arc_derivative) THEN
1002 ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
1005 REWRITE_TAC[REAL_ARITH `(y + y) * a * y * b = &2 * a * b * y * y`] THEN
1006 ONCE_REWRITE_TAC[REAL_ARITH `a + b - &4 = b + (a - &4)`] THEN
1007 CONV_TAC REAL_RAT_REDUCE_CONV THEN
1008 REWRITE_TAC[REAL_ARITH `&2 * y * #2.52 = &2 * #2.52 * y`];
1011 MP_TAC (SPECL [`y:real`; `&2`] arc_derivative) THEN
1014 ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
1017 CONV_TAC REAL_RAT_REDUCE_CONV THEN
1018 REWRITE_TAC[REAL_ARITH `(y + y) * &2 * y * &2 - (y * y + &0) * &4 = &4 * (y pow 2)`] THEN
1019 ASM_SIMP_TAC[REAL_FIELD `&2 <= y ==> ((y * y + &0) / (&2 * y * &2)) pow 2 = (y / &4) pow 2`] THEN
1020 ASM_SIMP_TAC[REAL_FIELD `&2 <= y ==> (&4 * y pow 2) / (&2 * y * &2) pow 2 = &1 / &4`];
1027 FIRST_ASSUM (fun th -> SUBGOAL_THEN ((fst o dest_eq o concl) th) MP_TAC) THENL
1029 REPEAT (POP_ASSUM (fun th -> ALL_TAC)) THEN
1030 REWRITE_TAC[IN_REAL_INTERVAL] THEN
1031 REPEAT STRIP_TAC THEN
1032 MATCH_MP_TAC (REAL_ARITH `(?c d. c <= a /\ b <= d /\ &0 <= c - d) ==> &0 <= a - b`) THEN
1033 MAP_EVERY EXISTS_TAC [`#0.13 * (-- &2)`; `-- #0.28`] THEN
1036 REWRITE_TAC[REAL_ARITH `a * --b <= c * --d <=> c * d <= a * b`] THEN
1037 MATCH_MP_TAC REAL_LE_MUL2 THEN
1038 ASM_SIMP_TAC[estimate2; estimate3];
1042 ASM_SIMP_TAC[estimate1] THEN
1047 POP_ASSUM (fun th -> REWRITE_TAC[th]) THEN
1048 DISCH_THEN (MP_TAC o SPECL [`x:real`; `#2.52`]) THEN
1049 ASM_REWRITE_TAC[IN_REAL_INTERVAL; REAL_ARITH `&2 <= #2.52 /\ #2.52 <= #2.52`]
1056 (* arclength (2 h0) (2 h0) 2 >= 0.816 *)
1058 let arc_lemma5 = prove(`arclength #2.52 #2.52 (&2) >= #0.816`,
1059 SUBGOAL_THEN `arclength #2.52 #2.52 (&2) = acs ((#2.52 * #2.52 + #2.52 * #2.52 - (&2) * (&2)) / (&2 * #2.52 * #2.52))` (fun th -> REWRITE_TAC[th]) THENL
1061 MATCH_MP_TAC Trigonometry1.ACS_ARCLENGTH THEN
1066 CONV_TAC (REAL_RAT_REDUCE_CONV) THEN
1067 SUBGOAL_THEN `#0.816 = acs (cos (#0.816))` MP_TAC THENL
1069 MATCH_MP_TAC (GSYM ACS_COS) THEN
1070 MP_TAC PI_APPROX_32 THEN
1074 DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th]) THEN
1075 REWRITE_TAC[real_ge] THEN
1076 MATCH_MP_TAC ACS_MONO_LE THEN
1077 REWRITE_TAC[COS_BOUNDS] THEN
1080 CONV_TAC REAL_RAT_LE_CONV;
1081 MP_TAC (CONJUNCT1 (REWRITE_RULE [ABS_LE_BOUNDS] (cos_eval `#0.816` 2))) THEN