Tactic to automate some routine pred_set theory by reduction to FOL,
using the given theorems as additional assumptions in the search.
LIBRARY
boss
DESCRIPTION
SET_TAC reduces basic set-theoretic operators (IN, SUBSET,
PSUBSET, INTER, UNION, INSERT, DELETE, REST, DISJOINT,
BIGINTER, BIGUNION, IMAGE, SING and GSPEC) in the goal to
their definitions in first-order logic (FOL) and then call METIS_TAC
to solve it. With SET_TAC, many simple set-theoretic results can be
directly proved without finding needed lemmas in pred_setTheory.
FAILURE
Fails if the underlying resolution machinery (METIS_TAC) cannot
prove the goal, or the supplied theorems are not enough for the FOL
reduction, e.g., when there are other set-theoretic operators in the goal.
EXAMPLE
A simple theorem about disjoint sets:
Theorem DISJOINT_RESTRICT_L :
!s t c. DISJOINT s t ==> DISJOINT (s INTER c) (t INTER c)
Proof SET_TAC []
QED
USES
SET_TAC can only progress the goal to a successful proof of the
(whole) goal or not at all. SET_RULE can be used to prove an
intermediate set-theoretic lemma (there is no way to provide extra
lemmas, however).
COMMENTS
The assumptions of a goal are ignored when SET_TAC is applied. To
include assumptions use ASM_SET_TAC.