1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
\DOC INDUCT
\TYPE {INDUCT : ((thm # thm) -> thm)}
\SYNOPSIS
Performs a proof by mathematical induction on the natural numbers.
\KEYWORDS
rule, induction.
\DESCRIBE
The derived inference rule {INDUCT} implements the rule of mathematical
induction:
{
A1 |- P[0] A2 |- !n. P[n] ==> P[SUC n]
----------------------------------------------- INDUCT
A1 u A2 |- !n. P[n]
}
\noindent When supplied with a theorem {A1 |- P[0]}, which asserts the base
case of a proof of the proposition {P[n]} by induction on {n}, and the theorem
{A2 |- !n. P[n] ==> P[SUC n]}, which asserts the step case in the induction on
{n}, the inference rule {INDUCT} returns {A1 u A2 |- !n. P[n]}.
\FAILURE
{INDUCT th1 th2} fails if the theorems {th1} and {th2} do not have the forms
{A1 |- P[0]} and {A2 |- !n. P[n] ==> P[SUC n]} respectively.
\SEEALSO
INDUCT_TAC.
\ENDDOC
|
