Example (13)

　今回は Example(11)のmy_thm02の応用として
\forall x:N\to R. \forall a\in R. \lim_{n\to\infty}(x_n-x_{n-1})=a \. \rightarrow\. \lim_{n\to\infty}\displaystyle\frac{x_n}{n}=a
を証明します．まずは

g`!x a. (\n. x n - x (n-1) ) tends_num_real a ==> (\n. (x n - x 0) / &n ) tends_num_real a`;;
e(REPEAT STRIP_TAC THEN SIMP_TAC[SEQ] THEN REPEAT STRIP_TAC);;
let lemma02 = SPECL[`a:real`;`(\k:num. (x:num->real) k - x (k-1) )`]my_thm02;;
e(MP_TAC (lemma02) THEN ASM_SIMP_TAC[SEQ] THEN DISCH_THEN(MP_TAC o (SPEC`e:real`)) THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC THEN EXISTS_TAC `N+1` THEN REPEAT STRIP_TAC THEN FIRST_X_ASSUM( MP_TAC o SPEC`n:num` ) THEN ASM_SIMP_TAC[ARITH_RULE`n>=N+1==>n>=N`] );;
let lemma01 = ( CONV_RULE(ONCE_DEPTH_CONV BETA_CONV THENC SIMP_CONV[ARITH_RULE`(n+1)-1=n/\1-1=0`])(INST [`(\n:num. (x:num->real) (n-1) )`,`f:num->real`] (DISCH_ALL(ADD_ASSUM`1<=n`(SPECL[`1`;`n:num`]SUM_DIFFS_ALT) ) ) ) );;
e(ASSUME_TAC (UNDISCH(ARITH_RULE`n>=N+1==>1<=n`)) );;
e(ASM_SIMP_TAC[lemma01] );;
let lemma03=top_thm();;

そして

g`!x a. (\n. x n - x (n-1) ) tends_num_real a ==> (\n. x n / &n ) tends_num_real a`;;
e(REPEAT STRIP_TAC THEN MP_TAC (SPEC_ALL lemma03) THEN ASM_SIMP_TAC[] THEN REPEAT STRIP_TAC THEN ASSUME_TAC (SPEC`(x:num->real) 0`SEQ_HARMONIC) );;
e(MP_TAC (SPECL[`(\n. (x n - x 0) / &n)`;`a:real`;`(\n. x 0 / &n)`;`&0`]SEQ_ADD) THEN ASM_SIMP_TAC[REAL_FIELD`(x n - x 0) / &n + x 0 / &n= x n/ &n`; REAL_ARITH`a+(&0)=a`]);;
let my_thm07=top_thm();;

となります．