Update from HH
[hl193./.git] / Tutorial / Real_analysis.ml
1 needs "Library/analysis.ml";;
2 needs "Library/transc.ml";;
3
4 let cheb = define
5  `(!x. cheb 0 x = &1) /\
6   (!x. cheb 1 x = x) /\
7   (!n x. cheb (n + 2) x = &2 * x * cheb (n + 1) x - cheb n x)`;;
8
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]);;
15
16 let CHEB_COS = prove
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
20   REPEAT STRIP_TAC 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);;
24
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]);;
29
30 let NUM_ADD2_CONV =
31   let add_tm = `(+):num->num->num`
32   and two_tm = `2` in
33   fun tm ->
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');;
37
38 let CHEB_CONV =
39   let [pth0;pth1;pth2] = CONJUNCTS cheb in
40   let rec conv tm =
41    (GEN_REWRITE_CONV I [pth0; pth1] ORELSEC
42     (LAND_CONV NUM_ADD2_CONV THENC
43      GEN_REWRITE_CONV I [pth2] THENC
44      COMB2_CONV
45       (funpow 3 RAND_CONV ((LAND_CONV NUM_ADD_CONV) THENC conv))
46       conv THENC
47      REAL_POLY_CONV)) tm in
48   conv;;
49
50 CHEB_CONV `cheb 8 x`;;
51
52 let CHEB_2N1 = prove
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
60   REPEAT(CHANGED_TAC
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`;
65
66                 cheb])) THEN
67   CONV_TAC REAL_RING);;
68
69 let IVT_LEMMA1 = prove
70  (`!f. (!x. f contl x)
71        ==> !x y. f(x) <= &0 /\ &0 <= f(y) ==> ?x. f(x) = &0`,
72   ASM_MESON_TAC[IVT; IVT2; REAL_LE_TOTAL]);;
73
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
79   ASM_MESON_TAC[]);;
80
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);;