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);;