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