SET_INDUCT_TAC : tactic

- STRUCTURE
- SYNOPSIS
- Tactic for induction on finite sets.
- LIBRARY
- pred_set
- DESCRIPTION
- SET_INDUCT_TAC is an induction tacic for proving properties of finite sets. When applied to a goal of the formSET_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.
!s. FINITE s ==> P[s]

The tactic specification of SET_INDUCT_TAC is:

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).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]

- 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.

HOL Kananaskis-14