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
32
33
|
\DOC INDUCT_TAC
\TYPE {INDUCT_TAC : tactic}
\SYNOPSIS
Performs tactical proof by mathematical induction on the natural numbers.
\KEYWORDS
tactic, induction.
\DESCRIBE
{INDUCT_TAC} reduces a goal {!n.P[n]}, where {n} has type {num}, to two
subgoals corresponding to the base and step cases in a proof by mathematical
induction on {n}. The induction hypothesis appears among the assumptions of the
subgoal for the step case. The specification of {INDUCT_TAC} is:
{
A ?- !n. P
======================================== INDUCT_TAC
A ?- P[0/n] A u {{P}} ?- P[SUC n'/n]
}
\noindent where {n'} is a primed variant of {n} that does not appear free in
the assumptions {A} (usually, {n'} just equals {n}). When {INDUCT_TAC} is
applied to a goal of the form {!n.P}, where {n} does not appear free in {P},
the subgoals are just {A ?- P} and {A u {{P}} ?- P}.
\FAILURE
{INDUCT_TAC g} fails unless the conclusion of the goal {g} has the form {!n.t},
where the variable {n} has type {num}.
\SEEALSO
INDUCT.
\ENDDOC
|
