1 needs "Library/analysis.ml";;
2 needs "Library/transc.ml";;
5 `(!x. cheb 0 x = &1) /\
7 (!n x. cheb (n + 2) x = &2 * x * cheb (n + 1) x - cheb n x)`;;
9 let CHEB_INDUCT = prove
10 (`!P. P 0 /\ P 1 /\ (!n. P n /\ P(n + 1) ==> P(n + 2)) ==> !n. P n`,
11 GEN_TAC THEN STRIP_TAC THEN
12 SUBGOAL_THEN `!n. P n /\ P(n + 1)` (fun th -> MESON_TAC[th]) THEN
13 INDUCT_TAC THEN ASM_SIMP_TAC[ADD1; GSYM ADD_ASSOC] THEN
14 ASM_SIMP_TAC[ARITH]);;
17 (`!n x. cheb n (cos x) = cos(&n * x)`,
18 MATCH_MP_TAC CHEB_INDUCT THEN
19 REWRITE_TAC[cheb; REAL_MUL_LZERO; REAL_MUL_LID; COS_0] THEN
21 ASM_REWRITE_TAC[GSYM REAL_OF_NUM_ADD; REAL_MUL_LID; REAL_ADD_RDISTRIB] THEN
22 REWRITE_TAC[COS_ADD; COS_DOUBLE; SIN_DOUBLE] THEN
23 MP_TAC(SPEC `x:real` SIN_CIRCLE) THEN CONV_TAC REAL_RING);;
25 let CHEB_RIPPLE = prove
26 (`!x. abs(x) <= &1 ==> abs(cheb n x) <= &1`,
27 REWRITE_TAC[GSYM REAL_BOUNDS_LE] THEN
28 MESON_TAC[CHEB_COS; ACS_COS; COS_BOUNDS]);;
31 let add_tm = `(+):num->num->num`
34 let m = mk_numeral(dest_numeral tm -/ Int 2) in
35 let tm' = mk_comb(mk_comb(add_tm,m),two_tm) in
36 SYM(NUM_ADD_CONV tm');;
39 let [pth0;pth1;pth2] = CONJUNCTS cheb in
41 (GEN_REWRITE_CONV I [pth0; pth1] ORELSEC
42 (LAND_CONV NUM_ADD2_CONV THENC
43 GEN_REWRITE_CONV I [pth2] THENC
45 (funpow 3 RAND_CONV ((LAND_CONV NUM_ADD_CONV) THENC conv))
47 REAL_POLY_CONV)) tm in
50 CHEB_CONV `cheb 8 x`;;
53 (`!n x. ((x - &1) * (cheb (2 * n + 1) x - &1) =
54 (cheb (n + 1) x - cheb n x) pow 2) /\
55 (&2 * (x pow 2 - &1) * (cheb (2 * n + 2) x - &1) =
56 (cheb (n + 2) x - cheb n x) pow 2)`,
57 ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN GEN_TAC THEN
58 MATCH_MP_TAC CHEB_INDUCT THEN
59 REWRITE_TAC[ARITH; cheb; CHEB_CONV `cheb 2 x`; CHEB_CONV `cheb 3 x`] THEN
61 (REWRITE_TAC[GSYM ADD_ASSOC; LEFT_ADD_DISTRIB; ARITH] THEN
62 REWRITE_TAC[ARITH_RULE `n + 5 = (n + 3) + 2`;
63 ARITH_RULE `n + 4 = (n + 2) + 2`;
64 ARITH_RULE `n + 3 = (n + 1) + 2`;
69 let IVT_LEMMA1 = prove
71 ==> !x y. f(x) <= &0 /\ &0 <= f(y) ==> ?x. f(x) = &0`,
72 ASM_MESON_TAC[IVT; IVT2; REAL_LE_TOTAL]);;
74 let IVT_LEMMA2 = prove
75 (`!f. (!x. f contl x) /\ (?x. f(x) <= x) /\ (?y. y <= f(y)) ==> ?x. f(x) = x`,
76 REPEAT STRIP_TAC THEN MP_TAC(SPEC `\x. f x - x` IVT_LEMMA1) THEN
77 ASM_SIMP_TAC[CONT_SUB; CONT_X] THEN
78 SIMP_TAC[REAL_LE_SUB_LADD; REAL_LE_SUB_RADD; REAL_SUB_0; REAL_ADD_LID] THEN
81 let SARKOVSKII_TRIVIAL = prove
82 (`!f:real->real. (!x. f contl x) /\ (?x. f(f(f(x))) = x) ==> ?x. f(x) = x`,
83 REPEAT STRIP_TAC THEN MATCH_MP_TAC IVT_LEMMA2 THEN ASM_REWRITE_TAC[] THEN
84 CONJ_TAC THEN MATCH_MP_TAC
85 (MESON[] `P x \/ P (f x) \/ P (f(f x)) ==> ?x:real. P x`) THEN
86 FIRST_ASSUM(UNDISCH_TAC o check is_eq o concl) THEN REAL_ARITH_TAC);;