1\DOC SET_INDUCT_TAC
2
3\TYPE {SET_INDUCT_TAC : tactic}
4
5\SYNOPSIS
6Tactic for induction on finite sets.
7
8\LIBRARY pred_set
9
10\DESCRIBE
11{SET_INDUCT_TAC} is an induction tacic for proving properties of finite
12sets.  When applied to a goal of the form
13{
14   !s. FINITE s ==> P[s]
15}
16{SET_INDUCT_TAC} reduces this goal to proving that the property
17{\s.P[s]} holds of the empty set and is preserved by insertion of an element
18into an arbitrary finite set.  Since every finite set can be built up from the
19empty set {{}} by repeated insertion of values, these subgoals imply that
20the property {\s.P[s]} holds of all finite sets.
21
22The tactic specification of {SET_INDUCT_TAC} is:
23{
24                 A ?- !s. FINITE s ==> P
25   ==========================================================  SET_INDUCT_TAC
26     A |- P[{{}}/s]
27     A u {FINITE s', P[s'/s], ~e IN s'} ?- P[e INSERT s'/s]
28}
29where {e} is a variable chosen so as not to appear free in the
30assumptions {A}, and {s'} is a primed variant of {s} that does not appear free
31in {A} (usually, {s'} is just {s}).
32
33\FAILURE
34{SET_INDUCT_TAC (A,g)} fails unless {g} has the form {!s. FINITE s ==> P},
35where the variable {s} has type {ty->bool} for some type {ty}.
36
37\ENDDOC
38