/usr/share/hol88-2.02.19940316/help/ENTRIES/INDUCT.doc is in hol88-help 2.02.19940316-35.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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
|