SET_RULE : term -> thm

SYNOPSIS
Attempt to prove elementary set-theoretic lemma.

DESCRIPTION
The function SET_RULE is a crude automated prover for set-theoretic facts. When applied to a term, it expands various set-theoretic definitions explicitly and then attempts to solve the result using MESON.

FAILURE CONDITIONS
Fails if the simple translation does not suffice, or the resulting goal is too deep for MESON.

EXAMPLE
  # SET_RULE `{x | ~(x IN s <=> x IN t)} = (s DIFF t) UNION (t DIFF s)`;;
  ...
  val it : thm = |- {x | ~(x IN s <=> x IN t)} = s DIFF t UNION t DIFF s

  # SET_RULE
     `UNIONS {t y | y IN x INSERT s} = t x UNION UNIONS {t y | y IN s}`;;
  val it : thm =
    |- UNIONS {t y | y IN x INSERT s} = t x UNION UNIONS {t y | y IN s}

SEE ALSO
MESON, MESON_TAC[], SET_TAC.