19 Real analysis (1)

　次の２つのパッケージの使用例を示します．OCamlの#useの代わりに，HOL Lightのneedsを使うとファイルのリロードが防げます．

needs "Library/analysis.ml";;
needs "Library/transc.ml";;

　まずは，チェビシェフの多項式

# let cheb = define
`(!x. cheb 0 x = &1) /\
(!x. cheb 1 x = x) /\
(!n x. cheb (n + 2) x = &2 * x * cheb (n + 1) x - cheb n x)`;;
val cheb : thm =
|- (!x. cheb 0 x = &1) /\
(!x. cheb 1 x = x) /\
(!n x. cheb (n + 2) x = &2 * x * cheb (n + 1) x - cheb n x)

が余弦のn倍角公式

# g `!n x. cheb n (cos x) = cos(&n * x)`;;
val it : goalstack = 1 subgoal (1 total)

`!n x. cheb n (cos x) = cos (&n * x)`

を与えることの証明です．証明には２ステップの仮定をとる帰納法を用いますが，先に証明した

# num2_INDUCTION;;
val it : thm =
|- !P. P 0 /\ P 1 /\ (!n. P n /\ P (SUC n) ==> P (SUC (SUC n)))
==> (!n. P n)

ではなく

# [ADD1; GSYM ADD_ASSOC];;
val it : thm list =
[|- !m. SUC m = m + 1; |- !m n p. (m + n) + p = m + n + p]

を参照して，SUCを消去した

# let CHEB_INDUCT = prove
(`!P. P 0 /\ P 1 /\ (!n. P n /\ P(n + 1) ==> P(n + 2)) ==> !n. P n`,
GEN_TAC THEN STRIP_TAC THEN
SUBGOAL_THEN `!n. P n /\ P(n + 1)` (fun th -> MESON_TAC[th]) THEN
INDUCT_TAC THEN ASM_SIMP_TAC[ADD1; GSYM ADD_ASSOC] THEN
ASM_SIMP_TAC[ARITH]);;
0..0..solved at 2
val ( CHEB_INDUCT ) : thm =
|- !P. P 0 /\ P 1 /\ (!n. P n /\ P (n + 1) ==> P (n + 2)) ==> (!n. P n)

を用います．なお，上の

SUBGOAL_THEN `!n. P n /\ P(n + 1)` (fun th -> MESON_TAC[th])

の部分は MESON_TAC[s] により t が証明できるとき
SUBGOAL_THEN s (fun s -> MESON_TAC[s]):
({A1;...;An} ?- t) |-> ({A1;...;An} ?- s)
例えば

# g `a \/ b`;;
Warning: Free variables in goal: a, b
val it : goalstack = 1 subgoal (1 total)

`a \/ b`

# e (SUBGOAL_THEN `a:bool` (fun s -> MESON_TAC[s]) );;
val it : goalstack = 1 subgoal (1 total)

`a`

のように，t をその十分条件である s に置き換えるテクニックであり，例えば

# g `a \/ b`;;
Warning: Free variables in goal: a, b
val it : goalstack = 1 subgoal (1 total)

`a \/ b`

# e (MATCH_MP_TAC (MESON[]`a==>(a\/b)`) );;
val it : goalstack = 1 subgoal (1 total)

`a`

でも結果は同じですが，MESON_TACを用いれば，sからtを導く際にASMを参照して ASM_MESON_TAC[s] とすることも可能です．

　num2_INDUCTION の改訂版を幾つか書いておきます．

# let num2_INDUCTION = prove(
`!P. P 0 /\ P 1 /\ (!n. P n /\ P (n+1) ==> P (n+2) ) ==> (!n. P n)` ,
( REPEAT STRIP_TAC THEN SUBGOAL_THEN `!n. P n /\ P (n+1)` (fun th -> MESON_TA
C[th]) ) THEN
( INDUCT_TAC ) THEN
( ASM_SIMP_TAC[ADD1;GSYM ADD_ASSOC] ) THEN
( ASM_SIMP_TAC[ARITH] ) );;
0..0..solved at 2
val num2_INDUCTION : thm =
|- !P. P 0 /\ P 1 /\ (!n. P n /\ P (n + 1) ==> P (n + 2)) ==> (!n. P n)
#
let num2_INDUCTION = prove(
`!P. P 0 /\ P 1 /\ (!n. P n /\ P (n+1) ==> P (n+2)) ==> (!n. P n)`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN `!n. P n /\ P (n+1)` ASSUME_TAC THENL
[ INDUCT_TAC THEN ASM_SIMP_TAC[ADD1;GSYM ADD_ASSOC] THEN ASM_SIMP_TAC[ARITH];
ASM_SIMP_TAC[] ] );;
val num2_INDUCTION : thm =
|- !P. P 0 /\ P 1 /\ (!n. P n /\ P (n + 1) ==> P (n + 2)) ==> (!n. P n)