Examples (4)

　等差数列の和の公式の証明です．
:num 版

# g`(?a b. !n. x n = a * n + b)==>(!n m. 2 * nsum(m..m+n) x = (SUC n)*( x m + x
(m+n) ) )`;;
Warning: Free variables in goal: x
val it : goalstack = 1 subgoal (1 total)

`(?a b. !n. x n = a * n + b)
==> (!n m. 2 * nsum (m..m + n) x = SUC n * (x m + x (m + n)))`

# e STRIP_TAC;;
val it : goalstack = 1 subgoal (1 total)

0 [`!n. x n = a * n + b`]

`!n m. 2 * nsum (m..m + n) x = SUC n * (x m + x (m + n))`

# e INDUCT_TAC;;
val it : goalstack = 2 subgoals (2 total)

0 [`!n. x n = a * n + b`]
1 [`!m. 2 * nsum (m..m + n) x = SUC n * (x m + x (m + n))`]

`!m. 2 * nsum (m..m + SUC n) x = SUC (SUC n) * (x m + x (m + SUC n))`

0 [`!n. x n = a * n + b`]

`!m. 2 * nsum (m..m + 0) x = SUC 0 * (x m + x (m + 0))`

# e ( REWRITE_TAC[ADD_CLAUSES;NSUM_CLAUSES_NUMSEG;NSUM_SING_NUMSEG] THEN ARITH_T
AC);;
val it : goalstack = 1 subgoal (1 total)

0 [`!n. x n = a * n + b`]
1 [`!m. 2 * nsum (m..m + n) x = SUC n * (x m + x (m + n))`]

`!m. 2 * nsum (m..m + SUC n) x = SUC (SUC n) * (x m + x (m + SUC n))`

# e ( REWRITE_TAC[ADD_CLAUSES;NSUM_CLAUSES_NUMSEG;NSUM_SING_NUMSEG;ARITH_RULE`m<
=SUC(m+n)`]);;
val it : goalstack = 1 subgoal (1 total)

0 [`!n. x n = a * n + b`]
1 [`!m. 2 * nsum (m..m + n) x = SUC n * (x m + x (m + n))`]

`!m. 2 * (nsum (m..m + n) x + x (SUC (m + n))) =
SUC (SUC n) * (x m + x (SUC (m + n)))`

# e ( ASM_REWRITE_TAC[ARITH_RULE`2*(a+b)=2*a+2*b`] );;
val it : goalstack = 1 subgoal (1 total)

0 [`!n. x n = a * n + b`]
1 [`!m. 2 * nsum (m..m + n) x = SUC n * (x m + x (m + n))`]

`!m. SUC n * ((a * m + b) + a * (m + n) + b) + 2 * a * SUC (m + n) + 2 * b =
SUC (SUC n) * ((a * m + b) + a * SUC (m + n) + b)`

# e ( ARITH_TAC );;
val it : goalstack = No subgoals

:real 版

g`(?a b. !n. x n = a * &n + b)
==> (!n m. sum (m..m + n) x = &(SUC n) * (x m + x (m + n)) / &2)`
e( STRIP_TAC );;
e( INDUCT_TAC );;
e( REWRITE_TAC [ADD_CLAUSES; SUM_SING_NUMSEG] THEN ARITH_TAC );;
e( ASM_REWRITE_TAC [ADD_CLAUSES; SUM_CLAUSES_NUMSEG; REAL;
ARITH_RULE `m <= SUC (m + n)`; GSYM REAL_ADD] THEN ARITH_TAC );;

まとめると

# prove
(`(?a b. !n. x n = a * &n + b)
==> (!n m. sum (m..m + n) x = &(SUC n) * (x m + x (m + n)) / &2)`,
STRIP_TAC THEN INDUCT_TAC THEN
ASM_REWRITE_TAC [ADD_CLAUSES; SUM_SING_NUMSEG; SUM_CLAUSES_NUMSEG; REAL;
ARITH_RULE `m <= SUC (m + n)`; GSYM REAL_ADD] THEN ARITH_TAC);;
val it : thm =
|- (?a b. !n. x n = a * &n + b)
==> (!n m. sum (m..m + n) x = &(SUC n) * (x m + x (m + n)) / &2)