SET_INDUCT_TAC

pred_setLib.SET_INDUCT_TAC : tactic

Tactic for induction on finite sets.

SET_INDUCT_TAC is an induction tacic for proving properties of finite sets. When applied to a goal of the form

   !s. FINITE s ==> P[s]

SET_INDUCT_TAC reduces this goal to proving that the property \s.P[s] holds of the empty set and is preserved by insertion of an element into an arbitrary finite set. Since every finite set can be built up from the empty set {} by repeated insertion of values, these subgoals imply that the property \s.P[s] holds of all finite sets.

The tactic specification of SET_INDUCT_TAC is:

                 A ?- !s. FINITE s ==> P
   ==========================================================  SET_INDUCT_TAC
     A |- P[{{}}/s]
     A u {FINITE s', P[s'/s], ~e IN s'} ?- P[e INSERT s'/s]

where e is a variable chosen so as not to appear free in the assumptions A, and s' is a primed variant of s that does not appear free in A (usually, s' is just s).

Failure

SET_INDUCT_TAC (A,g) fails unless g has the form !s. FINITE s ==> P, where the variable s has type ty->bool for some type ty.