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 LIST_INDUCT_TAC
\TYPE {LIST_INDUCT_TAC : tactic}
\SYNOPSIS
Performs tactical proof by structural induction on lists.
\KEYWORDS
tactic, list, induction.
\DESCRIBE
{LIST_INDUCT_TAC} reduces a goal {!l.P[l]}, where {l} ranges over lists, to two
subgoals corresponding to the base and step cases in a proof by structural
induction on {l}. The induction hypothesis appears among the assumptions of the
subgoal for the step case. The specification of {LIST_INDUCT_TAC} is:
{
A ?- !l. P
===================================================== LIST_INDUCT_TAC
A |- P[NIL/l] A u {{P[l'/l]}} ?- !h. P[CONS h l'/l]
}
\noindent where {l'} is a primed variant of {l} that does not appear free in
the assumptions {A} (usually, {l'} is just {l}). When {LIST_INDUCT_TAC} is
applied to a goal of the form {!l.P}, where {l} does not appear free in {P},
the subgoals are just {A ?- P} and {A u {{P}} ?- !h.P}.
\FAILURE
{LIST_INDUCT_TAC g} fails unless the conclusion of the goal {g} has the form
{!l.t}, where the variable {l} has type {(ty)list} for some type {ty}.
\SEEALSO
LIST_INDUCT.
\ENDDOC
|
